{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

module PlutusIR.Core.Type
  ( TyName (..)
  , Name (..)
  , VarDecl (..)
  , TyVarDecl (..)
  , varDeclNameString
  , tyVarDeclNameString
  , Kind (..)
  , Type (..)
  , Datatype (..)
  , datatypeNameString
  , Recursivity (..)
  , Strictness (..)
  , Binding (..)
  , Term (..)
  , Program (..)
  , Version (..)
  , applyProgram
  , termAnn
  , bindingAnn
  , progAnn
  , progVer
  , progTerm
  ) where

import PlutusCore (Kind, Name, TyName, Type (..), Version (..))
import PlutusCore qualified as PLC
import PlutusCore.Builtin (HasConstant (..), throwNotAConstant)
import PlutusCore.Core (UniOf)
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Flat ()
import PlutusCore.MkPlc (Def (..), TermLike (..), TyVarDecl (..), VarDecl (..))
import PlutusCore.Name.Unique qualified as PLC
import PlutusPrelude

import Universe

import Control.Lens.TH
import Control.Monad.Except
import Data.Hashable
import Data.Text qualified as T
import Data.Word
import PlutusCore.Error (ApplyProgramError (MkApplyProgramError))

-- Datatypes

data Datatype tyname name uni a
  = Datatype a (TyVarDecl tyname a) [TyVarDecl tyname a] name [VarDecl tyname name uni a]
  deriving stock ((forall a b.
 (a -> b)
 -> Datatype tyname name uni a -> Datatype tyname name uni b)
-> (forall a b.
    a -> Datatype tyname name uni b -> Datatype tyname name uni a)
-> Functor (Datatype tyname name uni)
forall a b.
a -> Datatype tyname name uni b -> Datatype tyname name uni a
forall a b.
(a -> b)
-> Datatype tyname name uni a -> Datatype tyname name uni b
forall tyname name (uni :: * -> *) a b.
a -> Datatype tyname name uni b -> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a b.
(a -> b)
-> Datatype tyname name uni a -> Datatype tyname name uni b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) a b.
(a -> b)
-> Datatype tyname name uni a -> Datatype tyname name uni b
fmap :: forall a b.
(a -> b)
-> Datatype tyname name uni a -> Datatype tyname name uni b
$c<$ :: forall tyname name (uni :: * -> *) a b.
a -> Datatype tyname name uni b -> Datatype tyname name uni a
<$ :: forall a b.
a -> Datatype tyname name uni b -> Datatype tyname name uni a
Functor, Int -> Datatype tyname name uni a -> ShowS
[Datatype tyname name uni a] -> ShowS
Datatype tyname name uni a -> String
(Int -> Datatype tyname name uni a -> ShowS)
-> (Datatype tyname name uni a -> String)
-> ([Datatype tyname name uni a] -> ShowS)
-> Show (Datatype tyname name uni a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
Int -> Datatype tyname name uni a -> ShowS
forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
[Datatype tyname name uni a] -> ShowS
forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
Datatype tyname name uni a -> String
$cshowsPrec :: forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
Int -> Datatype tyname name uni a -> ShowS
showsPrec :: Int -> Datatype tyname name uni a -> ShowS
$cshow :: forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
Datatype tyname name uni a -> String
show :: Datatype tyname name uni a -> String
$cshowList :: forall tyname name (uni :: * -> *) a.
(Show a, Show tyname, Show name, GShow uni) =>
[Datatype tyname name uni a] -> ShowS
showList :: [Datatype tyname name uni a] -> ShowS
Show, (forall x.
 Datatype tyname name uni a -> Rep (Datatype tyname name uni a) x)
-> (forall x.
    Rep (Datatype tyname name uni a) x -> Datatype tyname name uni a)
-> Generic (Datatype tyname name uni a)
forall x.
Rep (Datatype tyname name uni a) x -> Datatype tyname name uni a
forall x.
Datatype tyname name uni a -> Rep (Datatype tyname name uni a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) a x.
Rep (Datatype tyname name uni a) x -> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a x.
Datatype tyname name uni a -> Rep (Datatype tyname name uni a) x
$cfrom :: forall tyname name (uni :: * -> *) a x.
Datatype tyname name uni a -> Rep (Datatype tyname name uni a) x
from :: forall x.
Datatype tyname name uni a -> Rep (Datatype tyname name uni a) x
$cto :: forall tyname name (uni :: * -> *) a x.
Rep (Datatype tyname name uni a) x -> Datatype tyname name uni a
to :: forall x.
Rep (Datatype tyname name uni a) x -> Datatype tyname name uni a
Generic)

varDeclNameString :: VarDecl tyname Name uni a -> String
varDeclNameString :: forall tyname (uni :: * -> *) a.
VarDecl tyname Name uni a -> String
varDeclNameString = Text -> String
T.unpack (Text -> String)
-> (VarDecl tyname Name uni a -> Text)
-> VarDecl tyname Name uni a
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Text
PLC._nameText (Name -> Text)
-> (VarDecl tyname Name uni a -> Name)
-> VarDecl tyname Name uni a
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname Name uni a -> Name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName

tyVarDeclNameString :: TyVarDecl TyName a -> String
tyVarDeclNameString :: forall a. TyVarDecl TyName a -> String
tyVarDeclNameString = Text -> String
T.unpack (Text -> String)
-> (TyVarDecl TyName a -> Text) -> TyVarDecl TyName a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Text
PLC._nameText (Name -> Text)
-> (TyVarDecl TyName a -> Name) -> TyVarDecl TyName a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Name
PLC.unTyName (TyName -> Name)
-> (TyVarDecl TyName a -> TyName) -> TyVarDecl TyName a -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl TyName a -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName

datatypeNameString :: Datatype TyName name uni a -> String
datatypeNameString :: forall name (uni :: * -> *) a. Datatype TyName name uni a -> String
datatypeNameString (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
_ name
_ [VarDecl TyName name uni a]
_) = TyVarDecl TyName a -> String
forall a. TyVarDecl TyName a -> String
tyVarDeclNameString TyVarDecl TyName a
tn

-- Bindings

{- | Each multi-let-group has to be marked with its scoping:
* 'NonRec': the identifiers introduced by this multi-let are only linearly-scoped,
  i.e. an identifier cannot refer to itself or later-introduced identifiers of the group.
* 'Rec': an identifiers introduced by this multi-let group can use all other multi-lets
  of the same group (including itself), thus permitting (mutual) recursion.
-}
data Recursivity = NonRec | Rec
  deriving stock (Int -> Recursivity -> ShowS
[Recursivity] -> ShowS
Recursivity -> String
(Int -> Recursivity -> ShowS)
-> (Recursivity -> String)
-> ([Recursivity] -> ShowS)
-> Show Recursivity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Recursivity -> ShowS
showsPrec :: Int -> Recursivity -> ShowS
$cshow :: Recursivity -> String
show :: Recursivity -> String
$cshowList :: [Recursivity] -> ShowS
showList :: [Recursivity] -> ShowS
Show, Recursivity -> Recursivity -> Bool
(Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool) -> Eq Recursivity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Recursivity -> Recursivity -> Bool
== :: Recursivity -> Recursivity -> Bool
$c/= :: Recursivity -> Recursivity -> Bool
/= :: Recursivity -> Recursivity -> Bool
Eq, (forall x. Recursivity -> Rep Recursivity x)
-> (forall x. Rep Recursivity x -> Recursivity)
-> Generic Recursivity
forall x. Rep Recursivity x -> Recursivity
forall x. Recursivity -> Rep Recursivity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Recursivity -> Rep Recursivity x
from :: forall x. Recursivity -> Rep Recursivity x
$cto :: forall x. Rep Recursivity x -> Recursivity
to :: forall x. Rep Recursivity x -> Recursivity
Generic, Eq Recursivity
Eq Recursivity =>
(Recursivity -> Recursivity -> Ordering)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Recursivity)
-> (Recursivity -> Recursivity -> Recursivity)
-> Ord Recursivity
Recursivity -> Recursivity -> Bool
Recursivity -> Recursivity -> Ordering
Recursivity -> Recursivity -> Recursivity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Recursivity -> Recursivity -> Ordering
compare :: Recursivity -> Recursivity -> Ordering
$c< :: Recursivity -> Recursivity -> Bool
< :: Recursivity -> Recursivity -> Bool
$c<= :: Recursivity -> Recursivity -> Bool
<= :: Recursivity -> Recursivity -> Bool
$c> :: Recursivity -> Recursivity -> Bool
> :: Recursivity -> Recursivity -> Bool
$c>= :: Recursivity -> Recursivity -> Bool
>= :: Recursivity -> Recursivity -> Bool
$cmax :: Recursivity -> Recursivity -> Recursivity
max :: Recursivity -> Recursivity -> Recursivity
$cmin :: Recursivity -> Recursivity -> Recursivity
min :: Recursivity -> Recursivity -> Recursivity
Ord)
  deriving anyclass (Eq Recursivity
Eq Recursivity =>
(Int -> Recursivity -> Int)
-> (Recursivity -> Int) -> Hashable Recursivity
Int -> Recursivity -> Int
Recursivity -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Recursivity -> Int
hashWithSalt :: Int -> Recursivity -> Int
$chash :: Recursivity -> Int
hash :: Recursivity -> Int
Hashable)

