Module TopDown.S.Rewriting

module Rewriting: sig .. end

type rule = TopDown.S.T.t * TopDown.S.T.t

type t

A rewriting system. It is basically a mutable set of rewrite rules.

val create : unit -> t

New rewriting system

val copy : t -> t

Copy the rewriting system

val add : t -> rule -> unit

Add a rule to the system

val add_list : t -> rule list -> unit

val to_list : t -> rule list

List of rules

val rewrite_root : t -> TopDown.S.T.t -> TopDown.S.T.t

rewrite the term, but only its root. Subterms are not rewritten at all.

val rewrite : t -> TopDown.S.T.t -> TopDown.S.T.t

Normalize the term recursively. The returned type cannot be rewritten any further, assuming the rewriting system is terminating