Add tests for FCo

FCO/FCoImpl.hs

@@ -5,6 +5,8 @@ module FCoImpl
   , isVal
   , stepEval
   , typeOf
+  , typeOfCo
+  , typeOfCoReverse
   , fullEval
   , Variable(..)
   , Env(..)

FCO/Makefile

+asttool : *.hs
+	ghc Test.hs Comble.hs FCoSorts.hs FCoImpl.hs FiSorts.hs FiImpl.hs -dynamic -o test
+clean : 
+	rm test *.o *.hi
+

FCO/Test.hs

+import Test.QuickCheck
+import Data.Either
+import Data.Maybe
+import Control.Monad
+import System.CPUTime
+import Text.Printf
+
+import FCoSorts as CoS
+import FCoImpl as CoI
+import FiSorts as FiS
+import FiImpl as FiI
+import Comble
+
+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
+coPreservation :: Term -> Property
+coPreservation te = (isRight ty) && (not $ CoI.isVal te)
+                ==> (fromRight undefined ty) == (fromRight undefined tyStep)
+  where ty = CoI.typeOf te CoI.Nil
+        tyStep = (flip CoI.typeOf) CoI.Nil $ fromMaybe undefined $ CoI.stepEval te
+
+testCoPreservation size = quickCheckWithResult args $ CoS.forTermWithSize Z size subsize subsize coPreservation
+  where subsize = round $ logBase 1.7 $ fromIntegral size
+
+doCoPresTest :: [Integer] -> IO ()
+doCoPresTest []           = return ()
+doCoPresTest (size:sizes) = do printf "Testing preservation with size %d\n" size
+                               res <- time $ testCoPreservation size
+                               if isSuccess res
+                                 then doCoPresTest sizes
+                                 else return ()
+
+
+-- If a term is well-typed, it is either a 'value', or it is possible to performa reduction.
+coProgress :: Term -> Property
+coProgress te = isRight (CoI.typeOf te CoI.Nil)
+            ==> (CoI.isVal te) || (isJust (CoI.stepEval te))
+
+testCoProgress size = quickCheckWithResult args $ CoS.forTermWithSize Z size subsize subsize coProgress
+  where subsize = round $ logBase 1.7 $ fromIntegral size
+
+doCoProgTest :: [Integer] -> IO ()
+doCoProgTest []           = return ()
+doCoProgTest (size:sizes) = do printf "Testing progress with size %d\n" size
+                               res <- time $ testCoProgress size
+                               if isSuccess res
+                                 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 ()
+
+time :: IO a -> IO a
+time action = do start <- getCPUTime
+                 res <- action
+                 end <- getCPUTime
+                 printf "Time: %0.9f s\n" (((fromIntegral (end - start)) / 1000000000000.0) :: Double)
+                 return res
+
+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]
+          return ()