{- | Recursivity can form a 'Semigroup' / lattice, where 'NonRec' < 'Rec'.
The lattice is ordered by "power": a non-recursive binding group can be made recursive
and it will still work, but not vice versa.
The semigroup operation is the "join" of the lattice.
-}
instance Semigroup Recursivity where
  Recursivity
NonRec <> :: Recursivity -> Recursivity -> Recursivity
<> Recursivity
x = Recursivity
x
  Recursivity
Rec <> Recursivity
_    = Recursivity
Rec

data Strictness = NonStrict | Strict
  deriving stock (Int -> Strictness -> ShowS
[Strictness] -> ShowS
Strictness -> String
(Int -> Strictness -> ShowS)
-> (Strictness -> String)
-> ([Strictness] -> ShowS)
-> Show Strictness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Strictness -> ShowS
showsPrec :: Int -> Strictness -> ShowS
$cshow :: Strictness -> String
show :: Strictness -> String
$cshowList :: [Strictness] -> ShowS
showList :: [Strictness] -> ShowS
Show, Strictness -> Strictness -> Bool
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
/= :: Strictness -> Strictness -> Bool
Eq, (forall x. Strictness -> Rep Strictness x)
-> (forall x. Rep Strictness x -> Strictness) -> Generic Strictness
forall x. Rep Strictness x -> Strictness
forall x. Strictness -> Rep Strictness x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Strictness -> Rep Strictness x
from :: forall x. Strictness -> Rep Strictness x
$cto :: forall x. Rep Strictness x -> Strictness
to :: forall x. Rep Strictness x -> Strictness
Generic)

