lazy-lambda-calculus: 4b3e729e7aa1f77400dca97eeb868a0d31043cb5

     1: {-# Language FlexibleInstances #-}
     2: {-# Language MultiParamTypeClasses #-}
     3: {-# Language FlexibleContexts #-}
     4: {-# Language ExistentialQuantification #-}
     5: 
     6: module Data.Language.LC.Test where
     7: 
     8: import Control.Monad.Partial
     9: import Data.Nat
    10: import Data.Data
    11: import Data.Language.LC
    12: import Data.Map
    13: import Data.Maybe
    14: import Data.Test
    15: import Data.Typeable
    16: import Test.LazySmallCheck2012 hiding (Nat, Term, Const)
    17: import Test.LazySmallCheck2012.Core hiding (Term, C)
    18: 
    19: -- Randomly generate terms
    20: instance Serial a => Serial (Term a) where
    21:   series = cons1 Var \/
    22:            cons1 Lam \/
    23:            cons2 (:@)
    24: 
    25: equalIn   n x y = trueIn     n (fmap (== C x) (eval y))
    26: notDiffIn n x y = notFalseIn n (fmap (== C x) (eval y))
    27: 
    28: lcTestMap :: Map String Test
    29: lcTestMap = let i = (Lam 0 :: Term Nat) in
    30:             fromList [
    31:               ("evalCoterminates",
    32:                Test $ \x n -> let x' = evalN n (x :: Term Nat) in
    33:                               closed x ==> isJust x' || isNothing x'),
    34: 
    35:               ("omegaDiverges",
    36:                Test $ \n -> isNothing (evalN n (omega :: Term ()))),
    37: 
    38:               ("eval$$",
    39:                Test $ \x -> trueIn  1 (fmap (== C x) (eval i >>= ($$ x)))),
    40: 
    41:               ("evalSteps",
    42:                Test $ \x -> equalIn 3 x (i :@ i :@ Const x)),
    43: 
    44:               ("id",
    45:                Test $ \x -> equalIn 2 x (i :@ Const x)),
    46: 
    47:               ("yTerminates",
    48:                Test $ \x -> equalIn 7 x ((yComb :: Term Nat) :@ Lam (Lam 0) :@ Const x)),
    49: 
    50:               ("zConst",
    51:                Test $ \x -> equalIn 5 x (zComb :@ Lam (Lam 0) :@ Const (x :: Int)))
    52:             ]
    53: 
    54: testsRunner ts n = let next []                  = return ()
    55:                        next ((name, Test t):xs) = do print name
    56:                                                      depthCheck n t
    57:                                                      next xs in
    58:                    next . toList $ ts
    59: 
    60: testRunner ts n t = case Data.Map.lookup t ts of
    61:                       Nothing       -> error ("Could not find test " ++ t)
    62:                       Just (Test x) -> depthCheck n x
    63: 
    64: lcTests = testsRunner lcTestMap
    65: lcTest  = testRunner  lcTestMap
    66: 
    67: {-
    68: plus  Z    y = y
    69: plus (S x) y = S (plus x y)
    70: 
    71:  Z    a b = a
    72: (S x) a b = b (x a b)
    73: 
    74: plus f  Z    y = Z y _
    75: plus f (S x) y = (S x) _ (\x -> f x y)
    76: plus f x y = x y (\n -> f n y)
    77: \f (\x (\y ((x y) (\n ((f n) y)))))
    78: \  (\  (\  ((1 0) (\  ((3 0) 1)))))
    79: 
    80: plus = zComb :@ Lam (Lam (Lam (1 :@ 0 :@ (Lam (3 :@ 0 :@ 1)))))
    81: testPlus x y = let sum = plus :@ church x :@ church y
    82:                    result = force (2 * (x + y + 10)) (eval sum) in
    83:                result == Just (church (x + y))
    84: -}