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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct