-- editorconfig-checker-disable-file
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeOperators     #-}

module Evaluation.Golden
    ( test_golden
    , namesAndTests
    ) where

import Prelude hiding (even)

import PlutusCore.StdLib.Data.Bool
import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.Nat
import PlutusCore.StdLib.Data.ScottList
import PlutusCore.StdLib.Meta
import PlutusCore.StdLib.Meta.Data.Tuple
import PlutusCore.StdLib.Type

import PlutusCore
import PlutusCore.Compiler.Erase
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Generators.Hedgehog.Interesting
import PlutusCore.MkPlc
import PlutusCore.Pretty
import UntypedPlutusCore.Evaluation.Machine.Cek

import Data.Bifunctor
import Data.ByteString.Lazy qualified as BSL
import Data.Text (Text)
import Data.Text.Encoding (encodeUtf8)
import Test.Tasty
import Test.Tasty.Golden

-- (con integer)
integer :: uni `HasTypeLevel` Integer => Type TyName uni ()
integer :: forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()

-- (con string)
string :: uni `HasTypeLevel` Text => Type TyName uni ()
string :: forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Text ()

evenAndOdd :: uni `HasTypeAndTermLevel` Bool => Tuple (Term TyName Name uni fun) uni ()
evenAndOdd :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Bool =>
Tuple (Term TyName Name uni fun) uni ()
evenAndOdd = Quote (Tuple (Term TyName Name uni fun) uni ())
-> Tuple (Term TyName Name uni fun) uni ()
forall a. Quote a -> a
runQuote (Quote (Tuple (Term TyName Name uni fun) uni ())
 -> Tuple (Term TyName Name uni fun) uni ())
-> Quote (Tuple (Term TyName Name uni fun) uni ())
-> Tuple (Term TyName Name uni fun) uni ()
forall a b. (a -> b) -> a -> b
$ do
    let nat :: Type TyName uni ()
nat = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
natData

    Name
evenn <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"even"
    Name
oddd  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"odd"

    let eoFunc :: Term TyName Name uni fun ()
-> Name -> m (Term TyName Name uni fun ())
eoFunc Term TyName Name uni fun ()
b Name
recc = do
          Name
n <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"n"
          Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun () -> m (Term TyName Name uni fun ()))
-> Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$
              ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
n Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
              ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
