Deep tuple pattern generation

diff --git a/Expr.hs b/Expr.hs
index 2846c6b..180a376 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -9,13 +9,17 @@ data Expr
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
        | Lambda String Expr
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
        | Lambda String Expr

+       | Pair Expr Expr

        | Map
             deriving (Eq)
 
 data BoolExpr 
        | Map
             deriving (Eq)
 
 data BoolExpr 

-       = Equal Expr Expr
+       = BETrue
+       | Equal Expr Expr
+       | And BoolExpr BoolExpr

        | AllZipWith String String BoolExpr Expr Expr
        | 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)
        | UnCond String Bool Typ BoolExpr
        | TypeVarInst Int BoolExpr
             deriving (Eq)


@@ -24,11 +28,13 @@ data BoolExpr
 
 equal = Equal
 
 
 equal = Equal
 

+unpackPair = UnpackPair
+

 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
                                e1 `equal` app (app Map (lambda v2 v1')) e2
 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
                                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
                                AllZipWith v1 v2 rel e1 e2
 
 defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2


@@ -66,6 +72,9 @@ hasVar v (Conc es)    = any (hasVar v) es
 hasVar v (Lambda _ e) = hasVar v e
 hasVar v Map          = False
 
 hasVar v (Lambda _ e) = hasVar v e
 hasVar v Map          = False
 

+isTuple (TPair _ _) = True
+isTuple _           = False
+

 
 -- showing
 
 
 -- showing
 


@@ -89,6 +98,10 @@ instance Show Expr where
                                    showString v .
                                    showString " -> ".
                                   showsPrec 0 e 
                                    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
        showsPrec _ Map           = showString "map"
 
 showIntercalate i []  = id


@@ -99,6 +112,9 @@ instance Show BoolExpr where
        show (Equal e1 e2) = showsPrec 9 e1 $
                             showString " == " $
                             showsPrec 9 e2 ""
        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 " ++
                        "( " ++
        show (AllZipWith v1 v2 be e1 e2) =
                        "allZipWith " ++
                        "( " ++


@@ -115,17 +131,27 @@ instance Show BoolExpr where
                        showsPrec 11 e2 ""
        show (Condition v1 v2 t be1 be2) = 
                        "forall " ++
                        showsPrec 11 e2 ""
        show (Condition v1 v2 t be1 be2) = 
                        "forall " ++

-                       v1 ++
+                       showsPrec 11 v1 "" ++

                        " :: " ++
                        arrowInstType False t ++
                        ", " ++
                        " :: " ++
                        arrowInstType False t ++
                        ", " ++

-                       v2 ++
+                       showsPrec 11 v2 "" ++

                        " :: " ++
                        arrowInstType True t ++
                        ".\n" ++
                        " :: " ++
                        arrowInstType True t ++
                        ".\n" ++

-                       indent 2 (show be1) ++
-                       "==>\n" ++
+                       (if be1 /= BETrue then indent 2 (show be1) ++ "==>\n" else "") ++

                        indent 2 (show be2)
                        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 ++
        show (UnCond v1 b t be1) = 
                        "forall " ++
                        v1 ++


@@ -160,6 +186,6 @@ arrowInstType b = ait 0
        ait d (List t)                  = "[" ++ ait 0 t ++ "]"
        ait d (TEither t1 t2)           = "Either " ++ ait 11 t1 ++ 
                                                 " " ++ ait 11 t2
        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
 
 paren b p   =  if b then "(" ++ p ++ ")" else p

diff --git a/SimpleFT.hs b/SimpleFT.hs
index ec9d7af..add0c1a 100644 (file)
--- a/SimpleFT.hs
+++ b/SimpleFT.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternGuards  #-}
+{-# LANGUAGE PatternGuards, FlexibleContexts  #-}

 
 module SimpleFT where
 
 
 module SimpleFT where
 


@@ -18,29 +18,66 @@ freeTheorem' :: Expr -> Expr -> Typ -> Reader [String] BoolExpr
 freeTheorem' e1 e2 Int = return $
        Equal e1 e2
 
 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 (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
 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)
+