Commit 9b252108 authored by POTTIER Francois's avatar POTTIER Francois

Add Toolbox.mli.

parent f1d7e3a4
(* This functor is applied to a type of terms, equipped with visitor classes.
It produces a toolbox of useful functions that operate on terms. *)
module Make (Term : ToolboxInput.INPUT) : sig
open Term
(* A raw term is one where every name is represented as a string. This form
is typically produced by a parser, and consumed by a printer. It is not
used internally. *)
type raw_term =
(string, string) term
(* A nominal term is one where every name is represented as an atom. Although
this is not visible in this type definition, we may additionally impose a
Global Uniqueness Hypothesis (GUH), that is, we may require every binding
name occurrence to carry a distinct atom. *)
type nominal_term =
(Atom.t, Atom.t) term
val fa_term: nominal_term -> Atom.Set.t
val filter_term: (Atom.t -> bool) -> nominal_term -> Atom.t option
val closed_term: nominal_term -> bool
val occurs_term: Atom.t -> nominal_term -> bool
exception IllFormed of Atom.t (* = Atom.Set.NonDisjointUnion *)
val ba_term: nominal_term -> Atom.Set.t
val ba_terms: nominal_term list -> Atom.Set.t
val wf_term: nominal_term -> bool
val wf_terms: nominal_term list -> bool
val copy_term: nominal_term -> nominal_term
val show_term: nominal_term -> raw_term
exception Unbound of string (* = KitImport.Unbound *)
val import_term: KitImport.env -> raw_term -> nominal_term
val export_term: KitExport.env -> nominal_term -> raw_term
val size_term: (_, _) term -> int
val equiv_term: nominal_term -> nominal_term -> bool
val subst_term_term : nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_term_term1: nominal_term -> Atom.t -> nominal_term -> nominal_term
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment