{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternSynonyms #-}

-- |
-- Module: Covenant.ASG
-- Copyright: (C) MLabs 2025
-- License: Apache 2.0
-- Maintainer: koz@mlabs.city, sean@mlabs.city
--
-- The Covenant ASG, and ways to programmatically build it.
--
-- = Note
--
-- We use the term \'ASG\' to refer to \'abstract syntax graph\'. This is
-- because Covenant uses hash consing to ensure duplicate nodes do not exist,
-- thus producing a DAG structure, rather than a tree.
--
-- @since 1.0.0
module Covenant.ASG
  ( -- * The ASG itself

    -- ** Types
    ASG,

    -- ** Functions
    topLevelNode,
    nodeAt,

    -- * ASG components

    -- ** Types
    Id,
    Ref (..),
    Arg,
    CompNodeInfo
      ( Builtin1,
        Builtin2,
        Builtin3,
        Builtin6,
        Lam,
        Force
      ),
    ValNodeInfo (Lit, App, Thunk, Cata, DataConstructor, Match),
    ASGNode (..),
    ASGNodeType (..),

    -- ** Functions
    typeASGNode,

    -- * ASG builder

    -- ** Types
    CovenantError (..),
    ScopeInfo (..),
    ASGBuilder,
    TypeAppError (..),
    RenameError (..),
    UnRenameError (..),
    EncodingArgErr (..),
    CovenantTypeError (..),
    BoundTyVar,

    -- ** Introducers
    boundTyVar,
    arg,
    builtin1,
    builtin2,
    builtin3,
    builtin6,
    force,
    lam,
    err,
    lit,
    thunk,
    dataConstructor,

    -- ** Eliminators
    app,
    cata,
    match,

    -- ** Helpers
    ctor,
    lazyLam,
    dtype,

    -- *** Environment
    defaultDatatypes,

    -- *** Function
    runASGBuilder,
    -- only for tests
    ASGEnv (..),
  )
where

#if __GLASGOW_HASKELL__==908
import Data.Foldable (foldl')
#endif

import Control.Monad (foldM, join, unless, zipWithM)
import Control.Monad.Except
  ( ExceptT,
    MonadError (throwError),
    runExceptT,
  )
import Control.Monad.HashCons
  ( HashConsT,
    MonadHashCons (lookupRef, refTo),
    runHashConsT,
  )
import Control.Monad.Reader
  ( MonadReader (local),
    ReaderT,
    asks,
    runReaderT,
  )
import Covenant.Constant (AConstant, typeConstant)
import Covenant.Data (DatatypeInfo, mkDatatypeInfo)
import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
import Covenant.Index (Count, Index, count0, intCount, intIndex, wordCount)
import Covenant.Internal.KindCheck (EncodingArgErr (EncodingArgMismatch), checkEncodingArgs)
import Covenant.Internal.Ledger (ledgerTypes)
import Covenant.Internal.Rename
  ( RenameError
      ( InvalidAbstractionReference,
        InvalidScopeReference
      ),
    UnRenameError (NegativeDeBruijn, UnRenameWildCard),
    renameCompT,
    renameDatatypeInfo,
    renameValT,
    runRenameM,
    undoRename,
  )
import Covenant.Internal.Term
  ( ASGNode (ACompNode, AValNode, AnError),
    ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType),
    Arg (Arg),
    CompNodeInfo
      ( Builtin1Internal,
        Builtin2Internal,
        Builtin3Internal,
        Builtin6Internal,
        ForceInternal,
        LamInternal
      ),
    CovenantTypeError
      ( ApplyCompType,
        ApplyToError,
        ApplyToValType,
        BrokenIdReference,
        CataAlgebraWrongArity,
        CataApplyToNonValT,
        CataNoBaseFunctorForType,
        CataNoSuchType,
        CataNonRigidAlgebra,
        CataNotAnAlgebra,
        CataUnsuitable,
        CataWrongBuiltinType,
        CataWrongValT,
        ConstructorDoesNotExistForType,
        DatatypeInfoRenameError,
        EncodingError,
        FailedToRenameInstantiation,
        ForceCompType,
        ForceError,
        ForceNonThunk,
        IntroFormErrorNodeField,
        IntroFormWrongNumArgs,
        InvalidOpaqueField,
        LambdaResultsInCompType,
        LambdaResultsInNonReturn,
        MatchErrorAsHandler,
        MatchNoBBForm,
        MatchNoDatatypeInfo,
        MatchNonDatatypeScrutinee,
        MatchNonThunkBBF,
        MatchNonValTy,
        MatchPolymorphicHandler,
        MatchRenameBBFail,
        MatchRenameTyConArgFail,
        NoSuchArgument,
        OutOfScopeTyVar,
        RenameArgumentFailed,
        RenameFunctionFailed,
        ReturnCompType,
        ReturnWrapsCompType,
        ReturnWrapsError,
        ThunkError,
        ThunkValType,
        TypeDoesNotExist,
        UndeclaredOpaquePlutusDataCtor,
        UndoRenameFailure,
        UnificationError,
        WrongReturnType
      ),
    Id,
    Ref (AnArg, AnId),
    ValNodeInfo (AppInternal, CataInternal, DataConstructorInternal, LitInternal, MatchInternal, ThunkInternal),
    typeASGNode,
    typeId,
    typeRef,
  )
import Covenant.Internal.Type
  ( AbstractTy (BoundAt),
    BuiltinFlatT (ByteStringT, IntegerT),
    CompT (CompT),
    CompTBody (CompTBody),
    DataDeclaration (DataDeclaration),
    Renamed,
    TyName,
    ValT (BuiltinFlat, Datatype, ThunkT),
    arity,
  )
import Covenant.Internal.Unification
  ( TypeAppError
      ( DatatypeInfoRenameFailed,
        DoesNotUnify,
        ExcessArgs,
        ImpossibleHappened,
        InsufficientArgs,
        LeakingUnifiable,
        LeakingWildcard,
        NoBBForm,
        NoDatatypeInfo
      ),
    UnifyM,
    checkApp,
    fixUp,
    reconcile,
    runUnifyM,
    substitute,
    unify,
  )
import Covenant.Prim
  ( OneArgFunc,
    SixArgFunc,
    ThreeArgFunc,
    TwoArgFunc,
    typeOneArgFunc,
    typeSixArgFunc,
    typeThreeArgFunc,
    typeTwoArgFunc,
  )
import Covenant.Type
  ( CompT (Comp0),
    CompTBody (ReturnT),
    Constructor,
    ConstructorName,
    DataDeclaration (OpaqueData),
    PlutusDataConstructor (PlutusB, PlutusConstr, PlutusI, PlutusList, PlutusMap),
    Renamed (Unifiable),
    TyName (TyName),
    ValT (Abstraction),
    tyvar,
  )
import Data.Bimap (Bimap)
import Data.Bimap qualified as Bimap
import Data.Coerce (coerce)
import Data.Functor.Identity (Identity, runIdentity)
import Data.Kind (Type)
import Data.List (find)
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (fromJust, isJust, mapMaybe)
import Data.Set qualified as Set
import Data.Text qualified as T
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Void (Void, vacuous)
import Data.Wedge (Wedge, wedge)
import Data.Word (Word32)
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    at,
    folded,
    ix,
    lens,
    over,
    preview,
    review,
    toListOf,
    view,
    (%),
    _1,
    _2,
  )

-- | A fully-assembled Covenant ASG.
--
-- @since 1.0.0
newtype ASG = ASG (Id, Map Id ASGNode)
  deriving stock
    ( -- | @since 1.0.0
      ASG -> ASG -> Bool
(ASG -> ASG -> Bool) -> (ASG -> ASG -> Bool) -> Eq ASG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ASG -> ASG -> Bool
== :: ASG -> ASG -> Bool
$c/= :: ASG -> ASG -> Bool
/= :: ASG -> ASG -> Bool
Eq,
      -- | @since 1.0.0
      Int -> ASG -> ShowS
[ASG] -> ShowS
ASG -> [Char]
(Int -> ASG -> ShowS)
-> (ASG -> [Char]) -> ([ASG] -> ShowS) -> Show ASG
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ASG -> ShowS
showsPrec :: Int -> ASG -> ShowS
$cshow :: ASG -> [Char]
show :: ASG -> [Char]
$cshowList :: [ASG] -> ShowS
showList :: [ASG] -> ShowS
Show
    )

-- Note (Koz, 24/04/25): The `topLevelNode` and `nodeAt` functions use `fromJust`,
-- because we can guarantee it's impossible to miss. For an end user, the only
-- way to get hold of an `Id` is by inspecting a node, and since we control how
-- these are built and assigned, and users can't change them, it's safe.
--
-- It is technically possible to escape this safety regime by having two
-- different `ASG`s and mixing up their `Id`s. However, this is both vanishingly
-- unlikely and probably not worth trying to protect against, given the nuisance
-- of having to work in `Maybe` all the time.

-- | Retrieves the top-level node of an ASG.
--
-- @since 1.0.0
topLevelNode :: ASG -> ASGNode
topLevelNode :: ASG -> ASGNode
topLevelNode asg :: ASG
asg@(ASG (Id
rootId, Map Id ASGNode
_)) = Id -> ASG -> ASGNode
nodeAt Id
rootId ASG
asg

-- | Given an 'Id' and an ASG, produces the node corresponding to that 'Id'.
--
-- = Important note
--
-- This is only safe to use if the 'Id' comes from a node in the argument 'ASG'.
-- 'Id's valid in one ASG are not likely to be valid in another. \'Mixing
-- and matching\' 'Id's from different ASGs will at best produce unexpected
-- results, and at worst will crash. You have been warned.
--
-- @since 1.0.0
nodeAt :: Id -> ASG -> ASGNode
nodeAt :: Id -> ASG -> ASGNode
nodeAt Id
i (ASG (Id
_, Map Id ASGNode
mappings)) = Maybe ASGNode -> ASGNode
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe ASGNode -> ASGNode)
-> (Map Id ASGNode -> Maybe ASGNode) -> Map Id ASGNode -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Map Id ASGNode -> Maybe ASGNode
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id ASGNode -> ASGNode) -> Map Id ASGNode -> ASGNode
forall a b. (a -> b) -> a -> b
$ Map Id ASGNode
mappings

-- | The environment used when \'building up\' an 'ASG'. This type is exposed
-- only for testing, or debugging, and should /not/ be used in general by those
-- who just want to build an 'ASG'.
--
-- @since 1.2.0
data ASGEnv = ASGEnv ScopeInfo (Map TyName (DatatypeInfo AbstractTy))

-- | @since 1.2.0
instance
  (k ~ A_Lens, a ~ ScopeInfo, b ~ ScopeInfo) =>
  LabelOptic "scopeInfo" k ASGEnv ASGEnv a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx ASGEnv ASGEnv a b
labelOptic =
    (ASGEnv -> a) -> (ASGEnv -> b -> ASGEnv) -> Lens ASGEnv ASGEnv a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(ASGEnv ScopeInfo
si Map TyName (DatatypeInfo AbstractTy)
_) -> a
ScopeInfo
si)
      (\(ASGEnv ScopeInfo
_ Map TyName (DatatypeInfo AbstractTy)
dti) b
si -> ScopeInfo -> Map TyName (DatatypeInfo AbstractTy) -> ASGEnv
ASGEnv b
ScopeInfo
si Map TyName (DatatypeInfo AbstractTy)
dti)

-- | @since 1.2.0
instance
  (k ~ A_Lens, a ~ Map TyName (DatatypeInfo AbstractTy), b ~ Map TyName (DatatypeInfo AbstractTy)) =>
  LabelOptic "datatypeInfo" k ASGEnv ASGEnv a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx ASGEnv ASGEnv a b
labelOptic =
    (ASGEnv -> a) -> (ASGEnv -> b -> ASGEnv) -> Lens ASGEnv ASGEnv a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(ASGEnv ScopeInfo
_ Map TyName (DatatypeInfo AbstractTy)
dti) -> a
Map TyName (DatatypeInfo AbstractTy)
dti)
      (\(ASGEnv ScopeInfo
si Map TyName (DatatypeInfo AbstractTy)
_) b
dti -> ScopeInfo -> Map TyName (DatatypeInfo AbstractTy) -> ASGEnv
ASGEnv ScopeInfo
si b
Map TyName (DatatypeInfo AbstractTy)
dti)

-- | A tracker for scope-related information while building an ASG
-- programmatically. Currently only tracks available arguments.
--
-- = Important note
--
-- This is a fairly low-level type, designed specifically for ASG construction.
-- While you can do arbitrary things with it, changing things in it outside of
-- the functionality provided by this module is not recommended, unless you know
-- /exactly/ what you're doing.
--
-- @since 1.2.0
newtype ScopeInfo = ScopeInfo (Vector (Word32, Vector (ValT AbstractTy)))
  deriving stock
    ( -- | @since 1.0.0
      ScopeInfo -> ScopeInfo -> Bool
(ScopeInfo -> ScopeInfo -> Bool)
-> (ScopeInfo -> ScopeInfo -> Bool) -> Eq ScopeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopeInfo -> ScopeInfo -> Bool
== :: ScopeInfo -> ScopeInfo -> Bool
$c/= :: ScopeInfo -> ScopeInfo -> Bool
/= :: ScopeInfo -> ScopeInfo -> Bool
Eq,
      -- | @since 1.0.0
      Int -> ScopeInfo -> ShowS
[ScopeInfo] -> ShowS
ScopeInfo -> [Char]
(Int -> ScopeInfo -> ShowS)
-> (ScopeInfo -> [Char])
-> ([ScopeInfo] -> ShowS)
-> Show ScopeInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeInfo -> ShowS
showsPrec :: Int -> ScopeInfo -> ShowS
$cshow :: ScopeInfo -> [Char]
show :: ScopeInfo -> [Char]
$cshowList :: [ScopeInfo] -> ShowS
showList :: [ScopeInfo] -> ShowS
Show
    )

-- | Gives access to the argument information for the current, and all
-- enclosing, scopes. The \'outer\' 'Vector' is a stack of scopes, with lower
-- indexes corresponding to closer scopes: index 0 is our scope, 1 is our
-- enclosing scope, 2 is the enclosing scope of our enclosing scope, etc. The
-- \'inner\' 'Vector's are positional lists of argument types.
--
-- @since 1.2.0
instance
  (k ~ A_Lens, a ~ Vector (Word32, Vector (ValT AbstractTy)), b ~ Vector (Word32, Vector (ValT AbstractTy))) =>
  LabelOptic "argumentInfo" k ScopeInfo ScopeInfo a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx ScopeInfo ScopeInfo a b
labelOptic = (ScopeInfo -> a)
-> (ScopeInfo -> b -> ScopeInfo) -> Lens ScopeInfo ScopeInfo a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ScopeInfo -> a
forall a b. Coercible a b => a -> b
coerce (\ScopeInfo
_ b
v -> Vector (Word32, Vector (ValT AbstractTy)) -> ScopeInfo
ScopeInfo b
Vector (Word32, Vector (ValT AbstractTy))
v)

