{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
{-# 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 (ASG),

    -- ** Functions
    topLevelId,
    topLevelNode,
    nodeAt,

    -- * ASG components

    -- ** Types
    Id (Id),
    Ref (..),
    Arg (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,
    ctor',
    lazyLam,
    dtype,
    baseFunctorOf,
    naturalBF,
    negativeBF,
    app',

    -- *** 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, primBaseFunctorInfos)
import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
import Covenant.Index (Count, Index, count0, intCount, intIndex, ix0, 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 (UnsafeMkArg),
    BoundTyVar (BoundTyVar),
    CompNodeInfo
      ( Builtin1Internal,
        Builtin2Internal,
        Builtin3Internal,
        Builtin6Internal,
        ForceInternal,
        LamInternal
      ),
    CovenantTypeError
      ( ApplyCompType,
        ApplyToError,
        ApplyToValType,
        BaseFunctorDoesNotExistFor,
        BrokenIdReference,
        CataCouldNotRenameBB,
        CataCouldNotRenameHandler,
        CataCouldNotRenameSubstitutions,
        CataDidNotUnify,
        CataFixUpFailedForBB,
        CataHandlerNotAValType,
        CataInvalidStructure,
        CataMonomorphicBaseFunctor,
        CataNoTypeForBaseFunctor,
        CataNonRigidAlgebra,
        CataNotADatatypeBaseFunctor,
        CataNotAValueType,
        CataUnexpectedResultType,
        CataWrongArity,
        CataWrongNumberOfHandlers,
        CataWrongOutputType,
        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,
        WrongNumInstantiationsInApp,
        WrongReturnType
      ),
    Id (UnsafeMkId),
    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,
    concretifyFT,
    fixUp,
    reconcile,
    runUnifyM,
    substitute,
    unify,
  )
import Covenant.Prim
  ( OneArgFunc,
    SixArgFunc,
    ThreeArgFunc,
    TwoArgFunc,
    typeOneArgFunc,
    typeSixArgFunc,
    typeThreeArgFunc,
    typeTwoArgFunc,
  )
import Covenant.Type
  ( CompT (Comp0, Comp1, CompN),
    CompTBody (ArgsAndResult, ReturnT, (:--:>)),
    Constructor,
    ConstructorName,
    DataDeclaration (OpaqueData),
    PlutusDataConstructor (PlutusB, PlutusConstr, PlutusI, PlutusList, PlutusMap),
    Renamed (Unifiable),
    TyName (TyName),
    ValT (Abstraction),
    integerT,
    tyvar,
  )
import Covenant.Util (pattern ConsV, pattern NilV)
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, fromMaybe, 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 (Nowhere), wedge)
import Data.Word (Word32, Word64)
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    folded,
    ix,
    lens,
    over,
    preview,
    review,
    toListOf,
    view,
    (%),
    _1,
    _2,
  )

