From 9b2521083c683ffb5bd49d1786025034fdffbc64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= Date: Wed, 1 Feb 2017 15:24:56 +0100 Subject: [PATCH] Add Toolbox.mli. --- src/Toolbox.mli | 50 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 src/Toolbox.mli diff --git a/src/Toolbox.mli b/src/Toolbox.mli new file mode 100644 index 0000000..f22ba2f --- /dev/null +++ b/src/Toolbox.mli @@ -0,0 +1,50 @@ +(* 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 -- GitLab