BindingFormsUnbound.ml 11.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(* -------------------------------------------------------------------------- *)

(* This module defines a little language that allows the user to describe
   complex binding constructs, in the style of Weirich et al.'s "Binders
   unbound" (ICFP 2011). *)

(* Following alphaCaml and "Binders unbound", we distinguish "terms" versus
   "patterns". The syntax of these categories is as follows:

     t ::= ... (* products, sums, etc. *)
         | abstraction(p)

     p ::= ... (* products, sums, etc. *)
         | binder
         | inner(t)
         | outer(t)
         | rebind(p)
         | recursive(p)
         | repeat(p)

   On top of this syntax, we impose the restriction that [recursive] is
   forbidden under [recursive] and [repeat]. This restriction is dynamically
   checked, because checking it statically would be impossible or complicated,
   and would yield bad type error messages when it is violated.

   The combinator [inner(p)] can be viewed as sugar for [rebind(outer(p))].

   Our [rebind(p)] takes just one argument. Weirich et al.'s [rebind],
29 30
   which takes two arguments, is emulated by writing [p1 * rebind(p2)].
   This encoding relies on the fact that pairs are traversed left-to-right. *)
31 32 33 34 35 36 37 38 39 40 41

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

(* Type definitions. *)

type 'p abstraction =
  'p

type 'bn binder =
  'bn

POTTIER Francois's avatar
POTTIER Francois committed
42
type 't inner =
43 44
  't

POTTIER Francois's avatar
POTTIER Francois committed
45
type 't outer =
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
  't

type 'p rebind =
  'p

type 'p repeat =
  'p

type 'p recursive =
  'p

(* Weirich et al.'s [bind] combinator, which takes a pattern and a term and
   constructs a term, can be defined in terms of the above combinators, as
   follows. *)

(* In natural syntax, this is [abstraction (p * inner(t))]. *)

type ('p, 't) bind =
  ('p * 't inner) abstraction

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

(* When traversing a pattern, our visitors maintain a richer environment than
   when traversing a term. If a normal term-traversal environment has type
   ['env], then an enriched pattern-traversal environment has type ['env penv]
   as defined below. *)

(* The meaning of the above combinators is defined by the manner in which they
   extend or use this enriched environment. *)

(* The [current] component is a mutable reference to an environment. This
   environment is extended when a [binder] combinator is visited. This
   mutable state is implicitly threaded from left to right. *)

(* The [outer] component is an immutable environment. It is transmitted in
   a top-down manner. *)

(* The components [at_binder] and [at_outer] respectively determine what
   behavior is desired at [binder] and [outer]. *)

type 'env penv = {
  current: 'env ref;      (* do NOT replace this with a mutable field! *)
  outer: 'env;
  at_binder: at_binder;
  at_outer: at_outer;
}

(* At [binder], two behaviors are possible:
   - [Extend] means that [binder] extends the current environment.
   - [Lookup] means that [binder] does NOT extend the current environment:
     instead, it looks up the environment, which presumably has been extended
     already. *)

and at_binder =
  | Extend
  | Lookup

(* At [outer], two behaviors are possible:
   - [Visit] means that the embedded subterm is visited.
     The [outer] component of the enriched environment is used.
   - [DoNotVisit] means that the embedded subterm is not visited.
     In short, in that case, nothing happens. *)

and at_outer =
  | Visit
  | DoNotVisit

(* We are in [Extend] and [Visit] mode at the beginning, when entering an
   [abstraction], and remain in this mode as long as we are outside both
   [recursive] and [repeat].

   [DoNotVisit] is used in the first phase of visiting a [recursive] construct,
   to find all of the bound names before visiting any embedded subterms.

   [Lookup] is used in the second phase of visiting a [recursive] construct,
   because the environment has been extended already during the first phase.
   It is used also under [repeat]. *)

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

(* A few auxiliary functions. *)

(* [abstraction] initializes an enriched environment. [current] and [outer]
   are initialized with the environment that exists outside the abstraction.
   The behavior is initially [Extend/Visit]. *)

