(** Open terms and unification.

    A pattern is a {!Term.t} that may contain logic variables. Goals,
    rule heads, and rule bodies are made of patterns; solving a query
    means finding substitutions that close them back into terms.
    Unification here is the join mechanism of the whole language:
    shared variables across conjoined propositions unify, and that is
    what a join is. *)

type t =
  | Var of string
  | Integer of Z.t
  | Rational of Q.t
  | String of string
  | Nil
  | Record of t Label.Map.t

val of_term : Term.t -> t
(** Injects a closed term. Canonicity carries over unchanged. *)

val to_term : t -> Term.t option
(** Closes a pattern back into a term. [None] if any variable
    remains, so [Some] is proof of groundness. *)

val is_ground : t -> bool

val vars : t -> string list
(** Free variables, each reported once. The solver reports solutions
    for exactly these. *)

val cons : head:t -> tail:t -> t
(** One sequence cell over open terms, [{head: _ tail: _}]. The
    loader elaborates [#( ... )] in rule heads and bodies with
    this. *)

val equal : t -> t -> bool
(** Syntactic equality, variables by name. Used by the totality
    checker to compare head and body arguments. *)

val strictly_contains : t -> sub:t -> bool
(** Whether [sub] occurs strictly inside the pattern, at depth one or
    more. This is the structural decrease witness of the admission
    checker: a recursive call is safe when its argument is strictly
    contained in the head's. *)

val pp : Format.formatter -> t -> unit

(** The verified checker's view of patterns. Admission projects
    patterns through {!to_checker} and runs the containment and
    lexicographic checkers extracted from Rocq; the conversion is
    injective by leaf kind, and these two equalities are the
    trusted seam. *)
type checker_leaf

val checker_leaf_equal : checker_leaf -> checker_leaf -> bool

val to_checker : t -> (Label.t, checker_leaf) Decrease_extracted.term

(** Substitutions bind variables to patterns. They only grow;
    unification never revokes a binding. *)
module Subst : sig
  type pattern := t
  type t

  val empty : t

  val walk : t -> pattern -> pattern
  (** Follows variable bindings one level: the result is either a
      non-variable or an unbound variable. The solver's view of "what
      is this argument right now". *)

  val resolve : t -> pattern -> pattern
  (** Applies the substitution everywhere, recursively. Used to read
      answers out and to test groundness of arguments. *)

  val unify : t -> pattern -> pattern -> t option
  (** Extends the substitution so both sides are equal, or reports
      impossibility. Records unify only on identical label sets.
      Runs an occurs check: Sol terms are finite, so a solution that
      would need an infinite term is a failure, not a loop. *)
end