Name vars corresponding to daniels output, identify strict functions

diff --git a/Expr.hs b/Expr.hs
index 1a32d3d..6af565f 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -19,8 +19,14 @@ typedLeft, typedRight :: Expr -> Typ -> TypedExpr
 typedLeft  e t = TypedExpr e (instType False t)
 typedRight e t = TypedExpr e (instType True t)
 
+data EVar = F
+         | FromTypVar Int
+          | FromParam Int Bool
+            deriving (Eq, Typeable, Data)
+
 data Expr
-       = Var String
+       = Var EVar
+       | TheOneFunc
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
        | Lambda TypedExpr Expr
@@ -40,7 +46,7 @@ data BoolExpr
        | AndEither  LambdaBE LambdaBE Expr Expr
        | Condition [TypedExpr] BoolExpr BoolExpr
        | UnpackPair TypedExpr TypedExpr TypedExpr BoolExpr
-       | TypeVarInst Int BoolExpr
+       | TypeVarInst Bool Int BoolExpr
             deriving (Eq, Typeable, Data)
 
 -- Smart constructors
@@ -194,7 +200,7 @@ replaceTermBE d r = go
                           = condition vs (go cond) (go concl)
        go (UnpackPair v1 v2 e be)
                           = unpackPair v1 v2 (go' e) (go be)
-       go (TypeVarInst _ _) = error "TypeVarInst not expected here"
+       go (TypeVarInst _ _ _) = error "TypeVarInst not expected here"
 
        go' :: Data a => a -> a
        go' = replaceExpr d r
@@ -263,6 +269,10 @@ conc (Conc xs)  y        = Conc (xs  ++ [y])
 conc x         (Conc ys) = Conc ([x] ++ ys)
 conc x          y        = Conc ([x,y])
 
+
+-- Specialization of g'
+
+
 -- Helpers
 
 isApplOn :: Expr -> Expr -> Maybe Expr
@@ -271,14 +281,6 @@ 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 :: String -> Expr -> Bool
-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 (Pair e1 e2) = hasVar v e1 || hasVar v e2
-hasVar _ Map          = False
-
 occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
 e `occursIn` e'       = not (null (listify (==e) e'))
 
@@ -296,8 +298,14 @@ isTuple _           = False
 --  7 ==>
 --  6 forall
 
+instance Show EVar where
+       show F               = "f"
+       show (FromTypVar i)  = "g" ++ show i
+       show (FromParam i b) = "x" ++ show i ++ if b then "'" else ""
+
+
 instance Show Expr where
-       showsPrec _ (Var s)     = showString s
+       showsPrec _ (Var v)     = showsPrec 11 v
        showsPrec d (App e1 e2) = showParen (d>10) $
                showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
        showsPrec _ (Conc [])   = showString "id"
@@ -378,12 +386,14 @@ instance Show BoolExpr where
                        showsPrec 0 e "" ++
                        " in\n" ++
                        indent 2 (show be)
-       show (TypeVarInst i be) = 
+       show (TypeVarInst strict i be) = 
                        "forall types t" ++
                        show (2*i-1) ++
                        ", t" ++
                        show (2*i) ++
-                       ", function g" ++
+                       ", " ++
+                       (if strict then "strict " else "") ++
+                        "functions g" ++
                        show i ++
                        " :: t" ++
                        show (2*i-1) ++

diff --git a/SimpleFT.hs b/SimpleFT.hs
index 6f7ef5b..fbea0cf 100644 (file)
--- a/SimpleFT.hs
+++ b/SimpleFT.hs
@@ -12,31 +12,32 @@ test = putStrLn . show . freeTheorem . parseType
 
 freeTheorem :: Typ -> BoolExpr
 freeTheorem t = flip runReader freeVars $ 
-                       freeTheorem' (typedLeft  (Var "f") (unquantify t))
-                                    (typedRight (Var "f") (unquantify t))
+                       freeTheorem' (typedLeft  (Var F) (unquantify t))
+                                    (typedRight (Var F) (unquantify t))
                                      t
-freeVars :: [String]
-freeVars = map (:"") (delete 'f' ['a'..])
+freeVars :: [Int]
+freeVars = [1..]
 
 
-freeTheorem' :: (MonadReader [String] m) => TypedExpr -> TypedExpr -> Typ -> m BoolExpr
+freeTheorem' :: (MonadReader [Int] m) => TypedExpr -> TypedExpr -> Typ -> m BoolExpr
 
 freeTheorem' e1 e2 Int = return $
        equal e1 e2
 
 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
