module Covenant.Internal.Term
  ( CovenantTypeError (..),
    Id (..),
    typeId,
    Arg (..),
    typeArg,
    Ref (..),
    typeRef,
    CompNodeInfo (..),
    ValNodeInfo (..),
    ASGNode (..),
    typeASGNode,
    ASGNodeType (..),
    BoundTyVar (..),
  )
where

import Control.Monad.Except (MonadError (throwError))
import Control.Monad.HashCons (MonadHashCons (lookupRef))
import Covenant.Constant (AConstant)
import Covenant.DeBruijn (DeBruijn)
import Covenant.Index (Index)
import Covenant.Internal.KindCheck (EncodingArgErr)
import Covenant.Internal.Rename (RenameError, UnRenameError)
import Covenant.Internal.Type
  ( AbstractTy,
    BuiltinFlatT,
    CompT,
    TyName,
    ValT,
  )
import Covenant.Internal.Unification (TypeAppError)
import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc)
import Covenant.Type (ConstructorName, PlutusDataConstructor, Renamed)
import Data.Kind (Type)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Vector (Vector)
import Data.Void (Void)
import Data.Wedge (Wedge)
import Data.Word (Word64)

-- | An error that can arise during the construction of an ASG by programmatic
-- means.
--
-- @since 1.0.0
data CovenantTypeError
  = -- | An 'Id' has no corresponding node. This error should not arise under
    -- normal circumstances: the most likely explanation is that you're using an
    -- 'Id' that was made by a different ASG builder computation.
    --
    -- @since 1.0.0
    BrokenIdReference Id
  | -- | Computation-typed nodes can't be forced, but we tried anyway.
    --
    -- @since 1.0.0
    ForceCompType (CompT AbstractTy)
  | -- | Value-typed nodes that aren't thunks can't be forced, but we tried anyway.
    --
    -- @since 1.0.0
    ForceNonThunk (ValT AbstractTy)
  | -- | Error nodes can't be forced, but we tried anyway.
    --
    -- @since 1.0.0
    ForceError
  | -- | Value-typed nodes can't be thunked, but we tried anyway.
    --
    -- @since 1.0.0
    ThunkValType (ValT AbstractTy)
  | -- | Error nodes can't be thunked, but we tried anyway.
    --
    -- @since 1.0.0
    ThunkError
  | -- | Arguments can't be applied to a value-typed node, but we tried anyway.
    --
    -- @since 1.0.0
    ApplyToValType (ValT AbstractTy)
  | -- | Arguments can't be applied to error nodes, but we tried anyway.
    --
    -- @since 1.0.0
    ApplyToError
  | -- | Computation-typed nodes can't be applied as arguments, but we tried anyway.
    --
    -- @since 1.0.0
    ApplyCompType (CompT AbstractTy)
  | -- | Renaming the function in an application failed.
    --
    -- @since 1.0.0
    RenameFunctionFailed (CompT AbstractTy) RenameError
  | -- | Renaming an argument in an application failed.
    --
    -- @since 1.0.0
    RenameArgumentFailed (ValT AbstractTy) RenameError
  | -- | We failed to unify an expected argument type with the type of the
    -- argument we were actually given.
    --
    -- @since 1.0.0
    UnificationError TypeAppError
  | -- | An argument was requested that doesn't exist.
    --
    -- @since 1.0.0
    NoSuchArgument DeBruijn (Index "arg")
  | -- | Can't return a computation-typed node, but we tried anyway.
    --
    -- @since 1.0.0
    ReturnCompType (CompT AbstractTy)
  | -- | The body of a lambda results in a value-typed node, which isn't allowed.
    --
    -- @since 1.2.0
    LambdaResultsInCompType (CompT AbstractTy)
  | -- | The body of a lambda results in a computation-typed node which isn't
    -- a return, which isn't allowed.
    --
    -- @since 1.0.0
    LambdaResultsInNonReturn (CompT AbstractTy)
  | -- | A lambda body's return is wrapping an error, instead of being directly
    -- an error. This should not happen under normal circumstances and is most
    -- certainly a bug.
    --
    -- @since 1.0.0
    ReturnWrapsError
  | -- | We tried to return a computation-typed node, but this isn't allowed.
    --
    -- @since 1.0.0
    ReturnWrapsCompType (CompT AbstractTy)
  | -- | The result of an application is not what the computation being
    -- applied expected.
    --
    -- First field is the expected type, the second is what we actually got.
    --
    -- @since 1.0.0
    WrongReturnType (ValT AbstractTy) (ValT AbstractTy)
  | -- | Wraps an encoding argument mismatch error from KindCheck
    --
    -- @since 1.1.0
    EncodingError (EncodingArgErr AbstractTy)
  | -- | The first argument to a catamorphism wasn't an algebra, as
    -- it had the wrong arity.
    --
    -- @since 1.2.0
    CataAlgebraWrongArity Int
  | -- | The first argument to a catamorphism wasn't an algebra.
    --
    -- @since 1.1.0
    CataNotAnAlgebra ASGNodeType
  | -- | The second argument to a catamorphism wasn't a value type.
    --
    -- @since 1.1.0
    CataApplyToNonValT ASGNodeType
  | -- The algebra given to this catamorphism is not rigid (that is, its
    -- computation type binds variables).
    --
    -- @since 1.2.0
    CataNonRigidAlgebra (CompT AbstractTy)
  | -- | The second argument to a catamorphism is a builtin type, but not one
    -- we can eliminate with a catamorphism.
    --
    -- @since 1.1.0
    CataWrongBuiltinType BuiltinFlatT
  | -- | The second argument to a catamorphism is a value type, but not one we
    -- can eliminate with a catamorphism. Usually, this means it's a variable.
    --
    -- @since 1.1.0
    CataWrongValT (ValT AbstractTy)
  | -- | We requested a catamorphism for a type that doesn't exist.
    --
    -- @since 1.2.0
    CataNoSuchType TyName
  | -- | We requested a catamorphism for a type without a base functor.
    --
    -- @since 1.2.0
    CataNoBaseFunctorForType TyName
  | -- | The provided algebra is not suitable for the given type.
    --
    -- @since 1.1.0
    CataUnsuitable (CompT AbstractTy) (ValT AbstractTy)
  | -- | Someone attempted to construct a tyvar using a DB index or argument position
    --   which refers to a scope (or argument) that does not exist.
    --
    -- @since 1.2.0
    OutOfScopeTyVar DeBruijn (Index "tyvar")
  | -- | We failed to rename an "instantiation type" supplied to 'Covenant.ASG.app'.
    --
    -- @since 1.2.0
    FailedToRenameInstantiation RenameError
  | -- | Un-renaming failed.
    --
    -- @since 1.2.0
    UndoRenameFailure UnRenameError
  | -- | We tried to look up the 'DatatypeInfo' corresponding to a 'TyName' and came up empty handed.
    --
    -- @since 1.2.0
    TypeDoesNotExist TyName
  | -- | We tried to rename a 'DatatypeInfo' and failed.
    --
    -- @since 1.2.0
    DatatypeInfoRenameError RenameError
  | -- | We tried to look up a constructor for a given type. The type exists, but the constructor does not.
    --
    -- @since 1.2.0
    ConstructorDoesNotExistForType TyName ConstructorName
  | -- | When using the helper function to construct an introduction form, the type and constructor exist but the
    --   number of fields provided as an argument does not match the number of declared fields.
    --   The 'Int' is the /incorrect/ number of /supplied/ fields.
    --
    -- @since 1.2.0
    IntroFormWrongNumArgs TyName ConstructorName Int
  | -- | The user passed an error node as an argument to a datatype into form. We return the arguments given
    --   to 'Covenant.ASG.dataConstructor' in the error.
    --
    -- @since 1.2.0
    IntroFormErrorNodeField TyName ConstructorName (Vector Ref)
  | -- | The user tried to construct an introduction form using a Plutus @Data@ constructor not found in the
    --   opaque datatype declaration.
    --
    -- @since 1.2.0
    UndeclaredOpaquePlutusDataCtor (Set.Set PlutusDataConstructor) ConstructorName
  | -- | The user tried to construct an introduction form with a valid Plutus @Data@ constructor, but
    --   supplied a 'Covenant.ASG.Ref' to a field of the wrong type.
    --
    -- @since 1.2.0
    InvalidOpaqueField (Set.Set PlutusDataConstructor) ConstructorName [ValT Renamed]
  | -- The user tried to match on (i.e. use as a scrutinee) a node that wasn't a value.
    --
    -- @since 1.2.0
    MatchNonValTy ASGNodeType
  | -- | Internal error: we found a base functor Boehm-Berrarducci form that isn't a thunk after instantiation
    --   during pattern matching.Somehow we got a BFBB that is something other than a thunk after instantiation during pattern matching.
    --
    --   This should not normally happen: let us know if you see this error!
    --
    -- @since 1.2.0
    MatchNonThunkBBF (ValT Renamed)
  | -- | We encountered a rename error during pattern matching. This will refer
    -- to either the Boehm-Berrarducci form, or the base functor Boehm-Berrarducci form, depending on what type we tried to match.
    --
    -- @since 1.2.0
    MatchRenameBBFail RenameError
  | -- | This indicates that we encountered an error when renaming the arguments to the type constructor of the
    --   /scrutinee type/ during pattern matching. That is, if we're matching on @Either a b@, this means that
    --   either @a@ or @b@ failed to rename.
    --
    --  This should not normally happen: let us know if you see this error!
    --
    -- @since 1.2.0
    MatchRenameTyConArgFail RenameError
  | -- | A user tried to use a polymorphic handler in a pattern match, which is not currently allowed.
    --
    -- @since 1.2.0
    MatchPolymorphicHandler (ValT Renamed)
  | -- | We tried to use an error node as a pattern match handler.
    --
    -- @since 1.2.0
    MatchErrorAsHandler Ref
  | -- | The non-recursive branch of a pattern match needs a Boehm-Berrarducci form for the given type
    -- name, but it doesn't exist.
    --
    -- @since 1.2.0
    MatchNoBBForm TyName
  | -- | Someone tried to match on something that isn't a datatype.
    --
    -- @since 1.2.0
    MatchNonDatatypeScrutinee (ValT AbstractTy)
  | -- | The scrutinee is a datatype, be don't have it in our datatype dictionary.
    --
    -- @since 1.2.0
    MatchNoDatatypeInfo TyName
  | -- | We tried to get the base functor for a type in the ASG context, but the base functor does not exist.
    --   This can occur either because the type is not recursive and has no base functor, or because the type
    --   itself does not exist. It does not seem important to distinguish between the two failure cases.
    --
    -- @since 1.3.0
    BaseFunctorDoesNotExistFor TyName
  | -- | 'app' was called with a number of instantiation arguments that does not match the number of
    -- type variables bound in Count the CompT of the function to which arguments are being applied.
    -- The first Int is the  number of bound tyvars in the function type, the second is the number of
    -- instantiations supplied.
    --
    -- @since 1.3.0
    WrongNumInstantiationsInApp (CompT Renamed) Int Int
  | -- | A miscellaneous error, needed to catch various things that can go wrong during datatype preparation and
    -- deserialization.
    --
    -- @since 1.3.0
    OtherError Text
  deriving stock
    ( -- | @since 1.0.0
      CovenantTypeError -> CovenantTypeError -> Bool
(CovenantTypeError -> CovenantTypeError -> Bool)
-> (CovenantTypeError -> CovenantTypeError -> Bool)
-> Eq CovenantTypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CovenantTypeError -> CovenantTypeError -> Bool
== :: CovenantTypeError -> CovenantTypeError -> Bool
$c/= :: CovenantTypeError -> CovenantTypeError -> Bool
/= :: CovenantTypeError -> CovenantTypeError -> Bool
Eq,
      -- | @since 1.0.0
      Int -> CovenantTypeError -> ShowS
[CovenantTypeError] -> ShowS
CovenantTypeError -> String
(Int -> CovenantTypeError -> ShowS)
-> (CovenantTypeError -> String)
-> ([CovenantTypeError] -> ShowS)
-> Show CovenantTypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CovenantTypeError -> ShowS
showsPrec :: Int -> CovenantTypeError -> ShowS
$cshow :: CovenantTypeError -> String
show :: CovenantTypeError -> String
$cshowList :: [CovenantTypeError] -> ShowS
showList :: [CovenantTypeError] -> ShowS
Show
    )