n)) Type TyName uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Bool =>
Type tyname uni ()
bool) Term TyName Name uni fun ()
b) (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
recc

    FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
evenF <- ()
-> Name
-> FunctionType TyName uni ()
-> Term TyName Name uni fun ()
-> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
FunctionDef () Name
evenn (()
-> Type TyName uni ()
-> Type TyName uni ()
-> FunctionType TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
FunctionType () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat Type TyName uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Bool =>
Type tyname uni ()
bool) (Term TyName Name uni fun ()
 -> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
-> QuoteT Identity (Term TyName Name uni fun ())
-> QuoteT
     Identity
     (FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ()
-> Name -> QuoteT Identity (Term TyName Name uni fun ())
forall {m :: * -> *} {uni :: * -> *} {fun}.
(MonadQuote m,
 KnownTypeAst Void uni (ElaborateBuiltin uni Bool)) =>
Term TyName Name uni fun ()
-> Name -> m (Term TyName Name uni fun ())
eoFunc Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true Name
oddd
    FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
oddF  <- ()
-> Name
-> FunctionType TyName uni ()
-> Term TyName Name uni fun ()
-> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
FunctionDef () Name
oddd  (()
-> Type TyName uni ()
-> Type TyName uni ()
-> FunctionType TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
FunctionType () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat Type TyName uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Bool =>
Type tyname uni ()
bool) (Term TyName Name uni fun ()
 -> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
-> QuoteT Identity (Term TyName Name uni fun ())
-> QuoteT
     Identity
     (FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ()
-> Name -> QuoteT Identity (Term TyName Name uni fun ())
forall {m :: * -> *} {uni :: * -> *} {fun}.
(MonadQuote m,
 KnownTypeAst Void uni (ElaborateBuiltin uni Bool)) =>
Term TyName Name uni fun ()
-> Name -> m (Term TyName Name uni fun ())
eoFunc Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
false Name
evenn

    ()
-> Term TyName Name uni fun ()
-> [FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()]
-> Quote (Tuple (Term TyName Name uni fun) uni ())
forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann
-> [FunctionDef term TyName Name uni fun ann]
-> Quote (Tuple term uni ann)
getMutualFixOf () (Integer
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> term ()
fixN Integer
2 Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fixBy) [FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
evenF, FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
oddF]

even :: uni `HasTypeAndTermLevel` Bool => Term TyName Name uni fun ()
even :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Bool =>
Term TyName Name uni fun ()
even = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Int
-> Tuple (Term TyName Name uni fun) uni ()
-> Quote (Term TyName Name uni fun ())
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> Int -> Tuple term uni ann -> m (term ann)
tupleTermAt () Int
0 Tuple (Term TyName Name uni fun) uni ()
forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Bool =>
Tuple (Term TyName Name uni fun) uni ()
evenAndOdd

evenAndOddList :: Tuple (Term TyName Name uni fun) uni ()
evenAndOddList :: forall (uni :: * -> *) fun. Tuple (Term TyName Name uni fun) uni ()
evenAndOddList = Quote (Tuple (Term TyName Name uni fun) uni ())
-> Tuple (Term TyName Name uni fun) uni ()
forall a. Quote a -> a
runQuote (Quote (Tuple (Term TyName Name uni fun) uni ())
 -> Tuple (Term TyName Name uni fun) uni ())
-> Quote (Tuple (Term TyName Name uni fun) uni ())
-> Tuple (Term TyName Name uni fun) uni ()
forall a b. (a -> b) -> a -> b
$ do
    let list :: Type TyName uni ()
list = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
listData
        nat :: Type TyName uni ()
nat  = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
natData
        listNat :: Type TyName uni ()
listNat = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
list Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat

    Name
evenn <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"even"
    Name
oddd  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"odd"

    let eoFunc :: Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
eoFunc Term TyName Name uni fun ()
recc = do
          Name
l <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"l"
          Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun () -> m (Term TyName Name uni fun ()))
-> Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$
              ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
l Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
              ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (
                  ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
l)) Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat)
                  (()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst() Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
nil Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat))
              Term TyName Name uni fun ()
recc

    FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
evenF <- ()
-> Name
-> FunctionType TyName uni ()
-> Term TyName Name uni fun ()
-> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
FunctionDef () Name
evenn (()
-> Type TyName uni ()
-> Type TyName uni ()
-> FunctionType TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
FunctionType () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat) (Term TyName Name uni fun ()
 -> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
-> QuoteT Identity (Term TyName Name uni fun ())
-> QuoteT
     Identity
     (FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"head"
        Name
t <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"tail"
        Term TyName Name uni fun ()
-> QuoteT Identity (Term TyName Name uni fun ())
forall {m :: * -> *} {uni :: * -> *} {fun}.
MonadQuote m =>
Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
eoFunc (Term TyName Name uni fun ()
 -> QuoteT Identity (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> QuoteT Identity (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$
            ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
h Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
t Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
cons Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat) (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
h)) (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
oddd) (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
t)

    FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
oddF <- ()
-> Name
-> FunctionType TyName uni ()
-> Term TyName Name uni fun ()
-> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
FunctionDef () Name
oddd (()
-> Type TyName uni ()
-> Type TyName uni ()
-> FunctionType TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
FunctionType () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat) (Term TyName Name uni fun ()
 -> FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
-> QuoteT Identity (Term TyName Name uni fun ())
-> QuoteT
     Identity
     (FunctionDef (Term TyName Name uni fun) TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"head"
        Name
t <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"tail"
        Term TyName Name uni fun ()
-> QuoteT Identity (Term TyName Name uni fun ())
forall {m :: * -> *} {uni :: * -> *} {fun}.
MonadQuote m =>
Term TyName Name uni fun () -> m (Term TyName Name uni fun ())
eoFunc (Term TyName Name uni fun ()
 -> QuoteT Identity (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> QuoteT Identity (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$
            ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
h Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
t Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
listNat (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
evenn) (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
t)

    ()
-> Term TyName Name uni fun ()
-> [FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()]
-> Quote (Tuple (Term TyName Name uni fun) uni ())
forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann
-> [FunctionDef term TyName Name uni fun ann]
-> Quote (Tuple term uni ann)
getMutualFixOf () (Integer
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> term ()
fixN Integer
2 Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fixBy) [FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
evenF, FunctionDef (Term TyName Name uni fun) TyName Name uni fun ()
oddF]

evenList :: Term TyName Name uni fun ()
evenList :: forall (uni :: * -> *) fun. Term TyName Name uni fun ()
evenList = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Int
-> Tuple (Term TyName Name uni fun) uni ()
-> Quote (Term TyName Name uni fun ())
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> Int -> Tuple term uni ann -> m (term ann)
tupleTermAt () Int
0 Tuple (Term TyName Name uni fun) uni ()
forall (uni :: * -> *) fun. Tuple (Term TyName Name uni fun) uni ()
evenAndOddList

smallNatList :: Term TyName Name uni fun ()
smallNatList :: forall (uni :: * -> *) fun. Term TyName Name uni fun ()
smallNatList = Type TyName uni ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Type TyName uni () -> [term ()] -> term ()
metaListToScottList Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
nat [Term TyName Name uni fun ()]
nats where
    nats :: [Term TyName Name uni fun ()]
nats = (Integer -> Term TyName Name uni fun ())
-> [Integer] -> [Term TyName Name uni fun ()]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map Integer -> Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat [Integer
1,Integer
2,Integer
3]
    nat :: Type TyName uni ()
nat = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
natData

polyError :: Term TyName Name uni fun ()
polyError :: forall (uni :: * -> *) fun. Term TyName Name uni fun ()
polyError = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Type TyName uni () -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)

-- | For checking that evaluating a term to a non-constant results in all remaining variables
-- being instantiated.
closure :: uni `HasTypeAndTermLevel` Integer => Term TyName Name uni fun ()
closure :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Integer =>
Term TyName Name uni fun ()
closure = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
i <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i"
    Name
j <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"j"
    Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
i Type TyName uni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
j Type TyName uni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i)
        (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1

{- Tests for evaluation of builtins.  The main point of these is to check that
   interleaving of term and type arguments is correct, but a number of other
   tests checking that ill-typed builtins execute successfully (because types
   are ignored at runtime) are included.  At the moment the only polymorphic
   builtin we have is ifThenElse.

   We test a number of terms to check whether they typecheck and whether they
   evaluate without error.  There are four possible outcomes:

     * The term typechecks and evaluates successfully
     * The term typechecks and evaluation fails
     * The term is ill-typed but still evaluates successfully
     * The term is ill-typed and evaluation fails

   We'll denote these outcomes by WellTypedRuns, WellTypedFails, IllTypedRuns, and IllTypedFails
   respectively; each test is labelled with one of these.
-}

-- Various components that we'll use to build larger terms for testing

lte :: Term TyName Name DefaultUni DefaultFun ()
lte :: Term TyName Name DefaultUni DefaultFun ()
lte = () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
LessThanEqualsInteger

eleven :: Term TyName Name DefaultUni DefaultFun ()
eleven :: Term TyName Name DefaultUni DefaultFun ()
eleven = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
11

twentytwo :: Term TyName Name DefaultUni DefaultFun ()
twentytwo :: Term TyName Name DefaultUni DefaultFun ()
twentytwo = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
22

stringResultTrue :: Term TyName Name DefaultUni DefaultFun ()
stringResultTrue :: Term TyName Name DefaultUni DefaultFun ()
stringResultTrue = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"11 <= 22"

stringResultFalse :: Term TyName Name DefaultUni DefaultFun ()
stringResultFalse :: Term TyName Name DefaultUni DefaultFun ()
stringResultFalse = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"¬(11 <= 22)"

-- 11 <= 22
lteExpr :: Term TyName Name DefaultUni DefaultFun ()
lteExpr :: Term TyName Name DefaultUni DefaultFun ()
lteExpr = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
lte [Term TyName Name DefaultUni DefaultFun ()
eleven, Term TyName Name DefaultUni DefaultFun ()
twentytwo]


-- Various combinations of (partial) instantiation/application for ifThenElse

-- (builtin ifThenElse) : WellTypedRuns
ite :: Term TyName Name DefaultUni DefaultFun ()
ite :: Term TyName Name DefaultUni DefaultFun ()
ite = () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
IfThenElse

-- { (builtin ifThenElse) t }
iteAt :: Type TyName DefaultUni () -> Term TyName Name DefaultUni DefaultFun ()
iteAt :: Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
iteAt = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
ite

-- [ (builtin ifThenElse) (11<=22) ] : IllTypedFails (ifThenElse isn't
-- instantiated: type expected, term supplied.)
iteUninstantiatedWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedWithCond  = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
ite Term TyName Name DefaultUni DefaultFun ()
lteExpr

-- (builtin ifThenElse) (11<=22) "11 <= 22" "¬(11<=22)" : IllTypedFails (no
-- instantiation)
iteUninstantiatedFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedFullyApplied = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
ite [Term TyName Name DefaultUni DefaultFun ()
lteExpr, Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- { (builtin ifThenElse) (con integer) } : WellTypedRuns
iteAtInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtInteger = Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
iteAt Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer

-- [ { (builtin ifThenElse) (con integer) } (11<=22)] : WellTypedRuns
iteAtIntegerWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWithCond = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtInteger Term TyName Name DefaultUni DefaultFun ()
lteExpr

-- [ { (builtin ifThenElse) (con integer) } "11 <= 22" "¬(11<=22)" ] :
-- IllTypedRuns.  This is ill-typed because the first term argument is a string
-- and a boolean is expected.
-- At execution time the default unlifting mode (Deferred) dictates
-- that builtin has to be saturated before it can runtime check for its types.
-- This is contrary to the older unlfiting mode (Immediate)
-- the builtin application machinery unlifts an argument and checks its type the moment it gets it,
-- without waiting for full saturation.
iteAtIntegerWrongCondTypeUnSat :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeUnSat :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeUnSat = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
iteAtInteger [Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- [ { (builtin ifThenElse) (con integer) } "11 <= 22" "¬(11<=22)" "¬(11<=22)" ] :
-- IllTypedFails. This is ill-typed because the first term argument is a string
-- and a boolean is expected. At execution time,
-- the default unlifting mode (Deferred) can finally check for the types of the arguments to
-- builtin function, since the builtin application is fully saturated. The older unlifting
-- mode would also fail, but earlier before the builtin call got even saturated, see `iteAtIntegerWrongCondTypeUnSat`.
iteAtIntegerWrongCondTypeSat :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeSat :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeSat = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
iteAtInteger [Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- [ { (builtin ifThenElse) (con integer) } (11<=22) "11 <= 22" "¬(11<=22)" ] :
-- IllTypedRuns.  We're instantiating at `integer` but returning a string: at
-- execution time we only check that type instantiations and term arguments are
-- correctly interleaved, not that instantiations are correct.
iteAtIntegerFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerFullyApplied = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWithCond [Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- [ (builtin divideInteger) 1 0 ] : WellTypedFails. Division by zero.
diFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
diFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
diFullyApplied = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
DivideInteger)
    [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
    , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
    ]

-- { (builtin ifThenElse) (con string) } : WellTypedRuns
iteAtString :: Term TyName Name DefaultUni DefaultFun ()
iteAtString :: Term TyName Name DefaultUni DefaultFun ()
iteAtString = Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
iteAt Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string

-- [ { (builtin ifThenElse) (con string) } (11<=22) ] : WellTypedRuns
iteAtStringWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCond = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtString Term TyName Name DefaultUni DefaultFun ()
lteExpr

-- [ { (builtin ifThenElse) (con string) } (11<=22) 33 "abc" ] : IllTypedRuns
-- This is ill-typed because the first branch is of type @integer@ and the second branch is of type
-- @string@. It still runs succefully, because even in typed world (the CK machine) we don't look
-- at types at runtime.
iteAtStringWithCondWithIntegerWithString :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCondWithIntegerWithString :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCondWithIntegerWithString = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCond
    [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
33
    , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"abc"
    ]

-- [ { (builtin ifThenElse)  (con string) } (11<=22) "11 <= 22" "¬(11<=22)" ] : WellTypedRuns
iteAtStringFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtStringFullyApplied = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCond [Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- { builtin ifThenElse (fun (con integer) (con integer)) } : WellTypedRuns
iteAtIntegerArrowInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger = Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
iteAt (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer)

-- [ { (builtin ifThenElse) (fun (con integer) (con integer)) } (11<=22) ] : WellTypedRuns
iteAtIntegerArrowIntegerWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerWithCond = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger Term TyName Name DefaultUni DefaultFun ()
lteExpr

-- [ { (builtin ifThenElse) (fun (con integer) (con integer)) } (11<=22) (11 *) (22 -)] :
-- WellTypedRuns (returns a function of type int -> int)
iteAtIntegerArrowIntegerApplied1 ::  Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied1 :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied1 =  Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
                                   Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger
                                   [ Term TyName Name DefaultUni DefaultFun ()
lteExpr
                                   , ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
MultiplyInteger) Term TyName Name DefaultUni DefaultFun ()
eleven
                                   , ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger) Term TyName Name DefaultUni DefaultFun ()
twentytwo
                                   ]

-- [ { (builtin ifThenElse) (fun (con integer) (con integer)) } (11<=22) (*) (-)] :
-- IllTypedRuns (int -> int -> int instead of int -> int).
iteAtIntegerArrowIntegerApplied2 ::  Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied2 :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied2 =  Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
                                    Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger
                                    [ Term TyName Name DefaultUni DefaultFun ()
lteExpr
                                    , () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
MultiplyInteger
                                    , () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger
                                    ]

-- [ { (builtin ifThenElse) (fun (con integer) (con integer)) } (11<=22) (11 *) (22 -) 22] :
-- WellTypedRuns (ifThenElse returns a function which is then applied to a constant).
iteAtIntegerArrowIntegerAppliedApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerAppliedApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerAppliedApplied =  ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied1 Term TyName Name DefaultUni DefaultFun ()
twentytwo

-- { (builtin ifThenElse) (lam a . a -> a) } : IllTypedRuns.
-- Evaluation should succeed, but typechecking should fail with a kind error.
-- The built-in function machinery does allow builtins which are polymorphic
-- over higher-kinded types, but `ifThenElse` can only be instantiated with
-- types of kind *.
iteAtHigherKind :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKind :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKind = Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
iteAt (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) Type TyName DefaultUni ()
forall {uni :: * -> *}. Type TyName uni ()
aArrowA)
    where a :: TyName
a = Name -> TyName
TyName (Text -> Unique -> Name
Name Text
"a" (Int -> Unique
Unique Int
0))
          aArrowA :: Type TyName uni ()
aArrowA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)

-- [ { (builtin ifThenElse) (lam a . a -> a) } (11<=22) ] : IllTypedRuns
-- (illegal kind)
iteAtHigherKindWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindWithCond :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindWithCond = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKind Term TyName Name DefaultUni DefaultFun ()
lteExpr

-- [ {(builtin ifThenElse) (lam a . a -> a) } (11<=22) "11 <= 22" "¬(11<=22) ]" :
-- IllTypedRuns (illegal kind)
iteAtHigherKindFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindFullyApplied :: Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindFullyApplied = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKind Term TyName Name DefaultUni DefaultFun ()
lteExpr) [Term TyName Name DefaultUni DefaultFun ()
stringResultTrue, Term TyName Name DefaultUni DefaultFun ()
stringResultFalse]

-- { {(builtin ifThenElse) integer} integer } : IllTypedFails (instantiated twice).
iteAtIntegerAtInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerAtInteger :: Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerAtInteger = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
iteAtInteger Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer

-- { [ { (builtin ifThenElse) integer } (11<=22)] integer } : IllTypedFails
-- (term expected, type supplied).
iteTypeTermType :: Term TyName Name DefaultUni DefaultFun ()
iteTypeTermType :: Term TyName Name DefaultUni DefaultFun ()
iteTypeTermType = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWithCond Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string


-- Various attempts to instantiate the MultiplyInteger builtin. This is not
-- polymorphic, so most should fail (and we're checking that they _do_ fail).

-- (builtin multiplyInteger) (not tested)
mul ::  Term TyName Name DefaultUni DefaultFun ()
mul :: Term TyName Name DefaultUni DefaultFun ()
mul = () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
MultiplyInteger

-- [ [ (builtin multiplyInteger) 11 ] 22 ] : WellTypedRuns
mulOK :: Term TyName Name DefaultUni DefaultFun ()
mulOK :: Term TyName Name DefaultUni DefaultFun ()
mulOK = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
mul Term TyName Name DefaultUni DefaultFun ()
eleven) Term TyName Name DefaultUni DefaultFun ()
twentytwo

-- [ [ { (builtin multiplyInteger) string } 11 ] 22 ]: IllTypedFails
mulInstError1 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError1 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError1 = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
mul Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string) Term TyName Name DefaultUni DefaultFun ()
eleven) Term TyName Name DefaultUni DefaultFun ()
twentytwo

-- [ [ { (builtin multiplyInteger) 11 ] string } 22 ]: IllTypedFails
mulInstError2 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError2 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError2 = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
mul Term TyName Name DefaultUni DefaultFun ()
eleven) Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string) Term TyName Name DefaultUni DefaultFun ()
twentytwo

-- { [ [ (builtin multiplyInteger) 11 ] 22 ] string } : IllTypedFails
mulInstError3 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError3 :: Term TyName Name DefaultUni DefaultFun ()
mulInstError3 = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
mul Term TyName Name DefaultUni DefaultFun ()
eleven) Term TyName Name DefaultUni DefaultFun ()
twentytwo) Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string

tag1 :: Term TyName Name DefaultUni DefaultFun ()
tag1 :: Term TyName Name DefaultUni DefaultFun ()
tag1 = ()
-> Type TyName DefaultUni ()
-> Word64
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr () (() -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () [[Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer], [Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string]]) Word64
0 [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1]

tag2 :: Term TyName Name DefaultUni DefaultFun ()
tag2 :: Term TyName Name DefaultUni DefaultFun ()
tag2 = ()
-> Type TyName DefaultUni ()
-> Word64
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr () (() -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () [[Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer], [Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string]]) Word64
1 [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"hello"]

tagProd1 :: Term TyName Name DefaultUni DefaultFun ()
tagProd1 :: Term TyName Name DefaultUni DefaultFun ()
tagProd1 = ()
-> Type TyName DefaultUni ()
-> Word64
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr () (() -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () [[Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer, Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer, Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer], [Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string]]) Word64
0
    [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
4]

case1 :: Term TyName Name DefaultUni DefaultFun ()
case1 :: Term TyName Name DefaultUni DefaultFun ()
case1 = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
    let branch1 :: Term TyName Name DefaultUni fun ()
branch1 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (() -> Name -> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
a)
        branch2 :: Term TyName Name DefaultUni fun ()
branch2 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2)
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer Term TyName Name DefaultUni DefaultFun ()
tag1 [Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch1, Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch2]

case2 :: Term TyName Name DefaultUni DefaultFun ()
case2 :: Term TyName Name DefaultUni DefaultFun ()
case2 = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
    let branch1 :: Term TyName Name DefaultUni fun ()
branch1 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (() -> Name -> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
a)
        branch2 :: Term TyName Name DefaultUni fun ()
branch2 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2)
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer Term TyName Name DefaultUni DefaultFun ()
tag2 [Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch1, Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch2]

