Toolbox.mli 1.76 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
(* 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
POTTIER Francois's avatar
POTTIER Francois committed
35
  val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
POTTIER Francois's avatar
POTTIER Francois committed
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51

  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