-- | A unique identifier for a node in a Covenant program.
--
-- @since 1.0.0
newtype Id = Id Word64
  deriving
    ( -- | @since 1.0.0
      Id -> Id -> Bool
(Id -> Id -> Bool) -> (Id -> Id -> Bool) -> Eq Id
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Id -> Id -> Bool
== :: Id -> Id -> Bool
$c/= :: Id -> Id -> Bool
/= :: Id -> Id -> Bool
Eq,
      -- | @since 1.0.0
      Eq Id
Eq Id =>
(Id -> Id -> Ordering)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> Ord Id
Id -> Id -> Bool
Id -> Id -> Ordering
Id -> Id -> Id
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Id -> Id -> Ordering
compare :: Id -> Id -> Ordering
$c< :: Id -> Id -> Bool
< :: Id -> Id -> Bool
$c<= :: Id -> Id -> Bool
<= :: Id -> Id -> Bool
$c> :: Id -> Id -> Bool
> :: Id -> Id -> Bool
$c>= :: Id -> Id -> Bool
>= :: Id -> Id -> Bool
$cmax :: Id -> Id -> Id
max :: Id -> Id -> Id
$cmin :: Id -> Id -> Id
min :: Id -> Id -> Id
Ord,
      -- | @since 1.0.0
      Id
Id -> Id -> Bounded Id
forall a. a -> a -> Bounded a
$cminBound :: Id
minBound :: Id
$cmaxBound :: Id
maxBound :: Id
Bounded,
      -- | Needed for internal reasons, even though this type class is terrible.
      --
      -- @since 1.0.0
      Int -> Id
Id -> Int
Id -> [Id]
Id -> Id
Id -> Id -> [Id]
Id -> Id -> Id -> [Id]
(Id -> Id)
-> (Id -> Id)
-> (Int -> Id)
-> (Id -> Int)
-> (Id -> [Id])
-> (Id -> Id -> [Id])
-> (Id -> Id -> [Id])
-> (Id -> Id -> Id -> [Id])
-> Enum Id
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Id -> Id
succ :: Id -> Id
$cpred :: Id -> Id
pred :: Id -> Id
$ctoEnum :: Int -> Id
toEnum :: Int -> Id
$cfromEnum :: Id -> Int
fromEnum :: Id -> Int
$cenumFrom :: Id -> [Id]
enumFrom :: Id -> [Id]
$cenumFromThen :: Id -> Id -> [Id]
enumFromThen :: Id -> Id -> [Id]
$cenumFromTo :: Id -> Id -> [Id]
enumFromTo :: Id -> Id -> [Id]
$cenumFromThenTo :: Id -> Id -> Id -> [Id]
enumFromThenTo :: Id -> Id -> Id -> [Id]
Enum
    )
    via Word64
  deriving stock
    ( -- | @since 1.0.0
      Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
(Int -> Id -> ShowS)
-> (Id -> String) -> ([Id] -> ShowS) -> Show Id
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Id -> ShowS
showsPrec :: Int -> Id -> ShowS
$cshow :: Id -> String
show :: Id -> String
$cshowList :: [Id] -> ShowS
showList :: [Id] -> ShowS
Show
    )

