type context_node = M.qid option (* context node: None = root *)
type status = {
- genv: M.environment; (* global environment *)
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 *)
explicit: bool (* need explicit context root? *)
}
let hsize = 11 (* hash tables initial size *)
+(* Internal functions *******************************************************)
+
let initial_status size = {
- genv = []; path = []; node = None; nodes = []; explicit = true;
+ path = []; node = None; nodes = []; line = 1; explicit = true;
henv = H.create size; hcnt = H.create size
}
| None -> f None
| Some qid -> let f qid = f (Some qid) in relax_qid f qid
-let resolve_gref f st lenv gref =
+let resolve_gref f st local lenv gref =
let rec get_local f i = function
| [] -> f None
| (name, _) :: _ when fst name = fst gref -> f (Some i)
| Some i -> f gref (Some (Local i))
| None -> get_global g
in
- get_local f 0 lenv
+ if local then get_local f 0 lenv else f None
let resolve_gref_relaxed f st lenv gref =
let rec g gref = function
- | None -> relax_qid (resolve_gref g st lenv) gref
+ | None -> relax_qid (resolve_gref g st false lenv) gref
| Some resolved -> f gref resolved
in
- resolve_gref g st lenv gref
+ resolve_gref g st true lenv gref
let get_pars f st = function
| None -> f [] None
let f name = function
| Local i -> f (M.LRef i)
| Global defs ->
- let map1 f = xlate_term f st lenv in
- let map2 f (name, _) = f (M.GRef (name, [])) in
+ let l = List.length lenv in
+ let map1 f = xlate_term f st lenv in
+ let map2 f (name, _) = f (M.GRef (l, name, [])) in
let f tail =
- let f args = f (M.GRef (name, args)) in
+ let f args = f (M.GRef (l, name, args)) in
let f defs = Cps.list_rev_map_append f map2 defs ~tail in
Cps.list_sub_strict f defs args
in
let xlate_item f st = function
| A.Section (Some name) ->
- f {st with path = name :: st.path; nodes = st.node :: st.nodes}
+ f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
| A.Section None ->
begin match st.path, st.nodes with
| _ :: ptl, nhd :: ntl ->
- f {st with path = ptl; node = nhd; nodes = ntl}
+ f {st with path = ptl; node = nhd; nodes = ntl} None
| _ -> assert false
end
| A.Context None ->
- f {st with node = None}
+ f {st with node = None} None
| A.Context (Some name) ->
- let f name = f {st with node = Some name} in
- complete_qid f st name
+ let f name = f {st with node = Some name} None in
+ complete_qid f st name
| A.Block (name, w) ->
let f name =
let f pars =
let f ww =
H.add st.hcnt name ((name, ww) :: pars);
- f {st with node = Some name}
+ f {st with node = Some name} None
in
xlate_term f st pars w
in
let f pars =
let f name =
let f ww =
- let entry = (pars, name, ww, None) in
+ let entry = (st.line, pars, name, ww, None) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv}
+ f {st with line = succ st.line} (Some entry)
in
xlate_term f st pars w
in
let f pars =
let f name =
let f ww vv =
- let entry = (pars, name, ww, Some (trans, vv)) in
+ let entry = (st.line, pars, name, ww, Some (trans, vv)) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv}
+ f {st with line = succ st.line} (Some entry)
in
let f ww = xlate_term (f ww) st pars v in
xlate_term f st pars w
in
get_pars_relaxed f st
-let meta_of_aut f book =
- let f st = f st.genv in
- Cps.list_fold_left f xlate_item (initial_status hsize) book
+(* Interface functions ******************************************************)
+
+let initial_status = initial_status hsize
+
+let meta_of_aut = xlate_item