package libzipperposition

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

Clause context

A clause with a "hole" in it. Filling the whole with a term t is called "applying the context to t".

The point is to relate different applications of the same context.

type term = Logtk.Term.t
type subst = Logtk.Subst.t
type t

A context is represented as a regular array of literals, containing at least one specific variable x, paired with this variable x. Applying the context is a mere substitution

val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val make : Logtk.Literals.t -> var:Logtk.Term.var -> t

Make a context from a var and literals containing this var.

val extract : Logtk.Literals.t -> term -> t option

extract lits t returns None if t doesn't occur in lits. Otherwise, it creates a fresh var x, replaces t with x within lits, and returns the corresponding context. Basically, if extract lits t = Some c then apply c t = lits

val extract_exn : Logtk.Literals.t -> term -> t

Unsafe version of extract.

val trivial : Logtk.Literals.t -> term -> t

Trivial context, that contains 0 holes.

val apply : t -> term -> Logtk.Literals.t

apply c t fills the hole of c with the given term t. t and c share no free variables.

val apply_same_scope : t -> term -> Logtk.Literals.t

Same as apply, but now variables from the context and variables from the term live in the same scope

val raw_lits : t -> Logtk.Literals.t

give access to the underlying literals. Careful not to depend on the variable's actual name.

Sets of contexts

module Set : CCSet.S with type elt = t
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