{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module UntypedPlutusCore.Test.DeBruijn.Bad
  ( var0
  , lamAbs1
  , fun0var0
  , fun1var0
  , fun1var1
  , deepFun1
  , deepOut0
  , deepMix0_1
  , deepMix1_0
  , deepOutMix1_0
  , manyFree01
  , iteStrict0
  , iteLazy0
  , ite10
  , illITEStrict
  , illITELazy
  , illPartialBuiltin
  , illAdd
  , illOverAppBuiltin
  , illOverAppFun
  ) where

import PlutusCore.Default
import PlutusCore.MkPlc
import PlutusCore.StdLib.Data.Bool
import PlutusCore.StdLib.Data.Unit
import PlutusPrelude
import UntypedPlutusCore
import UntypedPlutusCore.Test.DeBruijn.Good

-- | A definitely out-of-scope variable. Our variables start at index 1.
var0 :: Term DeBruijn uni fun ()
var0 :: forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0 = () -> DeBruijn -> Term DeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn uni fun ())
-> DeBruijn -> Term DeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
0

-- | Build a `LamAbs` with the binder having a non-sensical index.
lamAbs1 :: t ~ Term DeBruijn uni fun () => t -> t
lamAbs1 :: forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 = ()
-> DeBruijn -> Term DeBruijn uni fun () -> Term DeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () (DeBruijn -> Term DeBruijn uni fun () -> Term DeBruijn uni fun ())
-> DeBruijn -> Term DeBruijn uni fun () -> Term DeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
1

fun0var0, fun1var0, fun1var1 :: Term DeBruijn DefaultUni DefaultFun ()
fun0var0 :: Term DeBruijn DefaultUni DefaultFun ()
fun0var0 = Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0
fun1var0 :: Term DeBruijn DefaultUni DefaultFun ()
fun1var0 = Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0
fun1var1 :: Term DeBruijn DefaultUni DefaultFun ()
fun1var1 = Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
1

{-| (lam1 ...n.... (Var n))
Wrong binders, Well-scoped variable -}
deepFun1 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepFun1 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepFun1 Natural
n =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      Index -> DeBruijn
DeBruijn (Index -> DeBruijn) -> Index -> DeBruijn
forall a b. (a -> b) -> a -> b
$
        Natural -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n

{-| (lam0 ...n.... (Var n+1))
Correct binders, Out-of-scope variable -}
deepOut0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepOut0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepOut0 Natural
n =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      Index -> DeBruijn
DeBruijn (Index -> DeBruijn) -> Index -> DeBruijn
forall a b. (a -> b) -> a -> b
$
        Natural -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Index) -> Natural -> Index
forall a b. (a -> b) -> a -> b
$
          Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1

{-| (lam0 ...n.... lam1 ...n.... (Var n+n))
Mix of correct and wrong binders, Well-scoped variable -}
deepMix0_1 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepMix0_1 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepMix0_1 Natural
n =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
        Index -> DeBruijn
DeBruijn (Index -> DeBruijn) -> Index -> DeBruijn
forall a b. (a -> b) -> a -> b
$
          Natural -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Index) -> Natural -> Index
forall a b. (a -> b) -> a -> b
$
            Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n

{-| (lam1 ...n.... lam0 ...n.... (Var n+n))
Mix of wrong and correct binders, well-scoped variable -}
deepMix1_0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepMix1_0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepMix1_0 Natural
n =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
        Index -> DeBruijn
DeBruijn (Index -> DeBruijn) -> Index -> DeBruijn
forall a b. (a -> b) -> a -> b
$
          Natural -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Index) -> Natural -> Index
forall a b. (a -> b) -> a -> b
$
            Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n

{-| (lam1 ...n.... lam0 ...n.... (Var n+n+1))
Mix of correct and wrong binders, out-of-scope variable -}
deepOutMix1_0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepOutMix1_0 :: Natural -> Term DeBruijn DefaultUni DefaultFun ()
deepOutMix1_0 Natural
n =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
n Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
        Index -> DeBruijn
DeBruijn (Index -> DeBruijn) -> Index -> DeBruijn
forall a b. (a -> b) -> a -> b
$
          Natural -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Index) -> Natural -> Index
forall a b. (a -> b) -> a -> b
$
            Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1

{-| [(force (builtin ifThenElse) (con bool True) (con bool True) var99]
Both branches are evaluated *before* the predicate,
so it is clear that this should fail in every case. -}
iteStrict0 :: Term DeBruijn DefaultUni DefaultFun ()
iteStrict0 :: Term DeBruijn DefaultUni DefaultFun ()
iteStrict0 =
  ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
IfThenElse)
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- pred
       , Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- then
       , Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0 -- else
       ]

