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