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 *)
let hsize = 11 (* hash tables initial size *)
+(* Internal functions *******************************************************)
+
let initial_status size = {
- genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
+ path = []; node = None; nodes = []; line = 1; explicit = true;
henv = H.create size; hcnt = H.create size
}
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 ww =
let entry = (st.line, pars, name, ww, None) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv; line = succ st.line}
+ f {st with line = succ st.line} (Some entry)
in
xlate_term f st pars w
in
let f ww vv =
let entry = (st.line, pars, name, ww, Some (trans, vv)) in
H.add st.henv name pars;
- f {st with genv = entry :: st.genv; line = succ st.line}
+ 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