SimpleFT.hs

   1 {-# LANGUAGE PatternGuards, FlexibleContexts  #-}
   2
   3 module SimpleFT where
   4
   5 import ParseType
   6 import Expr
   7 import Control.Monad.Reader
   8 import Data.List
   9
  10 test :: String -> IO ()
  11 test = putStrLn . show . freeTheorem . parseType
  12
  13 freeTheorem :: Typ -> BoolExpr
  14 freeTheorem t = flip runReader freeVars $
  15                         freeTheorem' (typedLeft  (Var F) (unquantify t))
  16                                      (typedRight (Var F) (unquantify t))
  17                                      t
  18 freeVars :: [Int]
  19 freeVars = [1..]
  20
  21
  22 freeTheorem' :: (MonadReader [Int] m) => TypedExpr -> TypedExpr -> Typ -> m BoolExpr
  23
  24 freeTheorem' e1 e2 Int = return $
  25         equal e1 e2
  26
  27 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
  28         let tv = TypedExpr (Var (FromTypVar i))
  29                            (Arrow (TVar (TypInst i False)) (TVar (TypInst i True)))
  30         in equal (app tv e1) e2
  31
  32 freeTheorem' e1 e2 (Arrow t1 t2) = getSideVars t1 $ \(v1,v2) -> do
  33         cond  <- freeTheorem'  v1  v2 t1
  34         concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
  35         return $ condition [ v1, v2 ] cond concl
  36
  37 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
  38         mapRel <- freeTheorem' v1 v2 t
  39         return $ allZipWith v1 v2 mapRel e1 e2
  40
  41 freeTheorem' e1 e2 (TEither t1 t2) = do
  42         rel1 <- genRel t1
  43         rel2 <- genRel t2
  44         return $ andEither rel1 rel2 e1 e2
  45
  46 freeTheorem' e1 e2 (TPair t1 t2)
  47         | (Pair   x1  x2) <- unTypeExpr e1
  48         , (Pair   y1  y2) <- unTypeExpr e2
  49            = do concl1 <- freeTheorem'
  50                         (TypedExpr x1 tx1)
  51                         (TypedExpr y1 ty1)
  52                         t1
  53                 concl2 <- freeTheorem'
  54                         (TypedExpr x2 tx2)
  55                         (TypedExpr y2 ty2)
  56                         t2
  57                 return $ aand concl1 concl2
  58         | otherwise
  59            = getVars 2 $ \[v1,v2] -> do
  60                 let x1 = TypedExpr (Var (FromParam v1 False)) tx1
  61                     x2 = TypedExpr (Var (FromParam v2 False)) tx2
  62                     y1 = TypedExpr (Var (FromParam v1 True)) ty1
  63                     y2 = TypedExpr (Var (FromParam v2 True)) ty2
  64                 concl1 <- freeTheorem' x1 y1 t1
  65                 concl2 <- freeTheorem' x2 y2 t2
  66                 return $ unpackPair x1 x2 e1 $
  67                                 unpackPair y1 y2 e2  $
  68                                         aand concl1 concl2
  69  where (TPair tx1 tx2) = typeOf e1
  70        (TPair ty1 ty2) = typeOf e2
  71
  72 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst True i `liftM` freeTheorem' e1 e2 t
  73 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst False i `liftM` freeTheorem' e1 e2 t
  74
  75 freeTheorem' _ _ t = error $ "Type " ++ show t ++ " passed to freeTheorem'"
  76
  77 genRel :: (MonadReader [Int] m) => Typ -> m LambdaBE
  78 genRel t = getSideVars t $ \(v1,v2) -> do
  79                 mapRel <- freeTheorem' v1 v2 t
  80                 return $ lambdaBE v1 v2 mapRel
  81
  82 getVars :: (MonadReader [Int] m) => Int -> ([Int] -> m a) -> m a
  83 getVars n a = asks (take n) >>= local (drop n) . a
  84
  85 getSideVars :: (MonadReader [Int] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
  86 getSideVars t a = getVars 1 $ \[v] ->
  87                 a (typedLeft  (Var (FromParam v False)) t,
  88                    typedRight (Var (FromParam v True))  t)