V_______________________________________________________________ *)
module U = NUri
-module H = U.UriHash
+module H = Hierarchy
module C = Cps
module Y = Entity
module T = Txt
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)
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
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
projects / helm.git / blobdiff