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