Initial check in
[darcs-mirror-polyfix.git] / SimpleFT.hs
1 {-# LANGUAGE PatternGuards  #-}
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 (List t) = do
22         [v1,v2] <- asks (take 2)
23         local (drop 2) $ do
24                 map <- freeTheorem' (Var v1) (Var v2) t
25                 case map of
26                   (Equal (Var v1') ev1) | v1' == v1 -> do
27                         return $ Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
28                   _ -> do
29                         return $ Pairwise v1 v2 map e1 e2
30
31 freeTheorem' e1 e2 (Arrow t1 t2) = do
32         [v1,v2] <- asks (take 2)
33         local (drop 2) $ do
34                 cond  <- freeTheorem' (Var v1) (Var v2) t1
35                 case cond of
36                   (Equal (Var v1') ev1) | v1' == v1 -> do
37                         concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
38                         return $ unCond v2 concl
39                   _ -> do
40                         concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
41                         return $ Condition v1 v2 cond concl
42
43 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
44         Equal e1 (App (Var ("g"++show i)) e2)
45
46 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
47 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t