2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
22 path : T.id list; (* current section path *)
23 line : int; (* line number *)
24 sort : int; (* first default sort index *)
25 mk_uri: G.uri_generator (* uri generator *)
28 let henv_size = 7000 (* hash tables initial size *)
30 let henv = Hashtbl.create henv_size (* optimized global environment *)
32 (* Internal functions *******************************************************)
34 let name_of_id ?(r=true) id = E.Name (id, r)
36 let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
38 let mk_gref f uri = f (D.TGRef ([], uri))
40 let uri_of_id st id path =
41 let str = String.concat "/" path in
42 let str = Filename.concat str id in
43 let str = st.mk_uri str in
46 let resolve_gref err f st id =
47 try f (Hashtbl.find henv id)
48 with Not_found -> err ()
50 let rec xlate_term f st lenv = function
52 | T.Impl _ -> assert false
56 let f h = f (D.TSort ([], h)) in
57 H.sort_of_string C.err f id
59 D.get_index C.err (mk_lref f i j) i j lenv
61 let err () = resolve_gref C.err (mk_gref f) st id in
62 D.resolve_lref err (mk_lref f) id lenv
64 let f uu tt = f (D.TCast ([], uu, tt)) in
65 let f uu = xlate_term (f uu) st lenv t in
66 xlate_term f st lenv u
68 let map f = xlate_term f st lenv in
69 let f vvs tt = f (D.TAppl ([], vvs, tt)) in
70 let f vvs = xlate_term (f vvs) st lenv t in
73 let abst_map (lenv, a, wws) (id, r, w) =
74 let attr = name_of_id ~r id in
75 let ww = xlate_term C.start st lenv w in
76 D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
78 let abbr_map (lenv, a, wws) (id, w) =
79 let attr = name_of_id id in
80 let ww = xlate_term C.start st lenv w in
81 D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
83 let void_map (lenv, a, n) id =
84 let attr = name_of_id id in
85 D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
87 let lenv, aa, bb = match b with
89 let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
90 let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
91 lenv, aa, D.Abst (n, wws)
93 let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
94 let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
97 let lenv = D.push_bind C.start lenv [] (D.Void 0) in
98 let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
101 let f tt = f (D.TBind (aa, bb, tt)) in
102 xlate_term f st lenv t
104 let xlate_term f st lenv t =
105 TT.contract (xlate_term f st lenv) t
107 let mk_contents n tt = function
108 | T.Decl -> [] , E.Abst (n, tt)
109 | T.Ax -> [E.InProp] , E.Abst (n, tt)
110 | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
111 | T.Def -> [] , E.Abbr tt
112 | T.Th -> [E.InProp] , E.Abbr tt
114 let xlate_entity err f gen st = function
117 | T.Section (Some name) ->
118 err {st with path = name :: st.path}
120 begin match st.path with
122 err {st with path = ptl}
126 let map st (xix, s) =
127 let ix = match xix with
131 {st with sort = H.set_sorts ix [s]}
133 err (List.fold_left map st sorts)
135 assert (H.set_graph id); err st
136 | T.Entity (main, kind, n, id, info, t) ->
137 let uri = uri_of_id st id st.path in
138 Hashtbl.add henv id uri;
139 let tt = xlate_term C.start st D.empty_lenv t in
141 print_newline (); CrgOutput.pp_term print_string tt;
144 let ms, b = mk_contents n tt kind in
145 let ms = if main then E.Main :: ms else ms in
146 let a = if ms <> [] then E.Meta ms :: a else a in
147 let a = if info <> ("", "") then E.Info info :: a else a in
148 let entity = E.Mark st.line :: a, uri, b in
149 f {st with line = succ st.line} entity
153 (* Interface functions ******************************************************)
155 let initial_status () =
156 Hashtbl.clear henv; {
157 path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
160 let refresh_status st = {st with
161 mk_uri = G.get_mk_uri ()
164 let crg_of_txt = xlate_entity