lazy-lambda-calculus: d634e87dc3c547664fd7b4b10492bd9c93e7ca1a

     1: {-# Language FlexibleInstances #-}
     2: {-# Language MultiParamTypeClasses #-}
     3: {-# Language FlexibleContexts #-}
     4: {-# Language ExistentialQuantification #-}
     5: {-# Language DeriveDataTypeable #-}
     6: 
     7: module Data.Language.LC.Self.Test where
     8: 
     9: import Control.Monad.Partial
    10: import Data.Nat
    11: import Data.Data
    12: import Data.Language.LC
    13: import Data.Language.LC.Test
    14: import Data.Language.LC.Self
    15: import Data.Map
    16: import Data.Maybe
    17: import Data.Typeable
    18: import Data.Test
    19: import Test.LazySmallCheck2012 hiding (Nat, Term, Const)
    20: import Test.LazySmallCheck2012.Core hiding (Term, C, mkTest)
    21: 
    22: import Debug.Trace
    23: 
    24: newtype Wrap a = W a deriving (Eq, Show, Data, Typeable)
    25: 
    26: instance Serial a => Serial (Wrap a) where
    27:   series = cons1 W
    28: 
    29: instance (Encodable a, Show a) => Encodable (Wrap a) where
    30:   mse (W x) = Lam (0 :@ mse x)
    31:   unmse x = eval' (0 :@ 1) [cast' x,
    32:                             Now (F (fmap (valMap W) . (>>= unmse)))]
    33: {-
    34: foo :: (Val a -> Partial (Val a)) -> Val (Wrap a) -> Partial (Val (Wrap a))
    35: foo m f = eval' (0 :@ 1) [Now f, Now (F (>>= bar m))]
    36: 
    37: bar :: (Val a -> Partial (Val a))
    38: bar = Now
    39: -}
    40: encodeDecode :: Encodable a => a -> Partial (Val a)
    41: encodeDecode = decode . mse
    42: 
    43: encodeDecodeIn n x = force n (encodeDecode x) == Just (C x)
    44: 
    45: mkTest :: (Serial a, Eq a, Encodable a) => (a -> Nat) -> Test
    46: mkTest f = Test $ \x -> encodeDecodeIn (f x) x
    47: 
    48: selfTestMap :: Map String Test
    49: selfTestMap = fromList [
    50: 
    51:                 -- Finite enumerations
    52:                 ("()",   mkTest (const 2 :: ()   -> Nat)),
    53: 
    54:                 ("Bool", mkTest (const 3 :: Bool -> Nat)),
    55: 
    56:                 -- Unbounded enumerations
    57:                 ("Nat",  mkTest (3+)),
    58: 
    59:                 -- Finite wrappers
    60:                 ("Wrap ()", mkTest (const 3 :: Wrap () -> Nat))
    61: 
    62:                 --("Partial ()", mkTest (((2+) . laterCount) :: Partial () -> Nat))
    63: 
    64:               ]
    65: 
    66: decodeNat n x = closed x ==> evalN n (mse (S Z) :@ Const Z :@ x) /= Just (C (S Z))
    67: 
    68: 
    69: 
    70: selfTest  = testRunner  selfTestMap
    71: selfTests = testsRunner selfTestMap