Types.hs

-- | CHR Virtual Machine — type definitions.
--
-- This module defines the abstract VM that serves as the intermediate
-- representation for the CHR compiler. The VM is a small imperative
-- language with domain-specific instructions for CHR constraint store
-- operations, logical variables, term manipulation, and propagation
-- history management.
--
-- Architecture:
--
--   CHR source (Prolog-compatible syntax)
--     → CHR compiler (Haskell)
--       → VM program (this representation)
--         → Backend: JavaScript code + JS runtime
--         → Backend: Scheme code + Scheme runtime
--         → Backend: Haskell interpreter + Haskell runtime
--
-- Design principles:
--
--   1. The VM instruction set is the complete interface between the
--      compiler and the runtime. The compiler never emits calls to
--      runtime functions by name.
--
--   2. CallExpr is used exclusively for calling compiler-generated
--      procedures (occurrence procedures, activate, tell, etc.).
--
--   3. HostCall is used for calling host language functions (arithmetic,
--      user-written guards and body expressions, etc.).
--
--   4. Logical variables and algebraic terms are opaque values from the
--      VM's perspective. The runtime provides NewVar, Unify, Equal,
--      MakeTerm, MatchTerm, and GetArg as primitives.
--
--   5. Recursion optimizations (trampolining, explicit stack) are the
--      responsibility of each backend, not the VM.
--
--   6. Expressions are split by the kind of value they produce:
--      'ValExpr' produces an ordinary 'Value' (the unification domain),
--      'IdExpr' produces a constraint identifier, and 'BoolExpr'
--      produces a boolean. Constraint identifiers cannot flow into
--      unification or term construction; the operands of conditionals
--      and short-circuiting operators are statically booleans. The
--      bridge from 'ValExpr' to 'BoolExpr' is the explicit 'BFromVal'
--      constructor, which carries a runtime check at the boundary.
module YCHR.Internal.VM.Types
  ( -- * Program structure
    Program (..),
    Procedure (..),
    ProcKind (..),
    EvaluableKey (..),

    -- * Statements
    Stmt (..),

    -- * Expressions
    ValExpr (..),
    IdExpr (..),
    BoolExpr (..),
    CallArg (..),

    -- * Runtime call stack frames
    StackFrame (..),

    -- * Supporting types
    ConstraintType (..),
    RuleId (..),
    Literal (..),
    ArgIndex (..),
    Name (..),
    Label (..),
  )
where

import Data.String (IsString (..))
import Data.Text (Text)
import Data.Text qualified as T
import YCHR.Internal.Loc (SourceLoc)
import YCHR.Internal.Types (ConstraintType (..), RuleId (..))
import YCHR.Internal.Types qualified as Types

-- | A runtime call stack frame.
--
-- Emitted by the compiler at rule fire and function entry points.
-- The interpreter maintains a stack of these for error reporting.
data StackFrame = StackFrame
  { -- | Human-readable label (e.g. @"rule transitivity"@ or @"function factorial\/1"@).
    frameLabel :: Text,
    -- | Source file location.
    frameSourceLoc :: SourceLoc,
    -- | Pretty-printed source code (from the parsed expression).
    frameSourceCode :: Text
  }
  deriving (Show, Eq)

-- | A VM program is a collection of named procedures.
data Program = Program
  { -- | Number of distinct constraint types (for pre-allocating the store).
    numTypes :: !Int,
    -- | Source names of constraint types, indexed by the 'ConstraintType'
    -- integer. @typeNames !! i@ is the structured source name of the
    -- type with index @i@. Used by runtime introspection (e.g.
    -- @print_store@) and preserved across VM serialization.
    typeNames :: ![Types.Name],
    -- | Number of rules in the program.
    numRules :: !Int,
    -- | Display names of rules, indexed by the 'RuleId' integer.
    -- @ruleNames !! i@ is the source name (or synthetic @__rule_N@
    -- fallback for anonymous rules) of the rule with id @i@. Used
    -- by runtime introspection and preserved across VM serialization.
    ruleNames :: ![Text],
    -- | The procedures that make up the program.
    procedures :: [Procedure],
    -- | Dispatch table for the @is@ deep-evaluator. Maps a
    -- @(functor, arity)@ key (as found on a @VTerm@) to the
    -- mangled procedure name in 'procedures'. One entry per
    -- user-defined function (prelude host calls are handled by
    -- the runtime's host-call registry, which is bare-functor
    -- keyed). Used by the runtime to call into user-defined
    -- functions when @is@ walks a dereferenced compound term.
    evaluables :: ![(EvaluableKey, Name)]
  }
  deriving (Show, Eq)