let abstraction (env : 'env) : 'env penv =
  { current = ref env; outer = env; at_binder = Extend; at_outer = Visit }

(* [rebind] copies the [current] component of the environment into the [outer]
   component. In other words, it locally changes the meaning of [outer]. *)

let rebind (penv : 'env penv) : 'env penv =
  { penv with outer = !(penv.current) }

(* [recursive] is forbidden under [recursive] or [repeat]. If this rule is
   violated, raise an exception that carries a readable explanation. *)

let check_recursive_permitted (penv : 'env penv) : unit =
  match penv.at_binder, penv.at_outer with
  | Extend, Visit ->
      ()
  | _, DoNotVisit
  | Lookup, _ ->
      failwith "AlphaLib: \"recursive\" cannot be used under \"recursive\" or \"repeat\"."

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

(* [map] *)

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

  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env
159
  method private virtual lookup: 'env -> 'bn1 -> 'bn2
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185

  (* [visit_abstraction] initializes an enriched environment using the
     auxiliary function [abstraction]. *)

  method private visit_abstraction: 'env 'p1 'p2 .
    ('env penv -> 'p1 -> 'p2) ->
    'env -> 'p1 abstraction -> 'p2 abstraction
  = fun visit_p env p1 ->
      visit_p (abstraction env) p1

  (* In [Extend] mode, [binder] extends the environment via a call to the
     virtual method [extend]. In [Lookup] mode, it uses the virtual method
     [lookup] instead, because (presumably) the environment has been extended
     already with this name. *)

  method private visit_binder:
    _ ->
    'env penv -> 'bn1 binder -> 'bn2 binder
  = fun _ penv x1 ->
      let env = !(penv.current) in
      match penv.at_binder with
      | Extend ->
          let x2, env = self#extend x1 env in
          penv.current := env;
          x2
      | Lookup ->
186
          self#lookup env x1
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269

  (* [inner(p)] can be viewed as sugar for [rebind(outer(p))]. Therefore, this
     code should ideally be generated. *)

  method private visit_inner: 'env 't1 't2 .
    ('env -> 't1 -> 't2) ->
    'env penv -> 't1 inner -> 't2 inner
  = fun visit_t penv t1 ->
      self#visit_rebind (self#visit_outer visit_t) penv t1

  (* In the [Visit] mode, an [outer] subterm is visited using the [outer]
     component of the enriched environment. In [DoNotVisit] mode, it must NOT
     be visited at all. This mode is used only in the discovery phase that
     takes place under a [recursive] construct. This discovery phase is
     performed only for its side effect, which is to extend the current
     environment; its result is discarded. Therefore, it is acceptable to
     return a dummy value here. Unfortunately, we must use an unsafe cast in
     order to produce a value of type ['t2]. An alternative would be to call
     [visit_t ... t1] anyway, but that would have the undesired effect of
     causing embedded terms to be visited twice when they appear under
     [recursive]. *)

  method private visit_outer: 'env 't1 't2 .
    ('env -> 't1 -> 't2) ->
    'env penv -> 't1 outer -> 't2 outer
  = fun visit_t penv t1 ->
      match penv.at_outer with
      | Visit ->
          visit_t penv.outer t1
      | DoNotVisit ->
          Obj.magic ()

  (* [visit_abstraction] updates the enriched environment using the auxiliary
     function [rebind]. *)

  method private visit_rebind: 'env 'p1 'p2 .
    ('env penv -> 'p1 -> 'p2) ->
    'env penv -> 'p1 rebind -> 'p2 rebind
  = fun visit_p penv p1 ->
      visit_p (rebind penv) p1

  (* A [recursive] is construct is visited in two successive phases. In the
     first phase, we use [Extend/DoNotVisit] mode, which means that the
     [current] component of the enriched environment is extended, but nothing
     else happens. The result of this phase is discarded. (It MUST be
     discarded, as we have used unsafe casts to build it.) In the second
     phase, we use [Lookup/Visit] mode, which means that the environment must
     not extended (it has been extended already). If a [binder] is encountered
     during this phase, the environment is looked up. If an embedded term is
     encountered during this phase, it is visited. *)

  method private visit_recursive: 'env 'p1 'p2 .
    ('env penv -> 'p1 -> 'p2) ->
    'env penv -> 'p1 recursive -> 'p2 recursive
  = fun visit_p penv p1 ->
      check_recursive_permitted penv;
      let _ = visit_p { penv with at_outer  = DoNotVisit } p1 in
              visit_p { penv with at_binder = Lookup     } p1

  (* A [repeat] construct causes a switch to [Lookup] mode. *)

  method private visit_repeat: 'env 'p1 'p2 .
    ('env penv -> 'p1 -> 'p2) ->
    'env penv -> 'p1 repeat -> 'p2 repeat
  = fun visit_p penv p1 ->
      let penv = { penv with at_binder = Lookup } in
      visit_p penv p1

  (* [bind(p, t)] is sugar for [abstraction (p * rebind(outer(t)))].
     Therefore, the following code should ideally be generated. We write it by
     hand in a slightly simpler form, where [visit_abstraction] is inlined. *)

  method private visit_bind: 'env 'p1 'p2 't1 't2 .
    ('env penv -> 'p1 -> 'p2) ->
    ('env -> 't1 -> 't2) ->
    'env -> ('p1, 't1) bind -> ('p2, 't2) bind
  = fun visit_p visit_t env (p1, t1) ->
      let penv = abstraction env in
      let p2 = visit_p penv p1 in
      let t2 = self#visit_inner visit_t penv t1 in
      p2, t2

end
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 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 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348

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

(* [iter] *)

(* This is like [map], only simpler. The [lookup] method is not required, as
   it would have result type [unit]. (And, presumably, would perform no side
   effect.) We simply remove it. The [extend] method returns an environment
   only. The implementation of [visit_outer] does not require an unsafe cast. *)

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

  method private virtual extend: 'bn -> 'env -> 'env

  method private visit_abstraction: 'env 'p .
    ('env penv -> 'p -> unit) ->
    'env -> 'p abstraction -> unit
  = fun visit_p env p ->
      visit_p (abstraction env) p

  method private visit_binder:
    _ ->
    'env penv -> 'bn binder -> unit
  = fun _ penv x ->
      let env = !(penv.current) in
      match penv.at_binder with
      | Extend ->
          let env = self#extend x env in
          penv.current := env
      | Lookup ->
          ()

  method private visit_inner: 'env 't .
    ('env -> 't -> unit) ->
    'env penv -> 't inner -> unit
  = fun visit_t penv t ->
      self#visit_rebind (self#visit_outer visit_t) penv t

  method private visit_outer: 'env 't .
    ('env -> 't -> unit) ->
    'env penv -> 't outer -> unit
  = fun visit_t penv t ->
      match penv.at_outer with
      | Visit ->
          visit_t penv.outer t
      | DoNotVisit ->
          ()

  method private visit_rebind: 'env 'p .
    ('env penv -> 'p -> unit) ->
    'env penv -> 'p rebind -> unit
  = fun visit_p penv p ->
      visit_p (rebind penv) p

  method private visit_recursive: 'env 'p .
    ('env penv -> 'p -> unit) ->
    'env penv -> 'p recursive -> unit
  = fun visit_p penv p ->
      check_recursive_permitted penv;
      let _ = visit_p { penv with at_outer  = DoNotVisit } p in
              visit_p { penv with at_binder = Lookup     } p

  method private visit_repeat: 'env 'p .
    ('env penv -> 'p -> unit) ->
    'env penv -> 'p repeat -> unit
  = fun visit_p penv p ->
      let penv = { penv with at_binder = Lookup } in
      visit_p penv p

  method private visit_bind: 'env 'p 't .
    ('env penv -> 'p -> unit) ->
    ('env -> 't -> unit) ->
    'env -> ('p, 't) bind -> unit
  = fun visit_p visit_t env (p, t) ->
      let penv = abstraction env in
      visit_p penv p;
      self#visit_inner visit_t penv t

end