Commit 111fadf7 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Add System F tests & memoization

parent 9d78e10c
asttool : *.hs
ghc Test.hs Comble.hs SystemFImpl.hs SystemFSorts.hs -dynamic -o test
clean :
rm test *.o *.hi
......@@ -4,6 +4,8 @@ import Control.Applicative
import Comble
import Test.QuickCheck
import Data.Array as A
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)
......@@ -95,7 +97,7 @@ termEnv (Z) = (Z)
forTermWithSize env nTerm nType prop = (let c = (termOfSize env nTerm nType)
n = (card c)
g = ((!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
in (forAll g prop))
typeOfSize env 0 = (empty)
......@@ -114,7 +116,7 @@ typeEnv (Z) = (Z)
forTypeWithSize env nType prop = (let c = (typeOfSize env nType)
n = (card c)
g = ((!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
in (forAll g prop))
genInt = (asum [(pure 0),(pure 1),(pure 2),(pure 3)])
......@@ -142,3 +144,51 @@ instance Ord Variable where
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)
-- Custom, non-generated code
-- We use a prefix tree for storing environments. Each environment has an associated table of possible terms.
data EnvTree i e = Node (EnvTree i e) (EnvTree i e) (Array i e)
-- Tabulate our function for generating terms over our possible range.
maketable :: (Ix i) => (i -> e) -> (i,i) -> A.Array i e
maketable f (l,u) =
listArray (l,u) (map f (range (l,u)))
-- Create the infinite lazy tree representing our space of possible Comble parameters.
-- An optimization would be reducing the term limit on the range by 1 every node we go down.
treeify :: (Ix i) => (Variable -> i -> e) -> Variable -> (i, i) -> EnvTree i e
treeify f env (l, u) = Node (treeify f (STermVar env) (l, u)) (treeify f (STypeVar env) (l, u)) (maketable (f env) (l, u))
-- Walk the tree, taking a left at every term abstraction and a right at every type abstraction until
-- we arrive at the table for our current environment.
walk :: (Ix i) => EnvTree i e -> Variable -> i -> e
walk (Node _ _ table) Z ix = table A.! ix
walk (Node l _ _ ) (STermVar n) ix = walk l n ix
walk (Node _ r _ ) (STypeVar n) ix = walk r n ix
memoTerm :: Variable -> Integer -> Integer -> Comble Term
memoTerm env nTe nType = memo env nTe
where
-- Define our tree.
tree :: EnvTree Integer (Comble Term)
tree = treeify go Z (0, nTe)
-- Whenever we need a value, don't calculate it, but look it up (which involves calculating it if
-- it hasn't been calculated already)
memo :: Variable -> Integer -> Comble Term
memo env nTerm = walk tree env nTerm
-- This function is just a slightly modified version of termOfSize
go :: Variable -> Integer -> Comble Term
go env 0 = (empty)
go env 1 = (TmVar <$> (getTermVar env (Z)))
go env nTerm = ((TmAbs <$> (memo (termEnv (STermVar env)) (nTerm - 1)) <*> (typeOfSize (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (memo (termEnv env) ((!!) l 0)) <*> (memo (termEnv env) ((!!) l 1)))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (memo (termEnv env) (nTerm - 1)) <*> (typeOfSize (typeEnv env) nType))
<|> (TmTAbs <$> (memo (termEnv (STypeVar env)) (nTerm - 1))))
forMemoTermWithSize env nTerm nType prop = (let c = (memoTerm env nTerm nType)
n = (card c)
g = ((Comble.!) <$> (pure c) <*> (chooseInteger (0, (n - 1))))
in (forAll g prop))
import Test.QuickCheck
import Data.Either
import Data.Maybe
import Control.Monad
import System.CPUTime
import Text.Printf
import SystemFSorts
import SystemFImpl
import Comble
args = Args{replay=Nothing, maxSuccess=1000, maxDiscardRatio=10000, maxSize=100, chatty=True, maxShrinks=100}
args = Args{replay=Nothing, maxSuccess=1000, maxDiscardRatio=1000000, maxSize=100, chatty=True, maxShrinks=100}
-- The type of a term does not change when a reduction step is performed
preservation :: Term -> Property
......@@ -20,3 +23,50 @@ progress :: Term -> Property
progress te = isRight (typeOf te Nil)
==> (isVal te) || (isJust (stepEval te))
testPreservation size = quickCheckWithResult args $ forTermWithSize Z size (round $ logBase 1.5 $ fromIntegral size) preservation
doPresTest :: [Integer] -> IO ()
doPresTest [] = return ()
doPresTest (size:sizes) = do printf "Testing preservation with size %d\n" size
res <- time $ testPreservation size
if isSuccess res
then doPresTest sizes
else return ()
testProgress size = quickCheckWithResult args $ forTermWithSize Z size (round $ logBase 1.5 $ fromIntegral size) progress
doProgTest :: [Integer] -> IO ()
doProgTest [] = return ()
doProgTest (size:sizes) = do printf "Testing progress with size %d\n" size
res <- time $ testProgress size
if isSuccess res
then doProgTest sizes
else return ()
testProgressMemo size = quickCheckWithResult args $ forMemoTermWithSize Z size (round $ logBase 1.5 $ fromIntegral size) progress
doProgTestMemo :: [Integer] -> IO ()
doProgTestMemo [] = return ()
doProgTestMemo (size:sizes) = do printf "Testing progress with size %d\n" size
res <- time $ testProgressMemo size
if isSuccess res
then doProgTestMemo sizes
else return ()
time :: IO a -> IO a
time action = do start <- getCPUTime
res <- action
end <- getCPUTime
printf "Average Time: %0.9f s\n" (((fromIntegral (end - start)) / 1000000000000.0) / 10.0 :: Double)
return res
main = do let sizes = [4..11]
printf "===Testing Preservation property===\n"
doPresTest sizes
printf "===Testing Progress property===\n"
doProgTest sizes
printf "===Testing Progress property with memoized Comble===\n"
doProgTestMemo [4..14]
return ()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment