{-# LANGUAGE FlexibleInstances     #-}
{-# 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 (..),
    applyProgram,
    termAnn,
    progAnn,
    progTerm,
    ) where

import PlutusPrelude

import Control.Lens.TH
import PlutusCore (Kind, Name, TyName, Type (..))
import PlutusCore qualified as PLC
import PlutusCore.Builtin (HasConstant (..), throwNotAConstant)
import PlutusCore.Core (UniOf)
import PlutusCore.Flat ()
import PlutusCore.MkPlc (Def (..), TermLike (..), TyVarDecl (..), VarDecl (..))
import PlutusCore.Name qualified as PLC

import Data.Text qualified as T

-- Datatypes

{- Note: [Serialization of PIR]
The serialized version of Plutus-IR will be included in  the final
executable for helping debugging and testing and providing better error
reporting. It is not meant to be stored on the chain, which means that
the underlying representation can vary. The `Generic` instances of the
terms can thus be used as backwards compatibility is not required.
-}

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

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

tyVarDeclNameString :: TyVarDecl TyName a -> String
tyVarDeclNameString :: 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.nameString (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 fun a -> String
datatypeNameString :: Datatype TyName Name uni fun a -> String
datatypeNameString (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
_ Name
_ [VarDecl TyName Name uni fun 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
showList :: [Recursivity] -> ShowS
$cshowList :: [Recursivity] -> ShowS
show :: Recursivity -> String
$cshow :: Recursivity -> String
showsPrec :: Int -> Recursivity -> ShowS
$cshowsPrec :: Int -> Recursivity -> ShowS
Show, Recursivity -> Recursivity -> Bool
(Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool) -> Eq Recursivity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Recursivity -> Recursivity -> Bool
$c/= :: Recursivity -> Recursivity -> Bool
== :: Recursivity -> Recursivity -> Bool
$c== :: 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
$cto :: forall x. Rep Recursivity x -> Recursivity
$cfrom :: forall x. Recursivity -> Rep Recursivity x
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
min :: Recursivity -> Recursivity -> Recursivity
$cmin :: Recursivity -> Recursivity -> Recursivity
max :: Recursivity -> Recursivity -> Recursivity
$cmax :: Recursivity -> Recursivity -> Recursivity
>= :: Recursivity -> Recursivity -> Bool
$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
compare :: Recursivity -> Recursivity -> Ordering
$ccompare :: Recursivity -> Recursivity -> Ordering
$cp1Ord :: Eq Recursivity
Ord)

-- | 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
showList :: [Strictness] -> ShowS
$cshowList :: [Strictness] -> ShowS
show :: Strictness -> String
$cshow :: Strictness -> String
showsPrec :: Int -> Strictness -> ShowS
$cshowsPrec :: Int -> Strictness -> ShowS
Show, Strictness -> Strictness -> Bool
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: 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
$cto :: forall x. Rep Strictness x -> Strictness
$cfrom :: forall x. Strictness -> Rep Strictness x
Generic)

data Binding tyname name uni fun a = TermBind a Strictness (VarDecl tyname name uni fun a) (Term tyname name uni fun a)
                           | TypeBind a (TyVarDecl tyname a) (Type tyname uni a)
                           | DatatypeBind a (Datatype tyname name uni fun a)
    deriving stock (a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
(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
<$ :: a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
fmap :: (a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
Functor, Int -> Binding tyname name uni fun a -> ShowS
[Binding tyname name uni fun a] -> ShowS
Binding tyname name uni fun a -> String
(Int -> Binding tyname name uni fun a -> ShowS)
-> (Binding tyname name uni fun a -> String)
-> ([Binding tyname name uni fun a] -> ShowS)
-> Show (Binding tyname name uni fun a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Int -> Binding tyname name uni fun a -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
[Binding tyname name uni fun a] -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Binding tyname name uni fun a -> String
showList :: [Binding tyname name uni fun a] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
[Binding tyname name uni fun a] -> ShowS
show :: Binding tyname name uni fun a -> String
$cshow :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Binding tyname name uni fun a -> String
showsPrec :: Int -> Binding tyname name uni fun a -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Int -> Binding tyname name uni fun a -> ShowS
Show, (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
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
Generic)

-- 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)
                        deriving stock (a -> Term tyname name uni fun b -> Term tyname name uni fun a
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
(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
<$ :: a -> Term tyname name uni fun b -> Term tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
fmap :: (a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
Functor, Int -> Term tyname name uni fun a -> ShowS
[Term tyname name uni fun a] -> ShowS
Term tyname name uni fun a -> String
(Int -> Term tyname name uni fun a -> ShowS)
-> (Term tyname name uni fun a -> String)
-> ([Term tyname name uni fun a] -> ShowS)
-> Show (Term tyname name uni fun a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Int -> Term tyname name uni fun a -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
[Term tyname name uni fun a] -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Term tyname name uni fun a -> String
showList :: [Term tyname name uni fun a] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
[Term tyname name uni fun a] -> ShowS
show :: Term tyname name uni fun a -> String
$cshow :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Term tyname name uni fun a -> String
showsPrec :: Int -> Term tyname name uni fun a -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
 Show tyname, Show fun) =>
Int -> Term tyname name uni fun a -> ShowS
Show, (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
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
Generic)

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

instance HasConstant (Term tyname name uni fun ()) where
    asConstant :: Maybe cause
-> Term tyname name uni fun ()
-> Either
     (ErrorWithCause err cause)
     (Some (ValueOf (UniOf (Term tyname name uni fun ()))))
asConstant Maybe cause
_        (Constant ()
_ Some (ValueOf uni)
val) = Some (ValueOf uni)
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant Maybe cause
mayCause Term tyname name uni fun ()
_                = Maybe cause
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall err cause (m :: * -> *) r.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause -> m r
throwNotAConstant Maybe cause
mayCause

    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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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
    termLet :: ann
-> TermDef (Term tyname name uni fun) tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
termLet ann
x (Def VarDecl tyname name uni fun 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 (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 fun 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 fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
Strict VarDecl tyname name uni fun ann
vd Term tyname name uni fun ann
bind)
    typeLet :: 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 (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)

-- no version as PIR is not versioned
data Program tyname name uni fun ann = Program
    { Program tyname name uni fun ann -> ann
_progAnn  :: ann
    , Program tyname name uni fun ann -> Term tyname name uni fun ann
_progTerm :: Term tyname name uni fun ann
    }
    deriving stock (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
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
Generic
makeLenses ''Program

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)

applyProgram
    :: Monoid a
    => Program tyname name uni fun a
    -> Program tyname name uni fun a
    -> Program tyname name uni fun a
applyProgram :: Program tyname name uni fun a
-> Program tyname name uni fun a -> Program tyname name uni fun a
applyProgram (Program a
a1 Term tyname name uni fun a
t1) (Program a
a2 Term tyname name uni fun a
t2) = a -> Term tyname name uni fun a -> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> 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) (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 a
forall a. Monoid a => a
mempty Term tyname name uni fun a
t1 Term tyname name uni fun a
t2)

termAnn :: Term tyname name uni fun a -> a
termAnn :: Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
t = case Term tyname name uni fun a
t of
  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