Commit 96413c28 authored by POTTIER Francois's avatar POTTIER Francois

Isolated the output signature of [Toolbox.Make].

parent e1ef36a0
open ToolboxInput
(* 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) = struct
module Make (Term : INPUT) = struct
open Term
include Term
(* -------------------------------------------------------------------------- *)
......
open ToolboxInput
open ToolboxOutput
(* 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
val ba_term: nominal_term -> Atom.Set.t
val avoids_term: Atom.Set.t -> nominal_term -> bool
val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool
val copy_term: nominal_term -> nominal_term
val avoid_term: Atom.Set.t -> 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_TVar_term:
(nominal_term -> nominal_term) ->
nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_TVar_term1:
(nominal_term -> nominal_term) ->
nominal_term -> Atom.t -> nominal_term -> nominal_term
end
module Make (Term : INPUT) : OUTPUT
with type ('bn, 'fn) term = ('bn, 'fn) Term.term
module type OUTPUT = sig
(* A type of terms, is parameterized over the representations of binding
name occurrences and free name occurrences. *)
type ('bn, 'fn) 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
val ba_term: nominal_term -> Atom.Set.t
val avoids_term: Atom.Set.t -> nominal_term -> bool
val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool
val copy_term: nominal_term -> nominal_term
val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
val show_term: nominal_term -> raw_term
exception Unbound of string
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_TVar_term:
(nominal_term -> nominal_term) ->
nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_TVar_term1:
(nominal_term -> nominal_term) ->
nominal_term -> Atom.t -> nominal_term -> nominal_term
end
......@@ -14,4 +14,5 @@ KitSubst
KitToDeBruijn
KitTrivial
ToolboxInput
ToolboxOutput
Toolbox
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