Module Logtk.HORewriting (.ml)

module HORewriting: LogtkHORewriting

type term = LogtkHOTerm.t 
type rule = term * term 
exception IllFormedRule of rule

Building rewrite systems


type t 
rewrite system
val empty : t
No rules
val add : t -> rule -> t
Add a rule. A rule must satisfy several conditions:
Raises IllFormedRule if the rule isn't valid.
val merge : t -> t -> t
Merge two rewrite systems
module Seq: sig .. end
val of_list : rule list -> t
val to_list : t -> rule list
include LogtkInterfaces.PRINT
include LogtkInterfaces.ORD
include LogtkInterfaces.HASH

Normalizing terms


val normalize : t -> term -> term
Normalize the term w.r.t to the rewrite system
val normalize_collect : t ->
term -> term * rule list
Normalize the term, and returns a list of rules used to normalize it.