1 {-# LANGUAGE PatternGuards #-}
7 import Control.Monad.Reader
9 test = putStrLn . show . freeTheorem . parseType
11 freeTheorem t = runReader (freeTheorem' (Var "f") (Var "f") t) freeVars
13 freeVars = (map (:"") ['a'..])
16 freeTheorem' :: Expr -> Expr -> Typ -> Reader [String] BoolExpr
18 freeTheorem' e1 e2 Int = return $
21 freeTheorem' e1 e2 (List t) = do
22 [v1,v2] <- asks (take 2)
24 map <- freeTheorem' (Var v1) (Var v2) t
26 (Equal (Var v1') ev1) | v1' == v1 -> do
27 return $ Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
29 return $ Pairwise v1 v2 map e1 e2
31 freeTheorem' e1 e2 (Arrow t1 t2) = do
32 [v1,v2] <- asks (take 2)
34 cond <- freeTheorem' (Var v1) (Var v2) t1
36 (Equal (Var v1') ev1) | v1' == v1 -> do
37 concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
38 return $ unCond v2 concl
40 concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
41 return $ Condition v1 v2 cond concl
43 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
44 Equal e1 (App (Var ("g"++show i)) e2)
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