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
| 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
= 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
conc x (Conc ys) = Conc ([x] ++ ys)
conc x y = Conc ([x,y])
+
+-- Specialization of g'
+
+
-- Helpers
isApplOn :: Expr -> Expr -> Maybe Expr
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'))
-- 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"
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) ++
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
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 $
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)