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