data Binding tyname name uni fun a
  = TermBind a Strictness (VarDecl tyname name uni a) (Term tyname name uni fun a)
  | TypeBind a (TyVarDecl tyname a) (Type tyname uni a)
  | DatatypeBind a (Datatype tyname name uni a)
  deriving stock ((forall a b.
 (a -> b)
 -> Binding tyname name uni fun a -> Binding tyname name uni fun b)
-> (forall a b.
    a
    -> Binding tyname name uni fun b -> Binding tyname name uni fun a)
-> Functor (Binding tyname name uni fun)
forall a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
forall a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
<$ :: forall a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
Functor, (forall x.
 Binding tyname name uni fun a
 -> Rep (Binding tyname name uni fun a) x)
-> (forall x.
    Rep (Binding tyname name uni fun a) x
    -> Binding tyname name uni fun a)
-> Generic (Binding tyname name uni fun a)
forall x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
forall x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
from :: forall x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
to :: forall x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
Generic)

deriving stock instance
  ( Show tyname
  , Show name
  , Show fun
  , Show a
  , GShow uni
  , Everywhere uni Show
  , Closed uni
  )
  => Show (Binding tyname name uni fun a)

-- Terms

{- Note [PIR as a PLC extension]
PIR is designed to be an extension of PLC, which means that we try and be strict superset of it.

The main benefit of this is simplicity, but we hope that in future it will make sharing of
theoretical and practical material easier. In the long run it would be nice if PIR was a "true"
extension of PLC (perhaps in the sense of "Trees that Grow"), and then we could potentially
even share most of the typechecker.
-}