case3 :: Term TyName Name DefaultUni DefaultFun ()
case3 :: Term TyName Name DefaultUni DefaultFun ()
case3 = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
    let branch1 :: Term TyName Name DefaultUni fun ()
branch1 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"no")
        branch2 :: Term TyName Name DefaultUni fun ()
branch2 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string (() -> Name -> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
a)
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string Term TyName Name DefaultUni DefaultFun ()
tag1 [Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch1, Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch2]

case4 :: Term TyName Name DefaultUni DefaultFun ()
case4 :: Term TyName Name DefaultUni DefaultFun ()
case4 = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
    let branch1 :: Term TyName Name DefaultUni fun ()
branch1 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"no")
        branch2 :: Term TyName Name DefaultUni fun ()
branch2 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string (() -> Name -> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
a)
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string Term TyName Name DefaultUni DefaultFun ()
tag2 [Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch1, Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch2]

caseProd1 :: Term TyName Name DefaultUni DefaultFun ()
caseProd1 :: Term TyName Name DefaultUni DefaultFun ()
caseProd1 = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
    Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
    Name
c <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"c"
    let branch1 :: Term TyName Name DefaultUni DefaultFun ()
branch1 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
b Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
c Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                    Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger) [
                      Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger) [() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
a, () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
b]
                      , () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
