KitImport.ml 777 Bytes
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3
(* This kit serves to construct an [import] function for terms, that is, a
   function that transforms strings to atoms. *)

4 5
(* We map every binding occurrence to a fresh atom, so the term that we
   produce satisfies global uniqueness. *)
POTTIER Francois's avatar
POTTIER Francois committed
6 7 8 9 10 11 12 13 14 15 16

module StringMap =
  Map.Make(String)

type env =
  Atom.t StringMap.t

let empty =
  StringMap.empty

let extend (x : string) (env : env) : Atom.t * env =
17
  let a = Atom.fresh x in
POTTIER Francois's avatar
POTTIER Francois committed
18 19 20 21 22 23 24 25 26 27 28 29
  let env = StringMap.add x a env in
  a, env

exception Unbound of string

let lookup (env : env) (x : string) : Atom.t =
  try
    StringMap.find x env
  with Not_found ->
    raise (Unbound x)

class ['self] map = object (_ : 'self)
30
  method private extend x env = extend x env
31 32
  method private lookup = lookup
  method private visit_'fn = lookup
POTTIER Francois's avatar
POTTIER Francois committed
33
end