Toolbox.cppo.ml 1.63 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3
(* This functor is applied to a type of terms, equipped with visitor classes.
   It produces a toolbox of useful functions that operate on terms. *)

4
module Make (Term : ToolboxInput.INPUT) = struct
POTTIER Francois's avatar
POTTIER Francois committed
5

POTTIER Francois's avatar
POTTIER Francois committed
6
  open Term
POTTIER Francois's avatar
POTTIER Francois committed
7 8 9

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

POTTIER Francois's avatar
POTTIER Francois committed
10 11 12
  (* 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
13

POTTIER Francois's avatar
POTTIER Francois committed
14 15
  type raw_term =
    (string, string) term
POTTIER Francois's avatar
POTTIER Francois committed
16

POTTIER Francois's avatar
POTTIER Francois committed
17 18 19 20
  (* 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
21

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

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

POTTIER Francois's avatar
POTTIER Francois committed
27 28 29 30 31 32 33
  (* 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
34

POTTIER Francois's avatar
POTTIER Francois committed
35 36
  __FA
  FA(term)
POTTIER Francois's avatar
POTTIER Francois committed
37

POTTIER Francois's avatar
POTTIER Francois committed
38 39
  __FILTER
  FILTER(term)
40

POTTIER Francois's avatar
POTTIER Francois committed
41 42
  __BA
  BA(term)
43

POTTIER Francois's avatar
POTTIER Francois committed
44 45 46
  __AVOIDS
  AVOIDS(term)

47 48 49
  __GUQ
  GUQ(term)

POTTIER Francois's avatar
POTTIER Francois committed
50 51
  __COPY
  COPY(term)
POTTIER Francois's avatar
POTTIER Francois committed
52

POTTIER Francois's avatar
POTTIER Francois committed
53 54 55
  __AVOID
  AVOID(term)

POTTIER Francois's avatar
POTTIER Francois committed
56 57
  __SHOW
  SHOW(term)
POTTIER Francois's avatar
POTTIER Francois committed
58

POTTIER Francois's avatar
POTTIER Francois committed
59 60
  __IMPORT
  IMPORT(term)
POTTIER Francois's avatar
POTTIER Francois committed
61

POTTIER Francois's avatar
POTTIER Francois committed
62 63
  __EXPORT
  EXPORT(term)
POTTIER Francois's avatar
POTTIER Francois committed
64

POTTIER Francois's avatar
POTTIER Francois committed
65 66
  __SIZE
  SIZE(term)
POTTIER Francois's avatar
POTTIER Francois committed
67

POTTIER Francois's avatar
POTTIER Francois committed
68 69
  __EQUIV
  EQUIV(term)
POTTIER Francois's avatar
POTTIER Francois committed
70

71 72 73
  (* Mnemonic: Substitute for variables in terms. *)
  __SUBST(TVar)
  SUBST(TVar, term)
POTTIER Francois's avatar
POTTIER Francois committed
74

POTTIER Francois's avatar
POTTIER Francois committed
75 76 77
(* -------------------------------------------------------------------------- *)

end