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_______________________________________________________________ *)
25 path : T.id list; (* current section path *)
26 line : int; (* line number *)
27 sort : int; (* first default sort index *)
28 ext : bool; (* extended applications *)
29 mk_uri: G.uri_generator (* uri generator *)
32 let henv_size = 7000 (* hash tables initial size *)
34 let henv = KH.create henv_size (* optimized global environment *)
37 Printf.printf "%s\n%!" s; C.err ()
39 (* Internal functions *******************************************************)
41 let mk_lref f a y i = f y (D.TLRef (a, i))
43 let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
45 let get err f e i = match D.get e i with
46 | _, _, _, D.Void -> err ()
47 | _, a, y, _ -> mk_lref f a y i
49 let resolve_gref err f st id =
51 let y, uri = KH.find henv id in f y uri
52 with Not_found -> err ()
54 let name_of_id ?(r=true) id =
55 if id = "" then None else Some (id, r)
57 let uri_of_id st id path =
58 let str = String.concat "/" path in
59 let str = KF.concat str id in
60 let str = st.mk_uri str in
63 let rec xlate_term f st lenv = function
65 CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
69 let y = E.bind_attrs ~main:(k, 0) () in
72 let f h = xlate_term f st lenv (T.Sort h) in
73 H.sort_of_string (xerr "sort not found") f id
75 get (xerr "index out of bounds") f lenv i
77 let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
78 D.resolve_lref err (mk_lref f) id lenv
80 let f uu y tt = f y (D.TCast (uu, tt)) in
81 let f _ uu = xlate_term (f uu) st lenv t in
82 xlate_term f st lenv u
84 let f vv y tt = f y (D.TAppl (st.ext, vv, tt)) in
85 let f _ vv = xlate_term (f vv) st lenv t in
86 xlate_term f st lenv v
88 let f e y tt = f y (D.TProj (e, tt)) in
89 let f (lenv, e) = xlate_term (f e) st lenv t in
90 C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
93 let f _ vv = D.push_appl f st.ext vv e in
94 xlate_term f st lenv v
96 let f e y tt = f y (D.TProj (e, tt)) in
97 let f e = xlate_term (f e) st lenv t in
98 C.list_fold_right f map vs D.empty_lenv
100 and xlate_bind st f (lenv, e) b =
101 let f lenv e = f (lenv, e) in
102 let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
103 let f y b = D.push_bind (f y b) E.empty_node y b lenv in
105 | T.Abst (n, id, r, w) ->
107 let y = E.bind_attrs ?name:(name_of_id id) () in
108 f y (D.Abst (false, n, ww))
110 xlate_term f st lenv w
113 let y = E.bind_attrs ?name:(name_of_id id) () in
116 xlate_term f st lenv v
118 let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
121 let mk_contents main kind tt =
122 let ms, b = match kind with
123 | T.Decl -> [] , E.Abst tt
124 | T.Ax -> [E.InProp] , E.Abst tt
125 | T.Cong -> [E.InProp; E.Progress], E.Abst tt
126 | T.Def -> [] , E.Abbr tt
127 | T.Th -> [E.InProp] , E.Abbr tt
129 if main then E.Main :: ms, b else ms, b
131 let xlate_entity err f gen st = function
134 | T.Section (Some name) ->
135 err {st with path = name :: st.path}
137 begin match st.path with
139 err {st with path = ptl}
143 let map st (xix, s) =
144 let ix = match xix with
148 {st with sort = H.set_sorts ix [s]}
150 err (KL.fold_left map st sorts)
152 assert (H.set_graph id); err st
153 | T.Constant (main, kind, id, info, t) ->
154 let uri = uri_of_id st id st.path in
156 KH.add henv id (ya, uri);
158 print_newline (); CrgOutput.pp_term print_string tt;
160 let meta, b = mk_contents main kind tt in
161 let na = E.node_attrs ~apix:st.line () in
162 let ra = E.root_attrs ~meta ~info () in
163 let entity = ra, na, uri, b in
164 f {st with line = succ st.line} entity
166 xlate_term g st D.empty_lenv t
170 (* Interface functions ******************************************************)
172 let initial_status () =
174 path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
177 let refresh_status st = {st with
178 mk_uri = G.get_mk_uri ()
181 let crg_of_txt = xlate_entity