Catch empty lambda in map
[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                 return $ case map of
26                   (Equal (Var v1') ev1) | v1' == v1 -> 
27                         if ev1 == (Var v2)
28                         then Equal e1 e2
29                         else Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
30                   _ ->       Pairwise v1 v2 map e1 e2
31
32 freeTheorem' e1 e2 (Arrow t1 t2) = do
33         [v1,v2] <- asks (take 2)
34         local (drop 2) $ do
35                 cond  <- freeTheorem' (Var v1) (Var v2) t1
36                 case cond of
37                   (Equal (Var v1') ev1) | v1' == v1 -> do
38                         concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
39                         return $ unCond v2 concl
40                   _ -> do
41                         concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
42                         return $ Condition v1 v2 cond concl
43
44 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
45         Equal e1 (App (Var ("g"++show i)) e2)
46
47 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
48 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t