-- | A Plutus primop with one argument.
--
-- @since 1.0.0
pattern Builtin1 :: OneArgFunc -> CompNodeInfo
pattern $mBuiltin1 :: forall {r}. CompNodeInfo -> (OneArgFunc -> r) -> ((# #) -> r) -> r
Builtin1 f <- Builtin1Internal f

-- | A Plutus primop with two arguments.
--
-- @since 1.0.0
pattern Builtin2 :: TwoArgFunc -> CompNodeInfo
pattern $mBuiltin2 :: forall {r}. CompNodeInfo -> (TwoArgFunc -> r) -> ((# #) -> r) -> r
Builtin2 f <- Builtin2Internal f

-- | A Plutus primop with three arguments.
--
-- @since 1.0.0
pattern Builtin3 :: ThreeArgFunc -> CompNodeInfo
pattern $mBuiltin3 :: forall {r}.
CompNodeInfo -> (ThreeArgFunc -> r) -> ((# #) -> r) -> r
Builtin3 f <- Builtin3Internal f

-- | A Plutus primop with six arguments.
--
-- @since 1.1.0
pattern Builtin6 :: SixArgFunc -> CompNodeInfo
pattern $mBuiltin6 :: forall {r}. CompNodeInfo -> (SixArgFunc -> r) -> ((# #) -> r) -> r
Builtin6 f <- Builtin6Internal f

-- | Force a thunk back into the computation it wraps.
--
-- @since 1.0.0
pattern Force :: Ref -> CompNodeInfo
pattern $mForce :: forall {r}. CompNodeInfo -> (Ref -> r) -> ((# #) -> r) -> r
Force r <- ForceInternal r

-- | A lambda.
--
-- @since 1.2.0
pattern Lam :: Ref -> CompNodeInfo
pattern $mLam :: forall {r}. CompNodeInfo -> (Ref -> r) -> ((# #) -> r) -> r
Lam r <- LamInternal r

{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Lam #-}

-- | A compile-time literal of a flat builtin type.
--
-- @since 1.0.0
pattern Lit :: AConstant -> ValNodeInfo
pattern $mLit :: forall {r}. ValNodeInfo -> (AConstant -> r) -> ((# #) -> r) -> r
Lit c <- LitInternal c

-- | An application of a computation (the 'Id' field) to some arguments (the
-- 'Vector' field).
--
-- @since 1.0.0
pattern App :: Id -> Vector Ref -> ValNodeInfo
pattern $mApp :: forall {r}.
ValNodeInfo -> (Id -> Vector Ref -> r) -> ((# #) -> r) -> r
App f args <- AppInternal f args

-- | Wrap a computation into a value (essentially delaying it).
--
-- @since 1.0.0
pattern Thunk :: Id -> ValNodeInfo
pattern $mThunk :: forall {r}. ValNodeInfo -> (Id -> r) -> ((# #) -> r) -> r
Thunk i <- ThunkInternal i

-- | \'Tear down\' a self-recursive value with an algebra.
--
-- @since 1.0.0
pattern Cata :: Ref -> Ref -> ValNodeInfo
pattern $mCata :: forall {r}. ValNodeInfo -> (Ref -> Ref -> r) -> ((# #) -> r) -> r
Cata algebraRef valRef <- CataInternal algebraRef valRef

-- | Inject (zero or more) fields into a data constructor
--
-- @since 1.2.0
pattern DataConstructor :: TyName -> ConstructorName -> Vector Ref -> ValNodeInfo
pattern $mDataConstructor :: forall {r}.
ValNodeInfo
-> (TyName -> ConstructorName -> Vector Ref -> r)
-> ((# #) -> r)
-> r
DataConstructor tyName ctorName fields <- DataConstructorInternal tyName ctorName fields

-- | Deconstruct a value of a data type using the supplied handlers for each arm
--
-- @since 1.2.0
pattern Match :: Ref -> Vector Ref -> ValNodeInfo
pattern $mMatch :: forall {r}.
ValNodeInfo -> (Ref -> Vector Ref -> r) -> ((# #) -> r) -> r
Match scrutinee handlers <- MatchInternal scrutinee handlers

{-# COMPLETE Lit, App, Thunk, Cata, DataConstructor, Match #-}

-- | Any problem that might arise when building an ASG programmatically.
--
-- @since 1.0.0
data CovenantError
  = -- | There was a type error when assembling the ASG. This provides the
    -- hash-consed state up to the point of the error.
    --
    -- @since 1.0.0
    TypeError (Bimap Id ASGNode) CovenantTypeError
  | -- | We tried to generate an ASG with no nodes in it.
    --
    -- @since 1.0.0
    EmptyASG
  | -- | We tried to generate as ASG whose top-level node is an error.
    --
    -- @since 1.0.0
    TopLevelError
  | -- | We tried to generate an ASG whose top-level node is a value.
    --
    -- @since 1.0.0
    TopLevelValue (Bimap Id ASGNode) (ValT AbstractTy) ValNodeInfo
  deriving stock
    ( -- | @since 1.0.0
      CovenantError -> CovenantError -> Bool
(CovenantError -> CovenantError -> Bool)
-> (CovenantError -> CovenantError -> Bool) -> Eq CovenantError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CovenantError -> CovenantError -> Bool
== :: CovenantError -> CovenantError -> Bool
$c/= :: CovenantError -> CovenantError -> Bool
/= :: CovenantError -> CovenantError -> Bool
Eq,
      -- | @since 1.0.0
      Int -> CovenantError -> ShowS
[CovenantError] -> ShowS
CovenantError -> [Char]
(Int -> CovenantError -> ShowS)
-> (CovenantError -> [Char])
-> ([CovenantError] -> ShowS)
-> Show CovenantError
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CovenantError -> ShowS
showsPrec :: Int -> CovenantError -> ShowS
$cshow :: CovenantError -> [Char]
show :: CovenantError -> [Char]
$cshowList :: [CovenantError] -> ShowS
showList :: [CovenantError] -> ShowS
Show
    )

-- | A concrete monadic stack, providing the minimum amount of functionality
-- needed to build an ASG using the combinators given in this module.
--
-- @since 1.0.0
newtype ASGBuilder (a :: Type)
  = ASGBuilder (ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a)
  deriving
    ( -- | @since 1.0.0
      (forall a b. (a -> b) -> ASGBuilder a -> ASGBuilder b)
-> (forall a b. a -> ASGBuilder b -> ASGBuilder a)
-> Functor ASGBuilder
forall a b. a -> ASGBuilder b -> ASGBuilder a
forall a b. (a -> b) -> ASGBuilder a -> ASGBuilder b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ASGBuilder a -> ASGBuilder b
fmap :: forall a b. (a -> b) -> ASGBuilder a -> ASGBuilder b
$c<$ :: forall a b. a -> ASGBuilder b -> ASGBuilder a
<$ :: forall a b. a -> ASGBuilder b -> ASGBuilder a
Functor,
      -- | @since 1.0.0
      Functor ASGBuilder
Functor ASGBuilder =>
(forall a. a -> ASGBuilder a)
-> (forall a b.
    ASGBuilder (a -> b) -> ASGBuilder a -> ASGBuilder b)
-> (forall a b c.
    (a -> b -> c) -> ASGBuilder a -> ASGBuilder b -> ASGBuilder c)
-> (forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b)
-> (forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder a)
-> Applicative ASGBuilder
forall a. a -> ASGBuilder a
forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder a
forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
forall a b. ASGBuilder (a -> b) -> ASGBuilder a -> ASGBuilder b
forall a b c.
(a -> b -> c) -> ASGBuilder a -> ASGBuilder b -> ASGBuilder c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> ASGBuilder a
pure :: forall a. a -> ASGBuilder a
$c<*> :: forall a b. ASGBuilder (a -> b) -> ASGBuilder a -> ASGBuilder b
<*> :: forall a b. ASGBuilder (a -> b) -> ASGBuilder a -> ASGBuilder b
$cliftA2 :: forall a b c.
(a -> b -> c) -> ASGBuilder a -> ASGBuilder b -> ASGBuilder c
liftA2 :: forall a b c.
(a -> b -> c) -> ASGBuilder a -> ASGBuilder b -> ASGBuilder c
$c*> :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
*> :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
$c<* :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder a
<* :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder a
Applicative,
      -- | @since 1.0.0
      Applicative ASGBuilder
Applicative ASGBuilder =>
(forall a b. ASGBuilder a -> (a -> ASGBuilder b) -> ASGBuilder b)
-> (forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b)
-> (forall a. a -> ASGBuilder a)
-> Monad ASGBuilder
forall a. a -> ASGBuilder a
forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
forall a b. ASGBuilder a -> (a -> ASGBuilder b) -> ASGBuilder b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. ASGBuilder a -> (a -> ASGBuilder b) -> ASGBuilder b
>>= :: forall a b. ASGBuilder a -> (a -> ASGBuilder b) -> ASGBuilder b
$c>> :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
>> :: forall a b. ASGBuilder a -> ASGBuilder b -> ASGBuilder b
$creturn :: forall a. a -> ASGBuilder a
return :: forall a. a -> ASGBuilder a
Monad,
      -- | @since 1.1.0
      MonadReader ASGEnv,
      -- | @since 1.0.0
      MonadError CovenantTypeError,
      -- | @since 1.0.0
      MonadHashCons Id ASGNode
    )
    via ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))

-- | A standard collection of types required for almost any realistic script.
-- This includes non-\'flat\' builtin types (such as lists and pairs), as well
-- as all types required by the ledger (including types like @Maybe@).
--
-- @since 1.1.0
defaultDatatypes :: Map TyName (DatatypeInfo AbstractTy)
defaultDatatypes :: Map TyName (DatatypeInfo AbstractTy)
defaultDatatypes = (DataDeclaration AbstractTy
 -> Map TyName (DatatypeInfo AbstractTy))
-> [DataDeclaration AbstractTy]
-> Map TyName (DatatypeInfo AbstractTy)
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
go [DataDeclaration AbstractTy]
ledgerTypes
  where
    go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
    go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
go DataDeclaration AbstractTy
decl = case DataDeclaration AbstractTy
-> Either BBFError (DatatypeInfo AbstractTy)
mkDatatypeInfo DataDeclaration AbstractTy
decl of
      Left BBFError
err' -> [Char] -> Map TyName (DatatypeInfo AbstractTy)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Map TyName (DatatypeInfo AbstractTy))
-> [Char] -> Map TyName (DatatypeInfo AbstractTy)
forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected failure in default datatypes: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> BBFError -> [Char]
forall a. Show a => a -> [Char]
show BBFError
err'
      Right DatatypeInfo AbstractTy
info -> TyName
-> DatatypeInfo AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
forall k a. k -> a -> Map k a
Map.singleton (Optic' A_Lens NoIx (DataDeclaration AbstractTy) TyName
-> DataDeclaration AbstractTy -> TyName
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (DataDeclaration AbstractTy) TyName
#datatypeName DataDeclaration AbstractTy
decl) DatatypeInfo AbstractTy
info

-- | Executes an 'ASGBuilder' to make a \'finished\' ASG.
--
-- @since 1.0.0
runASGBuilder ::
  forall (a :: Type).
  Map TyName (DatatypeInfo AbstractTy) ->
  ASGBuilder a ->
  Either CovenantError ASG
runASGBuilder :: forall a.
Map TyName (DatatypeInfo AbstractTy)
-> ASGBuilder a -> Either CovenantError ASG
runASGBuilder Map TyName (DatatypeInfo AbstractTy)
tyDict (ASGBuilder ReaderT
  ASGEnv
  (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))
  a
comp) =
  case Identity (Either CovenantTypeError a, Bimap Id ASGNode)
-> (Either CovenantTypeError a, Bimap Id ASGNode)
forall a. Identity a -> a
runIdentity (Identity (Either CovenantTypeError a, Bimap Id ASGNode)
 -> (Either CovenantTypeError a, Bimap Id ASGNode))
-> (ASGEnv
    -> Identity (Either CovenantTypeError a, Bimap Id ASGNode))
-> ASGEnv
-> (Either CovenantTypeError a, Bimap Id ASGNode)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashConsT Id ASGNode Identity (Either CovenantTypeError a)
-> Identity (Either CovenantTypeError a, Bimap Id ASGNode)
forall r e (m :: Type -> Type) a.
HashConsT r e m a -> m (a, Bimap r e)
runHashConsT (HashConsT Id ASGNode Identity (Either CovenantTypeError a)
 -> Identity (Either CovenantTypeError a, Bimap Id ASGNode))
-> (ASGEnv
    -> HashConsT Id ASGNode Identity (Either CovenantTypeError a))
-> ASGEnv
-> Identity (Either CovenantTypeError a, Bimap Id ASGNode)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT CovenantTypeError (HashConsT Id ASGNode Identity) a
-> HashConsT Id ASGNode Identity (Either CovenantTypeError a)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity) a
 -> HashConsT Id ASGNode Identity (Either CovenantTypeError a))
-> (ASGEnv
    -> ExceptT CovenantTypeError (HashConsT Id ASGNode Identity) a)
-> ASGEnv
-> HashConsT Id ASGNode Identity (Either CovenantTypeError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT
  ASGEnv
  (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))
  a
-> ASGEnv
-> ExceptT CovenantTypeError (HashConsT Id ASGNode Identity) a
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ReaderT
  ASGEnv
  (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))
  a
comp (ASGEnv -> (Either CovenantTypeError a, Bimap Id ASGNode))
-> ASGEnv -> (Either CovenantTypeError a, Bimap Id ASGNode)
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> Map TyName (DatatypeInfo AbstractTy) -> ASGEnv
ASGEnv (Vector (Word32, Vector (ValT AbstractTy)) -> ScopeInfo
ScopeInfo Vector (Word32, Vector (ValT AbstractTy))
forall a. Vector a
Vector.empty) Map TyName (DatatypeInfo AbstractTy)
tyDict of
    (Either CovenantTypeError a
result, Bimap Id ASGNode
bm) -> case Either CovenantTypeError a
result of
      Left CovenantTypeError
err' -> CovenantError -> Either CovenantError ASG
forall a b. a -> Either a b
Left (CovenantError -> Either CovenantError ASG)
-> (CovenantTypeError -> CovenantError)
-> CovenantTypeError
-> Either CovenantError ASG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap Id ASGNode -> CovenantTypeError -> CovenantError
TypeError Bimap Id ASGNode
bm (CovenantTypeError -> Either CovenantError ASG)
-> CovenantTypeError -> Either CovenantError ASG
forall a b. (a -> b) -> a -> b
$ CovenantTypeError
err'
      Right a
_ -> case Bimap Id ASGNode -> Int
forall a b. Bimap a b -> Int
Bimap.size Bimap Id ASGNode
bm of
        Int
0 -> CovenantError -> Either CovenantError ASG
forall a b. a -> Either a b
Left CovenantError
EmptyASG
        Int
_ -> do
          let (Id
i, ASGNode
rootNode') = Bimap Id ASGNode -> (Id, ASGNode)
forall a b. Bimap a b -> (a, b)
Bimap.findMax Bimap Id ASGNode
bm
          case ASGNode
rootNode' of
            ASGNode
AnError -> CovenantError -> Either CovenantError ASG
forall a b. a -> Either a b
Left CovenantError
TopLevelError
            ACompNode CompT AbstractTy
_ CompNodeInfo
_ -> ASG -> Either CovenantError ASG
forall a. a -> Either CovenantError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ASG -> Either CovenantError ASG)
-> ((Id, Map Id ASGNode) -> ASG)
-> (Id, Map Id ASGNode)
-> Either CovenantError ASG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Map Id ASGNode) -> ASG
ASG ((Id, Map Id ASGNode) -> Either CovenantError ASG)
-> (Id, Map Id ASGNode) -> Either CovenantError ASG
forall a b. (a -> b) -> a -> b
$ (Id
i, Bimap Id ASGNode -> Map Id ASGNode
forall a b. Bimap a b -> Map a b
Bimap.toMap Bimap Id ASGNode
bm)
            AValNode ValT AbstractTy
t ValNodeInfo
info -> CovenantError -> Either CovenantError ASG
forall a b. a -> Either a b
Left (CovenantError -> Either CovenantError ASG)
-> (ValNodeInfo -> CovenantError)
-> ValNodeInfo
-> Either CovenantError ASG
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bimap Id ASGNode -> ValT AbstractTy -> ValNodeInfo -> CovenantError
TopLevelValue Bimap Id ASGNode
bm ValT AbstractTy
t (ValNodeInfo -> Either CovenantError ASG)
-> ValNodeInfo -> Either CovenantError ASG
forall a b. (a -> b) -> a -> b
$ ValNodeInfo
info

-- | Given a scope and a positional argument index, construct that argument.
-- Will fail if that argument doesn't exist in the specified scope, or if the
-- specified scope doesn't exist.
--
-- @since 1.0.0
arg ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  DeBruijn ->
  Index "arg" ->
  m Arg
arg :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
DeBruijn -> Index "arg" -> m Arg
arg DeBruijn
scope Index "arg"
index = do
  let scopeAsInt :: Int
scopeAsInt = Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
scope
  let indexAsInt :: Int
indexAsInt = Optic' A_Prism NoIx Int (Index "arg") -> Index "arg" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "arg")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "arg"
index
  Maybe (ValT AbstractTy)
lookedUp <- (ASGEnv -> Maybe (ValT AbstractTy)) -> m (Maybe (ValT AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' An_AffineTraversal NoIx ASGEnv (ValT AbstractTy)
-> ASGEnv -> Maybe (ValT AbstractTy)
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
#scopeInfo Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
-> Optic
     A_Lens
     NoIx
     ScopeInfo
     ScopeInfo
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     A_Lens
     NoIx
     ASGEnv
     ASGEnv
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
#argumentInfo Optic
  A_Lens
  NoIx
  ASGEnv
  ASGEnv
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Word32, Vector (ValT AbstractTy))))
     NoIx
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
-> Optic
     An_AffineTraversal
     NoIx
     ASGEnv
     ASGEnv
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Word32, Vector (ValT AbstractTy))))
     NoIx
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (Vector (Word32, Vector (ValT AbstractTy)))
scopeAsInt Optic
  An_AffineTraversal
  NoIx
  ASGEnv
  ASGEnv
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
-> Optic
     A_Lens
     NoIx
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (Vector (ValT AbstractTy))
     (Vector (ValT AbstractTy))
-> Optic
     An_AffineTraversal
     NoIx
     ASGEnv
     ASGEnv
     (Vector (ValT AbstractTy))
     (Vector (ValT AbstractTy))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  (Vector (ValT AbstractTy))
  (Vector (ValT AbstractTy))
forall s t a b. Field2 s t a b => Lens s t a b
_2 Optic
  An_AffineTraversal
  NoIx
  ASGEnv
  ASGEnv
  (Vector (ValT AbstractTy))
  (Vector (ValT AbstractTy))
-> Optic
     (IxKind (Vector (ValT AbstractTy)))
     NoIx
     (Vector (ValT AbstractTy))
     (Vector (ValT AbstractTy))
     (ValT AbstractTy)
     (ValT AbstractTy)
-> Optic' An_AffineTraversal NoIx ASGEnv (ValT AbstractTy)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Vector (ValT AbstractTy))
-> Optic'
     (IxKind (Vector (ValT AbstractTy)))
     NoIx
     (Vector (ValT AbstractTy))
     (IxValue (Vector (ValT AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (Vector (ValT AbstractTy))
indexAsInt))
  case Maybe (ValT AbstractTy)
lookedUp of
    Maybe (ValT AbstractTy)
Nothing -> CovenantTypeError -> m Arg
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Arg)
-> (Index "arg" -> CovenantTypeError) -> Index "arg" -> m Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "arg" -> CovenantTypeError
NoSuchArgument DeBruijn
scope (Index "arg" -> m Arg) -> Index "arg" -> m Arg
forall a b. (a -> b) -> a -> b
$ Index "arg"
index
    Just ValT AbstractTy
t -> Arg -> m Arg
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Arg -> m Arg)
-> (ValT AbstractTy -> Arg) -> ValT AbstractTy -> m Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "arg" -> ValT AbstractTy -> Arg
Arg DeBruijn
scope Index "arg"
index (ValT AbstractTy -> m Arg) -> ValT AbstractTy -> m Arg
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t

-- | Construct a node corresponding to the given Plutus primop.
--
-- @since 1.0.0
builtin1 ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  OneArgFunc ->
  m Id
builtin1 :: forall (m :: Type -> Type).
MonadHashCons Id ASGNode m =>
OneArgFunc -> m Id
builtin1 OneArgFunc
bi = do
  let node :: ASGNode
node = CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode (OneArgFunc -> CompT AbstractTy
typeOneArgFunc OneArgFunc
bi) (CompNodeInfo -> ASGNode)
-> (OneArgFunc -> CompNodeInfo) -> OneArgFunc -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneArgFunc -> CompNodeInfo
Builtin1Internal (OneArgFunc -> ASGNode) -> OneArgFunc -> ASGNode
forall a b. (a -> b) -> a -> b
$ OneArgFunc
bi
  ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo ASGNode
node

-- | As 'builtin1', but for two-argument primops.
--
-- @since 1.0.0
builtin2 ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  TwoArgFunc ->
  m Id
builtin2 :: forall (m :: Type -> Type).
MonadHashCons Id ASGNode m =>
TwoArgFunc -> m Id
builtin2 TwoArgFunc
bi = do
  let node :: ASGNode
node = CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode (TwoArgFunc -> CompT AbstractTy
typeTwoArgFunc TwoArgFunc
bi) (CompNodeInfo -> ASGNode)
-> (TwoArgFunc -> CompNodeInfo) -> TwoArgFunc -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TwoArgFunc -> CompNodeInfo
Builtin2Internal (TwoArgFunc -> ASGNode) -> TwoArgFunc -> ASGNode
forall a b. (a -> b) -> a -> b
$ TwoArgFunc
bi
  ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo ASGNode
node

-- | As 'builtin1', but for three-argument primops.
--
-- @since 1.0.0
builtin3 ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  ThreeArgFunc ->
  m Id
builtin3 :: forall (m :: Type -> Type).
MonadHashCons Id ASGNode m =>
ThreeArgFunc -> m Id
builtin3 ThreeArgFunc
bi = do
  let node :: ASGNode
node = CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode (ThreeArgFunc -> CompT AbstractTy
typeThreeArgFunc ThreeArgFunc
bi) (CompNodeInfo -> ASGNode)
-> (ThreeArgFunc -> CompNodeInfo) -> ThreeArgFunc -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreeArgFunc -> CompNodeInfo
Builtin3Internal (ThreeArgFunc -> ASGNode) -> ThreeArgFunc -> ASGNode
forall a b. (a -> b) -> a -> b
$ ThreeArgFunc
bi
  ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo ASGNode
node

-- | As 'builtin1', but for six-argument primops.
--
-- @since 1.1.0
builtin6 ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  SixArgFunc ->
  m Id
builtin6 :: forall (m :: Type -> Type).
MonadHashCons Id ASGNode m =>
SixArgFunc -> m Id
builtin6 SixArgFunc
bi = do
  let node :: ASGNode
node = CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode (SixArgFunc -> CompT AbstractTy
typeSixArgFunc SixArgFunc
bi) (CompNodeInfo -> ASGNode)
-> (SixArgFunc -> CompNodeInfo) -> SixArgFunc -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SixArgFunc -> CompNodeInfo
Builtin6Internal (SixArgFunc -> ASGNode) -> SixArgFunc -> ASGNode
forall a b. (a -> b) -> a -> b
$ SixArgFunc
bi
  ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo ASGNode
node

-- | Given a reference to a thunk, turn it back into a computation. Will fail if
-- the reference isn't a thunk.
--
-- @since 1.0.0
force ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Ref ->
  m Id
force :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m Id
force Ref
r = do
  ASGNodeType
refT <- Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
r
  case ASGNodeType
refT of
    ValNodeType ValT AbstractTy
t -> case ValT AbstractTy
t of
      ThunkT CompT AbstractTy
compT -> ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Ref -> ASGNode) -> Ref -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode CompT AbstractTy
compT (CompNodeInfo -> ASGNode)
-> (Ref -> CompNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> CompNodeInfo
ForceInternal (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
r
      ValT AbstractTy
_ -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
ForceNonThunk (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t
    CompNodeType CompT AbstractTy
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
ForceCompType (CompT AbstractTy -> m Id) -> CompT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t
    ASGNodeType
ErrorNodeType -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError CovenantTypeError
ForceError

-- | Given a desired type, and a computation which will construct a lambda body
-- when executed (with the scope extended with the arguments the functions can
-- expect), construct a lambda.
--
-- = Important note
--
-- This combinator works slightly differently to the others in this module. This
-- is required because, due to hash consing, an ASG is typically built
-- \'bottom-up\', whereas function arguments (and their scopes) are necessarily
-- top-down. Thus, we need to \'delay\' the construction of a lambda's body to
-- ensure that proper scoped argument information can be given to it, hence why
-- the argument being passed is an @m Ref@.
--
-- @since 1.2.0
lam ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  CompT AbstractTy ->
  m Ref ->
  m Id
lam :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
CompT AbstractTy -> m Ref -> m Id
lam expectedT :: CompT AbstractTy
expectedT@(CompT Count "tyvar"
cnt (CompTBody NonEmptyVector (ValT AbstractTy)
xs)) m Ref
bodyComp = do
  let (Vector (ValT AbstractTy)
args, ValT AbstractTy
resultT) = NonEmptyVector (ValT AbstractTy)
-> (Vector (ValT AbstractTy), ValT AbstractTy)
forall a. NonEmptyVector a -> (Vector a, a)
NonEmpty.unsnoc NonEmptyVector (ValT AbstractTy)
xs
      cntW :: Word32
cntW = Optic' A_Lens NoIx (Count "tyvar") Word32
-> Count "tyvar" -> Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Count "tyvar") Word32
forall (ofWhat :: Symbol). Lens' (Count ofWhat) Word32
wordCount Count "tyvar"
cnt
  Ref
bodyRef <- (ASGEnv -> ASGEnv) -> m Ref -> m Ref
forall a. (ASGEnv -> ASGEnv) -> m a -> m a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic
  A_Lens
  NoIx
  ASGEnv
  ASGEnv
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
-> (Vector (Word32, Vector (ValT AbstractTy))
    -> Vector (Word32, Vector (ValT AbstractTy)))
-> ASGEnv
-> ASGEnv
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over (Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
#scopeInfo Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
-> Optic
     A_Lens
     NoIx
     ScopeInfo
     ScopeInfo
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     A_Lens
     NoIx
     ASGEnv
     ASGEnv
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
#argumentInfo) ((Word32, Vector (ValT AbstractTy))
-> Vector (Word32, Vector (ValT AbstractTy))
-> Vector (Word32, Vector (ValT AbstractTy))
forall a. a -> Vector a -> Vector a
Vector.cons (Word32
cntW, Vector (ValT AbstractTy)
args))) m Ref
bodyComp
  case Ref
bodyRef of
    AnArg (Arg DeBruijn
_ Index "arg"
_ ValT AbstractTy
argTy) -> do
      if ValT AbstractTy
argTy ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
resultT
        then ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Ref -> ASGNode) -> Ref -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode CompT AbstractTy
expectedT (CompNodeInfo -> ASGNode)
-> (Ref -> CompNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> CompNodeInfo
LamInternal (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
bodyRef
        else CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValT AbstractTy -> CovenantTypeError
WrongReturnType ValT AbstractTy
resultT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
argTy
    AnId Id
bodyId ->
      Id -> m (Maybe ASGNode)
forall r e (m :: Type -> Type).
MonadHashCons r e m =>
r -> m (Maybe e)
lookupRef Id
bodyId m (Maybe ASGNode) -> (Maybe ASGNode -> m Id) -> m Id
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe ASGNode
Nothing -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (Id -> CovenantTypeError) -> Id -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> CovenantTypeError
BrokenIdReference (Id -> m Id) -> Id -> m Id
forall a b. (a -> b) -> a -> b
$ Id
bodyId
        -- This unifies with anything, so we're fine
        Just ASGNode
AnError -> ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Id -> ASGNode) -> Id -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode CompT AbstractTy
expectedT (CompNodeInfo -> ASGNode) -> (Id -> CompNodeInfo) -> Id -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> CompNodeInfo
LamInternal (Ref -> CompNodeInfo) -> (Id -> Ref) -> Id -> CompNodeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Ref
AnId (Id -> m Id) -> Id -> m Id
forall a b. (a -> b) -> a -> b
$ Id
bodyId
        Just (AValNode ValT AbstractTy
ty ValNodeInfo
_) -> do
          if ValT AbstractTy
ty ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
resultT
            then ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Id -> ASGNode) -> Id -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CompNodeInfo -> ASGNode
ACompNode CompT AbstractTy
expectedT (CompNodeInfo -> ASGNode) -> (Id -> CompNodeInfo) -> Id -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> CompNodeInfo
LamInternal (Ref -> CompNodeInfo) -> (Id -> Ref) -> Id -> CompNodeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Ref
AnId (Id -> m Id) -> Id -> m Id
forall a b. (a -> b) -> a -> b
$ Id
bodyId
            else CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValT AbstractTy -> CovenantTypeError
WrongReturnType ValT AbstractTy
resultT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
ty
        Just (ACompNode CompT AbstractTy
t CompNodeInfo
_) -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id) -> CovenantTypeError -> m Id
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy -> CovenantTypeError
LambdaResultsInCompType CompT AbstractTy
t

-- | Construct the error node.
--
-- @since 1.0.0
err ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  m Id
err :: forall (m :: Type -> Type). MonadHashCons Id ASGNode m => m Id
err = ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo ASGNode
AnError

-- | Performs both term and type application. More precisely, given:
--
-- * An 'Id' referring to a computation; and
-- * A 'Vector' of 'Ref's for the desired term arguments to the computation, in
--   order; and
-- * A 'Vector' of (optional) type arguments to the computation, also in order.
--
-- we produce the result of that application.
--
-- This can fail for a range of reasons:
--
-- * Type mismatch between what the computation expects and what it's given
-- * Too many or too few arguments
-- * Not a computation type for 'Id' argument
-- * Not value types for 'Ref's
-- * Renaming failures (likely due to a malformed function or argument type)
--
-- = Note
--
-- We use the 'Wedge' data type to designate type arguments, as it can represent
-- the three possibilities we need:
--
-- * \'Infer this argument\', specified as 'Nowhere'.
-- * \'Use this type variable in our scope\', specified as 'Here'.
-- * \'Use this concrete type\', specified as 'There'.
--
-- @since 1.2.0
app ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  Id ->
  Vector Ref ->
  Vector (Wedge BoundTyVar (ValT Void)) ->
  m Id
app :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Id -> Vector Ref -> Vector (Wedge BoundTyVar (ValT Void)) -> m Id
app Id
fId Vector Ref
argRefs Vector (Wedge BoundTyVar (ValT Void))
instTys = do
  ASGNodeType
lookedUp <- Id -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
fId
  let rawSubs :: [(Index "tyvar", ValT AbstractTy)]
rawSubs = Vector (Wedge BoundTyVar (ValT Void))
-> [(Index "tyvar", ValT AbstractTy)]
mkSubstitutions Vector (Wedge BoundTyVar (ValT Void))
instTys
  [(Index "tyvar", ValT Renamed)]
subs <- [(Index "tyvar", ValT AbstractTy)]
-> m [(Index "tyvar", ValT Renamed)]
renameSubs [(Index "tyvar", ValT AbstractTy)]
rawSubs
  Vector Word32
scopeInfo <- m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope
  case ASGNodeType
lookedUp of
    CompNodeType CompT AbstractTy
fT -> case Vector Word32
-> RenameM (CompT Renamed) -> Either RenameError (CompT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (RenameM (CompT Renamed) -> Either RenameError (CompT Renamed))
-> (CompT AbstractTy -> RenameM (CompT Renamed))
-> CompT AbstractTy
-> Either RenameError (CompT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT (CompT AbstractTy -> Either RenameError (CompT Renamed))
-> CompT AbstractTy -> Either RenameError (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
fT of
      Left RenameError
err' -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (RenameError -> CovenantTypeError) -> RenameError -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameError -> CovenantTypeError
RenameFunctionFailed CompT AbstractTy
fT (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
      Right CompT Renamed
renamedFT -> do
        CompT Renamed
instantiatedFT <- [(Index "tyvar", ValT Renamed)]
-> CompT Renamed -> m (CompT Renamed)
instantiate [(Index "tyvar", ValT Renamed)]
subs CompT Renamed
renamedFT
        Vector (Maybe (ValT Renamed))
renamedArgs <- (Ref -> m (Maybe (ValT Renamed)))
-> Vector Ref -> m (Vector (Maybe (ValT Renamed)))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Ref -> m (Maybe (ValT Renamed))
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Vector Ref
argRefs
        Map TyName (DatatypeInfo AbstractTy)
tyDict <- (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo)
        ValT Renamed
result <- (TypeAppError -> m (ValT Renamed))
-> (ValT Renamed -> m (ValT Renamed))
-> Either TypeAppError (ValT Renamed)
-> m (ValT Renamed)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (CovenantTypeError -> m (ValT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT Renamed))
-> (TypeAppError -> CovenantTypeError)
-> TypeAppError
-> m (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAppError -> CovenantTypeError
UnificationError) ValT Renamed -> m (ValT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either TypeAppError (ValT Renamed) -> m (ValT Renamed))
-> Either TypeAppError (ValT Renamed) -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
instantiatedFT (Vector (Maybe (ValT Renamed)) -> [Maybe (ValT Renamed)]
forall a. Vector a -> [a]
Vector.toList Vector (Maybe (ValT Renamed))
renamedArgs)
        ValT AbstractTy
restored <- ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
result
        Map TyName (DatatypeInfo AbstractTy) -> ValT AbstractTy -> m ()
forall a (m :: Type -> Type).
MonadError CovenantTypeError m =>
Map TyName (DatatypeInfo a) -> ValT AbstractTy -> m ()
checkEncodingWithInfo Map TyName (DatatypeInfo AbstractTy)
tyDict ValT AbstractTy
restored
        ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Vector Ref -> ASGNode) -> Vector Ref -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
restored (ValNodeInfo -> ASGNode)
-> (Vector Ref -> ValNodeInfo) -> Vector Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Vector Ref -> ValNodeInfo
AppInternal Id
fId (Vector Ref -> m Id) -> Vector Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Vector Ref
argRefs
    ValNodeType ValT AbstractTy
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
ApplyToValType (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t
    ASGNodeType
ErrorNodeType -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError CovenantTypeError
ApplyToError
  where
    mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void)) -> [(Index "tyvar", ValT AbstractTy)]
    mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void))
-> [(Index "tyvar", ValT AbstractTy)]
mkSubstitutions =
      ([(Index "tyvar", ValT AbstractTy)]
 -> Int
 -> Wedge BoundTyVar (ValT Void)
 -> [(Index "tyvar", ValT AbstractTy)])
-> [(Index "tyvar", ValT AbstractTy)]
-> Vector (Wedge BoundTyVar (ValT Void))
-> [(Index "tyvar", ValT AbstractTy)]
forall a b. (a -> Int -> b -> a) -> a -> Vector b -> a
Vector.ifoldl'
        ( \[(Index "tyvar", ValT AbstractTy)]
acc Int
i' Wedge BoundTyVar (ValT Void)
w ->
            let i :: Index "tyvar"
i = Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Int
i'
             in [(Index "tyvar", ValT AbstractTy)]
-> (BoundTyVar -> [(Index "tyvar", ValT AbstractTy)])
-> (ValT Void -> [(Index "tyvar", ValT AbstractTy)])
-> Wedge BoundTyVar (ValT Void)
-> [(Index "tyvar", ValT AbstractTy)]
forall c a b. c -> (a -> c) -> (b -> c) -> Wedge a b -> c
wedge
                  [(Index "tyvar", ValT AbstractTy)]
acc
                  (\(BoundTyVar DeBruijn
dbIx Index "tyvar"
posIx) -> (Index "tyvar"
i, DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar DeBruijn
dbIx Index "tyvar"
posIx) (Index "tyvar", ValT AbstractTy)
-> [(Index "tyvar", ValT AbstractTy)]
-> [(Index "tyvar", ValT AbstractTy)]
forall a. a -> [a] -> [a]
: [(Index "tyvar", ValT AbstractTy)]
acc)
                  (\ValT Void
v -> (Index "tyvar"
i, ValT Void -> ValT AbstractTy
forall (f :: Type -> Type) a. Functor f => f Void -> f a
vacuous ValT Void
v) (Index "tyvar", ValT AbstractTy)
-> [(Index "tyvar", ValT AbstractTy)]
-> [(Index "tyvar", ValT AbstractTy)]
forall a. a -> [a] -> [a]
: [(Index "tyvar", ValT AbstractTy)]
acc)
                  Wedge BoundTyVar (ValT Void)
w
        )
        []

    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
    renameSubs :: [(Index "tyvar", ValT AbstractTy)]
-> m [(Index "tyvar", ValT Renamed)]
renameSubs [(Index "tyvar", ValT AbstractTy)]
subs =
      m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope m (Vector Word32)
-> (Vector Word32 -> m [(Index "tyvar", ValT Renamed)])
-> m [(Index "tyvar", ValT Renamed)]
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Vector Word32
scope -> case ((Index "tyvar", ValT AbstractTy)
 -> Either RenameError (Index "tyvar", ValT Renamed))
-> [(Index "tyvar", ValT AbstractTy)]
-> Either RenameError [(Index "tyvar", ValT Renamed)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((ValT AbstractTy -> Either RenameError (ValT Renamed))
-> (Index "tyvar", ValT AbstractTy)
-> Either RenameError (Index "tyvar", ValT Renamed)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> (Index "tyvar", a) -> f (Index "tyvar", b)
traverse (Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (RenameM (ValT Renamed) -> Either RenameError (ValT Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> ValT AbstractTy
-> Either RenameError (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT)) [(Index "tyvar", ValT AbstractTy)]
subs of
        Left RenameError
err' -> CovenantTypeError -> m [(Index "tyvar", ValT Renamed)]
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m [(Index "tyvar", ValT Renamed)])
-> CovenantTypeError -> m [(Index "tyvar", ValT Renamed)]
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
FailedToRenameInstantiation RenameError
err'
        Right [(Index "tyvar", ValT Renamed)]
res -> [(Index "tyvar", ValT Renamed)]
-> m [(Index "tyvar", ValT Renamed)]
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [(Index "tyvar", ValT Renamed)]
res

    instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
    instantiate :: [(Index "tyvar", ValT Renamed)]
-> CompT Renamed -> m (CompT Renamed)
instantiate [] CompT Renamed
fn = CompT Renamed -> m (CompT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CompT Renamed
fn
    instantiate [(Index "tyvar", ValT Renamed)]
subs CompT Renamed
fn = do
      ValT Renamed
instantiated <- UnifyM (ValT Renamed) -> m (ValT Renamed)
forall (m :: Type -> Type) a.
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
UnifyM a -> m a
liftUnifyM (UnifyM (ValT Renamed) -> m (ValT Renamed))
-> (ValT Renamed -> UnifyM (ValT Renamed))
-> ValT Renamed
-> m (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> UnifyM (ValT Renamed)
fixUp (ValT Renamed -> m (ValT Renamed))
-> ValT Renamed -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ((Index "tyvar", ValT Renamed) -> ValT Renamed -> ValT Renamed)
-> ValT Renamed -> [(Index "tyvar", ValT Renamed)] -> ValT Renamed
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Index "tyvar"
i, ValT Renamed
t) ValT Renamed
f -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
t ValT Renamed
f) (CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT CompT Renamed
fn) [(Index "tyvar", ValT Renamed)]
subs
      case ValT Renamed
instantiated of
        ThunkT CompT Renamed
res -> CompT Renamed -> m (CompT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CompT Renamed
res
        ValT Renamed
other ->
          CovenantTypeError -> m (CompT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (CompT Renamed))
-> (Text -> CovenantTypeError) -> Text -> m (CompT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAppError -> CovenantTypeError
UnificationError (TypeAppError -> CovenantTypeError)
-> (Text -> TypeAppError) -> Text -> CovenantTypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> TypeAppError
ImpossibleHappened (Text -> m (CompT Renamed)) -> Text -> m (CompT Renamed)
forall a b. (a -> b) -> a -> b
$
            Text
"Impossible happened: Result of tyvar instantiation should be a thunk, but is: "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (ValT Renamed -> [Char]
forall a. Show a => a -> [Char]
show ValT Renamed
other)

-- | Introduce a data constructor.
--
-- The first argument is a type name (for example, @\"Maybe\"@). The second
-- argument is a constructor of that type (for example, @\"Just\"@ or
-- @\"Nothing\"@). The third argument are the values to \'fill in\' all the fields
-- of the constructor requested.
--
-- = Note
--
-- 'dataConstructor' yields thunks, which must be forced, and then possibly have
-- type arguments applied to them. The reason for this is subtle, but important.
-- Consider the @Nothing@ constructor of @Maybe@: as this has no fields, we
-- cannot use the field type to determine what the type argument to @Maybe@
-- should be in this case. As datatype terms are values, they do not bind type
-- variables, and thus, we cannot have a return type that makes sense in this
-- case.
--
-- We resolve this problem by returning a thunk. In the case of our example,
-- @Nothing@ would produce @<forall a . !Maybe a>@.
--
-- @since 1.2.0
dataConstructor ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  TyName ->
  ConstructorName ->
  Vector Ref ->
  m Id
dataConstructor :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
TyName -> ConstructorName -> Vector Ref -> m Id
dataConstructor TyName
tyName ConstructorName
ctorName Vector Ref
fields = do
  DatatypeInfo Renamed
thisTyInfo <- m (DatatypeInfo Renamed)
lookupDatatypeInfo
  let thisTyDecl :: DataDeclaration Renamed
thisTyDecl = Optic
  A_Lens
  NoIx
  (DatatypeInfo Renamed)
  (DatatypeInfo Renamed)
  (DataDeclaration Renamed)
  (DataDeclaration Renamed)
-> DatatypeInfo Renamed -> DataDeclaration Renamed
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic
  A_Lens
  NoIx
  (DatatypeInfo Renamed)
  (DatatypeInfo Renamed)
  (DataDeclaration Renamed)
  (DataDeclaration Renamed)
#originalDecl DatatypeInfo Renamed
thisTyInfo
  Vector (ValT Renamed)
renamedFieldTypes <-
    (Ref -> m (Maybe (ValT Renamed)))
-> Vector Ref -> m (Vector (Maybe (ValT Renamed)))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Ref -> m (Maybe (ValT Renamed))
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Vector Ref
fields
      m (Vector (Maybe (ValT Renamed)))
-> (Vector (Maybe (ValT Renamed)) -> m (Vector (ValT Renamed)))
-> m (Vector (ValT Renamed))
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ( \case
              Maybe (Vector (ValT Renamed))
Nothing -> CovenantTypeError -> m (Vector (ValT Renamed))
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Vector (ValT Renamed)))
-> CovenantTypeError -> m (Vector (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ TyName -> ConstructorName -> Vector Ref -> CovenantTypeError
IntroFormErrorNodeField TyName
tyName ConstructorName
ctorName Vector Ref
fields
              Just Vector (ValT Renamed)
ok -> Vector (ValT Renamed) -> m (Vector (ValT Renamed))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Vector (ValT Renamed)
ok
          )
        (Maybe (Vector (ValT Renamed)) -> m (Vector (ValT Renamed)))
-> (Vector (Maybe (ValT Renamed)) -> Maybe (Vector (ValT Renamed)))
-> Vector (Maybe (ValT Renamed))
-> m (Vector (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Maybe (ValT Renamed)) -> Maybe (Vector (ValT Renamed))
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a.
Monad m =>
Vector (m a) -> m (Vector a)
sequence
  {- The procedures for handling a typed declared as Opaque and a "normal" type are totally different.

     For Opaque types, we just have to check that the "ConstructorName" we get corresponds to a constructor of
     PlutusData, then validate that the arguments conform with that PlutusData constructor.
  -}
  case DataDeclaration Renamed
thisTyDecl of
    OpaqueData TyName
_ Set PlutusDataConstructor
opaqueCtorSet -> do
      Set PlutusDataConstructor -> Vector (ValT Renamed) -> m ()
checkOpaqueArgs Set PlutusDataConstructor
opaqueCtorSet Vector (ValT Renamed)
renamedFieldTypes
      ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> ASGNode -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode (TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tyName Vector (ValT AbstractTy)
forall a. Monoid a => a
mempty) (TyName -> ConstructorName -> Vector Ref -> ValNodeInfo
DataConstructorInternal TyName
tyName ConstructorName
ctorName Vector Ref
fields)
    DataDeclaration TyName
_ Count "tyvar"
count Vector (Constructor Renamed)
ctors DataEncoding
_ -> do
      -- First we check that the arity of the constructor is equal to the number of fields in the decl.
      Int -> DatatypeInfo Renamed -> m ()
checkFieldArity (Vector Ref -> Int
forall a. Vector a -> Int
Vector.length Vector Ref
fields) DatatypeInfo Renamed
thisTyInfo
      -- Then we resolve the supplied field Refs, rename, and throw an error if we're passed an error node.

      -- Then we construct the return type.
      ValT Renamed
resultThunk <- Count "tyvar"
-> Vector (Constructor Renamed)
-> Vector (ValT Renamed)
-> m (ValT Renamed)
mkResultThunk Count "tyvar"
count Vector (Constructor Renamed)
ctors Vector (ValT Renamed)
renamedFieldTypes
      -- Then we undo the renaming.
      ValT AbstractTy
restored <- ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
resultThunk
      -- Then we check the compatibility of the arguments with the datatype's encoding.
      (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo) m (Map TyName (DatatypeInfo AbstractTy))
-> (Map TyName (DatatypeInfo AbstractTy) -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Map TyName (DatatypeInfo AbstractTy)
dti -> Map TyName (DatatypeInfo AbstractTy) -> ValT AbstractTy -> m ()
forall a (m :: Type -> Type).
MonadError CovenantTypeError m =>
Map TyName (DatatypeInfo a) -> ValT AbstractTy -> m ()
checkEncodingWithInfo Map TyName (DatatypeInfo AbstractTy)
dti ValT AbstractTy
restored
      -- Finally, if nothing has thrown an error, we return a reference to our result node, decorated with the
      -- return type we constructed.
      ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> ASGNode -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
restored (TyName -> ConstructorName -> Vector Ref -> ValNodeInfo
DataConstructorInternal TyName
tyName ConstructorName
ctorName Vector Ref
fields)
  where
    {- Constructs the result type of the introduction form. Arguments are:
         1. The count (number of tyvars) from the data declaration.
         2. The vector of constructors from the data declaration.
         3. The (renamed and resolved) vector of supplied arguments.

       The procedure goes like:
         1. Extract the argument types from the constructor in the declaration. Any tyvars here
            *have* to be Unifiable (unless something has slipped past the kind checker) -
            data declarations have atomic, independent scopes.
         2. Unify those with the actual, supplied field types, yielding a set of substitutions.
         3. Construct a fully abstract (i.e. parameterized only by unifiable type variables) representation of the
            type constructor.
         4. Apply those substitutions to the abstract type constructor.
         5. Wrap the "concretified" type constructor in a thunk and use `fixUp` to sort out the `Count` and
            indices.
    -}
    mkResultThunk :: Count "tyvar" -> Vector (Constructor Renamed) -> Vector (ValT Renamed) -> m (ValT Renamed)
    mkResultThunk :: Count "tyvar"
-> Vector (Constructor Renamed)
-> Vector (ValT Renamed)
-> m (ValT Renamed)
mkResultThunk Count "tyvar"
count' Vector (Constructor Renamed)
declCtors Vector (ValT Renamed)
fieldArgs' = do
      [ValT Renamed]
declCtorFields <- Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList (Vector (ValT Renamed) -> [ValT Renamed])
-> (Constructor Renamed -> Vector (ValT Renamed))
-> Constructor Renamed
-> [ValT Renamed]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx (Constructor Renamed) (Vector (ValT Renamed))
-> Constructor Renamed -> Vector (ValT Renamed)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Constructor Renamed) (Vector (ValT Renamed))
#constructorArgs (Constructor Renamed -> [ValT Renamed])
-> m (Constructor Renamed) -> m [ValT Renamed]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Constructor Renamed) -> m (Constructor Renamed)
forall (t :: Type -> Type) a.
Foldable t =>
t (Constructor a) -> m (Constructor a)
findConstructor Vector (Constructor Renamed)
declCtors
      Map (Index "tyvar") (ValT Renamed)
subs <- [ValT Renamed]
-> [ValT Renamed] -> m (Map (Index "tyvar") (ValT Renamed))
unifyFields [ValT Renamed]
declCtorFields [ValT Renamed]
fieldArgs
      let tyConAbstractArgs :: [ValT Renamed]
tyConAbstractArgs = (Int -> Maybe (ValT Renamed)) -> [Int] -> [ValT Renamed]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Index "tyvar" -> ValT Renamed)
-> Maybe (Index "tyvar") -> Maybe (ValT Renamed)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Renamed -> ValT Renamed
forall a. a -> ValT a
Abstraction (Renamed -> ValT Renamed)
-> (Index "tyvar" -> Renamed) -> Index "tyvar" -> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index "tyvar" -> Renamed
Unifiable) (Maybe (Index "tyvar") -> Maybe (ValT Renamed))
-> (Int -> Maybe (Index "tyvar")) -> Int -> Maybe (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex) [Int
0, Int
1 .. (Int
count Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
          tyConAbstract :: ValT Renamed
tyConAbstract = TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tyName ([ValT Renamed] -> Vector (ValT Renamed)
forall a. [a] -> Vector a
Vector.fromList [ValT Renamed]
tyConAbstractArgs)
      let tyConConcrete :: ValT Renamed
tyConConcrete = (ValT Renamed -> Index "tyvar" -> ValT Renamed -> ValT Renamed)
-> ValT Renamed
-> Map (Index "tyvar") (ValT Renamed)
-> ValT Renamed
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' (\ValT Renamed
acc Index "tyvar"
i ValT Renamed
t -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
t ValT Renamed
acc) ValT Renamed
tyConAbstract Map (Index "tyvar") (ValT Renamed)
subs
      UnifyM (ValT Renamed) -> m (ValT Renamed)
forall (m :: Type -> Type) a.
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
UnifyM a -> m a
liftUnifyM (UnifyM (ValT Renamed) -> m (ValT Renamed))
-> (ValT Renamed -> UnifyM (ValT Renamed))
-> ValT Renamed
-> m (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> UnifyM (ValT Renamed)
fixUp (ValT Renamed -> UnifyM (ValT Renamed))
-> (ValT Renamed -> ValT Renamed)
-> ValT Renamed
-> UnifyM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (CompT Renamed -> ValT Renamed)
-> (ValT Renamed -> CompT Renamed) -> ValT Renamed -> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompTBody Renamed -> CompT Renamed
forall a. CompTBody a -> CompT a
Comp0 (CompTBody Renamed -> CompT Renamed)
-> (ValT Renamed -> CompTBody Renamed)
-> ValT Renamed
-> CompT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> CompTBody Renamed
forall a. ValT a -> CompTBody a
ReturnT (ValT Renamed -> m (ValT Renamed))
-> ValT Renamed -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed
tyConConcrete
      where
        count :: Int
        count :: Int
count = Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
count'

        fieldArgs :: [ValT Renamed]
        fieldArgs :: [ValT Renamed]
fieldArgs = Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList Vector (ValT Renamed)
fieldArgs'

    {- Unifies the declaration fields (which may be abstract) with the supplied fields
       (which will be "concrete", in the sense that "they have to be rigid if they're tyvars").

       Returns a (reconciled) set of substitutions which can be applied to a fully-abstract (i.e.
       parameterized only by Unifiable tyVars) to yield the concrete, applied type constructor.
    -}
    unifyFields :: [ValT Renamed] -> [ValT Renamed] -> m (Map (Index "tyvar") (ValT Renamed))
    unifyFields :: [ValT Renamed]
-> [ValT Renamed] -> m (Map (Index "tyvar") (ValT Renamed))
unifyFields [ValT Renamed]
declFields [ValT Renamed]
suppliedFields = UnifyM (Map (Index "tyvar") (ValT Renamed))
-> m (Map (Index "tyvar") (ValT Renamed))
forall (m :: Type -> Type) a.
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
UnifyM a -> m a
liftUnifyM (UnifyM (Map (Index "tyvar") (ValT Renamed))
 -> m (Map (Index "tyvar") (ValT Renamed)))
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
-> m (Map (Index "tyvar") (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ do
      [Map (Index "tyvar") (ValT Renamed)]
rawSubs <- (ValT Renamed
 -> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> [ValT Renamed]
-> [ValT Renamed]
-> UnifyM [Map (Index "tyvar") (ValT Renamed)]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ValT Renamed
-> ValT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))
unify [ValT Renamed]
declFields [ValT Renamed]
suppliedFields
      (Map (Index "tyvar") (ValT Renamed)
 -> Map (Index "tyvar") (ValT Renamed)
 -> UnifyM (Map (Index "tyvar") (ValT Renamed)))
-> Map (Index "tyvar") (ValT Renamed)
-> [Map (Index "tyvar") (ValT Renamed)]
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map (Index "tyvar") (ValT Renamed)
-> Map (Index "tyvar") (ValT Renamed)
-> UnifyM (Map (Index "tyvar") (ValT Renamed))
reconcile Map (Index "tyvar") (ValT Renamed)
forall k a. Map k a
Map.empty [Map (Index "tyvar") (ValT Renamed)]
rawSubs

    {- Checks that the number of fields supplied as arguments is equal to the
       number of fields in the corresponding constructor of the data declaration.

       This is needed because `zipWithM unifyFields` won't throw an error in the case that they are not equal.
    -}
    checkFieldArity :: Int -> DatatypeInfo Renamed -> m ()
    checkFieldArity :: Int -> DatatypeInfo Renamed -> m ()
checkFieldArity Int
actualNumFields DatatypeInfo Renamed
dtInfo = do
      let ctors :: [Constructor Renamed]
ctors = Optic' A_Fold NoIx (DatatypeInfo Renamed) (Constructor Renamed)
-> DatatypeInfo Renamed -> [Constructor Renamed]
forall k (is :: IxList) s a.
Is k A_Fold =>
Optic' k is s a -> s -> [a]
toListOf (Optic
  A_Lens
  NoIx
  (DatatypeInfo Renamed)
  (DatatypeInfo Renamed)
  (DataDeclaration Renamed)
  (DataDeclaration Renamed)
#originalDecl Optic
  A_Lens
  NoIx
  (DatatypeInfo Renamed)
  (DatatypeInfo Renamed)
  (DataDeclaration Renamed)
  (DataDeclaration Renamed)
-> Optic
     A_Fold
     NoIx
     (DataDeclaration Renamed)
     (DataDeclaration Renamed)
     (Vector (Constructor Renamed))
     (Vector (Constructor Renamed))
-> Optic
     A_Fold
     NoIx
     (DatatypeInfo Renamed)
     (DatatypeInfo Renamed)
     (Vector (Constructor Renamed))
     (Vector (Constructor Renamed))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Fold
  NoIx
  (DataDeclaration Renamed)
  (DataDeclaration Renamed)
  (Vector (Constructor Renamed))
  (Vector (Constructor Renamed))
#datatypeConstructors Optic
  A_Fold
  NoIx
  (DatatypeInfo Renamed)
  (DatatypeInfo Renamed)
  (Vector (Constructor Renamed))
  (Vector (Constructor Renamed))
-> Optic
     A_Fold
     NoIx
     (Vector (Constructor Renamed))
     (Vector (Constructor Renamed))
     (Constructor Renamed)
     (Constructor Renamed)
-> Optic' A_Fold NoIx (DatatypeInfo Renamed) (Constructor Renamed)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Fold
  NoIx
  (Vector (Constructor Renamed))
  (Vector (Constructor Renamed))
  (Constructor Renamed)
  (Constructor Renamed)
forall (f :: Type -> Type) a. Foldable f => Fold (f a) a
folded) DatatypeInfo Renamed
dtInfo
      Int
expectedNumFields <- Vector (ValT Renamed) -> Int
forall a. Vector a -> Int
Vector.length (Vector (ValT Renamed) -> Int)
-> (Constructor Renamed -> Vector (ValT Renamed))
-> Constructor Renamed
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx (Constructor Renamed) (Vector (ValT Renamed))
-> Constructor Renamed -> Vector (ValT Renamed)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Constructor Renamed) (Vector (ValT Renamed))
#constructorArgs (Constructor Renamed -> Int) -> m (Constructor Renamed) -> m Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constructor Renamed] -> m (Constructor Renamed)
forall (t :: Type -> Type) a.
Foldable t =>
t (Constructor a) -> m (Constructor a)
findConstructor [Constructor Renamed]
ctors
      Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Int
actualNumFields Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
expectedNumFields) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ()) -> CovenantTypeError -> m ()
forall a b. (a -> b) -> a -> b
$
          TyName -> ConstructorName -> Int -> CovenantTypeError
IntroFormWrongNumArgs TyName
tyName ConstructorName
ctorName Int
actualNumFields

    checkOpaqueArgs :: Set.Set PlutusDataConstructor -> Vector (ValT Renamed) -> m ()
    checkOpaqueArgs :: Set PlutusDataConstructor -> Vector (ValT Renamed) -> m ()
checkOpaqueArgs Set PlutusDataConstructor
declCtors Vector (ValT Renamed)
fieldArgs' = case ConstructorName
ctorName of
      ConstructorName
"I" -> PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
PlutusI [BuiltinFlatT -> ValT Renamed
forall a. BuiltinFlatT -> ValT a
BuiltinFlat BuiltinFlatT
IntegerT]
      ConstructorName
"B" -> PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
PlutusB [BuiltinFlatT -> ValT Renamed
forall a. BuiltinFlatT -> ValT a
BuiltinFlat BuiltinFlatT
ByteStringT]
      ConstructorName
"List" -> PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
PlutusList [TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"List" ([ValT Renamed] -> Vector (ValT Renamed)
forall a. [a] -> Vector a
Vector.fromList [TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"Data" Vector (ValT Renamed)
forall a. Monoid a => a
mempty])]
      ConstructorName
"Map" -> PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
PlutusMap [TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"Map" ([ValT Renamed] -> Vector (ValT Renamed)
forall a. [a] -> Vector a
Vector.fromList [TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"Data" Vector (ValT Renamed)
forall a. Monoid a => a
mempty, TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"Data" Vector (ValT Renamed)
forall a. Monoid a => a
mempty])]
      ConstructorName
"Constr" -> PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
PlutusConstr [BuiltinFlatT -> ValT Renamed
forall a. BuiltinFlatT -> ValT a
BuiltinFlat BuiltinFlatT
IntegerT, TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"List" ([ValT Renamed] -> Vector (ValT Renamed)
forall a. [a] -> Vector a
Vector.fromList [TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"Data" Vector (ValT Renamed)
forall a. Monoid a => a
mempty])]
      ConstructorName
_ -> CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ()) -> CovenantTypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Set PlutusDataConstructor -> ConstructorName -> CovenantTypeError
UndeclaredOpaquePlutusDataCtor Set PlutusDataConstructor
declCtors ConstructorName
ctorName
      where
        fieldArgs :: [ValT Renamed]
        fieldArgs :: [ValT Renamed]
fieldArgs = Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList Vector (ValT Renamed)
fieldArgs'
        opaqueCheck :: PlutusDataConstructor -> [ValT Renamed] -> m ()
        opaqueCheck :: PlutusDataConstructor -> [ValT Renamed] -> m ()
opaqueCheck PlutusDataConstructor
setMustHaveThis [ValT Renamed]
fieldShouldBeThis = do
          Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (PlutusDataConstructor
setMustHaveThis PlutusDataConstructor -> Set PlutusDataConstructor -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set PlutusDataConstructor
declCtors) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (Set PlutusDataConstructor -> ConstructorName -> CovenantTypeError
UndeclaredOpaquePlutusDataCtor Set PlutusDataConstructor
declCtors ConstructorName
ctorName)
          Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ([ValT Renamed]
fieldArgs [ValT Renamed] -> [ValT Renamed] -> Bool
forall a. Eq a => a -> a -> Bool
== [ValT Renamed]
fieldShouldBeThis) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (Set PlutusDataConstructor
-> ConstructorName -> [ValT Renamed] -> CovenantTypeError
InvalidOpaqueField Set PlutusDataConstructor
declCtors ConstructorName
ctorName [ValT Renamed]
fieldArgs)

    -- convenience helpers

    -- Looks up a constructor in a foldable container of constructors (which is probably always a vector but w/e)
    -- Exists to avoid duplicating this code in a few places.
    findConstructor ::
      forall (t :: Type -> Type) (a :: Type).
      (Foldable t) =>
      t (Constructor a) ->
      m (Constructor a)
    findConstructor :: forall (t :: Type -> Type) a.
Foldable t =>
t (Constructor a) -> m (Constructor a)
findConstructor t (Constructor a)
xs = case (Constructor a -> Bool)
-> t (Constructor a) -> Maybe (Constructor a)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\Constructor a
x -> Optic' A_Lens NoIx (Constructor a) ConstructorName
-> Constructor a -> ConstructorName
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Constructor a) ConstructorName
#constructorName Constructor a
x ConstructorName -> ConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorName
ctorName) t (Constructor a)
xs of
      Maybe (Constructor a)
Nothing -> CovenantTypeError -> m (Constructor a)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Constructor a))
-> CovenantTypeError -> m (Constructor a)
forall a b. (a -> b) -> a -> b
$ TyName -> ConstructorName -> CovenantTypeError
ConstructorDoesNotExistForType TyName
tyName ConstructorName
ctorName
      Just Constructor a
ctor' -> Constructor a -> m (Constructor a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Constructor a
ctor'

    -- Looks up the DatatypeInfo for the type argument supplied
    -- and also renames (and rethrows the rename error if renaming fails)
    lookupDatatypeInfo :: m (DatatypeInfo Renamed)
    lookupDatatypeInfo :: m (DatatypeInfo Renamed)
lookupDatatypeInfo =
      (ASGEnv -> Maybe (DatatypeInfo AbstractTy))
-> m (Maybe (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' An_AffineTraversal NoIx ASGEnv (DatatypeInfo AbstractTy)
-> ASGEnv -> Maybe (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (Map TyName (DatatypeInfo AbstractTy))
     (DatatypeInfo AbstractTy)
     (DatatypeInfo AbstractTy)
-> Optic' An_AffineTraversal NoIx ASGEnv (DatatypeInfo AbstractTy)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tyName)) m (Maybe (DatatypeInfo AbstractTy))
-> (Maybe (DatatypeInfo AbstractTy) -> m (DatatypeInfo Renamed))
-> m (DatatypeInfo Renamed)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (DatatypeInfo AbstractTy)
Nothing -> CovenantTypeError -> m (DatatypeInfo Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (DatatypeInfo Renamed))
-> CovenantTypeError -> m (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> CovenantTypeError
TypeDoesNotExist TyName
tyName
        Just DatatypeInfo AbstractTy
infoAbstract -> case DatatypeInfo AbstractTy
-> Either RenameError (DatatypeInfo Renamed)
renameDatatypeInfo DatatypeInfo AbstractTy
infoAbstract of
          Left RenameError
e -> CovenantTypeError -> m (DatatypeInfo Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (DatatypeInfo Renamed))
-> CovenantTypeError -> m (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
DatatypeInfoRenameError RenameError
e
          Right DatatypeInfo Renamed
infoRenamed -> DatatypeInfo Renamed -> m (DatatypeInfo Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure DatatypeInfo Renamed
infoRenamed

-- | Construct a node corresponding to the given constant.
--
-- @since 1.0.0
lit ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m) =>
  AConstant ->
  m Id
lit :: forall (m :: Type -> Type).
MonadHashCons Id ASGNode m =>
AConstant -> m Id
lit AConstant
c = ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (AConstant -> ASGNode) -> AConstant -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode (AConstant -> ValT AbstractTy
forall a. AConstant -> ValT a
typeConstant AConstant
c) (ValNodeInfo -> ASGNode)
-> (AConstant -> ValNodeInfo) -> AConstant -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AConstant -> ValNodeInfo
LitInternal (AConstant -> m Id) -> AConstant -> m Id
forall a b. (a -> b) -> a -> b
$ AConstant
c

-- | Given an 'Id' referring to a computation, build a thunk wrapping it. Will
-- fail if the 'Id' does not refer to a computation node.
--
-- @since 1.0.0
thunk ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Id ->
  m Id
thunk :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m Id
thunk Id
i = do
  ASGNodeType
idT <- Id -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
i
  case ASGNodeType
idT of
    CompNodeType CompT AbstractTy
t -> ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Id -> ASGNode) -> Id -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode (CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT CompT AbstractTy
t) (ValNodeInfo -> ASGNode) -> (Id -> ValNodeInfo) -> Id -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> ValNodeInfo
ThunkInternal (Id -> m Id) -> Id -> m Id
forall a b. (a -> b) -> a -> b
$ Id
i
    ValNodeType ValT AbstractTy
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
ThunkValType (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t
    ASGNodeType
ErrorNodeType -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError CovenantTypeError
ThunkError

-- | Given a 'Ref' to an algebra (that is, something taking a base functor and
-- producing some result), and a 'Ref' to a value associated with that base
-- functor, build a catamorphism to tear it down. This can fail for a range of
-- reasons:
--
-- * First 'Ref' is not a thunk taking one argument
-- * The argument to the thunk isn't a base functor, or isn't a suitable base
--   functor for the second argument
-- * Second argument is not a value type
--
-- = Note
--
-- 'cata' cannot work with /non-rigid/ algebras; that is, all algebras must be
-- functions that bind no type variables of their own.
--
-- @since 1.1.0
cata ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  Ref ->
  Ref ->
  m Id
cata :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> Ref -> m Id
cata Ref
rAlg Ref
rVal =
  Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
rVal m ASGNodeType -> (ASGNodeType -> m Id) -> m Id
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValNodeType ValT AbstractTy
valT ->
      Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
rAlg m ASGNodeType -> (ASGNodeType -> m Id) -> m Id
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        t :: ASGNodeType
t@(ValNodeType (ThunkT CompT AbstractTy
algT)) -> case CompT AbstractTy
algT of
          Comp0 (CompTBody NonEmptyVector (ValT AbstractTy)
nev) -> do
            let algebraArity :: Int
algebraArity = CompT AbstractTy -> Int
forall a. CompT a -> Int
arity CompT AbstractTy
algT
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Int
algebraArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (Int -> CovenantTypeError) -> Int -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> CovenantTypeError
CataAlgebraWrongArity (Int -> m ()) -> Int -> m ()
forall a b. (a -> b) -> a -> b
$ Int
algebraArity)
            case NonEmptyVector (ValT AbstractTy)
nev NonEmptyVector (ValT AbstractTy) -> Int -> ValT AbstractTy
forall a. NonEmptyVector a -> Int -> a
NonEmpty.! Int
0 of
              Datatype TyName
bfName Vector (ValT AbstractTy)
bfTyArgs -> do
                -- If we got this far, we know at minimum that we have somewhat
                -- sensical arguments. Now we have to make sure that we have a
                -- suitable type for the algebra, and a suitable thing to tear
                -- down.
                --
                -- After verifying this, we use `tryApply` so the unification
                -- machinery can produce the type we expect with proper
                -- concretifications.
                Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Vector (ValT AbstractTy) -> Int
forall a. Vector a -> Int
Vector.length Vector (ValT AbstractTy)
bfTyArgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (ASGNodeType -> CovenantTypeError) -> ASGNodeType -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataNotAnAlgebra (ASGNodeType -> m ()) -> ASGNodeType -> m ()
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t)
                let lastTyArg :: ValT AbstractTy
lastTyArg = Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. Vector a -> a
Vector.last Vector (ValT AbstractTy)
bfTyArgs
                Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (NonEmptyVector (ValT AbstractTy)
nev NonEmptyVector (ValT AbstractTy) -> Int -> ValT AbstractTy
forall a. NonEmptyVector a -> Int -> a
NonEmpty.! Int
1 ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
lastTyArg) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (ASGNodeType -> CovenantTypeError) -> ASGNodeType -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataNotAnAlgebra (ASGNodeType -> m ()) -> ASGNodeType -> m ()
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t)
                ValT AbstractTy
appliedArgT <- case ValT AbstractTy
valT of
                  BuiltinFlat BuiltinFlatT
bT -> case BuiltinFlatT
bT of
                    BuiltinFlatT
ByteStringT -> do
                      Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (TyName
bfName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"ByteString_F") (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataUnsuitable CompT AbstractTy
algT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
valT)
                      ValT AbstractTy -> m (ValT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> m (ValT AbstractTy))
-> ValT AbstractTy -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
"ByteString_F" (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> (ValT AbstractTy -> Vector (ValT AbstractTy))
-> ValT AbstractTy
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> Vector (ValT AbstractTy)
forall a. a -> Vector a
Vector.singleton (ValT AbstractTy -> ValT AbstractTy)
-> ValT AbstractTy -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
lastTyArg
                    BuiltinFlatT
IntegerT -> do
                      let isSuitableBaseFunctor :: Bool
isSuitableBaseFunctor = TyName
bfName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"Natural_F" Bool -> Bool -> Bool
|| TyName
bfName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"Negative_F"
                      Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
isSuitableBaseFunctor (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataUnsuitable CompT AbstractTy
algT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
valT)
                      ValT AbstractTy -> m (ValT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> m (ValT AbstractTy))
-> ValT AbstractTy -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
bfName (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> (ValT AbstractTy -> Vector (ValT AbstractTy))
-> ValT AbstractTy
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> Vector (ValT AbstractTy)
forall a. a -> Vector a
Vector.singleton (ValT AbstractTy -> ValT AbstractTy)
-> ValT AbstractTy -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
lastTyArg
                    BuiltinFlatT
_ -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (BuiltinFlatT -> CovenantTypeError)
-> BuiltinFlatT
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinFlatT -> CovenantTypeError
CataWrongBuiltinType (BuiltinFlatT -> m (ValT AbstractTy))
-> BuiltinFlatT -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT
bT
                  Datatype TyName
tyName Vector (ValT AbstractTy)
tyVars -> do
                    Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
lookedUp <- (ASGEnv -> Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
-> m (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic'
  A_Lens
  NoIx
  ASGEnv
  (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
-> ASGEnv -> Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic
     A_Lens
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (Map TyName (DatatypeInfo AbstractTy))
     (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
     (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
-> Optic'
     A_Lens
     NoIx
     ASGEnv
     (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic
     A_Lens
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (Map TyName (DatatypeInfo AbstractTy))
     (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
     (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tyName))
                    case Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
lookedUp of
                      Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
Nothing -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (TyName -> CovenantTypeError) -> TyName -> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> CovenantTypeError
CataNoSuchType (TyName -> m (ValT AbstractTy)) -> TyName -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TyName
tyName
                      Just IxValue (Map TyName (DatatypeInfo AbstractTy))
info -> case Optic'
  A_Lens
  NoIx
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> IxValue (Map TyName (DatatypeInfo AbstractTy))
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic'
  A_Lens
  NoIx
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
#baseFunctor IxValue (Map TyName (DatatypeInfo AbstractTy))
info of
                        Just (DataDeclaration TyName
actualBfName Count "tyvar"
_ Vector (Constructor AbstractTy)
_ DataEncoding
_, ValT AbstractTy
_) -> do
                          Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (TyName
bfName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
actualBfName) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataUnsuitable CompT AbstractTy
algT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
valT)
                          let lastTyArg' :: ValT AbstractTy
lastTyArg' = ValT AbstractTy -> ValT AbstractTy
stepDownDB ValT AbstractTy
lastTyArg
                          ValT AbstractTy -> m (ValT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> m (ValT AbstractTy))
-> (ValT AbstractTy -> ValT AbstractTy)
-> ValT AbstractTy
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
bfName (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> (ValT AbstractTy -> Vector (ValT AbstractTy))
-> ValT AbstractTy
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT AbstractTy)
-> ValT AbstractTy -> Vector (ValT AbstractTy)
forall a. Vector a -> a -> Vector a
Vector.snoc Vector (ValT AbstractTy)
tyVars (ValT AbstractTy -> m (ValT AbstractTy))
-> ValT AbstractTy -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
lastTyArg'
                        Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
_ -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (TyName -> CovenantTypeError) -> TyName -> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> CovenantTypeError
CataNoBaseFunctorForType (TyName -> m (ValT AbstractTy)) -> TyName -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TyName
tyName
                  ValT AbstractTy
_ -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
CataWrongValT (ValT AbstractTy -> m (ValT AbstractTy))
-> ValT AbstractTy -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
valT
                ValT AbstractTy
resultT <- CompT AbstractTy -> ValT AbstractTy -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
CompT AbstractTy -> ValT AbstractTy -> m (ValT AbstractTy)
tryApply CompT AbstractTy
algT ValT AbstractTy
appliedArgT
                ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Ref -> ASGNode) -> Ref -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
resultT (ValNodeInfo -> ASGNode) -> (Ref -> ValNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> Ref -> ValNodeInfo
CataInternal Ref
rAlg (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
rVal
              ValT AbstractTy
_ -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ASGNodeType -> CovenantTypeError) -> ASGNodeType -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataNotAnAlgebra (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
          CompT AbstractTy
_ -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
CataNonRigidAlgebra (CompT AbstractTy -> m Id) -> CompT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
algT
        ASGNodeType
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ASGNodeType -> CovenantTypeError) -> ASGNodeType -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataNotAnAlgebra (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
    ASGNodeType
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ASGNodeType -> CovenantTypeError) -> ASGNodeType -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataApplyToNonValT (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t

-- | Perform a pattern match. The first argument is the value to be matched on,
-- and the second argument is a 'Vector' of \'handlers\' for each possible
-- \'arm\' of the type of the value to be matched on.
--
-- All handlers must be thunks, and must all return the same (concrete) result.
-- Polymorphic \'handlers\' (that is, thunks whose computation binds type
-- variables of its own) will fail to compile.
--
-- @since 1.2.0
match ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  Ref ->
  Vector Ref ->
  m Id
match :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> Vector Ref -> m Id
match Ref
scrutinee Vector Ref
handlers = do
  ASGNodeType
scrutNodeTy <- Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
scrutinee
  case ASGNodeType
scrutNodeTy of
    ValNodeType scrutTy :: ValT AbstractTy
scrutTy@(Datatype TyName
tn Vector (ValT AbstractTy)
args) ->
      ValT AbstractTy -> m Bool
isRecursive ValT AbstractTy
scrutTy m Bool -> (Bool -> m Id) -> m Id
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True -> TyName -> Vector (ValT AbstractTy) -> m Id
goRecursive TyName
tn Vector (ValT AbstractTy)
args
        Bool
False -> TyName -> Vector (ValT AbstractTy) -> m Id
goNonRecursive TyName
tn Vector (ValT AbstractTy)
args
    ValNodeType ValT AbstractTy
other -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id) -> CovenantTypeError -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy -> CovenantTypeError
MatchNonDatatypeScrutinee ValT AbstractTy
other
    ASGNodeType
other -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id) -> CovenantTypeError -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType -> CovenantTypeError
MatchNonValTy ASGNodeType
other
  where
    isRecursive :: ValT AbstractTy -> m Bool
    isRecursive :: ValT AbstractTy -> m Bool
isRecursive (Datatype TyName
tyName Vector (ValT AbstractTy)
_) = do
      Bool
datatypeInfoExists <- (ASGEnv -> Bool) -> m Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))) -> Bool)
-> (ASGEnv
    -> Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy))))
-> ASGEnv
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> ASGEnv -> Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tyName))
      if Bool
datatypeInfoExists
        then (ASGEnv -> Bool) -> m Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Maybe (DataDeclaration AbstractTy, ValT AbstractTy) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (DataDeclaration AbstractTy, ValT AbstractTy) -> Bool)
-> (ASGEnv -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> ASGEnv
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
 -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> (ASGEnv
    -> Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy)))
-> ASGEnv
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> ASGEnv
-> Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tyName Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     A_Lens
     NoIx
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic'
  A_Lens
  NoIx
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
#baseFunctor))
        else CovenantTypeError -> m Bool
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Bool) -> CovenantTypeError -> m Bool
forall a b. (a -> b) -> a -> b
$ TyName -> CovenantTypeError
MatchNoDatatypeInfo TyName
tyName
    isRecursive ValT AbstractTy
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False

    goRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
    goRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
goRecursive tn :: TyName
tn@(TyName Text
rawTn) Vector (ValT AbstractTy)
tyConArgs = do
      -- This fromJust is safe b/c the presence of absence of base functor data is the condition that
      -- determines whether we're in this branch or the non-recursive one
      ValT AbstractTy
rawBFBB <- (ASGEnv -> ValT AbstractTy) -> m (ValT AbstractTy)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks ((DataDeclaration AbstractTy, ValT AbstractTy) -> ValT AbstractTy
forall a b. (a, b) -> b
snd ((DataDeclaration AbstractTy, ValT AbstractTy) -> ValT AbstractTy)
-> (ASGEnv -> (DataDeclaration AbstractTy, ValT AbstractTy))
-> ASGEnv
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
-> (DataDeclaration AbstractTy, ValT AbstractTy)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
 -> (DataDeclaration AbstractTy, ValT AbstractTy))
-> (ASGEnv -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> ASGEnv
-> (DataDeclaration AbstractTy, ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
 -> Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> (ASGEnv
    -> Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy)))
-> ASGEnv
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> ASGEnv
-> Maybe (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tn Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     A_Lens
     NoIx
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic'
  A_Lens
  NoIx
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
#baseFunctor))
      CompT Renamed
bfbb <- ValT AbstractTy -> m (CompT Renamed)
instantiateBFBB ValT AbstractTy
rawBFBB
      [ValT Renamed]
handlers' <- Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList (Vector (ValT Renamed) -> [ValT Renamed])
-> m (Vector (ValT Renamed)) -> m [ValT Renamed]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ref -> m (ValT Renamed))
-> Vector Ref -> m (Vector (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Ref -> m (ValT Renamed)
cleanupHandler Vector Ref
handlers
      Map TyName (DatatypeInfo AbstractTy)
tyDict <- (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo)
      case Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
bfbb (ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just (ValT Renamed -> Maybe (ValT Renamed))
-> [ValT Renamed] -> [Maybe (ValT Renamed)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [ValT Renamed]
handlers') of
        Right ValT Renamed
appliedBfbb -> do
          ValT AbstractTy
result <- ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
appliedBfbb
          ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> ASGNode -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
result (Ref -> Vector Ref -> ValNodeInfo
MatchInternal Ref
scrutinee Vector Ref
handlers)
        Left TypeAppError
err' -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (TypeAppError -> CovenantTypeError) -> TypeAppError -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAppError -> CovenantTypeError
UnificationError (TypeAppError -> m Id) -> TypeAppError -> m Id
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
      where
        instantiateBFBB :: ValT AbstractTy -> m (CompT Renamed)
        instantiateBFBB :: ValT AbstractTy -> m (CompT Renamed)
instantiateBFBB ValT AbstractTy
bfbb = do
          -- we have a BFBB like:
          -- listBB :: forall a r . r -> <a -> r -> !r> -> !r
          -- And we need to:
          --   1. Instantiate all of the type arguments to the original datatype (e.g. the 'a' in List a)
          --      into the BFBB
          --   2. Instantiate the *last* tyvar bound by the BBBF to the type of the original datatype
          --      giving us, e.g. ListF a (List a)
          Vector Word32
scope <- m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope
          ValT Renamed
renamedBFBB <- case Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (ValT AbstractTy -> RenameM (ValT Renamed)
renameValT ValT AbstractTy
bfbb) of
            Left RenameError
err' -> CovenantTypeError -> m (ValT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT Renamed))
-> CovenantTypeError -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
MatchRenameBBFail RenameError
err'
            Right ValT Renamed
res -> ValT Renamed -> m (ValT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
res
          -- The type constructor for the base-functor variant of the scrutinee type.
          let scrut :: ValT AbstractTy
scrut = TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn Vector (ValT AbstractTy)
tyConArgs
          let scrutF :: ValT AbstractTy
scrutF = TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype (Text -> TyName
TyName (Text -> TyName) -> Text -> TyName
forall a b. (a -> b) -> a -> b
$ Text
rawTn Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_F") (Vector (ValT AbstractTy)
-> ValT AbstractTy -> Vector (ValT AbstractTy)
forall a. Vector a -> a -> Vector a
Vector.snoc Vector (ValT AbstractTy)
tyConArgs ValT AbstractTy
scrut)
          -- These are arguments to the original type constructor plus the snoc'd original type.
          -- E.g. if we have:
          --      Scrutinee: List Int
          --   this should be:
          --   [Int, List Int]
          let bfInstArgs :: Vector (ValT AbstractTy)
bfInstArgs = Vector (ValT AbstractTy)
-> ValT AbstractTy -> Vector (ValT AbstractTy)
forall a. Vector a -> a -> Vector a
Vector.snoc Vector (ValT AbstractTy)
tyConArgs ValT AbstractTy
scrutF
          Vector (ValT Renamed)
renamedArgs <- case Vector Word32
-> RenameM (Vector (ValT Renamed))
-> Either RenameError (Vector (ValT Renamed))
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope ((ValT AbstractTy -> RenameM (ValT Renamed))
-> Vector (ValT AbstractTy) -> RenameM (Vector (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> RenameM (ValT Renamed)
renameValT Vector (ValT AbstractTy)
bfInstArgs) of
            Left RenameError
err' -> CovenantTypeError -> m (Vector (ValT Renamed))
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Vector (ValT Renamed)))
-> CovenantTypeError -> m (Vector (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
MatchRenameTyConArgFail RenameError
err'
            Right Vector (ValT Renamed)
res -> Vector (ValT Renamed) -> m (Vector (ValT Renamed))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Vector (ValT Renamed)
res
          let subs :: Vector (Index "tyvar", ValT Renamed)
              subs :: Vector (Index "tyvar", ValT Renamed)
subs = (Int -> ValT Renamed -> (Index "tyvar", ValT Renamed))
-> Vector (ValT Renamed) -> Vector (Index "tyvar", ValT Renamed)
forall a b. (Int -> a -> b) -> Vector a -> Vector b
Vector.imap (\Int
i ValT Renamed
v -> (Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Int
i, ValT Renamed
v)) Vector (ValT Renamed)
renamedArgs
              subbed :: ValT Renamed
subbed = (ValT Renamed -> (Index "tyvar", ValT Renamed) -> ValT Renamed)
-> ValT Renamed
-> Vector (Index "tyvar", ValT Renamed)
-> ValT Renamed
forall b a. (b -> a -> b) -> b -> Vector a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ValT Renamed
bbf (Index "tyvar"
i, ValT Renamed
v) -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
v ValT Renamed
bbf) ValT Renamed
renamedBFBB Vector (Index "tyvar", ValT Renamed)
subs
          case ValT Renamed
subbed of
            ThunkT CompT Renamed
bfComp -> CompT Renamed -> m (CompT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CompT Renamed
bfComp
            ValT Renamed
other -> CovenantTypeError -> m (CompT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (CompT Renamed))
-> CovenantTypeError -> m (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed -> CovenantTypeError
MatchNonThunkBBF ValT Renamed
other

    -- Unwraps a thunk handler if it is a handler for a nullary constructor.
    cleanupHandler :: Ref -> m (ValT Renamed)
    cleanupHandler :: Ref -> m (ValT Renamed)
cleanupHandler Ref
r =
      Ref -> m (Maybe (ValT Renamed))
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Ref
r m (Maybe (ValT Renamed))
-> (Maybe (ValT Renamed) -> m (ValT Renamed)) -> m (ValT Renamed)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (ValT Renamed)
Nothing ->
          CovenantTypeError -> m (ValT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT Renamed))
-> CovenantTypeError -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Ref -> CovenantTypeError
MatchErrorAsHandler Ref
r
        Just ValT Renamed
hVal -> case ValT Renamed
hVal of
          hdlr :: ValT Renamed
hdlr@(ThunkT (CompT Count "tyvar"
cnt (ReturnT ValT Renamed
v)))
            | Count "tyvar"
cnt Count "tyvar" -> Count "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count0 -> ValT Renamed -> m (ValT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
v
            | Bool
otherwise -> CovenantTypeError -> m (ValT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT Renamed))
-> CovenantTypeError -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed -> CovenantTypeError
MatchPolymorphicHandler ValT Renamed
hdlr
          ValT Renamed
other -> ValT Renamed -> m (ValT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
other

    goNonRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
    goNonRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
goNonRecursive TyName
tn Vector (ValT AbstractTy)
tyConArgs = do
      Maybe (ValT AbstractTy)
rawBBF <- (ASGEnv -> Maybe (ValT AbstractTy)) -> m (Maybe (ValT AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Maybe (Maybe (ValT AbstractTy)) -> Maybe (ValT AbstractTy)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Maybe (ValT AbstractTy)) -> Maybe (ValT AbstractTy))
-> (ASGEnv -> Maybe (Maybe (ValT AbstractTy)))
-> ASGEnv
-> Maybe (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' An_AffineTraversal NoIx ASGEnv (Maybe (ValT AbstractTy))
-> ASGEnv -> Maybe (Maybe (ValT AbstractTy))
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic'
     An_AffineTraversal
     NoIx
     ASGEnv
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map TyName (DatatypeInfo AbstractTy))
-> Optic'
     (IxKind (Map TyName (DatatypeInfo AbstractTy)))
     NoIx
     (Map TyName (DatatypeInfo AbstractTy))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Index (Map TyName (DatatypeInfo AbstractTy))
TyName
tn Optic'
  An_AffineTraversal
  NoIx
  ASGEnv
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Optic
     A_Lens
     NoIx
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (Maybe (ValT AbstractTy))
     (Maybe (ValT AbstractTy))
-> Optic' An_AffineTraversal NoIx ASGEnv (Maybe (ValT AbstractTy))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (ValT AbstractTy))
  (Maybe (ValT AbstractTy))
#bbForm))
      (CompT Renamed
instantiatedBBF :: CompT Renamed) <- Maybe (ValT AbstractTy)
-> Vector (ValT AbstractTy) -> m (CompT Renamed)
instantiateBB Maybe (ValT AbstractTy)
rawBBF Vector (ValT AbstractTy)
tyConArgs
      [ValT Renamed]
handlers' <- Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList (Vector (ValT Renamed) -> [ValT Renamed])
-> m (Vector (ValT Renamed)) -> m [ValT Renamed]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ref -> m (ValT Renamed))
-> Vector Ref -> m (Vector (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Ref -> m (ValT Renamed)
cleanupHandler Vector Ref
handlers
      Map TyName (DatatypeInfo AbstractTy)
tyDict <- (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo)
      case Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
instantiatedBBF (ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just (ValT Renamed -> Maybe (ValT Renamed))
-> [ValT Renamed] -> [Maybe (ValT Renamed)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [ValT Renamed]
handlers') of
        Right ValT Renamed
appliedBBF -> do
          ValT AbstractTy
result <- ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
appliedBBF
          ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> ASGNode -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
result (Ref -> Vector Ref -> ValNodeInfo
MatchInternal Ref
scrutinee Vector Ref
handlers)
        Left TypeAppError
err' -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (TypeAppError -> CovenantTypeError) -> TypeAppError -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAppError -> CovenantTypeError
UnificationError (TypeAppError -> m Id) -> TypeAppError -> m Id
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
      where
        instantiateBB :: Maybe (ValT AbstractTy) -> Vector (ValT AbstractTy) -> m (CompT Renamed)
        instantiateBB :: Maybe (ValT AbstractTy)
-> Vector (ValT AbstractTy) -> m (CompT Renamed)
instantiateBB Maybe (ValT AbstractTy)
Nothing Vector (ValT AbstractTy)
_ = CovenantTypeError -> m (CompT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (CompT Renamed))
-> CovenantTypeError -> m (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> CovenantTypeError
MatchNoBBForm TyName
tn
        instantiateBB (Just ValT AbstractTy
bb) Vector (ValT AbstractTy)
tyArgs = do
          Vector Word32
scope <- m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope
          ValT Renamed
renamedBB <- case Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (ValT AbstractTy -> RenameM (ValT Renamed)
renameValT ValT AbstractTy
bb) of
            Left RenameError
err' -> CovenantTypeError -> m (ValT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT Renamed))
-> CovenantTypeError -> m (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
MatchRenameBBFail RenameError
err'
            Right ValT Renamed
res -> ValT Renamed -> m (ValT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT Renamed
res
          Vector (ValT Renamed)
renamedArgs <- case Vector Word32
-> RenameM (Vector (ValT Renamed))
-> Either RenameError (Vector (ValT Renamed))
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope ((ValT AbstractTy -> RenameM (ValT Renamed))
-> Vector (ValT AbstractTy) -> RenameM (Vector (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> RenameM (ValT Renamed)
renameValT Vector (ValT AbstractTy)
tyArgs) of
            Left RenameError
err' -> CovenantTypeError -> m (Vector (ValT Renamed))
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Vector (ValT Renamed)))
-> CovenantTypeError -> m (Vector (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ RenameError -> CovenantTypeError
MatchRenameTyConArgFail RenameError
err'
            Right Vector (ValT Renamed)
res -> Vector (ValT Renamed) -> m (Vector (ValT Renamed))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Vector (ValT Renamed)
res
          let subs :: Vector (Index "tyvar", ValT Renamed)
              subs :: Vector (Index "tyvar", ValT Renamed)
subs = (Int -> ValT Renamed -> (Index "tyvar", ValT Renamed))
-> Vector (ValT Renamed) -> Vector (Index "tyvar", ValT Renamed)
forall a b. (Int -> a -> b) -> Vector a -> Vector b
Vector.imap (\Int
i ValT Renamed
v -> (Maybe (Index "tyvar") -> Index "tyvar"
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index "tyvar") -> Index "tyvar")
-> (Int -> Maybe (Index "tyvar")) -> Int -> Index "tyvar"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int (Index "tyvar")
-> Int -> Maybe (Index "tyvar")
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex (Int -> Index "tyvar") -> Int -> Index "tyvar"
forall a b. (a -> b) -> a -> b
$ Int
i, ValT Renamed
v)) Vector (ValT Renamed)
renamedArgs
              subbed :: ValT Renamed
subbed = (ValT Renamed -> (Index "tyvar", ValT Renamed) -> ValT Renamed)
-> ValT Renamed
-> Vector (Index "tyvar", ValT Renamed)
-> ValT Renamed
forall b a. (b -> a -> b) -> b -> Vector a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ValT Renamed
bbf (Index "tyvar"
i, ValT Renamed
v) -> Index "tyvar" -> ValT Renamed -> ValT Renamed -> ValT Renamed
substitute Index "tyvar"
i ValT Renamed
v ValT Renamed
bbf) ValT Renamed
renamedBB Vector (Index "tyvar", ValT Renamed)
subs
          case ValT Renamed
subbed of
            ThunkT CompT Renamed
bbComp -> CompT Renamed -> m (CompT Renamed)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CompT Renamed
bbComp
            ValT Renamed
other -> CovenantTypeError -> m (CompT Renamed)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (CompT Renamed))
-> CovenantTypeError -> m (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed -> CovenantTypeError
MatchNonThunkBBF ValT Renamed
other

-- Helpers

-- Note (Koz, 13/08/2025): We need this procedure specifically for `cata`. The
-- reason for this has to do with how we construct the 'base functor form' of
-- the value to be torn down by the catamorphism, in order to use the
-- unification machinery to get the type of the final result.
--
-- To be specific, suppose we have `<List_F r (Maybe r) -> !Maybe r>` as our algebra
-- argument (where `r` is some rigid), and `List r` as the value to be torn
-- down. If we assume the rigid is bound one scope away, `r`'s DeBruijn index
-- will be `S Z` for
-- the value to be torn down, but `S (S Z)` for the algebra argument. The way
-- our approach works is:
--
-- 1. Look at the algebra argument, specifically the base functor type. Take its
--    last type argument, which we will call `last`.
-- 2. Determine the base functor for the value to be torn down. Cook up a new
--    instance of the base functor type, copying all the type arguments from the
--    value to be torn down in the same order. Then put `last` at the end.
-- 3. Force the algebra argument thunk, then try and apply the result of Step 2
--    to that.
--
-- Following the steps above for our example, we would proceed as follows:
--
-- 1. Set `last` as `Maybe r`.
-- 2. Cook up `List_F r (Maybe r)`. Note that this matches what the algebra
--    expects.
-- 3. Use the unifier with `List_F r (Maybe r) -> !Maybe r`, applying the
--    argument `List_F r (Maybe r)` from Step 2.
--
-- However, if `last` is a rigid, we have an 'off by one error'. To see why,
-- consider the form of the algebra argument:
--
-- `ThunkT . Comp0 $ Datatype "List_F" [tyvar (S (S Z)) ix0, ....`
--
-- However, `tyvar (S (S Z)) ix0` is not valid in the scope of the value to be
-- torn down: that same rigid would have DeBruijn index `S Z` there instead.
-- This applies the same if the tyvar is part of a datatype.
--
-- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn
-- index by one for our process.
stepDownDB :: ValT AbstractTy -> ValT AbstractTy
stepDownDB :: ValT AbstractTy -> ValT AbstractTy
stepDownDB = \case
  Abstraction (BoundAt DeBruijn
db Index "tyvar"
i) -> case DeBruijn
db of
    -- This is impossible, so we just return it unmodified
    DeBruijn
Z -> AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db Index "tyvar"
i)
    (S DeBruijn
db') -> AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db' Index "tyvar"
i)
  Datatype TyName
tyName Vector (ValT AbstractTy)
tyArgs -> TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tyName (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> (Vector (ValT AbstractTy) -> Vector (ValT AbstractTy))
-> Vector (ValT AbstractTy)
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValT AbstractTy -> ValT AbstractTy)
-> Vector (ValT AbstractTy) -> Vector (ValT AbstractTy)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ValT AbstractTy -> ValT AbstractTy
stepDownDB (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ Vector (ValT AbstractTy)
tyArgs
  ValT AbstractTy
x -> ValT AbstractTy
x

renameArg ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  Ref ->
  m (Maybe (ValT Renamed))
renameArg :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Ref
r =
  m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope m (Vector Word32)
-> (Vector Word32 -> m (Maybe (ValT Renamed)))
-> m (Maybe (ValT Renamed))
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Vector Word32
scope ->
    Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
r m ASGNodeType
-> (ASGNodeType -> m (Maybe (ValT Renamed)))
-> m (Maybe (ValT Renamed))
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      CompNodeType CompT AbstractTy
t -> CovenantTypeError -> m (Maybe (ValT Renamed))
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Maybe (ValT Renamed)))
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m (Maybe (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
ApplyCompType (CompT AbstractTy -> m (Maybe (ValT Renamed)))
-> CompT AbstractTy -> m (Maybe (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t
      ValNodeType ValT AbstractTy
t -> case Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (RenameM (ValT Renamed) -> Either RenameError (ValT Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> ValT AbstractTy
-> Either RenameError (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT (ValT AbstractTy -> Either RenameError (ValT Renamed))
-> ValT AbstractTy -> Either RenameError (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t of
        Left RenameError
err' -> CovenantTypeError -> m (Maybe (ValT Renamed))
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (Maybe (ValT Renamed)))
-> (RenameError -> CovenantTypeError)
-> RenameError
-> m (Maybe (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameError -> CovenantTypeError
RenameArgumentFailed ValT AbstractTy
t (RenameError -> m (Maybe (ValT Renamed)))
-> RenameError -> m (Maybe (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ RenameError
err'
        Right ValT Renamed
renamed -> Maybe (ValT Renamed) -> m (Maybe (ValT Renamed))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (ValT Renamed) -> m (Maybe (ValT Renamed)))
-> (ValT Renamed -> Maybe (ValT Renamed))
-> ValT Renamed
-> m (Maybe (ValT Renamed))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just (ValT Renamed -> m (Maybe (ValT Renamed)))
-> ValT Renamed -> m (Maybe (ValT Renamed))
forall a b. (a -> b) -> a -> b
$ ValT Renamed
renamed
      ASGNodeType
ErrorNodeType -> Maybe (ValT Renamed) -> m (Maybe (ValT Renamed))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (ValT Renamed)
forall a. Maybe a
Nothing

checkEncodingWithInfo ::
  forall (a :: Type) (m :: Type -> Type).
  (MonadError CovenantTypeError m) =>
  Map TyName (DatatypeInfo a) ->
  ValT AbstractTy ->
  m ()
checkEncodingWithInfo :: forall a (m :: Type -> Type).
MonadError CovenantTypeError m =>
Map TyName (DatatypeInfo a) -> ValT AbstractTy -> m ()
checkEncodingWithInfo Map TyName (DatatypeInfo a)
tyDict ValT AbstractTy
valT = case (DatatypeInfo a -> DataEncoding)
-> Map TyName (DatatypeInfo a)
-> ValT AbstractTy
-> Either (EncodingArgErr AbstractTy) ()
forall a info.
(info -> DataEncoding)
-> Map TyName info -> ValT a -> Either (EncodingArgErr a) ()
checkEncodingArgs (Optic' A_Lens NoIx (DatatypeInfo a) DataEncoding
-> DatatypeInfo a -> DataEncoding
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Optic
  A_Lens
  NoIx
  (DatatypeInfo a)
  (DatatypeInfo a)
  (DataDeclaration a)
  (DataDeclaration a)
#originalDecl Optic
  A_Lens
  NoIx
  (DatatypeInfo a)
  (DatatypeInfo a)
  (DataDeclaration a)
  (DataDeclaration a)
-> Optic
     A_Lens
     NoIx
     (DataDeclaration a)
     (DataDeclaration a)
     DataEncoding
     DataEncoding
-> Optic' A_Lens NoIx (DatatypeInfo a) DataEncoding
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (DataDeclaration a)
  (DataDeclaration a)
  DataEncoding
  DataEncoding
#datatypeEncoding)) Map TyName (DatatypeInfo a)
tyDict ValT AbstractTy
valT of
  Left EncodingArgErr AbstractTy
encErr -> CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ()) -> CovenantTypeError -> m ()
forall a b. (a -> b) -> a -> b
$ EncodingArgErr AbstractTy -> CovenantTypeError
EncodingError EncodingArgErr AbstractTy
encErr
  Right {} -> () -> m ()
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

tryApply ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  CompT AbstractTy ->
  ValT AbstractTy ->
  m (ValT AbstractTy)
tryApply :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
CompT AbstractTy -> ValT AbstractTy -> m (ValT AbstractTy)
tryApply CompT AbstractTy
algebraT ValT AbstractTy
argT =
  m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope m (Vector Word32)
-> (Vector Word32 -> m (ValT AbstractTy)) -> m (ValT AbstractTy)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Vector Word32
scope -> case Vector Word32
-> RenameM (CompT Renamed) -> Either RenameError (CompT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (RenameM (CompT Renamed) -> Either RenameError (CompT Renamed))
-> (CompT AbstractTy -> RenameM (CompT Renamed))
-> CompT AbstractTy
-> Either RenameError (CompT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT (CompT AbstractTy -> Either RenameError (CompT Renamed))
-> CompT AbstractTy -> Either RenameError (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
algebraT of
    Left RenameError
err' -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (RenameError -> CovenantTypeError)
-> RenameError
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameError -> CovenantTypeError
RenameFunctionFailed CompT AbstractTy
algebraT (RenameError -> m (ValT AbstractTy))
-> RenameError -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ RenameError
err'
    Right CompT Renamed
renamedAlgebraT -> case Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scope (RenameM (ValT Renamed) -> Either RenameError (ValT Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> ValT AbstractTy
-> Either RenameError (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT (ValT AbstractTy -> Either RenameError (ValT Renamed))
-> ValT AbstractTy -> Either RenameError (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
argT of
      Left RenameError
err' -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (RenameError -> CovenantTypeError)
-> RenameError
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameError -> CovenantTypeError
RenameArgumentFailed ValT AbstractTy
argT (RenameError -> m (ValT AbstractTy))
-> RenameError -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ RenameError
err'
      Right ValT Renamed
renamedArgT -> do
        Map TyName (DatatypeInfo AbstractTy)
tyDict <- (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo)
        case Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
renamedAlgebraT [ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just ValT Renamed
renamedArgT] of
          Left TypeAppError
err' -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> (TypeAppError -> CovenantTypeError)
-> TypeAppError
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAppError -> CovenantTypeError
UnificationError (TypeAppError -> m (ValT AbstractTy))
-> TypeAppError -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
          Right ValT Renamed
resultT -> ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
resultT

-- Putting this here to reduce chance of annoying manual merge (will move later)

-- | Wrapper around an `Arg` that we know represents an in-scope type variable.
-- @since 1.2.0
data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
  deriving stock
    ( -- @since 1.2.0
      Int -> BoundTyVar -> ShowS
[BoundTyVar] -> ShowS
BoundTyVar -> [Char]
(Int -> BoundTyVar -> ShowS)
-> (BoundTyVar -> [Char])
-> ([BoundTyVar] -> ShowS)
-> Show BoundTyVar
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BoundTyVar -> ShowS
showsPrec :: Int -> BoundTyVar -> ShowS
$cshow :: BoundTyVar -> [Char]
show :: BoundTyVar -> [Char]
$cshowList :: [BoundTyVar] -> ShowS
showList :: [BoundTyVar] -> ShowS
Show,
      -- @since 1.2.0
      BoundTyVar -> BoundTyVar -> Bool
(BoundTyVar -> BoundTyVar -> Bool)
-> (BoundTyVar -> BoundTyVar -> Bool) -> Eq BoundTyVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoundTyVar -> BoundTyVar -> Bool
== :: BoundTyVar -> BoundTyVar -> Bool
$c/= :: BoundTyVar -> BoundTyVar -> Bool
/= :: BoundTyVar -> BoundTyVar -> Bool
Eq,
      -- @since 1.2.0
      Eq BoundTyVar
Eq BoundTyVar =>
(BoundTyVar -> BoundTyVar -> Ordering)
-> (BoundTyVar -> BoundTyVar -> Bool)
-> (BoundTyVar -> BoundTyVar -> Bool)
-> (BoundTyVar -> BoundTyVar -> Bool)
-> (BoundTyVar -> BoundTyVar -> Bool)
-> (BoundTyVar -> BoundTyVar -> BoundTyVar)
-> (BoundTyVar -> BoundTyVar -> BoundTyVar)
-> Ord BoundTyVar
BoundTyVar -> BoundTyVar -> Bool
BoundTyVar -> BoundTyVar -> Ordering
BoundTyVar -> BoundTyVar -> BoundTyVar
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
$ccompare :: BoundTyVar -> BoundTyVar -> Ordering
compare :: BoundTyVar -> BoundTyVar -> Ordering
$c< :: BoundTyVar -> BoundTyVar -> Bool
< :: BoundTyVar -> BoundTyVar -> Bool
$c<= :: BoundTyVar -> BoundTyVar -> Bool
<= :: BoundTyVar -> BoundTyVar -> Bool
$c> :: BoundTyVar -> BoundTyVar -> Bool
> :: BoundTyVar -> BoundTyVar -> Bool
$c>= :: BoundTyVar -> BoundTyVar -> Bool
>= :: BoundTyVar -> BoundTyVar -> Bool
$cmax :: BoundTyVar -> BoundTyVar -> BoundTyVar
max :: BoundTyVar -> BoundTyVar -> BoundTyVar
$cmin :: BoundTyVar -> BoundTyVar -> BoundTyVar
min :: BoundTyVar -> BoundTyVar -> BoundTyVar
Ord
    )

-- | Given a DeBruijn index (designating scope) and positional index (designating
-- which variable in that scope we are interested in), retrieve an in-scope type
-- variable.
--
-- This will error if we request a type variable in a scope that doesn't exist,
-- or at a position that doesn't exist in that scope.
--
-- @since 1.2.0
boundTyVar ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  DeBruijn ->
  Index "tyvar" ->
  m BoundTyVar
boundTyVar :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
DeBruijn -> Index "tyvar" -> m BoundTyVar
boundTyVar DeBruijn
scope Index "tyvar"
index = do
  let scopeAsInt :: Int
scopeAsInt = Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
scope
      indexAsWord :: Word32
      indexAsWord :: Word32
indexAsWord = Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word32) -> Int -> Word32
forall a b. (a -> b) -> a -> b
$ Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
index
  Bool
tyVarInScope <-
    (ASGEnv -> Maybe Word32) -> m (Maybe Word32)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' An_AffineTraversal NoIx ASGEnv Word32
-> ASGEnv -> Maybe Word32
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
#scopeInfo Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
-> Optic
     A_Lens
     NoIx
     ScopeInfo
     ScopeInfo
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     A_Lens
     NoIx
     ASGEnv
     ASGEnv
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
#argumentInfo Optic
  A_Lens
  NoIx
  ASGEnv
  ASGEnv
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Word32, Vector (ValT AbstractTy))))
     NoIx
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
-> Optic
     An_AffineTraversal
     NoIx
     ASGEnv
     ASGEnv
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Word32, Vector (ValT AbstractTy))))
     NoIx
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (Vector (Word32, Vector (ValT AbstractTy)))
scopeAsInt Optic
  An_AffineTraversal
  NoIx
  ASGEnv
  ASGEnv
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
-> Optic
     A_Lens
     NoIx
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
     Word32
     Word32
-> Optic' An_AffineTraversal NoIx ASGEnv Word32
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  (IxValue (Vector (Word32, Vector (ValT AbstractTy))))
  Word32
  Word32
forall s t a b. Field1 s t a b => Lens s t a b
_1)) m (Maybe Word32) -> (Maybe Word32 -> m Bool) -> m Bool
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe Word32
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
      Just Word32
varsBoundAtScope ->
        -- varsBoundAtScope is the count of the CompT binding context verbatim
        if Word32
varsBoundAtScope Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word32
0
          then Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
          else Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Word32
indexAsWord Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
< Word32
varsBoundAtScope
  if Bool
tyVarInScope
    then BoundTyVar -> m BoundTyVar
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (DeBruijn -> Index "tyvar" -> BoundTyVar
BoundTyVar DeBruijn
scope Index "tyvar"
index)
    else CovenantTypeError -> m BoundTyVar
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m BoundTyVar)
-> CovenantTypeError -> m BoundTyVar
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> CovenantTypeError
OutOfScopeTyVar DeBruijn
scope Index "tyvar"
index

-- To avoid annoying code duplication

-- Helper to avoid having to manually catch and rethrow the error
undoRenameM ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  ValT Renamed ->
  m (ValT AbstractTy)
undoRenameM :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM ValT Renamed
val = do
  Vector Word32
scope <- (ASGEnv -> Vector Word32) -> m (Vector Word32)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (((Word32, Vector (ValT AbstractTy)) -> Word32)
-> Vector (Word32, Vector (ValT AbstractTy)) -> Vector Word32
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word32, Vector (ValT AbstractTy)) -> Word32
forall a b. (a, b) -> a
fst (Vector (Word32, Vector (ValT AbstractTy)) -> Vector Word32)
-> (ASGEnv -> Vector (Word32, Vector (ValT AbstractTy)))
-> ASGEnv
-> Vector Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic
  A_Lens
  NoIx
  ASGEnv
  ASGEnv
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
-> ASGEnv -> Vector (Word32, Vector (ValT AbstractTy))
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
#scopeInfo Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
-> Optic
     A_Lens
     NoIx
     ScopeInfo
     ScopeInfo
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     A_Lens
     NoIx
     ASGEnv
     ASGEnv
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
#argumentInfo))
  case Vector Word32
-> ValT Renamed -> Either UnRenameError (ValT AbstractTy)
undoRename Vector Word32
scope ValT Renamed
val of
    Left UnRenameError
err' -> CovenantTypeError -> m (ValT AbstractTy)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy))
-> CovenantTypeError -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ UnRenameError -> CovenantTypeError
UndoRenameFailure UnRenameError
err'
    Right ValT AbstractTy
renamed -> ValT AbstractTy -> m (ValT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
renamed

askScope ::
  forall (m :: Type -> Type).
  (MonadReader ASGEnv m) =>
  m (Vector Word32)
askScope :: forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope = (ASGEnv -> Vector Word32) -> m (Vector Word32)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (((Word32, Vector (ValT AbstractTy)) -> Word32)
-> Vector (Word32, Vector (ValT AbstractTy)) -> Vector Word32
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word32, Vector (ValT AbstractTy)) -> Word32
forall a b. (a, b) -> a
fst (Vector (Word32, Vector (ValT AbstractTy)) -> Vector Word32)
-> (ASGEnv -> Vector (Word32, Vector (ValT AbstractTy)))
-> ASGEnv
-> Vector Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic
  A_Lens
  NoIx
  ASGEnv
  ASGEnv
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
-> ASGEnv -> Vector (Word32, Vector (ValT AbstractTy))
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
#scopeInfo Optic A_Lens NoIx ASGEnv ASGEnv ScopeInfo ScopeInfo
-> Optic
     A_Lens
     NoIx
     ScopeInfo
     ScopeInfo
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
-> Optic
     A_Lens
     NoIx
     ASGEnv
     ASGEnv
     (Vector (Word32, Vector (ValT AbstractTy)))
     (Vector (Word32, Vector (ValT AbstractTy)))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Word32, Vector (ValT AbstractTy)))
  (Vector (Word32, Vector (ValT AbstractTy)))
#argumentInfo))

-- Runs a UnifyM computation in our abstract monad. Again, largely to avoid superfluous code
-- duplication.
liftUnifyM ::
  forall (m :: Type -> Type) (a :: Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  UnifyM a ->
  m a
liftUnifyM :: forall (m :: Type -> Type) a.
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
UnifyM a -> m a
liftUnifyM UnifyM a
act = do
  Map TyName (DatatypeInfo AbstractTy)
tyDict <- (ASGEnv -> Map TyName (DatatypeInfo AbstractTy))
-> m (Map TyName (DatatypeInfo AbstractTy))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
-> ASGEnv -> Map TyName (DatatypeInfo AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx ASGEnv (Map TyName (DatatypeInfo AbstractTy))
#datatypeInfo)
  case Map TyName (DatatypeInfo AbstractTy)
-> UnifyM a -> Either TypeAppError a
forall a.
Map TyName (DatatypeInfo AbstractTy)
-> UnifyM a -> Either TypeAppError a
runUnifyM Map TyName (DatatypeInfo AbstractTy)
tyDict UnifyM a
act of
    Left TypeAppError
e -> CovenantTypeError -> m a
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m a) -> CovenantTypeError -> m a
forall a b. (a -> b) -> a -> b
$ TypeAppError -> CovenantTypeError
UnificationError TypeAppError
e
    Right a
res -> a -> m a
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
res

-- Utility functions for ASG construction. These are not strictly necessary, but are extremely convenient.

-- | Constructs a datatype value at given constructor. This is different to
-- 'dataConstructor', as it doesn't produce a thunk.
--
-- The third argument is a 'Vector' of values to \'fill in\' all the fields
-- required by the stated constructor. The fourth argument is a 'Vector' of
-- \'type instantiations\', which allow \'concretification\' of any lingering
-- polymorphic type variables which are not determined by the field values given
-- as the third argument.
--
-- = Example
--
-- Consider @Left 3@. In this case, the field only determines the first type
-- argument to the @Either@ data type, and if we used 'dataConstructor', we
-- would be left with a thunk of type @<forall a . !Either Integer a>@. Using
-- 'ctor', we can immediately specify what @a@ should be, and unwrap the thunk.
--
-- @since 1.2.0
ctor ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  TyName ->
  ConstructorName ->
  Vector.Vector Ref ->
  Vector.Vector (Wedge BoundTyVar (ValT Void)) ->
  m Id
ctor :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
TyName
-> ConstructorName
-> Vector Ref
-> Vector (Wedge BoundTyVar (ValT Void))
-> m Id
ctor TyName
tn ConstructorName
cn Vector Ref
args Vector (Wedge BoundTyVar (ValT Void))
instTys = do
  Id
dataThunk <- TyName -> ConstructorName -> Vector Ref -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
TyName -> ConstructorName -> Vector Ref -> m Id
dataConstructor TyName
tn ConstructorName
cn Vector Ref
args
  Id
dataForced <- Ref -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m Id
force (Id -> Ref
AnId Id
dataThunk)
  Id -> Vector Ref -> Vector (Wedge BoundTyVar (ValT Void)) -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Id -> Vector Ref -> Vector (Wedge BoundTyVar (ValT Void)) -> m Id
app Id
dataForced Vector Ref
forall a. Monoid a => a
mempty Vector (Wedge BoundTyVar (ValT Void))
instTys

-- | As 'lam', but produces a thunk value instead of a computation.
--
-- @since 1.2.0
lazyLam ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  CompT AbstractTy ->
  m Ref ->
  m Id
lazyLam :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
CompT AbstractTy -> m Ref -> m Id
lazyLam CompT AbstractTy
expected m Ref
bodyComp = CompT AbstractTy -> m Ref -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
CompT AbstractTy -> m Ref -> m Id
lam CompT AbstractTy
expected m Ref
bodyComp m Id -> (Id -> m Id) -> m Id
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Id -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m Id
thunk

-- | Helper to avoid using 'Vector.fromList' when defining data types.
--
-- @since 1.2.0
dtype :: TyName -> [ValT AbstractTy] -> ValT AbstractTy
dtype :: TyName -> [ValT AbstractTy] -> ValT AbstractTy
dtype TyName
tn = TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> ([ValT AbstractTy] -> Vector (ValT AbstractTy))
-> [ValT AbstractTy]
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ValT AbstractTy] -> Vector (ValT AbstractTy)
forall a. [a] -> Vector a
Vector.fromList