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