Large refactor: Use TypedExpr data type
[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
9 test = putStrLn . show . freeTheorem . parseType
10
11 freeTheorem t = flip runReader freeVars $ 
12                         freeTheorem' (typedLeft  (Var "f") (unquantify t))
13                                      (typedRight (Var "f") (unquantify t))
14                                      t
15 freeVars = (map (:"") ['a'..])
16
17
18 freeTheorem' :: TypedExpr -> TypedExpr -> Typ -> Reader [String] BoolExpr
19
20 freeTheorem' e1 e2 Int = return $
21         equal e1 e2
22
23 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
24         let tv = TypedExpr (Var ("g"++show i))
25                            (Arrow (TVar (TypInst i False)) (TVar (TypInst i True)))
26         in equal (app tv e1) e2
27
28 freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
29         -- Create patterns for (possily nested) tuples and only give
30         -- the inner variables names
31         fillTuplevars False t1 $ \tve1 -> 
32                 fillTuplevars True t1 $ \tve2 ->  do
33                         let ve1 = unTypeExpr tve1
34                             ve2 = unTypeExpr tve2
35                         cond  <- freeTheorem' (tve1) (tve2) t1
36                         concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
37                         return $ Condition [tve1, tve2] cond concl
38
39         -- No tuple on the left hand side:
40                                  | otherwise  = getSideVars t1 $ \(v1,v2) -> do
41         cond  <- freeTheorem'  v1  v2 t1
42         -- See if the variables (tv*) actually have equivalent terms (ev*)
43         case (defFor  v1 cond, defFor  v2 cond) of
44           (Just ev1, _) -> do
45                 concl <- freeTheorem' (app e1 ev1) (app e2  v2) t2
46                 return $ unCond v2 concl
47           (Nothing,Just ev2) -> do
48                 concl <- freeTheorem' (app e1  v1) (app e2 ev2) t2
49                 return $ unCond v1 concl
50           _ -> do
51                 concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
52                 return $ Condition [ v1, v2 ] cond concl
53
54 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
55         map <- freeTheorem' v1 v2 t
56         return $ allZipWith v1 v2 map e1 e2
57
58 {-
59 freeTheorem' e1 e2 (TPair t1 t2) = getVars 4 $ \[x1,x2,y1,y2] -> do
60         concl1 <- freeTheorem' (Var x1) (Var y1) t1
61         concl2 <- freeTheorem' (Var x2) (Var y2) t2
62         return $ Condition x1 y1 t1 BETrue $
63                  Condition x2 y2 t2 (
64                         And (Equal e2 (Pair (Var y1) (Var y2)))
65                             (Equal e1 (Pair (Var x1) (Var x2)))) $
66                         And concl1 concl2
67 -}
68
69 freeTheorem' e1 e2 t@(TPair t1 t2) 
70         | (Pair   x1  x2) <- unTypeExpr e1
71         , (Pair   y1  y2) <- unTypeExpr e2
72            = do concl1 <- freeTheorem' 
73                         (TypedExpr x1 tx1)
74                         (TypedExpr y1 ty1)
75                         t1
76                 concl2 <- freeTheorem'
77                         (TypedExpr x2 tx2)
78                         (TypedExpr y2 ty2)
79                         t2
80                 return $ And concl1 concl2
81         | otherwise
82            = getVars 4 $ \[x1',x2',y1',y2'] -> do
83                 let x1 = TypedExpr (Var x1') tx1
84                     x2 = TypedExpr (Var x2') tx2
85                     y1 = TypedExpr (Var y1') ty1
86                     y2 = TypedExpr (Var y2') ty2
87                 concl1 <- freeTheorem' x1 y1 t1
88                 concl2 <- freeTheorem' x2 y2 t2
89                 return $ unpackPair x1 x2 e1 $
90                                 unpackPair y1 y2 e2  $
91                                         And concl1 concl2
92  where (TPair tx1 tx2) = typeOf e1
93        (TPair ty1 ty2) = typeOf e2
94
95 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
96 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
97
98 getVars :: (MonadReader [String] m) => Int -> ([String] -> m a) -> m a
99 getVars n a = asks (take n) >>= local (drop n) . a 
100
101 getSideVars :: (MonadReader [String] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
102 getSideVars t a = getVars 2 $ \[v1,v2] -> a (typedLeft (Var v1) t, typedRight (Var v2) t)
103
104 fillTuplevars :: (MonadReader [String] m) => Bool -> Typ -> (TypedExpr -> m a) -> m a
105 fillTuplevars rightSide t@(TPair t1 t2) a = do
106         fillTuplevars rightSide t1 $ \ve1 ->
107                 fillTuplevars rightSide t2 $ \ve2 ->
108                         let pair = Pair (unTypeExpr ve1) (unTypeExpr ve2) in
109                         a (TypedExpr pair (instType rightSide t))
110 fillTuplevars rightSide t a = getVars 1 $ \[s] ->
111                         a (TypedExpr (Var s) (instType rightSide t))
112