{- Note [Declarations in Plutus Core]
In Plutus Core declarations are usually *flattened*, i.e. `(lam x ty t)`, whereas
in Plutus IR they are *reified*, i.e. `(termBind (vardecl x ty) t)`.

Plutus IR needs reified declarations to make it easier to parse *lists* of declarations,
which occur in a few places.

However, we also include all of Plutus Core's term syntax in our term syntax (and we also use
its types). We therefore have somewhat inconsistent syntax since declarations in Plutus
Core terms will be flattened. This makes the embedding obvious and makes life easier
if we were ever to use the Plutus Core AST "for real".

It would be nice to resolve the inconsistency, but this would probably require changing
Plutus Core to use reified declarations.
-}

-- See Note [PIR as a PLC extension]
data Term tyname name uni fun a
  = -- Plutus Core (ish) forms, see Note [Declarations in Plutus Core]
    Let a Recursivity (NonEmpty (Binding tyname name uni fun a)) (Term tyname name uni fun a)
  | Var a name
  | TyAbs a tyname (Kind a) (Term tyname name uni fun a)
  | LamAbs a name (Type tyname uni a) (Term tyname name uni fun a)
  | Apply a (Term tyname name uni fun a) (Term tyname name uni fun a)
  | Constant a (PLC.Some (PLC.ValueOf uni))
  | Builtin a fun
  | TyInst a (Term tyname name uni fun a) (Type tyname uni a)
  | Error a (Type tyname uni a)
  | IWrap a (Type tyname uni a) (Type tyname uni a) (Term tyname name uni fun a)
  | Unwrap a (Term tyname name uni fun a)
  | -- See Note [Constr tag type]
    Constr a (Type tyname uni a) Word64 [Term tyname name uni fun a]
  | Case a (Type tyname uni a) (Term tyname name uni fun a) [Term tyname name uni fun a]
  deriving stock ((forall a b.
 (a -> b)
 -> Term tyname name uni fun a -> Term tyname name uni fun b)
-> (forall a b.
    a -> Term tyname name uni fun b -> Term tyname name uni fun a)
-> Functor (Term tyname name uni fun)
forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
<$ :: forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
Functor, (forall x.
 Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x)
-> (forall x.
    Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a)
-> Generic (Term tyname name uni fun a)
forall x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
forall x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
from :: forall x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
to :: forall x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
Generic)

deriving stock instance
  ( Show tyname
  , Show name
  , GShow uni
  , Everywhere uni Show
  , Show fun
  , Show a
  , Closed uni
  )
  => Show (Term tyname name uni fun a)

-- See Note [ExMemoryUsage instances for non-constants].
instance ExMemoryUsage (Term tyname name uni fun ann) where
  memoryUsage :: Term tyname name uni fun ann -> CostRose
memoryUsage =
    String -> Term tyname name uni fun ann -> CostRose
