1 {-# LANGUAGE PatternGuards, FlexibleContexts #-}
7 import Control.Monad.Reader
10 test :: String -> IO ()
11 test = putStrLn . show . freeTheorem . parseType
13 freeTheorem :: Typ -> BoolExpr
14 freeTheorem t = flip runReader freeVars $
15 freeTheorem' (typedLeft (Var F) (unquantify t))
16 (typedRight (Var F) (unquantify t))
22 freeTheorem' :: (MonadReader [Int] m) => TypedExpr -> TypedExpr -> Typ -> m BoolExpr
24 freeTheorem' e1 e2 Int = return $
27 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
28 let tv = TypedExpr (Var (FromTypVar i))
29 (Arrow (TVar (TypInst i False)) (TVar (TypInst i True)))
30 in equal (app tv e1) e2
32 freeTheorem' e1 e2 (Arrow t1 t2) = getSideVars t1 $ \(v1,v2) -> do
33 cond <- freeTheorem' v1 v2 t1
34 concl <- freeTheorem' (app e1 v1) (app e2 v2) t2
35 return $ condition [ v1, v2 ] cond concl
37 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
38 mapRel <- freeTheorem' v1 v2 t
39 return $ allZipWith v1 v2 mapRel e1 e2
41 freeTheorem' e1 e2 (TEither t1 t2) = do
44 return $ andEither rel1 rel2 e1 e2
46 freeTheorem' e1 e2 (TPair t1 t2)
47 | (Pair x1 x2) <- unTypeExpr e1
48 , (Pair y1 y2) <- unTypeExpr e2
49 = do concl1 <- freeTheorem'
53 concl2 <- freeTheorem'
57 return $ aand concl1 concl2
59 = getVars 2 $ \[v1,v2] -> do
60 let x1 = TypedExpr (Var (FromParam v1 False)) tx1
61 x2 = TypedExpr (Var (FromParam v2 False)) tx2
62 y1 = TypedExpr (Var (FromParam v1 True)) ty1
63 y2 = TypedExpr (Var (FromParam v2 True)) ty2
64 concl1 <- freeTheorem' x1 y1 t1
65 concl2 <- freeTheorem' x2 y2 t2
66 return $ unpackPair x1 x2 e1 $
69 where (TPair tx1 tx2) = typeOf e1
70 (TPair ty1 ty2) = typeOf e2
72 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst True i `liftM` freeTheorem' e1 e2 t
73 freeTheorem' e1 e2 (All (TypVar i) t) = TypeVarInst False i `liftM` freeTheorem' e1 e2 t
75 freeTheorem' _ _ t = error $ "Type " ++ show t ++ " passed to freeTheorem'"
77 genRel :: (MonadReader [Int] m) => Typ -> m LambdaBE
78 genRel t = getSideVars t $ \(v1,v2) -> do
79 mapRel <- freeTheorem' v1 v2 t
80 return $ lambdaBE v1 v2 mapRel
82 getVars :: (MonadReader [Int] m) => Int -> ([Int] -> m a) -> m a
83 getVars n a = asks (take n) >>= local (drop n) . a
85 getSideVars :: (MonadReader [Int] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
86 getSideVars t a = getVars 1 $ \[v] ->
87 a (typedLeft (Var (FromParam v False)) t,
88 typedRight (Var (FromParam v True)) t)