the commit continues

computing the "ages" in the Automath component rather than in the brg kernel

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 548e1ec73ad7094f60d9455d3cf960ab5ae75db1..dfd51aa47d0e3392c67a6802dcc1b2e091bdd7ae 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -30,7 +30,7 @@ type status = {
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
    line: int;                (* line number *)
-   mk_uri:G.uri_generator    (* uri generator *) 
+   mk_uri: G.uri_generator;  (* uri generator *) 
 }
 
 type resolver = Local of int
@@ -138,14 +138,15 @@ let rec xlate_term f st lenv = function
       in
       let map2 f t = xlate_term f st lenv t in
       let g qid (a, _) =
-         let gref = D.TGRef ([], uri_of_qid qid) in
+         let gref age = D.TGRef ([age], uri_of_qid qid) in
         match args, a with
-           | [], [] -> f gref
-           | _      ->
-              let f args = f (D.TAppl ([], args, gref)) in
+           | [], [age]    -> f (gref age)
+           | _ , age :: a ->
+              let f args = f (D.TAppl ([], args, gref age)) in
               let f args = C.list_rev_map f map2 args in
               let f a = C.list_rev_map_append f map1 a ~tail:args in
               C.list_sub_strict f a args
+            | _             -> assert false
       in
       let g qid = resolve_gref_relaxed g st qid in
       let err () = complete_qid g st name in
@@ -184,7 +185,8 @@ let xlate_entity err f st = function
          let lenv = lenv_of_cnt cnt in
         let f qid = 
             let f ww =
-               K.add henv (uri_of_qid qid) cnt;
+               let age = E.Apix st.line in
+               K.add henv (uri_of_qid qid) (age :: a, ws);
               let t = match ws with
                  | [] -> ww
                  | _  -> D.TBind (a, D.Abst (N.infinite, ws), ww)
@@ -193,7 +195,7 @@ let xlate_entity err f st = function
            print_newline (); CrgOutput.pp_term print_string t;
 *)
               let b = E.Abst (N.infinite, t) in
-              let entity = [E.Mark st.line], uri_of_qid qid, b in
+              let entity = [age], uri_of_qid qid, b in
               f {st with line = succ st.line} entity
            in
            xlate_term f st lenv w
@@ -208,7 +210,8 @@ let xlate_entity err f st = function
          let f qid = 
             let f ww =
               let f vv =
-                  K.add henv (uri_of_qid qid) cnt;
+                  let age = E.Apix st.line in
+                  K.add henv (uri_of_qid qid) (age :: a, ws);
                   let t = match ws with
                     | [] -> D.TCast ([], ww, vv)
                     | _  -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
@@ -217,7 +220,7 @@ let xlate_entity err f st = function
            print_newline (); CrgOutput.pp_term print_string t;
 *)
                  let b = E.Abbr t in
-                 let a = E.Mark st.line :: if trans then [] else [E.Meta [E.Private]] in
+                 let a = age :: if trans then [] else [E.Meta [E.Private]] in
                  let entity = a, uri_of_qid qid, b in
                  f {st with line = succ st.line} entity
               in

diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml
index 0b1f1da178df5d7f61233369befb09afbd6bbda1..d2daed49a26fc96820331ea5416ebf5de3082a5b 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgEnvironment.ml
+++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml
@@ -12,23 +12,15 @@
 module U = NUri
 module K = U.UriHash
 module E = Entity
-module B = Brg
 
 let hsize = 7000 
 let env = K.create hsize
 
-(* Internal functions *******************************************************)
-
-let get_age = 
-   let age = ref 0 in
-   fun () -> incr age; !age
-
 (* Interface functions ******************************************************)
 
 (* decps *)
-let set_entity (a, uri, b) =
-   let age = get_age () in
-   let entity = (E.Apix age :: a), uri, b in
+let set_entity entity =
+   let _, uri, _ = entity in
    K.add env uri entity; entity
 
 let get_entity uri =