Either handling
[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 :: [String]
19 freeVars = map (:"") (delete 'f' ['a'..])
20
21
22 freeTheorem' :: (MonadReader [String] 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 ("g"++show 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) | isTuple t1 = do
33         -- Create patterns for (possily nested) tuples and only give
34         -- the inner variables names
35         fillTuplevars False t1 $ \vars1 tve1  -> 
36                 fillTuplevars True t1 $ \vars2 tve2  ->  do
37                         cond  <- freeTheorem' (tve1) (tve2) t1
38                         concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
39                         return $ condition (vars1 ++ vars2) cond concl
40
41         -- No tuple on the left hand side:
42                                  | otherwise  = getSideVars t1 $ \(v1,v2) -> do
43         cond  <- freeTheorem'  v1  v2 t1
44         concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
45         return $ condition [ v1, v2 ] cond concl
46
47 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
48         mapRel <- freeTheorem' v1 v2 t
49         return $ allZipWith v1 v2 mapRel e1 e2
50
51 freeTheorem' e1 e2 (TEither t1 t2) = do
52         rel1 <- genRel t1
53         rel2 <- genRel t2
54         return $ andEither rel1 rel2 e1 e2
55
56 freeTheorem' e1 e2 (TPair t1 t2) 
57         | (Pair   x1  x2) <- unTypeExpr e1
58         , (Pair   y1  y2) <- unTypeExpr e2
59            = do concl1 <- freeTheorem' 
60                         (TypedExpr x1 tx1)
61                         (TypedExpr y1 ty1)
62                         t1
63                 concl2 <- freeTheorem'
64                         (TypedExpr x2 tx2)
65                         (TypedExpr y2 ty2)
66                         t2
67                 return $ aand concl1 concl2
68         | otherwise
69            = getVars 4 $ \[x1',x2',y1',y2'] -> do
70                 let x1 = TypedExpr (Var x1') tx1
71                     x2 = TypedExpr (Var x2') tx2
72                     y1 = TypedExpr (Var y1') ty1
73                     y2 = TypedExpr (Var y2') ty2
74                 concl1 <- freeTheorem' x1 y1 t1
75                 concl2 <- freeTheorem' x2 y2 t2
76                 return $ unpackPair x1 x2 e1 $
77                                 unpackPair y1 y2 e2  $
78                                         aand concl1 concl2
79  where (TPair tx1 tx2) = typeOf e1
80        (TPair ty1 ty2) = typeOf e2
81
82 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `liftM` freeTheorem' e1 e2 t
83 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `liftM` freeTheorem' e1 e2 t
84
85 freeTheorem' _ _ t = error $ "Type " ++ show t ++ " passed to freeTheorem'"
86
87 genRel :: (MonadReader [String] m) => Typ -> m LambdaBE
88 genRel t = getSideVars t $ \(v1,v2) -> do
89                 mapRel <- freeTheorem' v1 v2 t
90                 return $ lambdaBE v1 v2 mapRel
91
92 getVars :: (MonadReader [String] m) => Int -> ([String] -> m a) -> m a
93 getVars n a = asks (take n) >>= local (drop n) . a 
94
95 getSideVars :: (MonadReader [String] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
96 getSideVars t a = getVars 2 $ \[v1,v2] -> a (typedLeft (Var v1) t, typedRight (Var v2) t)
97
98 -- Given a (nested) tuple type, generates vars for each place
99 -- and returns them, once as list and onces as one (nested) tuple
100 fillTuplevars :: (MonadReader [String] m) =>
101                  Bool -> Typ -> ([TypedExpr] -> TypedExpr -> m a) -> m a
102 fillTuplevars rightSide t@(TPair t1 t2) a = do
103         fillTuplevars rightSide t1 $ \vars1 ve1  ->
104                 fillTuplevars rightSide t2 $ \vars2 ve2 ->
105                         let untypedPair  = Pair (unTypeExpr ve1) (unTypeExpr ve2)
106                             tpair = TypedExpr untypedPair (instType rightSide t)
107                         in a (vars1 ++ vars2) tpair
108 fillTuplevars rightSide t a = getVars 1 $ \[s] ->
109                         let tvar = TypedExpr (Var s) (instType rightSide t)
110                         in a [tvar] tvar