forall a. HasCallStack => String -> a
Prelude.error String
"Internal error: 'memoryUsage' for IR 'Term' is not supposed to be forced"

type instance UniOf (Term tyname name uni fun ann) = uni

instance HasConstant (Term tyname name uni fun ()) where
  asConstant :: Term tyname name uni fun ()
-> Either
     BuiltinError (Some (ValueOf (UniOf (Term tyname name uni fun ()))))
asConstant (Constant ()
_ Some (ValueOf uni)
val) = Some (ValueOf uni) -> Either BuiltinError (Some (ValueOf uni))
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
  asConstant Term tyname name uni fun ()
_                = Either BuiltinError (Some (ValueOf uni))
Either
  BuiltinError (Some (ValueOf (UniOf (Term tyname name uni fun ()))))
forall (m :: * -> *) void. MonadError BuiltinError m => m void
throwNotAConstant

  fromConstant :: Some (ValueOf (UniOf (Term tyname name uni fun ())))
-> Term tyname name uni fun ()
fromConstant = () -> Some (ValueOf uni) -> Term tyname name uni fun ()
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant ()

instance TermLike (Term tyname name uni fun) tyname name uni fun where
  var :: forall ann. ann -> name -> Term tyname name uni fun ann
var = ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var
  tyAbs :: forall ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
tyAbs = ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs
  lamAbs :: forall ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
lamAbs = ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
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
  apply :: forall ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
apply = ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
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
  constant :: forall ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
constant = ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant
  builtin :: forall ann. ann -> fun -> Term tyname name uni fun ann
builtin = ann -> fun -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin
  tyInst :: forall ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
tyInst = ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst
  unwrap :: forall ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
unwrap = ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap
  iWrap :: forall ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
iWrap = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap
  error :: forall ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
error = ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error
  constr :: forall ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
constr = ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
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
  kase :: forall ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
kase = ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
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

  termLet :: forall ann.
