Simple Main/SemSyn split
[darcs-mirror-sem_syn.git] / SemSyn.hs
1 {-# OPTIONS -XFlexibleInstances #-}
2
3 module SemSyn where
4
5 import Text.PrettyPrint
6 import Control.Monad.State
7 import Control.Monad.Error
8 import Data.List
9 import Data.Maybe (fromJust, isNothing, isJust)
10 import Debug.Trace 
11
12 import Data.Function (on)
13
14 import Data.Map (Map)
15 import qualified Data.Map as Map
16
17 import Data.Set (Set)
18 import qualified Data.Set as Set
19
20 import Data.Graph 
21
22 import Util 
23 import AST
24
25 import Parser
26 import Type
27 import Shapify
28 import CodeGen 
29
30
31 data Config 
32     = Config 
33       { 
34         inputFile   :: Maybe String, -- ^ Path to input file
35         execMode    :: ExecMode,
36         outputMode  :: OutputMode, 
37         isShowType  :: Bool
38       }
39
40 data ExecMode 
41     = Normal | Shapify | ShapifyPlus | Help | Debug 
42
43 data OutputMode = PseudoCode | HaskellCode | ForwardCode
44
45 defaultConfig = Config { 
46                   inputFile   = Nothing, 
47                   execMode    = Normal, 
48                   outputMode  = PseudoCode,
49                   isShowType  = True  }
50
51
52 outputCode :: Config -> Bool -> AST -> AST -> IO ()
53 outputCode conf isShapify orig ast =
54     let (p1,p2,p3) = constructBwdFunction ast
55     in case outputMode conf of 
56          ForwardCode -> 
57              do print $ ppr (typeFilter ast)
58          PseudoCode  ->
59              do print $ ppr (constructTypeDecl p2)
60                 print $ ppr orig $$  ppr (typeFilter p1) $$ ppr (typeFilter p2) $$ ppr (typeFilterT p3)
61          HaskellCode ->
62              do putStrLn $ "import Control.Monad"
63                 putStrLn $ "import BUtil"
64                 when isShapify $
65                      print $ vcat $ map genBwdDef 
66                                (let AST decls = typeInference orig
67                                 in map (\(Decl f t _ _:_) -> (f,t)) $ 
68                                      groupBy isSameFunc decls)
69                 print $ ppr (constructTypeDecl p2)
70                 print $ ppr $ generateCodeBwd (orig,p1,p2,p3)
71     where
72       typeFilter  = if isShowType conf then id else eraseType
73       typeFilterT = if isShowType conf then id else eraseTypeT
74       genBwdDef (Name fName,(TFun is ts t)) =
75           case (ts,t) of 
76             ([TCon (Name "List") [TVar i]],TCon (Name "List") [TVar j]) | i == j  ->
77                 ppr (Name fName) <> text "_Bb bias s v" $$
78                   nest 4 (text "= gen_put_bias bias Main." <> ppr (Name fName) 
79                                <> text "(\\x y -> castError $ (" 
80                                <> ppr (NBwd $ IName fName is)
81                                <> text " $! x) $! y) s v" ) $$
82                 ppr (Name fName) <> text "_Bbd = withDefaultBias "
83                     <> ppr (Name fName) <> text "_Bb" $$
84                 ppr (Name fName) <> text "_Bd = withDefault "
85                     <> ppr (Name fName) <> text "_B" $$
86                 ppr (Name fName) <> text "_B s v = " 
87                   <> ppr (Name fName) <> text "_Bb rear s v" 
88             _ ->
89                 empty
90                                   
91
92
93 checkTreeless :: AST -> Bool
94 checkTreeless (AST decls) = all checkTreelessD decls
95     where
96       checkTreelessD (Decl _ _ _ e) = checkTreelessE e
97       checkTreelessE (EVar _ _ _)    = True
98       checkTreelessE (ECon _ _ _ es) = all checkTreelessE es
99       checkTreelessE (EFun _ _ _ es) = all isVariable es
100       isVariable (EVar _ _ _) = True
101       isVariable _            = False
102
103 checkAffine :: AST -> Bool 
104 checkAffine (AST decls) = all checkAffineD decls
105     where
106       checkAffineD (Decl _ _ _ e) = checkAffineE e 
107       checkAffineE e = (varsE e == snub (varsE e))
108       varsE (EVar _ _ v) = [v]
109       varsE (ECon _ _ _ es) = concatMap varsE es
110       varsE (EFun _ _ _ es) = concatMap varsE es
111
112
113            
114 type Automaton s = Map s [Deriv s]
115 data Deriv s    = DCon Name [s]
116                 | DEps s 
117                 | DAny
118
119 pprAM :: (Ppr a, Ppr t) => Map t [Deriv a] -> Doc
120 pprAM am = 
121     vcat $ map pprDs $ Map.toList am
122     where
123       pprDs (i,ds) = 
124           ppr i $$
125           nest 4 (vcat $ map (\d -> text " -> " <> pprD d) ds)
126       pprD (DAny)      = text "_" 
127       pprD (DEps s)    = ppr s
128       pprD (DCon c ss) = ppr c <> parens (hcat $ punctuate comma (map ppr ss))
129
130 data AState = ASType Int
131             | ASExp  Int
132             | ASFun  Name
133      deriving (Eq,Ord)
134
135 instance Ppr AState where
136     ppr (ASType i) = text $ "T" ++ show i 
137     ppr (ASExp  x) = text $ "E" ++ show x
138     ppr (ASFun  n) = text $ "F" ++ show n
139
140 instance Show AState where
141     show = show . ppr 
142
143 initTAMap :: Type -> State Int (AState, Map AState [Deriv AState])
144 initTAMap s = constructTypeMap s
145     where
146       uniq = do { i <- get; put (i+1); return i }
147       listType t =
148           do { (st,m) <- constructTypeMap t
149              ; i <- uniq
150              ; let m1 = Map.insert (ASType i) [DCon (Name "Nil")[], 
151                                                DCon (Name "Cons") [ASType i, st]] m
152              ; return (ASType i, m1) }
153       natType = 
154           do { let m1 = Map.insert (ASType 0) [DCon (Name "Z") [], 
155                                                DCon (Name "S") [ASType 0]] (Map.empty)
156              ; return (ASType 0, m1) }
157       anyType =
158           do { let m1 = Map.insert (ASType 1) [DAny] (Map.empty)
159              ; return (ASType 1, m1) }
160       constructTypeMap (TCon (Name "List") [t]) =
161           listType t
162       constructTypeMap (TCon (Name "Nat") []) =
163           natType 
164       constructTypeMap (TVar i) = 
165           anyType
166       constructTypeMap _ =
167           anyType -- Not Supported
168
169 testOverlap :: AST -> Doc 
170 testOverlap (AST decl) = 
171     let fDs = groupBy isSameFunc decl
172     in evalState (do { docs <- mapM f fDs
173                      ; return $ vcat docs }) initCAConf 
174     where
175       am = constructAutomaton (AST decl) initTAMap 
176       f (ds@(Decl g t ps e:es)) = 
177           do { b <- checkInjectivity am (AST decl) g
178              ; let di  = text "Injectivity: " <> text (show $ b)
179              ; ba <- checkAmbiguity am (ASFun g)
180              ; let da  = text "Ambiguity: " <> text (show $ ba)
181              ; dol <- pol ds 
182              ; return $ text (show g) $$ nest 4 (da $$ di $$ dol) }
183       pol ds = let is  = [ ASExp $ fromJust $ idofE e | (Decl f t ps e) <- ds ] 
184                    ijs = [ (i,j) | vs <- [zip is [0..]], (i,x) <- vs, (j,y) <- vs ]
185                in 
186                  do { bs <- mapM (uncurry $ checkOverlapS am (Set.empty)) ijs 
187                     ; let vs = map (map snd) $ groupBy ((==) `on` (fst.fst)) $ zip ijs bs 
188                     ; return $ vcat ( map g vs )}
189           where g bs = hcat ( map (\h -> if h then text "O" else text "-") bs)
190           
191 isNonErasing :: Decl -> Bool
192 isNonErasing (Decl _ _ ps e) =
193     null $ (snub $ concatMap varsP ps) \\ varsE e
194
195
196 checkInjectivity :: Automaton AState -> AST -> Name -> State (CAConf AState) Bool
197 checkInjectivity am (AST decl) f =
198     checkInj (Set.empty) f 
199     where
200       checkInj env f =
201           do { inj  <- getInjSet
202              ; ninj <- getNonInjSet
203              ; if Set.member f inj || Set.member f env then 
204                    return True
205                else if Set.member f ninj then 
206                    return False
207                else
208                    do { b1 <- checkAmbiguity am (ASFun f)
209                       ; when b1 (addNonInj f)
210                       ; let dsF = filter (\(Decl g _ _ _) -> g == f) decl
211                       ; let b2  = all isNonErasing dsF
212                       ; when (not b2) (addNonInj f )
213                       ; let fs = concatMap calledFunctions dsF
214                       ; b3  <- mapM (checkInj (Set.insert f env)) fs
215                       ; when (not $ and b3) (addNonInj f)
216                       ; if (not b1) && b2 && and b3 then
217                             when (Set.null env) (addInj f) >> return True
218                         else
219                             return False } }
220
221 testTupling :: AST -> TAST
222 testTupling ast = 
223     evalState (do { cAst <- optimizedComplementation am ast
224                   ; tAst <- doTupling am ast cAst
225                   ; return tAst }) initCAConf
226     where
227       am = constructAutomaton ast initTAMap 
228
229
230 data TypeDecl = TypeDecl Name [Int] [ConDef]
231 data ConDef   = ConDef Name [Type] -- NB: First Order
232
233 instance Ppr TypeDecl where
234     ppr (TypeDecl c is cdefs) = 
235         text "data" <+> ppr c <+>
236              hsep (map (\i -> text "t" <> ppr i) is) $$ nest 4 (ppr cdefs)
237     pprList decls =
238         vcat $ map ppr decls
239
240 instance Ppr ConDef where
241     ppr (ConDef n ts) = ppr n <+> hsep (map pprT ts)
242         where
243           pprT (TVar i) = ppr (TVar i)
244           pprT t        = parens (ppr t)
245     pprList []        = empty 
246     pprList (c:cs)    = text "=" <+> ppr c $$
247                         f cs
248         where f []     = empty 
249               f [c]    = text "|" <+> ppr c 
250               f (c:cs) = text "|" <+> ppr c $$ f cs  
251
252 -- Extract Type Definition from the complement definition
253 -- FIXME: More Smart Definition
254 constructTypeDecl :: AST -> [ TypeDecl ]
255 constructTypeDecl (AST cdecls) = [ TypeDecl (cmplName) vs condef ]
256     where
257       cmplName = Name "Cmpl"
258       vs = snub $ concat $ evalState (mapM extractVarsT cdecls) (0,[])
259       extractVarsT (Decl _ _ _ e) =
260           case e of 
261             (ECon _ _ c es) -> 
262                 do { trav <- traversedList
263                    ; if c `elem` trav then 
264                          return []
265                      else
266                          do { addTraversed c 
267                             ; let ws = [ w | (EVar _ _ w) <- es ]
268                             ; is <- mapM (\_ -> uniq) ws 
269                             ; return $ is }}
270             _ -> 
271                 return []
272       uniq = do { (i,t) <- get; put (i+1,t); return i }
273       traversedList  = do { (i,t) <- get; return t }
274       addTraversed t = do { (i,tt) <- get; put (i,t:tt) }
275       condef = concat $ evalState (mapM mkConDef cdecls) (0,[])
276       mkConDef (Decl _ _ _ e) =
277           case e of 
278             (ECon _ _ c es) -> 
279                 do { trav <- traversedList
280                    ; if c `elem` trav then 
281                          return []
282                      else 
283                          do { addTraversed c 
284                             ; let ws = [ w | (EVar _ _ w) <- es ]
285                             ; let fs = [ TCon cmplName [ TVar i | i <- vs ] | (EFun _ _ _ _) <- es ]
286                             ; is <- mapM (\_ -> uniq) ws 
287                             ; return $ [ ConDef c (map TVar is ++ fs) ] } }
288             _ ->
289                 return [] 
290                   
291
292
293
294
295 constructBwdFunction :: AST -> (AST, AST, TAST) 
296 constructBwdFunction ast =
297     evalState ( do { cmpl <- optimizedComplementation am ast
298                    ; tpl  <- doTupling am ast cmpl 
299                    ; let itpl = localInversion tpl 
300                    ; let fs = functions ast
301                    ; bwds <- mapM constructBWD fs 
302                    ; return $ (AST bwds, cmpl, itpl)
303                    }) initCAConf
304     where
305       am = constructAutomaton ast initTAMap 
306       functions (AST decls) = map (\(Decl f _ _ _:_) -> f) $ groupBy isSameFunc decls 
307       pS = PVar Nothing TUndet (Name "s")
308       pV = PVar Nothing TUndet (Name "v")
309       eS = EVar Nothing TUndet (Name "s")
310       eV = EVar Nothing TUndet (Name "v")
311       constructBWD f = do { b <- checkInjectivity am ast f 
312                           ; if b then 
313                                 return $ Decl (NBwd f) FTUndet [pS,pV] 
314                                            (EFun Nothing TUndet (NInv f) [eV])
315                             else
316                                 return $ Decl (NBwd f) FTUndet [pS,pV]
317                                            (EFun Nothing TUndet (NInv (NTuple f)) 
318                                                      [eV, EFun Nothing TUndet (NCmpl f) [eS]]) } 
319
320 localInversion :: TAST -> TAST
321 localInversion (TAST tdecls) = TAST $ map localInversionD tdecls
322
323 localInversionD :: TDecl -> TDecl 
324 localInversionD (TDecl f ps es vdecls) =
325     TDecl (NInv f) (map e2p es) (map p2e ps) (map linvVD vdecls)
326     where
327       e2p (EVar i t v)    = PVar i t v 
328       e2p (ECon i t c es) = PCon i t c (map e2p es)
329       p2e (PVar i t v)    = EVar i t v 
330       p2e (PCon i t c ps) = ECon i t c (map p2e ps)
331       linvVD (VDecl vs f us) = VDecl us (NInv f) vs 
332       
333 -- doTupling :: AST -> AST -> TAST 
334 doTupling :: Automaton AState -> AST -> AST -> State (CAConf AState) TAST
335 doTupling am (AST decls) (AST cdecls) =
336     do { tdecls <- mapM tupleD $ zip decls cdecls 
337        ; return $ TAST tdecls }
338     where
339       fCalls (EFun _ _ f es) = [(f,es)] 
340       fCalls (ECon _ _ _ es) = concatMap fCalls es
341       fCalls _               = []
342       convE mp (EFun i t f es) = case lookup (f,es) mp of
343                                    Just v  -> EVar i t v 
344                                    Nothing -> EFun i t f es -- never happens
345       convE mp (EVar i t v )   = EVar i t v 
346       convE mp (ECon i t c es) = ECon i t c (map (convE mp) es)
347       tupleD (Decl f _ ps e, Decl _ _ _ ce) =
348           do { b <- checkInjectivity am (AST decls) f
349              ; if b then 
350                    return $ tupleDInj f ps e 
351                else 
352                    return $ tupleDNInj f ps e ce }
353       tupleDInj f ps e = TDecl f ps [convE vnMap e] wdecls -- keep function-name if injective 
354           where
355             funCalls = fCalls e 
356             vnMap    = zip funCalls [ NTupleV i | i <- [1..] ]
357             wdecls = map (\((f,es),v) -> VDecl [v] f [u | (EVar _ _ u) <- es ]) vnMap 
358       tupleDNInj f ps e ce = TDecl (NTuple f) ps [convE vnMap e, convE cnMap ce] wdecls 
359           where
360             funCalls  = fCalls e
361             ninjCalls = [ (f,es) | (NCmpl f, es) <- fCalls ce ]
362             injCalls  = funCalls \\ ninjCalls 
363             vnMap    = zip funCalls [ NTupleV  i | i <- [1..] ]
364             cnMap    = zip (map (\(f,es) -> (NCmpl f,es)) funCalls) [ NTupleVC i | i <- [1..] ]
365             wdecls   = map convW vnMap 
366                 where 
367                   convW ((f,es),v@(NTupleV i)) 
368                       | (f,es) `elem` injCalls = VDecl [v] f [u | (EVar _ _ u) <- es ]
369                       | otherwise              = VDecl [v,NTupleVC i] (NTuple f) [u | (EVar _ _ u) <- es ]
370                                        
371             
372                                       
373                           
374
375
376
377
378                       
379 calledFunctions (Decl _ _ _ e) = snub $ calledFunctionsE e 
380 calledFunctionsE (ECon _ _ _ es) = concatMap calledFunctionsE es
381 calledFunctionsE (EFun _ _ f es) = f:concatMap calledFunctionsE es 
382 calledFunctionsE _               = []
383                             
384
385 testComplementation (AST decls) = 
386     evalState (optimizedComplementation am (AST decls)) initCAConf
387     where
388       am = constructAutomaton (AST decls) initTAMap 
389       
390
391 optimizedComplementation am (AST decls) 
392     = do { cmpl   <- complementation am (AST decls)
393          ; cmpl'  <- optimizeByRemove am cmpl
394          ; cmpl'' <- optimizeByRename am cmpl' 
395          ; return $ cmpl'' }
396
397 optimizeByRename am (AST cdecls) =
398     do { let cfdeclss = groupBy isSameFunc cdecls
399        ; cfdeclss' <- mapM optRename cfdeclss 
400        ; return $ AST $ concat cfdeclss' }
401     where
402       optRename cfdecls = 
403          do { let ids = [ (i,[ (v,t) | (EVar _ t v) <- es  ],length es)  
404                                | (Decl _ _ _ (ECon _ _ (NCConE i) es)) <- cfdecls ]
405             ; idss <- grouping [] ids 
406             ; return $ map (doRename idss) cfdecls }
407 --      grouping :: [[(Int,[(Name,Type)])]] -> [(Int,[(Name,Type)])] -> State (CAConf AState) [[(Int,[(Name,Type)])]]
408       grouping gs []      = return gs 
409       grouping gs (i:ids) =
410          do { gs' <- checkGroup i gs 
411             ; grouping gs' ids }
412 --      checkGroup :: (Int,[(Name,Type)]) -> [[(Int,[(Name,Type)])]] -> State (CAConf AState) [[(Int,[(Name,Type)])]]
413       checkGroup i [] = return $ [ [i] ]
414       checkGroup i (g:gs) =
415           do { b <- compatible i g  
416              ; if b then 
417                    return $ (i:g):gs
418                else
419                    do { gs' <- checkGroup i gs 
420                       ; return $ g:gs' } }
421       compatible i [] = return $ True
422       compatible (i,vs,l) ((i',vs',l'):ls) =
423           do { b <- checkOverlapS am Set.empty (ASExp i) (ASExp i')
424              ; let b2 = (sort $ map snd vs) == (sort $ map snd vs') 
425              ; if (not b) && b2 && l == l' then 
426                    compatible (i,vs,l) ls 
427                else
428                    return False }
429       doRename idss (Decl f t ps (ECon ei et (NCConE i) es)) = 
430           Decl f t ps (ECon ei et (NCConU f j) es') 
431           where
432             j = fix (\f n iss -> 
433                          case iss of 
434                            is:iss -> 
435                                if i `elem` (map (\(a,_,_) -> a) is) then 
436                                    n 
437                                else 
438                                    f (n+1) iss) 1 idss 
439             es' = sortBy (compare `on` typeofE) [ e | (e@(EVar _ _ _)) <- es ]
440                   ++ [ e | (e@(EFun _ _ _ _)) <- es ]
441       doRename idss d = d 
442             
443           
444           
445                  
446
447 optimizeByRemove am (AST cdecls) =
448     do { let cfdeclss = groupBy isSameFunc cdecls 
449        ; cfdeclss' <- mapM optRem cfdeclss 
450        ; return $ AST $ concat cfdeclss' }
451     where
452       fromInj (Decl _ _ _ (ECon _ _ (NCConF _) _)) = True
453       fromInj _                                    = False
454       optRem cfdecls 
455           | fromInj (head cfdecls) = return cfdecls
456           | otherwise = 
457               mapM (\(Decl f t ps e) -> do { e' <- tryRemove e; return $ Decl f t ps e'}) cfdecls                 
458           where ids = [ i | (Decl _ _ _ (ECon _ _ (NCConE i) _)) <- cfdecls ]
459                 tryRemove (ex@(ECon ei et (NCConE i) [EFun ei' et' f es])) = 
460                     do { b <- checkNonOverlapAll i ids 
461                        ; if b then 
462                              return $ EFun ei' et' f es
463                          else
464                              return $ ex }
465                 tryRemove ex = return ex 
466                 checkNonOverlapAll i [] = return $ True
467                 checkNonOverlapAll i (j:jds) | i == j    = checkNonOverlapAll i jds 
468                                              | otherwise = do { b <- checkOverlapS am (Set.empty) (ASExp i) (ASExp j)
469                                                               ; if b then 
470                                                                     return False
471                                                                 else
472                                                                     checkNonOverlapAll i jds }
473
474 complementation am (ast@(AST decls)) =
475     do { cdecls <- mapM (complementationD am ast) decls
476        ; return $ AST cdecls }
477
478 complementationD am ast (Decl f ftype ps e) =                 
479     do { b <- checkInjectivity am ast f
480        ; if b then 
481              return $ (Decl (NCmpl f) FTUndet ps (ECon Nothing TUndet cNameC []))
482          else 
483              do { let fs = fCalls e 
484                 ; fs' <- filterNonInj fs
485                 ; let e' = cExp unusedVars fs' 
486                 ; return $ (Decl (NCmpl f) FTUndet ps e') }
487        }
488     where
489       unusedVars = snub $ (snub $ concatMap varsWithTP ps) \\ (snub $ varsWithTE e)
490       varsWithTP (PVar _ t v)    = [EVar Nothing t v]
491       varsWithTP (PCon _ _ _ ps) = concatMap varsWithTP ps
492       varsWithTE (EVar _ t v)    = [EVar Nothing t v]
493       varsWithTE (ECon _ _ _ es) = concatMap varsWithTE es 
494       varsWithTE (EFun _ _ _ es) = concatMap varsWithTE es 
495       fCalls (ECon _ _ _ es) = concatMap fCalls es 
496       fCalls (EFun _ _ f es) = (f,es):concatMap fCalls es
497       fCalls _               = []
498       filterNonInj []          = return []
499       filterNonInj ((f,es):fs) = do { b <- checkInjectivity am ast f 
500                                     ; if b then 
501                                           filterNonInj fs 
502                                       else
503                                           do { fs' <- filterNonInj fs
504                                              ; return $ (f,es):fs' } }
505       cNameC = NCConF f 
506       cName  = NCConE (fromJust $ idofE e)
507       cExp vs fs = ECon Nothing TUndet cName $ 
508                        vs ++ (map (\(f,es) -> EFun Nothing TUndet (NCmpl f) es) fs)
509
510
511
512 constructAutomaton :: AST -> (Type -> State Int (AState,Automaton AState)) -> Automaton AState
513 constructAutomaton (AST decl) initTAMap =
514     removeEps $ evalState (unionM $ map constructAMD decl) 2 
515     where
516       unionM []     = return $ Map.empty
517       unionM (m:ms) = do { r1 <- unionM ms 
518                          ; r2 <- m
519                          ; return $ Map.unionWith (++) r1 r2 }
520       constructAMD (Decl f t ps e) = 
521           do { (st,m) <- constructAME e
522              ; return $ Map.insertWith (++) (ASFun f) [DEps st] m }
523       constructAME (ECon i t c es) =
524           do { ims <- mapM constructAME es
525              ; let (is,ms) = unzip ims
526              ; let m       = Map.unions ms
527              ; let s       = ASExp $ fromJust i 
528              ; return (s, Map.insertWith (++) s [DCon c is] m)}
529       constructAME (EFun i t f es) = -- Assume Treeless
530           let s = ASExp $ fromJust i  
531           in return (s, Map.insertWith (++) s [DEps $ ASFun f] (Map.empty))
532       constructAME (EVar i t x) =
533           do { (st,m) <- initTAMap t 
534              ; let s = ASExp $ fromJust i 
535              ; return (s, Map.insertWith (++) s [DEps st] m) }
536      
537 allStates :: Ord s => Automaton s -> [s]
538 allStates am = 
539     snub $ foldr (++) [] $ map (\(i,d) -> i:concatMap allStatesDerive d) $ Map.toList am 
540
541
542 allStatesDerive (DCon _ is) = is
543 allStatesDerive (DAny)      = []
544 allStatesDerive (DEps i)    = [i]
545
546 removeEps :: Automaton AState -> Automaton AState 
547 removeEps am = 
548     foldr (Map.unionWith (++)) Map.empty $
549          map f $ Map.toList am
550     where
551       f (i,ds) = Map.fromList [ (j,filter nonEpsD ds) | j <- reachableA i ]
552       isEps (_,DEps _) = True
553       isEps _          = False
554       nonEpsD (DEps _) = False
555       nonEpsD _        = True
556       erules       = filter isEps $ concatMap (\(i,ds) -> [(i,d)|d<-ds]) $ Map.toList am
557       aStates      = allStates am
558       (graph,v2n,k2v) = graphFromEdges $ map (\(i,is) -> (i,i,is)) $
559                             Map.toList $ Map.fromListWith (++) $
560                               (map (\(i,DEps j) -> (j,[i])) erules
561                                ++ map (\i->(i,[i])) aStates)
562       reachableA k = map (\(n,_,_) -> n) $ map v2n $ reachable graph (fromJust $ k2v k) 
563                            
564               
565 type AmbSet   s = Set s
566 type UnAmbSet s = Set s
567 type OLSet    s = Set (s,s)
568 type UnOLSet  s = Set (s,s)
569 type InjSet     = Set Name
570 type NonInjSet  = Set Name
571 type CAConf   s = (AmbSet s, UnAmbSet s, OLSet s, UnOLSet s, InjSet, NonInjSet)
572
573 initCAConf = (Set.empty,Set.empty,Set.empty,Set.empty,Set.empty,Set.empty)
574
575 ambset    (s,_,_,_,_,_) = s
576 unambset  (_,s,_,_,_,_) = s 
577 olset     (_,_,s,_,_,_) = s 
578 unolset   (_,_,_,s,_,_) = s
579 injset    (_,_,_,_,s,_) = s  
580 noninjset (_,_,_,_,_,s) = s  
581
582 getAmbSet :: Ord s => State (CAConf s) (AmbSet s)
583 getAmbSet   = get >>= (return . ambset)
584
585 getUnAmbSet :: Ord s => State (CAConf s) (UnAmbSet s)
586 getUnAmbSet = get >>= (return . unambset)
587
588 getOLSet :: Ord s => State (CAConf s) (OLSet s)
589 getOLSet    = get >>= (return . olset)
590
591 getUnOLSet :: Ord s => State (CAConf s) (UnOLSet s)
592 getUnOLSet  = get >>= (return . unolset)
593
594 getInjSet :: State (CAConf s) InjSet
595 getInjSet   = get >>= (return . injset)
596
597 getNonInjSet :: State (CAConf s) NonInjSet
598 getNonInjSet = get >>= (return . noninjset)
599
600 addAmb    x = do { (a,ua,o,uo,inj,ninj) <- get; put (Set.insert x a,ua,o,uo,inj,ninj) }
601 addUnAmb  x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,Set.insert x ua,o,uo,inj,ninj) }
602 addOL     x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,Set.insert x o,uo,inj,ninj) }
603 addUnOL   x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,Set.insert x uo,inj,ninj) }
604 addInj    x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,Set.insert x inj,ninj) }
605 addNonInj x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,inj,Set.insert x ninj) }
606
607 checkAmbiguity :: Ord s => Automaton s -> s -> State (CAConf s) Bool
608 checkAmbiguity am s = 
609     do { amb    <- getAmbSet 
610        ; unamb  <- getUnAmbSet
611        ; if (Set.member s amb) then 
612              return True
613          else if (Set.member s unamb) then 
614              return False
615          else
616              do { b <- checkAmb am unamb s 
617                 ; when (not b) (addUnAmb s)
618                 ; return b } }
619     where
620       distinctPairs ds = let vs = zip ds [0..]
621                          in [ (d1,d2) | (d1,i) <- vs, (d2,j) <- vs, i < j ]
622       checkOL (d1,d2) = checkOverlap am (Set.empty) d1 d2 
623       checkAmb am env s =
624           let derives = fromJust $ Map.lookup s am 
625               dPairs  = distinctPairs derives
626           in do { rs <- mapM checkOL dPairs 
627                 ; if or rs then 
628                       addAmb s >> return True
629                   else 
630                       do { let ss = [ s | d <- derives, s <- allStatesDerive d, not (Set.member s env) ]
631                          ; rs <- mapM (checkAmb am (Set.insert s env)) ss
632                          ; return $ or rs }}
633     
634
635 checkOverlap am env (DEps s1)    (DEps s2) = checkOverlapS am env s1 s2
636 checkOverlap am env (DCon c1 s1) (DCon c2 s2)
637     | c1 == c2 =
638         do { rs <- mapM (uncurry (checkOverlapS am env)) $ zip s1 s2
639            ; return $ and rs }
640     | otherwise = return False
641
642 checkOverlap am env DAny _ = return True
643 checkOverlap am env _ DAny = return True
644 checkOverlap am env _ _    = return False
645
646 checkOverlapS :: Ord s => Automaton s -> Set (s,s) -> s -> s -> State (CAConf s) Bool
647 checkOverlapS am env s1 s2 
648     | Set.member (s1,s2) env || Set.member (s2,s1) env 
649       = return False 
650     | otherwise 
651       = do { ol  <- getOLSet 
652            ; uol <- getUnOLSet
653            ; if Set.member (s1,s2) ol || Set.member (s2,s1) ol then 
654                  return True
655              else if Set.member (s1,s2) uol || Set.member (s2,s1) uol then 
656                  return False
657              else
658                  let derives1 = fromJust $ Map.lookup s1 am 
659                      derives2 = fromJust $ Map.lookup s2 am 
660                      comb     = [ (d1,d2) | d1 <- derives1, d2 <- derives2 ]
661                  in do { rs <- mapM (uncurry $ checkOverlap am (Set.insert (s1,s2) env)) comb
662                        ; if all not rs then 
663                              do { when (Set.null env) (addUnOL (s1,s2))
664                                 ; return False }
665                          else
666                              do { addOL (s1,s2)
667                                 ; return True } }}
668                                        
669