-- editorconfig-checker-disable-file
{-| Description : Property based testing for Plutus Core

This file contains the tests and some associated machinery but not the
generators.
-}

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeApplications      #-}

module PlutusCore.Generators.NEAT.Spec
  ( tests
  , Options (..)
  , TestFail (..)
  , bigTest
  , packAssertion
  , tynames
  , names
  , throwCtrex
  , Ctrex (..)
  , handleError
  , handleUError
  , GenDepth (..)
  , GenMode (..)
  ) where

import PlutusCore
import PlutusCore.Compiler.Erase
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Generators.NEAT.Common
import PlutusCore.Generators.NEAT.Term
import PlutusCore.Normalize
import PlutusCore.Pretty

import UntypedPlutusCore qualified as U
import UntypedPlutusCore.Evaluation.Machine.Cek qualified as U

import Control.Monad (unless)
import Control.Monad.Except (ExceptT, catchError, liftEither, runExceptT, throwError, withExceptT)
import Control.Search (Enumerable (..), Options (..), search')
import Data.Maybe
import Data.Stream qualified as Stream
import Data.Tagged
import Data.Text qualified as Text
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.Options
import Text.Printf

-- * Property-based tests

-- | Search depth, measured in program size
newtype GenDepth = GenDepth {GenDepth -> Int
unGenDepth :: Int}
    deriving newtype (ReadPrec [GenDepth]
ReadPrec GenDepth
Int -> ReadS GenDepth
ReadS [GenDepth]
(Int -> ReadS GenDepth)
-> ReadS [GenDepth]
-> ReadPrec GenDepth
-> ReadPrec [GenDepth]
-> Read GenDepth
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GenDepth
readsPrec :: Int -> ReadS GenDepth
$creadList :: ReadS [GenDepth]
readList :: ReadS [GenDepth]
$creadPrec :: ReadPrec GenDepth
readPrec :: ReadPrec GenDepth
$creadListPrec :: ReadPrec [GenDepth]
readListPrec :: ReadPrec [GenDepth]
Read, GenDepth -> GenDepth -> Bool
(GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool) -> Eq GenDepth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GenDepth -> GenDepth -> Bool
== :: GenDepth -> GenDepth -> Bool
$c/= :: GenDepth -> GenDepth -> Bool
/= :: GenDepth -> GenDepth -> Bool
Eq, Eq GenDepth
Eq GenDepth =>
(GenDepth -> GenDepth -> Ordering)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> Bool)
-> (GenDepth -> GenDepth -> GenDepth)
-> (GenDepth -> GenDepth -> GenDepth)
-> Ord GenDepth
GenDepth -> GenDepth -> Bool
GenDepth -> GenDepth -> Ordering
GenDepth -> GenDepth -> GenDepth
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GenDepth -> GenDepth -> Ordering
compare :: GenDepth -> GenDepth -> Ordering
$c< :: GenDepth -> GenDepth -> Bool
< :: GenDepth -> GenDepth -> Bool
$c<= :: GenDepth -> GenDepth -> Bool
<= :: GenDepth -> GenDepth -> Bool
$c> :: GenDepth -> GenDepth -> Bool
> :: GenDepth -> GenDepth -> Bool
$c>= :: GenDepth -> GenDepth -> Bool
>= :: GenDepth -> GenDepth -> Bool
$cmax :: GenDepth -> GenDepth -> GenDepth
max :: GenDepth -> GenDepth -> GenDepth
$cmin :: GenDepth -> GenDepth -> GenDepth
min :: GenDepth -> GenDepth -> GenDepth
Ord)

-- | Search strategy
newtype GenMode = GenMode {GenMode -> Options
unGenMode :: Options}
    deriving newtype (ReadPrec [GenMode]
ReadPrec GenMode
Int -> ReadS GenMode
ReadS [GenMode]
(Int -> ReadS GenMode)
-> ReadS [GenMode]
-> ReadPrec GenMode
-> ReadPrec [GenMode]
-> Read GenMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GenMode
readsPrec :: Int -> ReadS GenMode
$creadList :: ReadS [GenMode]
readList :: ReadS [GenMode]
$creadPrec :: ReadPrec GenMode
readPrec :: ReadPrec GenMode
$creadListPrec :: ReadPrec [GenMode]
readListPrec :: ReadPrec [GenMode]
Read)

