Unbound.ml 2.88 KB
Newer Older
1 2 3 4 5 6
(*
type mode =
  | ModeOutsideRec (* [inner] component is irrelevant; embedded subterms cannot be marked [inner] *)
  | ModeRec1       (* [inner] and [outer] components both irrelevant; embedded subterms not visited *)
  | ModeRec2       (* [inner] and [outer] components both relevant; embedded subterms visited *)
 *)
7

8 9 10 11
type ('env, 'extra) penv = {
    current: 'env ref; (* threaded left to right *)
    extra: 'extra;
  }
12

13 14 15 16 17 18 19
type 'env outside_rec_penv =
  ('env, 'env) penv (* [extra] is outer env *)

type 'p abstraction =
  'p

type 't outer =
20 21 22 23 24
  't

type ('p, 't) rebind =
  'p * 't

25 26
(*
type 't inner =
27 28
  't

29 30 31 32
type 'p recursive =
  'p
 *)

33 34 35 36
class virtual ['self] map = object (self : 'self)

  method private virtual extend: 'bn1 -> 'env -> 'bn2 * 'env

37 38 39 40 41 42
  method private visit_abstraction: 'p1 'p2 .
    ('env outside_rec_penv -> 'p1 -> 'p2) ->
    'env -> 'p1 abstraction -> 'p2 abstraction
  = fun visit_p env p1 ->
      let penv = { current = ref env; extra = env } in
      visit_p penv p1
43 44 45

  method private visit_outer: 't1 't2 .
    ('env -> 't1 -> 't2) ->
46 47 48 49 50 51 52 53 54 55 56 57
    ('env, 'env) penv -> 't1 outer -> 't2 outer
  = fun visit_t penv t1 ->
      let env = penv.extra in
      visit_t env t1

  method private visit_'bn: 'extra .
    ('env, 'extra) penv -> 'bn1 -> 'bn2
  = fun penv x1 ->
      let env = !(penv.current) in
      let x2, env = self#extend x1 env in
      penv.current := env;
      x2
58

59 60 61 62 63 64 65 66 67 68 69 70 71
  method private visit_rebind: 'p1 'p2 'q1 'q2 .
    ('env outside_rec_penv -> 'p1 -> 'p2) ->
    ('env outside_rec_penv -> 'q1 -> 'q2) ->
    'env outside_rec_penv -> ('p1, 'q1) rebind -> ('p2, 'q2) rebind
  = fun visit_p visit_q penv (p1, q1) ->
      let p2 = visit_p penv p1 in
      (* Copy [current] into [outer]. This changes the meaning of [outer]
         in the right-hand side of [rebind]. *)
      let penv = { penv with extra = !(penv.current) } in
      let q2 = visit_q penv q1 in
      p2, q2

(*
72 73 74 75 76 77
  method private visit_inner: 't1 't2 .
    ('env -> 't1 -> 't2) ->
    'env patenv -> 't1 inner -> 't2 inner
  = fun visit_t patenv t1 ->
      match patenv with
      | ModeNormal r ->
78 79
          (* [inner] outside of [rec] does not make sense. *)
          assert false
80

81 82 83
 *)
(*
  method private visit_recursive: 'p1 'p2 .
84
    ('env patenv -> 'p1 -> 'p2) ->
85 86 87 88 89 90 91 92
    'env patenv -> 'p1 recursive -> 'p2 recursive
  = fun visit_p patenv p1 ->
      match patenv with
      | ModeNormal r ->
          let patenv = ModeRecPhase1 { current = r.current } in
          visit_p patenv p1;
          let inner = patenv.current in
          let patenv = ModeRecPhase2 { current = r.current
93
 *)
94

95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
end

(*
type 'bn pat =
  | PZero
  | POne
  | PVar of 'bn
  | PTuple of 'bn pat list
  | PConj of 'bn pat * 'bn pat
  | PDisj of 'bn pat * 'bn pat

and ('bn, 'fn) expr =
  | EVar of 'fn
  | EAdd of ('bn, 'fn) expr * ('bn, 'fn) expr
  | ELet of ('bn pat, ('bn, 'fn) expr) bind

[@@deriving visitors { variety = "map"; ancestors = ["libmap"] }]
 *)