Toolbox.cppo.ml 1.63 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

POTTIER Francois's avatar
POTTIER Francois committed
37 38
  __FA
  FA(term)
POTTIER Francois's avatar
POTTIER Francois committed
39

POTTIER Francois's avatar
POTTIER Francois committed
40 41
  __FILTER
  FILTER(term)
42

POTTIER Francois's avatar
POTTIER Francois committed
43 44
  __BA
  BA(term)
45

POTTIER Francois's avatar
POTTIER Francois committed
46 47 48
  __AVOIDS
  AVOIDS(term)

49 50 51
  __GUQ
  GUQ(term)

POTTIER Francois's avatar
POTTIER Francois committed
52 53
  __COPY
  COPY(term)
POTTIER Francois's avatar
POTTIER Francois committed
54

POTTIER Francois's avatar
POTTIER Francois committed
55 56 57
  __AVOID
  AVOID(term)

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

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

64 65 66
  __SHOW
  SHOW(term)

POTTIER Francois's avatar
POTTIER Francois committed
67 68
  __SIZE
  SIZE(term)
POTTIER Francois's avatar
POTTIER Francois committed
69

POTTIER Francois's avatar
POTTIER Francois committed
70 71
  __EQUIV
  EQUIV(term)
POTTIER Francois's avatar
POTTIER Francois committed
72

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

POTTIER Francois's avatar
POTTIER Francois committed
77 78 79
(* -------------------------------------------------------------------------- *)

end