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