[Init] Implementation of "Combining Syntactic and Semantic Bidirectionalization"
authorKazutaka Matsuda <kztk@kb.ecei.tohoku.ac.jp>
Wed, 30 Jun 2010 09:09:45 +0000 (09:09 +0000)
committerKazutaka Matsuda <kztk@kb.ecei.tohoku.ac.jp>
Wed, 30 Jun 2010 09:09:45 +0000 (09:09 +0000)
13 files changed:
AST.hs [new file with mode: 0644]
BUtil.hs [new file with mode: 0644]
CodeGen.hs [new file with mode: 0644]
Main.hs [new file with mode: 0644]
Makefile [new file with mode: 0644]
Parser.hs [new file with mode: 0644]
Shapify.hs [new file with mode: 0644]
Type.hs [new file with mode: 0644]
Util.hs [new file with mode: 0644]
example/init.txt [new file with mode: 0644]
example/initHalf.txt [new file with mode: 0644]
example/rev.txt [new file with mode: 0644]
example/seive.txt [new file with mode: 0644]

diff --git a/AST.hs b/AST.hs
new file mode 100644 (file)
index 0000000..0d05ce3
--- /dev/null
+++ b/AST.hs
@@ -0,0 +1,243 @@
+module AST where 
+
+import Util 
+import Text.PrettyPrint
+import Data.List (groupBy)
+
+import Control.Monad.State
+
+data AST = AST [ Decl ]
+
+instance Ppr AST where
+    ppr (AST ds) = 
+        let dss = groupBy (\(Decl f _ _ _) (Decl g _ _ _) -> f == g) ds
+        in vcat $ map pprDecls dss 
+        where 
+          pprDecls (d:ds) =
+              ppr d $$ pprDeclsSimp ds 
+          pprDeclsSimp ds
+              = vcat $ map (\(Decl f _ ps e) -> ppr (Decl f FTUndet ps e)) ds
+
+instance Show AST where 
+    show = show . ppr 
+
+data Name 
+    = Name     String 
+    | IName    String [Int]
+    | NCmpl    Name 
+    | NTuple   Name 
+    | NTupleV  Int      -- Variable Introduced by Tupling 
+    | NTupleVC Int      -- Variable Introduced by Tupling 
+    | NBwd     Name
+    | NInv     Name 
+    | NCConF   Name     -- Constructor Name in Complement (1)
+    | NCConE   Int      -- Constructor Name in Complement (2)
+    | NCConU   Name Int -- After Renaming  
+          deriving (Eq,Ord)
+
+instance Ppr Name where
+    ppr  (Name s) = text s
+    ppr  (IName s is) = text s <> text "_" <> 
+                        (hcat $ punctuate (text "_") $ map ppr is)
+    ppr  (NCmpl n)  = ppr n <> text "_Cmpl" 
+    ppr  (NTuple n) = ppr n <> text "_T"  
+    ppr  (NTupleV i)  = text "tv" <> ppr i
+    ppr  (NTupleVC i) = text "tc" <> ppr i
+    ppr  (NInv n)     = ppr n <> text "_I" 
+    ppr  (NBwd n)     = ppr n <> text "_B"
+    ppr  (NCConF n)   = text "C" <> ppr n
+    ppr  (NCConE i)   = text "C" <> ppr i 
+    ppr  (NCConU n i) = text "C" <> ppr n <> text "_" <> ppr i
+
+instance Show Name where
+    show = show . ppr 
+
+data Decl = Decl Name FType [Pat] Exp
+
+instance Ppr Decl where
+    ppr (Decl fname ftype ps e) = 
+        addSig (ppr fname <> 
+                     parens (hsep $ punctuate comma (map ppr ps)) $$
+                     nest 4 (text "=") $$
+                     nest 6 (ppr e))
+        where 
+          addSig d = 
+              case ftype of
+                FTUndet -> empty <> d
+                _       -> ppr fname <+> text "::" <+> ppr ftype $$ d            
+instance Show Decl where
+    show = show . ppr 
+
+data Exp  = EVar ID Type Name 
+          | EFun ID Type Name [Exp] -- Exp must be variable (treeless)
+          | ECon ID Type Name [Exp]
+       deriving (Ord,Eq)
+
+type ID = Maybe Int
+
+addPprType t d = 
+    case t of 
+      TUndet -> d
+      _      -> d <> text "::" <> ppr t 
+
+instance Ppr Exp where
+    ppr (EVar _ t vname)     
+        = addPprType t (ppr vname)
+    ppr (EFun _ t fname es) 
+        = addPprType t $
+            ppr fname <>
+            parens (sep $ punctuate comma (map ppr es))          
+    ppr (ECon _ t cname []) 
+        = addPprType t $ ppr cname 
+    ppr (ECon _ t cname es)
+        = addPprType t $ 
+             ppr cname <>
+             parens (sep $ punctuate comma (map ppr es))
+
+instance Show Exp where
+    show = show . ppr 
+
+data Pat  = PVar ID Type Name
+          | PCon ID Type Name [Pat] 
+       deriving (Ord,Eq)
+
+instance Ppr Pat where
+    ppr (PVar _ t vname)     
+        = addPprType t (ppr vname)
+    ppr (PCon _ t cname [])
+        = addPprType t (ppr cname)
+    ppr (PCon _ t cname ps)
+        = addPprType t $ ppr cname 
+          <> parens (sep $ punctuate comma (map ppr ps))
+          
+instance Show Pat where
+    show = show . ppr 
+
+data FType 
+    = TFun [Int] [Type] Type -- Quantified Vars, Input Types, Output Type.
+      -- e.g. forall a. [a] -> a 
+      --      ==> TFun [TVar 1] [ TCon "[]" [TVar 1] ] (TVar 1)
+    | FTUndet
+      deriving (Eq,Ord)
+
+instance Ppr FType where
+    ppr (FTUndet) = text "??"
+    ppr (TFun is ts t) =
+        (case is of 
+          [] -> empty 
+          _  -> text "forall" <+>
+                hsep (map pprTV is) <>
+                text ".")
+         <+> argType <+>
+             ppr t 
+        where
+          argType = 
+              case ts of 
+                []  -> empty 
+                [t] -> ppr t <+> text "->" 
+                _   -> 
+                    parens (sep $ punctuate comma (map ppr ts)) 
+                               <+> text "->"
+          pprTV i = text ("t" ++ show i)
+             
+instance Show FType where
+    show = show . ppr 
+
+data Type = TUndet           -- PlaceHolder
+          | TVar Int         -- Type Variable
+          | TCon Name [Type] -- e.g. [Int], Map Int [Char]
+            deriving (Eq,Ord)
+            
+instance Ppr Type where
+    ppr (TUndet)        = text "?"
+    ppr (TVar i)        = text ("t" ++ show i) 
+    ppr (TCon tname ts) =
+        ppr tname <+> 
+             hsep (map (\t -> f t (ppr t)) ts)
+        where
+          f (TUndet) x = x
+          f (TVar i) x = x 
+          f (TCon tname []) x = x
+          f _ x = parens x
+instance Show Type where 
+    show = show . ppr 
+
+
+
+typeofP (PVar _ t _)   = t 
+typeofP (PCon _ t _ _) = t 
+typeofE (EVar _ t _)   = t 
+typeofE (ECon _ t _ _) = t
+typeofE (EFun _ t _ _) = t 
+
+
+idofP (PVar t _ _)   = t 
+idofP (PCon t _ _ _) = t 
+idofE (EVar t _ _)   = t 
+idofE (ECon t _ _ _) = t
+idofE (EFun t _ _ _) = t 
+
+varsP p = snub $ vp p
+    where vp (PVar _ _ x)    = [x]
+          vp (PCon _ _ _ ps) = concatMap vp ps
+varsE e = snub $ ve e 
+    where ve (EVar _ _ x)    = [x]
+          ve (ECon _ _ _ es) = concatMap ve es
+          ve (EFun _ _ _ es) = concatMap ve es
+
+
+-- assignIDsAST :: AST -> AST
+assignIDsAST (AST decls) = 
+    AST $ evalState (mapM assignIDsD decls) 10
+
+assignIDsD :: Decl -> State Int (Decl) 
+assignIDsD (Decl f t ps e) = 
+    do { ps' <- mapM assignIDsP ps 
+       ; e   <- assignIDsE e 
+       ; return $ Decl f t ps e }
+    where
+      uniq = do { i <- get; put (i+1) ; return $ Just (i+1) }
+      assignIDsE (EVar _ t x) = 
+          do { i <- uniq
+             ; return $ EVar i t x }
+      assignIDsE (ECon _ t c es) = 
+          do { i <- uniq 
+             ; es' <- mapM assignIDsE es
+             ; return $ ECon i t c es' }
+      assignIDsE (EFun _ t f es) = 
+          do { i <- uniq 
+             ; es' <- mapM assignIDsE es
+             ; return $ EFun i t f es' }
+
+      assignIDsP (PVar _ t x) =
+          do { i <- uniq
+             ; return $ PVar i t x }
+      assignIDsP (PCon _ t c ps) = 
+          do { i <- uniq
+             ; ps' <- mapM assignIDsP ps 
+             ; return $ PCon i t c ps' }
+
+isSameFunc (Decl f _ _ _) (Decl g _ _ _) = f == g 
+
+
+-- After Tupling
+
+data TAST  = TAST [TDecl]
+data TDecl = TDecl Name [Pat] [Exp] [VDecl] -- f(ps) = es where ... 
+data VDecl = VDecl [Name] Name [Name]          -- vs = f(us)
+
+instance Ppr TAST where 
+    ppr (TAST tdecls) = vcat $ map ppr tdecls 
+instance Ppr TDecl where
+    ppr (TDecl f ps es vdecls) =
+        ppr f <> parens (hsep $ punctuate comma (map ppr ps)) $$
+            nest 4 (text "=" <+> parens (hsep $ punctuate comma (map ppr es))) $$
+            if null vdecls then 
+                empty 
+            else 
+                (nest 6 (text "where") $$
+                 nest 8 (vcat $ map ppr vdecls))
+instance Ppr VDecl where
+    ppr (VDecl vs f us) = parens (hsep $ punctuate comma (map ppr vs))
+                          <+> text "=" <+> ppr f <>
+                          parens (hsep $ punctuate comma (map ppr us))
diff --git a/BUtil.hs b/BUtil.hs
new file mode 100644 (file)
index 0000000..2e0eb47
--- /dev/null
+++ b/BUtil.hs
@@ -0,0 +1,69 @@
+{-# OPTIONS -XRank2Types -XCPP #-}
+module BUtil where
+
+import qualified Data.IntMap as IntMap 
+import Control.Monad 
+
+import System.IO.Unsafe
+
+#if __GLASGOW_HASKELL__ >= 610 
+import Control.OldException
+#else
+import Control.Exception
+#endif
+
+data Nat = S Nat | Z deriving (Show,Eq)
+
+toNat x = if x == 0 then 
+              Z
+          else 
+              S (toNat $ x-1)
+
+fromNat Z     = 0
+fromNat (S x) = 1 + fromNat x
+
+fromDistinctList = IntMap.fromList 
+
+gen_put_bias :: Bias 
+                -> (forall a. [a] -> [a]) 
+                -> (Nat -> Nat -> Maybe Nat) 
+                -> [a] -> [a] 
+                -> Maybe [Maybe a]
+gen_put_bias bias get sput s v =
+    do { let ls = length s  
+       ; let g = fromDistinctList (zip (bias ls) s)
+       ; l' <- maybe (fail "...")
+                     return
+                     (sput (toNat ls) (toNat (length v)))
+       ; let t = bias (fromNat l')
+       ; let h = fromDistinctList (zip (get t) v)
+       ; let h'= IntMap.union h g 
+       ; return (map (flip IntMap.lookup h') t) }
+
+withDefaultBias put bias d s v =
+    do { s' <- put bias s v 
+       ; return (map (maybe d id) s') }
+
+withDefault put d s v =
+    do { s' <- put s v 
+       ; return (map (maybe d id) s') }
+
+gen_put_dbias :: Bias -> (forall a. [a] -> [a]) 
+                 -> (Nat -> Nat -> Maybe Nat)
+                 -> a -> [a] -> [a] -> Maybe [a]
+gen_put_dbias bias get sput d s v =
+    do { s' <- gen_put_bias bias get sput s v
+       ; return (map (maybe d id) s') }
+
+castError :: a -> Maybe a 
+castError f = unsafePerformIO $ 
+    do { r <- try (evaluate f)
+       ; case r of
+           Left  e -> return $ Nothing 
+           Right r -> return $ Just $ r }
+
+type Bias = Int -> [ Int ]
+rear l    = [ 0 .. l - 1 ]
+front l   = reverse [ 0 .. l - 1 ]
+middle l  = [1,3..l] + (reverse [2,4..l])
+borders l = (reverse [1,3..l])+[2,4..l]
diff --git a/CodeGen.hs b/CodeGen.hs
new file mode 100644 (file)
index 0000000..88089c9
--- /dev/null
@@ -0,0 +1,97 @@
+{-# OPTIONS -XMultiParamTypeClasses -XTemplateHaskell #-}
+
+module CodeGen where
+
+import qualified Language.Haskell.TH as TH
+
+import Text.PrettyPrint 
+import Debug.Trace
+import Data.List (groupBy)
+
+import AST
+import Util
+
+generateCodeBwd :: (AST, AST, AST, TAST) -> [ TH.Dec ]
+generateCodeBwd (orig, bwd, cmpl, tinv) = 
+    convCmpl orig ++ convBWD bwd ++ convCmpl cmpl ++ convNDet tinv 
+
+convP (PCon _ _ (Name "Cons") [p1,p2]) = 
+    TH.InfixP (convP p1) (TH.mkName ":") (convP p2)
+convP (PCon _ _ (Name "Nil") []) =
+    TH.ListP []
+convP (PCon _ _ c cs) = 
+    TH.ConP (TH.mkName $ show c) $ map convP cs
+convP (PVar _ _ v)    = TH.VarP (TH.mkName $ show v) 
+
+returnE e     = TH.AppE (TH.VarE $ TH.mkName "return") e
+mplusE  e1 e2 = TH.AppE (TH.AppE (TH.VarE $ TH.mkName "mplus") e1) e2 
+mzeroE        = TH.VarE $ TH.mkName "mzero"
+
+name :: Show a => a -> TH.Name
+name  = TH.mkName . show 
+nameE = TH.VarE . name 
+
+apply f es = foldl TH.AppE f es
+
+convBWD (AST decls) = map convBWDD decls 
+    where
+      convBWDD (Decl f _ ps e) = TH.FunD (TH.mkName $ show f)
+                                 [ TH.Clause (map convP ps) (TH.NormalB $ convE e) [] ]
+      convE (EFun _ _ (NInv f) [EVar _ _ v]) = 
+          TH.AppE (TH.VarE $ TH.mkName "head") $ 
+            TH.AppE (nameE (NInv f)) (nameE v)
+      convE (EFun _ _ (NInv (NTuple f)) 
+                      [EVar _ _ v, EFun _ _ (NCmpl _) [EVar _ _ s]]) = 
+          TH.AppE (TH.VarE $ TH.mkName "head") $ 
+             apply (nameE (NInv (NTuple f))) 
+                       [nameE v, TH.AppE (nameE (NCmpl f)) (nameE s)]
+
+convCmpl (AST decls) = map convCmplF $ groupBy isSameFunc decls
+    where 
+      convCmplF (ds@(Decl f _ _ _:_)) =
+          TH.FunD (name f) $ map convCmplD ds 
+      convCmplD (Decl _ _ ps e) = TH.Clause [TH.TupP $ map convP ps] (TH.NormalB $ convE e) []
+      convE (EVar _ _ v)    = nameE v
+      convE (ECon _ _ (Name "Cons") [e1,e2]) = TH.InfixE (Just $ convE e1) (TH.VarE $ TH.mkName ":") (Just $ convE e2)
+      convE (ECon _ _ (Name "Nil")  [])      = TH.ListE []
+      convE (ECon _ _ c es) = apply (TH.ConE (name c)) $ map convE es 
+      convE (EFun _ _ f es) = apply (TH.VarE (name f)) $ [TH.TupE $ map convE es ]
+
+
+convE (EVar _ _ v)    = nameE v
+convE (ECon _ _ (Name "Cons") [e1,e2]) = TH.InfixE (Just $ convE e1) (TH.VarE $ TH.mkName ":") (Just $ convE e2)
+convE (ECon _ _ (Name "Nil")  [])      = TH.ListE []
+convE (ECon _ _ c es) = apply (TH.ConE (name c)) $ map convE es 
+convE (EFun _ _ f es) = apply (TH.VarE (name f)) $ map convE es 
+
+
+convNDet (TAST tdecls) 
+    = concatMap convNDetF $ groupBy isSameFuncT tdecls 
+    where
+      isSameFuncT (TDecl f _ _ _) (TDecl g _ _ _) = f == g 
+      vars    = [ TH.mkName $ "x"    ++ show i        | i <- [1..] ]
+      funcs f = [ TH.mkName $ show f ++ "_" ++ show i | i <- [1..] ] -- name f = TH.mkName $ show f 
+      convNDetF (ds@(TDecl f ps _ _:_)) = -- NInj
+          [ TH.FunD (name f) 
+            [ TH.Clause (map TH.VarP $ take (length ps) vars)
+                        (TH.NormalB mpluses)
+                        [] ] ]
+          ++ zipWith convNDetD ds (funcs f)
+          where
+            mpluses = foldr mplusE mzeroE $
+                        map (\f -> apply (TH.VarE f) $ map TH.VarE (take (length ps) vars) ) $
+                            take (length ds) (funcs f)
+      convNDetD (TDecl _ ps es vs) f =
+          TH.FunD f [ TH.Clause (map convP ps)         (TH.NormalB $ convEs es vs) [],
+                      TH.Clause [ TH.WildP | _ <- ps]  (TH.NormalB mzeroE) [] ]
+      
+      convEs es vs = TH.DoE $ (map mkBind vs) ++ [ TH.NoBindS (returnE $ TH.TupE $ map convE es) ]
+          where
+            mkBind (VDecl us f vs) = TH.BindS (TH.TupP $ map (TH.VarP . name) us)
+                                           (apply (nameE f) $ map (TH.VarE . name) vs)
+                                           
+      
+
+instance Ppr TH.Dec where
+    ppr = text . show . TH.ppr
+    pprList vs = vcat $ map ppr vs 
\ No newline at end of file
diff --git a/Main.hs b/Main.hs
new file mode 100644 (file)
index 0000000..d956d86
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,776 @@
+{-# OPTIONS -XFlexibleInstances #-}
+
+module Main where
+
+import Text.PrettyPrint
+import Control.Monad.State
+import Control.Monad.Error
+import Data.List
+import Data.Maybe (fromJust, isNothing)
+import Debug.Trace 
+
+import Data.Function (on)
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Data.Graph 
+
+import Util 
+import AST
+
+import Parser
+import Type
+import Shapify
+import CodeGen 
+
+import System.IO
+import System.Environment
+
+data Config 
+    = Config 
+      { 
+        inputFile   :: Maybe String, -- ^ Path to input file
+        execMode    :: ExecMode,
+        outputMode  :: OutputMode
+      }
+
+data ExecMode 
+    = Normal | Shapify | ShapifyPlus | Help | Debug 
+
+data OutputMode = PseudoCode | HaskellCode 
+
+defaultConfig = Config { 
+                  inputFile   = Nothing, 
+                  execMode    = Normal, 
+                  outputMode  = PseudoCode }
+
+parseArgs :: [[Char]] -> Config -> Config 
+parseArgs args conf =
+    case args of 
+      ("-f":x:xs) ->
+          parseArgs xs (conf { inputFile = Just x })
+      ("-s":xs) ->
+          parseArgs xs (conf { execMode = Shapify })
+      ("-ss":xs) ->
+          parseArgs xs (conf { execMode = ShapifyPlus })
+      ("-h":xs) ->
+          parseArgs xs (conf { execMode = Help })
+      ("-H":xs) ->
+          parseArgs xs (conf { outputMode = HaskellCode, execMode = ShapifyPlus } )
+      ("-P":xs) ->
+          parseArgs xs (conf { outputMode = PseudoCode } )
+      ("-d":xs) ->
+          parseArgs xs (conf { execMode = Debug })
+      (x:xs) | isNothing (inputFile conf) ->
+          parseArgs xs (conf { inputFile = Just x })
+      (x:xs) ->
+          parseArgs xs conf
+      [] ->
+          conf
+
+progName = "Main"
+
+usage = show $ 
+    text "USAGE" $$
+    text "-----" $$
+         nest 4 (text $ progName ++ "[-ss] (-P|-H) [-f] [FILENAME]\n") $+$ 
+                  
+         text ("This program is a prototype implementation of the paper:\n") $$
+         nest 4 (sep [text "Janis Voigtlander, Zhenjiang Hu, Kazutaka Matsuda and Meng Wang:",
+                       text "Combining Syntactic and Semantic Bidirectionalization.",
+                       text "ICFP 2010.\n"])
+         $$
+         wrap 80 ( "Given a \"get\" function defined in a file specified by FILENAME,"
+                  ++ "the program returns \"put\" function by combining "
+                  ++ "semantic bidirectionalization (Janis Voiglander: POPL'09) "
+                  ++ "and syntatic bidirectionalization (Kazutaka Matsuda et al.: ICFP'07). A typical usage is \""++ progName ++ " -ss -H FILENAME\", which corresponding to the paper.\n"
+                  ) $+$
+    text "OPTIONS" $$
+    text "-------" $$
+         pprOptions ([ 
+               (text "-ss", text"Converts \"List Unit\"s to \"Nat\"s"), 
+               (text"-H", text"Returns a Haskell source code of \"put\" function." $$ text "This options implies \"-ss\"."),
+               (text"-P", text"Returns a pseudo code only after syntatic bidirectionalization [DEFAULT]"),                                                       
+               (text"-h", text"Show this help message") ])                      
+--          vcat [nest 4 (text "-t"),
+--                nest 8 (text "Type inference only"),
+--                nest 4 (text "-s"),
+--                nest 8 (vcat [text"Replace all expressions/patterns \"e :: t\"",
+--                              text"in function with type \"forall ...t... . ...\"."]) ,
+--                nest 4 (text "-ss"),
+--                nest 8 (vcat [text "Replace all expressions/patterns \"[] :: List Unit\" with \"Z :: Nat\"",
+--                              text "and \"Cons(_,x) :: List Unit\" with \"S(x)::Nat\"."]),
+--                nest 4 (text "-h"),
+--                nest 8 (text "Show this help messange.")]
+    where
+      pprOptions ps = vcat $ concatMap 
+                      (\(a,b) -> [nest 4 a,nest 8 b]) ps 
+      wrap n s = wrap' n s [] 
+          where wrap' 0 (' ':s) buf = wrap' 0 s buf 
+                wrap' 0 s buf  = (text (reverse buf)) $$ wrap' n s []
+                wrap' m [] buf = (text (reverse buf))
+                wrap' m (' ':s) buf  
+                    | m - lnextSpace s < 0 =
+                        text (reverse buf) $$ wrap' n s []
+                    | otherwise = 
+                        wrap' (m-1) s (' ':buf)
+                wrap' m (c:s) buf | m > 0 =
+                    wrap' (m-1) s (c:buf)
+                lnextSpace [] = 0
+                lnextSpace (' ':_) = 0
+                lnextSpace (c:s)   = 1 + lnextSpace s 
+
+main :: IO ()
+main = do { args <- getArgs 
+          ; let conf = parseArgs args defaultConfig
+          ; case execMode conf of 
+              Help -> putStrLn usage 
+              _ -> 
+                  do { csterr <- case inputFile conf of
+                                   Nothing -> 
+                                       do cont <- getContents
+                                          return $ parseString cont
+                                   Just filename ->
+                                       parseFile filename
+                     ; case csterr of
+                         Left err -> hPutStrLn stderr (show err)
+                         Right cprog -> 
+                             case execMode conf of 
+                               Normal -> 
+                                   outputCode (outputMode conf) False (cprog) (typeInference cprog)
+                               Shapify ->
+                               -- outputCode (outputMode conf) False (cprog) (shapify $ typeInference cprog)
+                                   putStrLn "Not Supported Now."
+                               ShapifyPlus ->
+                                   outputCode (outputMode conf) True  (cprog) (introNat $ shapify $ typeInference cprog)
+                               Debug ->
+                                   do { print $ ppr   $ cprog
+                                      -- ; print $ pprAM $ constructAutomaton (typeInference cprog) initTAMap
+                                      ; let (p1,p2,p3) = constructBwdFunction (typeInference cprog)
+                                      ; print $ ppr p1 $$ ppr p2 $$ ppr p3
+                                      ; print $ ppr $ constructTypeDecl p2 
+                                      ; print $ ppr $ generateCodeBwd (typeInference cprog, p1,p2,p3)
+                                      ; putStrLn ""
+                                      ; putStrLn $ "---- After \"Shapify\" ----" 
+                                      ; let cprog' = introNat $ shapify $ typeInference cprog 
+                                      -- ; print $ pprAM $ constructAutomaton cprog' initTAMap
+                                      ; print $ cprog'                                       
+                                      ; let (p1,p2,p3) = constructBwdFunction cprog' 
+                                      ; print $ ppr p1 $$ ppr p2 $$ ppr p3
+                                      ; putStrLn ""
+                                      }
+                     }
+          }
+
+outputCode o isShapify orig ast =
+    let (p1,p2,p3) = constructBwdFunction ast
+    in case o of 
+         PseudoCode  ->
+             do print $ ppr (constructTypeDecl p2)
+                print $ ppr orig $$  ppr p1 $$ ppr p2 $$ ppr p3 
+         HaskellCode ->
+             do putStrLn $ "import Control.Monad"
+                putStrLn $ "import BUtil"
+                when isShapify $
+                     print $ vcat $ map genBwdDef 
+                               (let AST decls = typeInference orig
+                                in map (\(Decl f t _ _:_) -> (f,t)) $ 
+                                     groupBy isSameFunc decls)
+                print $ ppr (constructTypeDecl p2)
+                print $ ppr $ generateCodeBwd (orig,p1,p2,p3)
+    where
+      genBwdDef (Name fName,(TFun is ts t)) =
+          case (ts,t) of 
+            ([TCon (Name "List") [TVar i]],TCon (Name "List") [TVar j]) | i == j  ->
+                ppr (Name fName) <> text "_Bb bias s v" $$
+                  nest 4 (text "= gen_put_bias bias Main." <> ppr (Name fName) 
+                               <> text "(\\x y -> castError $ (" 
+                               <> ppr (NBwd $ IName fName is)
+                               <> text " $! x) $! y) s v" ) $$
+                ppr (Name fName) <> text "_Bbd = withDefaultBias "
+                    <> ppr (Name fName) <> text "_Bb" $$
+                ppr (Name fName) <> text "_Bd = withDefault "
+                    <> ppr (Name fName) <> text "_B" $$
+                ppr (Name fName) <> text "_B s v = " 
+                  <> ppr (Name fName) <> text "_Bb rear s v" 
+            _ ->
+                empty
+                                  
+
+
+checkTreeless :: AST -> Bool
+checkTreeless (AST decls) = all checkTreelessD decls
+    where
+      checkTreelessD (Decl _ _ _ e) = checkTreelessE e
+      checkTreelessE (EVar _ _ _)    = True
+      checkTreelessE (ECon _ _ _ es) = all checkTreelessE es
+      checkTreelessE (EFun _ _ _ es) = all isVariable es
+      isVariable (EVar _ _ _) = True
+      isVariable _            = False
+
+checkAffine :: AST -> Bool 
+checkAffine (AST decls) = all checkAffineD decls
+    where
+      checkAffineD (Decl _ _ _ e) = checkAffineE e 
+      checkAffineE e = (varsE e == snub (varsE e))
+      varsE (EVar _ _ v) = [v]
+      varsE (ECon _ _ _ es) = concatMap varsE es
+      varsE (EFun _ _ _ es) = concatMap varsE es
+
+
+           
+type Automaton s = Map s [Deriv s]
+data Deriv s    = DCon Name [s]
+                | DEps s 
+                | DAny
+
+pprAM am = 
+    vcat $ map pprDs $ Map.toList am
+    where
+      pprDs (i,ds) = 
+          ppr i $$
+          nest 4 (vcat $ map (\d -> text " -> " <> pprD d) ds)
+      pprD (DAny)      = text "_" 
+      pprD (DEps s)    = ppr s
+      pprD (DCon c ss) = ppr c <> parens (hcat $ punctuate comma (map ppr ss))
+
+data AState = ASType Int
+            | ASExp  Int
+            | ASFun  Name
+     deriving (Eq,Ord)
+
+instance Ppr AState where
+    ppr (ASType i) = text $ "T" ++ show i 
+    ppr (ASExp  x) = text $ "E" ++ show x
+    ppr (ASFun  n) = text $ "F" ++ show n
+
+instance Show AState where
+    show = show . ppr 
+
+initTAMap s = constructTypeMap s
+    where
+      uniq = do { i <- get; put (i+1); return i }
+      listType t =
+          do { (st,m) <- constructTypeMap t
+             ; i <- uniq
+             ; let m1 = Map.insert (ASType i) [DCon (Name "Nil")[], 
+                                               DCon (Name "Cons") [ASType i, st]] m
+             ; return (ASType i, m1) }
+      natType = 
+          do { let m1 = Map.insert (ASType 0) [DCon (Name "Z") [], 
+                                               DCon (Name "S") [ASType 0]] (Map.empty)
+             ; return (ASType 0, m1) }
+      anyType =
+          do { let m1 = Map.insert (ASType 1) [DAny] (Map.empty)
+             ; return (ASType 1, m1) }
+      constructTypeMap (TCon (Name "List") [t]) =
+          listType t
+      constructTypeMap (TCon (Name "Nat") []) =
+          natType 
+      constructTypeMap (TVar i) = 
+          anyType
+      constructTypeMap _ =
+          anyType -- Not Supported
+
+testOverlap :: AST -> Doc 
+testOverlap (AST decl) = 
+    let fDs = groupBy isSameFunc decl
+    in evalState (do { docs <- mapM f fDs
+                     ; return $ vcat docs }) initCAConf 
+    where
+      am = constructAutomaton (AST decl) initTAMap 
+      f (ds@(Decl g t ps e:es)) = 
+          do { b <- checkInjectivity am (AST decl) g
+             ; let di  = text "Injectivity: " <> text (show $ b)
+             ; ba <- checkAmbiguity am (ASFun g)
+             ; let da  = text "Ambiguity: " <> text (show $ ba)
+             ; dol <- pol ds 
+             ; return $ text (show g) $$ nest 4 (da $$ di $$ dol) }
+      pol ds = let is  = [ ASExp $ fromJust $ idofE e | (Decl f t ps e) <- ds ] 
+                   ijs = [ (i,j) | vs <- [zip is [0..]], (i,x) <- vs, (j,y) <- vs ]
+               in 
+                 do { bs <- mapM (uncurry $ checkOverlapS am (Set.empty)) ijs 
+                    ; let vs = map (map snd) $ groupBy ((==) `on` (fst.fst)) $ zip ijs bs 
+                    ; return $ vcat ( map g vs )}
+          where g bs = hcat ( map (\h -> if h then text "O" else text "-") bs)
+          
+isNonErasing (Decl _ _ ps e) =
+    null $ (snub $ concatMap varsP ps) \\ varsE e
+
+
+
+checkInjectivity am (AST decl) f =
+    checkInj (Set.empty) f 
+    where
+      checkInj env f =
+          do { inj  <- getInjSet
+             ; ninj <- getNonInjSet
+             ; if Set.member f inj || Set.member f env then 
+                   return True
+               else if Set.member f ninj then 
+                   return False
+               else
+                   do { b1 <- checkAmbiguity am (ASFun f)
+                      ; when b1 (addNonInj f)
+                      ; let dsF = filter (\(Decl g _ _ _) -> g == f) decl
+                      ; let b2  = all isNonErasing dsF
+                      ; when (not b2) (addNonInj f )
+                      ; let fs = concatMap calledFunctions dsF
+                      ; b3  <- mapM (checkInj (Set.insert f env)) fs
+                      ; when (not $ and b3) (addNonInj f)
+                      ; if (not b1) && b2 && and b3 then
+                            when (Set.null env) (addInj f) >> return True
+                        else
+                            return False } }
+
+testTupling ast = 
+    evalState (do { cAst <- optimizedComplementation am ast
+                  ; tAst <- doTupling am ast cAst
+                  ; return tAst }) initCAConf
+    where
+      am = constructAutomaton ast initTAMap 
+
+
+data TypeDecl = TypeDecl Name [Int] [ConDef]
+data ConDef   = ConDef Name [Type] -- NB: First Order
+
+instance Ppr TypeDecl where
+    ppr (TypeDecl c is cdefs) = 
+        text "data" <+> ppr c <+>
+             hsep (map (\i -> text "t" <> ppr i) is) $$ nest 4 (ppr cdefs)
+    pprList decls =
+        vcat $ map ppr decls
+
+instance Ppr ConDef where
+    ppr (ConDef n ts) = ppr n <+> hsep (map pprT ts)
+        where
+          pprT (TVar i) = ppr (TVar i)
+          pprT t        = parens (ppr t)
+    pprList []        = empty 
+    pprList (c:cs)    = text "=" <+> ppr c $$
+                        f cs
+        where f []     = empty 
+              f [c]    = text "|" <+> ppr c 
+              f (c:cs) = text "|" <+> ppr c $$ f cs  
+
+-- Extract Type Definition from the complement definition
+-- FIXME: More Smart Definition
+constructTypeDecl :: AST -> [ TypeDecl ]
+constructTypeDecl (AST cdecls) = [ TypeDecl (cmplName) vs condef ]
+    where
+      cmplName = Name "Cmpl"
+      vs = snub $ concat $ evalState (mapM extractVarsT cdecls) (0,[])
+      extractVarsT (Decl _ _ _ e) =
+          case e of 
+            (ECon _ _ c es) -> 
+                do { trav <- traversedList
+                   ; if c `elem` trav then 
+                         return []
+                     else
+                         do { addTraversed c 
+                            ; let ws = [ w | (EVar _ _ w) <- es ]
+                            ; is <- mapM (\_ -> uniq) ws 
+                            ; return $ is }}
+            _ -> 
+                return []
+      uniq = do { (i,t) <- get; put (i+1,t); return i }
+      traversedList  = do { (i,t) <- get; return t }
+      addTraversed t = do { (i,tt) <- get; put (i,t:tt) }
+      condef = concat $ evalState (mapM mkConDef cdecls) (0,[])
+      mkConDef (Decl _ _ _ e) =
+          case e of 
+            (ECon _ _ c es) -> 
+                do { trav <- traversedList
+                   ; if c `elem` trav then 
+                         return []
+                     else 
+                         do { addTraversed c 
+                            ; let ws = [ w | (EVar _ _ w) <- es ]
+                            ; let fs = [ TCon cmplName [ TVar i | i <- vs ] | (EFun _ _ _ _) <- es ]
+                            ; is <- mapM (\_ -> uniq) ws 
+                            ; return $ [ ConDef c (map TVar is ++ fs) ] } }
+            _ ->
+                return [] 
+                  
+
+
+
+
+constructBwdFunction :: AST -> (AST, AST, TAST) 
+constructBwdFunction ast =
+    evalState ( do { cmpl <- optimizedComplementation am ast
+                   ; tpl  <- doTupling am ast cmpl 
+                   ; let itpl = localInversion tpl 
+                   ; let fs = functions ast
+                   ; bwds <- mapM constructBWD fs 
+                   ; return $ (AST bwds, cmpl, itpl)
+                   }) initCAConf
+    where
+      am = constructAutomaton ast initTAMap 
+      functions (AST decls) = map (\(Decl f _ _ _:_) -> f) $ groupBy isSameFunc decls 
+      pS = PVar Nothing TUndet (Name "s")
+      pV = PVar Nothing TUndet (Name "v")
+      eS = EVar Nothing TUndet (Name "s")
+      eV = EVar Nothing TUndet (Name "v")
+      constructBWD f = do { b <- checkInjectivity am ast f 
+                          ; if b then 
+                                return $ Decl (NBwd f) FTUndet [pS,pV] 
+                                           (EFun Nothing TUndet (NInv f) [eV])
+                            else
+                                return $ Decl (NBwd f) FTUndet [pS,pV]
+                                           (EFun Nothing TUndet (NInv (NTuple f)) 
+                                                     [eV, EFun Nothing TUndet (NCmpl f) [eS]]) } 
+
+localInversion :: TAST -> TAST
+localInversion (TAST tdecls) = TAST $ map localInversionD tdecls
+
+localInversionD :: TDecl -> TDecl 
+localInversionD (TDecl f ps es vdecls) =
+    TDecl (NInv f) (map e2p es) (map p2e ps) (map linvVD vdecls)
+    where
+      e2p (EVar i t v)    = PVar i t v 
+      e2p (ECon i t c es) = PCon i t c (map e2p es)
+      p2e (PVar i t v)    = EVar i t v 
+      p2e (PCon i t c ps) = ECon i t c (map p2e ps)
+      linvVD (VDecl vs f us) = VDecl us (NInv f) vs 
+      
+-- doTupling :: AST -> AST -> TAST 
+doTupling am (AST decls) (AST cdecls) =
+    do { tdecls <- mapM tupleD $ zip decls cdecls 
+       ; return $ TAST tdecls }
+    where
+      fCalls (EFun _ _ f es) = [(f,es)] 
+      fCalls (ECon _ _ _ es) = concatMap fCalls es
+      fCalls _               = []
+      convE mp (EFun i t f es) = case lookup (f,es) mp of
+                                   Just v  -> EVar i t v 
+                                   Nothing -> EFun i t f es -- never happens
+      convE mp (EVar i t v )   = EVar i t v 
+      convE mp (ECon i t c es) = ECon i t c (map (convE mp) es)
+      tupleD (Decl f _ ps e, Decl _ _ _ ce) =
+          do { b <- checkInjectivity am (AST decls) f
+             ; if b then 
+                   return $ tupleDInj f ps e 
+               else 
+                   return $ tupleDNInj f ps e ce }
+      tupleDInj f ps e = TDecl f ps [convE vnMap e] wdecls -- keep function-name if injective 
+          where
+            funCalls = fCalls e 
+            vnMap    = zip funCalls [ NTupleV i | i <- [1..] ]
+            wdecls = map (\((f,es),v) -> VDecl [v] f [u | (EVar _ _ u) <- es ]) vnMap 
+      tupleDNInj f ps e ce = TDecl (NTuple f) ps [convE vnMap e, convE cnMap ce] wdecls 
+          where
+            funCalls  = fCalls e
+            ninjCalls = [ (f,es) | (NCmpl f, es) <- fCalls ce ]
+            injCalls  = funCalls \\ ninjCalls 
+            vnMap    = zip funCalls [ NTupleV  i | i <- [1..] ]
+            cnMap    = zip (map (\(f,es) -> (NCmpl f,es)) funCalls) [ NTupleVC i | i <- [1..] ]
+            wdecls   = map convW vnMap 
+                where 
+                  convW ((f,es),v@(NTupleV i)) 
+                      | (f,es) `elem` injCalls = VDecl [v] f [u | (EVar _ _ u) <- es ]
+                      | otherwise              = VDecl [v,NTupleVC i] (NTuple f) [u | (EVar _ _ u) <- es ]
+                                       
+            
+                                      
+                          
+
+
+
+
+                      
+calledFunctions (Decl _ _ _ e) = snub $ calledFunctionsE e 
+calledFunctionsE (ECon _ _ _ es) = concatMap calledFunctionsE es
+calledFunctionsE (EFun _ _ f es) = f:concatMap calledFunctionsE es 
+calledFunctionsE _               = []
+                            
+
+testComplementation (AST decls) = 
+    evalState (optimizedComplementation am (AST decls)) initCAConf
+    where
+      am = constructAutomaton (AST decls) initTAMap 
+      
+
+optimizedComplementation am (AST decls) 
+    = do { cmpl   <- complementation am (AST decls)
+         ; cmpl'  <- optimizeByRemove am cmpl
+         ; cmpl'' <- optimizeByRename am cmpl' 
+         ; return $ cmpl'' }
+
+optimizeByRename am (AST cdecls) =
+    do { let cfdeclss = groupBy isSameFunc cdecls
+       ; cfdeclss' <- mapM optRename cfdeclss 
+       ; return $ AST $ concat cfdeclss' }
+    where
+      optRename cfdecls = 
+         do { let ids = [ (i,[ (v,t) | (EVar _ t v) <- es  ],length es)  
+                               | (Decl _ _ _ (ECon _ _ (NCConE i) es)) <- cfdecls ]
+            ; idss <- grouping [] ids 
+            ; return $ map (doRename idss) cfdecls }
+--      grouping :: [[(Int,[(Name,Type)])]] -> [(Int,[(Name,Type)])] -> State (CAConf AState) [[(Int,[(Name,Type)])]]
+      grouping gs []      = return gs 
+      grouping gs (i:ids) =
+         do { gs' <- checkGroup i gs 
+            ; grouping gs' ids }
+--      checkGroup :: (Int,[(Name,Type)]) -> [[(Int,[(Name,Type)])]] -> State (CAConf AState) [[(Int,[(Name,Type)])]]
+      checkGroup i [] = return $ [ [i] ]
+      checkGroup i (g:gs) =
+          do { b <- compatible i g  
+             ; if b then 
+                   return $ (i:g):gs
+               else
+                   do { gs' <- checkGroup i gs 
+                      ; return $ g:gs' } }
+      compatible i [] = return $ True
+      compatible (i,vs,l) ((i',vs',l'):ls) =
+          do { b <- checkOverlapS am Set.empty (ASExp i) (ASExp i')
+             ; let b2 = (sort $ map snd vs) == (sort $ map snd vs') 
+             ; if (not b) && b2 && l == l' then 
+                   compatible (i,vs,l) ls 
+               else
+                   return False }
+      doRename idss (Decl f t ps (ECon ei et (NCConE i) es)) = 
+          Decl f t ps (ECon ei et (NCConU f j) es') 
+          where
+            j = fix (\f n iss -> 
+                         case iss of 
+                           is:iss -> 
+                               if i `elem` (map (\(a,_,_) -> a) is) then 
+                                   n 
+                               else 
+                                   f (n+1) iss) 1 idss 
+            es' = sortBy (compare `on` typeofE) [ e | (e@(EVar _ _ _)) <- es ]
+                  ++ [ e | (e@(EFun _ _ _ _)) <- es ]
+      doRename idss d = d 
+            
+          
+          
+                 
+
+optimizeByRemove am (AST cdecls) =
+    do { let cfdeclss = groupBy isSameFunc cdecls 
+       ; cfdeclss' <- mapM optRem cfdeclss 
+       ; return $ AST $ concat cfdeclss' }
+    where
+      fromInj (Decl _ _ _ (ECon _ _ (NCConF _) _)) = True
+      fromInj _                                    = False
+      optRem cfdecls 
+          | fromInj (head cfdecls) = return cfdecls
+          | otherwise = 
+              mapM (\(Decl f t ps e) -> do { e' <- tryRemove e; return $ Decl f t ps e'}) cfdecls                 
+          where ids = [ i | (Decl _ _ _ (ECon _ _ (NCConE i) _)) <- cfdecls ]
+                tryRemove (ex@(ECon ei et (NCConE i) [EFun ei' et' f es])) = 
+                    do { b <- checkNonOverlapAll i ids 
+                       ; if b then 
+                             return $ EFun ei' et' f es
+                         else
+                             return $ ex }
+                tryRemove ex = return ex 
+                checkNonOverlapAll i [] = return $ True
+                checkNonOverlapAll i (j:jds) | i == j    = checkNonOverlapAll i jds 
+                                             | otherwise = do { b <- checkOverlapS am (Set.empty) (ASExp i) (ASExp j)
+                                                              ; if b then 
+                                                                    return False
+                                                                else
+                                                                    checkNonOverlapAll i jds }
+
+complementation am (ast@(AST decls)) =
+    do { cdecls <- mapM (complementationD am ast) decls
+       ; return $ AST cdecls }
+
+complementationD am ast (Decl f ftype ps e) =                 
+    do { b <- checkInjectivity am ast f
+       ; if b then 
+             return $ (Decl (NCmpl f) FTUndet ps (ECon Nothing TUndet cNameC []))
+         else 
+             do { let fs = fCalls e 
+                ; fs' <- filterNonInj fs
+                ; let e' = cExp unusedVars fs' 
+                ; return $ (Decl (NCmpl f) FTUndet ps e') }
+       }
+    where
+      unusedVars = snub $ (snub $ concatMap varsWithTP ps) \\ (snub $ varsWithTE e)
+      varsWithTP (PVar _ t v)    = [EVar Nothing t v]
+      varsWithTP (PCon _ _ _ ps) = concatMap varsWithTP ps
+      varsWithTE (EVar _ t v)    = [EVar Nothing t v]
+      varsWithTE (ECon _ _ _ es) = concatMap varsWithTE es 
+      varsWithTE (EFun _ _ _ es) = concatMap varsWithTE es 
+      fCalls (ECon _ _ _ es) = concatMap fCalls es 
+      fCalls (EFun _ _ f es) = (f,es):concatMap fCalls es
+      fCalls _               = []
+      filterNonInj []          = return []
+      filterNonInj ((f,es):fs) = do { b <- checkInjectivity am ast f 
+                                    ; if b then 
+                                          filterNonInj fs 
+                                      else
+                                          do { fs' <- filterNonInj fs
+                                             ; return $ (f,es):fs' } }
+      cNameC = NCConF f 
+      cName  = NCConE (fromJust $ idofE e)
+      cExp vs fs = ECon Nothing TUndet cName $ 
+                       vs ++ (map (\(f,es) -> EFun Nothing TUndet (NCmpl f) es) fs)
+
+
+
+constructAutomaton :: AST -> (Type -> State Int (AState,Automaton AState)) -> Automaton AState
+constructAutomaton (AST decl) initTAMap =
+    removeEps $ evalState (unionM $ map constructAMD decl) 2 
+    where
+      unionM []     = return $ Map.empty
+      unionM (m:ms) = do { r1 <- unionM ms 
+                         ; r2 <- m
+                         ; return $ Map.unionWith (++) r1 r2 }
+      constructAMD (Decl f t ps e) = 
+          do { (st,m) <- constructAME e
+             ; return $ Map.insertWith (++) (ASFun f) [DEps st] m }
+      constructAME (ECon i t c es) =
+          do { ims <- mapM constructAME es
+             ; let (is,ms) = unzip ims
+             ; let m       = Map.unions ms
+             ; let s       = ASExp $ fromJust i 
+             ; return (s, Map.insertWith (++) s [DCon c is] m)}
+      constructAME (EFun i t f es) = -- Assume Treeless
+          let s = ASExp $ fromJust i  
+          in return (s, Map.insertWith (++) s [DEps $ ASFun f] (Map.empty))
+      constructAME (EVar i t x) =
+          do { (st,m) <- initTAMap t 
+             ; let s = ASExp $ fromJust i 
+             ; return (s, Map.insertWith (++) s [DEps st] m) }
+     
+allStates :: Ord s => Automaton s -> [s]
+allStates am = 
+    snub $ foldr (++) [] $ map (\(i,d) -> i:concatMap allStatesDerive d) $ Map.toList am 
+
+
+allStatesDerive (DCon _ is) = is
+allStatesDerive (DAny)      = []
+allStatesDerive (DEps i)    = [i]
+
+removeEps :: Automaton AState -> Automaton AState 
+removeEps am = 
+    foldr (Map.unionWith (++)) Map.empty $
+         map f $ Map.toList am
+    where
+      f (i,ds) = Map.fromList [ (j,filter nonEpsD ds) | j <- reachableA i ]
+      isEps (_,DEps _) = True
+      isEps _          = False
+      nonEpsD (DEps _) = False
+      nonEpsD _        = True
+      erules       = filter isEps $ concatMap (\(i,ds) -> [(i,d)|d<-ds]) $ Map.toList am
+      aStates      = allStates am
+      (graph,v2n,k2v) = graphFromEdges $ map (\(i,is) -> (i,i,is)) $
+                            Map.toList $ Map.fromListWith (++) $
+                              (map (\(i,DEps j) -> (j,[i])) erules
+                               ++ map (\i->(i,[i])) aStates)
+      reachableA k = map (\(n,_,_) -> n) $ map v2n $ reachable graph (fromJust $ k2v k) 
+                           
+              
+type AmbSet   s = Set s
+type UnAmbSet s = Set s
+type OLSet    s = Set (s,s)
+type UnOLSet  s = Set (s,s)
+type InjSet     = Set Name
+type NonInjSet  = Set Name
+type CAConf   s = (AmbSet s, UnAmbSet s, OLSet s, UnOLSet s, InjSet, NonInjSet)
+
+initCAConf = (Set.empty,Set.empty,Set.empty,Set.empty,Set.empty,Set.empty)
+
+ambset    (s,_,_,_,_,_) = s
+unambset  (_,s,_,_,_,_) = s 
+olset     (_,_,s,_,_,_) = s 
+unolset   (_,_,_,s,_,_) = s
+injset    (_,_,_,_,s,_) = s  
+noninjset (_,_,_,_,_,s) = s  
+
+getAmbSet :: Ord s => State (CAConf s) (AmbSet s)
+getAmbSet   = get >>= (return . ambset)
+
+getUnAmbSet :: Ord s => State (CAConf s) (UnAmbSet s)
+getUnAmbSet = get >>= (return . unambset)
+
+getOLSet :: Ord s => State (CAConf s) (OLSet s)
+getOLSet    = get >>= (return . olset)
+
+getUnOLSet :: Ord s => State (CAConf s) (UnOLSet s)
+getUnOLSet  = get >>= (return . unolset)
+
+getInjSet :: State (CAConf s) InjSet
+getInjSet   = get >>= (return . injset)
+
+getNonInjSet :: State (CAConf s) NonInjSet
+getNonInjSet = get >>= (return . noninjset)
+
+addAmb    x = do { (a,ua,o,uo,inj,ninj) <- get; put (Set.insert x a,ua,o,uo,inj,ninj) }
+addUnAmb  x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,Set.insert x ua,o,uo,inj,ninj) }
+addOL     x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,Set.insert x o,uo,inj,ninj) }
+addUnOL   x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,Set.insert x uo,inj,ninj) }
+addInj    x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,Set.insert x inj,ninj) }
+addNonInj x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,inj,Set.insert x ninj) }
+
+checkAmbiguity :: Ord s => Automaton s -> s -> State (CAConf s) Bool
+checkAmbiguity am s = 
+    do { amb    <- getAmbSet 
+       ; unamb  <- getUnAmbSet
+       ; if (Set.member s amb) then 
+             return True
+         else if (Set.member s unamb) then 
+             return False
+         else
+             do { b <- checkAmb am unamb s 
+                ; when (not b) (addUnAmb s)
+                ; return b } }
+    where
+      distinctPairs ds = let vs = zip ds [0..]
+                         in [ (d1,d2) | (d1,i) <- vs, (d2,j) <- vs, i < j ]
+      checkOL (d1,d2) = checkOverlap am (Set.empty) d1 d2 
+      checkAmb am env s =
+          let derives = fromJust $ Map.lookup s am 
+              dPairs  = distinctPairs derives
+          in do { rs <- mapM checkOL dPairs 
+                ; if or rs then 
+                      addAmb s >> return True
+                  else 
+                      do { let ss = [ s | d <- derives, s <- allStatesDerive d, not (Set.member s env) ]
+                         ; rs <- mapM (checkAmb am (Set.insert s env)) ss
+                         ; return $ or rs }}
+    
+
+checkOverlap am env (DEps s1)    (DEps s2) = checkOverlapS am env s1 s2
+checkOverlap am env (DCon c1 s1) (DCon c2 s2)
+    | c1 == c2 =
+        do { rs <- mapM (uncurry (checkOverlapS am env)) $ zip s1 s2
+           ; return $ and rs }
+    | otherwise = return False
+
+checkOverlap am env DAny _ = return True
+checkOverlap am env _ DAny = return True
+checkOverlap am env _ _    = return False
+
+checkOverlapS :: Ord s => Automaton s -> Set (s,s) -> s -> s -> State (CAConf s) Bool
+checkOverlapS am env s1 s2 
+    | Set.member (s1,s2) env || Set.member (s2,s1) env 
+      = return False 
+    | otherwise 
+      = do { ol  <- getOLSet 
+           ; uol <- getUnOLSet
+           ; if Set.member (s1,s2) ol || Set.member (s2,s1) ol then 
+                 return True
+             else if Set.member (s1,s2) uol || Set.member (s2,s1) uol then 
+                 return False
+             else
+                 let derives1 = fromJust $ Map.lookup s1 am 
+                     derives2 = fromJust $ Map.lookup s2 am 
+                     comb     = [ (d1,d2) | d1 <- derives1, d2 <- derives2 ]
+                 in do { rs <- mapM (uncurry $ checkOverlap am (Set.insert (s1,s2) env)) comb
+                       ; if all not rs then 
+                             do { when (Set.null env) (addUnOL (s1,s2))
+                                ; return False }
+                         else
+                             do { addOL (s1,s2)
+                                ; return True } }}
+                                       
+
diff --git a/Makefile b/Makefile
new file mode 100644 (file)
index 0000000..b5c7b0b
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,11 @@
+TARGET = Main
+
+all : $(TARGET)
+
+$(TARGET): Main.hs AST.hs Parser.hs Util.hs Type.hs Shapify.hs CodeGen.hs
+       ghc --make -o $(TARGET) Main.hs
+
+clean:
+       rm $(TARGET)
+       rm -rf *.o *.hi
+       rm *~
\ No newline at end of file
diff --git a/Parser.hs b/Parser.hs
new file mode 100644 (file)
index 0000000..4de88ba
--- /dev/null
+++ b/Parser.hs
@@ -0,0 +1,137 @@
+module Parser (parseProgram, parseExpression, parseFile, parseString) where
+
+import Text.ParserCombinators.Parsec
+import qualified Text.ParserCombinators.Parsec.Token as Tk
+import Text.ParserCombinators.Parsec.Language
+
+import AST
+
+varId :: Parser String
+varId = do { c <- lower
+           ; cs <- many (alphaNum <|> char '_')
+           ; return $ (c:cs) }
+
+conId :: Parser String
+conId = do { c <- upper 
+           ; cs <- many (alphaNum <|> char '_')
+           ; return $ (c:cs) }
+
+number :: Parser Int
+number = do { cs <- many1 digit
+            ; return $ read cs }
+
+myLexer = Tk.makeTokenParser 
+            $ emptyDef {
+                    commentStart = "{-"
+                  , commentEnd   = "-}"
+                  , commentLine  = "--"           
+                  , reservedNames = ["let", "in","case","data","type"]
+                 }
+
+parens = Tk.parens myLexer
+symbol = Tk.symbol myLexer
+comma  = Tk.comma myLexer
+lexeme = Tk.lexeme myLexer
+reserved = Tk.reserved myLexer
+whiteSpace = Tk.whiteSpace myLexer
+
+
+cnv f s = case f s of
+            Left  err -> Left $ show err
+            Right r   -> Right $ r 
+
+parseProgram = 
+    (parse pProg "")
+
+parseExpression = 
+    (parse pExp "")
+
+
+parseString s = 
+    parseProgram s 
+
+
+parseFile filename =
+    return . parseProgram =<< readFile filename
+
+
+pProg = do { whiteSpace
+           ; ds <- many (lexeme pDecl)
+           ; return $ assignIDsAST (AST ds) }
+
+
+pDecl = do { pos <- getPosition 
+            ; fName <- lexeme varId 
+            ; ps    <- parens (pPats)
+            ; symbol "=" 
+            ; e     <- pExp
+            ; return $ Decl (Name fName) FTUndet ps e }
+
+
+pPats = sepBy pPat comma 
+
+
+pPat = do { pos <- getPosition 
+          ; do { c <- lexeme conId                
+               ; ps <- option [] $ parens pPats 
+               ; return $ PCon Nothing TUndet (Name c) ps }
+            <|> 
+            do { c <- lexeme $ number
+               ; return $ PCon Nothing TUndet (Name $show c) [] }
+            <|>
+            do { c <- lexeme varId
+               ; return $ PVar Nothing TUndet (Name c) }
+            <|>
+            do { _ <- string "("
+               ; p <- pPat 
+               ; _ <- string ")" 
+               ; return p } }
+
+
+pTExp = do { whiteSpace
+           ; pos <- getPosition
+           ; do { c  <- lexeme conId
+                ; es <- option [] $ parens (sepBy (pTExp) comma)
+                ; return $ ECon Nothing TUndet (Name c) es }
+             <|>
+             do { c <- lexeme $ number
+                ; return $ ECon Nothing TUndet (Name $ show c) [] }
+             <|>
+             do { c <- lexeme varId 
+                ; do { es <- parens (sepBy (pArg) comma) 
+                     ; return $ EFun Nothing TUndet (Name c) es }
+                  <|>
+                  do { return $ EVar Nothing TUndet (Name c) } } 
+             <|> 
+             do { _ <- string "("
+                ; c <- pTExp 
+                ; _ <- string ")" 
+                ; return c }}
+
+pExp = do { whiteSpace
+          ; pos <- getPosition
+          ; do { c  <- lexeme conId
+               ; es <- option [] $ parens (sepBy (pExp) comma)
+               ; return $ ECon Nothing TUndet (Name c) es }
+            <|>
+            do { c <- lexeme $ number
+               ; return $ ECon Nothing TUndet (Name $ show c) [] }
+            <|>
+            do { c <- lexeme varId 
+               ; do { es <- parens (sepBy (pExp) comma) 
+                    ; return $ EFun Nothing TUndet (Name c) es }
+                 <|>
+                 do { return $ EVar Nothing TUndet (Name c) } } 
+            <|> 
+            do { _ <- string "("
+               ; e <- pExp
+               ; _ <- string ")"
+               ; return e }
+          }
+
+
+pArg = do { pos <- getPosition
+          ; c <- lexeme varId
+          ; return $ EVar Nothing TUndet (Name c)} 
+
+
diff --git a/Shapify.hs b/Shapify.hs
new file mode 100644 (file)
index 0000000..cecfbdc
--- /dev/null
@@ -0,0 +1,169 @@
+module Shapify where
+
+import Util 
+import AST
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import Data.Function (fix)
+import Data.Maybe
+import Data.List ((\\), intersect)
+
+-- replaces  "Nil :: Unit"            -> "Z"
+--           "Cons(_,y) :: List Unit" ->  S(y)
+introNat :: AST -> AST 
+introNat (AST decls) =
+    AST $ map introNatD decls 
+    where
+      natT = TCon (Name "Nat") []
+      zP i   = PCon i natT (Name "Z") []
+      sP i x = PCon i natT (Name "S") [x]
+      zE i   = ECon i natT (Name "Z") []
+      sE i x = ECon i natT (Name "S") [x]
+      introNatD (Decl f (TFun is ts t) ps e) =
+          let ts' = map replT ts 
+              t'  = replT t
+              ps' = map replP ps
+              e'  = replE e
+          in Decl f (TFun is ts' t') ps' e'
+      replT (TCon (Name "List") [TCon (Name "Unit") []]) 
+          = TCon (Name "Nat") []
+      replT (TVar i)    = TVar i
+      replT (TCon c ts) = TCon c (map replT ts)
+
+      replP (PVar i (TCon (Name "List") [TCon (Name "Unit") []]) x)
+          = PVar i (TCon (Name "Nat") []) x
+      replP (PCon i (TCon (Name "List") [TCon (Name "Unit") []]) 
+                      (Name "Nil") [])
+          = zP i
+      replP (PCon i (TCon (Name "List") [TCon (Name "Unit") []])
+                      (Name "Cons") [x,y])
+          = sP i (replP y)
+      replP (PCon i t c ps)
+          = PCon i (replT t) c (map replP ps)
+
+      replE (EVar i (TCon (Name "List") [TCon (Name "Unit") []]) x)
+          = EVar i (TCon (Name "Nat") []) x
+      replE (ECon i (TCon (Name "List") [TCon (Name "Unit") []]) 
+                      (Name "Nil") [])
+          = zE i 
+      replE (ECon i (TCon (Name "List") [TCon (Name "Unit") []])
+                      (Name "Cons") [x,y])
+          = sE i (replE y)
+      replE (ECon i t c es) = ECon i (replT t) c (map replE es)
+      replE (EFun i t f es) = EFun i (replT t) f (map replE es)
+      
+
+-- removes parameters/arguments of which type is Unit
+-- FIXME: This function only checks "Unit" but no singleton types.
+specializeUnit :: AST -> AST
+specializeUnit (AST decls) =
+    assignIDsAST $ AST $ map spUnitD decls 
+    where
+      spUnitD (Decl f (TFun is ts t) ps e) =
+          let isUnits = map isUnit ts 
+              ts'     = map fst $ filter (\(_,b) -> not b) $ zip ts isUnits 
+              ps'     = map fst $ filter (\(_,b) -> not b) $ zip ps isUnits 
+          in Decl f (TFun is ts' t) ps' (spUnitE e)
+      spUnitE (EVar i t x)    = EVar i t x
+      spUnitE (ECon i t c es) = ECon i t c (map spUnitE es)
+      spUnitE (EFun i t f es) = 
+          let isUnits = map isUnit (map typeofE es) 
+              es'     = map fst $ filter (\(_,b) -> not b) $ 
+                          zip (map spUnitE es) isUnits 
+          in EFun i t f es' 
+      isUnit (TCon (Name "Unit") []) = True
+      isUnit _                       = False
+              
+
+-- replaces all "e::t" -> "Unit::Unit"
+--          and "p::t" -> "Unit::Unit" 
+-- in functions with type 
+--              "forall ... t ... . ..."
+shapify :: AST -> AST
+shapify (AST decls) = --AST $ map shapifyD decls 
+    specializeUnit $ 
+     AST $ fix (\f proced pend rdecls -> 
+                 let rest = pend \\ proced 
+                 in if null rest then 
+                        rdecls 
+                    else
+                        let decls' = shapifySig rest
+                            pend'  = collectPending decls'
+                        in f (rest++proced) pend' (decls'++rdecls))
+            [] initPend []
+    where
+--       initPend = Map.toList $ Map.fromList $ map 
+--                    (\(Decl f (TFun is ts t) _ _) -> 
+--                         (f,TFun [] (map (replT is) ts) (replT is t))) decls
+      initPend = Map.toList $ Map.fromList $ map
+                  (\(Decl f (TFun is _ _) _ _) -> (f,is)) decls
+
+      unitT = TCon (Name "Unit") []
+      unitP i = PCon i unitT (Name "Unit") []
+      unitE i = ECon i unitT (Name "Unit") []
+              
+      signituresMap 
+          = Map.fromList $ map 
+            (\(Decl f (TFun is ts t) _ _) -> (f,TFun is ts t)) decls
+
+      collectPending decls =
+          snub $ concatMap (\(Decl _ _ _ e) -> funCallsWithT e) decls
+      funCallsWithT (EVar _ _ _)    = []
+      funCallsWithT (ECon _ _ _ es) = concatMap funCallsWithT es
+      funCallsWithT (EFun _ _ (IName f is) es) 
+          = (Name f,is):concatMap funCallsWithT es 
+      funCallsWithT (EFun _ _ _ es) = concatMap funCallsWithT es 
+--       funCallsWithT (EFun t f es) = (f,TFun [] (map typeofE es) t):
+--                                        concatMap funCallsWithT es
+      shapifySig [] = []
+      shapifySig ((f,is'):rs)
+          = concatMap (\(d@(Decl g (TFun _ _ _) _ _))  ->
+                           if f == g then 
+                               [shapifyD is' d]
+                           else
+                               []
+                           ) decls ++shapifySig rs 
+      unifyU []                                   = []
+      unifyU ((TCon (Name "Unit") [], TVar i):rs)    = i:unifyU rs
+      unifyU ((TVar i, TCon (Name "Unit") []):rs)    = i:unifyU rs
+      unifyU ((TCon c ts, TCon c' ts'):rs) | c == c' = unifyU (zip ts ts') ++ unifyU rs
+      unifyU (_:rs)                                  = unifyU rs 
+      shapifyD is' (Decl (Name s) (TFun is ts t) ps e)
+          = let ftype = (TFun (is\\is') (map (replT is') ts) (replT is' t))
+            in Decl (IName s is') ftype
+                   (map (replP is') ps) (replE is' e)
+      replT is (TVar i) | i `elem` is = unitT
+                        | otherwise   = TVar i 
+      replT is (TCon c ts) = TCon c (map (replT is) ts)
+
+      replP is p = 
+          case typeofP p of 
+            TVar i | i `elem` is -> unitP (idofP p) 
+            _ -> 
+                case p of 
+                  PVar i t x    -> PVar i (replT is t) x
+                  PCon i t c ps -> PCon i (replT is t) c (map (replP is) ps)
+
+      replE is e = 
+          case typeofE e of 
+            TVar i | i `elem` is -> unitE (idofE e)
+            _ -> 
+                case e of 
+                  EVar i t x    -> EVar i (replT is t) x
+                  ECon i t c es -> ECon i (replT is t) c (map (replE is) es)
+                  EFun i t (IName f _) es ->
+                      funCallE i is t f es                       
+                  EFun i t (Name f) es ->
+                      funCallE i is t f es
+          where funCallE i is t f es = 
+                    let es' = map (replE is) es 
+                        TFun is' ts' t' 
+                            = fromJust $ Map.lookup (Name f) signituresMap 
+                        ts  = map typeofE es' 
+                        is'' = intersect 
+                                 is' 
+                                 (snub $ unifyU $ zip (t:ts) (t':ts'))
+                    in  
+                      EFun i (replT is t) (IName f is'') es'
diff --git a/Type.hs b/Type.hs
new file mode 100644 (file)
index 0000000..35e615e
--- /dev/null
+++ b/Type.hs
@@ -0,0 +1,246 @@
+module Type where
+
+import AST 
+
+import Data.Graph 
+import Control.Monad.State
+import Control.Monad.Error
+import Util
+import Data.Maybe
+import Data.List (nub,nubBy,union)
+
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+
+-- type inference
+
+initTMap :: [ (Name, FType) ]
+initTMap =
+    [ (Name "Z",   TFun [] [] (TCon (Name "Nat") [])),
+      (Name "S",   TFun [] [TCon (Name "Nat") []] (TCon (Name "Nat") [])),
+      (Name "Nil",  TFun [0] [] (TCon (Name "List") [TVar 0])),
+      (Name "Cons", TFun [0] [TVar 0, TCon (Name "List") [TVar 0]] 
+                (TCon (Name "List") [TVar 0])) ]
+
+
+typeInference (AST decls) = 
+    let mAst = do { (decls',_,_) <- 
+                        foldr (\decls m -> 
+                                   do (rdecls, tMap,  icount)  <- m
+                                      (decls', tMap', icount') <- inferenceStep decls tMap icount
+                                      return $ (decls'++rdecls, tMap', icount')
+                              ) (return ([],initTMap,initIcount)) declss
+                  ; return $ AST decls' } 
+    in case mAst of 
+         Left s  -> error s 
+         Right a ->  a 
+    where
+      initIcount = 100 -- FIXME 
+      declss = 
+          let scc = stronglyConnComp callGraph 
+          in  reverse $ map (\x -> case x of 
+                           AcyclicSCC f  -> 
+                               filter (\(Decl g _ _ _) -> f == g) decls
+                           CyclicSCC  fs -> 
+                               filter (\(Decl g _ _ _) -> g `elem` fs) decls) scc
+--      callGraph = map (\f -> (f,f,snub $ f:funCallsE e)) $
+--                     grupBy $ map (\(Decl f _ _ _) -> f) decls
+      callGraph = 
+          let fMap  = Map.fromListWith union $ 
+                       map (\(Decl f _ _ e) -> (f,f:funCallsE e)) decls 
+              fMap' = Map.map (snub) fMap 
+          in map (\(f,fs) -> (f,f,fs)) $ Map.toList fMap'
+      funCallsE (EVar _ _ v)    = []
+      funCallsE (EFun _ _ f es) = f:concatMap funCallsE es 
+      funCallsE (ECon _ _ _ es) = concatMap funCallsE es 
+
+
+inferenceStep decls tmap icount = 
+    let (decls0,  (tmpMap, icount0))  
+            = runState (makeInitConstr tmap decls) ([],icount)
+        (decls' , (constr, icount')) 
+            = runState (mapM (assignTypeVars tmpMap tmap) decls0) ([],icount0)
+    in
+      do { (tmpMap', etypeMap') <- solveConstr tmpMap constr
+         ; let decls'' = map (repl tmpMap' etypeMap') decls'
+         ; return (decls'', tmpMap' ++ tmap, icount') }
+        where 
+          repl tM cM (Decl f ftype ps e) =
+              Decl f (fromJust $ lookup f tM) (map replP ps) (replE e)
+              where
+                replP (PVar id (TVar i) v)    
+                    = PVar id (fromJust $ lookup i cM) v
+                replP (PCon id (TVar i) c ps)
+                    = PCon id (fromJust $ lookup i cM) c (map replP ps)
+                replE (EVar id (TVar i) v)
+                    = EVar id (fromJust $ lookup i cM) v
+                replE (ECon id (TVar i) c es)
+                    = ECon id (fromJust $ lookup i cM) c (map replE es)
+                replE (EFun id (TVar i) c es)
+                    = EFun id (fromJust $ lookup i cM) c (map replE es)
+          extractConstr ds = map (\(Decl f t _ _) -> (f,t)) $
+                                nubBy isSameFunc ds
+
+
+
+solveConstr tmpMap constr 
+    = substStep constr (tmpMap, rearrange constr)
+    where 
+      introForAll (k,TFun _ ts t) =
+          let vs = snub $ varsT t ++ concatMap varsT ts 
+          in (k,TFun vs ts t)
+      rearrange constr = 
+          let vs = nub $ concatMap (\(t1,t2) -> varsT t1 ++ varsT t2) constr 
+          in map (\x -> (x,TVar x)) vs                
+      varsT (TVar i)    = [i]
+      varsT (TCon _ ts) = concatMap varsT ts 
+      varsT (TUndet)    = []
+      substStep [] (tM,cM) = return (map introForAll tM,cM)
+      substStep ((t,t'):cs) (tM,cM) =
+          do { subs <- unify t t'
+             ; substStep
+                  (performSubstC subs cs)
+                  (performSubstTM subs tM, performSubstCM subs cM) }
+      performSubstC subs cs
+          = map (\(t1,t2) -> (performSubstT subs t1, performSubstT subs t2)) cs
+      performSubstTM subs tM 
+          = map (\(k,v) -> (k, performSubstFT subs v)) tM
+      performSubstCM subs cM
+          = map (\(k,v) -> (k, performSubstT subs v)) cM
+      performSubstFT subs (TFun is ts t) 
+          = TFun [] (map (performSubstT subs) ts) (performSubstT subs t)
+      performSubstT subs (TUndet) = TUndet 
+      performSubstT subs (TVar i) = 
+          case lookup (TVar i) subs of 
+            Just t' -> t'
+            _       -> TVar i
+      performSubstT subs (TCon c ts) =
+          TCon c (map (performSubstT subs) ts)
+      unify :: Type -> Type -> Either String [ (Type, Type) ]
+      unify (TVar i) t | not (i `elem` varsT t) = return [ (TVar i, t) ]
+      unify t (TVar i) | not (i `elem` varsT t) = return [ (TVar i, t) ]
+      unify (TVar i) (TVar j) | i == j = return []
+      unify (TCon c ts) (TCon c' ts') | c == c' 
+          = do { ss <- mapM (uncurry unify) $ zip ts ts'
+               ; return $ concat ss }
+      unify t t' = throwError $ "Can't unify types: " ++ show ( ppr (t,t'))
+                 
+    
+               
+
+makeInitConstr tmap decls =
+    do { mapM_ (\(Decl f t ps e) ->
+                      do { tmpMap <- getTmpMap 
+                         ; case t of
+                             FTUndet -> 
+                                 case lookup f tmpMap of 
+                                   Just t' -> 
+                                       return ()
+                                   _ -> 
+                                       do { i  <- newTypeVar 
+                                          ; is <- mapM (\_->newTypeVar) ps 
+                                          ; let t' = TFun [] (map TVar is) (TVar i) 
+                                          ; putTmpMap ((f,t'):tmpMap)
+                                          ; return ()  }
+                             _ -> 
+                                 putTmpMap ((f,t):tmpMap)}) $ 
+         (nubBy isSameFunc decls)
+       ; tmpMap <- getTmpMap
+       ; let decls' = map (\(Decl f t ps e) -> 
+                             Decl f (fromJust $ lookup f tmpMap) ps e) decls
+       ; return decls' }
+    where getTmpMap    = do { (tmpMap,i) <- get; return tmpMap }
+          putTmpMap tm = do { (_,i) <- get; put (tm,i) }
+          newTypeVar   = do { (tm,i) <- get; put (tm,i+1); return i}
+
+    
+               
+
+assignTypeVars tmpMap typeMap (Decl fname ftype ps e) =
+    do ps' <- mapM assignTypeVarsP ps
+       e'  <- assignTypeVarsE      e
+       unifyFT ftype (TFun [] (map typeofP ps') (typeofE e'))
+       let vtp = concatMap vtMapP ps'
+       let vte = vtMapE e'
+       mapM_ (\(x,t) -> case (lookup x vte) of 
+                          { Just t' -> unifyT t t'; _ -> return ()}) vtp 
+       mapM_ (\(x,t) -> case (lookup x vte) of 
+                          { Just t' -> unifyT t t' }) vte 
+       return $ Decl fname ftype ps' e'
+    where
+      vtMapP (PVar _ t x)    = [(x,t)]
+      vtMapP (PCon _ _ c ps) = concatMap vtMapP ps 
+      vtMapE (EVar _ t x)    = [(x,t)]
+      vtMapE (ECon _ _ c es) = concatMap vtMapE es
+      vtMapE (EFun _ _ c es) = concatMap vtMapE es
+--      newTypeVar :: State ( [(Type,Type)], Int ) Int
+      newTypeVar = do { (constr, icount) <- get
+                      ; put (constr, icount+1)
+                      ; return icount }
+      addConstr s t = do { (constr, icount) <- get
+                           ; put ((s,t):constr, icount) }
+      assignTypeVarsP (PVar id t v) = 
+          do { i <- newTypeVar
+             ; unifyT t (TVar i) 
+             ; return $ PVar id (TVar i) v } 
+      assignTypeVarsP (PCon id t c ps) = 
+          do { i <- newTypeVar
+             ; case lookup c typeMap of
+                 Just t' -> 
+                     do { ps' <- mapM assignTypeVarsP ps 
+                        ; unifyFT t' (TFun [] (map typeofP ps') (TVar i))
+                        ; unifyT  t  (TVar i)
+                        ; return $ PCon id (TVar i) c ps' }}
+      assignTypeVarsE (EVar id t v) = 
+          do { i <- newTypeVar 
+             ; unifyT t (TVar i)
+             ; return $ EVar id (TVar i) v }
+      assignTypeVarsE (ECon id t c es) =
+          do { i <- newTypeVar
+             ; case lookup c typeMap of
+                 Just t' -> 
+                     do { es' <- mapM assignTypeVarsE es 
+                        ; unifyFT t' (TFun [] (map typeofE es') (TVar i))
+                        ; unifyT  t  (TVar i)
+                        ; return $ ECon id (TVar i) c es' }}
+      assignTypeVarsE (EFun id t f es) =
+          do { i <- newTypeVar
+             ; case lookup f (typeMap ++ tmpMap)  of
+                 Just t' -> 
+                     do { es' <- mapM assignTypeVarsE es 
+                        ; unifyFT t' (TFun [] (map typeofE es') (TVar i))
+                        ; unifyT  t  (TVar i)
+                        ; return $ EFun id (TVar i) f es' }
+                 _ ->
+                     error $ (show f ++ " is not in " ++ show (typeMap ++ tmpMap))
+             }
+--      unifyT :: Type -> Type -> State ([(Type,Type)],Int) ()
+      unifyT (TUndet) _ = return ()
+      unifyT _ (TUndet) = return ()
+      unifyT (TVar i) (TVar j) | i == j = return ()
+      unifyT t t'       = addConstr t t'
+      unifyFT (FTUndet) _ = return ()
+      unifyFT _ (FTUndet) = return ()
+      unifyFT t t' = 
+          do { s  <- escapeForAll t 
+             ; s' <- escapeForAll t'
+             ; case (s,s') of 
+                 (TFun _ ts t, TFun _ ts' t') ->
+                     mapM_ (uncurry unifyT) $ zip (t:ts) (t':ts') }
+      escapeForAll (TFun is ts t) =
+          do { is' <- mapM (\_ -> newTypeVar) is 
+             ; let ts' = map (replaceTVar (zip is is')) ts
+             ; let t'   = replaceTVar (zip is is') t 
+             ; return $ TFun [] ts' t'}
+      replaceTVar table TUndet = TUndet
+      replaceTVar table (TVar i) =
+          case lookup i table of
+            Just j -> TVar j 
+            _      -> TVar i
+      replaceTVar table (TCon t ts) =
+          TCon t (map (replaceTVar table) ts)
+
+                     
+                          
\ No newline at end of file
diff --git a/Util.hs b/Util.hs
new file mode 100644 (file)
index 0000000..f23591c
--- /dev/null
+++ b/Util.hs
@@ -0,0 +1,42 @@
+module Util where 
+
+import Text.PrettyPrint
+import Data.List (group, sort)
+
+class Ppr a where
+    ppr :: a -> Doc 
+    pprList :: [a] -> Doc 
+    pprList as = brackets (sep $ punctuate comma (map ppr as))
+
+instance (Ppr Int) where 
+    ppr i = int i 
+
+instance (Ppr Integer) where
+    ppr i = integer i 
+
+
+instance (Ppr a, Ppr b) => Ppr (a,b) where
+    ppr (a,b) = parens (sep $ punctuate comma [ppr a, ppr b])
+
+instance (Ppr a, Ppr b, Ppr c) => Ppr (a,b,c) where 
+    ppr (a,b,c) = parens (sep $ punctuate comma [ppr a, ppr b, ppr c])
+
+instance Ppr a => Ppr [a] where
+    ppr as    = pprList as -- brackets (sep $ punctuate comma (map ppr as))
+
+instance Ppr Char where
+    ppr c     = char c
+
+instance (Ppr a, Ppr b) => Ppr (Either a b) where
+    ppr (Left a)  = text "Left"  <+> ppr a 
+    ppr (Right b) = text "Right" <+> ppr b
+
+instance (Ppr a) => Ppr (Maybe a) where
+    ppr (Nothing) = text "Nothing"
+    ppr (Just a)  = text "Just" <+> ppr a 
+
+
+{-# SPECIALIZE snub :: [Int] -> [Int] #-}
+{-# SPECIALIZE snub :: [String] -> [String] #-}
+snub :: Ord a => [a] -> [a]
+snub = map head . group .  sort  
diff --git a/example/init.txt b/example/init.txt
new file mode 100644 (file)
index 0000000..5869f43
--- /dev/null
@@ -0,0 +1,5 @@
+init (Nil)         = Nil
+init (Cons(a,Nil)) = Nil
+init (Cons(a,Cons(b,x))) = Cons(a,initWork(b,x))
+initWork(a,Nil)       = Nil
+initWork(a,Cons(b,x)) = Cons(a,initWork(b,x))
diff --git a/example/initHalf.txt b/example/initHalf.txt
new file mode 100644 (file)
index 0000000..69d4482
--- /dev/null
@@ -0,0 +1,7 @@
+initHalf(Nil)       = Nil
+initHalf(Cons(a,x)) = Cons(a,initHalfWork(x,x))
+
+initHalfWork(xs, Nil)         = Nil
+initHalfWork(xs, Cons(x,Nil)) = Nil
+initHalfWork(Cons(a,x), Cons(b,Cons(c,y)))
+    = Cons(a,initHalfWork(x,y))
diff --git a/example/rev.txt b/example/rev.txt
new file mode 100644 (file)
index 0000000..015da67
--- /dev/null
@@ -0,0 +1,3 @@
+reverse(xs) = rev(xs,Nil)
+rev(Nil,y)       = y
+rev(Cons(a,x),y) = rev(x,Cons(a,y))
diff --git a/example/seive.txt b/example/seive.txt
new file mode 100644 (file)
index 0000000..e6d3fff
--- /dev/null
@@ -0,0 +1,3 @@
+seive (Nil)               = Nil
+seive (Cons(a,Nil))       = Nil
+seive (Cons(a,Cons(b,x))) = Cons(b,seive(x))