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