package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkRewriting on HO terms

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:

  • every free variable on the RHS must occur in the LHS
  • every free variable on the RHS must not occur under any binder (would cause problems with De Bruijn indices)
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 with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int
include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int

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.