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

module PlutusCore
    (
      -- * Parser
      parseProgram
    , parseTerm
    , parseType
    , parseScoped
    , topSourcePos
    -- * Builtins
    , Some (..)
    , SomeTypeIn (..)
    , Kinded (..)
    , ValueOf (..)
    , someValueOf
    , someValue
    , someValueType
    , Esc
    , Contains (..)
    , Includes
    , Closed (..)
    , EverywhereAll
    , knownUniOf
    , GShow (..)
    , show
    , GEq (..)
    , deriveGEq
    , HasUniApply (..)
    , checkStar
    , withApplicable
    , (:~:) (..)
    , type (<:)
    , DefaultUni (..)
    , pattern DefaultUniList
    , pattern DefaultUniPair
    , DefaultFun (..)
    -- * AST
    , Term (..)
    , termSubterms
    , termSubtypes
    , UniOf
    , Type (..)
    , typeSubtypes
    , Kind (..)
    , ParseError (..)
    , Version (..)
    , Program (..)
    , Name (..)
    , TyName (..)
    , Unique (..)
    , UniqueMap (..)
    , Normalized (..)
    , defaultVersion
    , termAnn
    , typeAnn
    , tyVarDeclAnn
    , tyVarDeclName
    , tyVarDeclKind
    , varDeclAnn
    , varDeclName
    , varDeclType
    , tyDeclAnn
    , tyDeclType
    , tyDeclKind
    , progAnn
    , progVer
    , progTerm
    , mapFun
    -- * DeBruijn representation
    , DeBruijn (..)
    , NamedDeBruijn (..)
    , deBruijnTerm
    , unDeBruijnTerm
    -- * Lexer
    , SourcePos
    -- * Formatting
    , format
    -- * Processing
    , HasUniques
    , Rename (..)
    -- * Type checking
    , module TypeCheck
    , printType
    , normalizeTypesIn
    , normalizeTypesInProgram
    , AsTypeError (..)
    , TypeError
    , parseTypecheck
    -- for testing
    , typecheckPipeline
    -- * Errors
    , Error (..)
    , AsError (..)
    , NormCheckError (..)
    , AsNormCheckError (..)
    , UniqueError (..)
    , AsUniqueError (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    -- * Base functors
    , TermF (..)
    , TypeF (..)
    -- * Quotation and term construction
    , Quote
    , runQuote
    , QuoteT
    , runQuoteT
    , MonadQuote
    , liftQuote
    -- * Name generation
    , freshUnique
    , freshName
    , freshTyName
    -- * Evaluation
    , EvaluationResult (..)
    , UnliftingMode (..)
    -- * Combining programs
    , applyProgram
    -- * Benchmarking
    , termSize
    , typeSize
    , kindSize
    , programSize
    , serialisedSize
    -- * Budgeting defaults
    , defaultBuiltinCostModel
    , defaultBuiltinsRuntime
    , defaultCekCostModel
    , defaultCekMachineCosts
    , defaultCekParameters
    , defaultCostModelParams
    , defaultUnliftingMode
    , unitCekParameters
    -- * CEK machine costs
    , cekMachineCostsPrefix
    , CekMachineCosts (..)
    ) where

import PlutusPrelude

import PlutusCore.Builtin
import PlutusCore.Check.Uniques qualified as Uniques
import PlutusCore.Core
import PlutusCore.DeBruijn
import PlutusCore.Default
import PlutusCore.Error
import PlutusCore.Evaluation.Machine.Ck
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Flat ()
import PlutusCore.Name
import PlutusCore.Normalize
import PlutusCore.Pretty
import PlutusCore.Quote
import PlutusCore.Rename
import PlutusCore.Size
import PlutusCore.TypeCheck as TypeCheck

import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts

import Control.Monad.Except
import Data.ByteString.Lazy qualified as BSL
import Data.Text qualified as T
import PlutusCore.Parser (parseProgram, parseTerm, parseType)
import Text.Megaparsec (SourcePos, errorBundlePretty, initialPos)

topSourcePos :: SourcePos
topSourcePos :: SourcePos
topSourcePos = FilePath -> SourcePos
initialPos FilePath
"top"

printType ::(AsTypeError e (Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun SourcePos,
        MonadError e m)
    => BSL.ByteString
    -> m T.Text
printType :: ByteString -> m Text
printType ByteString
bs = QuoteT m Text -> m Text
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m Text -> m Text) -> QuoteT m Text -> m Text
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
T.pack (FilePath -> Text)
-> (Normalized (Type TyName DefaultUni ()) -> FilePath)
-> Normalized (Type TyName DefaultUni ())
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> FilePath
forall a. Show a => a -> FilePath
show (Doc Any -> FilePath)
-> (Normalized (Type TyName DefaultUni ()) -> Doc Any)
-> Normalized (Type TyName DefaultUni ())
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Normalized (Type TyName DefaultUni ()) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty (Normalized (Type TyName DefaultUni ()) -> Text)
-> QuoteT m (Normalized (Type TyName DefaultUni ()))
-> QuoteT m Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Program TyName Name DefaultUni DefaultFun SourcePos
scoped <- ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *).
MonadQuote f =>
ByteString
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
parseScoped ByteString
bs
    TypeCheckConfig DefaultUni DefaultFun
