Module Rewriting

module Rewriting: sig .. end

Contains the functions responsible for rewriting and normalization.

type rrules_set

A set of rewriting rules.

val new_rules_set : (bool * Term.term * Term.term) list -> rrules_set

A new set of rewriting rules, containing the given list

val add_first_rule : rrules_set -> bool * Term.term * Term.term -> rrules_set

Add a rewriting rule: whether the rewritten term has to be ground, LHS and RHS -- to the set, at the start.

val add_last_rule : rrules_set -> bool * Term.term * Term.term -> rrules_set

Add a rewriting rule to the set, at the end.

val merge_rules : rrules_set -> rrules_set -> rrules_set

val empty_rrules : rrules_set -> bool

val rewrite : Term.decls_set -> rrules_set -> Term.term -> Term.term

Rewrite a Term using the set of rules.

Normalisation

val normalise_brackets : Term.term -> Term.term

Just normalise the special bracketing function.

val normalise : Term.decls_set ->
       Term.term Term.TermHashtbl.t ->
       (string, rrules_set) Hashtbl.t ->
       (string -> bool) -> (Term.term -> Term.term) -> Term.term -> Term.term

Normalise the Term.