-- | Dispatch key for the @is@ deep-evaluator. Parallel in structure
-- to 'YCHR.Internal.Types.Identifier', but carries the VM-encoded form of the
-- functor (the same text stored on @VTerm@ values), so dispatch is
-- a direct map lookup with no need to invert
-- 'YCHR.Internal.Compile.Names.encodeText'.
data EvaluableKey = EvaluableKey
  { functor :: !Name,
    arity :: !Int
  }
  deriving (Show, Eq, Ord)

-- | A named procedure with parameters and a body.
--
-- The compiler generates procedures for:
--   * @tell_c@: adding a constraint from host language or rule bodies
--   * @activate_c@: trying all occurrences for a constraint
--   * @occurrence_c_j@: checking one occurrence of a constraint
--   * @reactivate_dispatch@: dispatching reactivation by constraint type
--
-- Note: @reactivate_all@ (paper §5.1–5.2) is not generated.  YCHR
-- implements the /Selective Constraint Reactivation/ optimization
-- (paper §5.3, observer pattern): 'Store' registers constraints as
-- observers of their arguments, 'Unify' populates the reactivation
-- queue for affected constraints, and 'DrainReactivationQueue'
-- processes only those constraints.
data Procedure = Procedure
  { -- | Procedure name
    name :: Name,
    -- | Parameter names
    params :: [Name],
    -- | Body statements
    body :: [Stmt],
    -- | Structural classification of the procedure. The compiler sets
    -- this at the (single) construction site; the interpreter reads it
    -- to label trace events without re-parsing the mangled name.
    -- Backends that don't care about tracing simply ignore the field.
    procKind :: !ProcKind
  }
  deriving (Show, Eq)

-- | Structural classification of a generated 'Procedure'.
--
-- Used by the interpreter's tracer (`:trace` in the REPL) to label
-- events with their ωr role without parsing the procedure's mangled
-- name. Each constructor carries the source-level data the tracer
-- needs to render readable output.
--
-- Lifted lambdas use 'PKFunction' with a name beginning with
-- @__lambda_@; the trace formatter recognises the prefix and renders
-- them as @lambda#N@.
data ProcKind
  = -- | @tell_c@: entry point for adding a constraint.
    PKTell !ConstraintType
  | -- | @activate_c@: try all occurrences for a constraint.
    PKActivate !ConstraintType
  | -- | @occurrence_c_j@: the @j@-th occurrence of constraint @c@,
    -- belonging to the rule identified by 'RuleId'. The display name
    -- is carried alongside so the tracer can label events without a
    -- second lookup into 'Program.ruleNames'.
    PKOccurrence !ConstraintType !Int !RuleId !Text
  | -- | @reactivate_dispatch@: route a reactivated constraint to its
    -- @activate_c@.
    PKReactivateDispatch
  | -- | @call_N@: dispatcher for @'$call'/N@.
    PKCallDispatch !Int
  | -- | A user-defined function or lifted lambda. Carries the source
    -- qualified name and arity.
    PKFunction !Types.QualifiedName !Int
  deriving (Show, Eq)