c
                      ]
        branch2 :: Term TyName Name DefaultUni fun ()
branch2 = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
a Type TyName DefaultUni ()
forall (uni :: * -> *). HasTypeLevel uni Text => Type TyName uni ()
string (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2)
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer Term TyName Name DefaultUni DefaultFun ()
tagProd1 [Term TyName Name DefaultUni DefaultFun ()
branch1, Term TyName Name DefaultUni DefaultFun ()
forall {fun}. Term TyName Name DefaultUni fun ()
branch2]

caseNoBranch :: Term TyName Name DefaultUni DefaultFun ()
caseNoBranch :: Term TyName Name DefaultUni DefaultFun ()
caseNoBranch = ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer Term TyName Name DefaultUni DefaultFun ()
tag1 []

caseNonTag :: Term TyName Name DefaultUni DefaultFun ()
caseNonTag :: Term TyName Name DefaultUni DefaultFun ()
caseNonTag = ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case () Type TyName DefaultUni ()
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
integer (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1) []

-- | For testing that an accidental exception will get caught.
headSingletonException :: Term TyName Name DefaultUni DefaultFun ()
headSingletonException :: Term TyName Name DefaultUni DefaultFun ()
headSingletonException
    = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
HeadList) (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Bool ())
    (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> [Bool] -> Term TyName Name DefaultUni DefaultFun ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () [[Char] -> Bool
forall a. [Char] -> a
errorWithoutStackTrace [Char]
"catch me if you can" :: Bool]

-- Running the tests

goldenVsPretty :: PrettyPlc a => String -> String -> a -> TestTree
goldenVsPretty :: forall a. PrettyPlc a => [Char] -> [Char] -> a -> TestTree
goldenVsPretty [Char]
extn [Char]
name a
value =
    [Char] -> [Char] -> IO ByteString -> TestTree
goldenVsString [Char]
name ([Char]
"untyped-plutus-core/test/Evaluation/Golden/" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
extn) (IO ByteString -> TestTree) -> IO ByteString -> TestTree
forall a b. (a -> b) -> a -> b
$
        ByteString -> IO ByteString
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString)
-> (Doc Any -> ByteString) -> Doc Any -> IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
BSL.fromStrict (ByteString -> ByteString)
-> (Doc Any -> ByteString) -> Doc Any -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ByteString
encodeUtf8 (Text -> ByteString) -> (Doc Any -> Text) -> Doc Any -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> Text
forall ann. Doc ann -> Text
forall str ann. Render str => Doc ann -> str
render (Doc Any -> IO ByteString) -> Doc Any -> IO ByteString
forall a b. (a -> b) -> a -> b
$ a -> Doc Any
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcClassicSimple a
value

