BindingForms.ml 12.5 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
  method private visit_tele: 't1 't2 .
107 108 109 110 111 112 113 114 115 116 117 118
    ('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

119
  method private visit_telescope: 't1 't2 'u1 'u2 .
120 121 122 123 124 125 126 127 128
    _ ->
    ('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
  method private visit_tele: 't .
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
    ('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

184
  method private visit_telescope: 't 'u .
185 186 187 188 189 190 191 192 193 194 195 196
    _ ->
    ('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
  method private visit_tele: 't .
234 235 236 237 238 239 240 241 242 243 244 245
    ('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

246
  method private visit_telescope: 't 'u.
247 248 249 250 251 252 253 254 255
    _ ->
    ('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

299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323
  method private visit_tele: 't1 't2 't3 .
    ('env -> 't1 -> 't2 -> 't3) ->
    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> ('bn3, 't3) tele * 'env
  = fun visit_t env xts1 xts2 ->
      match xts1, xts2 with
      | [], [] ->
          [], env
      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
          let t3 = visit_t env t1 t2 in
          let x3, env = self#extend x1 x2 env in
          let xts3, env = self#visit_tele visit_t env xts1 xts2 in
          (x3, t3) :: xts3, env
      | _, _ ->
          VisitorsRuntime.fail()

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

POTTIER Francois's avatar
POTTIER Francois committed
324 325
end

POTTIER Francois's avatar
POTTIER Francois committed
326 327 328 329
(* -------------------------------------------------------------------------- *)

(* [reduce2] *)

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

332
  inherit ['z] VisitorsRuntime.monoid
333

334 335 336
  method private visit_'bn: void -> void -> void -> void
  = fun _ _ _ -> assert false

POTTIER Francois's avatar
POTTIER Francois committed
337 338 339 340
  method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env

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

341
  method private visit_abs: 'term1 'term2 .
POTTIER Francois's avatar
POTTIER Francois committed
342 343
    _ ->
    ('env -> 'term1 -> 'term2 -> 'z) ->
344
    'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
POTTIER Francois's avatar
POTTIER Francois committed
345
  = fun _ visit_term env (x1, t1) (x2, t2) ->
POTTIER Francois's avatar
POTTIER Francois committed
346
      let env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
347
      self#restrict x1 x2 (visit_term env' t1 t2)
POTTIER Francois's avatar
POTTIER Francois committed
348

349
  method private visit_def: 't1 'u1 't2 'u2 .
350
    _ ->
351 352 353
    ('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
354
  = fun _ visit_t visit_u env (recursive1, x1, t1, u1) (recursive2, x2, t2, u2) ->
355
      if recursive1 <> recursive2 then VisitorsRuntime.fail();
356
      let env' = self#extend x1 x2 env in
POTTIER Francois's avatar
POTTIER Francois committed
357 358
      let zt = visit_t (choose recursive1 env env') t1 t2 in
      let zu = self#restrict x1 x2 (visit_u env' u1 u2) in
359 360
      self#plus zt zu

361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
  method private visit_tele: 't1 't2 .
    ('env -> 't1 -> 't2 -> 'z) ->
    'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'z * 'env
  = fun visit_t env xts1 xts2 ->
      match xts1, xts2 with
      | [], [] ->
          self#zero, env
      | (x1, t1) :: xts1, (x2, t2) :: xts2 ->
          let zt = visit_t env t1 t2 in
          let env = self#extend x1 x2 env in
          let zxts, env = self#visit_tele visit_t env xts1 xts2 in
          self#plus zt zxts, env
      | _, _ ->
          VisitorsRuntime.fail()

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

POTTIER Francois's avatar
POTTIER Francois committed
386 387
end

POTTIER Francois's avatar
POTTIER Francois committed
388 389 390 391
(* -------------------------------------------------------------------------- *)

(* [iter2] *)

POTTIER Francois's avatar
POTTIER Francois committed
392 393
class virtual ['self] iter2 = object (_ : 'self)
  inherit ['self] reduce2
394
  inherit [_] VisitorsRuntime.unit_monoid
POTTIER Francois's avatar
POTTIER Francois committed
395 396
  method private restrict _ _ () = ()
end