BindingFormsAbs.ml 3.52 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(* -------------------------------------------------------------------------- *)

(* A universal, concrete type of single-name abstractions. *)

(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
   in de Bruijn style, etc. -- so we parameterize the abstraction over the
   type ['bn] of the bound name and over the type ['term] of the body. This
   makes this type definition almost trivial -- it is just a pair -- but it
   still serves as a syntactic marker of where abstractions are located. *)

type ('bn, 'term) abs =
  'bn * 'term

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

(* The main effect of a binding construct is to cause the environment to be
   enriched when the abstraction is traversed. The following visitor methods
   define where the environment is enriched. *)

(* These methods do not know the type of the environment, and do not know how
21 22 23
   it is enriched; the latter task is delegated to the virtual method
   [extend]. The implementation of this method is provided by separate
   ``kits''. *)
24 25 26 27 28 29 30 31 32

(* We need several varieties of visitors, which is a bit painful. As of now,
   [iter], [map], [endo], [iter2] are required: see [ToolboxInput]. *)

(* The visitor methods are polymorphic in the type of terms. This is
   important, as it means that one can use several instances of a binding
   construct in a single type definition and still be able to construct
   well-typed visitors. *)

33 34 35
(* The virtual method [extend] is not polymorphic in the types of bound names
   and environments. On the contrary, each kit comes with certain specific
   types of bound names and environments. *)
36 37 38 39 40 41 42

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

(* [iter] *)

class virtual ['self] iter = object (self : 'self)

43
  method private virtual extend: 'env -> 'bn -> 'env
44 45 46 47 48 49

  method private visit_abs: 'term .
    _ ->
    ('env -> 'term -> unit) ->
    'env -> ('bn, 'term) abs -> unit
  = fun _ visit_term env (x, t) ->
50
      let env' = self#extend env x in
51 52 53 54 55 56 57 58 59 60
      visit_term env' t

end

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

(* [iter2] *)

class virtual ['self] iter2 = object (self : 'self)

61
  method private virtual extend: 'env -> 'bn1 -> 'bn2 -> 'env
62 63 64 65 66 67

  method private visit_abs: 'term1 'term2 .
    _ ->
    ('env -> 'term1 -> 'term2 -> 'z) ->
    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
  = fun _ visit_term env (x1, t1) (x2, t2) ->
68
      let env' = self#extend env x1 x2 in
69 70 71 72 73 74 75 76 77 78
      visit_term env' t1 t2

end

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

(* [map] *)

class virtual ['self] map = object (self : 'self)

79
  method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
80 81 82 83 84 85

  method private visit_abs: 'term1 'term2 .
    _ ->
    ('env -> 'term1 -> 'term2) ->
    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs
  = fun _ visit_term env (x1, t1) ->
86 87
      let env, x2 = self#extend env x1 in
      let t2 = visit_term env t1 in
88 89 90 91 92 93 94 95 96 97
      x2, t2

end

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

(* [endo] *)

class virtual ['self] endo = object (self : 'self)

98
  method private virtual extend: 'env -> 'bn1 -> 'env * 'bn2
99 100 101 102 103 104

  method private visit_abs: 'term .
    _ ->
    ('env -> 'term -> 'term) ->
    'env -> ('bn, 'term) abs -> ('bn, 'term) abs
  = fun _ visit_term env ((x1, t1) as this) ->
105 106
      let env, x2 = self#extend env x1 in
      let t2 = visit_term env t1 in
107 108 109 110 111 112
      if x1 == x2 && t1 == t2 then
        this
      else
        x2, t2

end