config <- SourcePos -> QuoteT m (TypeCheckConfig DefaultUni DefaultFun)
forall err (m :: * -> *) term (uni :: * -> *) fun ann.
(MonadError err m, AsTypeError err term uni fun ann,
 Typecheckable uni fun) =>
ann -> m (TypeCheckConfig uni fun)
getDefTypeCheckConfig SourcePos
topSourcePos
    TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun SourcePos
-> QuoteT m (Normalized (Type TyName DefaultUni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
(MonadError err m, MonadQuote m,
 AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, GEq uni, Ix fun) =>
TypeCheckConfig uni fun
-> Program TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferTypeOfProgram TypeCheckConfig DefaultUni DefaultFun
config Program TyName Name DefaultUni DefaultFun SourcePos
scoped

-- | Parse and rewrite so that names are globally unique, not just unique within
-- their scope.
-- don't require there to be no free variables at this point, we might be parsing an open term
parseScoped :: (MonadQuote f) =>
    BSL.ByteString
    -> f (Program TyName Name DefaultUni DefaultFun SourcePos)
parseScoped :: ByteString
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
parseScoped ByteString
bs = do
    case ByteString
-> Either
     (ParseErrorBundle Text ParseError)
     (Program TyName Name DefaultUni DefaultFun SourcePos)
parseProgram ByteString
bs of
        -- when fail, pretty print the parse errors.
        Left ParseErrorBundle Text ParseError
err ->
            FilePath -> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a. FilePath -> a
errorWithoutStackTrace (FilePath
 -> f (Program TyName Name DefaultUni DefaultFun SourcePos))
-> FilePath
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text ParseError -> FilePath
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> FilePath
errorBundlePretty ParseErrorBundle Text ParseError
err
        -- otherwise,
        Right Program TyName Name DefaultUni DefaultFun SourcePos
p -> do
            -- run @rename@ through the program
            Program TyName Name DefaultUni DefaultFun SourcePos
renamed <- QuoteT f (Program TyName Name DefaultUni DefaultFun SourcePos)
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT f (Program TyName Name DefaultUni DefaultFun SourcePos)
 -> f (Program TyName Name DefaultUni DefaultFun SourcePos))
-> QuoteT f (Program TyName Name DefaultUni DefaultFun SourcePos)
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ Program TyName Name DefaultUni DefaultFun SourcePos
-> QuoteT f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename Program TyName Name DefaultUni DefaultFun SourcePos
p
            -- check the program for @UniqueError@'s
            let checked :: Either
  (UniqueError SourcePos)
  (Program TyName Name DefaultUni DefaultFun SourcePos)
checked = (Program TyName Name DefaultUni DefaultFun SourcePos
 -> Either (UniqueError SourcePos) ())
-> Program TyName Name DefaultUni DefaultFun SourcePos
-> Either
     (UniqueError SourcePos)
     (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through ((UniqueError SourcePos -> Bool)
-> Program TyName Name DefaultUni DefaultFun SourcePos
-> Either (UniqueError SourcePos) ()
forall ann name tyname e (m :: * -> *) (uni :: * -> *) fun.
(Ord ann, HasUnique name TermUnique, HasUnique tyname TypeUnique,
 AsUniqueError e ann, MonadError e m) =>
(UniqueError ann -> Bool)
-> Program tyname name uni fun ann -> m ()
Uniques.checkProgram (Bool -> UniqueError SourcePos -> Bool
forall a b. a -> b -> a
const Bool
True)) Program TyName Name DefaultUni DefaultFun SourcePos
renamed
            case Either
  (UniqueError SourcePos)
  (Program TyName Name DefaultUni DefaultFun SourcePos)
checked of
                -- pretty print the error
                Left (UniqueError SourcePos
err :: UniqueError SourcePos) ->
                    FilePath -> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a. FilePath -> a
errorWithoutStackTrace (FilePath
 -> f (Program TyName Name DefaultUni DefaultFun SourcePos))
-> FilePath
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ Doc Any -> FilePath
forall str ann. Render str => Doc ann -> str
render (Doc Any -> FilePath) -> Doc Any -> FilePath
forall a b. (a -> b) -> a -> b
$ UniqueError SourcePos -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty UniqueError SourcePos
err
                -- if there's no errors, return the parsed program
                Right Program TyName Name DefaultUni DefaultFun SourcePos
_ -> Program TyName Name DefaultUni DefaultFun SourcePos
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Program TyName Name DefaultUni DefaultFun SourcePos
p

-- | Parse a program and typecheck it.
parseTypecheck :: (AsTypeError
   e
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   SourcePos,
 MonadError e m, MonadQuote m) =>
    TypeCheckConfig DefaultUni DefaultFun
    -> BSL.ByteString -> m (Normalized (Type TyName DefaultUni ()))
parseTypecheck :: TypeCheckConfig DefaultUni DefaultFun
-> ByteString -> m (Normalized (Type TyName DefaultUni ()))
parseTypecheck TypeCheckConfig DefaultUni DefaultFun
cfg = TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun SourcePos
-> m (Normalized (Type TyName DefaultUni ()))
forall e a (m :: * -> *).
(AsTypeError
   e
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   a,
 MonadError e m, MonadQuote m) =>
TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun a
-> m (Normalized (Type TyName DefaultUni ()))
typecheckPipeline TypeCheckConfig DefaultUni DefaultFun
cfg (Program TyName Name DefaultUni DefaultFun SourcePos
 -> m (Normalized (Type TyName DefaultUni ())))
-> (ByteString
    -> m (Program TyName Name DefaultUni DefaultFun SourcePos))
-> ByteString
-> m (Normalized (Type TyName DefaultUni ()))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ByteString
-> m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *).
MonadQuote f =>
ByteString
-> f (Program TyName Name DefaultUni DefaultFun SourcePos)
parseScoped

-- | Typecheck a program.
typecheckPipeline
    :: (AsTypeError e (Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun a,
        MonadError e m,
        MonadQuote m)
    => TypeCheckConfig DefaultUni DefaultFun
    -> Program TyName Name DefaultUni DefaultFun a
    -> m (Normalized (Type TyName DefaultUni ()))
typecheckPipeline :: TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun a
-> m (Normalized (Type TyName DefaultUni ()))
typecheckPipeline = TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun a
-> m (Normalized (Type TyName DefaultUni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
(MonadError err m, MonadQuote m,
 AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, GEq uni, Ix fun) =>
TypeCheckConfig uni fun
-> Program TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
inferTypeOfProgram

format :: (Monad m,
 PrettyBy
   config (Program TyName Name DefaultUni DefaultFun SourcePos)) =>
 config -> BSL.ByteString -> m T.Text
format :: config -> ByteString -> m Text
format config
cfg ByteString
bs = do
    case ByteString
-> Either
     (ParseErrorBundle Text ParseError)
     (Program TyName Name DefaultUni DefaultFun SourcePos)
parseProgram ByteString
bs of
        -- when fail, pretty print the parse errors.
        Left ParseErrorBundle Text ParseError
err ->
            FilePath -> m Text
forall a. FilePath -> a
errorWithoutStackTrace (FilePath -> m Text) -> FilePath -> m Text
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text ParseError -> FilePath
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> FilePath
errorBundlePretty ParseErrorBundle Text ParseError
err
        -- otherwise,
        Right Program TyName Name DefaultUni DefaultFun SourcePos
p -> do
            -- run @rename@ through the program
            Program TyName Name DefaultUni DefaultFun SourcePos
renamed <- QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
-> m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
 -> m (Program TyName Name DefaultUni DefaultFun SourcePos))
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
-> m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ Program TyName Name DefaultUni DefaultFun SourcePos
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename Program TyName Name DefaultUni DefaultFun SourcePos
p
            QuoteT m Text -> m Text
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m Text -> m Text) -> QuoteT m Text -> m Text
forall a b. (a -> b) -> a -> b
$ (Program TyName Name DefaultUni DefaultFun SourcePos -> Text)
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
-> QuoteT m Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (config
-> Program TyName Name DefaultUni DefaultFun SourcePos -> Text
forall str a config.
(PrettyBy config a, Render str) =>
config -> a -> str
displayBy config
cfg) (QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
 -> QuoteT m Text)
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
-> QuoteT m Text
forall a b. (a -> b) -> a -> b
$ Program TyName Name DefaultUni DefaultFun SourcePos
-> QuoteT m (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename Program TyName Name DefaultUni DefaultFun SourcePos
renamed

-- | Take one PLC program and apply it to another.
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 Version a
_ Term tyname name uni fun a
t1) (Program a
a2 Version a
_ Term tyname name uni fun a
t2) = a
-> Version a
-> Term tyname name uni fun a
-> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version 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 -> Version a
forall ann. ann -> Version ann
defaultVersion a
forall a. Monoid a => a
mempty) (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)