Toolbox.cppo.ml 1.38 KB
Newer Older
1 2
open ToolboxInput

POTTIER Francois's avatar
POTTIER Francois committed
3 4 5
(* This functor is applied to a type of terms, equipped with visitor classes.
   It produces a toolbox of useful functions that operate on terms. *)

6
module Make (Term : INPUT) = struct
POTTIER Francois's avatar
POTTIER Francois committed
7

8
  include Term
POTTIER Francois's avatar
POTTIER Francois committed
9 10 11

(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
12 13 14
  (* 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. *)
POTTIER Francois's avatar
POTTIER Francois committed
15

POTTIER Francois's avatar
POTTIER Francois committed
16 17
  type raw_term =
    (string, string) term
POTTIER Francois's avatar
POTTIER Francois committed
18

POTTIER Francois's avatar
POTTIER Francois committed
19 20 21 22
  (* 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. *)
POTTIER Francois's avatar
POTTIER Francois committed
23

POTTIER Francois's avatar
POTTIER Francois committed
24 25
  type nominal_term =
    (Atom.t, Atom.t) term
POTTIER Francois's avatar
POTTIER Francois committed
26 27 28

(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
29 30 31 32 33 34 35
  (* All of the code is produced by macro-expansion. *)

  (* This serves as a test of our macros, which can also be used directly by
     the end user, in situations where the functor [Toolbox.Make] cannot be
     used. *)

  #include "AlphaLibMacros.cppo.ml"
POTTIER Francois's avatar
POTTIER Francois committed
36

37 38
  __ALL
  ALL(term)
POTTIER Francois's avatar
POTTIER Francois committed
39

40 41 42
  (* Mnemonic: Substitute for variables in terms. *)
  __SUBST(TVar)
  SUBST(TVar, term)
POTTIER Francois's avatar
POTTIER Francois committed
43

POTTIER Francois's avatar
POTTIER Francois committed
44 45 46
(* -------------------------------------------------------------------------- *)

end