-- Get the type of an `Id`, or fail.
typeId ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Id ->
  m ASGNodeType
typeId :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
i = do
  Maybe ASGNode
lookedUp <- Id -> m (Maybe ASGNode)
forall r e (m :: Type -> Type).
MonadHashCons r e m =>
r -> m (Maybe e)
lookupRef Id
i
  case Maybe ASGNode
lookedUp of
    Maybe ASGNode
Nothing -> CovenantTypeError -> m ASGNodeType
forall a. CovenantTypeError -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (CovenantTypeError -> m ASGNodeType)
-> (Id -> CovenantTypeError) -> Id -> m ASGNodeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> CovenantTypeError
BrokenIdReference (Id -> m ASGNodeType) -> Id -> m ASGNodeType
forall a b. (a -> b) -> a -> b
$ Id
i
    Just ASGNode
node -> ASGNodeType -> m ASGNodeType
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ASGNodeType -> m ASGNodeType)
-> (ASGNode -> ASGNodeType) -> ASGNode -> m ASGNodeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASGNode -> ASGNodeType
typeASGNode (ASGNode -> m ASGNodeType) -> ASGNode -> m ASGNodeType
forall a b. (a -> b) -> a -> b
$ ASGNode
node

-- | An argument passed to a function in a Covenant program.
--
-- @since 1.0.0
data Arg = Arg DeBruijn (Index "arg") (ValT AbstractTy)
  deriving stock
    ( -- | @since 1.0.0
      Arg -> Arg -> Bool
(Arg -> Arg -> Bool) -> (Arg -> Arg -> Bool) -> Eq Arg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Arg -> Arg -> Bool
== :: Arg -> Arg -> Bool
$c/= :: Arg -> Arg -> Bool
/= :: Arg -> Arg -> Bool
Eq,
      -- | @since 1.0.0
      Eq Arg
Eq Arg =>
(Arg -> Arg -> Ordering)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Bool)
-> (Arg -> Arg -> Arg)
-> (Arg -> Arg -> Arg)
-> Ord Arg
Arg -> Arg -> Bool
Arg -> Arg -> Ordering
Arg -> Arg -> Arg
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Arg -> Arg -> Ordering
compare :: Arg -> Arg -> Ordering
$c< :: Arg -> Arg -> Bool
< :: Arg -> Arg -> Bool
$c<= :: Arg -> Arg -> Bool
<= :: Arg -> Arg -> Bool
$c> :: Arg -> Arg -> Bool
> :: Arg -> Arg -> Bool
$c>= :: Arg -> Arg -> Bool
>= :: Arg -> Arg -> Bool
$cmax :: Arg -> Arg -> Arg
max :: Arg -> Arg -> Arg
$cmin :: Arg -> Arg -> Arg
min :: Arg -> Arg -> Arg
Ord,
      -- | @since 1.0.0
      Int -> Arg -> ShowS
