Add tests for System F

SystemF/Comble.hs

@@ -48,36 +48,11 @@ toList c = go c [] where
   go (App (Pure fun) arg _) acc = (fun <$> (toList arg)) ++ acc
   go (App fun arg _)        acc = ((toList fun) <*> (toList arg)) ++ acc
 
-data Tree elem = Leaf | Node (Tree elem) elem (Tree elem) deriving Show
+splitn :: (Integral a) => Integer -> a -> [[a]]
+splitn 0 _ = [[0]] -- This function is used to distribute sizes over branches, returning 0 here means only size-0, eg 'empty' can be generated.
+splitn 1 x = [[x]]
+splitn n x = concatMap (\y -> map (y:) $ splitn (n-1) (x-y)) [1..(x-1)]
 
-treesOfSize :: (Alternative effect) => Integer -> effect (Tree ())
-treesOfSize n = memoGo n where
-  table    = tabulate go (0,n)
-  memoGo m = table A.! m where
-  go 0
-    = pure Leaf
-  go (s+1)
-    = asum [ pure Node <*> memoGo s1 <*> pure () <*> memoGo s2
-           | (s1, s2) <- split2 s]
-
-split2 :: (Integral int) => int -> [(int, int)]
-split2 n = [(a, n - a) | a <- [0 .. n]]
-
-asum :: (Alternative effect) => [effect val] -> effect val
+asum :: [Comble val] -> Comble val
 asum = foldr (<|>) empty
 
-tabulate :: (A.Ix i) =>  (i -> e) -> (i,i) -> A.Array i e
-tabulate f (l,u) =
-  A.listArray (l,u) (map f (A.range (l,u)))
-
-data LC = Var Integer | Lam LC | Apply LC LC deriving Show
-
-termsOfSize :: Alternative effect => Integer -> effect LC
-termsOfSize n = memoGo (n,0) where
-  table       = tabulate go ((0,0),(n,n))
-  memoGo p    = table A.! p
-  go (0,m)   = asum [pure (Var v) | v <- [0..m-1]]
-  go (s+1,m) =
-       asum [pure (Var v) | v <- [0..m-1]]
-   <|> (Lam <$> go (s,m+1))
-   <|> asum [ pure Apply <*> memoGo (s1,m) <*> memoGo (s2, m) | (s1, s2) <- split2 s]

