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