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