module Covenant.Internal.Term
  ( CovenantTypeError (..),
    Id (..),
    typeId,
    Arg (..),
    typeArg,
    Ref (..),
    typeRef,
    CompNodeInfo (..),
    ValNodeInfo (..),
    ASGNode (..),
    typeASGNode,
    ASGNodeType (..),
  )
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.Vector (Vector)
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
  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
  | AppInternal Id (Vector Ref)
  | 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
    )