-- | Statements (imperative, side-effecting).
data Stmt
  = -- General control flow

    -- | Bind a local variable to the result of a value expression.
    LetVal Name ValExpr
  | -- | Bind a local variable to the result of an id expression.
    LetId Name IdExpr
  | -- | Mutate an existing value-bound variable.
    AssignVal Name ValExpr
  | -- | Mutate an existing id-bound variable.
    AssignId Name IdExpr
  | -- | Conditional: condition, then-branch, else-branch.
    If BoolExpr [Stmt] [Stmt]
  | -- | Labeled loop over constraint store.
    --
    -- @Foreach label constraintType suspVar indexConditions body@
    --
    -- Iterates over all stored constraints of the given type that
    -- satisfy the index conditions. Each condition @(i, expr)@ requires
    -- that argument @i@ of the constraint is 'Equal' to @expr@.
    --
    -- The current constraint suspension is bound to @suspVar@ in each
    -- iteration; references it via 'IdVar' inside the body, and use
    -- 'FieldArg'/'FieldType' to access its fields.
    --
    -- The iterator must satisfy the robustness, correctness,
    -- completeness, and weak termination properties as specified
    -- in the CHR compilation literature.
    Foreach Label ConstraintType Name [(ArgIndex, ValExpr)] [Stmt]
  | -- | Jump to the next iteration of the labeled 'Foreach' loop.
    Continue Label
  | -- | Exit the labeled 'Foreach' loop.
    Break Label
  | -- | Return a value from the current procedure.
    Return ValExpr
  | -- | Evaluate a value expression for its side effects, discard the result.
    ExprStmt ValExpr
  | -- | Evaluate a boolean expression for its side effects, discard the result.
    BoolExprStmt BoolExpr
  | -- Constraint store operations

    -- | Add a constraint suspension to the constraint store.
    -- The argument is a constraint identifier (as returned
    -- by 'CreateConstraint'). This also registers the constraint
    -- as an observer of its arguments for reactivation purposes.
    Store IdExpr
  | -- | Remove a constraint from the constraint store and mark it
    -- as no longer alive.
    Kill IdExpr
  | -- Propagation history

    -- | Record that a rule has fired with the given combination
    -- of constraint identifiers, to prevent redundant re-firing
    -- of propagation rules.
    AddHistory RuleId [IdExpr]
  | -- Reactivation

    -- | Process all constraints pending reactivation.
    --
    -- @DrainReactivationQueue suspVar body@
    --
    -- Iterates over the reactivation queue (populated as a side
    -- effect of 'Unify'), binding each pending constraint suspension
    -- to @suspVar@ (referenced via 'IdVar') and executing @body@.
    -- The body typically dispatches to the appropriate @activate_c@
    -- procedure based on constraint type.
    DrainReactivationQueue Name [Stmt]
  | -- Call stack frames

    -- | Push a frame onto the runtime call stack.
    -- Emitted by the compiler at rule fire and function entry points.
    -- The interpreter automatically pops frames when a procedure
    -- returns (save\/restore around 'callProc').
    PushFrame StackFrame
  deriving (Show, Eq)

-- | Value-producing expressions: everything that evaluates to an
-- ordinary 'Value' from the unification domain.
data ValExpr
  = -- | Reference to a value-bound variable (local or parameter).
    Var Name
  | -- | A literal value.
    Lit Literal
  | -- | Call a compiler-generated procedure and return its result.
    CallExpr Name [CallArg]
  | -- | Call a host language function. Used for arithmetic operators,
    -- comparisons, and user-written expressions in guards and bodies.
    -- Host functions return values; they cannot return constraint
    -- identifiers.
    HostCall Name [ValExpr]
  | -- | Switch evaluation into deep deref-aware mode for the nested
    -- expression: 'Var' references are dereferenced (following binding
    -- chains) before use, and this mode propagates recursively into
    -- sub-expressions ('CallExpr', 'MakeTerm', etc.). Used for guard
    -- expressions and the non-'Var' right-hand sides of @is@.
    EvalDeep ValExpr
  | -- | The @is@-with-variable-RHS case: evaluate the nested expression
    -- in deep-deref mode and then walk the resulting 'Value',
    -- evaluating any compound subterm whose @(functor, arity)@ names
    -- a declared evaluable. Emitted only by 'compileBodyGoal' for
    -- @D.BodyIs v expr@ when @expr@ is syntactically a variable; this
    -- is the marker that makes the walker fire for @R is X@ without
    -- affecting guards or other 'EvalDeep' use sites. See the
    -- "Variable RHS in @is@" subsection of the type-system reference.
    EvalIs ValExpr
  | -- Logical variables

    -- | Create a fresh unbound logical variable.
    NewVar
  | -- Term operations

    -- | Construct a compound term: @MakeTerm functor args@.
    MakeTerm Name [ValExpr]
  | -- | Extract an argument from a compound term by index (0-based).
    GetArg ValExpr Int
  | -- Suspension field access

    -- | Extract a constraint argument from a suspension by index.
    FieldArg IdExpr ArgIndex
  | -- | Extract the constraint type tag from a suspension.
    FieldType IdExpr
  deriving (Show, Eq)

