Large refactor: Use TypedExpr data type
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 12:08:07 +0000 (12:08 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 12:08:07 +0000 (12:08 +0000)
Expr.hs
ParseType.hs
SimpleFT.hs

diff --git a/Expr.hs b/Expr.hs
index a956f82..1fd49bc 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
-{-# LANGUAGE PatternGuards  #-}
+{-# LANGUAGE PatternGuards, DeriveDataTypeable   #-}
 module Expr where
 
 import Data.List
 import ParseType
 
+import Data.Generics hiding (typeOf)
+import Data.Generics.Schemes
+
 data TypedExpr = TypedExpr
        { unTypeExpr    :: Expr
        , typeOf        :: Typ
-       , onRightSide   :: Bool
-       } deriving (Eq)
+       } deriving (Eq, Typeable, Data)
+
+typedLeft, typedRight :: Expr -> Typ -> TypedExpr
+typedLeft  e t = TypedExpr e (instType False t)
+typedRight e t = TypedExpr e (instType True t)
 
 data Expr
        = Var String
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
-       | Lambda String Expr
+       | Lambda TypedExpr Expr
        | Pair Expr Expr
        | Map
-            deriving (Eq)
+            deriving (Eq, Typeable, Data)
 
 data BoolExpr 
        = BETrue
        | Equal Expr Expr
        | And BoolExpr BoolExpr
-       | AllZipWith String String BoolExpr Expr Expr
-       | Condition TypedExpr TypedExpr  BoolExpr BoolExpr
-       | UnpackPair String String Expr Bool Typ BoolExpr
-       | UnCond String Bool Typ BoolExpr
+       | AllZipWith TypedExpr TypedExpr BoolExpr Expr Expr
+       | Condition [TypedExpr] BoolExpr BoolExpr
+       | UnpackPair TypedExpr TypedExpr TypedExpr BoolExpr
        | TypeVarInst Int BoolExpr
-            deriving (Eq)
+            deriving (Eq, Typeable, Data)
 
 -- 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
+equal te1 te2 | typeOf te1 /= typeOf te2 = error "Type mismatch in equal"
+              | otherwise                = Equal (unTypeExpr te1) (unTypeExpr te2)
 
 unpackPair = UnpackPair
 
 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
-                               e1 `equal` app (app Map (lambda v2 v1')) e2
+                               e1 `equal` amap (lambda v2 v1') e2
                            | Just v2' <- defFor v2 rel =
-                               app (app Map (lambda v1 v2')) e1 `equal` e2
+                               amap (lambda v1 v2') e1 `equal` e2
                            | otherwise =
-                               AllZipWith v1 v2 rel e1 e2
+                               AllZipWith v1 v2 rel (unTypeExpr e1) (unTypeExpr e2)
+
+amap tf tl | Arrow t1 t2 <- typeOf tf
+           , List t      <- typeOf tl
+           , t1 == t
+           = let tMap = TypedExpr Map (Arrow (List t1) (List t2))
+            in app (app tMap tf) tl
+amap tf tl | otherwise = error "Type error in map"
 
 -- | Is inside the term a definition for the variable?
-defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
-                         | (Var v) == e2 = Just e1
-defFor v (e1 `And` e2)   | Just d  <- defFor v e1
-                        , Nothing <- defFor v e2 = Just d
-defFor v (e1 `And` e2)   | Just d  <- defFor v e2
-                        , Nothing <- defFor v e1 = Just d
-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 b t (Equal l' r')
+defFor :: TypedExpr -> BoolExpr -> Maybe TypedExpr
+defFor tv be | Just e' <- defFor' (unTypeExpr tv) be
+                         = Just (TypedExpr e' (typeOf tv))
+             | otherwise = Nothing
+       
+defFor' v (e1 `Equal` e2) | v == e1                 = Just e2
+                          | v == e2                 = Just e1
+defFor' v (e1 `And` e2)   | Just d  <- defFor' v e1
+                         , Nothing <- defFor' v e2 = Just d
+defFor' v (e1 `And` e2)   | Just d  <- defFor' v e2
+                         , Nothing <- defFor' v e1 = Just d
+defFor' _ _                                         = Nothing
+
+app te1 te2 | Arrow t1 t2 <- typeOf te1
+           , t3          <- typeOf te2 
+            , t1 == t3 
+            = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
+ where app' Map (Conc []) = Conc []
+       app' (Conc []) v   = v
+       app' f v           = App f v
+app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
+                                                           show te1 ++ " " ++ show te2
+
+unCond v (Equal l r) | (Just l') <- isApplOn (unTypeExpr v) l 
+                    , (Just r') <- isApplOn (unTypeExpr v) r = 
+       if v `occursIn` l' || v `occursIn` r'
+       then Condition [v] BETrue (Equal l' r')
        else (Equal l' r')
-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
+unCond v e = Condition [v] BETrue e
 
+lambda tv e = TypedExpr inner (Arrow (typeOf tv) (typeOf e))
+  where inner | (Just e') <- isApplOn (unTypeExpr tv) (unTypeExpr e)
+             , not (unTypeExpr tv `occursIn` e')
+                          = e'
+             | tv == e   = Conc []
+              | otherwise = Lambda tv (unTypeExpr e)
 
 conc f (Conc fs) = Conc (f:fs)
 
 -- Helpers
 
-isApplOn v (Var _)                                         = Nothing
-isApplOn v (App f (Var v')) | v == v'                      = Just (Conc [f])
-isApplOn v (App f e)        | (Just inner) <- isApplOn v e = Just (conc f inner)
-isApplOn _ _                                               = Nothing
+isApplOn e e'         | e == e'                       = Nothing
+isApplOn e (App f e') | e == e'                       = Just (Conc [f])
+isApplOn e (App f e') | (Just inner) <- isApplOn e e' = Just (conc f inner)
+isApplOn _ _                                          = Nothing
 
 hasVar v (Var v')     = v == v'
 hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
@@ -87,6 +109,8 @@ hasVar v (Conc es)    = any (hasVar v) es
 hasVar v (Lambda _ e) = hasVar v e
 hasVar v Map          = False
 
+e `occursIn` e'       = not (null (listify (==e) e'))
+
 isTuple (TPair _ _) = True
 isTuple _           = False
 
@@ -108,11 +132,11 @@ instance Show Expr where
        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 $ 
-                                  showString "\\" .
-                                   showString v .
-                                   showString " -> ".
-                                  showsPrec 0 e 
+       showsPrec d (Lambda tv e) = showParen True $ 
+                                   showString "\\" .
+                                    showsPrec 0 tv .
+                                    showString " -> ".
+                                   showsPrec 0 e 
        showsPrec _ (Pair e1 e2) = showParen True $ 
                                   showsPrec 0 e1 .
                                   showString "," .
@@ -124,11 +148,11 @@ showIntercalate i [x] = x
 showIntercalate i (x:xs) = x . i . showIntercalate i xs
 
 instance Show TypedExpr where
-       showsPrec d (TypedExpr e t rightSide) = 
+       showsPrec d (TypedExpr e t) = 
                showParen (d>10) $
                        showsPrec 0 e .
                        showString " :: " .
-                       showString (arrowInstType rightSide t)
+                       showString (showTypePrec 0 t)
 
 instance Show BoolExpr where
        show (Equal e1 e2) = showsPrec 9 e1 $
@@ -141,9 +165,9 @@ instance Show BoolExpr where
                        "allZipWith " ++
                        "( " ++
                        "\\" ++
-                       v1 ++
+                       showsPrec 11 v1 "" ++
                        " " ++
-                       v2 ++
+                       showsPrec 11 v2 "" ++
                        " -> " ++
                        show be ++
                        ")" ++
@@ -151,32 +175,21 @@ instance Show BoolExpr where
                        showsPrec 11 e1 "" ++
                        " " ++
                        showsPrec 11 e2 ""
-       show (Condition tv1 tv2 be1 be2) = 
+       show (Condition tvars be1 be2) = 
                        "forall " ++
-                       showsPrec 0 tv1 "" ++
-                       ", " ++
-                       showsPrec 0 tv2 "" ++
+                       intercalate ", " (map show tvars) ++
                        ".\n" ++
                        (if be1 /= BETrue then indent 2 (show be1) ++ "==>\n" else "") ++
                        indent 2 (show be2)
-       show (UnpackPair v1 v2 e b t be) = 
+       show (UnpackPair v1 v2 e be) = 
                        "let (" ++
-                       v1 ++
+                       showsPrec 0 v1 "" ++
                        "," ++
-                       v2 ++
+                       showsPrec 0 v2 "" ++
                        ") = " ++
                        showsPrec 0 e "" ++
-                       " :: " ++
-                       arrowInstType b t ++
                        " in\n" ++
                        indent 2 (show be)
-       show (UnCond v1 b t be1) = 
-                       "forall " ++
-                       v1 ++
-                       " :: " ++
-                       arrowInstType b t ++
-                       ".\n" ++
-                       indent 2 (show be1)
        show (TypeVarInst i be) = 
                        "forall types t" ++
                        show (2*i-1) ++
@@ -193,17 +206,17 @@ instance Show BoolExpr where
 
 indent n = unlines . map (replicate n ' ' ++) . lines
 
-arrowInstType :: Bool -> Typ -> String
-arrowInstType b = ait 0
-  where 
-       ait _ Int                       = "Int" 
-       ait _ (TVar (TypVar i)) | not b = "t" ++  show (2*i-1)
-                                |     b = "t" ++  show (2*i)
-       ait d (Arrow t1 t2)             = paren (d>9) $ 
-                                                 ait 10 t1 ++ " -> " ++ ait 9 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 ++ ")"
+showTypePrec :: Int -> Typ -> String
+showTypePrec _ Int                         = "Int" 
+showTypePrec _ (TVar (TypVar i))            = "a"++show i
+showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
+                                   |     b = "t" ++  show (2*i)
+showTypePrec d (Arrow t1 t2)                = paren (d>9) $ 
+                                 showTypePrec 10 t1 ++ " -> " ++ showTypePrec 9 t2 
+showTypePrec d (List t)                    = "[" ++ showTypePrec 0 t ++ "]"
+showTypePrec d (TEither t1 t2)             = "Either " ++ showTypePrec 11 t1 ++ 
+                                                   " " ++ showTypePrec 11 t2
+showTypePrec d (TPair t1 t2)               = "(" ++ showTypePrec 0 t1 ++
+                                              "," ++ showTypePrec 0 t2 ++ ")"
 
 paren b p   =  if b then "(" ++ p ++ ")" else p
index f251a8a..624f0b8 100644 (file)
@@ -1,6 +1,8 @@
 {-# LANGUAGE FlexibleContexts, PatternSignatures, DeriveDataTypeable #-}
 module ParseType (
          parseType
+       , instType
+       , unquantify
        , TypVar(..)
        , Typ(..)
        ) where
@@ -19,7 +21,12 @@ import Data.Generics.Schemes
 import Data.Char
 import Data.Maybe
 
-newtype TypVar = TypVar Int deriving (Show, Eq, Typeable, Data)
+data TypVar = TypVar Int        -- alpha, beta etc.
+            | TypInst Int Bool  -- t1,t2 etc
+       deriving (Show, Eq, Typeable, Data)
+
+instType :: Bool -> Typ -> Typ
+instType rightSide typ = everywhere (mkT (\(TypVar i) -> TypInst i rightSide)) typ
 
 data Typ    = TVar    TypVar
             | Arrow   Typ     Typ
@@ -32,6 +39,10 @@ data Typ    = TVar    TypVar
             | TEither  Typ     Typ
             deriving (Show, Eq, Typeable, Data)
 
+unquantify (All     _ t) = unquantify t
+unquantify (AllStar _ t) = unquantify t
+unquantify t             = t
+
 parseType = either error id . parseType'
 
 -- | A simple type parser.
index 150a03d..5a3d81e 100644 (file)
@@ -8,18 +8,22 @@ import Control.Monad.Reader
 
 test = putStrLn . show . freeTheorem . parseType
 
-freeTheorem t = runReader (freeTheorem' (Var "f") (Var "f") t) freeVars
-
+freeTheorem t = flip runReader freeVars $ 
+                       freeTheorem' (typedLeft  (Var "f") (unquantify t))
+                                    (typedRight (Var "f") (unquantify t))
+                                     t
 freeVars = (map (:"") ['a'..])
 
 
-freeTheorem' :: Expr -> Expr -> Typ -> Reader [String] BoolExpr
+freeTheorem' :: TypedExpr -> TypedExpr -> Typ -> Reader [String] BoolExpr
 
 freeTheorem' e1 e2 Int = return $
-       Equal e1 e2
+       equal e1 e2
 
 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
-       Equal (App (Var ("g"++show i)) e1) e2
+       let tv = TypedExpr (Var ("g"++show i))
+                           (Arrow (TVar (TypInst i False)) (TVar (TypInst i True)))
+       in equal (app tv e1) e2
 
 freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
        -- Create patterns for (possily nested) tuples and only give
@@ -28,30 +32,27 @@ freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
                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 tve1 tve2 cond concl
+                       cond  <- freeTheorem' (tve1) (tve2) t1
+                       concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
+                       return $ Condition [tve1, tve2] cond concl
 
        -- No tuple on the left hand side:
-                                 | otherwise  = getVars 2 $ \[v1,v2] -> do
-       cond  <- freeTheorem' (Var v1) (Var v2) t1
-       -- See if the variables actually have definitions
-       case (defFor v1 cond, defFor v2 cond) of
+                                 | otherwise  = getSideVars t1 $ \(v1,v2) -> do
+       cond  <- freeTheorem'  v1  v2 t1
+       -- See if the variables (tv*) actually have equivalent terms (ev*)
+       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
+               concl <- freeTheorem' (app e1 ev1) (app e2  v2) t2
+               return $ unCond v2 concl
          (Nothing,Just ev2) -> do
-               concl <- freeTheorem' (App e1 (Var v1)) (App e2 ev2)      t2
-               return $ unCond v1 False t1 concl
+               concl <- freeTheorem' (app e1  v1) (app e2 ev2) t2
+               return $ unCond v1 concl
          _ -> do
-               concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
-               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
+               concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
+               return $ Condition [ v1, v2 ] cond concl
+
+freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
+       map <- freeTheorem' v1 v2 t
        return $ allZipWith v1 v2 map e1 e2
 
 {-
@@ -65,17 +66,31 @@ freeTheorem' e1 e2 (TPair t1 t2) = getVars 4 $ \[x1,x2,y1,y2] -> do
                        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 t@(TPair t1 t2) 
+       | (Pair   x1  x2) <- unTypeExpr e1
+       , (Pair   y1  y2) <- unTypeExpr e2
+          = do concl1 <- freeTheorem' 
+                       (TypedExpr x1 tx1)
+                       (TypedExpr y1 ty1)
+                       t1
+               concl2 <- freeTheorem'
+                       (TypedExpr x2 tx2)
+                       (TypedExpr y2 ty2)
+                       t2
+               return $ And concl1 concl2
+       | otherwise
+          = getVars 4 $ \[x1',x2',y1',y2'] -> do
+               let x1 = TypedExpr (Var x1') tx1
+                   x2 = TypedExpr (Var x2') tx2
+                   y1 = TypedExpr (Var y1') ty1
+                   y2 = TypedExpr (Var y2') ty2
+               concl1 <- freeTheorem' x1 y1 t1
+               concl2 <- freeTheorem' x2 y2 t2
+               return $ unpackPair x1 x2 e1 $
+                               unpackPair y1 y2 e2  $
+                                       And concl1 concl2
+ where (TPair tx1 tx2) = typeOf e1
+       (TPair ty1 ty2) = typeOf 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
@@ -83,12 +98,15 @@ 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 
 
+getSideVars :: (MonadReader [String] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
+getSideVars t a = getVars 2 $ \[v1,v2] -> a (typedLeft (Var v1) t, typedRight (Var v2) t)
+
 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)
+                       a (TypedExpr pair (instType rightSide t))
 fillTuplevars rightSide t a = getVars 1 $ \[s] ->
-                       a (TypedExpr (Var s) t rightSide)
+                       a (TypedExpr (Var s) (instType rightSide t))