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

module PlutusCore
    (
      -- * Parser
      parseProgram
    , parseTerm
    , parseType
    , parseScoped
    , topAlexPosn
    -- * Builtins
    , Some (..)
    , SomeTypeIn (..)
    , Kinded (..)
    , ValueOf (..)
    , someValueOf
    , someValue
    , 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
    , allKeywords
    , termAnn
    , typeAnn
    , tyVarDeclAnn
    , tyVarDeclName
    , tyVarDeclKind
    , varDeclAnn
    , varDeclName
    , varDeclType
    , tyDeclAnn
    , tyDeclType
    , tyDeclKind
    , progAnn
    , progVer
    , progTerm
    , mapFun
    -- * DeBruijn representation
    , DeBruijn (..)
    , NamedDeBruijn (..)
    , deBruijnTerm
    , unDeBruijnTerm
    -- * Lexer
    , AlexPosn (..)
    -- * Formatting
    , format
    , formatDoc
    -- * Processing
    , HasUniques
    , Rename (..)
    -- * Type checking
    , module TypeCheck
    , fileType
    , fileTypeCfg
    , 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 (..)
    -- * Combining programs
    , applyProgram
    -- * Benchmarking
    , termSize
    , typeSize
    , kindSize
    , programSize
    , serialisedSize
    -- * Budgeting defaults
    , defaultBuiltinCostModel
    , defaultBuiltinsRuntime
    , defaultCekCostModel
    , defaultCekMachineCosts
    , defaultCekParameters
    , defaultCostModelParams
    , unitCekParameters
    -- * CEK machine costs
    , cekMachineCostsPrefix
    , CekMachineCosts (..)
    ) where

import PlutusPrelude

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.Lexer
import PlutusCore.Lexer.Type
import PlutusCore.Name
import PlutusCore.Normalize
import PlutusCore.Parser
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

-- | Given a file at @fibonacci.plc@, @fileType "fibonacci.plc"@ will display
-- its type or an error message.
fileType :: FilePath -> IO T.Text
fileType :: FilePath -> IO Text
fileType = (ByteString -> Text) -> IO ByteString -> IO Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Error DefaultUni DefaultFun AlexPosn -> Text)
-> (Text -> Text)
-> Either (Error DefaultUni DefaultFun AlexPosn) Text
-> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error DefaultUni DefaultFun AlexPosn -> Text
prettyErr Text -> Text
forall a. a -> a
id (Either (Error DefaultUni DefaultFun AlexPosn) Text -> Text)
-> (ByteString
    -> Either (Error DefaultUni DefaultFun AlexPosn) Text)
-> ByteString
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Either (Error DefaultUni DefaultFun AlexPosn) Text
forall e (m :: * -> *).
(AsParseError e AlexPosn, AsUniqueError e AlexPosn,
 AsTypeError
   e
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   AlexPosn,
 MonadError e m) =>
ByteString -> m Text
printType) (IO ByteString -> IO Text)
-> (FilePath -> IO ByteString) -> FilePath -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO ByteString
BSL.readFile
    where
        prettyErr :: Error DefaultUni DefaultFun AlexPosn -> T.Text
        prettyErr :: Error DefaultUni DefaultFun AlexPosn -> Text
prettyErr = Error DefaultUni DefaultFun AlexPosn -> Text
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcDef

-- | Given a file, display
-- its type or an error message, optionally dumping annotations and debug
-- information.
fileTypeCfg :: PrettyConfigPlc -> FilePath -> IO T.Text
fileTypeCfg :: PrettyConfigPlc -> FilePath -> IO Text
fileTypeCfg PrettyConfigPlc
cfg = (ByteString -> Text) -> IO ByteString -> IO Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Error DefaultUni DefaultFun AlexPosn -> Text)
-> (Text -> Text)
-> Either (Error DefaultUni DefaultFun AlexPosn) Text
-> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error DefaultUni DefaultFun AlexPosn -> Text
prettyErr Text -> Text
forall a. a -> a
id (Either (Error DefaultUni DefaultFun AlexPosn) Text -> Text)
-> (ByteString
    -> Either (Error DefaultUni DefaultFun AlexPosn) Text)
-> ByteString
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Either (Error DefaultUni DefaultFun AlexPosn) Text
forall e (m :: * -> *).
(AsParseError e AlexPosn, AsUniqueError e AlexPosn,
 AsTypeError
   e
   (Term TyName Name DefaultUni DefaultFun ())
   DefaultUni
   DefaultFun
   AlexPosn,
 MonadError e m) =>
ByteString -> m Text
printType) (IO ByteString -> IO Text)
-> (FilePath -> IO ByteString) -> FilePath -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO ByteString
BSL.readFile
    where
        prettyErr :: Error DefaultUni DefaultFun AlexPosn -> T.Text
        prettyErr :: Error DefaultUni DefaultFun AlexPosn -> Text
prettyErr = PrettyConfigPlc -> Error DefaultUni DefaultFun AlexPosn -> Text
forall str a config.
(PrettyBy config a, Render str) =>
config -> a -> str
displayBy PrettyConfigPlc
cfg

