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