ToolboxInput.ml 2.38 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 13 14 15 16 17 18 19 20 21 22 23 24

  (* 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
     abstraction is entered. In the [reduce] visitor, the private methods
     [zero] and [plus] are used to specify how summaries should be computed,
     while the private method [restrict] is used to specify how a summary
     should be restricted when an abstraction is exited. *)

  (* 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)
    method private virtual extend : 'bn -> 'env -> 'env
    method private virtual visit_'fn : 'env -> 'fn -> _
25
    method visit_term : 'env -> ('bn, 'fn) term -> unit
26 27 28 29 30
  end

  class virtual ['self] map : object ('self)
    method private virtual extend : 'bn1 -> 'env -> 'bn2 * 'env
    method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2
31 32
    method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term
    method private visit_TVar : 'env -> 'fn1 -> ('bn2, 'fn2) term
33 34 35 36 37
  end

  class virtual ['self] endo : object ('self)
    method private virtual extend : 'bn -> 'env -> 'bn * 'env
    method private virtual visit_'fn : 'env -> 'fn -> 'fn
38 39
    method visit_term : 'env -> ('bn, 'fn) term -> ('bn, 'fn) term
    method private visit_TVar : 'env -> ('bn, 'fn) term -> 'fn -> ('bn, 'fn) term
40 41 42 43 44 45 46 47
  end

  class virtual ['self] reduce : object ('self)
    method private virtual extend : 'bn -> 'env -> 'env
    method private virtual visit_'fn : 'env -> 'fn -> 'z
    method private virtual zero : 'z
    method private virtual plus : 'z -> 'z -> 'z
    method private virtual restrict : 'bn -> 'z -> 'z
48
    method visit_term : 'env -> ('bn, 'fn) term -> 'z
49 50 51 52 53
  end

  class virtual ['self] iter2 : object ('self)
    method private virtual extend : 'bn1 -> 'bn2 -> 'env -> 'env
    method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2 -> _
54
    method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term -> unit
55 56 57
  end

end