module U = NUri
module H = U.UriHash
module C = Cps
+module O = Options
module Y = Entity
module M = Meta
module A = Aut
(* 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 *)
-(* Internal functions *******************************************************)
+let henv = H.create henv_size (* optimized global environment *)
-let initial_status cover = {
- path = []; node = None; nodes = []; line = 1; cover = cover;
- henv = H.create henv_size; hcnt = H.create hcnt_size
-}
+let hcnt = H.create hcnt_size (* optimized context *)
+
+(* Internal functions *******************************************************)
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
(* Interface functions ******************************************************)
-let initial_status ?(cover="") () =
- initial_status cover
+let initial_status () =
+ H.clear henv; H.clear hcnt; {
+ path = []; node = None; nodes = []; line = 1; cover = !O.cover
+}
+
+let refresh_status st = {st with
+ cover = !O.cover
+}
let meta_of_aut = xlate_entity