BindingForms.ml 10.7 KB
Newer Older
1 2
type void

POTTIER Francois's avatar
POTTIER Francois committed
3 4 5 6 7 8 9 10 11 12
(* -------------------------------------------------------------------------- *)

(* 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. *)

13
type ('bn, 'term) abs =
POTTIER Francois's avatar
POTTIER Francois committed
14 15 16 17
  'bn * 'term

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

18 19 20 21 22 23 24 25
(* A definition is a binding form of the form [let (rec) x = t in u]. The name
   [x] is in scope in [u]. It is in scope in [t] if the definition is marked
   recursive; otherwise, it is not. The terms [t] and [u] need not belong to the
   same syntactic category. *)

type recursive =
  | NonRecursive
  | Recursive
26

27
type ('bn, 't, 'u) def =
28
  recursive * 'bn * 't * 'u
29

30 31 32 33 34 35
let choose recursive env env' =
  match recursive with
  | NonRecursive ->
      env
  | Recursive ->
      env'
36 37 38

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

39 40 41 42 43 44 45 46 47 48 49 50 51
(* A telescope is represented as a pair of a tele and a scope. A tele is a
   list of bindings, where, in [(x, t) :: xts], the name [x] is considered
   bound in [xts]. Furthermore, in a telescope [xts, u], all of the names
   in the domain of [xts] are considered bound in [u]. *)

type ('bn, 't) tele =
  ('bn * 't) list

type ('bn, 't, 'u) telescope =
  ('bn, 't) tele * 'u

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

POTTIER Francois's avatar
POTTIER Francois committed
52 53 54 55 56 57 58 59 60 61 62
(* The main effect of an abstraction is to cause the environment to be
   enriched when the abstraction is traversed. The following classes define
   where the environment is enriched. *)

(* These classes do not know the type of the environment, and do not know how
   it is enriched; the latter task is delegated to virtual methods, such as
   [extend] and [restrict]. The implementation of these methods is provided
   by separate ``kits''. *)

(* We need one class per variety of visitor, which is a bit painful. *)

POTTIER Francois's avatar
POTTIER Francois committed
63 64 65
(* The method [visit_abs] is polymorphic in the type of terms. This is
   important, as it means that one can use several instances of [abs] in a
   single type definition and still be able to construct well-typed
POTTIER Francois's avatar
POTTIER Francois committed
66 67 68 69 70 71 72 73 74
   visitors. *)

(* The virtual methods [extend] and [restrict] are 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. *)

(* Because [iter] and [iter2] are special cases of [reduce] and [reduce2],
   respectively, we define them that way, so as to save effort. *)

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

(* [map] *)

POTTIER Francois's avatar
POTTIER Francois committed
79 80
class virtual ['self] map = object (self : 'self)

81 82 83
  method private visit_'bn: void -> void -> void
  = fun _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
84 85
  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env

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

95
  method private visit_def: 't1 't2 'u1 'u2 .
96
    _ ->
97 98 99
    ('env -> 't1 -> 't2) ->
    ('env -> 'u1 -> 'u2) ->
    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def
POTTIER Francois's avatar
POTTIER Francois committed
100
  = fun _ visit_t visit_u env (recursive, x1, t1, u1) ->
POTTIER Francois's avatar
POTTIER Francois committed
101
      let x2, env' = self#extend x1 env in
POTTIER Francois's avatar
POTTIER Francois committed
102 103
      let t2 = visit_t (choose recursive env env') t1 in
      let u2 = visit_u env' u1 in
104
      recursive, x2, t2, u2
105

106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  method visit_tele: 't1 't2 .
    ('env -> 't1 -> 't2) ->
    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele * 'env
  = fun visit_t env xts1 ->
      match xts1 with
      | [] ->
          [], env
      | (x1, t1) :: xts1 ->
          let t2 = visit_t env t1 in
          let x2, env = self#extend x1 env in
          let xts2, env = self#visit_tele visit_t env xts1 in
          (x2, t2) :: xts2, env

  method visit_telescope: 't1 't2 'u1 'u2 .
    _ ->
    ('env -> 't1 -> 't2) ->
    ('env -> 'u1 -> 'u2) ->
    'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope
  = fun _ visit_t visit_u env (xts1, u1) ->
      let xts2, env = self#visit_tele visit_t env xts1 in
      let u2 = visit_u env u1 in
      xts2, u2

POTTIER Francois's avatar
POTTIER Francois committed
129 130
end

POTTIER Francois's avatar
POTTIER Francois committed
131 132 133 134
(* -------------------------------------------------------------------------- *)

(* [endo] *)

POTTIER Francois's avatar
POTTIER Francois committed
135 136
class virtual ['self] endo = object (self : 'self)

137 138 139
  method private visit_'bn: void -> void -> void
  = fun _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
140 141
  method private virtual extend: 'bn -> 'env -> 'bn * 'env

142
  method private visit_abs: 'term .
POTTIER Francois's avatar
POTTIER Francois committed
143 144
    _ ->
    ('env -> 'term -> 'term) ->
145
    'env -> ('bn, 'term) abs -> ('bn, 'term) abs
POTTIER Francois's avatar
POTTIER Francois committed
146
  = fun _ visit_term env ((x1, t1) as this) ->
POTTIER Francois's avatar
POTTIER Francois committed
147
      let x2, env' = self#extend x1 env in
POTTIER Francois's avatar
POTTIER Francois committed
148
      let t2 = visit_term env' t1 in
POTTIER Francois's avatar
POTTIER Francois committed
149
      if x1 == x2 && t1 == t2 then
POTTIER Francois's avatar
POTTIER Francois committed
150 151
        this
      else
POTTIER Francois's avatar
POTTIER Francois committed
152
        x2, t2
POTTIER Francois's avatar
POTTIER Francois committed
153

154
  method private visit_def: 't 'u .
155
    _ ->
156 157 158
    ('env -> 't -> 't) ->
    ('env -> 'u -> 'u) ->
    'env -> ('bn, 't, 'u) def -> ('bn, 't, 'u) def
POTTIER Francois's avatar
POTTIER Francois committed
159
  = fun _ visit_t visit_u env ((recursive, x1, t1, u1) as this) ->
POTTIER Francois's avatar
POTTIER Francois committed
160
      let x2, env' = self#extend x1 env in
POTTIER Francois's avatar
POTTIER Francois committed
161 162
      let t2 = visit_t (choose recursive env env') t1 in
      let u2 = visit_u env' u1 in
POTTIER Francois's avatar
POTTIER Francois committed
163
      if x1 == x2 && t1 == t2 && u1 == u2 then
164 165
        this
      else
166
        recursive, x2, t2, u2
167

168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
  method visit_tele: 't .
    ('env -> 't -> 't) ->
    'env -> ('bn, 't) tele -> ('bn, 't) tele * 'env
  = fun visit_t env xts1 ->
      match xts1 with
      | [] ->
          [], env
      | ((x1, t1) :: xts1) as this ->
          let t2 = visit_t env t1 in
          let x2, env = self#extend x1 env in
          let xts2, env = self#visit_tele visit_t env xts1 in
          if x1 == x2 && t1 == t2 && xts1 == xts2 then
            this, env
          else
            (x2, t2) :: xts2, env

  method visit_telescope: 't 'u .
    _ ->
    ('env -> 't -> 't) ->
    ('env -> 'u -> 'u) ->
    'env -> ('bn, 't, 'u) telescope -> ('bn, 't, 'u) telescope
  = fun _ visit_t visit_u env ((xts1, u1) as this) ->
      let xts2, env = self#visit_tele visit_t env xts1 in
      let u2 = visit_u env u1 in
      if xts1 == xts2 && u1 == u2 then
        this
      else
        xts2, u2

POTTIER Francois's avatar
POTTIER Francois committed
197 198
end

POTTIER Francois's avatar
POTTIER Francois committed
199 200 201 202
(* -------------------------------------------------------------------------- *)

(* [reduce] *)

POTTIER Francois's avatar
POTTIER Francois committed
203 204
class virtual ['self] reduce = object (self : 'self)

205
  inherit ['z] VisitorsRuntime.monoid
206

207 208 209
  method private visit_'bn: void -> void -> void
  = fun _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
210 211 212 213
  method private virtual extend: 'bn -> 'env -> 'env

  method private virtual restrict: 'bn -> 'z -> 'z

214
  method private visit_abs: 'term .
POTTIER Francois's avatar
POTTIER Francois committed
215 216
    _ ->
    ('env -> 'term -> 'z) ->
217
    'env -> ('bn, 'term) abs -> 'z
POTTIER Francois's avatar
POTTIER Francois committed
218
  = fun _ visit_term env (x, t) ->
POTTIER Francois's avatar
POTTIER Francois committed
219
      let env' = self#extend x env in
POTTIER Francois's avatar
POTTIER Francois committed
220
      self#restrict x (visit_term env' t)
POTTIER Francois's avatar
POTTIER Francois committed
221

222
  method private visit_def: 't 'u .
223
    _ ->
224 225 226
    ('env -> 't -> 'z) ->
    ('env -> 'u -> 'z) ->
    'env -> ('bn, 't, 'u) def -> 'z
POTTIER Francois's avatar
POTTIER Francois committed
227
  = fun _ visit_t visit_u env (recursive, x, t, u) ->
228
      let env' = self#extend x env in
POTTIER Francois's avatar
POTTIER Francois committed
229 230
      let zt = visit_t (choose recursive env env') t in
      let zu = self#restrict x (visit_u env' u) in
231 232
      self#plus zt zu

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
  method visit_tele: 't .
    ('env -> 't -> 'z) ->
    'env -> ('bn, 't) tele -> 'z * 'env
  = fun visit_t env xts ->
      match xts with
      | [] ->
          self#zero, env
      | (x, t) :: xts ->
          let zt = visit_t env t in
          let env = self#extend x env in
          let zxts, env = self#visit_tele visit_t env xts in
          self#plus zt zxts, env

  method visit_telescope: 't 'u.
    _ ->
    ('env -> 't -> 'z) ->
    ('env -> 'u -> 'z) ->
    'env -> ('bn, 't, 'u) telescope -> 'z
  = fun _ visit_t visit_u env (xts, u) ->
      let zxts, env = self#visit_tele visit_t env xts in
      let zu = visit_u env u in
      self#plus zxts zu

POTTIER Francois's avatar
POTTIER Francois committed
256 257
end

POTTIER Francois's avatar
POTTIER Francois committed
258 259 260 261
(* -------------------------------------------------------------------------- *)

(* [iter] *)

POTTIER Francois's avatar
POTTIER Francois committed
262 263
class virtual ['self] iter = object (_ : 'self)
  inherit ['self] reduce
264
  inherit [_] VisitorsRuntime.unit_monoid
POTTIER Francois's avatar
POTTIER Francois committed
265 266 267
  method private restrict _ () = ()
end

POTTIER Francois's avatar
POTTIER Francois committed
268 269 270 271
(* -------------------------------------------------------------------------- *)

(* [map2] *)

POTTIER Francois's avatar
POTTIER Francois committed
272 273
class virtual ['self] map2 = object (self : 'self)

274 275 276
  method private visit_'bn: void -> void -> void -> void
  = fun _ _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
277 278
  method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'bn3 * 'env

279
  method private visit_abs: 'term1 'term2 'term3 .
POTTIER Francois's avatar
POTTIER Francois committed
280 281
    _ ->
    ('env -> 'term1 -> 'term2 -> 'term3) ->
282
    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> ('bn3, 'term3) abs
POTTIER Francois's avatar
POTTIER Francois committed
283
  = fun _ visit_term env (x1, t1) (x2, t2) ->
POTTIER Francois's avatar
POTTIER Francois committed
284
      let x3, env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
285
      x3, visit_term env' t1 t2
POTTIER Francois's avatar
POTTIER Francois committed
286

287
  method private visit_def: 't1 'u1 't2 'u2 't3 'u3 .
288
    _ ->
289 290 291
    ('env -> 't1 -> 't2 -> 't3) ->
    ('env -> 'u1 -> 'u2 -> 'u3) ->
    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> ('bn3, 't3, 'u3) def
POTTIER Francois's avatar
POTTIER Francois committed
292
  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
293
      if recursive1 <> recursive2 then VisitorsRuntime.fail();
294
      let x3, env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
295 296
      let t3 = visit_t (choose recursive1 env env') t1 t2 in
      let u3 = visit_u env' u1 u2 in
297
      recursive1, x3, t3, u3
298

POTTIER Francois's avatar
POTTIER Francois committed
299 300
end

POTTIER Francois's avatar
POTTIER Francois committed
301 302 303 304
(* -------------------------------------------------------------------------- *)

(* [reduce2] *)

POTTIER Francois's avatar
POTTIER Francois committed
305 306
class virtual ['self] reduce2 = object (self : 'self)

307 308
  method private virtual plus: 'z -> 'z -> 'z

309 310 311
  method private visit_'bn: void -> void -> void -> void
  = fun _ _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
312 313 314 315
  method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env

  method private virtual restrict: 'bn1 -> 'bn2 -> 'z -> 'z

316
  method private visit_abs: 'term1 'term2 .
POTTIER Francois's avatar
POTTIER Francois committed
317 318
    _ ->
    ('env -> 'term1 -> 'term2 -> 'z) ->
319
    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
POTTIER Francois's avatar
POTTIER Francois committed
320
  = fun _ visit_term env (x1, t1) (x2, t2) ->
POTTIER Francois's avatar
POTTIER Francois committed
321
      let env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
322
      self#restrict x1 x2 (visit_term env' t1 t2)
POTTIER Francois's avatar
POTTIER Francois committed
323

324
  method private visit_def: 't1 'u1 't2 'u2 .
325
    _ ->
326 327 328
    ('env -> 't1 -> 't2 -> 'z) ->
    ('env -> 'u1 -> 'u2 -> 'z) ->
    'env -> ('bn1, 't1, 'u1) def -> ('bn2, 't2, 'u2) def -> 'z
POTTIER Francois's avatar
POTTIER Francois committed
329
  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
330
      if recursive1 <> recursive2 then VisitorsRuntime.fail();
331
      let env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
332 333
      let zt = visit_t (choose recursive1 env env') t1 t2 in
      let zu = self#restrict x1 x2 (visit_u env' u1 u2) in
334 335
      self#plus zt zu

POTTIER Francois's avatar
POTTIER Francois committed
336 337
end

POTTIER Francois's avatar
POTTIER Francois committed
338 339 340 341
(* -------------------------------------------------------------------------- *)

(* [iter2] *)

POTTIER Francois's avatar
POTTIER Francois committed
342 343
class virtual ['self] iter2 = object (_ : 'self)
  inherit ['self] reduce2
344
  inherit [_] VisitorsRuntime.unit_monoid
POTTIER Francois's avatar
POTTIER Francois committed
345 346
  method private restrict _ _ () = ()
end