X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgTxt.ml;h=1cb2b3ee90cde40bddfd7319928a2c9b895908d9;hb=689118326fbe47231865b26c66ae89144459be6a;hp=57e9460702fd37f1a18ac2b2134145fc8f3e4445;hpb=93205dc852fa208b48a05757d05d9910b7d45fa1;p=helm.git diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml index 57e946070..1cb2b3ee9 100644 --- a/helm/software/lambda-delta/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml @@ -10,7 +10,7 @@ V_______________________________________________________________ *) module U = NUri -module H = U.UriHash +module H = Hierarchy module C = Cps module Y = Entity module T = Txt @@ -19,17 +19,18 @@ module D = Crg type status = { path: T.id list; (* current section path *) line: int; (* line number *) + sort: int; (* first default sort index *) mk_uri:Y.uri_generator (* uri generator *) } let henv_size = 7000 (* hash tables initial size *) -let henv = H.create henv_size (* optimized global environment *) +let henv = Hashtbl.create henv_size (* optimized global environment *) (* Internal functions *******************************************************) let initial_status mk_uri = { - path = []; line = 1; mk_uri = mk_uri + path = []; line = 1; sort = 0; mk_uri = mk_uri } let name_of_id id = Y.Name (id, true) @@ -44,29 +45,20 @@ let uri_of_id st id path = let str = st.mk_uri str in U.uri_of_string str -let complete_id f st id = f id st.path - -let resolve_gref st id path = - let uri = uri_of_id st id path in - try H.find henv uri; Some uri - with Not_found -> None - -let rec resolve_gref_relaxed err f st id path = - match resolve_gref st id path, path with - | Some uri, _ -> f uri - | None, _ :: path -> resolve_gref_relaxed err f st id path - | None, [] -> err () +let resolve_gref err f st id = + try f (Hashtbl.find henv id) + with Not_found -> err () let rec xlate_term f st lenv = function | T.Sort h -> f (D.TSort ([], h)) | T.NSrt id -> - let f h = (D.TSort ([], h)) in - Hierarchy.sort_of_string C.err f id + let f h = f (D.TSort ([], h)) in + H.sort_of_string C.err f id | T.LRef (i, j) -> D.get_index C.err (mk_lref f i j) i j lenv | T.NRef id -> - let err () = complete_id (resolve_gref_relaxed C.err (mk_gref f) st) st id in + let err () = resolve_gref C.err (mk_gref f) st id in D.resolve_lref err (mk_lref f) id lenv | T.Cast (u, t) -> let f uu tt = f (D.TCast ([], uu, tt)) in @@ -78,56 +70,67 @@ let rec xlate_term f st lenv = function let f vvs = xlate_term (f vvs) st lenv t in C.list_map f map vs | T.Bind (b, t) -> - let lenv, a, bb = match b with + let map1 (lenv, a, wws) (id, w) = + let attr = name_of_id id in + let ww = xlate_term C.start st lenv w in + D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws + in + let map2 (lenv, a, n) id = + let attr = name_of_id id in + D.push2 C.err C.start lenv attr (), attr :: a, succ n + in + let lenv, aa, bb = match b with | T.Abst xws -> - let map (lenv, a, wws) (id, w) = - let attr = name_of_id id in - let ww = xlate_term C.start st lenv w in - D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws - in let lenv = D.push_bind C.start lenv [] (D.Abst []) in - let lenv, a, wws = List.fold_left map (lenv, [], []) xws in - lenv, a, D.Abst wws + let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in + lenv, aa, D.Abst wws | T.Abbr xvs -> - let map (lenv, a, vvs) (id, v) = - let attr = name_of_id id in - let vv = xlate_term C.start st lenv v in - D.push2 C.err C.start lenv attr ~t:vv (), attr :: a, vv :: vvs - in let lenv = D.push_bind C.start lenv [] (D.Abbr []) in - let lenv, a, vvs = List.fold_left map (lenv, [], []) xvs in - lenv, a, D.Abbr vvs + let lenv, aa, vvs = List.fold_left map1 (lenv, [], []) xvs in + lenv, aa, D.Abbr vvs | T.Void ids -> - let map (lenv, a, n) id = - let attr = name_of_id id in - D.push2 C.err C.start lenv attr (), attr :: a, succ n - in let lenv = D.push_bind C.start lenv [] (D.Void 0) in - let lenv, a, n = List.fold_left map (lenv, [], 0) ids in - lenv, a, D.Void n + let lenv, aa, n = List.fold_left map2 (lenv, [], 0) ids in + lenv, aa, D.Void n in - let f tt = f (D.TBind (a, bb, tt)) in + let f tt = f (D.TBind (aa, bb, tt)) in xlate_term f st lenv t - + +let mk_contents tt = function + | T.Decl -> [], Y.Abst tt + | T.Ax -> [], Y.Abst tt + | T.Def -> [], Y.Abbr tt + | T.Th -> [], Y.Abbr tt let xlate_entity err f st = function - | T.Section (Some name) -> + | T.Section (Some name) -> err {st with path = name :: st.path} - | T.Section None -> + | T.Section None -> begin match st.path with | _ :: ptl -> err {st with path = ptl} - | _ -> assert false + | _ -> assert false end - | T.Global (def, id, meta, t) -> + | T.Sorts sorts -> + let map st (xix, s) = + let ix = match xix with + | None -> st.sort + | Some ix -> ix + in + {st with sort = H.set_sorts ix [s]} + in + err (List.fold_left map st sorts) + | T.Graph id -> + assert (H.set_graph id); err st + | T.Entity (kind, id, meta, t) -> let uri = uri_of_id st id st.path in - H.add henv uri (); + Hashtbl.add henv id uri; let tt = xlate_term C.start st D.empty_lenv t in (* print_newline (); CrgOutput.pp_term print_string tt; *) - let a = if meta <> "" then [Y.Meta meta] else [] in - let b = if def then Y.Abbr tt else Y.Abst tt in + let a, b = mk_contents tt kind in + let a = if meta <> "" then Y.Meta meta :: a else a in let entity = Y.Mark st.line :: a, uri, b in f {st with line = succ st.line} entity