KitSubst.ml 2.04 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3
(* This kit serves to construct a [subst] function for terms -- a function
   that substitutes things (possibly terms) for atoms. *)

POTTIER Francois's avatar
POTTIER Francois committed
4 5
(* An environment is a map of atoms to things. We require every binder [x]
   encountered along the way to be fresh with respect to [env]. *)
POTTIER Francois's avatar
POTTIER Francois committed
6

POTTIER Francois's avatar
POTTIER Francois committed
7 8
type 'thing env =
  'thing Atom.Map.t
POTTIER Francois's avatar
POTTIER Francois committed
9

10
let extend env x =
POTTIER Francois's avatar
POTTIER Francois committed
11
  (* We would like to check that [x] is fresh for [env], but can only
POTTIER Francois's avatar
POTTIER Francois committed
12 13
     perform the domain check. The codomain check cannot be performed
     since the type of things is abstract here. *)
POTTIER Francois's avatar
POTTIER Francois committed
14 15
  assert (not (Atom.Map.mem x env));
  (* Since [x] is fresh for [env], no capture is possible. Thus, no
POTTIER Francois's avatar
POTTIER Francois committed
16
     freshening of the bound name is required. Thus, we can keep the
POTTIER Francois's avatar
POTTIER Francois committed
17
     substitution [env], unchanged, under the binder. *)
18
  env, x
POTTIER Francois's avatar
POTTIER Francois committed
19

20 21 22 23 24 25
let lookup env x =
  try
    Atom.Map.find x env
  with Not_found ->
    assert false

POTTIER Francois's avatar
POTTIER Francois committed
26 27
class ['self] map = object (_ : 'self)
  method private extend = extend
28
  method private lookup = lookup
29 30 31 32 33 34 35 36
  (* [visit_'fn] must be implemented. There could be several kinds of
     nodes that carry variables of type ['fn], say, [FooVar] and [BarVar],
     and the user may decide to substitute away [FooVar] nodes, but leave
     [BarVar] nodes untouched. Another reason is, in an encoding of ML
     disjunction patterns where a bound name can appear several times,
     things may be set up so that [visit_'bn] is called at the first
     occurrence and [visit_'fn] is called at subsequent occurrences. *)
  method private visit_'fn _env x = x
POTTIER Francois's avatar
POTTIER Francois committed
37 38
end

POTTIER Francois's avatar
POTTIER Francois committed
39
let apply (copy : 'thing -> 'thing)
POTTIER Francois's avatar
POTTIER Francois committed
40
          (env : 'thing env)
POTTIER Francois's avatar
POTTIER Francois committed
41 42
          (this : 'thing) (x : Atom.t)
: 'thing =
POTTIER Francois's avatar
POTTIER Francois committed
43
  match Atom.Map.find x env with
POTTIER Francois's avatar
POTTIER Francois committed
44
  | u ->
POTTIER Francois's avatar
POTTIER Francois committed
45 46 47
      (* Possibly copy the term that is grafted, so as to maintain global
         uniqueness. The client controls which [copy] operation should be
         used here. *)
POTTIER Francois's avatar
POTTIER Francois committed
48 49
      copy u
  | exception Not_found ->
POTTIER Francois's avatar
POTTIER Francois committed
50 51 52
      (* [x] is not affected by the substitution, so the original thing is
         returned. [this] should be [Var x], where [Var] is the constructor
         for variables in the syntax of things. *)
POTTIER Francois's avatar
POTTIER Francois committed
53
      this