{-| [(force (builtin ifThenElse) (con bool True) (delay true) (delay var99)]
The branches are *lazy*. The evaluation result (success or failure) depends on how the machine
ignores  the irrelevant to the computation) part of the environment. -}
iteLazy0 :: Term DeBruijn DefaultUni DefaultFun ()
iteLazy0 :: Term DeBruijn DefaultUni DefaultFun ()
iteLazy0 =
  ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
IfThenElse)
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- pred
       , ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- then
       , ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0 -- else
       ]

-- | [(force (builtin ifThenElse) (con bool True) (lam0 var1) (lam1 var0)]
ite10 :: Term DeBruijn DefaultUni DefaultFun ()
ite10 :: Term DeBruijn DefaultUni DefaultFun ()
ite10 =
  ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
IfThenElse)
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- pred
       , Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
idFun0 -- then
       , Term DeBruijn DefaultUni DefaultFun ()
fun1var0 -- else
       ]

-- | An example with a lot of free vars
manyFree01 :: Term DeBruijn DefaultUni DefaultFun ()
manyFree01 :: Term DeBruijn DefaultUni DefaultFun ()
manyFree01 =
  Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
5 (()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
10 Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}.
Term name uni fun () -> Term name uni fun ()
forceDelay Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0)) (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    Natural
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a. Natural -> (a -> a) -> a -> a
timesA Natural
20 Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}.
Term name uni fun () -> Term name uni fun ()
forceDelay (Term DeBruijn DefaultUni DefaultFun ()
 -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      () -> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn DefaultUni DefaultFun ())
-> DeBruijn -> Term DeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
        Index -> DeBruijn
DeBruijn Index
1
  where
    forceDelay :: Term name uni fun () -> Term name uni fun ()
forceDelay = () -> Term name uni fun () -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term name uni fun () -> Term name uni fun ())
-> (Term name uni fun () -> Term name uni fun ())
-> Term name uni fun ()
-> Term name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Term name uni fun () -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()

-- * Examples will ill-typed terms

{-| [(force (builtin ifThenElse) (con bool True) (con bool  True) (con unit ())]
Note that the branches have **different** types. The machine cannot catch such a type error. -}
illITEStrict :: Term DeBruijn DefaultUni DefaultFun ()
illITEStrict :: Term DeBruijn DefaultUni DefaultFun ()
illITEStrict =
  ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
IfThenElse)
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- pred
       , Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- then
       , Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval -- else
       ]

{-| [(force (builtin ifThenElse) (con bool True) (lam x (con bool  True)) (lam x (con unit ()))]
The branches are *lazy*. Note that the branches have **different** types.
The machine cannot catch such a type error. -}
illITELazy :: Term DeBruijn DefaultUni DefaultFun ()
illITELazy :: Term DeBruijn DefaultUni DefaultFun ()
illITELazy =
  ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
IfThenElse)
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- pred
       , Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- then
       , ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true -- else
       ]

{-| [(builtin addInteger) (con integer 1) (con unit ())]
Interesting because it involves a runtime type-error of a builtin. -}
illAdd :: Term DeBruijn DefaultUni DefaultFun ()
illAdd :: Term DeBruijn DefaultUni DefaultFun ()
illAdd =
  () -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
AddInteger
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       , Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval
       ]

{-| [(builtin addInteger) (con integer 1) (con integer 1) (con integer 1)]
Interesting because it involves a (builtin) over-saturation type-error,
which the machine can recognize. -}
illOverAppBuiltin :: Term DeBruijn DefaultUni DefaultFun ()
illOverAppBuiltin :: Term DeBruijn DefaultUni DefaultFun ()
illOverAppBuiltin =
  () -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
AddInteger
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       , Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       , Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       ]

{-| [(lam x x) (con integer 1) (con integer 1)]
Interesting because it involves a (lambda) over-saturation type-error,
which the machine can recognize. -}
illOverAppFun :: Term DeBruijn DefaultUni DefaultFun ()
illOverAppFun :: Term DeBruijn DefaultUni DefaultFun ()
illOverAppFun =
  Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
idFun0
    Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       , Term DeBruijn DefaultUni DefaultFun ()
forall name fun. Term name DefaultUni fun ()
one
       ]

{-| [addInteger true]
this relates to the immediate vs deferred unlifting.
this used to be an immediate type error but now it is deferred until saturation. -}
illPartialBuiltin :: Term DeBruijn DefaultUni DefaultFun ()
illPartialBuiltin :: Term DeBruijn DefaultUni DefaultFun ()
illPartialBuiltin = ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
AddInteger) Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true

-- helpers

one :: Term name DefaultUni fun ()
one :: forall name fun. Term name DefaultUni fun ()
one = 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