-- | Boolean-producing expressions. Operands of 'If', 'BNot', 'BAnd',
-- and 'BOr' are statically booleans, so the interpreter never has to
-- runtime-check the shape of a boolean condition. The 'BFromVal'
-- constructor is the explicit bridge for a 'ValExpr' (typically a
-- user-defined function call or an arbitrary host call) used in
-- boolean position; it carries a runtime shape check at evaluation.
data BoolExpr
  = -- | Boolean literal.
    BLit Bool
  | -- | Logical negation.
    BNot BoolExpr
  | -- | Logical conjunction (short-circuiting).
    BAnd BoolExpr BoolExpr
  | -- | Logical disjunction (short-circuiting).
    BOr BoolExpr BoolExpr
  | -- | Check whether a value is a compound term with the given
    -- functor and arity: @BMatchTerm expr functor arity@.
    BMatchTerm ValExpr Name Int
  | -- | Check equality of two terms (ask semantics). No mutation.
    -- Uses Prolog @==@ semantics: two distinct unbound variables
    -- are not equal.
    BEqual ValExpr ValExpr
  | -- | Compare two constraint identifiers for equality.
    BIdEqual IdExpr IdExpr
  | -- | Check whether a constraint (identified by its constraint
    -- identifier) is still alive in the constraint store.
    BAlive IdExpr
  | -- | Check whether a constraint suspension has the given type.
    -- Used for dispatching in the reactivation procedure.
    BIsConstraintType IdExpr ConstraintType
  | -- | Check that a rule has not previously fired with the given
    -- combination of constraint identifiers.
    BNotInHistory RuleId [IdExpr]
  | -- | Unify two terms (tell semantics). Returns a boolean indicating
    -- success. May mutate logical variables as a side effect. On
    -- success, also pushes affected constraints onto the reactivation
    -- queue (see 'DrainReactivationQueue').
    BUnify ValExpr ValExpr
  | -- | Bridge from 'ValExpr' to 'BoolExpr'. Used for value expressions
    -- whose result the compiler cannot statically prove is a boolean
    -- (e.g. user-defined function calls in guards, host calls whose
    -- return kind isn't recorded). Runtime-checks that the wrapped
    -- value evaluates to 'VBool'.
    BFromVal ValExpr
  | -- | Switch evaluation into deep deref-aware mode for the nested
    -- boolean expression. Mirrors 'EvalDeep' for 'BoolExpr': any
    -- 'ValExpr' or 'IdExpr' payloads inside the nested expression
    -- are evaluated in deep-deref mode.
    BEvalDeep BoolExpr
  deriving (Show, Eq)

-- | Constraint-identifier-producing expressions.
--
-- Constraint identifiers are produced in only three ways: by
-- 'CreateConstraint', by referencing an id-bound variable
-- ('IdVar' — populated by the parameter list, 'Foreach',
-- 'DrainReactivationQueue', or a 'LetId' binding), or by
-- a procedure that returns one (currently no such procedure
-- is generated, but the constructor is reserved).
data IdExpr
  = -- | Reference to an id-bound variable (local or parameter).
    IdVar Name
  | -- | Create a new constraint suspension with the given type and
    -- arguments. Returns a constraint identifier. The constraint
    -- is not yet stored; use 'Store' to add it to the constraint store.
    CreateConstraint ConstraintType [ValExpr]
  deriving (Show, Eq)

-- | Procedure-call argument. Procedures may take a heterogeneous
-- mix of value and id parameters; this wrapper makes the kind
-- explicit at every call site.
data CallArg
  = AVal ValExpr
  | AId IdExpr
  deriving (Show, Eq)

-- | Literal values.
data Literal
  = -- | Integer literal. Arbitrary precision; the runtime carries
    -- 'Integer' end to end so user programs cannot silently overflow.
    IntLit Integer
  | -- | Floating-point literal.
    FloatLit Double
  | -- | Atom literal (symbolic constant).
    AtomLit Text
  | -- | Text (string) literal.
    TextLit Text
  | -- | Boolean literal.
    BoolLit Bool
  | -- | Wildcard literal: evaluates to 'VWildcard'.
    WildcardLit
  deriving (Show, Eq)

-- | Zero-based index into a constraint's argument list.
newtype ArgIndex = ArgIndex Int
  deriving (Show, Eq)

-- | Variable or procedure name.
newtype Name = Name {unName :: Text}
  deriving (Show, Eq, Ord)

instance IsString Name where fromString = Name . T.pack

-- | Label for 'Foreach' loops, used with 'Continue' and 'Break'.
newtype Label = Label {unLabel :: Text}
  deriving (Show, Eq, Ord)

instance IsString Label where fromString = Label . T.pack