KitExport.ml 1.52 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
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
(* This kit serves to construct an [export] function for terms, that is, a
   function that transforms atoms back to strings. *)

(* The environment is an injective mapping of atoms to strings. We keep track
   of its codomain by recording a mapping of hints to integers. *)

module StringMap =
  Map.Make(String)

type env = {
  graph: string Atom.Map.t;
  codomain: int StringMap.t;
}

let empty = {
  graph = Atom.Map.empty;
  codomain = StringMap.empty;
}

let next env hint : int =
  try
    StringMap.find hint env.codomain
  with Not_found ->
    0

26
let extend env x =
POTTIER Francois's avatar
POTTIER Francois committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
  (* We must pick a suitable string to stand for the atom [x]. We must
     pick a string that does not appear in the image through [env] of
     the free atoms of [body]. However, at this point, we do not have
     access to the free atoms of [body], so we must pick a string [s]
     that does not appear in the codomain of [env]. *)
  let hint = Atom.hint x in
  let i = next env hint in
  let s =
    if i = 0 then hint (* a cosmetic detail *)
    else Printf.sprintf "%s%d" hint i
  in
  let env = {
    graph = Atom.Map.add x s env.graph;
    codomain = StringMap.add hint (i+1) env.codomain;
  } in
42
  env, s
POTTIER Francois's avatar
POTTIER Francois committed
43 44 45 46 47 48 49

let lookup env a =
  try
    Atom.Map.find a env.graph
  with Not_found ->
    (* The atom [a] must be in the domain of [env]. *)
    assert false
50
      (* Instead of failing, we could also log an error and return "?". *)
POTTIER Francois's avatar
POTTIER Francois committed
51 52 53

class ['self] map = object (_ : 'self)
  method private extend = extend
54
  method private lookup = lookup
POTTIER Francois's avatar
POTTIER Francois committed
55 56
  method private visit_'fn = lookup
end