plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusIR.TypeCheck.Internal

Description

The internal module of the type checker that defines the actual algorithms, but not the user-facing API.

Synopsis

Documentation

newtype BuiltinTypes (uni ∷ TypeType) fun Source #

Mapping from Builtins to their Normalized Kinds.

Constructors

BuiltinTypes 

Fields

type TypeCheckT (uni ∷ TypeType) fun cfg (m ∷ TypeType) = ReaderT (TypeCheckEnv uni fun cfg) m Source #

The type checking monad that the type checker runs in. In contains a TypeCheckEnv and allows to throw TypeErrors.

type MonadKindCheck err term (uni ∷ TypeType) fun ann (m ∷ TypeType) = (MonadError err m, AsTypeError err term uni fun ann, ToKind uni) Source #

The constraints that are required for kind checking.

type MonadTypeCheck err term (uni ∷ TypeType) fun ann (m ∷ TypeType) = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun) Source #

The general constraints that are required for type checking a Plutus AST.

type MonadTypeCheckPir err uni fun ann m = (MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m, AsTypeErrorExt err uni ann) Source #

The constraints that are required for type checking Plutus IR.

tccBuiltinTypesHasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun) Source #

data PirTCConfig uni fun Source #

extending the plc typecheck config with AllowEscape

data AllowEscape Source #

Extra flag to be passed in the TypeCheckM Reader context, to signal if the PIR expression currently being typechecked is at the top-level and thus its type can escape, or nested and thus not allowed to escape.

Constructors

YesEscape 
NoEscape 

inferTypeM ∷ ∀ err m uni fun ann. MonadTypeCheckPir err uni fun ann m ⇒ Term TyName Name uni fun ann → PirTCEnv uni fun m (Normalized (Type TyName uni ())) Source #

Synthesize the type of a term, returning a normalized type.

checkTypeMMonadTypeCheckPir err uni fun ann m ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → PirTCEnv uni fun m () Source #

Check a Term against a NormalizedType.

runTypeCheckMPirTCConfig uni fun → PirTCEnv uni fun m a → m a Source #

Run a TypeCheckM computation by supplying a TypeCheckConfig to it. Differs from its PLC version in that is passes an extra env flag YesEscape.