instance IsOption GenDepth where
    defaultValue :: GenDepth
defaultValue = Int -> GenDepth
GenDepth Int
20
    parseValue :: String -> Maybe GenDepth
parseValue = String -> Maybe GenDepth
forall a. Read a => String -> Maybe a
safeRead
    optionName :: Tagged GenDepth String
optionName = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenDepth String
"gen-depth"
    optionHelp :: Tagged GenDepth String
optionHelp = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenDepth String
"Gen depth"

instance IsOption GenMode where
    defaultValue :: GenMode
defaultValue = Options -> GenMode
GenMode Options
OF
    parseValue :: String -> Maybe GenMode
parseValue = String -> Maybe GenMode
forall a. Read a => String -> Maybe a
safeRead
    optionName :: Tagged GenMode String
optionName = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenMode String
"gen-mode"
    optionHelp :: Tagged GenMode String
optionHelp = forall {k} (s :: k) b. b -> Tagged s b
forall s b. b -> Tagged s b
Tagged @GenMode String
"Gen Mode"

tests :: TestTree
tests :: TestTree
tests =
  String -> [TestTree] -> TestTree
testGroup String
"NEAT"
  -- the `adjustOption (min ...)` allows to make these big tests easier at runtime
  [ (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
10) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    String
-> Kind () -> (Kind () -> ClosedTypeG -> Assertion) -> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"normalization commutes with conversion from generated types"
      (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
      ((Kind () -> ClosedTypeG -> ExceptT TestFail Quote ())
-> Kind () -> ClosedTypeG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion Kind () -> ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes)
  , (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
12) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    String
-> Kind ()
-> (Kind () -> Normalized ClosedTypeG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"normal types cannot reduce"
      (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
      ((Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ())
-> Kind () -> Normalized ClosedTypeG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce)
  , (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
15) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    String
-> ClosedTypeG
-> (ClosedTypeG -> ClosedTermG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"type preservation - CK"
      (TypeBuiltinG -> ClosedTypeG
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyUnitG)
      ((ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ())
-> ClosedTypeG -> ClosedTermG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation)
  , (GenDepth -> GenDepth) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (GenDepth -> GenDepth -> GenDepth
forall a. Ord a => a -> a -> a
min (GenDepth -> GenDepth -> GenDepth)
-> GenDepth -> GenDepth -> GenDepth
forall a b. (a -> b) -> a -> b
$ Int -> GenDepth
GenDepth Int
15) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    String
-> ClosedTypeG
-> (ClosedTypeG -> ClosedTermG -> Assertion)
-> TestTree
forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
"typed CK vs untyped CEK produce the same output"
      (TypeBuiltinG -> ClosedTypeG
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyUnitG)
      ((ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ())
-> ClosedTypeG -> ClosedTermG -> Assertion
forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval)
  ]


{- NOTE:

The tests below perform multiple steps in a pipeline, they take in
kind & type or type & term and then perform operations on them passing
the result along to the next one, sometimes the result is passed to
several operations and/or several results are later combined and
sometimes a result is discarded. Quite a lot of this is inherently
sequential. There is some limited opportunity for parallelism which is
not exploited.

-}

-- handle a user error and turn it back into an error term
handleError :: Type TyName DefaultUni ()
       -> U.ErrorWithCause (U.EvaluationError structural operational) term
       -> Either (U.ErrorWithCause (U.EvaluationError structural operational) term)
                 (Term TyName Name DefaultUni DefaultFun ())
handleError :: forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty ErrorWithCause (EvaluationError structural operational) term
e = case ErrorWithCause (EvaluationError structural operational) term
-> EvaluationError structural operational
forall err cause. ErrorWithCause err cause -> err
U._ewcError ErrorWithCause (EvaluationError structural operational) term
e of
  U.StructuralEvaluationError structural
_  -> ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term TyName Name DefaultUni DefaultFun ())
forall a.
ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrorWithCause (EvaluationError structural operational) term
e
  U.OperationalEvaluationError operational
_ -> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term TyName Name DefaultUni DefaultFun ())
forall a.
a
-> Either
     (ErrorWithCause (EvaluationError structural operational) term) a
forall (m :: * -> *) a. Monad m => a -> m a
return (()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error () Type TyName DefaultUni ()
ty)

-- untyped version of `handleError`
handleUError ::
          U.ErrorWithCause (U.EvaluationError structural operational) term
       -> Either (U.ErrorWithCause (U.EvaluationError structural operational) term)
                 (U.Term Name DefaultUni DefaultFun ())
handleUError :: forall structural operational term.
ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term Name DefaultUni DefaultFun ())
handleUError ErrorWithCause (EvaluationError structural operational) term
e = case ErrorWithCause (EvaluationError structural operational) term
-> EvaluationError structural operational
forall err cause. ErrorWithCause err cause -> err
U._ewcError ErrorWithCause (EvaluationError structural operational) term
e of
  U.StructuralEvaluationError structural
_  -> ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term Name DefaultUni DefaultFun ())
forall a.
ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrorWithCause (EvaluationError structural operational) term
e
  U.OperationalEvaluationError operational
