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