Carry types with functions

diff --git a/Expr.hs b/Expr.hs
index 2563050..a956f82 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -4,6 +4,12 @@ module Expr where
 import Data.List
 import ParseType
 
+data TypedExpr = TypedExpr
+       { unTypeExpr    :: Expr
+       , typeOf        :: Typ
+       , onRightSide   :: Bool
+       } deriving (Eq)
+
 data Expr
        = Var String
        | App Expr Expr
@@ -18,7 +24,7 @@ data BoolExpr
        | Equal Expr Expr
        | And BoolExpr BoolExpr
        | AllZipWith String String BoolExpr Expr Expr
-       | Condition Expr Expr Typ BoolExpr BoolExpr
+       | Condition TypedExpr TypedExpr  BoolExpr BoolExpr
        | UnpackPair String String Expr Bool Typ BoolExpr
        | UnCond String Bool Typ BoolExpr
        | TypeVarInst Int BoolExpr
@@ -26,6 +32,10 @@ data BoolExpr
 
 -- Smart constructors
 
+-- Left or right side of a relation (affects type variables)
+typedLeft e t = TypedExpr e t False
+typedRight e t = TypedExpr e t True
+
 equal = Equal
 
 unpackPair = UnpackPair
@@ -113,6 +123,13 @@ showIntercalate i []  = id
 showIntercalate i [x] = x
 showIntercalate i (x:xs) = x . i . showIntercalate i xs
 
+instance Show TypedExpr where
+       showsPrec d (TypedExpr e t rightSide) = 
+               showParen (d>10) $
+                       showsPrec 0 e .
+                       showString " :: " .
+                       showString (arrowInstType rightSide t)
+
 instance Show BoolExpr where
        show (Equal e1 e2) = showsPrec 9 e1 $
                             showString " == " $
@@ -134,15 +151,11 @@ instance Show BoolExpr where
                        showsPrec 11 e1 "" ++
                        " " ++
                        showsPrec 11 e2 ""
-       show (Condition v1 v2 t be1 be2) = 
+       show (Condition tv1 tv2 be1 be2) = 
                        "forall " ++
-                       showsPrec 11 v1 "" ++
-                       " :: " ++
-                       arrowInstType False t ++
+                       showsPrec 0 tv1 "" ++
                        ", " ++
-                       showsPrec 11 v2 "" ++
-                       " :: " ++
-                       arrowInstType True t ++
+                       showsPrec 0 tv2 "" ++
                        ".\n" ++
                        (if be1 /= BETrue then indent 2 (show be1) ++ "==>\n" else "") ++
                        indent 2 (show be2)

diff --git a/SimpleFT.hs b/SimpleFT.hs
index 9113a61..150a03d 100644 (file)
--- a/SimpleFT.hs
+++ b/SimpleFT.hs
@@ -24,11 +24,13 @@ freeTheorem' e1 e2 (TVar (TypVar i)) = return $
 freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
        -- Create patterns for (possily nested) tuples and only give
        -- the inner variables names
-       fillTuplevars t1 $ \ve1 -> 
-               fillTuplevars t1 $ \ve2 ->  do
-                       cond  <- freeTheorem' ve1 ve2 t1
+       fillTuplevars False t1 $ \tve1 -> 
+               fillTuplevars True t1 $ \tve2 ->  do
+                       let ve1 = unTypeExpr tve1
+                            ve2 = unTypeExpr tve2
+                       cond  <- freeTheorem' (ve1) (ve2) t1
                        concl <- freeTheorem' (App e1 ve1) (App e2 ve2) t2
-                       return $ Condition ve1 ve2 t1 cond concl
+                       return $ Condition tve1 tve2 cond concl
 
        -- No tuple on the left hand side:
                                  | otherwise  = getVars 2 $ \[v1,v2] -> do
@@ -43,7 +45,10 @@ freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
                return $ unCond v1 False t1 concl
          _ -> do
                concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
-               return $ Condition (Var v1) (Var v2) t1 cond concl
+               return $ Condition (typedLeft (Var v1) t1)
+                                   (typedRight(Var v2) t1)
+                                   cond
+                                   concl
 
 freeTheorem' e1 e2 (List t) = getVars 2 $ \[v1,v2] -> do
        map <- freeTheorem' (Var v1) (Var v2) t
@@ -78,10 +83,12 @@ freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1
 getVars :: (MonadReader [String] m) => Int -> ([String] -> m a) -> m a
 getVars n a = asks (take n) >>= local (drop n) . a 
 
-fillTuplevars :: (MonadReader [String] m) => Typ -> (Expr -> m a) -> m a
-fillTuplevars (TPair t1 t2) a = do
-       fillTuplevars t1 $ \ve1 ->
-               fillTuplevars t2 $ \ve2 ->
-                       a (Pair ve1 ve2)
-fillTuplevars _ a = getVars 1 $ \[s] -> a (Var s)
+fillTuplevars :: (MonadReader [String] m) => Bool -> Typ -> (TypedExpr -> m a) -> m a
+fillTuplevars rightSide t@(TPair t1 t2) a = do
+       fillTuplevars rightSide t1 $ \ve1 ->
+               fillTuplevars rightSide t2 $ \ve2 ->
+                       let pair = Pair (unTypeExpr ve1) (unTypeExpr ve2) in
+                       a (TypedExpr pair t rightSide)
+fillTuplevars rightSide t a = getVars 1 $ \[s] ->
+                       a (TypedExpr (Var s) t rightSide)