_ -> Term Name DefaultUni DefaultFun ()
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term Name DefaultUni DefaultFun ())
forall a.
a
-> Either
     (ErrorWithCause (EvaluationError structural operational) term) a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
U.Error ())

-- |Property: check if the type is preserved by evaluation.
--
-- This property is expected to hold for the CK machine.
--
prop_typePreservation :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_typePreservation ClosedTypeG
tyG ClosedTermG
tmG = do
  TypeCheckConfig DefaultUni DefaultFun
tcConfig <- (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   (TypeCheckConfig DefaultUni DefaultFun)
 -> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun))
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig ()

  -- Check if the type checker for generated terms is sound:
  Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
 -> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) ClosedTypeG
tyG
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
  Term TyName Name DefaultUni DefaultFun ()
tm <- (GenError -> TestFail)
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm Stream Text
tynames Stream Text
names ClosedTypeG
tyG ClosedTermG
tmG
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tm (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)

  -- Check if the converted term, when evaluated by CK, still has the same type:

  Term TyName Name DefaultUni DefaultFun ()
tmCK <- (CkEvaluationException DefaultUni DefaultFun -> TestFail)
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CkEvaluationException DefaultUni DefaultFun -> TestFail
CkP (ExceptT
   (CkEvaluationException DefaultUni DefaultFun)
   Quote
   (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
  (CkEvaluationException DefaultUni DefaultFun)
  (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
   (CkEvaluationException DefaultUni DefaultFun)
   (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      (CkEvaluationException DefaultUni DefaultFun)
      Quote
      (Term TyName Name DefaultUni DefaultFun ()))
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
     (CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
defaultBuiltinsRuntimeForTesting Term TyName Name DefaultUni DefaultFun ()
tm Either
  (CkEvaluationException DefaultUni DefaultFun)
  (Term TyName Name DefaultUni DefaultFun ())
-> (CkEvaluationException DefaultUni DefaultFun
    -> Either
         (CkEvaluationException DefaultUni DefaultFun)
         (Term TyName Name DefaultUni DefaultFun ()))
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall a.
Either (CkEvaluationException DefaultUni DefaultFun) a
-> (CkEvaluationException DefaultUni DefaultFun
    -> Either (CkEvaluationException DefaultUni DefaultFun) a)
-> Either (CkEvaluationException DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` Type TyName DefaultUni ()
-> CkEvaluationException DefaultUni DefaultFun
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tmCK (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)

-- |Property: check if both the typed CK and untyped CEK machines produce the same output
-- modulo erasure.
--
prop_agree_termEval :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval :: ClosedTypeG -> ClosedTermG -> ExceptT TestFail Quote ()
prop_agree_termEval ClosedTypeG
tyG ClosedTermG
tmG = do
  TypeCheckConfig DefaultUni DefaultFun
tcConfig <- (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   (TypeCheckConfig DefaultUni DefaultFun)
 -> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun))
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
-> ExceptT TestFail Quote (TypeCheckConfig DefaultUni DefaultFun)
forall a b. (a -> b) -> a -> b
$ ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (TypeCheckConfig DefaultUni DefaultFun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig ()

  -- Check if the type checker for generated terms is sound:
  Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
 -> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) ClosedTypeG
tyG
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
  Term TyName Name DefaultUni DefaultFun ()
tm <- (GenError -> TestFail)
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> ExceptT
     GenError Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm Stream Text
tynames Stream Text
names ClosedTypeG
tyG ClosedTermG
tmG
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ TypeCheckConfig DefaultUni DefaultFun
-> ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Normalized (Type TyName DefaultUni ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> m ()
checkType TypeCheckConfig DefaultUni DefaultFun
tcConfig () Term TyName Name DefaultUni DefaultFun ()
tm (Type TyName DefaultUni () -> Normalized (Type TyName DefaultUni ())
forall a. a -> Normalized a
Normalized Type TyName DefaultUni ()
ty)

  -- run typed CK on input
  Term TyName Name DefaultUni DefaultFun ()
tmCk <- (CkEvaluationException DefaultUni DefaultFun -> TestFail)
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CkEvaluationException DefaultUni DefaultFun -> TestFail
CkP (ExceptT
   (CkEvaluationException DefaultUni DefaultFun)
   Quote
   (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      TestFail Quote (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     TestFail Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
  (CkEvaluationException DefaultUni DefaultFun)
  (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
   (CkEvaluationException DefaultUni DefaultFun)
   (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      (CkEvaluationException DefaultUni DefaultFun)
      Quote
      (Term TyName Name DefaultUni DefaultFun ()))
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT
     (CkEvaluationException DefaultUni DefaultFun)
     Quote
     (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
     (CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
forall term.
HasMeaningIn DefaultUni term =>
BuiltinsRuntime DefaultFun term
defaultBuiltinsRuntimeForTesting Term TyName Name DefaultUni DefaultFun ()
tm Either
  (CkEvaluationException DefaultUni DefaultFun)
  (Term TyName Name DefaultUni DefaultFun ())
-> (CkEvaluationException DefaultUni DefaultFun
    -> Either
         (CkEvaluationException DefaultUni DefaultFun)
         (Term TyName Name DefaultUni DefaultFun ()))
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall a.
Either (CkEvaluationException DefaultUni DefaultFun) a
-> (CkEvaluationException DefaultUni DefaultFun
    -> Either (CkEvaluationException DefaultUni DefaultFun) a)
-> Either (CkEvaluationException DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` Type TyName DefaultUni ()
-> CkEvaluationException DefaultUni DefaultFun
-> Either
     (CkEvaluationException DefaultUni DefaultFun)
     (Term TyName Name DefaultUni DefaultFun ())
forall structural operational term.
Type TyName DefaultUni ()
-> ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term TyName Name DefaultUni DefaultFun ())
handleError Type TyName DefaultUni ()
ty

  -- erase CK output
  let tmUCk :: Term Name DefaultUni DefaultFun ()
tmUCk = Term TyName Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term TyName Name DefaultUni DefaultFun ()
tmCk

  -- run untyped CEK on erased input
  Term Name DefaultUni DefaultFun ()
tmUCek <- (CekEvaluationException Name DefaultUni DefaultFun -> TestFail)
-> ExceptT
     (CekEvaluationException Name DefaultUni DefaultFun)
     Quote
     (Term Name DefaultUni DefaultFun ())
-> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT CekEvaluationException Name DefaultUni DefaultFun -> TestFail
UCekP (ExceptT
   (CekEvaluationException Name DefaultUni DefaultFun)
   Quote
   (Term Name DefaultUni DefaultFun ())
 -> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ()))
-> ExceptT
     (CekEvaluationException Name DefaultUni DefaultFun)
     Quote
     (Term Name DefaultUni DefaultFun ())
-> ExceptT TestFail Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Either
  (CekEvaluationException Name DefaultUni DefaultFun)
  (Term Name DefaultUni DefaultFun ())
-> ExceptT
     (CekEvaluationException Name DefaultUni DefaultFun)
     Quote
     (Term Name DefaultUni DefaultFun ())
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either
   (CekEvaluationException Name DefaultUni DefaultFun)
   (Term Name DefaultUni DefaultFun ())
 -> ExceptT
      (CekEvaluationException Name DefaultUni DefaultFun)
      Quote
      (Term Name DefaultUni DefaultFun ()))
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
-> ExceptT
     (CekEvaluationException Name DefaultUni DefaultFun)
     Quote
     (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
U.evaluateCekNoEmit MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
defaultCekParametersForTesting (Term TyName Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term TyName Name DefaultUni DefaultFun ()
tm) Either
  (CekEvaluationException Name DefaultUni DefaultFun)
  (Term Name DefaultUni DefaultFun ())
-> (CekEvaluationException Name DefaultUni DefaultFun
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
forall a.
Either (CekEvaluationException Name DefaultUni DefaultFun) a
-> (CekEvaluationException Name DefaultUni DefaultFun
    -> Either (CekEvaluationException Name DefaultUni DefaultFun) a)
-> Either (CekEvaluationException Name DefaultUni DefaultFun) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` CekEvaluationException Name DefaultUni DefaultFun
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
forall structural operational term.
ErrorWithCause (EvaluationError structural operational) term
-> Either
     (ErrorWithCause (EvaluationError structural operational) term)
     (Term Name DefaultUni DefaultFun ())
handleUError

  -- check if typed CK and untyped CEK give the same output modulo erasure
  Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term Name DefaultUni DefaultFun ()
tmUCk Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun () -> Bool
forall a. Eq a => a -> a -> Bool
== Term Name DefaultUni DefaultFun ()
tmUCek) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
    Ctrex -> ExceptT TestFail Quote ()
throwCtrex (ClosedTypeG
-> ClosedTermG
-> [(String, Term Name DefaultUni DefaultFun ())]
-> Ctrex
CtrexUntypedTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String
"untyped CK",Term Name DefaultUni DefaultFun ()
tmUCk),(String
"untyped CEK",Term Name DefaultUni DefaultFun ()
tmUCek)])

-- |Property: the following diagram commutes for well-kinded types...
--
-- @
--                  convertClosedType
--    ClosedTypeG ---------------------> Type TyName DefaultUni ()
--         |                                        |
--         |                                        |
--         | normalizeTypeG                         | normalizeType
--         |                                        |
--         v                                        v
--    ClosedTypeG ---------------------> Type TyName DefaultUni ()
--                  convertClosedType
-- @
--
prop_normalizeConvertCommuteTypes :: Kind ()
                                  -> ClosedTypeG
                                  -> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes :: Kind () -> ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG = do
  -- Check if the kind checker for generated types is sound:
  Type TyName DefaultUni ()
ty <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
 -> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames Kind ()
k ClosedTypeG
tyG
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty Kind ()
k

  -- Check if the converted type, when reduced, still has the same kind:
  Type TyName DefaultUni ()
ty1 <- (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   (Type TyName DefaultUni ())
 -> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a. Normalized a -> a
unNormalized (Normalized (Type TyName DefaultUni ())
 -> Type TyName DefaultUni ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (Normalized (Type TyName DefaultUni ()))
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     (Normalized (Type TyName DefaultUni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType Type TyName DefaultUni ()
ty
  (TypeError
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   ()
 -> TestFail)
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> TestFail
TypeError (ExceptT
   (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
   Quote
   ()
 -> ExceptT TestFail Quote ())
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
-> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$ KindCheckConfig
-> ()
-> Type TyName DefaultUni ()
-> Kind ()
-> ExceptT
     (TypeError
        (Term TyName Name DefaultUni DefaultFun ())
        DefaultUni
        DefaultFun
        ())
     Quote
     ()
forall err term (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err term uni fun ann m =>
KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
checkKind KindCheckConfig
defKindCheckConfig () Type TyName DefaultUni ()
ty Kind ()
k

  -- Check if normalization for generated types is sound:
  Type TyName DefaultUni ()
ty2 <- (GenError -> TestFail)
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT GenError -> TestFail
GenError (ExceptT GenError Quote (Type TyName DefaultUni ())
 -> ExceptT TestFail Quote (Type TyName DefaultUni ()))
-> ExceptT GenError Quote (Type TyName DefaultUni ())
-> ExceptT TestFail Quote (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Stream Text
-> Kind ()
-> ClosedTypeG
-> ExceptT GenError Quote (Type TyName DefaultUni ())
forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames Kind ()
k (ClosedTypeG -> ClosedTypeG
forall n. TypeG n -> TypeG n
normalizeTypeG ClosedTypeG
tyG)

  Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type TyName DefaultUni ()
ty1 Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
== Type TyName DefaultUni ()
ty2) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
    Ctrex -> ExceptT TestFail Quote ()
throwCtrex (Kind ()
-> ClosedTypeG
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Ctrex
CtrexNormalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2)



-- |Property: normal types cannot reduce
prop_normalTypesCannotReduce :: Kind ()
                             -> Normalized ClosedTypeG
                             -> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce :: Kind () -> Normalized ClosedTypeG -> ExceptT TestFail Quote ()
prop_normalTypesCannotReduce Kind ()
k (Normalized ClosedTypeG
tyG) =
  Bool -> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe ClosedTypeG -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe ClosedTypeG -> Bool) -> Maybe ClosedTypeG -> Bool
forall a b. (a -> b) -> a -> b
$ ClosedTypeG -> Maybe ClosedTypeG
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG ClosedTypeG
tyG) (ExceptT TestFail Quote () -> ExceptT TestFail Quote ())
-> ExceptT TestFail Quote () -> ExceptT TestFail Quote ()
forall a b. (a -> b) -> a -> b
$
    Ctrex -> ExceptT TestFail Quote ()
throwCtrex (Kind () -> ClosedTypeG -> Ctrex
CtrexNormalTypesCannotReduce Kind ()
k ClosedTypeG
tyG)

-- * Test failures

-- NOTE: a test may fail for several reasons:
--       - we encounter an error in the generator;
--       - we encounter an error while type checking Plutus terms;
--       - we encounter an error while converting to deBruijn notation;
--       - we encounter an error while running the Agda terms;
--       - we found a counter-example.
--
-- This is distinction is not strictly enforced as ultimately
-- everything leads to a counter-example of some kind

data TestFail
  = GenError GenError
  | TypeError
    (TypeError
      (Term TyName Name DefaultUni DefaultFun ())
      DefaultUni
      DefaultFun
      ())
  | AgdaErrorP ()
  | FVErrorP FreeVariableError
  | CkP (CkEvaluationException DefaultUni DefaultFun)
  | UCekP (U.CekEvaluationException Name DefaultUni DefaultFun)
  | Ctrex Ctrex

data Ctrex
  = CtrexNormalizeConvertCommuteTypes
    (Kind ())
    ClosedTypeG
    (Type TyName DefaultUni ())
    (Type TyName DefaultUni ())
  | CtrexNormalTypesCannotReduce
    (Kind ())
    ClosedTypeG
  | CtrexKindCheckFail
    (Kind ())
    ClosedTypeG
  | CtrexKindPreservationFail
    (Kind ())
    ClosedTypeG
  | CtrexKindMismatch
    (Kind ())
    ClosedTypeG
    (Kind ())
    (Kind ())
  | CtrexTypeNormalizationFail
    (Kind ())
    ClosedTypeG
  | CtrexTypeNormalizationMismatch
    (Kind ())
    ClosedTypeG
    (Type TyName DefaultUni ())
    (Type TyName DefaultUni ())
  | CtrexTypeCheckFail
    ClosedTypeG
    ClosedTermG
  | CtrexTypePreservationFail
    ClosedTypeG
    ClosedTermG
    (Term TyName Name DefaultUni DefaultFun ())
    (Term TyName Name DefaultUni DefaultFun ())
  | CtrexTermEvaluationFail
    String
    ClosedTypeG
    ClosedTermG
  | CtrexTermEvaluationMismatch
    ClosedTypeG
    ClosedTermG
    [(String,Term TyName Name DefaultUni DefaultFun ())]
  | CtrexUntypedTermEvaluationMismatch
    ClosedTypeG
    ClosedTermG
    [(String,U.Term Name DefaultUni DefaultFun ())]

instance Show TestFail where
  show :: TestFail -> String
show (TypeError TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
e)  = String
"type error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
-> String
forall a. Show a => a -> String
show TypeError
  (Term TyName Name DefaultUni DefaultFun ())
  DefaultUni
  DefaultFun
  ()
e
  show (GenError GenError
e)   = String
"generator error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GenError -> String
forall a. Show a => a -> String
show GenError
e
  show (Ctrex Ctrex
e)      = String
"counter example error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctrex -> String
forall a. Show a => a -> String
show Ctrex
e
  show (AgdaErrorP ()
e) = String
"agda error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ () -> String
forall a. Show a => a -> String
show ()
e
  show (FVErrorP FreeVariableError
e)   = String
"free variable error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FreeVariableError -> String
forall a. Show a => a -> String
show FreeVariableError
e
  show (CkP CkEvaluationException DefaultUni DefaultFun
e)        = String
"CK error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CkEvaluationException DefaultUni DefaultFun -> String
forall a. Show a => a -> String
show CkEvaluationException DefaultUni DefaultFun
e
  show (UCekP CekEvaluationException Name DefaultUni DefaultFun
e)      = String
"UCEK error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CekEvaluationException Name DefaultUni DefaultFun -> String
forall a. Show a => a -> String
show CekEvaluationException Name DefaultUni DefaultFun
e

instance Show Ctrex where
  show :: Ctrex -> String
show (CtrexNormalizeConvertCommuteTypes Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2) =
    String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
      String
tpl
      (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
      (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
      (Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty1))
      (Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty2))
    where
      tpl :: String
tpl = [String] -> String
unlines
            [ String
"Counterexample found: %s :: %s"
            , String
"- convert then normalize gives %s"
            , String
"- normalize then convert gives %s"
            ]

  show (CtrexNormalTypesCannotReduce Kind ()
k ClosedTypeG
tyG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
    where
      tpl :: String
tpl = String
"Counterexample found: normal type %s of kind %s can reduce."

  show (CtrexKindCheckFail Kind ()
k ClosedTypeG
tyG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
    where
      tpl :: String
tpl = String
"Counterexample found (kind check fail): %s :: %s"
  show (CtrexKindPreservationFail Kind ()
k ClosedTypeG
tyG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
    where
      tpl :: String
tpl = String
"Counterexample found (kind preservation fail): %s :: %s"
  show (CtrexKindMismatch Kind ()
k ClosedTypeG
tyG Kind ()
k' Kind ()
k'') =
    String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
      String
tpl
      (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
      (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
      (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k'))
      (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k''))
    where
      tpl :: String
tpl = [String] -> String
unlines
            [ String
"Counterexample found: %s :: %s"
            , String
"- inferer1 gives %s"
            , String
"- inferer2 gives %s"
            ]
  show (CtrexTypeNormalizationFail Kind ()
k ClosedTypeG
tyG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
    where
      tpl :: String
tpl = String
"Counterexample found (type normalisation fail): %s :: %s"
  show (CtrexTypeNormalizationMismatch Kind ()
k ClosedTypeG
tyG Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
ty2) =
    String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf
      String
tpl
      (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
      (Doc Any -> String
forall a. Show a => a -> String
show (Kind () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Kind () -> Doc ann
pretty Kind ()
k))
      (Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty1))
      (Doc Any -> String
forall a. Show a => a -> String
show (Type TyName DefaultUni () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Type TyName DefaultUni () -> Doc ann
pretty Type TyName DefaultUni ()
ty2))
    where
      tpl :: String
tpl = [String] -> String
unlines
            [ String
"Counterexample found: %s :: %s"
            , String
"- normalizer1 gives %s"
            , String
"- normalizer2 gives %s"
            ]
  show (CtrexTypeCheckFail ClosedTypeG
tyG ClosedTermG
tmG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
    where
      tpl :: String
tpl = String
"Counterexample found (typecheck fail): %s :: %s"
  show (CtrexTermEvaluationFail String
s ClosedTypeG
tyG ClosedTermG
tmG) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG)
    where
      tpl :: String
tpl = String
"Counterexample found (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" term evaluation fail): %s :: %s"
  show (CtrexTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String, Term TyName Name DefaultUni DefaultFun ())]
tms) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, Term TyName Name DefaultUni DefaultFun ())] -> String
forall {a}. Pretty a => [(String, a)] -> String
results [(String, Term TyName Name DefaultUni DefaultFun ())]
tms
    where
      tpl :: String
tpl = String
"TypedTermEvaluationMismatch\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Counterexample found: %s :: %s\n"
      results :: [(String, a)] -> String
results ((String
s,a
t):[(String, a)]
ts) = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" evaluation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, a)] -> String
results [(String, a)]
ts
      results []         = String
""
  show (CtrexUntypedTermEvaluationMismatch ClosedTypeG
tyG ClosedTermG
tmG [(String, Term Name DefaultUni DefaultFun ())]
tms) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, Term Name DefaultUni DefaultFun ())] -> String
forall {a}. Pretty a => [(String, a)] -> String
results [(String, Term Name DefaultUni DefaultFun ())]
tms
    where
      tpl :: String
tpl = String
"UntypedTermEvaluationMismatch\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Counterexample found: %s :: %s\n"
      results :: [(String, a)] -> String
results ((String
s,a
t):[(String, a)]
ts) = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" evaluation: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, a)] -> String
results [(String, a)]
ts
      results []         = String
""
  show (CtrexTypePreservationFail ClosedTypeG
tyG ClosedTermG
tmG Term TyName Name DefaultUni DefaultFun ()
tm1 Term TyName Name DefaultUni DefaultFun ()
tm2) =
    String -> String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
tpl (ClosedTermG -> String
forall a. Show a => a -> String
show ClosedTermG
tmG) (ClosedTypeG -> String
forall a. Show a => a -> String
show ClosedTypeG
tyG) (Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name DefaultUni DefaultFun () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Term TyName Name DefaultUni DefaultFun () -> Doc ann
pretty Term TyName Name DefaultUni DefaultFun ()
tm1)) (Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name DefaultUni DefaultFun () -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Term TyName Name DefaultUni DefaultFun () -> Doc ann
pretty Term TyName Name DefaultUni DefaultFun ()
tm2))
    where
      tpl :: String
tpl = [String] -> String
unlines
            [ String
"Counterexample found: %s :: %s"
            , String
"before evaluation: %s"
            , String
"after evaluation:  %s"
            ]

-- | Throw a counter-example.
throwCtrex :: Ctrex -> ExceptT TestFail Quote ()
throwCtrex :: Ctrex -> ExceptT TestFail Quote ()
throwCtrex Ctrex
ctrex = TestFail -> ExceptT TestFail Quote ()
forall a. TestFail -> ExceptT TestFail Quote a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Ctrex -> TestFail
Ctrex Ctrex
ctrex)

-- |Stream of type names t0, t1, t2, ..
tynames :: Stream.Stream Text.Text
tynames :: Stream Text
tynames = Text -> Stream Text
mkTextNameStream Text
"t"

-- |Stream of names x0, x1, x2, ..
names :: Stream.Stream Text.Text
names :: Stream Text
names = Text -> Stream Text
mkTextNameStream Text
"x"

-- | given a prop, generate one test
packAssertion :: (Show e) => (t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion :: forall e t a.
Show e =>
(t -> a -> ExceptT e Quote ()) -> t -> a -> Assertion
packAssertion t -> a -> ExceptT e Quote ()
f t
t a
a =
  case Quote (Either e ()) -> Either e ()
forall a. Quote a -> a
runQuote (Quote (Either e ()) -> Either e ())
-> (ExceptT e Quote () -> Quote (Either e ()))
-> ExceptT e Quote ()
-> Either e ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT e Quote () -> Quote (Either e ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT e Quote () -> Either e ())
-> ExceptT e Quote () -> Either e ()
forall a b. (a -> b) -> a -> b
$ t -> a -> ExceptT e Quote ()
f t
t a
a of
    Left  e
e -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure (String -> Assertion) -> String -> Assertion
forall a b. (a -> b) -> a -> b
$ e -> String
forall a. Show a => a -> String
show e
e
    Right ()
_ -> () -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | generate examples using `search'` and then generate one big test
-- that applies the given test to each of them.

bigTest :: (Check t a, Enumerable a)
        => String -> t -> (t -> a -> Assertion) -> TestTree
bigTest :: forall t a.
(Check t a, Enumerable a) =>
String -> t -> (t -> a -> Assertion) -> TestTree
bigTest String
s t
t t -> a -> Assertion
f = (GenMode -> TestTree) -> TestTree
forall v. IsOption v => (v -> TestTree) -> TestTree
askOption ((GenMode -> TestTree) -> TestTree)
-> (GenMode -> TestTree) -> TestTree
forall a b. (a -> b) -> a -> b
$ \ GenMode
genMode -> (GenDepth -> TestTree) -> TestTree
forall v. IsOption v => (v -> TestTree) -> TestTree
askOption ((GenDepth -> TestTree) -> TestTree)
-> (GenDepth -> TestTree) -> TestTree
forall a b. (a -> b) -> a -> b
$ \ GenDepth
genDepth -> String -> IO String -> TestTree
testCaseInfo String
s (IO String -> TestTree) -> IO String -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  [a]
as <- Options -> Int -> (a -> Cool) -> IO [a]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [a]
search' (GenMode -> Options
unGenMode GenMode
genMode) (GenDepth -> Int
unGenDepth GenDepth
genDepth) (\a
a ->  t -> a -> Cool
forall t a. Check t a => t -> a -> Cool
check t
t a
a)
  [()]
_  <- (a -> Assertion) -> [a] -> IO [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (t -> a -> Assertion
f t
t) [a]
as
  String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as)