Commit 9256e44d authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Add test code for elaboration to main

parent 79c9cedd
......@@ -13,8 +13,6 @@ data Variable = Z
| STypeVar Variable
deriving(Show, Eq)
plus (Z) h = h
plus h (Z) = h
plus x1 (STermVar x2) = (STermVar (plus x1 x2))
......
......@@ -9,6 +9,7 @@ import FCoSorts as CoS
import FCoImpl as CoI
import FiSorts as FiS
import FiImpl as FiI
import Elaborate as El
import Comble
args = Args{replay=Nothing, maxSuccess=1000, maxDiscardRatio=1000000, maxSize=100, chatty=True, maxShrinks=100}
......@@ -48,27 +49,20 @@ doCoProgTest (size:sizes) = do printf "Testing progress with size %d\n" size
then doCoProgTest sizes
else return ()
---- The reverse of a type coercion is the original type (?)
--coercionReversible :: (CoS.Coercion, CoS.Type) -> Property
--coercionReversible (co, ty) = (isRight forward) && (isRight backward)
-- ==> (fromRight undefined forward) == (fromRight undefined backward)
-- where forward = CoI.typeOfCo co ty
-- backward = CoI.typeOfCoReverse co $ fromRight undefined forward
--
--testCoercionReverse :: Integer -> IO Result
--testCoercionReverse size = let coercions = CoS.coercionOfSize Z size size
-- types = CoS.typeUpToSize Z size
-- g = (,) <$> ((!) <$> pure coercions <*> chooseInteger (0, (card coercions) - 1))
-- <*> ((!) <$> pure types <*> chooseInteger (0, (card types) - 1))
-- in quickCheckWithResult args $ forAll g coercionReversible
--
--doCoercionReverseTest :: [Integer] -> IO ()
--doCoercionReverseTest [] = return ()
--doCoercionReverseTest (size:sizes) = do printf "Testing coercion reversability with size %d\n" size
-- res <- time $ testCoercionReverse size
-- if isSuccess res
-- then doCoercionReverseTest sizes
-- else return ()
-- If a Fi term is well-typed, it has a corresponding FCo term
elaboration :: FiS.FiTerm -> Property
elaboration te = isRight (FiI.typeOf te FiI.Nil)
==> isRight $ El.elaborate te FiI.Nil
testElaboration size = quickCheckWithResult args $ FiS.forFiTermWithSize FiS.Z size subsize elaboration
where subsize = round $ logBase 1.5 $ fromIntegral size
doElaborationTest :: [Integer] -> IO ()
doElaborationTest (size:sizes) = do printf "Testing elaboration with size %d\n" size
res <- time $ testElaboration size
if isSuccess res
then doElaborationTest sizes
else return ()
time :: IO a -> IO a
time action = do start <- getCPUTime
......@@ -81,6 +75,7 @@ main = do printf "===Testing Preservation property for FCo===\n"
doCoPresTest [4..7]
printf "===Testing Progress property for FCo===\n"
doCoProgTest [4..7]
-- printf "===Testing Reverse property for FCo===\n"
-- doCoercionReverseTest [4..8]
printf "===Testing Elaboration property===\n"
doElaborationTest [4..10]
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