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