Module Rewrite.Term

Rewriting on Terms

type rule
module Rule : sig ... end
module Set : sig ... end
type rule_set = Set.t
module Rule_inst_set : sig ... end

Set of rules with their instantiation

val normalize_term : ?⁠max_steps:int -> term -> term * Rule_inst_set.t

normalize t computes the normal form of t w.r.t the set of rewrite rules stored in IDs. Returns the new term and the set of rules that were used

parameter max_steps

number of steps after which we stop

val normalize_term_fst : ?⁠max_steps:int -> term -> term

Same as normalize_term but ignores the set of rules

val narrow_term : ?⁠subst:Unif_subst.t -> scope_rules:Scoped.scope -> term Scoped.t -> (rule * Unif_subst.t) Iter.t

narrow_term ~scope_rule t finds the set of rules (l --> r) in IDs and substitutions sigma such that sigma(l) = sigma(t)

parameter scope_rules

used for rules (LEFT)