-- | Print the type of a program contained in a 'ByteString'
printType
    :: (AsParseError e AlexPosn,
        AsUniqueError e AlexPosn,
        AsTypeError e (Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun AlexPosn,
        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 AlexPosn
scoped <- ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, AsUniqueError e AlexPosn, MonadError e m,
 MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseScoped ByteString
bs
    TypeCheckConfig DefaultUni DefaultFun
config <- AlexPosn -> 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 AlexPosn
topAlexPosn
    TypeCheckConfig DefaultUni DefaultFun
-> Program TyName Name DefaultUni DefaultFun AlexPosn
-> 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 AlexPosn
scoped

-- | Parse and rewrite so that names are globally unique, not just unique within
-- their scope.
parseScoped
    :: (AsParseError e AlexPosn,
        AsUniqueError e AlexPosn,
        MonadError e m,
        MonadQuote m)
    => BSL.ByteString
    -> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
-- don't require there to be no free variables at this point, we might be parsing an open term
parseScoped :: ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseScoped = (Program TyName Name DefaultUni DefaultFun AlexPosn -> m ())
-> Program TyName Name DefaultUni DefaultFun AlexPosn
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through ((UniqueError AlexPosn -> Bool)
-> Program TyName Name DefaultUni DefaultFun AlexPosn -> m ()
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 AlexPosn -> Bool
forall a b. a -> b -> a
const Bool
True)) (Program TyName Name DefaultUni DefaultFun AlexPosn
 -> m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> (ByteString
    -> m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Program TyName Name DefaultUni DefaultFun AlexPosn
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename (Program TyName Name DefaultUni DefaultFun AlexPosn
 -> m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> (ByteString
    -> m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, MonadError e m, MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgram

-- | Parse a program and typecheck it.
parseTypecheck
    :: (AsParseError e AlexPosn,
        AsUniqueError e AlexPosn,
        AsTypeError e (Term TyName Name DefaultUni DefaultFun ()) DefaultUni DefaultFun AlexPosn,
        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 AlexPosn
-> 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 AlexPosn
 -> m (Normalized (Type TyName DefaultUni ())))
-> (ByteString
    -> m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> 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 AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, AsUniqueError e AlexPosn, MonadError e m,
 MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
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

parseProgramDef
    :: (AsParseError e AlexPosn, MonadError e m, MonadQuote m)
    => BSL.ByteString -> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgramDef :: ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgramDef = ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, MonadError e m, MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgram

formatDoc :: (AsParseError e AlexPosn, MonadError e m) => PrettyConfigPlc -> BSL.ByteString -> m (Doc a)
-- don't use parseScoped since we don't bother running sanity checks when we format
formatDoc :: PrettyConfigPlc -> ByteString -> m (Doc a)
formatDoc PrettyConfigPlc
cfg = QuoteT m (Doc a) -> m (Doc a)
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m (Doc a) -> m (Doc a))
-> (ByteString -> QuoteT m (Doc a)) -> ByteString -> m (Doc a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Program TyName Name DefaultUni DefaultFun AlexPosn -> Doc a)
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
-> QuoteT m (Doc a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrettyConfigPlc
-> Program TyName Name DefaultUni DefaultFun AlexPosn -> Doc a
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg) (QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
 -> QuoteT m (Doc a))
-> (ByteString
    -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> QuoteT m (Doc a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Program TyName Name DefaultUni DefaultFun AlexPosn
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename (Program TyName Name DefaultUni DefaultFun AlexPosn
 -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> (ByteString
    -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, MonadError e m, MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgramDef)

format
    :: (AsParseError e AlexPosn, MonadError e m)
    => PrettyConfigPlc -> BSL.ByteString -> m T.Text
-- don't use parseScoped since we don't bother running sanity checks when we format
format :: PrettyConfigPlc -> ByteString -> m Text
format PrettyConfigPlc
cfg = QuoteT m Text -> m Text
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m Text -> m Text)
-> (ByteString -> QuoteT m Text) -> ByteString -> m Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Program TyName Name DefaultUni DefaultFun AlexPosn -> Text)
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
-> QuoteT m Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrettyConfigPlc
-> Program TyName Name DefaultUni DefaultFun AlexPosn -> Text
forall str a config.
(PrettyBy config a, Render str) =>
config -> a -> str
displayBy PrettyConfigPlc
cfg) (QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
 -> QuoteT m Text)
-> (ByteString
    -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> QuoteT m Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Program TyName Name DefaultUni DefaultFun AlexPosn
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename (Program TyName Name DefaultUni DefaultFun AlexPosn
 -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> (ByteString
    -> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn))
-> ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ByteString
-> QuoteT m (Program TyName Name DefaultUni DefaultFun AlexPosn)
forall e (m :: * -> *).
(AsParseError e AlexPosn, MonadError e m, MonadQuote m) =>
ByteString
-> m (Program TyName Name DefaultUni DefaultFun AlexPosn)
parseProgramDef)

-- | 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)