lambda-delta: we added the support for position indexes in global references

[helm.git] / helm / software / lambda-delta / toplevel / metaAut.ml

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 370bf4cfd6cee01bfc68f5c1d78a8f9e248b5060..5b85e46cbea703dd21fafe6f53b7242c6b5025b5 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -39,6 +39,7 @@ type status = {
    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? *)
 }
 
@@ -48,7 +49,7 @@ type resolver = Local of int
 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
 }
 
@@ -133,10 +134,11 @@ let rec xlate_term f st lenv = function
       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
@@ -175,9 +177,9 @@ let xlate_item f st = function
       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
@@ -188,9 +190,9 @@ let xlate_item f st = function
       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