(* qualified identifier: uri, name, qualifiers *)
type qid = M.uri * M.id * M.id list
-type environment = M.pars H.t
-
type context_node = qid option (* context node: None = root *)
type status = {
- henv: environment; (* optimized global environment *)
path: M.id list; (* current section path *)
- hcnt: environment; (* optimized context *)
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
+let henv = H.create henv_size (* optimized global environment *)
+
+let hcnt = H.create hcnt_size (* optimized context *)
+
(* Internal functions *******************************************************)
-let initial_status cover = {
+let initial_status cover =
+ H.clear henv; H.clear hcnt; {
path = []; node = None; nodes = []; line = 1; cover = cover;
- henv = H.create henv_size; hcnt = H.create hcnt_size
}
let id_of_name (id, _, _) = id
resolve_lref f st l lenv id
let resolve_gref f st qid =
- try let args = H.find st.henv (uri_of_qid qid) in f qid (Some args)
+ try let args = H.find henv (uri_of_qid qid) in f qid (Some args)
with Not_found -> f qid None
let resolve_gref_relaxed f st qid =
+(* this is not tail recursive *)
let rec g qid = function
| None -> relax_qid (resolve_gref g st) st qid
| Some args -> f qid args
let get_pars f st = function
| None -> f [] None
| Some qid as node ->
- try let pars = H.find st.hcnt (uri_of_qid qid) in f pars None
+ try let pars = H.find hcnt (uri_of_qid qid) in f pars None
with Not_found -> f [] (Some node)
let get_pars_relaxed f st =
+(* this is not tail recursive *)
let rec g pars = function
| None -> f pars
| Some node -> relax_opt_qid (get_pars g st) st node
in
get_pars g st st.node
+(* this is not tail recursive on the GRef branch *)
let rec xlate_term f st lenv = function
| A.Sort sort ->
f (M.Sort sort)
let f qid =
let f pars =
let f ww =
- H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars);
+ H.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
err {st with node = Some qid}
in
xlate_term f st pars w
let f pars =
let f qid =
let f ww =
- H.add st.henv (uri_of_qid qid) pars;
+ H.add henv (uri_of_qid qid) pars;
let a = [Y.Mark st.line] in
let entry = pars, ww, None in
let entity = a, uri_of_qid qid, Y.Abst entry in
let f pars =
let f qid =
let f ww vv =
- H.add st.henv (uri_of_qid qid) pars;
+ H.add henv (uri_of_qid qid) pars;
let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
let entry = pars, ww, Some vv in
let entity = a, uri_of_qid qid, Y.Abbr entry in