[Arg] -> ShowS
Arg -> String
(Int -> Arg -> ShowS)
-> (Arg -> String) -> ([Arg] -> ShowS) -> Show Arg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Arg -> ShowS
showsPrec :: Int -> Arg -> ShowS
$cshow :: Arg -> String
show :: Arg -> String
$cshowList :: [Arg] -> ShowS
showList :: [Arg] -> ShowS
Show
    )

-- Helper to get the type of an argument.
typeArg :: Arg -> ValT AbstractTy
typeArg :: Arg -> ValT AbstractTy
typeArg (Arg DeBruijn
_ Index "arg"
_ ValT AbstractTy
t) = ValT AbstractTy
t

-- | A general reference in a Covenant program.
--
-- @since 1.0.0
data Ref
  = -- | A function argument.
    --
    -- @since 1.0.0
    AnArg Arg
  | -- | A link to an ASG node.
    --
    -- @since 1.0.0
    AnId Id
  deriving stock
    ( -- | @since 1.0.0
      Ref -> Ref -> Bool
(Ref -> Ref -> Bool) -> (Ref -> Ref -> Bool) -> Eq Ref
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ref -> Ref -> Bool
== :: Ref -> Ref -> Bool
$c/= :: Ref -> Ref -> Bool
/= :: Ref -> Ref -> Bool
Eq,
      -- | @since 1.0.0
      Eq Ref
Eq Ref =>
(Ref -> Ref -> Ordering)
-> (Ref -> Ref -> Bool)
-> (Ref -> Ref -> Bool)
-> (Ref -> Ref -> Bool)
-> (Ref -> Ref -> Bool)
-> (Ref -> Ref -> Ref)
-> (Ref -> Ref -> Ref)
-> Ord Ref
Ref -> Ref -> Bool
Ref -> Ref -> Ordering
Ref -> Ref -> Ref
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Ref -> Ref -> Ordering
compare :: Ref -> Ref -> Ordering
$c< :: Ref -> Ref -> Bool
< :: Ref -> Ref -> Bool
$c<= :: Ref -> Ref -> Bool
<= :: Ref -> Ref -> Bool
$c> :: Ref -> Ref -> Bool
> :: Ref -> Ref -> Bool
$c>= :: Ref -> Ref -> Bool
>= :: Ref -> Ref -> Bool
$cmax :: Ref -> Ref -> Ref
max :: Ref -> Ref -> Ref
$cmin :: Ref -> Ref -> Ref
min :: Ref -> Ref -> Ref
Ord,
      -- | @since 1.0.0
      Int -> Ref -> ShowS
[Ref] -> ShowS
Ref -> String
(Int -> Ref -> ShowS)
-> (Ref -> String) -> ([Ref] -> ShowS) -> Show Ref
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ref -> ShowS
showsPrec :: Int -> Ref -> ShowS
$cshow :: Ref -> String
show :: Ref -> String
$cshowList :: [Ref] -> ShowS
showList :: [Ref] -> ShowS
Show
    )

