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