\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module H = U.UriHash
-module C = Cps
-module Y = Entity
-module T = Txt
-module D = Crg
+module U = NUri
+module H = Hierarchy
+module C = Cps
+module O = Options
+module Y = Entity
+module T = Txt
+module TT = TxtTxt
+module D = Crg
type status = {
- path: T.id list; (* current section path *)
- line: int; (* line number *)
- mk_uri:Y.uri_generator (* uri generator *)
+ path : T.id list; (* current section path *)
+ line : int; (* line number *)
+ sort : int; (* first default sort index *)
+ mk_uri: O.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
-}
-
-let name_of_id id = Y.Name (id, true)
+let name_of_id ?(r=true) id = Y.Name (id, r)
let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
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 ->
+ | T.Inst _
+ | T.Impl _ -> assert false
+ | 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
- | T.LRef (i, j) ->
+ | T.NSrt 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
+ | T.NRef id ->
+ 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) ->
+ | T.Cast (u, t) ->
let f uu tt = f (D.TCast ([], uu, tt)) in
let f uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
- | T.Appl (vs, t) ->
+ | T.Appl (vs, t) ->
let map f = xlate_term f st lenv in
let f vvs tt = f (D.TAppl ([], vvs, 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
+ | T.Bind (b, t) ->
+ let abst_map (lenv, a, wws) (id, r, w) =
+ let attr = name_of_id ~r 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 abbr_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 void_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, 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 abst_map (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 abbr_map (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 void_map (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 xlate_entity err f st = function
- | T.Section (Some name) ->
+let xlate_term f st lenv t =
+ TT.contract (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 gen st = function
+ | T.Require _ ->
+ err st
+ | 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
+ | T.Generate _ ->
+ err st
(* Interface functions ******************************************************)
-let initial_status mk_uri =
- initial_status mk_uri
+let initial_status () =
+ Hashtbl.clear henv; {
+ path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+ mk_uri = O.get_mk_uri ()
+}
let crg_of_txt = xlate_entity