Showing with types

diff --git a/Expr.hs b/Expr.hs
index 0c44f7a..52c99d2 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -2,11 +2,12 @@
 module Expr where
 
 import Data.List
+import ParseType
 
 data Expr
        = Var String
        | App Expr Expr
-       | Conc [Expr]
+       | Conc [Expr] -- Conc [] is Id
        | Lambda String Expr
        | Map
             deriving (Eq)
@@ -14,21 +15,39 @@ data Expr
 data BoolExpr 
        = Equal Expr Expr
        | Pairwise String String BoolExpr Expr Expr
-       | Condition String String BoolExpr BoolExpr
-       | UnCond String BoolExpr
+       | Condition String String Typ BoolExpr BoolExpr
+       | UnCond String Bool Typ BoolExpr
        | TypeVarInst Int BoolExpr
             deriving (Eq)
 
 -- Smart constructors
 
-unCond v (Equal l r) | (Just l') <- isApplOn v l 
-                    , (Just r') <- isApplOn v r = 
+equal = Equal
+
+pairwise v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
+                               e1 `equal` app (app Map (lambda v2 v1')) e2
+                         | Just v2' <- defFor v2 rel =
+                               app (app Map (lambda v1 v2')) e1 `equal` e2
+                         | otherwise =
+                               Pairwise v1 v2 rel e1 e2
+
+defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
+                         | (Var v) == e2 = Just e1
+defFor _ _                               = Nothing
+
+app Map (Conc []) = Conc []
+app (Conc []) v   = v
+app f v           = App f v
+
+unCond v b t (Equal l r) | (Just l') <- isApplOn v l 
+                        , (Just r') <- isApplOn v r = 
        if hasVar v l' || hasVar v r'
-       then UnCond v (Equal l' r')
+       then UnCond v b t (Equal l' r')
        else (Equal l' r')
-unCond v e = UnCond v e
+unCond v b t e = UnCond v b t e
 
 lambda v e | (Just e') <- isApplOn v e, not (hasVar v e') = e'
+          | Var v == e                                   = Conc []
            | otherwise                                    = Lambda v e
 
 
@@ -44,6 +63,8 @@ isApplOn _ _                                               = Nothing
 hasVar v (Var v')     = v == v'
 hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
 hasVar v (Conc es)    = any (hasVar v) es
+hasVar v (Lambda _ e) = hasVar v e
+hasVar v Map          = False
 
 
 -- showing
@@ -59,6 +80,8 @@ instance Show Expr where
        showsPrec d (Var s)     = showString s
        showsPrec d (App e1 e2) = showParen (d>10) $
                showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
+       showsPrec d (Conc [])   = showString "id"
+       showsPrec d (Conc [e])  = showsPrec d e
        showsPrec d (Conc es)   = showParen (d>9) $
                showIntercalate (showString " . ") (map (showsPrec 10) es)
        showsPrec d (Lambda v e) = showParen True $ 
@@ -81,30 +104,38 @@ instance Show BoolExpr where
                        showParen (d>10) $
                        showString "allZipWith " .
                        showParen True ( 
-                               showString "(\\" .
+                               showString "\\" .
                                showString v1 .
                                showChar ' ' .
                                showString v2 . 
                                showString " -> " .
-                               showsPrec 0 e1
+                               showsPrec 0 be
                        ) .
                        showChar ' ' .
+                       showsPrec 11 e1 .
+                       showChar ' ' .
                        showsPrec 11 e2
-       showsPrec d (Condition v1 v2 be1 be2) = 
+       showsPrec d (Condition v1 v2 t be1 be2) = 
                        showParen (d>6) $
                        showString "forall " . 
                        showString v1 . 
-                       showChar ' ' .
+                       showString " :: " .
+                       arrowInstType False t .
+                       showString ", " .
                        showString v2 . 
-                       showString ". " .
+                       showString " :: " .
+                       arrowInstType True t .
+                       showString ".\n" .
                        showsPrec 9 be1 .
                        showString " ==> " .
                        showsPrec 6 be2
-       showsPrec d (UnCond v1 be1) = 
+       showsPrec d (UnCond v1 b t be1) = 
                        showParen (d>6) $
                        showString "forall " . 
                        showString v1 . 
-                       showString ". " .
+                       showString " :: " .
+                       arrowInstType b t .
+                       showString ".\n" .
                        showsPrec 6 be1
        showsPrec d (TypeVarInst i be) = 
                        showParen (d>6) $
@@ -121,3 +152,10 @@ instance Show BoolExpr where
                        showString ".\n" .
                        showsPrec 6 be
 
+arrowInstType :: Bool -> Typ -> ShowS
+arrowInstType b Int                    = showString "Int" 
+arrowInstType False (TVar (TypVar i))  = showString "t" .  shows (2*i-1)
+arrowInstType True (TVar (TypVar i))   = showString "t" .  shows (2*i)
+arrowInstType b (Arrow t1 t2)          = arrowInstType b t1 .
+                                         showString " -> " .
+                                         arrowInstType b t2

diff --git a/SimpleFT.hs b/SimpleFT.hs
index 12585dc..7f297d4 100644 (file)
--- a/SimpleFT.hs
+++ b/SimpleFT.hs
@@ -22,27 +22,25 @@ freeTheorem' e1 e2 (List t) = do
        [v1,v2] <- asks (take 2)
        local (drop 2) $ do
                map <- freeTheorem' (Var v1) (Var v2) t
-               return $ case map of
-                 (Equal (Var v1') ev1) | v1' == v1 -> 
-                       if ev1 == (Var v2)
-                       then Equal e1 e2
-                       else Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
-                 _ ->       Pairwise v1 v2 map e1 e2
+               return $ pairwise 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 cond of
-                 (Equal (Var v1') ev1) | v1' == v1 -> do
-                       concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
-                       return $ unCond v2 concl
+               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 cond concl
+                       return $ Condition v1 v2 t1 cond concl
 
 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
-       Equal e1 (App (Var ("g"++show i)) e2)
+       Equal (App (Var ("g"++show i)) e1) e2
 
 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