{-# LANGUAGE PatternSynonyms #-}

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

    -- ** Types
    ASG,

    -- ** Functions
    topLevelNode,
    nodeAt,

    -- * ASG components

    -- ** Types
    Id,
    Ref (..),
    Arg,
    CompNodeInfo
      ( Builtin1,
        Builtin2,
        Builtin3,
        Lam,
        Force,
        Return
      ),
    ValNodeInfo (Lit, App, Thunk),
    ASGNode (..),

    -- ** Functions
    typeASGNode,

    -- * ASG builder

    -- ** Types
    CovenantError (..),
    ScopeInfo,
    ASGBuilder,
    CovenantTypeError
      ( BrokenIdReference,
        ForceCompType,
        ForceNonThunk,
        ForceError,
        ThunkValType,
        ThunkError,
        ApplyToValType,
        ApplyToError,
        ApplyCompType,
        RenameFunctionFailed,
        RenameArgumentFailed,
        NoSuchArgument,
        ReturnCompType,
        LambdaResultsInValType,
        LambdaResultsInNonReturn,
        ReturnWrapsError,
        ReturnWrapsCompType,
        WrongReturnType,
        UnificationError
      ),
    RenameError
      ( InvalidAbstractionReference,
        IrrelevantAbstraction,
        UndeterminedAbstraction
      ),

    -- ** Introducers
    arg,
    builtin1,
    builtin2,
    builtin3,
    force,
    ret,
    lam,
    err,
    lit,
    thunk,
    app,

    -- ** Elimination
    runASGBuilder,
  )
where

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.DeBruijn (DeBruijn, asInt)
import Covenant.Index (Index, count0, intIndex)
import Covenant.Internal.Rename
  ( RenameError
      ( InvalidAbstractionReference,
        IrrelevantAbstraction,
        UndeterminedAbstraction
      ),
    renameCompT,
    renameValT,
    runRenameM,
    undoRename,
  )
import Covenant.Internal.Term
  ( ASGNode (ACompNode, AValNode, AnError),
    ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType),
    Arg (Arg),
    CompNodeInfo
      ( Builtin1Internal,
        Builtin2Internal,
        Builtin3Internal,
        ForceInternal,
        LamInternal,
        ReturnInternal
      ),
    CovenantTypeError
      ( ApplyCompType,
        ApplyToError,
        ApplyToValType,
        BrokenIdReference,
        ForceCompType,
        ForceError,
        ForceNonThunk,
        LambdaResultsInNonReturn,
        LambdaResultsInValType,
        NoSuchArgument,
        RenameArgumentFailed,
        RenameFunctionFailed,
        ReturnCompType,
        ReturnWrapsCompType,
        ReturnWrapsError,
        ThunkError,
        ThunkValType,
        UnificationError,
        WrongReturnType
      ),
    Id,
    Ref (AnArg, AnId),
    ValNodeInfo (AppInternal, LitInternal, ThunkInternal),
    typeASGNode,
    typeId,
    typeRef,
  )
import Covenant.Internal.Type
  ( AbstractTy,
    CompT (CompT),
    CompTBody (CompTBody),
    Renamed,
    ValT (ThunkT),
  )
import Covenant.Internal.Unification (checkApp)
import Covenant.Prim
  ( OneArgFunc,
    ThreeArgFunc,
    TwoArgFunc,
    typeOneArgFunc,
    typeThreeArgFunc,
    typeTwoArgFunc,
  )
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.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (fromJust)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty qualified as NonEmpty
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    ix,
    lens,
    over,
    preview,
    review,
    (%),
  )

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

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

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

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

