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