import Data.List
import ParseType
+data TypedExpr = TypedExpr
+ { unTypeExpr :: Expr
+ , typeOf :: Typ
+ , onRightSide :: Bool
+ } deriving (Eq)
+
data Expr
= Var String
| App Expr Expr
| 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
-- 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
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 " == " $
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)
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
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
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)