-- | 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.0.0
newtype ScopeInfo = ScopeInfo (Vector (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 -> String
(Int -> ScopeInfo -> ShowS)
-> (ScopeInfo -> String)
-> ([ScopeInfo] -> ShowS)
-> Show ScopeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeInfo -> ShowS
showsPrec :: Int -> ScopeInfo -> ShowS
$cshow :: ScopeInfo -> String
show :: ScopeInfo -> String
$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.0.0
instance
  (k ~ A_Lens, a ~ Vector (Vector (ValT AbstractTy)), b ~ Vector (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 (Vector (ValT AbstractTy)) -> ScopeInfo
ScopeInfo b
Vector (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

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

-- | Produce the result of a computation.
--
-- @since 1.0.0
pattern Return :: Ref -> CompNodeInfo
pattern $mReturn :: forall {r}. CompNodeInfo -> (Ref -> r) -> ((# #) -> r) -> r
Return r <- ReturnInternal r

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

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

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

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

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

{-# COMPLETE Lit, App, Thunk #-}

-- | 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 -> String
(Int -> CovenantError -> ShowS)
-> (CovenantError -> String)
-> ([CovenantError] -> ShowS)
-> Show CovenantError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CovenantError -> ShowS
showsPrec :: Int -> CovenantError -> ShowS
$cshow :: CovenantError -> String
show :: CovenantError -> String
$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 ScopeInfo (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.0.0
      MonadReader ScopeInfo,
      -- | @since 1.0.0
      MonadError CovenantTypeError,
      -- | @since 1.0.0
      MonadHashCons Id ASGNode
    )
    via ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))

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

-- | Given a scope and a positional argument index, construct that argument.
-- Will fail if that argument doesn't exist in the specified scope, or if the
-- specified scope doesn't exist.
--
-- @since 1.0.0
arg ::
  forall (m :: Type -> Type).
  (MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>
  DeBruijn ->
  Index "arg" ->
  m Arg
arg :: forall (m :: Type -> Type).
(MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>
DeBruijn -> Index "arg" -> m Arg
arg DeBruijn
scope Index "arg"
index = do
  let scopeAsInt :: Int
scopeAsInt = DeBruijn -> Int
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 <- (ScopeInfo -> 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 ScopeInfo (ValT AbstractTy)
-> ScopeInfo -> 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
  ScopeInfo
  ScopeInfo
  (Vector (Vector (ValT AbstractTy)))
  (Vector (Vector (ValT AbstractTy)))
#argumentInfo Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Vector (ValT AbstractTy)))
  (Vector (Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Vector (ValT AbstractTy))))
     NoIx
     (Vector (Vector (ValT AbstractTy)))
     (Vector (Vector (ValT AbstractTy)))
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (IxValue (Vector (Vector (ValT AbstractTy))))
-> Optic
     An_AffineTraversal
     NoIx
     ScopeInfo
     ScopeInfo
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (IxValue (Vector (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 (Vector (ValT AbstractTy)))
-> Optic
     (IxKind (Vector (Vector (ValT AbstractTy))))
     NoIx
     (Vector (Vector (ValT AbstractTy)))
     (Vector (Vector (ValT AbstractTy)))
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (IxValue (Vector (Vector (ValT AbstractTy))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (Vector (Vector (ValT AbstractTy)))
scopeAsInt Optic
  An_AffineTraversal
  NoIx
  ScopeInfo
  ScopeInfo
  (IxValue (Vector (Vector (ValT AbstractTy))))
  (IxValue (Vector (Vector (ValT AbstractTy))))
-> Optic
     (IxKind (IxValue (Vector (Vector (ValT AbstractTy)))))
     NoIx
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (ValT AbstractTy)
     (ValT AbstractTy)
-> Optic' An_AffineTraversal NoIx ScopeInfo (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 (IxValue (Vector (Vector (ValT AbstractTy))))
-> Optic'
     (IxKind (IxValue (Vector (Vector (ValT AbstractTy)))))
     NoIx
     (IxValue (Vector (Vector (ValT AbstractTy))))
     (IxValue (IxValue (Vector (Vector (ValT AbstractTy)))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (IxValue (Vector (Vector (ValT AbstractTy))))
indexAsInt))
  case Maybe (ValT AbstractTy)
lookedUp of
    Maybe (ValT AbstractTy)
Nothing -> CovenantTypeError -> m Arg
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Arg)
-> (Index "arg" -> CovenantTypeError) -> Index "arg" -> m Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "arg" -> CovenantTypeError
NoSuchArgument DeBruijn
scope (Index "arg" -> m Arg) -> Index "arg" -> m Arg
forall a b. (a -> b) -> a -> b
$ Index "arg"
index
    Just ValT AbstractTy
t -> Arg -> m Arg
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Arg -> m Arg)
-> (ValT AbstractTy -> Arg) -> ValT AbstractTy -> m Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "arg" -> ValT AbstractTy -> Arg
Arg DeBruijn
scope Index "arg"
index (ValT AbstractTy -> m Arg) -> ValT AbstractTy -> m Arg
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t

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

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

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

-- | 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 the result of a function body (either a value or an error), construct
-- the return for it. Will fail if that reference aims at a computation node.
--
-- @since 1.0.0
ret ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Ref ->
  m Id
ret :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m Id
ret 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 -> do
      let t' :: CompT AbstractTy
t' = Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count0 (CompTBody AbstractTy -> CompT AbstractTy)
-> (ValT AbstractTy -> CompTBody AbstractTy)
-> ValT AbstractTy
-> CompT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> (ValT AbstractTy -> NonEmptyVector (ValT AbstractTy))
-> ValT AbstractTy
-> CompTBody AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> NonEmptyVector (ValT AbstractTy)
forall a. a -> NonEmptyVector a
NonEmpty.singleton (ValT AbstractTy -> CompT AbstractTy)
-> ValT AbstractTy -> CompT AbstractTy
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t
      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
t' (CompNodeInfo -> ASGNode)
-> (Ref -> CompNodeInfo) -> Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref -> CompNodeInfo
ReturnInternal (Ref -> m Id) -> Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Ref
r
    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
ReturnCompType (CompT AbstractTy -> m Id) -> CompT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t
    ASGNodeType
ErrorNodeType -> m Id
forall (m :: Type -> Type). MonadHashCons Id ASGNode m => m Id
err

-- | 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 Id@.
--
-- @since 1.0.0
lam ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>
  CompT AbstractTy ->
  m Id ->
  m Id
lam :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m,
 MonadReader ScopeInfo m) =>
CompT AbstractTy -> m Id -> m Id
lam expectedT :: CompT AbstractTy
expectedT@(CompT Count "tyvar"
_ (CompTBody NonEmptyVector (ValT AbstractTy)
xs)) m Id
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
  Id
bodyId <- (ScopeInfo -> ScopeInfo) -> m Id -> m Id
forall a. (ScopeInfo -> ScopeInfo) -> m a -> m a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic
  A_Lens
  NoIx
  ScopeInfo
  ScopeInfo
  (Vector (Vector (ValT AbstractTy)))
  (Vector (Vector (ValT AbstractTy)))
-> (Vector (Vector (ValT AbstractTy))
    -> Vector (Vector (ValT AbstractTy)))
-> ScopeInfo
-> ScopeInfo
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
  ScopeInfo
  ScopeInfo
  (Vector (Vector (ValT AbstractTy)))
  (Vector (Vector (ValT AbstractTy)))
#argumentInfo (Vector (ValT AbstractTy)
-> Vector (Vector (ValT AbstractTy))
-> Vector (Vector (ValT AbstractTy))
forall a. a -> Vector a -> Vector a
Vector.cons Vector (ValT AbstractTy)
args)) m Id
bodyComp
  Maybe ASGNode
bodyNode <- Id -> m (Maybe ASGNode)
forall r e (m :: Type -> Type).
MonadHashCons r e m =>
r -> m (Maybe e)
lookupRef Id
bodyId
  case Maybe ASGNode
bodyNode of
    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
. Id -> CompNodeInfo
LamInternal (Id -> m Id) -> Id -> m Id
forall a b. (a -> b) -> a -> b
$ Id
bodyId
    Just (ACompNode CompT AbstractTy
t CompNodeInfo
specs) -> case CompNodeInfo
specs of
      ReturnInternal Ref
r -> do
        ASGNodeType
rT <- Ref -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef Ref
r
        case ASGNodeType
rT of
          -- Note (Koz, 17/04/2025): I am not 100% sure about this, but I can't
          -- see how anything else would make sense.
          ValNodeType ValT AbstractTy
actualT ->
            if ValT AbstractTy
resultT ValT AbstractTy -> ValT AbstractTy -> Bool
forall a. Eq a => a -> a -> Bool
== ValT AbstractTy
actualT
              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
. Id -> CompNodeInfo
LamInternal (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
actualT
          ASGNodeType
ErrorNodeType -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError CovenantTypeError
ReturnWrapsError -- Should be impossible
          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
ReturnWrapsCompType (CompT AbstractTy -> m Id) -> CompT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ 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)
-> (CompT AbstractTy -> CovenantTypeError)
-> CompT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> CovenantTypeError
LambdaResultsInNonReturn (CompT AbstractTy -> m Id) -> CompT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
t
    Just (AValNode ValT AbstractTy
t ValNodeInfo
_) -> 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
LambdaResultsInValType (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT 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

-- | Given an 'Id' referring to a computation, and a 'Vector' of 'Ref's to the
-- desired arguments, construct the application of the arguments to that
-- computation. 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
--
-- @since 1.0.0
app ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Id ->
  Vector Ref ->
  m Id
app :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> Vector Ref -> m Id
app Id
fId Vector Ref
argRefs = do
  ASGNodeType
lookedUp <- Id -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
fId
  case ASGNodeType
lookedUp of
    CompNodeType CompT AbstractTy
fT -> case RenameM (CompT Renamed) -> Either RenameError (CompT Renamed)
forall a. RenameM a -> Either RenameError a
runRenameM (RenameM (CompT Renamed) -> Either RenameError (CompT Renamed))
-> (CompT AbstractTy -> RenameM (CompT Renamed))
-> CompT AbstractTy
-> Either RenameError (CompT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT (CompT AbstractTy -> Either RenameError (CompT Renamed))
-> CompT AbstractTy -> Either RenameError (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ CompT AbstractTy
fT of
      Left RenameError
err' -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (RenameError -> CovenantTypeError) -> RenameError -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT AbstractTy -> RenameError -> CovenantTypeError
RenameFunctionFailed CompT AbstractTy
fT (RenameError -> m Id) -> RenameError -> m Id
forall a b. (a -> b) -> a -> b
$ RenameError
err'
      Right CompT Renamed
renamedFT -> do
        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) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Vector Ref
argRefs
        case CompT Renamed
-> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed)
checkApp CompT Renamed
renamedFT ([Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed))
-> (Vector (Maybe (ValT Renamed)) -> [Maybe (ValT Renamed)])
-> Vector (Maybe (ValT Renamed))
-> Either TypeAppError (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Maybe (ValT Renamed)) -> [Maybe (ValT Renamed)]
forall a. Vector a -> [a]
Vector.toList (Vector (Maybe (ValT Renamed))
 -> Either TypeAppError (ValT Renamed))
-> Vector (Maybe (ValT Renamed))
-> Either TypeAppError (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ Vector (Maybe (ValT Renamed))
renamedArgs of
          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'
          Right ValT Renamed
result -> do
            let restored :: ValT AbstractTy
restored = ValT Renamed -> ValT AbstractTy
undoRename ValT Renamed
result
            ASGNode -> m Id
forall r e (m :: Type -> Type). MonadHashCons r e m => e -> m r
refTo (ASGNode -> m Id) -> (Vector Ref -> ASGNode) -> Vector Ref -> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ValNodeInfo -> ASGNode
AValNode ValT AbstractTy
restored (ValNodeInfo -> ASGNode)
-> (Vector Ref -> ValNodeInfo) -> Vector Ref -> ASGNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Vector Ref -> ValNodeInfo
AppInternal Id
fId (Vector Ref -> m Id) -> Vector Ref -> m Id
forall a b. (a -> b) -> a -> b
$ Vector Ref
argRefs
    ValNodeType ValT AbstractTy
t -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m Id)
-> (ValT AbstractTy -> CovenantTypeError)
-> ValT AbstractTy
-> m Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> CovenantTypeError
ApplyToValType (ValT AbstractTy -> m Id) -> ValT AbstractTy -> m Id
forall a b. (a -> b) -> a -> b
$ ValT AbstractTy
t
    ASGNodeType
ErrorNodeType -> CovenantTypeError -> m Id
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError CovenantTypeError
ApplyToError

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

-- Helpers

renameArg ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Ref -> m (Maybe (ValT Renamed))
renameArg :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m (Maybe (ValT Renamed))
renameArg Ref
r =
  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 RenameM (ValT Renamed) -> Either RenameError (ValT Renamed)
forall a. RenameM a -> Either RenameError a
runRenameM (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