-- Helper for getting a type for any reference.
typeRef ::
  forall (m :: Type -> Type).
  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
  Ref ->
  m ASGNodeType
typeRef :: forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Ref -> m ASGNodeType
typeRef = \case
  AnArg Arg
arg -> ASGNodeType -> m ASGNodeType
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ASGNodeType -> m ASGNodeType)
-> (Arg -> ASGNodeType) -> Arg -> m ASGNodeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> ASGNodeType
ValNodeType (ValT AbstractTy -> ASGNodeType)
-> (Arg -> ValT AbstractTy) -> Arg -> ASGNodeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg -> ValT AbstractTy
typeArg (Arg -> m ASGNodeType) -> Arg -> m ASGNodeType
forall a b. (a -> b) -> a -> b
$ Arg
arg
  AnId Id
i -> Id -> m ASGNodeType
forall (m :: Type -> Type).
(MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
Id -> m ASGNodeType
typeId Id
i

-- | Computation-term-specific node information.
--
-- @since 1.0.0
data CompNodeInfo
  = Builtin1Internal OneArgFunc
  | Builtin2Internal TwoArgFunc
  | Builtin3Internal ThreeArgFunc
  | Builtin6Internal SixArgFunc
  | LamInternal Ref
  | ForceInternal Ref
  deriving stock
    ( -- | @since 1.0.0
      CompNodeInfo -> CompNodeInfo -> Bool
(CompNodeInfo -> CompNodeInfo -> Bool)
-> (CompNodeInfo -> CompNodeInfo -> Bool) -> Eq CompNodeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompNodeInfo -> CompNodeInfo -> Bool
== :: CompNodeInfo -> CompNodeInfo -> Bool
$c/= :: CompNodeInfo -> CompNodeInfo -> Bool
/= :: CompNodeInfo -> CompNodeInfo -> Bool
Eq,
      -- | @since 1.0.0
      Eq CompNodeInfo
Eq CompNodeInfo =>
(CompNodeInfo -> CompNodeInfo -> Ordering)
-> (CompNodeInfo -> CompNodeInfo -> Bool)
-> (CompNodeInfo -> CompNodeInfo -> Bool)
-> (CompNodeInfo -> CompNodeInfo -> Bool)
-> (CompNodeInfo -> CompNodeInfo -> Bool)
-> (CompNodeInfo -> CompNodeInfo -> CompNodeInfo)
-> (CompNodeInfo -> CompNodeInfo -> CompNodeInfo)
-> Ord CompNodeInfo
CompNodeInfo -> CompNodeInfo -> Bool
CompNodeInfo -> CompNodeInfo -> Ordering
CompNodeInfo -> CompNodeInfo -> CompNodeInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CompNodeInfo -> CompNodeInfo -> Ordering
compare :: CompNodeInfo -> CompNodeInfo -> Ordering
$c< :: CompNodeInfo -> CompNodeInfo -> Bool
< :: CompNodeInfo -> CompNodeInfo -> Bool
$c<= :: CompNodeInfo -> CompNodeInfo -> Bool
<= :: CompNodeInfo -> CompNodeInfo -> Bool
$c> :: CompNodeInfo -> CompNodeInfo -> Bool
> :: CompNodeInfo -> CompNodeInfo -> Bool
$c>= :: CompNodeInfo -> CompNodeInfo -> Bool
>= :: CompNodeInfo -> CompNodeInfo -> Bool
$cmax :: CompNodeInfo -> CompNodeInfo -> CompNodeInfo
max :: CompNodeInfo -> CompNodeInfo -> CompNodeInfo
$cmin :: CompNodeInfo -> CompNodeInfo -> CompNodeInfo
min :: CompNodeInfo -> CompNodeInfo -> CompNodeInfo
Ord,
      -- | @since 1.0.0
      Int -> CompNodeInfo -> ShowS
[CompNodeInfo] -> ShowS
CompNodeInfo -> String
(Int -> CompNodeInfo -> ShowS)
-> (CompNodeInfo -> String)
-> ([CompNodeInfo] -> ShowS)
-> Show CompNodeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompNodeInfo -> ShowS
showsPrec :: Int -> CompNodeInfo -> ShowS
$cshow :: CompNodeInfo -> String
show :: CompNodeInfo -> String
$cshowList :: [CompNodeInfo] -> ShowS
showList :: [CompNodeInfo] -> ShowS
Show
    )

-- | Value-term-specific node information.
--
-- @since 1.0.0
data ValNodeInfo
  = LitInternal AConstant
  | -- | @since 1.3.0
    AppInternal Id (Vector Ref) (Vector (Wedge BoundTyVar (ValT Void)))
  | ThunkInternal Id
  | -- | @since 1.1.0
    CataInternal Ref Ref
  | -- | @since 1.2.0
    DataConstructorInternal TyName ConstructorName (Vector Ref)
  | -- | @since 1.2.0
    MatchInternal Ref (Vector Ref)
  deriving stock
    ( -- | @since 1.0.0
      ValNodeInfo -> ValNodeInfo -> Bool
(ValNodeInfo -> ValNodeInfo -> Bool)
-> (ValNodeInfo -> ValNodeInfo -> Bool) -> Eq ValNodeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ValNodeInfo -> ValNodeInfo -> Bool
== :: ValNodeInfo -> ValNodeInfo -> Bool
$c/= :: ValNodeInfo -> ValNodeInfo -> Bool
/= :: ValNodeInfo -> ValNodeInfo -> Bool
Eq,
      -- | @since 1.0.0
      Eq ValNodeInfo
Eq ValNodeInfo =>
(ValNodeInfo -> ValNodeInfo -> Ordering)
-> (ValNodeInfo -> ValNodeInfo -> Bool)
-> (ValNodeInfo -> ValNodeInfo -> Bool)
-> (ValNodeInfo -> ValNodeInfo -> Bool)
-> (ValNodeInfo -> ValNodeInfo -> Bool)
-> (ValNodeInfo -> ValNodeInfo -> ValNodeInfo)
-> (ValNodeInfo -> ValNodeInfo -> ValNodeInfo)
-> Ord ValNodeInfo
ValNodeInfo -> ValNodeInfo -> Bool
ValNodeInfo -> ValNodeInfo -> Ordering
ValNodeInfo -> ValNodeInfo -> ValNodeInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ValNodeInfo -> ValNodeInfo -> Ordering
compare :: ValNodeInfo -> ValNodeInfo -> Ordering
$c< :: ValNodeInfo -> ValNodeInfo -> Bool
< :: ValNodeInfo -> ValNodeInfo -> Bool
$c<= :: ValNodeInfo -> ValNodeInfo -> Bool
<= :: ValNodeInfo -> ValNodeInfo -> Bool
$c> :: ValNodeInfo -> ValNodeInfo -> Bool
> :: ValNodeInfo -> ValNodeInfo -> Bool
$c>= :: ValNodeInfo -> ValNodeInfo -> Bool
>= :: ValNodeInfo -> ValNodeInfo -> Bool
$cmax :: ValNodeInfo -> ValNodeInfo -> ValNodeInfo
max :: ValNodeInfo -> ValNodeInfo -> ValNodeInfo
$cmin :: ValNodeInfo -> ValNodeInfo -> ValNodeInfo
min :: ValNodeInfo -> ValNodeInfo -> ValNodeInfo
Ord,
      -- | @since 1.0.0
      Int -> ValNodeInfo -> ShowS
[ValNodeInfo] -> ShowS
ValNodeInfo -> String
(Int -> ValNodeInfo -> ShowS)
-> (ValNodeInfo -> String)
-> ([ValNodeInfo] -> ShowS)
-> Show ValNodeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ValNodeInfo -> ShowS
showsPrec :: Int -> ValNodeInfo -> ShowS
$cshow :: ValNodeInfo -> String
show :: ValNodeInfo -> String
$cshowList :: [ValNodeInfo] -> ShowS
showList :: [ValNodeInfo] -> ShowS
Show
    )

-- | A single node in a Covenant ASG. Where appropriate, these carry their
-- types.
--
-- @since 1.0.0
data ASGNode
  = -- | A computation-typed node.
    --
    -- @since 1.0.0
    ACompNode (CompT AbstractTy) CompNodeInfo
  | -- | A value-typed node
    --
    -- @since 1.0.0
    AValNode (ValT AbstractTy) ValNodeInfo
  | -- | An error node.
    --
    -- @since 1.0.0
    AnError
  deriving stock
    ( -- | @since 1.0.0
      ASGNode -> ASGNode -> Bool
(ASGNode -> ASGNode -> Bool)
-> (ASGNode -> ASGNode -> Bool) -> Eq ASGNode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ASGNode -> ASGNode -> Bool
== :: ASGNode -> ASGNode -> Bool
$c/= :: ASGNode -> ASGNode -> Bool
/= :: ASGNode -> ASGNode -> Bool
Eq,
      -- | @since 1.0.0
      Eq ASGNode
Eq ASGNode =>
(ASGNode -> ASGNode -> Ordering)
-> (ASGNode -> ASGNode -> Bool)
-> (ASGNode -> ASGNode -> Bool)
-> (ASGNode -> ASGNode -> Bool)
-> (ASGNode -> ASGNode -> Bool)
-> (ASGNode -> ASGNode -> ASGNode)
-> (ASGNode -> ASGNode -> ASGNode)
-> Ord ASGNode
ASGNode -> ASGNode -> Bool
ASGNode -> ASGNode -> Ordering
ASGNode -> ASGNode -> ASGNode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ASGNode -> ASGNode -> Ordering
compare :: ASGNode -> ASGNode -> Ordering
$c< :: ASGNode -> ASGNode -> Bool
< :: ASGNode -> ASGNode -> Bool
$c<= :: ASGNode -> ASGNode -> Bool
<= :: ASGNode -> ASGNode -> Bool
$c> :: ASGNode -> ASGNode -> Bool
> :: ASGNode -> ASGNode -> Bool
$c>= :: ASGNode -> ASGNode -> Bool
>= :: ASGNode -> ASGNode -> Bool
$cmax :: ASGNode -> ASGNode -> ASGNode
max :: ASGNode -> ASGNode -> ASGNode
$cmin :: ASGNode -> ASGNode -> ASGNode
min :: ASGNode -> ASGNode -> ASGNode
Ord,
      -- | @since 1.0.0
      Int -> ASGNode -> ShowS
[ASGNode] -> ShowS
ASGNode -> String
(Int -> ASGNode -> ShowS)
-> (ASGNode -> String) -> ([ASGNode] -> ShowS) -> Show ASGNode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ASGNode -> ShowS
showsPrec :: Int -> ASGNode -> ShowS
$cshow :: ASGNode -> String
show :: ASGNode -> String
$cshowList :: [ASGNode] -> ShowS
showList :: [ASGNode] -> ShowS
Show
    )

-- | Produces the type of any ASG node.
--
-- @since 1.0.0
typeASGNode :: ASGNode -> ASGNodeType
typeASGNode :: ASGNode -> ASGNodeType
typeASGNode = \case
  ACompNode CompT AbstractTy
t CompNodeInfo
_ -> CompT AbstractTy -> ASGNodeType
CompNodeType CompT AbstractTy
t
  AValNode ValT AbstractTy
t ValNodeInfo
_ -> ValT AbstractTy -> ASGNodeType
ValNodeType ValT AbstractTy
t
  ASGNode
AnError -> ASGNodeType
ErrorNodeType

-- | Helper data type representing the type of any ASG node whatsoever.
--
-- @since 1.0.0
data ASGNodeType
  = CompNodeType (CompT AbstractTy)
  | ValNodeType (ValT AbstractTy)
  | ErrorNodeType
  deriving stock
    ( -- | @since 1.0.0
      ASGNodeType -> ASGNodeType -> Bool
(ASGNodeType -> ASGNodeType -> Bool)
-> (ASGNodeType -> ASGNodeType -> Bool) -> Eq ASGNodeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ASGNodeType -> ASGNodeType -> Bool
== :: ASGNodeType -> ASGNodeType -> Bool
$c/= :: ASGNodeType -> ASGNodeType -> Bool
/= :: ASGNodeType -> ASGNodeType -> Bool
Eq,
      -- | @since 1.0.0
      Eq ASGNodeType
Eq ASGNodeType =>
(ASGNodeType -> ASGNodeType -> Ordering)
-> (ASGNodeType -> ASGNodeType -> Bool)
-> (ASGNodeType -> ASGNodeType -> Bool)
-> (ASGNodeType -> ASGNodeType -> Bool)
-> (ASGNodeType -> ASGNodeType -> Bool)
-> (ASGNodeType -> ASGNodeType -> ASGNodeType)
-> (ASGNodeType -> ASGNodeType -> ASGNodeType)
-> Ord ASGNodeType
ASGNodeType -> ASGNodeType -> Bool
ASGNodeType -> ASGNodeType -> Ordering
ASGNodeType -> ASGNodeType -> ASGNodeType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ASGNodeType -> ASGNodeType -> Ordering
compare :: ASGNodeType -> ASGNodeType -> Ordering
$c< :: ASGNodeType -> ASGNodeType -> Bool
< :: ASGNodeType -> ASGNodeType -> Bool
$c<= :: ASGNodeType -> ASGNodeType -> Bool
<= :: ASGNodeType -> ASGNodeType -> Bool
$c> :: ASGNodeType -> ASGNodeType -> Bool
> :: ASGNodeType -> ASGNodeType -> Bool
$c>= :: ASGNodeType -> ASGNodeType -> Bool
>= :: ASGNodeType -> ASGNodeType -> Bool
$cmax :: ASGNodeType -> ASGNodeType -> ASGNodeType
max :: ASGNodeType -> ASGNodeType -> ASGNodeType
$cmin :: ASGNodeType -> ASGNodeType -> ASGNodeType
min :: ASGNodeType -> ASGNodeType -> ASGNodeType
Ord,
      -- | @since 1.0.0
      Int -> ASGNodeType -> ShowS
[ASGNodeType] -> ShowS
ASGNodeType -> String
(Int -> ASGNodeType -> ShowS)
-> (ASGNodeType -> String)
-> ([ASGNodeType] -> ShowS)
-> Show ASGNodeType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ASGNodeType -> ShowS
showsPrec :: Int -> ASGNodeType -> ShowS
$cshow :: ASGNodeType -> String
show :: ASGNodeType -> String
$cshowList :: [ASGNodeType] -> ShowS
showList :: [ASGNodeType] -> ShowS
Show
    )

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