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