package datalog

  1. Overview
  2. Docs
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