-- | A read-only pattern for exposing the internals of an 'Id'.
--
-- @since 1.3.1
pattern Id :: Word64 -> Id
pattern $mId :: forall {r}. Id -> (Word64 -> r) -> ((# #) -> r) -> r
Id w <- UnsafeMkId w

-- | A read-only pattern for exposing the internals of an 'Arg'.
--
-- @since 1.3.1
pattern Arg :: DeBruijn -> Index "arg" -> ValT AbstractTy -> Arg
pattern $mArg :: forall {r}.
Arg
-> (DeBruijn -> Index "arg" -> ValT AbstractTy -> r)
-> ((# #) -> r)
-> r
Arg db i t <- UnsafeMkArg db i t

-- | A fully-assembled Covenant ASG.
--
-- @since 1.0.0
newtype ASG = ASGInternal (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
    )

{-# COMPLETE ASG #-}

-- | @since 1.3.0
pattern ASG :: Map Id ASGNode -> ASG
pattern $mASG :: forall {r}. ASG -> (Map Id ASGNode -> r) -> ((# #) -> r) -> r
ASG m <- ASGInternal (_, m)

-- 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 'Id' of an ASG.
--
-- @since 1.3.0
topLevelId :: ASG -> Id
topLevelId :: ASG -> Id
topLevelId (ASGInternal (Id
i, Map Id ASGNode
_)) = Id
i

-- | Retrieves the top-level node of an ASG.
--
-- @since 1.0.0
topLevelNode :: ASG -> ASGNode
topLevelNode :: ASG -> ASGNode
topLevelNode asg :: ASG
asg@(ASGInternal (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 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
-- first 'Vector' argument contains the term arguments, while the second 'Vector'
-- argument contains the type arguments, as one of:
--
-- * 'Data.Wedge.Nowhere', meaning \'inferred\';
-- * 'Data.Wedge.Here', meaning \'a bound type variable from a parent scope\';
-- or
-- * 'Data.Wedge.There', meaning \'a concrete type\'.
--
-- The final CompT is the concretified function type, which is necessary for codegen.
-- @since 1.3.0
pattern App ::
  Id ->
  Vector Ref ->
  Vector (Wedge BoundTyVar (ValT Void)) ->
  CompT AbstractTy ->
  ValNodeInfo
pattern $mApp :: forall {r}.
ValNodeInfo
-> (Id
    -> Vector Ref
    -> Vector (Wedge BoundTyVar (ValT Void))
    -> CompT AbstractTy
    -> r)
-> ((# #) -> r)
-> r
App f args instTys concreteFnTy <- AppInternal f args instTys concreteFnTy

-- | 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. The first argument is
-- the signature of the algebra used; the second argument is
-- a list of \'handlers\' for the base functor, represented similar to 'Match'
-- handlers, while the third is the type of thing to be torn down.
--
-- @since 1.4.0
pattern Cata :: CompT AbstractTy -> Vector Ref -> Ref -> ValNodeInfo
pattern $mCata :: forall {r}.
ValNodeInfo
-> (CompT AbstractTy -> Vector Ref -> Ref -> r)
-> ((# #) -> r)
-> r
Cata algT handlerRefs valRef <- CataInternal algT handlerRefs 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 Map TyName (DatatypeInfo AbstractTy)
-> Map TyName (DatatypeInfo AbstractTy)
-> Map TyName (DatatypeInfo AbstractTy)
forall a. Semigroup a => a -> a -> a
<> Map TyName (DatatypeInfo AbstractTy)
primBaseFunctorInfos
  where
    go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
    go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
go DataDeclaration AbstractTy
decl = case DataDeclaration AbstractTy
-> Either BBFError (Map TyName (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 Map TyName (DatatypeInfo AbstractTy)
info -> Map TyName (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
ASGInternal ((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
UnsafeMkArg DeBruijn
scope Index "arg"
index (ValT AbstractTy -> Arg)
-> (ValT AbstractTy -> ValT AbstractTy) -> ValT AbstractTy -> Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType DeBruijn
scope (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 (UnsafeMkArg 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)
--
-- = Notes
--
-- We use the 'Wedge' data type to designate type arguments, as it can represent
-- the three possibilities we need:
--
-- * \'Infer this argument\', specified as 'Data.Wedge.Nowhere'.
-- * \'Use this type variable in our scope\', specified as 'Data.Wedge.Here'.
-- * \'Use this concrete type\', specified as 'Data.Wedge.There'.
--
-- The *only* purpose of explicit type application arguments is to instantiate a tyvar in the result which is
-- not determined by any argument. These variables are instantiated after every other argument has been concretified.
--
-- For example, if you have a function
--   @f :: forall a b c. (a -> b) -> (b -> a) -> b -> Either a c@
-- Then you will need to supply _one_ explicit type application to concretify @c@.
--
-- @since 1.3.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 renamedFT :: CompT Renamed
renamedFT@(CompT Count "tyvar"
count CompTBody Renamed
_) -> do
        let numInstantiations :: Int
numInstantiations = Vector (Wedge BoundTyVar (ValT Void)) -> Int
forall a. Vector a -> Int
Vector.length Vector (Wedge BoundTyVar (ValT Void))
instTys
            numVars :: Int
numVars = 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
        if Int
numInstantiations Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
numVars
          then 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 Renamed -> Int -> Int -> CovenantTypeError
WrongNumInstantiationsInApp CompT Renamed
renamedFT Int
numVars Int
numInstantiations
          else do
            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
            let concretifiedFT :: CompT Renamed
concretifiedFT = CompT Renamed -> Vector (Maybe (ValT Renamed)) -> CompT Renamed
concretifyFT CompT Renamed
renamedFT Vector (Maybe (ValT Renamed))
renamedArgs
            CompT Renamed
instantiatedFT <- [(Index "tyvar", ValT Renamed)]
-> CompT Renamed -> m (CompT Renamed)
instantiate [(Index "tyvar", ValT Renamed)]
subs CompT Renamed
concretifiedFT
            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
            CompT AbstractTy
unRenamedFnTy <- CompT Renamed -> m (CompT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
CompT Renamed -> m (CompT AbstractTy)
undoRenameCompT CompT Renamed
instantiatedFT
            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)
-> (ValNodeInfo -> ASGNode) -> ValNodeInfo -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
restored (ValNodeInfo -> m Id) -> ValNodeInfo -> m Id
forall a b. (a -> b) -> a -> b
$ Id
-> Vector Ref
-> Vector (Wedge BoundTyVar (ValT Void))
-> CompT AbstractTy
-> ValNodeInfo
AppInternal Id
fId Vector Ref
argRefs Vector (Wedge BoundTyVar (ValT Void))
instTys CompT AbstractTy
unRenamedFnTy
    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
    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

    -- NOTE: The helper function below only concerns instantiations that result from
    --       explicit type applications (via the third argument to `app`).
    --
    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
        )
        []

    instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
    instantiate :: [(Index "tyvar", ValT Renamed)]
-> CompT Renamed -> m (CompT Renamed)
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 computation type for an algebra (the \'stated algebra type\'), as
-- well as a set of handlers designed to deal with each case of the stated
-- algebra's base functor, plus a 'Ref' to a value associated with that base
-- functor, build a catamorphism to tear that value down.
--
-- Ensure the following:
--
-- * The stated algebra type must be a 'Comp0' taking a base functor and
--   returning the same type as the last type variable instantiation of that base
--   functor.
-- * The handlers must be provided in the same order as the constructors of the
--   parameter of the stated algebra type. Handlers for \'arms\' with no fields
--   must be non-thunks, while handlers for \'arms\' with fields must be thunks.
-- * The third argument must be a value type with a base functor.
--
-- @since 1.3.0
cata ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  CompT AbstractTy ->
  Vector Ref ->
  Ref ->
  m Id
cata :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
CompT AbstractTy -> Vector Ref -> Ref -> m Id
cata CompT AbstractTy
algT Vector Ref
handlers Ref
rVal =
  CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
forall (m :: Type -> Type).
(MonadReader ASGEnv m, MonadError CovenantTypeError m) =>
CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
getCataInfo CompT AbstractTy
algT m (ValT AbstractTy, CataInfo)
-> ((ValT AbstractTy, CataInfo) -> 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
    (ValT AbstractTy
resultT, CataInfo
IntegerCata) ->
      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 (BuiltinFlat BuiltinFlatT
IntegerT) -> ValT AbstractTy -> CompT AbstractTy -> m Id
tryApply ValT AbstractTy
resultT CompT AbstractTy
integerBB
        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
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
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
CataNotAValueType (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
    (ValT AbstractTy
resultT, CataInfo
ByteStringCata) ->
      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 (BuiltinFlat BuiltinFlatT
ByteStringT) -> ValT AbstractTy -> CompT AbstractTy -> m Id
tryApply ValT AbstractTy
resultT CompT AbstractTy
bsBB
        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
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
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
CataNotAValueType (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
    (ValT AbstractTy
resultT, RigidCata TyName
expectedTyName CompT AbstractTy
bbForm) ->
      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 t :: ValT AbstractTy
t@(Datatype TyName
tyName Vector (ValT AbstractTy)
_) -> do
          Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (TyName
tyName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
expectedTyName) (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
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t)
          ValT AbstractTy -> CompT AbstractTy -> m Id
tryApply ValT AbstractTy
resultT CompT AbstractTy
bbForm
        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
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
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
CataNotAValueType (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
    (ValT AbstractTy
resultT, NonRigidCata TyName
expectedTyName ValT AbstractTy
bbf) ->
      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 t :: ValT AbstractTy
t@(Datatype TyName
tyName Vector (ValT AbstractTy)
tyVars) -> do
          Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (TyName
tyName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
expectedTyName) (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
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t)
          ValT AbstractTy
-> ValT AbstractTy -> Vector (ValT AbstractTy) -> m Id
tryApplySubstituting ValT AbstractTy
resultT ValT AbstractTy
bbf Vector (ValT AbstractTy)
tyVars
        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
. CompT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataInvalidStructure CompT AbstractTy
algT (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
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
CataNotAValueType (ASGNodeType -> m Id) -> ASGNodeType -> m Id
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
  where
    integerBB :: CompT AbstractTy
    integerBB :: CompT AbstractTy
integerBB =
      CompTBody AbstractTy -> CompT AbstractTy
forall a. CompTBody a -> CompT a
Comp1 (CompTBody AbstractTy -> CompT AbstractTy)
-> CompTBody AbstractTy -> CompT AbstractTy
forall a b. (a -> b) -> a -> b
$
        DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar DeBruijn
Z Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0
          ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompTBody AbstractTy -> CompT AbstractTy
forall a. CompTBody a -> CompT a
Comp0 (CompTBody AbstractTy -> CompT AbstractTy)
-> CompTBody AbstractTy -> CompT AbstractTy
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar (DeBruijn -> DeBruijn
S DeBruijn
Z) Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0 ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> ValT AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a
ReturnT (DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar (DeBruijn -> DeBruijn
S DeBruijn
Z) Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0))
          ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> ValT AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a
ReturnT (DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar DeBruijn
Z Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0)
    bsBB :: CompT AbstractTy
    bsBB :: CompT AbstractTy
bsBB =
      CompTBody AbstractTy -> CompT AbstractTy
forall a. CompTBody a -> CompT a
Comp1 (CompTBody AbstractTy -> CompT AbstractTy)
-> CompTBody AbstractTy -> CompT AbstractTy
forall a b. (a -> b) -> a -> b
$
        DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar DeBruijn
Z Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0
          ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompTBody AbstractTy -> CompT AbstractTy
forall a. CompTBody a -> CompT a
Comp0 (CompTBody AbstractTy -> CompT AbstractTy)
-> CompTBody AbstractTy -> CompT AbstractTy
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
forall a. ValT a
integerT ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar (DeBruijn -> DeBruijn
S DeBruijn
Z) Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0 ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> ValT AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a
ReturnT (DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar (DeBruijn -> DeBruijn
S DeBruijn
Z) Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0))
          ValT AbstractTy -> CompTBody AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a -> CompTBody a
:--:> ValT AbstractTy -> CompTBody AbstractTy
forall a. ValT a -> CompTBody a
ReturnT (DeBruijn -> Index "tyvar" -> ValT AbstractTy
tyvar DeBruijn
Z Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0)
    tryApplySubstituting :: ValT AbstractTy -> ValT AbstractTy -> Vector (ValT AbstractTy) -> m Id
    tryApplySubstituting :: ValT AbstractTy
-> ValT AbstractTy -> Vector (ValT AbstractTy) -> m Id
tryApplySubstituting ValT AbstractTy
resultT ValT AbstractTy
bbThunk Vector (ValT AbstractTy)
subs = do
      Vector Word32
scopeInfo <- m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope
      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 Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (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
bbThunk of
        Right ValT Renamed
renamedBBThunk -> case (ValT AbstractTy -> Either RenameError (ValT Renamed))
-> Vector (ValT AbstractTy)
-> Either RenameError (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 (Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (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) Vector (ValT AbstractTy)
subs of
          Right Vector (ValT Renamed)
renamedSubs -> case Map TyName (DatatypeInfo AbstractTy)
-> UnifyM (ValT Renamed) -> Either TypeAppError (ValT Renamed)
forall a.
Map TyName (DatatypeInfo AbstractTy)
-> UnifyM a -> Either TypeAppError a
runUnifyM Map TyName (DatatypeInfo AbstractTy)
tyDict (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
. Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
doSubsVal Vector (ValT Renamed)
renamedSubs (ValT Renamed -> UnifyM (ValT Renamed))
-> ValT Renamed -> UnifyM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed
renamedBBThunk) of
            Right ValT Renamed
substitutedBBThunk -> do
              Vector (ValT AbstractTy)
asArgs <- (Ref -> m (ValT AbstractTy))
-> Vector Ref -> m (Vector (ValT AbstractTy))
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 AbstractTy)
handlerToArg Vector Ref
handlers
              case (ValT AbstractTy -> Either RenameError (ValT Renamed))
-> Vector (ValT AbstractTy)
-> Either RenameError (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 (Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (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) Vector (ValT AbstractTy)
asArgs of
                Right Vector (ValT Renamed)
renamedHandlers -> case Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict (ValT Renamed -> CompT Renamed
forall a. Show a => ValT a -> CompT a
fromThunk ValT Renamed
substitutedBBThunk) ((ValT Renamed -> Maybe (ValT Renamed))
-> [ValT Renamed] -> [Maybe (ValT Renamed)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just ([ValT Renamed] -> [Maybe (ValT Renamed)])
-> (Vector (ValT Renamed) -> [ValT Renamed])
-> Vector (ValT Renamed)
-> [Maybe (ValT Renamed)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList (Vector (ValT Renamed) -> [Maybe (ValT Renamed)])
-> Vector (ValT Renamed) -> [Maybe (ValT Renamed)]
forall a b. (a -> b) -> a -> b
$ Vector (ValT Renamed)
renamedHandlers) of
                  Right ValT Renamed
result -> do
                    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
                    Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (ValT AbstractTy
restored ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
resultT) (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
. ValT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataUnexpectedResultType ValT AbstractTy
resultT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
restored)
                    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
restored (ValNodeInfo -> ASGNode) -> (Ref -> ValNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> Vector Ref -> Ref -> ValNodeInfo
CataInternal CompT AbstractTy
algT Vector Ref
handlers (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
rVal
                  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
. CompT AbstractTy -> Vector Ref -> TypeAppError -> CovenantTypeError
CataDidNotUnify CompT AbstractTy
algT Vector Ref
handlers (TypeAppError -> m Id) -> TypeAppError -> m Id
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
                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 -> Vector Ref -> RenameError -> CovenantTypeError
CataCouldNotRenameHandler CompT AbstractTy
algT Vector Ref
handlers (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
            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
. CompT AbstractTy
-> Vector Ref
-> Vector (ValT AbstractTy)
-> ValT Renamed
-> TypeAppError
-> CovenantTypeError
CataFixUpFailedForBB CompT AbstractTy
algT Vector Ref
handlers Vector (ValT AbstractTy)
subs ValT Renamed
renamedBBThunk (TypeAppError -> m Id) -> TypeAppError -> m Id
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
          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
-> Vector Ref
-> CompT AbstractTy
-> Vector (ValT AbstractTy)
-> RenameError
-> CovenantTypeError
CataCouldNotRenameSubstitutions CompT AbstractTy
algT Vector Ref
handlers (ValT AbstractTy -> CompT AbstractTy
forall a. Show a => ValT a -> CompT a
fromThunk ValT AbstractTy
bbThunk) Vector (ValT AbstractTy)
subs (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
        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
-> Vector Ref
-> CompT AbstractTy
-> RenameError
-> CovenantTypeError
CataCouldNotRenameBB CompT AbstractTy
algT Vector Ref
handlers (ValT AbstractTy -> CompT AbstractTy
forall a. Show a => ValT a -> CompT a
fromThunk ValT AbstractTy
bbThunk) (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
    fromThunk :: forall (a :: Type). (Show a) => ValT a -> CompT a
    fromThunk :: forall a. Show a => ValT a -> CompT a
fromThunk = \case
      ThunkT CompT a
t -> CompT a
t
      ValT a
t -> [Char] -> CompT a
forall a. HasCallStack => [Char] -> a
error ([Char] -> CompT a) -> [Char] -> CompT a
forall a b. (a -> b) -> a -> b
$ [Char]
"cata: ValT given by getCataInfo wasn't a thunk as expected" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ValT a -> [Char]
forall a. Show a => a -> [Char]
show ValT a
t
    tryApply :: ValT AbstractTy -> CompT AbstractTy -> m Id
    tryApply :: ValT AbstractTy -> CompT AbstractTy -> m Id
tryApply ValT AbstractTy
resultT CompT AbstractTy
bb = do
      let bbArity :: Int
bbArity = CompT AbstractTy -> Int
forall a. CompT a -> Int
arity CompT AbstractTy
bb
      Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Int
bbArity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector Ref -> Int
forall a. Vector a -> Int
Vector.length Vector Ref
handlers) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (Vector Ref -> CovenantTypeError) -> Vector Ref -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> Vector Ref -> CovenantTypeError
CataWrongNumberOfHandlers CompT AbstractTy
algT (Vector Ref -> m ()) -> Vector Ref -> m ()
forall a b. (a -> b) -> a -> b
$ Vector Ref
handlers)
      Vector Word32
scopeInfo <- m (Vector Word32)
forall (m :: Type -> Type).
MonadReader ASGEnv m =>
m (Vector Word32)
askScope
      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
bb of
        Right CompT Renamed
renamedBB -> 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)
          Vector (ValT AbstractTy)
asArgs <- (Ref -> m (ValT AbstractTy))
-> Vector Ref -> m (Vector (ValT AbstractTy))
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 AbstractTy)
handlerToArg Vector Ref
handlers
          case (ValT AbstractTy -> Either RenameError (ValT Renamed))
-> Vector (ValT AbstractTy)
-> Either RenameError (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 (Vector Word32
-> RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (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) Vector (ValT AbstractTy)
asArgs of
            Right Vector (ValT Renamed)
renamedHandlers -> case Map TyName (DatatypeInfo AbstractTy)
-> CompT Renamed
-> [Maybe (ValT Renamed)]
-> Either TypeAppError (ValT Renamed)
checkApp Map TyName (DatatypeInfo AbstractTy)
tyDict CompT Renamed
renamedBB ((ValT Renamed -> Maybe (ValT Renamed))
-> [ValT Renamed] -> [Maybe (ValT Renamed)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ValT Renamed -> Maybe (ValT Renamed)
forall a. a -> Maybe a
Just ([ValT Renamed] -> [Maybe (ValT Renamed)])
-> (Vector (ValT Renamed) -> [ValT Renamed])
-> Vector (ValT Renamed)
-> [Maybe (ValT Renamed)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT Renamed) -> [ValT Renamed]
forall a. Vector a -> [a]
Vector.toList (Vector (ValT Renamed) -> [Maybe (ValT Renamed)])
-> Vector (ValT Renamed) -> [Maybe (ValT Renamed)]
forall a b. (a -> b) -> a -> b
$ Vector (ValT Renamed)
renamedHandlers) of
              Right ValT Renamed
result -> do
                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
                Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (ValT AbstractTy
restored ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
resultT) (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
. ValT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataUnexpectedResultType ValT AbstractTy
resultT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
restored)
                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
restored (ValNodeInfo -> ASGNode) -> (Ref -> ValNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> Vector Ref -> Ref -> ValNodeInfo
CataInternal CompT AbstractTy
algT Vector Ref
handlers (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
rVal
              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
. CompT AbstractTy -> Vector Ref -> TypeAppError -> CovenantTypeError
CataDidNotUnify CompT AbstractTy
algT Vector Ref
handlers (TypeAppError -> m Id) -> TypeAppError -> m Id
forall a b. (a -> b) -> a -> b
$ TypeAppError
err'
            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 -> Vector Ref -> RenameError -> CovenantTypeError
CataCouldNotRenameHandler CompT AbstractTy
algT Vector Ref
handlers (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
        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
-> Vector Ref
-> CompT AbstractTy
-> RenameError
-> CovenantTypeError
CataCouldNotRenameBB CompT AbstractTy
algT Vector Ref
handlers CompT AbstractTy
bb (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
    handlerToArg :: Ref -> m (ValT AbstractTy)
    handlerToArg :: Ref -> m (ValT AbstractTy)
handlerToArg =
      Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef (Ref -> m ASGNodeType)
-> (ASGNodeType -> m (ValT AbstractTy))
-> Ref
-> m (ValT AbstractTy)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
        ValNodeType ValT AbstractTy
t -> ValT AbstractTy -> m (ValT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ValT AbstractTy
t
        ASGNodeType
t -> 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))
-> (ASGNodeType -> CovenantTypeError)
-> ASGNodeType
-> m (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNodeType -> CovenantTypeError
CataHandlerNotAValType (ASGNodeType -> m (ValT AbstractTy))
-> ASGNodeType -> m (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ ASGNodeType
t
    doSubsComp :: Vector (ValT Renamed) -> CompT Renamed -> CompT Renamed
    doSubsComp :: Vector (ValT Renamed) -> CompT Renamed -> CompT Renamed
doSubsComp Vector (ValT Renamed)
subs (CompT Count "tyvar"
count (CompTBody NonEmptyVector (ValT Renamed)
nev)) = Count "tyvar" -> CompTBody Renamed -> CompT Renamed
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
count (CompTBody Renamed -> CompT Renamed)
-> (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> NonEmptyVector (ValT Renamed)
-> CompT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT Renamed) -> CompTBody Renamed
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> (NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed))
-> NonEmptyVector (ValT Renamed)
-> CompTBody Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValT Renamed -> ValT Renamed)
-> NonEmptyVector (ValT Renamed) -> NonEmptyVector (ValT Renamed)
forall a b. (a -> b) -> NonEmptyVector a -> NonEmptyVector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
doSubsVal Vector (ValT Renamed)
subs) (NonEmptyVector (ValT Renamed) -> CompT Renamed)
-> NonEmptyVector (ValT Renamed) -> CompT Renamed
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT Renamed)
nev
    doSubsVal :: Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
    doSubsVal :: Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
doSubsVal Vector (ValT Renamed)
subs = \case
      -- Note (Koz, 11/11/2025): The indexing ends up being a bit strange here,
      -- as the _last_ tyvar in a BB form is always meant to stay abstract.
      -- However, this means that if we have `n` substitutions, we have `n + 1`
      -- possible unifiables for those substitutions to go into. Thus, doing a
      -- blind indexing into `subs` can blow up.
      --
      -- Thus, if we 'miss', we should leave it alone.
      t :: ValT Renamed
t@(Abstraction (Unifiable Index "tyvar"
i)) -> ValT Renamed -> Maybe (ValT Renamed) -> ValT Renamed
forall a. a -> Maybe a -> a
fromMaybe ValT Renamed
t (Maybe (ValT Renamed) -> ValT Renamed)
-> Maybe (ValT Renamed) -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ Vector (ValT Renamed)
subs Vector (ValT Renamed) -> Int -> Maybe (ValT Renamed)
forall a. Vector a -> Int -> Maybe a
Vector.!? 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"
i
      ThunkT CompT Renamed
someComp -> CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (CompT Renamed -> ValT Renamed)
-> (CompT Renamed -> CompT Renamed)
-> CompT Renamed
-> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT Renamed) -> CompT Renamed -> CompT Renamed
doSubsComp Vector (ValT Renamed)
subs (CompT Renamed -> ValT Renamed) -> CompT Renamed -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ CompT Renamed
someComp
      Datatype TyName
tyName Vector (ValT Renamed)
tyVars -> TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tyName (Vector (ValT Renamed) -> ValT Renamed)
-> (Vector (ValT Renamed) -> Vector (ValT Renamed))
-> Vector (ValT Renamed)
-> ValT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValT Renamed -> ValT Renamed)
-> Vector (ValT Renamed) -> Vector (ValT Renamed)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
doSubsVal Vector (ValT Renamed)
subs) (Vector (ValT Renamed) -> ValT Renamed)
-> Vector (ValT Renamed) -> ValT Renamed
forall a b. (a -> b) -> a -> b
$ Vector (ValT Renamed)
tyVars
      ValT Renamed
t -> ValT Renamed
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.
--
-- = Note
--
-- Opaque the handlers for an opaque type must follow the order:
--
--  @
--  [ PlutusI,
--    PlutusB,
--    PlutusConstr,
--    PlutusMap,
--    PlutusList
--  ]
--  @
--
--  Where types not included in the provided constructors to the opaque declaration are omitted.
--
--  Furthermore, the handlers for opaque constructors operate on the unwrapped arguments to
--  their respective PlutusData constructor. That is, for some result type @r@, the handlers for a
--  an opaque type which uses all the constructors should have the types:
--
--  @
--    PlutusI :: Integer -> r
--    PlutusB :: ByteString -> r
--    PlutusConstr :: Integer -> [Data] -> r
--    PlutusMap :: [(Integer,Data)] -> r
--    PlutusList :: [Data] -> r
--  @
--
-- @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)))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (Maybe (DataDeclaration AbstractTy, ValT 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)))
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT 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)))
     (IxValue (Map TyName (DatatypeInfo AbstractTy)))
     (Maybe (DataDeclaration AbstractTy, ValT 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)))
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
  (Maybe (DataDeclaration AbstractTy, ValT 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
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rawTn) (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

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

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

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

undoRenameCompT ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  CompT Renamed ->
  m (CompT AbstractTy)
undoRenameCompT :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
CompT Renamed -> m (CompT AbstractTy)
undoRenameCompT CompT Renamed
comp =
  ValT Renamed -> m (ValT AbstractTy)
forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
ValT Renamed -> m (ValT AbstractTy)
undoRenameM (CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT CompT Renamed
comp) m (ValT AbstractTy)
-> (ValT AbstractTy -> m (CompT AbstractTy))
-> m (CompT 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
>>= \case
    ThunkT CompT AbstractTy
res -> CompT AbstractTy -> m (CompT AbstractTy)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CompT AbstractTy
res
    -- This really should be impossible, not just unlikely.
    ValT AbstractTy
_other -> [Char] -> m (CompT AbstractTy)
forall a. HasCallStack => [Char] -> a
error [Char]
"Undoing renaming on a CompT resulting in something other than a thunk, which should be totally impossible"

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

-- | 'ctor' without the instantiation arguments, which are left up to inference.
--
-- @since 1.3.0
ctor' ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  TyName ->
  ConstructorName ->
  Vector.Vector Ref ->
  m Id
ctor' :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
TyName -> ConstructorName -> Vector Ref -> m Id
ctor' TyName
tn ConstructorName
cn Vector Ref
args = 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 -> m Id
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Id -> Vector Ref -> m Id
app' Id
dataForced Vector Ref
forall a. Monoid a => a
mempty

-- | A variant of `app` which does not take a 'Vector' of type instantiation
-- arguments and instead will try to infer all type arguments.
--
-- @since 1.3.0
app' ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  Id ->
  Vector Ref ->
  m Id
app' :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ASGEnv m) =>
Id -> Vector Ref -> m Id
app' Id
fId Vector Ref
args =
  Id -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
fId 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
    CompNodeType (CompT Count "tyvar"
count CompTBody AbstractTy
_) -> do
      let numVars :: Int
numVars = 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
          instArgs :: Vector (Wedge BoundTyVar (ValT Void))
instArgs = Int
-> Wedge BoundTyVar (ValT Void)
-> Vector (Wedge BoundTyVar (ValT Void))
forall a. Int -> a -> Vector a
Vector.replicate Int
numVars Wedge BoundTyVar (ValT Void)
forall a b. Wedge a b
Nowhere
      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
fId Vector Ref
args Vector (Wedge BoundTyVar (ValT Void))
instArgs
    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

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

-- | Helper for constructing a base functor name without having know the internal naming convention for
--   base functors.
--
-- @since 1.3.0
baseFunctorOf ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
  TyName ->
  m TyName
baseFunctorOf :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
TyName -> m TyName
baseFunctorOf (TyName Text
tn) = do
  let bfTn :: TyName
bfTn = Text -> TyName
TyName (Text
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
tn)
  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 Optic'
  (IxKind (Map TyName (DatatypeInfo AbstractTy)))
  NoIx
  (Map TyName (DatatypeInfo AbstractTy))
  (IxValue (Map TyName (DatatypeInfo AbstractTy)))
-> Map TyName (DatatypeInfo AbstractTy)
-> 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 (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
bfTn) Map TyName (DatatypeInfo AbstractTy)
tyDict of
    Maybe (IxValue (Map TyName (DatatypeInfo AbstractTy)))
Nothing -> CovenantTypeError -> m TyName
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m TyName) -> CovenantTypeError -> m TyName
forall a b. (a -> b) -> a -> b
$ TyName -> CovenantTypeError
BaseFunctorDoesNotExistFor (Text -> TyName
TyName Text
tn)
    Just {} -> TyName -> m TyName
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TyName
bfTn

-- | The name of the @Natural@ base functor for @Integer@.
--
-- This is required because @Integer@ is the only type with two base functors,
-- and thus, its base functor cannot be determined from the type name alone.
--
-- @since 1.3.0
naturalBF :: TyName
naturalBF :: TyName
naturalBF = Text -> TyName
TyName Text
"#Natural"

-- | The name of the @Negative@ base functor for @Integer@.
--
-- This is required because @Integer@ is the only type with two base functors,
-- and thus, its base functor cannot be determined from the type name alone.
--
-- @since 1.3.0
negativeBF :: TyName
negativeBF :: TyName
negativeBF = Text -> TyName
TyName Text
"#Negative"

-- Used as a helper for catamorphisms to classify what we need to do based on
-- the stated algebra type
data CataInfo
  = IntegerCata
  | ByteStringCata
  | RigidCata TyName (CompT AbstractTy)
  | NonRigidCata TyName (ValT AbstractTy)

getCataInfo ::
  forall (m :: Type -> Type).
  (MonadReader ASGEnv m, MonadError CovenantTypeError m) =>
  CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
getCataInfo :: forall (m :: Type -> Type).
(MonadReader ASGEnv m, MonadError CovenantTypeError m) =>
CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
getCataInfo CompT AbstractTy
t = case CompT AbstractTy
t of
  Comp0 (CompTBody NonEmptyVector (ValT AbstractTy)
nev) -> do
    Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (NonEmptyVector (ValT AbstractTy) -> Int
forall a. NonEmptyVector a -> Int
NonEmpty.length NonEmptyVector (ValT AbstractTy)
nev Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2) (CovenantTypeError -> m ()
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ())
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
CataWrongArity (CompT AbstractTy -> m ()) -> CompT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t)
    let inputT :: ValT AbstractTy
inputT = NonEmptyVector (ValT AbstractTy)
nev NonEmptyVector (ValT AbstractTy) -> Int -> ValT AbstractTy
forall a. NonEmptyVector a -> Int -> a
NonEmpty.! Int
0
    let outputT :: ValT AbstractTy
outputT = NonEmptyVector (ValT AbstractTy)
nev NonEmptyVector (ValT AbstractTy) -> Int -> ValT AbstractTy
forall a. NonEmptyVector a -> Int -> a
NonEmpty.! Int
1
    case ValT AbstractTy
inputT of
      Datatype TyName
bfTyName Vector (ValT AbstractTy)
bfTyVars ->
        (ValT AbstractTy -> ValT AbstractTy
stepDown ValT AbstractTy
outputT,) (CataInfo -> (ValT AbstractTy, CataInfo))
-> m CataInfo -> m (ValT AbstractTy, CataInfo)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> case Vector (ValT AbstractTy)
-> Maybe (Vector (ValT AbstractTy), ValT AbstractTy)
forall a. Vector a -> Maybe (Vector a, a)
Vector.unsnoc Vector (ValT AbstractTy)
bfTyVars of
          Just (Vector (ValT AbstractTy)
tyVarInsts, ValT AbstractTy
lastT) -> do
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (ValT AbstractTy
lastT ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
outputT) (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
. ValT AbstractTy -> ValT AbstractTy -> CovenantTypeError
CataWrongOutputType ValT AbstractTy
outputT (ValT AbstractTy -> m ()) -> ValT AbstractTy -> m ()
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
lastT)
            if
              | TyName
bfTyName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
naturalBF -> CataInfo -> m CataInfo
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CataInfo
IntegerCata
              | TyName
bfTyName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
negativeBF -> CataInfo -> m CataInfo
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CataInfo
IntegerCata
              -- Note (Koz, 10/11/2025): This is hacky as hell, but since
              -- ByteString is technically a builtin type, this is the only
              -- way to spot its base functor.
              | TyName
bfTyName TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"#ByteString" -> CataInfo -> m CataInfo
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CataInfo
ByteStringCata
              | Bool
otherwise -> do
                  Map TyName (DatatypeInfo AbstractTy)
datatypes <- (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 (Maybe (TyName, CompT AbstractTy)
 -> TyName
 -> DatatypeInfo AbstractTy
 -> Maybe (TyName, CompT AbstractTy))
-> Maybe (TyName, CompT AbstractTy)
-> Map TyName (DatatypeInfo AbstractTy)
-> Maybe (TyName, CompT AbstractTy)
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' (TyName
-> Maybe (TyName, CompT AbstractTy)
-> TyName
-> DatatypeInfo AbstractTy
-> Maybe (TyName, CompT AbstractTy)
go TyName
bfTyName) Maybe (TyName, CompT AbstractTy)
forall a. Maybe a
Nothing Map TyName (DatatypeInfo AbstractTy)
datatypes of
                    Just (TyName
k, CompT AbstractTy
bbf) -> case Vector (ValT AbstractTy)
tyVarInsts of
                      Vector (ValT AbstractTy)
NilV -> CataInfo -> m CataInfo
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CataInfo -> m CataInfo)
-> (CompT AbstractTy -> CataInfo) -> CompT AbstractTy -> m CataInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> CompT AbstractTy -> CataInfo
RigidCata TyName
k (CompT AbstractTy -> m CataInfo) -> CompT AbstractTy -> m CataInfo
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
bbf
                      ConsV ValT AbstractTy
_ Vector (ValT AbstractTy)
_ -> CataInfo -> m CataInfo
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CataInfo -> m CataInfo)
-> (CompT AbstractTy -> CataInfo) -> CompT AbstractTy -> m CataInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> ValT AbstractTy -> CataInfo
NonRigidCata TyName
k (ValT AbstractTy -> CataInfo)
-> (CompT AbstractTy -> ValT AbstractTy)
-> CompT AbstractTy
-> CataInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (CompT AbstractTy -> m CataInfo) -> CompT AbstractTy -> m CataInfo
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
bbf
                    Maybe (TyName, CompT AbstractTy)
Nothing -> CovenantTypeError -> m CataInfo
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m CataInfo)
-> (TyName -> CovenantTypeError) -> TyName -> m CataInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> CovenantTypeError
CataNoTypeForBaseFunctor (TyName -> m CataInfo) -> TyName -> m CataInfo
forall a b. (a -> b) -> a -> b
$ TyName
bfTyName
          Maybe (Vector (ValT AbstractTy), ValT AbstractTy)
_ -> CovenantTypeError -> m CataInfo
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m CataInfo)
-> (TyName -> CovenantTypeError) -> TyName -> m CataInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> CovenantTypeError
CataMonomorphicBaseFunctor (TyName -> m CataInfo) -> TyName -> m CataInfo
forall a b. (a -> b) -> a -> b
$ TyName
bfTyName
      ValT AbstractTy
_ -> CovenantTypeError -> m (ValT AbstractTy, CataInfo)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy, CataInfo))
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m (ValT AbstractTy, CataInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
CataNotADatatypeBaseFunctor (ValT AbstractTy -> m (ValT AbstractTy, CataInfo))
-> ValT AbstractTy -> m (ValT AbstractTy, CataInfo)
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
inputT
  CompT AbstractTy
_ -> CovenantTypeError -> m (ValT AbstractTy, CataInfo)
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m (ValT AbstractTy, CataInfo))
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m (ValT AbstractTy, CataInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
CataNonRigidAlgebra (CompT AbstractTy -> m (ValT AbstractTy, CataInfo))
-> CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t
  where
    go ::
      TyName ->
      Maybe (TyName, CompT AbstractTy) ->
      TyName ->
      DatatypeInfo AbstractTy ->
      Maybe (TyName, CompT AbstractTy)
    go :: TyName
-> Maybe (TyName, CompT AbstractTy)
-> TyName
-> DatatypeInfo AbstractTy
-> Maybe (TyName, CompT AbstractTy)
go TyName
targetTyName Maybe (TyName, CompT AbstractTy)
acc TyName
currTyName DatatypeInfo AbstractTy
currTyInfo = case Maybe (TyName, CompT AbstractTy)
acc of
      Maybe (TyName, CompT AbstractTy)
Nothing -> case Optic
  A_Lens
  NoIx
  (DatatypeInfo AbstractTy)
  (DatatypeInfo AbstractTy)
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
-> 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
  (DatatypeInfo AbstractTy)
  (DatatypeInfo AbstractTy)
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
  (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
#baseFunctor DatatypeInfo AbstractTy
currTyInfo of
        Just (DataDeclaration TyName
name Count "tyvar"
_ Vector (Constructor AbstractTy)
_ DataEncoding
_, ValT AbstractTy
_) ->
          if TyName
name TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
targetTyName
            then case Optic
  A_Lens
  NoIx
  (DatatypeInfo AbstractTy)
  (DatatypeInfo AbstractTy)
  (Maybe (ValT AbstractTy))
  (Maybe (ValT AbstractTy))
-> DatatypeInfo AbstractTy -> Maybe (ValT AbstractTy)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic
  A_Lens
  NoIx
  (DatatypeInfo AbstractTy)
  (DatatypeInfo AbstractTy)
  (Maybe (ValT AbstractTy))
  (Maybe (ValT AbstractTy))
#bbForm DatatypeInfo AbstractTy
currTyInfo of
              Just (ThunkT CompT AbstractTy
bbfTy) -> (TyName, CompT AbstractTy) -> Maybe (TyName, CompT AbstractTy)
forall a. a -> Maybe a
Just (TyName
currTyName, CompT AbstractTy
bbfTy)
              Maybe (ValT AbstractTy)
_ -> Maybe (TyName, CompT AbstractTy)
acc -- technically impossible
            else Maybe (TyName, CompT AbstractTy)
acc
        Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
_ -> Maybe (TyName, CompT AbstractTy)
acc
      Maybe (TyName, CompT AbstractTy)
_ -> Maybe (TyName, CompT AbstractTy)
acc
    -- Note (Koz, 11/11/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 r (Maybe r) -> !Maybe r>` as our
    -- stated algebra type, with `r` rigid. Suppose also that the value to be torn
    -- down is `List r`. If we assume the rigid `r` is bound one scope away, `r`'s
    -- DeBruijn index will be different for each of these:
    --
    -- \* In the stated algebra type, `r`'s index will be `S (S Z)`; but
    -- \* In the value to be torn down, `r`'s index will be `S Z`.
    --
    -- As part of what we do here, we 'collect' the expected result of the
    -- catamorphism according to the stated algebra type. Then, we use a
    -- combination of the value to be torn down (or more precisely, its
    -- Boehm-Berrarducci form), together with the handlers, as arguments to the
    -- unifier to see what result we get on that basis. In theory, if the expected
    -- result type and the result of this unification agree, we type check.
    -- However, this would fail in our case: as the stated algebra type is
    -- `Comp0 $ Datatype "#List" [tyvar (S (S Z)) ix0, ...`, the expected result
    -- type would be `Datatype "Maybe" [tyvar (S (S Z) ix0]`. However, this is not
    -- valid in the scope of the value to be torn down: that same rigid would have
    -- the DeBruijn index `S Z` in that scope instead. This applies regardless of
    -- whether the tyvar is part of a datatype or not. This gives us an 'off by
    -- one' error.
    --
    -- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn
    -- index by one for our process. This is, in fact, _why_ stated algebra
    -- types must be rigid: if they weren't, this process would become far more
    -- complicated, as we would now have to be careful to establish _which_
    -- tyvars need 'stepping down' and which don't!
    stepDown :: ValT AbstractTy -> ValT AbstractTy
    stepDown :: ValT AbstractTy -> ValT AbstractTy
stepDown = \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
stepDown (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

fixArgType :: DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType :: DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType DeBruijn
distance = \case
  Abstraction AbstractTy
tyVar ->
    let tyVar' :: AbstractTy
tyVar' = DeBruijn -> AbstractTy -> AbstractTy
addDeBruijn DeBruijn
distance AbstractTy
tyVar
     in AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction AbstractTy
tyVar'
  ThunkT (CompN Count "tyvar"
cnt (ArgsAndResult Vector (ValT AbstractTy)
args ValT AbstractTy
res)) ->
    let args' :: Vector (ValT AbstractTy)
args' = (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 (DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType DeBruijn
distance) Vector (ValT AbstractTy)
args
        res' :: ValT AbstractTy
res' = DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType DeBruijn
distance ValT AbstractTy
res
     in CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT (Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompN Count "tyvar"
cnt (Vector (ValT AbstractTy) -> ValT AbstractTy -> CompTBody AbstractTy
forall a. Vector (ValT a) -> ValT a -> CompTBody a
ArgsAndResult Vector (ValT AbstractTy)
args' ValT AbstractTy
res'))
  bi :: ValT AbstractTy
bi@(BuiltinFlat {}) -> ValT AbstractTy
bi
  Datatype TyName
tn Vector (ValT AbstractTy)
dtArgs -> TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a b. (a -> b) -> a -> b
$ (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 (DeBruijn -> ValT AbstractTy -> ValT AbstractTy
fixArgType DeBruijn
distance) Vector (ValT AbstractTy)
dtArgs
  where
    addDeBruijn :: DeBruijn -> AbstractTy -> AbstractTy
    addDeBruijn :: DeBruijn -> AbstractTy -> AbstractTy
addDeBruijn DeBruijn
toAdd (BoundAt DeBruijn
db Index "tyvar"
indx) =
      let db' :: DeBruijn
db' = Maybe DeBruijn -> DeBruijn
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DeBruijn -> DeBruijn)
-> (Int -> Maybe DeBruijn) -> Int -> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Prism NoIx Int DeBruijn -> Int -> Maybe DeBruijn
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int DeBruijn
asInt (Int -> DeBruijn) -> Int -> DeBruijn
forall a b. (a -> b) -> a -> b
$ 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
toAdd Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 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
db
       in DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db' Index "tyvar"
indx