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 = putStrLn . show . freeTheorem . parseType
  11
  12 freeTheorem t = flip runReader freeVars $
  13                         freeTheorem' (typedLeft  (Var "f") (unquantify t))
  14                                      (typedRight (Var "f") (unquantify t))
  15                                      t
  16 freeVars = map (:"") (delete 'f' ['a'..])
  17
  18
  19 freeTheorem' :: TypedExpr -> TypedExpr -> Typ -> Reader [String] BoolExpr
  20
  21 freeTheorem' e1 e2 Int = return $
  22         equal e1 e2
  23
  24 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
  25         let tv = TypedExpr (Var ("g"++show i))
  26                            (Arrow (TVar (TypInst i False)) (TVar (TypInst i True)))
  27         in equal (app tv e1) e2
  28
  29 freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
  30         -- Create patterns for (possily nested) tuples and only give
  31         -- the inner variables names
  32         fillTuplevars False t1 $ \vars1 tve1  ->
  33                 fillTuplevars True t1 $ \vars2 tve2  ->  do
  34                         cond  <- freeTheorem' (tve1) (tve2) t1
  35                         concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
  36                         return $ condition (vars1 ++ vars2) cond concl
  37
  38         -- No tuple on the left hand side:
  39                                  | otherwise  = getSideVars t1 $ \(v1,v2) -> do
  40         cond  <- freeTheorem'  v1  v2 t1
  41         concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
  42         return $ condition [ v1, v2 ] cond concl
  43
  44 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
  45         map <- freeTheorem' v1 v2 t
  46         return $ allZipWith v1 v2 map e1 e2
  47
  48 {-
  49 freeTheorem' e1 e2 (TPair t1 t2) = getVars 4 $ \[x1,x2,y1,y2] -> do
  50         concl1 <- freeTheorem' (Var x1) (Var y1) t1
  51         concl2 <- freeTheorem' (Var x2) (Var y2) t2
  52         return $ Condition x1 y1 t1 BETrue $
  53                  Condition x2 y2 t2 (
  54                         And (Equal e2 (Pair (Var y1) (Var y2)))
  55                             (Equal e1 (Pair (Var x1) (Var x2)))) $
  56                         And concl1 concl2
  57 -}
  58
  59 freeTheorem' e1 e2 t@(TPair t1 t2)
  60         | (Pair   x1  x2) <- unTypeExpr e1
  61         , (Pair   y1  y2) <- unTypeExpr e2
  62            = do concl1 <- freeTheorem'
  63                         (TypedExpr x1 tx1)
  64                         (TypedExpr y1 ty1)
  65                         t1
  66                 concl2 <- freeTheorem'
  67                         (TypedExpr x2 tx2)
  68                         (TypedExpr y2 ty2)
  69                         t2
  70                 return $ aand concl1 concl2
  71         | otherwise
  72            = getVars 4 $ \[x1',x2',y1',y2'] -> do
  73                 let x1 = TypedExpr (Var x1') tx1
  74                     x2 = TypedExpr (Var x2') tx2
  75                     y1 = TypedExpr (Var y1') ty1
  76                     y2 = TypedExpr (Var y2') ty2
  77                 concl1 <- freeTheorem' x1 y1 t1
  78                 concl2 <- freeTheorem' x2 y2 t2
  79                 return $ unpackPair x1 x2 e1 $
  80                                 unpackPair y1 y2 e2  $
  81                                         aand concl1 concl2
  82  where (TPair tx1 tx2) = typeOf e1
  83        (TPair ty1 ty2) = typeOf e2
  84
  85 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
  86 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
  87
  88 getVars :: (MonadReader [String] m) => Int -> ([String] -> m a) -> m a
  89 getVars n a = asks (take n) >>= local (drop n) . a
  90
  91 getSideVars :: (MonadReader [String] m) => Typ -> ((TypedExpr,TypedExpr) -> m a) -> m a
  92 getSideVars t a = getVars 2 $ \[v1,v2] -> a (typedLeft (Var v1) t, typedRight (Var v2) t)
  93
  94 -- Given a (nested) tuple type, generates vars for each place
  95 -- and returns them, once as list and onces as one (nested) tuple
  96 fillTuplevars :: (MonadReader [String] m) =>
  97                  Bool -> Typ -> ([TypedExpr] -> TypedExpr -> m a) -> m a
  98 fillTuplevars rightSide t@(TPair t1 t2) a = do
  99         fillTuplevars rightSide t1 $ \vars1 ve1  ->
 100                 fillTuplevars rightSide t2 $ \vars2 ve2 ->
 101                         let pair  = Pair (unTypeExpr ve1) (unTypeExpr ve2)
 102                             tpair = TypedExpr pair (instType rightSide t)
 103                         in a (vars1 ++ vars2) tpair
 104 fillTuplevars rightSide t a = getVars 1 $ \[s] ->
 105                         let tvar = TypedExpr (Var s) (instType rightSide t)
 106                         in a [tvar] tvar