datalog.top_down
Make.Rewriting
datalog
datalog.caml_interface
datalog.unix
type rule = T.t * 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 -> T.t -> T.t
rewrite the term, but only its root. Subterms are not rewritten at all.
val rewrite : t -> T.t -> T.t
Normalize the term recursively. The returned type cannot be rewritten any further, assuming the rewriting system is terminating