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