-- Why is it needed here, but not in "Universe.Core"?
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE PatternSynonyms    #-}

module PlutusCore
    (
      -- * Parser
      parseProgram
    , parseTerm
    , parseType
    , SourcePos
    , SrcSpan (..)
    , SrcSpans
    -- * Builtins
    , Some (..)
    , SomeTypeIn (..)
    , Kinded (..)
    , ValueOf (..)
    , someValueOf
    , someValue
    , someValueType
    , Esc
    , Contains (..)
    , Closed (..)
    , EverywhereAll
    , knownUniOf
    , GShow (..)
    , show
    , GEq (..)
    , HasUniApply (..)
    , checkStar
    , withApplicable
    , (:~:) (..)
    , type (<:)
    , HasTypeLevel
    , HasTermLevel
    , HasTypeAndTermLevel
    , DefaultUni (..)
    , pattern DefaultUniList
    , pattern DefaultUniPair
    , DefaultFun (..)
    -- * AST
    , Term (..)
    , termSubterms
    , termSubtypes
    , termMapNames
    , programMapNames
    , UniOf
    , Type (..)
    , typeSubtypes
    , typeMapNames
    , Kind (..)
    , toPatFuncKind
    , fromPatFuncKind
    , argsFunKind
    , ParserError (..)
    , Version (..)
    , Program (..)
    , Name (..)
    , TyName (..)
    , Unique (..)
    , UniqueMap (..)
    , UniqueSet (..)
    , Normalized (..)
    , latestVersion
    , termAnn
    , typeAnn
    , tyVarDeclAnn
    , tyVarDeclName
    , tyVarDeclKind
    , varDeclAnn
    , varDeclName
    , varDeclType
    , tyDeclAnn
    , tyDeclType
    , tyDeclKind
    , progAnn
    , progVer
    , progTerm
    , mapFun
    -- * DeBruijn representation
    , DeBruijn (..)
    , TyDeBruijn (..)
    , NamedDeBruijn (..)
    , NamedTyDeBruijn (..)
    , deBruijnTerm
    , unDeBruijnTerm
    -- * Processing
    , HasUniques
    , Rename (..)
    -- * Type checking
    , module TypeCheck
    , normalizeTypesIn
    , normalizeTypesInProgram
    , AsTypeError (..)
    , TypeError
    -- * Errors
    , Error (..)
    , AsError (..)
    , NormCheckError (..)
    , AsNormCheckError (..)
    , UniqueError (..)
    , AsUniqueError (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    -- * Quotation and term construction
    , Quote
    , runQuote
    , QuoteT
    , runQuoteT
    , MonadQuote
    , liftQuote
    -- * Name generation
    , freshUnique
    , freshName
    , freshTyName
    -- * Evaluation
    , EvaluationResult (..)
    -- * Combining programs
    , applyProgram
    -- * Benchmarking
    , termSize
    , typeSize
    , kindSize
    , programSize
    , serialisedSize
    ) where


import PlutusCore.Annotation
import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.DeBruijn
import PlutusCore.Default
import PlutusCore.Error
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Flat ()
import PlutusCore.Name.Unique
import PlutusCore.Name.UniqueMap
import PlutusCore.Name.UniqueSet
import PlutusCore.Normalize
import PlutusCore.Parser
import PlutusCore.Quote
import PlutusCore.Rename
import PlutusCore.Size
import PlutusCore.Subst
import PlutusCore.TypeCheck as TypeCheck

import Control.Monad.Except

-- | 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 ann.
Term tyname name uni fun ann -> ann
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 ann.
Term tyname name uni fun ann -> ann
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