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