Remove special Tuple handling in allquantors
[darcs-mirror-polyfix.git] / SimpleFT.hs
1 {-# LANGUAGE PatternGuards, FlexibleContexts  #-}
2
3 module SimpleFT where
4
5 import ParseType
6 import Expr
7 import Control.Monad.Reader
8 import Data.List
9
10 test :: String -> IO ()
11 test = putStrLn . show . freeTheorem . parseType
12
13 freeTheorem :: Typ -> BoolExpr
14 freeTheorem t = flip runReader freeVars $ 
15                         freeTheorem' (typedLeft  (Var F) (unquantify t))
16                                      (typedRight (Var F) (unquantify t))
17                                      t
18 freeVars :: [Int]
19 freeVars = [1..]
20
21
22 freeTheorem' :: (MonadReader [Int] m) => TypedExpr -> TypedExpr -> Typ -> m BoolExpr
23
24 freeTheorem' e1 e2 Int = return $
25         equal e1 e2
26
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
31
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
36
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
40
41 freeTheorem' e1 e2 (TEither t1 t2) = do
42         rel1 <- genRel t1
43         rel2 <- genRel t2
44         return $ andEither rel1 rel2 e1 e2
45
46 freeTheorem' e1 e2 (TPair t1 t2) 
47         | (Pair   x1  x2) <- unTypeExpr e1
48         , (Pair   y1  y2) <- unTypeExpr e2
49            = do concl1 <- freeTheorem' 
50                         (TypedExpr x1 tx1)
51                         (TypedExpr y1 ty1)
52                         t1
53                 concl2 <- freeTheorem'
54                         (TypedExpr x2 tx2)
55                         (TypedExpr y2 ty2)
56                         t2
57                 return $ aand concl1 concl2
58         | otherwise
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 $
67                                 unpackPair y1 y2 e2  $
68                                         aand concl1 concl2
69  where (TPair tx1 tx2) = typeOf e1
70        (TPair ty1 ty2) = typeOf e2
71
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
74
75 freeTheorem' _ _ t = error $ "Type " ++ show t ++ " passed to freeTheorem'"
76
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
81
82 getVars :: (MonadReader [Int] m) => Int -> ([Int] -> m a) -> m a
83 getVars n a = asks (take n) >>= local (drop n) . a 
84
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)