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