-       let tv = TypedExpr (Var ("g"++show i))
+       let tv = TypedExpr (Var (FromTypVar 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
        -- the inner variables names
-       fillTuplevars False t1 $ \vars1 tve1  -> 
-               fillTuplevars True t1 $ \vars2 tve2  ->  do
-                       cond  <- freeTheorem' (tve1) (tve2) t1
-                       concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
-                       return $ condition (vars1 ++ vars2) cond concl
+       fillTuplevars t1 $ \ vars (tve1, tve2) -> do
+--     fillTuplevars False t1 $ \vars1 tve1  -> 
+--             fillTuplevars True t1 $ \vars2 tve2  ->  do
+               cond  <- freeTheorem' (tve1) (tve2) t1
+               concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
+               return $ condition vars cond concl
 
        -- No tuple on the left hand side:
                                  | otherwise  = getSideVars t1 $ \(v1,v2) -> do
@@ -66,11 +67,11 @@ freeTheorem' e1 e2 (TPair t1 t2)
                        t2
                return $ aand 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
+          = getVars 2 $ \[v1,v2] -> do
+               let x1 = TypedExpr (Var (FromParam v1 False)) tx1
+                   x2 = TypedExpr (Var (FromParam v2 False)) tx2
+                   y1 = TypedExpr (Var (FromParam v1 True)) ty1
+                   y2 = TypedExpr (Var (FromParam v2 True)) ty2
                concl1 <- freeTheorem' x1 y1 t1
                concl2 <- freeTheorem' x2 y2 t2
                return $ unpackPair x1 x2 e1 $
@@ -79,32 +80,32 @@ freeTheorem' e1 e2 (TPair t1 t2)
  where (TPair tx1 tx2) = typeOf e1
        (TPair ty1 ty2) = typeOf e2
 
-freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `liftM` freeTheorem' e1 e2 t
-freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `liftM` freeTheorem' e1 e2 t
+freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst True i `liftM` freeTheorem' e1 e2 t
+freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst False i `liftM` freeTheorem' e1 e2 t
 
 freeTheorem' _ _ t = error $ "Type " ++ show t ++ " passed to freeTheorem'"
 
-genRel :: (MonadReader [String] m) => Typ -> m LambdaBE
+genRel :: (MonadReader [Int] m) => Typ -> m LambdaBE
 genRel t = getSideVars t $ \(v1,v2) -> do
                mapRel <- freeTheorem' v1 v2 t
                return $ lambdaBE v1 v2 mapRel
 
-getVars :: (MonadReader [String] m) => Int -> ([String] -> m a) -> m a
+getVars :: (MonadReader [Int] m) => Int -> ([Int] -> 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)
+getSideVars :: (MonadReader [Int] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
+getSideVars t a = getVars 1 $ \[v] ->
+               a (typedLeft  (Var (FromParam v False)) t,
+                   typedRight (Var (FromParam v True))  t)
 
 -- Given a (nested) tuple type, generates vars for each place
 -- and returns them, once as list and onces as one (nested) tuple
-fillTuplevars :: (MonadReader [String] m) =>
-                 Bool -> Typ -> ([TypedExpr] -> TypedExpr -> m a) -> m a
-fillTuplevars rightSide t@(TPair t1 t2) a = do
-       fillTuplevars rightSide t1 $ \vars1 ve1  ->
-               fillTuplevars rightSide t2 $ \vars2 ve2 ->
-                       let untypedPair  = Pair (unTypeExpr ve1) (unTypeExpr ve2)
-                           tpair = TypedExpr untypedPair (instType rightSide t)
-                       in a (vars1 ++ vars2) tpair
-fillTuplevars rightSide t a = getVars 1 $ \[s] ->
-                       let tvar = TypedExpr (Var s) (instType rightSide t)
-                       in a [tvar] tvar
+fillTuplevars :: (MonadReader [Int] m) =>
+                 Typ -> ([TypedExpr] -> (TypedExpr,TypedExpr) -> m a) -> m a
+fillTuplevars t@(TPair t1 t2) a = do
+       fillTuplevars t1 $ \vars1 (l1,l2)  ->
+               fillTuplevars t2 $ \vars2 (r1,r2) ->
+                       a (vars1 ++ vars2) (pair l1 r1, pair l2 r2)
+
+fillTuplevars t a = getSideVars t $ \(v1,v2) ->
+                       a [v1,v2] (v1,v2)