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