| App Expr Expr
| Conc [Expr] -- Conc [] is Id
| Lambda String Expr
+ | Pair Expr Expr
| Map
deriving (Eq)
data BoolExpr
- = Equal Expr Expr
+ = BETrue
+ | Equal Expr Expr
+ | And BoolExpr BoolExpr
| AllZipWith String String BoolExpr Expr Expr
- | Condition String String Typ BoolExpr BoolExpr
+ | Condition Expr Expr Typ BoolExpr BoolExpr
+ | UnpackPair String String Expr Bool Typ BoolExpr
| UnCond String Bool Typ BoolExpr
| TypeVarInst Int BoolExpr
deriving (Eq)
equal = Equal
+unpackPair = UnpackPair
+
allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
e1 `equal` app (app Map (lambda v2 v1')) e2
- | Just v2' <- defFor v2 rel =
+ | Just v2' <- defFor v2 rel =
app (app Map (lambda v1 v2')) e1 `equal` e2
- | otherwise =
+ | otherwise =
AllZipWith v1 v2 rel e1 e2
defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
hasVar v (Lambda _ e) = hasVar v e
hasVar v Map = False
+isTuple (TPair _ _) = True
+isTuple _ = False
+
-- showing
showString v .
showString " -> ".
showsPrec 0 e
+ showsPrec _ (Pair e1 e2) = showParen True $
+ showsPrec 0 e1 .
+ showString "," .
+ showsPrec 0 e2
showsPrec _ Map = showString "map"
showIntercalate i [] = id
show (Equal e1 e2) = showsPrec 9 e1 $
showString " == " $
showsPrec 9 e2 ""
+ show (And be1 be2) = show be1 ++
+ " && " ++
+ show be2
show (AllZipWith v1 v2 be e1 e2) =
"allZipWith " ++
"( " ++
showsPrec 11 e2 ""
show (Condition v1 v2 t be1 be2) =
"forall " ++
- v1 ++
+ showsPrec 11 v1 "" ++
" :: " ++
arrowInstType False t ++
", " ++
- v2 ++
+ showsPrec 11 v2 "" ++
" :: " ++
arrowInstType True t ++
".\n" ++
- indent 2 (show be1) ++
- "==>\n" ++
+ (if be1 /= BETrue then indent 2 (show be1) ++ "==>\n" else "") ++
indent 2 (show be2)
+ show (UnpackPair v1 v2 e b t be) =
+ "let (" ++
+ v1 ++
+ "," ++
+ v2 ++
+ ") = " ++
+ showsPrec 0 e "" ++
+ " :: " ++
+ arrowInstType b t ++
+ " in\n" ++
+ indent 2 (show be)
show (UnCond v1 b t be1) =
"forall " ++
v1 ++
ait d (List t) = "[" ++ ait 0 t ++ "]"
ait d (TEither t1 t2) = "Either " ++ ait 11 t1 ++
" " ++ ait 11 t2
- ait d (TPair t1 t2) = "(" ++ ait 0 t1 ++ ", " ++ ait 0 t2 ++ ")"
+ ait d (TPair t1 t2) = "(" ++ ait 0 t1 ++ "," ++ ait 0 t2 ++ ")"
paren b p = if b then "(" ++ p ++ ")" else p
-{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternGuards, FlexibleContexts #-}
module SimpleFT where
freeTheorem' e1 e2 Int = return $
Equal e1 e2
-freeTheorem' e1 e2 (List t) = do
- [v1,v2] <- asks (take 2)
- local (drop 2) $ do
- map <- freeTheorem' (Var v1) (Var v2) t
- return $ allZipWith v1 v2 map e1 e2
-
-freeTheorem' e1 e2 (Arrow t1 t2) = do
- [v1,v2] <- asks (take 2)
- local (drop 2) $ do
- cond <- freeTheorem' (Var v1) (Var v2) t1
- case (defFor v1 cond, defFor v2 cond) of
- (Just ev1, _) -> do
- concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
- return $ unCond v2 True t1 concl
- (Nothing,Just ev2) -> do
- concl <- freeTheorem' (App e1 (Var v1)) (App e2 ev2) t2
- return $ unCond v1 False t1 concl
- _ -> do
- concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
- return $ Condition v1 v2 t1 cond concl
-
freeTheorem' e1 e2 (TVar (TypVar i)) = return $
Equal (App (Var ("g"++show i)) e1) e2
+freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
+ fillTuplevars t1 $ \ve1 ->
+ fillTuplevars t1 $ \ve2 -> do
+ cond <- freeTheorem' ve1 ve2 t1
+ concl <- freeTheorem' (App e1 ve1) (App e2 ve2) t2
+ return $ Condition ve1 ve2 t1 cond concl
+
+ | otherwise = getVars 2 $ \[v1,v2] -> do
+ cond <- freeTheorem' (Var v1) (Var v2) t1
+ case (defFor v1 cond, defFor v2 cond) of
+ (Just ev1, _) -> do
+ concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
+ return $ unCond v2 True t1 concl
+ (Nothing,Just ev2) -> do
+ concl <- freeTheorem' (App e1 (Var v1)) (App e2 ev2) t2
+ 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
+
+freeTheorem' e1 e2 (List t) = getVars 2 $ \[v1,v2] -> do
+ map <- freeTheorem' (Var v1) (Var v2) t
+ return $ allZipWith v1 v2 map e1 e2
+
+{-
+freeTheorem' e1 e2 (TPair t1 t2) = getVars 4 $ \[x1,x2,y1,y2] -> do
+ concl1 <- freeTheorem' (Var x1) (Var y1) t1
+ concl2 <- freeTheorem' (Var x2) (Var y2) t2
+ return $ Condition x1 y1 t1 BETrue $
+ Condition x2 y2 t2 (
+ And (Equal e2 (Pair (Var y1) (Var y2)))
+ (Equal e1 (Pair (Var x1) (Var x2)))) $
+ And concl1 concl2
+-}
+
+freeTheorem' (Pair x1 x2) (Pair y1 y2) (TPair t1 t2) = do
+ concl1 <- freeTheorem' x1 y1 t1
+ concl2 <- freeTheorem' x2 y2 t2
+ return $ And concl1 concl2
+
+freeTheorem' e1 e2 t@(TPair t1 t2) = getVars 4 $ \[x1,x2,y1,y2] -> do
+ concl1 <- freeTheorem' (Var x1) (Var y1) t1
+ concl2 <- freeTheorem' (Var x2) (Var y2) t2
+ return $ unpackPair x1 x2 e1 False t $
+ unpackPair y1 y2 e2 True t $
+ And concl1 concl2
+
freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
freeTheorem' e1 e2 (All (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 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)
+