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 *)
let initial_status size = {
- genv = []; path = []; node = None; nodes = []; explicit = true;
+ genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
henv = H.create size; hcnt = H.create size
}
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 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 genv = entry :: st.genv; line = succ st.line}
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 genv = entry :: st.genv; line = succ st.line}
in
let f ww = xlate_term (f ww) st pars v in
xlate_term f st pars w