SystemF/SystemFImpl.hs

 module SystemFImpl (
+    Env(Nil, ETermVar, ETypeVar),
     isVal,
     getTypeFromEnv,
     stepEval,
@@ -6,14 +7,24 @@ module SystemFImpl (
     typeOf
 ) where
 
-import HaskellOutput
+import SystemFSorts
+
+countTyped :: Either a b -> (Integer, Integer)
+countTyped (Left l)  = (1, 0)
+countTyped (Right r) = (0, 1)
+
+sumTuples (xl, xr) (yl, yr) = (xl + yl, xr + yr)
+
+data Env = ETermVar Type Env
+         | ETypeVar Env
+         | Nil
 
 isVal :: Term -> Bool
 isVal (TmAbs x t)              = True
 isVal (TmTAbs t1)              = True
 isVal _ = False
 
-getTypeFromEnv :: Env -> HNat -> Either String Type
+getTypeFromEnv :: Env -> Variable -> Either String Type
 getTypeFromEnv (ETermVar ty _) Z = return ty
 getTypeFromEnv _ Z = Left "wrong or no binding for term"
 getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
@@ -28,13 +39,13 @@ stepEval (TmApp (TmAbs t ty) t2)
     Just
       (termshiftminus
          (STermVar Z)
-         (termtermSubstitute (termshiftplus (STermVar Z) t2) Z t))
+         (termTermSubstitute (termshiftplus (STermVar Z) t2) Z t))
 --type application
 stepEval (TmTApp (TmTAbs t) ty) =
   Just
     (termshiftminus
        (STypeVar Z)
-       (termtypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
+       (termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
 --R-CTXT
 stepEval (TmApp t1 t2)
   | isVal t1 = do
@@ -78,10 +89,10 @@ typeOf (TmTApp t ty) ctx =
       return
         (typeshiftminus
            (STypeVar Z)
-           (typetypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
+           (typeTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
     Left a -> Left a
     _ -> Left "not a type abstraction"
 typeOf (TmTAbs t) ctx = do
   ty <- typeOf t (ETypeVar ctx)
   return (TyAll ty)
-typeOf (TmNum _) ctx = Right TyBase
+

SystemF/SystemFSorts.hs

+module SystemFSorts where
+import Data.List 
+import Control.Applicative 
+import Comble 
+import Test.QuickCheck 
+
+data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
+
+data Term = TmVar Variable | TmAbs Term Type | TmApp Term Term | TmTApp Term Type | TmTAbs Term deriving(Show, Eq)
+
+data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyBase deriving(Show, Eq)
+
+
+plus (Z) h = h
+plus h (Z) = h
+plus x1 (STermVar x2) = (STermVar (plus x1 x2))
+plus x1 (STypeVar x2) = (STypeVar (plus x1 x2))
+
+minus (Z) (Z) = (Z)
+minus (Z) _ = (error "You cannot substract zero with a positive number")
+minus result (Z) = result
+minus (STermVar h1) (STermVar h2) = (minus h1 h2)
+minus (STermVar h1) (STypeVar h2) = (error "differing namespace found in minus")
+minus (STypeVar h1) (STermVar h2) = (error "differing namespace found in minus")
+minus (STypeVar h1) (STypeVar h2) = (minus h1 h2)
+
+generateHnatTermVar 0 c = c
+generateHnatTermVar n c = (STermVar (generateHnatTermVar (n - 1) c))
+
+generateHnatTypeVar 0 c = c
+generateHnatTypeVar n c = (STypeVar (generateHnatTypeVar (n - 1) c))
+
+termshiftHelpplus d c (TmVar var) = if (var >= c) then (TmVar (plus var d)) else (TmVar var)
+
+typeshiftHelpplus d c (TyVar var) = if (var >= c) then (TyVar (plus var d)) else (TyVar var)
+
+termshiftplus d t = (termmap (termshiftHelpplus d) (typeshiftHelpplus d) (Z) t)
+
+typeshiftplus d t = (typemap (typeshiftHelpplus d) (Z) t)
+
+termshiftHelpminus d c (TmVar var) = if (var >= c) then (TmVar (minus var d)) else (TmVar var)
+
+typeshiftHelpminus d c (TyVar var) = if (var >= c) then (TyVar (minus var d)) else (TyVar var)
+
+termshiftminus d t = (termmap (termshiftHelpminus d) (typeshiftHelpminus d) (Z) t)
+
+typeshiftminus d t = (typemap (typeshiftHelpminus d) (Z) t)
+
+termmap onTermVar onTypeVar c (TmVar var) = (onTermVar c (TmVar var))
+termmap onTermVar onTypeVar c (TmAbs x t) = (TmAbs (termmap onTermVar onTypeVar (STermVar c) x) (typemap onTypeVar c t))
+termmap onTermVar onTypeVar c (TmApp t1 t2) = (TmApp (termmap onTermVar onTypeVar c t1) (termmap onTermVar onTypeVar c t2))
+termmap onTermVar onTypeVar c (TmTApp t1 t) = (TmTApp (termmap onTermVar onTypeVar c t1) (typemap onTypeVar c t))
+termmap onTermVar onTypeVar c (TmTAbs t1) = (TmTAbs (termmap onTermVar onTypeVar (STypeVar c) t1))
+
+typemap onTypeVar c (TyVar var) = (onTypeVar c (TyVar var))
+typemap onTypeVar c (TyArr t1 t2) = (TyArr (typemap onTypeVar c t1) (typemap onTypeVar c t2))
+typemap onTypeVar c (TyAll t1) = (TyAll (typemap onTypeVar (STypeVar c) t1))
+typemap onTypeVar c (TyBase) = (TyBase)
+
+termSubstituteHelp sub c (TmVar var) = if (var == c) then (termshiftplus c sub) else (TmVar var)
+
+termTermSubstitute sub orig t = (termmap (termSubstituteHelp sub) (\c x -> x) orig t)
+
+termTypeSubstitute sub orig t = (termmap (\c x -> x) (typeSubstituteHelp sub) orig t)
+
+typeSubstituteHelp sub c (TyVar var) = if (var == c) then (typeshiftplus c sub) else (TyVar var)
+
+typeTypeSubstitute sub orig t = (typemap (typeSubstituteHelp sub) orig t)
+
+freeVariablesTerm c (TmVar var) = if (var >= c) then [(minus var c)] else []
+freeVariablesTerm c (TmAbs x t) = (nub (concat [(freeVariablesTerm (STermVar c) x),(freeVariablesType c t)]))
+freeVariablesTerm c (TmApp t1 t2) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesTerm c t2)]))
+freeVariablesTerm c (TmTApp t1 t) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesType c t)]))
+freeVariablesTerm c (TmTAbs t1) = (nub (concat [(freeVariablesTerm (STypeVar c) t1)]))
+
+freeVariablesType c (TyVar var) = if (var >= c) then [(minus var c)] else []
+freeVariablesType c (TyArr t1 t2) = (nub (concat [(freeVariablesType c t1),(freeVariablesType c t2)]))
+freeVariablesType c (TyAll t1) = (nub (concat [(freeVariablesType (STypeVar c) t1)]))
+freeVariablesType c (TyBase) = (nub (concat [[]]))
+
+termOfSize env 0 nType = (empty)
+termOfSize env 1 nType = (TmVar <$> (getTermVar env (Z)))
+termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType) <*> (typeOfSize (typeEnv env) nType))
+                              <|> (asum (map (\l -> (TmApp <$> (termOfSize (termEnv env) ((!!) l 0) nType) <*> (termOfSize (termEnv env) ((!!) l 1) nType))) (splitn 2 (nTerm - 1))))
+                              <|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType) <*> (typeOfSize (typeEnv env) nType))
+                              <|> (TmTAbs <$> (termOfSize (termEnv (STypeVar env)) (nTerm - 1) nType)))
+
+termUpToSize env 0 nType = (empty)
+termUpToSize env nTerm nType = ((termUpToSize env (nTerm - 1) nType)
+                                <|> (termOfSize env nTerm nType))
+
+termEnv (STermVar next) = (STermVar (termEnv next))
+termEnv (STypeVar next) = (STypeVar (termEnv next))
+termEnv (Z) = (Z)
+
+forTermWithSize env nTerm nType prop = (let c = (termOfSize env nTerm nType)
+                                            n = (card c)
+                                            g = ((!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
+                                        in (forAll g prop))
+
+typeOfSize env 0 = (empty)
+typeOfSize env 1 = ((TyVar <$> (getTypeVar env (Z)))
+                    <|> (pure TyBase))
+typeOfSize env nType = ((asum (map (\l -> (TyArr <$> (typeOfSize (typeEnv env) ((!!) l 0)) <*> (typeOfSize (typeEnv env) ((!!) l 1)))) (splitn 2 (nType - 1))))
+                        <|> (TyAll <$> (typeOfSize (typeEnv (STypeVar env)) (nType - 1))))
+
+typeUpToSize env 0 = (empty)
+typeUpToSize env nType = ((typeUpToSize env (nType - 1))
+                          <|> (typeOfSize env nType))
+
+typeEnv (STypeVar next) = (STypeVar (typeEnv next))
+typeEnv (STermVar next) = (typeEnv next)
+typeEnv (Z) = (Z)
+
+forTypeWithSize env nType prop = (let c = (typeOfSize env nType)
+                                      n = (card c)
+                                      g = ((!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
+                                  in (forAll g prop))
+
+genInt = (asum [(pure 0),(pure 1),(pure 2),(pure 3)])
+
+genString = (asum [(pure "a"),(pure "b"),(pure "c"),(pure "d")])
+
+reverseVar (Z) res = res
+reverseVar (STermVar next) res = (reverseVar next (STermVar res))
+reverseVar (STypeVar next) res = (reverseVar next (STypeVar res))
+
+getTermVar (Z) _ = (empty)
+getTermVar (STermVar next) abs = ((pure (reverseVar abs (Z)))
+                                  <|> (getTermVar next (STermVar abs)))
+getTermVar (STypeVar next) abs = (getTermVar next (STypeVar abs))
+
+getTypeVar (Z) _ = (empty)
+getTypeVar (STypeVar next) abs = ((pure (reverseVar abs (Z)))
+                                  <|> (getTypeVar next (STypeVar abs)))
+getTypeVar (STermVar next) abs = (getTypeVar next (STermVar abs))
+instance Ord Variable where
+  compare (Z) (Z) = (EQ)
+  compare (Z) _ = (LT)
+  compare _ (Z) = (GT)
+  compare (STermVar h1) (STermVar h2) = (compare h1 h2)
+  compare (STermVar h1) (STypeVar h2) = (error "differing namespace found in compare")
+  compare (STypeVar h1) (STermVar h2) = (error "differing namespace found in compare")
+  compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)

SystemF/Test.hs

+import Test.QuickCheck
+import Data.Either
+import Data.Maybe
+
+import SystemFSorts
+import SystemFImpl
+import Comble
+
+args = Args{replay=Nothing, maxSuccess=1000, maxDiscardRatio=10000, maxSize=100, chatty=True, maxShrinks=100}
+
+-- The type of a term does not change when a reduction step is performed
+preservation :: Term -> Property
+preservation te = (isRight ty) && (not $ isVal te)
+              ==> (fromRight undefined ty) == (fromRight undefined tyStep)
+  where ty = typeOf te Nil
+        tyStep = (flip typeOf) Nil $ fromMaybe undefined $ stepEval te
+
+-- If a term is well-typed, it is either a 'value', or it is possible to performa reduction.
+progress :: Term -> Property
+progress te = isRight (typeOf te Nil)
+          ==> (isVal te) || (isJust (stepEval te))
+

SystemF/haskellOutput.hs

-module HaskellOutput
-  ( Env(..)
-  , HNat(..)
-  , Type(..)
-  , typetypeSubstitute
-  , freeVariablesType
-  , typeshiftplus
-  , typeshiftminus
-  , Term(..)
-  , termtermSubstitute
-  , termtypeSubstitute
-  , freeVariablesTerm
-  , termshiftplus
-  , termshiftminus
-  , generateHnatTypeVar
-  , generateHnatTermVar
-  ) where
-
-import           Data.List
-
-data Type
-  = TyVar HNat
-  | TyArr Type
-          Type
-  | TyAll Type
-  | TyBase
-  deriving (Show, Eq)
-
-data Term
-  = TmVar HNat
-  | TmAbs Term
-          Type
-  | TmApp Term
-          Term
-  | TmTApp Term
-           Type
-  | TmTAbs Term
-  | TmNum Int
-  deriving (Show, Eq)
-
-data HNat
-  = Z
-  | STypeVar HNat
-  | STermVar HNat
-  deriving (Show, Eq)
-
-plus x1 (STypeVar x2) = STypeVar (plus x1 x2)
-plus x1 (STermVar x2) = STermVar (plus x1 x2)
-plus Z h              = h
-plus h Z              = h
-
-instance Ord HNat where
-  compare (STypeVar h1) (STypeVar h2) = compare h1 h2
-  compare (STypeVar h1) (STermVar h2) =
-    error "differing namespace found in compare "
-  compare (STermVar h1) (STypeVar h2) =
-    error "differing namespace found in compare "
-  compare (STermVar h1) (STermVar h2) = compare h1 h2
-  compare Z Z = EQ
-  compare Z _ = LT
-  compare _ Z = GT
-
-minus (STypeVar h1) (STypeVar h2) = minus h1 h2
-minus (STypeVar h1) (STermVar h2) = error "differing namespace found in minus "
-minus (STermVar h1) (STypeVar h2) = error "differing namespace found in minus "
-minus (STermVar h1) (STermVar h2) = minus h1 h2
-minus Z Z = Z
-minus Z _ = error " You cannot substract zero with a positive number "
-minus result Z = result
-
-data Env
-  = Nil
-  | ETypeVar Env
-  | ETermVar Type
-             Env
-  deriving (Show, Eq)
-
-generateHnatTypeVar 0 c = c
-generateHnatTypeVar n c = STypeVar (generateHnatTypeVar (n - 1) c)
-
-generateHnatTermVar 0 c = c
-generateHnatTermVar n c = STermVar (generateHnatTermVar (n - 1) c)
-
-typemap :: (HNat -> Type -> Type) -> HNat -> Type -> Type
-typemap onTypeVar c (TyVar hnat) = onTypeVar c (TyVar hnat)
-typemap onTypeVar c (TyArr t1 t2) =
-  TyArr (typemap onTypeVar c t1) (typemap onTypeVar c t2)
-typemap onTypeVar c (TyAll t1) = TyAll (typemap onTypeVar (STypeVar c) t1)
-typemap onTypeVar c (TyBase) = TyBase
-
-termmap ::
-     (HNat -> Term -> Term) -> (HNat -> Type -> Type) -> HNat -> Term -> Term
-termmap onTermVar onTypeVar c (TmVar hnat) = onTermVar c (TmVar hnat)
-termmap onTermVar onTypeVar c (TmAbs x t) =
-  TmAbs (termmap onTermVar onTypeVar (STermVar c) x) (typemap onTypeVar c t)
-termmap onTermVar onTypeVar c (TmApp t1 t2) =
-  TmApp (termmap onTermVar onTypeVar c t1) (termmap onTermVar onTypeVar c t2)
-termmap onTermVar onTypeVar c (TmTApp t1 t) =
-  TmTApp (termmap onTermVar onTypeVar c t1) (typemap onTypeVar c t)
-termmap onTermVar onTypeVar c (TmTAbs t1) =
-  TmTAbs (termmap onTermVar onTypeVar (STypeVar c) t1)
-
-typeshiftHelpplus d c (TyVar hnat)
-  | hnat >= c = TyVar (plus hnat d)
-  | otherwise = TyVar hnat
-
-termshiftHelpplus d c (TmVar hnat)
-  | hnat >= c = TmVar (plus hnat d)
-  | otherwise = TmVar hnat
-
-typeshiftplus :: HNat -> Type -> Type
-typeshiftplus d t = typemap (typeshiftHelpplus d) Z t
-
-termshiftplus :: HNat -> Term -> Term
-termshiftplus d t = termmap (termshiftHelpplus d) (typeshiftHelpplus d) Z t
-
-typeshiftHelpminus d c (TyVar hnat)
-  | hnat >= c = TyVar (minus hnat d)
-  | otherwise = TyVar hnat
-
-termshiftHelpminus d c (TmVar hnat)
-  | hnat >= c = TmVar (minus hnat d)
-  | otherwise = TmVar hnat
-
-typeshiftminus :: HNat -> Type -> Type
-typeshiftminus d t = typemap (typeshiftHelpminus d) Z t
-
-termshiftminus :: HNat -> Term -> Term
-termshiftminus d t = termmap (termshiftHelpminus d) (typeshiftHelpminus d) Z t
-
-typeSubstituteHelp sub orig c (TyVar hnat)
-  | hnat == plus orig c = typeshiftplus c sub
-  | otherwise = TyVar hnat
-
-termSubstituteHelp sub orig c (TmVar hnat)
-  | hnat == plus orig c = termshiftplus c sub
-  | otherwise = TmVar hnat
-
-typetypeSubstitute :: Type -> HNat -> Type -> Type
-typetypeSubstitute sub orig t = typemap (typeSubstituteHelp sub orig) Z t
-
-termtermSubstitute :: Term -> HNat -> Term -> Term
-termtermSubstitute sub orig t =
-  termmap (termSubstituteHelp sub orig) (\c x -> x) Z t
-
-termtypeSubstitute :: Type -> HNat -> Term -> Term
-termtypeSubstitute sub orig t =
-  termmap (\c x -> x) (typeSubstituteHelp sub orig) Z t
-
-freeVariablesType :: HNat -> Type -> [HNat]
-freeVariablesType c (TyVar hnat)
-  | hnat >= c = [minus hnat c]
-  | otherwise = []
-freeVariablesType c (TyArr t1 t2) =
-  nub ((freeVariablesType c t1) ++ (freeVariablesType c t2))
-freeVariablesType c (TyAll t1) = nub ((freeVariablesType (STypeVar c) t1))
-freeVariablesType c (TyBase) = nub ([])
-
-freeVariablesTerm :: HNat -> Term -> [HNat]
-freeVariablesTerm c (TmVar hnat)
-  | hnat >= c = [minus hnat c]
-  | otherwise = []
-freeVariablesTerm c (TmAbs x t) =
-  nub ((freeVariablesTerm (STermVar c) x) ++ (freeVariablesType c t))
-freeVariablesTerm c (TmApp t1 t2) =
-  nub ((freeVariablesTerm c t1) ++ (freeVariablesTerm c t2))
-freeVariablesTerm c (TmTApp t1 t) =
-  nub ((freeVariablesTerm c t1) ++ (freeVariablesType c t))
-freeVariablesTerm c (TmTAbs t1) = nub ((freeVariablesTerm (STypeVar c) t1))