ToolboxInput.ml 1.78 KB
Newer Older
1 2 3
module type INPUT = sig

  (* Suppose there is a type of terms, which is parameterized over the
4
     representations of binding name occurrences and free name occurrences. *)
5

6
  type ('bn, 'fn) term
7 8 9 10 11 12

  (* Suppose the type of terms is equipped with the following visitors. *)

  (* The private virtual method [visit_'fn] is used to specify what should
     be done at free name occurrences. The private virtual method [extend]
     is used to indicate how the environment should be extended when an
13
     abstraction is entered. *)
14 15 16 17 18 19

  (* Suppose the data constructor for variables is named [TVar], so that
     the method [visit_TVar] is used to specify what behavior at variables
     is desired. *)

  class virtual ['self] iter : object ('self)
20
    method private virtual extend : 'env -> 'bn -> 'env
21
    method private virtual visit_'fn : 'env -> 'fn -> _
22
    method visit_term : 'env -> ('bn, 'fn) term -> unit
23 24 25
  end

  class virtual ['self] map : object ('self)
26
    method private virtual extend : 'env -> 'bn1 -> 'env * 'bn2
27
    method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2
28 29
    method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term
    method private visit_TVar : 'env -> 'fn1 -> ('bn2, 'fn2) term
30 31 32
  end

  class virtual ['self] endo : object ('self)
33
    method private virtual extend : 'env -> 'bn -> 'env * 'bn
34
    method private virtual visit_'fn : 'env -> 'fn -> 'fn
35 36
    method visit_term : 'env -> ('bn, 'fn) term -> ('bn, 'fn) term
    method private visit_TVar : 'env -> ('bn, 'fn) term -> 'fn -> ('bn, 'fn) term
37 38 39
  end

  class virtual ['self] iter2 : object ('self)
40
    method private virtual extend : 'env -> 'bn1 -> 'bn2 -> 'env
41
    method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2 -> _
42
    method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term -> unit
43 44 45
  end

end