ann
-> TermDef (Term tyname name uni fun) tyname name uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
termLet ann
x (Def VarDecl tyname name uni ann
vd Term tyname name uni fun ann
bind) = ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
NonRec (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding tyname name uni fun ann
 -> NonEmpty (Binding tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
Strict VarDecl tyname name uni ann
vd Term tyname name uni fun ann
bind)
  typeLet :: forall ann.
ann
-> TypeDef tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
typeLet ann
x (Def TyVarDecl tyname ann
vd Type tyname uni ann
bind) = ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
NonRec (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding tyname name uni fun ann
 -> NonEmpty (Binding tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
vd Type tyname uni ann
bind)

data Program tyname name uni fun ann = Program
  { forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> ann
_progAnn  :: ann
  , forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> Version
_progVer  :: Version
  -- ^ The version of the program. This corresponds to the underlying Plutus Core version.
  , forall tyname name (uni :: * -> *) fun ann.
Program tyname name uni fun ann -> Term tyname name uni fun ann
_progTerm :: Term tyname name uni fun ann
  }
  deriving stock ((forall a b.
 (a -> b)
 -> Program tyname name uni fun a -> Program tyname name uni fun b)
-> (forall a b.
    a
    -> Program tyname name uni fun b -> Program tyname name uni fun a)
-> Functor (Program tyname name uni fun)
forall a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
forall a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> Program tyname name uni fun a -> Program tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
<$ :: forall a b.
a -> Program tyname name uni fun b -> Program tyname name uni fun a
Functor, (forall x.
 Program tyname name uni fun ann
 -> Rep (Program tyname name uni fun ann) x)
-> (forall x.
    Rep (Program tyname name uni fun ann) x
    -> Program tyname name uni fun ann)
-> Generic (Program tyname name uni fun ann)
forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
from :: forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
to :: forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
Generic)
makeLenses ''Program

deriving stock instance
  ( Show tyname
  , Show name
  , GShow uni
  , Everywhere uni Show
  , Show fun
  , Show ann
  , Closed uni
  )
  => Show (Program tyname name uni fun ann)

type instance
  PLC.HasUniques (Term tyname name uni fun ann) =
    (PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)

type instance
  PLC.HasUniques (Program tyname name uni fun ann) =
    PLC.HasUniques (Term tyname name uni fun ann)

{- | Applies one program to another. Fails if the versions do not match
and tries to merge annotations.
-}
applyProgram
  :: (MonadError ApplyProgramError m, Semigroup a)
  => Program tyname name uni fun a
  -> Program tyname name uni fun a
  -> m (Program tyname name uni fun a)
applyProgram :: forall (m :: * -> *) a tyname name (uni :: * -> *) fun.
(MonadError ApplyProgramError m, Semigroup a) =>
Program tyname name uni fun a
-> Program tyname name uni fun a
-> m (Program tyname name uni fun a)
applyProgram (Program a
a1 Version
v1 Term tyname name uni fun a
t1) (Program a
a2 Version
v2 Term tyname name uni fun a
t2)
  | Version
v1 Version -> Version -> Bool
forall a. Eq a => a -> a -> Bool
== Version
v2 =
      Program tyname name uni fun a -> m (Program tyname name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Program tyname name uni fun a
 -> m (Program tyname name uni fun a))
-> Program tyname name uni fun a
-> m (Program tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ a
-> Version
-> Term tyname name uni fun a
-> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program (a
a1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a2) Version
v1 (a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a -> a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
t1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
t2) Term tyname name uni fun a
t1 Term tyname name uni fun a
t2)
applyProgram (Program a
_a1 Version
v1 Term tyname name uni fun a
_t1) (Program a
_a2 Version
v2 Term tyname name uni fun a
_t2) =
  ApplyProgramError -> m (Program tyname name uni fun a)
forall a. ApplyProgramError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ApplyProgramError -> m (Program tyname name uni fun a))
-> ApplyProgramError -> m (Program tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ Version -> Version -> ApplyProgramError
MkApplyProgramError Version
v1 Version
v2

termAnn :: Term tyname name uni fun a -> a
termAnn :: forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> a
termAnn = \case
  Let a
a Recursivity
_ NonEmpty (Binding tyname name uni fun a)
_ Term tyname name uni fun a
_    -> a
a
  Var a
a name
_        -> a
a
  TyAbs a
a tyname
_ Kind a
_ Term tyname name uni fun a
_  -> a
a
  LamAbs a
a name
_ Type tyname uni a
_ Term tyname name uni fun a
_ -> a
a
  Apply a
a Term tyname name uni fun a
_ Term tyname name uni fun a
_    -> a
a
  Constant a
a Some (ValueOf uni)
_   -> a
a
  Builtin a
a fun
_    -> a
a
  TyInst a
a Term tyname name uni fun a
_ Type tyname uni a
_   -> a
a
  Error a
a Type tyname uni a
_      -> a
a
  IWrap a
a Type tyname uni a
_ Type tyname uni a
_ Term tyname name uni fun a
_  -> a
a
  Unwrap a
a Term tyname name uni fun a
_     -> a
a
  Constr a
a Type tyname uni a
_ Word64
_ [Term tyname name uni fun a]
_ -> a
a
  Case a
a Type tyname uni a
_ Term tyname name uni fun a
_ [Term tyname name uni fun a]
_   -> a
a

bindingAnn :: Binding tyname name uni fun a -> a
bindingAnn :: forall tyname name (uni :: * -> *) fun a.
Binding tyname name uni fun a -> a
bindingAnn = \case
  TermBind a
a Strictness
_ VarDecl tyname name uni a
_ Term tyname name uni fun a
_ -> a
a
  TypeBind a
a TyVarDecl tyname a
_ Type tyname uni a
_   -> a
a
  DatatypeBind a
a Datatype tyname name uni a
_ -> a
a