From: Ferruccio Guidi 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 =