Remove TypSamples
[darcs-mirror-polyfix.git] / Expr.hs
diff --git a/Expr.hs b/Expr.hs
index 6af565f..b895827 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -26,13 +26,14 @@ data EVar = F
 
 data Expr
        = Var EVar
-       | TheOneFunc
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
        | Lambda TypedExpr Expr
        | Pair Expr Expr
        | Map
+       | ConstUnit
        | EitherMap
+       | EUnit
             deriving (Eq, Typeable, Data)
 
 data LambdaBE = CurriedEquals Typ
@@ -109,11 +110,13 @@ andEither lbe1 lbe2 e1 e2 | Just f1 <- arg1IsFunc lbe1
                          | otherwise
                           = AndEither lbe1 lbe2 (unTypeExpr e1) (unTypeExpr e2)
 
+arg1IsFunc :: LambdaBE -> Maybe TypedExpr
 arg1IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 arg1IsFunc (LambdaBE v1 v2 rel) | Just v1' <- defFor v1 rel
                                 = Just (lambda v2 v1')
                                | otherwise = Nothing
 
+arg2IsFunc :: LambdaBE -> Maybe TypedExpr
 arg2IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 arg2IsFunc (LambdaBE v1 v2 rel) | Just v2' <- defFor v2 rel
                                 = Just (lambda v1 v2')
@@ -199,19 +202,26 @@ replaceTermBE d r = go
        go (Condition vs cond concl)
                           = condition vs (go cond) (go concl)
        go (UnpackPair v1 v2 e be)
-                          = unpackPair v1 v2 (go' e) (go be)
+                          = unpackPair v1 v2 (goT e) (go be)
        go (TypeVarInst _ _ _) = error "TypeVarInst not expected here"
 
-       go' :: Data a => a -> a
        go' = replaceExpr d r
 
+       goT te = te { unTypeExpr = go' (unTypeExpr te) }
+
        goL (CurriedEquals t)   = (CurriedEquals t)
        goL (LambdaBE v1 v2 be) = lambdaBE v1 v2 (go be)
 
-replaceExpr :: Data a => Expr -> Expr -> a -> a
-replaceExpr d r = everywhere (mkT go)
-  where go e | e == d    = r 
-             | otherwise = e
+
+replaceExpr :: Expr -> Expr -> Expr -> Expr
+replaceExpr d r = go
+  where go e | e == d    = r
+        go (App e1 e2)   = app' (go e1) (go e2)
+       go (Conc es)     = foldr conc (Conc []) (map go es)
+       go (Lambda te e) = lambda' te (go e)
+       go (Pair e1 e2)  = Pair (go e1) (go e2)
+       go e             = e
+
 
 -- | Is inside the term a definition for the variable?
 findReplacer :: TypedExpr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
@@ -249,19 +259,24 @@ app te1 te2 | Arrow t1 t2 <- typeOf te1
            , t3          <- typeOf te2 
             , t1 == t3 
             = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
- where app' Map (Conc []) = Conc []   -- map id = id
-       app' (Conc []) v   = v         -- id x   = x
-       app' f v           = App f v
 app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
                                                            show te1 ++ " " ++ show te2
 
+app' :: Expr -> Expr -> Expr
+app' Map (Conc []) = Conc []   -- map id = id
+app' ConstUnit _   = EUnit     -- id x   = x
+app' (Conc []) v   = v         -- id x   = x
+app' f v           = App f v
+
 lambda :: TypedExpr -> TypedExpr -> TypedExpr
-lambda tv e = TypedExpr inner (Arrow (typeOf tv) (typeOf e))
-  where inner | (Just e') <- isApplOn (unTypeExpr tv) (unTypeExpr e)
+lambda tv e = TypedExpr (lambda' tv (unTypeExpr e)) (Arrow (typeOf tv) (typeOf e))
+
+lambda' :: TypedExpr -> Expr -> Expr
+lambda' tv e  | (Just e') <- isApplOn (unTypeExpr tv) e
              , not (unTypeExpr tv `occursIn` e')
-                          = e'
-             | tv == e   = Conc []
-              | otherwise = Lambda tv (unTypeExpr e)
+                                     = e'
+             | unTypeExpr tv == e   = Conc []
+              | otherwise            = Lambda tv e
 
 conc :: Expr -> Expr -> Expr
 conc (Conc xs) (Conc ys) = Conc (xs  ++ ys)
@@ -272,6 +287,16 @@ conc x          y        = Conc ([x,y])
 
 -- Specialization of g'
 
+specialize :: BoolExpr -> BoolExpr
+specialize (TypeVarInst strict i be') = 
+               replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else ConstUnit) .
+               everywhere (mkT $ go) $
+               be
+       where be = specialize be'
+              go (TypInst i' _) | i' == i = TUnit
+              go tv                       = tv                 
+-- No need to go further once we are through the quantors
+specialize be = be
 
 -- Helpers
 
@@ -321,7 +346,9 @@ instance Show Expr where
                                   showsPrec 0 e1 .
                                   showString "," .
                                   showsPrec 0 e2
+       showsPrec _ EUnit         = showString "()"
        showsPrec _ Map           = showString "map"
+       showsPrec d ConstUnit     = showParen (d>10) $ showString "const ()"
        showsPrec _ EitherMap     = showString "eitherMap"
 
 showIntercalate :: ShowS -> [ShowS] -> ShowS
@@ -392,8 +419,8 @@ instance Show BoolExpr where
                        ", t" ++
                        show (2*i) ++
                        ", " ++
-                       (if strict then "strict " else "") ++
-                        "functions g" ++
+                       (if strict then "strict " else "(strict) ") ++
+                       "functions g" ++
                        show i ++
                        " :: t" ++
                        show (2*i-1) ++
@@ -410,6 +437,7 @@ showTypePrec _ Int                      = "Int"
 showTypePrec _ (TVar (TypVar i))            = "a"++show i
 showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
                                    |     b = "t" ++  show (2*i)
+showTypePrec _ (TVar (TUnit))               = "()"
 showTypePrec d (Arrow t1 t2)                = paren (d>9) $ 
                                                showTypePrec 10 t1 ++
                                                " -> " ++