Module Logtk.HO_unif

Higher-Order Unification

type term = Term.t
type penalty = int

penalty on the search space

val enum_prop : ?⁠mode:[ `And | `Or | `Neg | `Quants | `TF | `Eq | `Combinators | `Full | `Pragmatic | `Simple | `None ] -> Term.var Scoped.t -> enum_cache:Logtk.Term.Set.t Stdlib.ref -> signature:Signature.t -> offset:int -> (Subst.t * penalty) list

Given a variable of type τ1…τn -> prop, enumerate possible shapes for it

parameter v

the variable to refine + its scope. Must return prop.

parameter offset

to create fresh variables (should be unused elsewhere)

parameter mode

if `Neg, only tries negation; `None, do nothing; otherwise do all connectives

type pair = Type.t list * term * term

unification pair

val pp_pair : pair CCFormat.printer
val unif_pairs : ?⁠fuel:int -> pair list Scoped.t -> offset:int -> (pair list * Unif_subst.t * penalty * Subst.Renaming.t) list

unif_pairs pairs ~scope_new_vars returns a list of (partial) solutions to the HO unification problem pairs. Each solution is a list of remaining constraints (with the substitution already applied), a substitution, some penalty to influence the search space, and a renaming used for the substitution

val default_fuel : int Stdlib.ref

Default amount of fuel for unif_pairs

val enable_norm_subst : bool Stdlib.ref

If true, substitutions obtained with unif_pairs are normalized and β-reduced