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