goldenVsEvaluatedCK :: String -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCK :: [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCK [Char]
name
    = [Char]
-> [Char]
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term Name DefaultUni DefaultFun ()))
     (Term Name DefaultUni DefaultFun ())
-> TestTree
forall a. PrettyPlc a => [Char] -> [Char] -> a -> TestTree
goldenVsPretty [Char]
".plc.golden" [Char]
name
    (Either
   (ErrorWithCause
      (EvaluationError (MachineError DefaultFun) CkUserError)
      (Term Name DefaultUni DefaultFun ()))
   (Term Name DefaultUni DefaultFun ())
 -> TestTree)
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Either
         (ErrorWithCause
            (EvaluationError (MachineError DefaultFun) CkUserError)
            (Term Name DefaultUni DefaultFun ()))
         (Term Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorWithCause
   (EvaluationError (MachineError DefaultFun) CkUserError)
   (Term TyName Name DefaultUni DefaultFun ())
 -> ErrorWithCause
      (EvaluationError (MachineError DefaultFun) CkUserError)
      (Term Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term TyName Name DefaultUni DefaultFun ()))
     (Term TyName Name DefaultUni DefaultFun ())
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term Name DefaultUni DefaultFun ()))
     (Term Name DefaultUni DefaultFun ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((Term TyName Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> ErrorWithCause
     (EvaluationError (MachineError DefaultFun) CkUserError)
     (Term TyName Name DefaultUni DefaultFun ())
-> ErrorWithCause
     (EvaluationError (MachineError DefaultFun) CkUserError)
     (Term Name DefaultUni DefaultFun ())
forall a b.
(a -> b)
-> ErrorWithCause
     (EvaluationError (MachineError DefaultFun) CkUserError) a
-> ErrorWithCause
     (EvaluationError (MachineError DefaultFun) CkUserError) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 ()
-> 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
    (Either
   (ErrorWithCause
      (EvaluationError (MachineError DefaultFun) CkUserError)
      (Term TyName Name DefaultUni DefaultFun ()))
   (Term TyName Name DefaultUni DefaultFun ())
 -> Either
      (ErrorWithCause
         (EvaluationError (MachineError DefaultFun) CkUserError)
         (Term Name DefaultUni DefaultFun ()))
      (Term Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Either
         (ErrorWithCause
            (EvaluationError (MachineError DefaultFun) CkUserError)
            (Term TyName Name DefaultUni DefaultFun ()))
         (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term Name DefaultUni DefaultFun ()))
     (Term Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term TyName Name 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

goldenVsEvaluatedCEK :: String -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCEK :: [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCEK [Char]
name
    = [Char]
-> [Char]
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
-> TestTree
forall a. PrettyPlc a => [Char] -> [Char] -> a -> TestTree
goldenVsPretty [Char]
".uplc.golden" [Char]
name
    (Either
   (CekEvaluationException Name DefaultUni DefaultFun)
   (Term Name DefaultUni DefaultFun ())
 -> TestTree)
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException Name DefaultUni DefaultFun)
         (Term Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ())
evaluateCekNoEmit MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
defaultCekParametersForTesting
    (Term Name DefaultUni DefaultFun ()
 -> Either
      (CekEvaluationException Name DefaultUni DefaultFun)
      (Term Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException Name DefaultUni DefaultFun)
     (Term Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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

runTypecheck
    :: Term TyName Name DefaultUni DefaultFun ()
    -> Either (Error DefaultUni DefaultFun ()) (Normalized (Type TyName DefaultUni ()))
runTypecheck :: Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
runTypecheck Term TyName Name DefaultUni DefaultFun ()
term =
  QuoteT
  (Either (Error DefaultUni DefaultFun ()))
  (Normalized (Type TyName DefaultUni ()))
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT
   (Either (Error DefaultUni DefaultFun ()))
   (Normalized (Type TyName DefaultUni ()))
 -> Either
      (Error DefaultUni DefaultFun ())
      (Normalized (Type TyName DefaultUni ())))
-> QuoteT
     (Either (Error DefaultUni DefaultFun ()))
     (Normalized (Type TyName DefaultUni ()))
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
forall a b. (a -> b) -> a -> b
$ do
    TypeCheckConfig DefaultUni DefaultFun
tcConfig <- ()
-> QuoteT
     (Either (Error DefaultUni DefaultFun ()))
     (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 ()
    TypeCheckConfig DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> QuoteT
     (Either (Error DefaultUni DefaultFun ()))
     (Normalized (Type TyName DefaultUni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferType TypeCheckConfig DefaultUni DefaultFun
tcConfig Term TyName Name DefaultUni DefaultFun ()
term

goldenVsTypechecked :: String -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypechecked :: [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypechecked [Char]
name = [Char]
-> [Char]
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
-> TestTree
forall a. PrettyPlc a => [Char] -> [Char] -> a -> TestTree
goldenVsPretty [Char]
".type.golden" [Char]
name (Either
   (Error DefaultUni DefaultFun ())
   (Normalized (Type TyName DefaultUni ()))
 -> TestTree)
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Either
         (Error DefaultUni DefaultFun ())
         (Normalized (Type TyName DefaultUni ())))
-> Term TyName Name DefaultUni DefaultFun ()
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
runTypecheck

goldenVsTypecheckedEvaluatedCK :: String -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypecheckedEvaluatedCK :: [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypecheckedEvaluatedCK [Char]
name Term TyName Name DefaultUni DefaultFun ()
term =
    -- The CK machine can evaluate an ill-typed term to a well-typed one, so we check
    -- that the term is well-typed before checking that the type of the result is the
    -- one stored in the golden file (we could simply check the two types for equality,
    -- but since we're doing golden testing in this file, why not do it here as well).
    case (Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (Normalized (Type TyName DefaultUni ()))
runTypecheck Term TyName Name DefaultUni DefaultFun ()
term, BuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (ErrorWithCause
        (EvaluationError (MachineError DefaultFun) CkUserError)
        (Term TyName Name 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 ()
term) of
        (Right Normalized (Type TyName DefaultUni ())
_, Right Term TyName Name DefaultUni DefaultFun ()
res) -> [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypechecked [Char]
name Term TyName Name DefaultUni DefaultFun ()
res
        (Either
   (Error DefaultUni DefaultFun ())
   (Normalized (Type TyName DefaultUni ())),
 Either
   (ErrorWithCause
      (EvaluationError (MachineError DefaultFun) CkUserError)
      (Term TyName Name DefaultUni DefaultFun ()))
   (Term TyName Name DefaultUni DefaultFun ()))
_                    -> [Char] -> [TestTree] -> TestTree
testGroup [Char]
name []

namesAndTests :: [(String, Term TyName Name DefaultUni DefaultFun ())]
namesAndTests :: [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTests =
   [ ([Char]
"even2", ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Bool =>
Term TyName Name uni fun ()
even (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ Integer -> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
2)
   , ([Char]
"even3", ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Bool =>
Term TyName Name uni fun ()
even (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ Integer -> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
3)
   , ([Char]
"evenList", ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
natSum (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term TyName Name uni fun ()
evenList Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term TyName Name uni fun ()
smallNatList)
   , ([Char]
"polyError", Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term TyName Name uni fun ()
polyError)
   , ([Char]
"polyErrorInst", ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term TyName Name uni fun ()
polyError (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()))
   , ([Char]
"closure", Term TyName Name DefaultUni DefaultFun ()
forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Integer =>
Term TyName Name uni fun ()
closure)
   , ([Char]
"ite", Term TyName Name DefaultUni DefaultFun ()
ite)
   , ([Char]
"iteUninstantiatedWithCond", Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedWithCond)
   , ([Char]
"iteUninstantiatedFullyApplied", Term TyName Name DefaultUni DefaultFun ()
iteUninstantiatedFullyApplied)
   , ([Char]
"iteAtInteger", Term TyName Name DefaultUni DefaultFun ()
iteAtInteger)
   , ([Char]
"iteAtIntegerWithCond", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWithCond)
   , ([Char]
"iteAtIntegerWrongCondTypeUnSat", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeUnSat)
   , ([Char]
"iteAtIntegerWrongCondTypeSat", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerWrongCondTypeSat)
   , ([Char]
"iteAtIntegerFullyApplied", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerFullyApplied)
   , ([Char]
"diFullyApplied", Term TyName Name DefaultUni DefaultFun ()
diFullyApplied)
   , ([Char]
"iteAtString", Term TyName Name DefaultUni DefaultFun ()
iteAtString)
   , ([Char]
"iteAtStringWithCond", Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCond)
   , ([Char]
"iteAtStringWithCondWithIntegerWithString", Term TyName Name DefaultUni DefaultFun ()
iteAtStringWithCondWithIntegerWithString)
   , ([Char]
"iteAtStringFullyApplied", Term TyName Name DefaultUni DefaultFun ()
iteAtStringFullyApplied)
   , ([Char]
"iteAtIntegerArrowInteger", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowInteger)
   , ([Char]
"iteAtIntegerArrowIntegerWithCond", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerWithCond)
   , ([Char]
"iteAtIntegerArrowIntegerApplied1", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied1)
   , ([Char]
"iteAtIntegerArrowIntegerApplied2", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerApplied2)
   , ([Char]
"iteAtIntegerArrowIntegerAppliedApplied", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerArrowIntegerAppliedApplied)
   , ([Char]
"iteAtHigherKind", Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKind)
   , ([Char]
"iteAtHigherKindWithCond", Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindWithCond)
   , ([Char]
"iteAtHigherKindFullyApplied", Term TyName Name DefaultUni DefaultFun ()
iteAtHigherKindFullyApplied)
   , ([Char]
"iteAtIntegerAtInteger", Term TyName Name DefaultUni DefaultFun ()
iteAtIntegerAtInteger)
   , ([Char]
"iteTypeTermType", Term TyName Name DefaultUni DefaultFun ()
iteTypeTermType)
   , ([Char]
"mulOK", Term TyName Name DefaultUni DefaultFun ()
mulOK)
   , ([Char]
"mulInstError1", Term TyName Name DefaultUni DefaultFun ()
mulInstError1)
   , ([Char]
"mulInstError2", Term TyName Name DefaultUni DefaultFun ()
mulInstError2)
   , ([Char]
"mulInstError3", Term TyName Name DefaultUni DefaultFun ()
mulInstError3)
   , ([Char]
"tag1", Term TyName Name DefaultUni DefaultFun ()
tag1)
   , ([Char]
"tag2", Term TyName Name DefaultUni DefaultFun ()
tag2)
   , ([Char]
"tagProd1", Term TyName Name DefaultUni DefaultFun ()
tagProd1)
   , ([Char]
"case1", Term TyName Name DefaultUni DefaultFun ()
case1)
   , ([Char]
"case2", Term TyName Name DefaultUni DefaultFun ()
case2)
   , ([Char]
"case3", Term TyName Name DefaultUni DefaultFun ()
case3)
   , ([Char]
"case4", Term TyName Name DefaultUni DefaultFun ()
case4)
   , ([Char]
"caseProd1", Term TyName Name DefaultUni DefaultFun ()
caseProd1)
   , ([Char]
"caseNoBranch", Term TyName Name DefaultUni DefaultFun ()
caseNoBranch)
   , ([Char]
"caseNonTag", Term TyName Name DefaultUni DefaultFun ()
caseNonTag)
   ]

-- | An extension of 'namesAndTests' that only works with the CEK machine and not the CK one.
namesAndTestsCek :: [(String, Term TyName Name DefaultUni DefaultFun ())]
namesAndTestsCek :: [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTestsCek
    = ([Char]
"headSingletonException", Term TyName Name DefaultUni DefaultFun ()
headSingletonException)
    ([Char], Term TyName Name DefaultUni DefaultFun ())
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
forall a. a -> [a] -> [a]
: [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTests

test_golden :: TestTree
test_golden :: TestTree
test_golden = [Char] -> [TestTree] -> TestTree
testGroup [Char]
"golden"
              [ [Char] -> [TestTree] -> TestTree
testGroup [Char]
"CK"  ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree)
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
-> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree)
-> ([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCK)  [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTests
              -- The CEK tests have been added to the plutus-conformance tests
              -- (mostly renamed since there's no instantation, and with some
              -- duplicates removed).  We should also add the typed tests to the
              -- conformance suite and remove them from here once we've done
              -- that.
              , [Char] -> [TestTree] -> TestTree
testGroup [Char]
"CEK" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree)
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
-> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree)
-> ([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsEvaluatedCEK) [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTestsCek
              , [Char] -> [TestTree] -> TestTree
testGroup [Char]
"Typechecking" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree)
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
-> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree)
-> ([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypechecked) [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTestsCek
              , [Char] -> [TestTree] -> TestTree
testGroup [Char]
"Typechecking CK output" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ (([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree)
-> [([Char], Term TyName Name DefaultUni DefaultFun ())]
-> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree)
-> ([Char], Term TyName Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Char] -> Term TyName Name DefaultUni DefaultFun () -> TestTree
goldenVsTypecheckedEvaluatedCK) [([Char], Term TyName Name DefaultUni DefaultFun ())]
namesAndTests
              ]