From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 10 Nov 2014 19:22:34 +0000 (+0000)
Subject: the commit continues
X-Git-Tag: make_still_working~800
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9861cbe2be2023fe6c183747eb5d8f2b56d82ba;p=helm.git

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 548e1ec73..dfd51aa47 100644
--- 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 0b1f1da17..d2daed49a 100644
--- 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 =