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 mk_uri: G.uri_generator (* uri generator *)
31 let henv_size = 7000 (* hash tables initial size *)
33 let henv = KH.create henv_size (* optimized global environment *)
36 Printf.printf "%s\n%!" s; C.err ()
38 (* Internal functions *******************************************************)
40 let mk_lref f a i = f a (D.TLRef (a, i))
42 let mk_gref f a uri = f a (D.TGRef (a, uri))
44 let get err f e i = match D.get e i with
45 | _, _, D.Void -> err ()
46 | _, a, _ -> mk_lref f a i
48 let resolve_gref err f st id =
50 let a, uri = KH.find henv id in f a uri
51 with Not_found -> err ()
53 let name_of_id ?(r=true) id =
54 if id = "" then None else Some (id, r)
56 let uri_of_id st id path =
57 let str = String.concat "/" path in
58 let str = KF.concat str id in
59 let str = st.mk_uri str in
62 let rec xlate_term f st lenv = function
64 CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
68 let a = E.node_attrs ~sort:h () in
71 let f h = xlate_term f st lenv (T.Sort h) in
72 H.sort_of_string (xerr "sort not found") f id
74 get (xerr "index out of bounds") f lenv i
76 let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
77 D.resolve_lref err (mk_lref f) id lenv
79 let f uu a tt = f a (D.TCast (a, uu, tt)) in
80 let f _ uu = xlate_term (f uu) st lenv t in
81 xlate_term f st lenv u
83 let f vv a tt = f a (D.TAppl (a, vv, tt)) in
84 let f _ vv = xlate_term (f vv) st lenv t in
85 xlate_term f st lenv v
87 let f e a tt = f a (D.TProj (a, e, tt)) in
88 let f (lenv, e) = xlate_term (f e) st lenv t in
89 C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
92 let f _ vv = D.push_appl f E.empty_node vv e in
93 xlate_term f st lenv v
95 let f e a tt = f a (D.TProj (a, e, tt)) in
96 let f e = xlate_term (f e) st lenv t in
97 C.list_fold_right f map vs D.empty_lenv
99 and xlate_bind st f (lenv, e) b =
100 let f lenv e = f (lenv, e) in
101 let f a b lenv = D.push_bind (f lenv) a b e in
102 let f a b = D.push_bind (f a b) a b lenv in
104 | T.Abst (n, id, r, w) ->
106 let a = {a with E.n_name = name_of_id ~r id} in
107 f a (D.Abst (false, n, ww))
109 xlate_term f st lenv w
112 let a = {a with E.n_name = name_of_id id} in
115 xlate_term f st lenv v
117 let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
120 let mk_contents main kind tt =
121 let ms, b = match kind with
122 | T.Decl -> [] , E.Abst tt
123 | T.Ax -> [E.InProp] , E.Abst tt
124 | T.Cong -> [E.InProp; E.Progress], E.Abst tt
125 | T.Def -> [] , E.Abbr tt
126 | T.Th -> [E.InProp] , E.Abbr tt
128 if main then E.Main :: ms, b else ms, b
130 let xlate_entity err f gen st = function
133 | T.Section (Some name) ->
134 err {st with path = name :: st.path}
136 begin match st.path with
138 err {st with path = ptl}
142 let map st (xix, s) =
143 let ix = match xix with
147 {st with sort = H.set_sorts ix [s]}
149 err (KL.fold_left map st sorts)
151 assert (H.set_graph id); err st
152 | T.Constant (main, kind, id, info, t) ->
153 let uri = uri_of_id st id st.path in
156 print_newline (); CrgOutput.pp_term print_string tt;
158 let na = {na with E.n_apix = st.line} in
159 KH.add henv id (na, uri);
160 let meta, b = mk_contents main kind tt in
161 let ra = E.root_attrs ~meta ~info () in
162 let entity = ra, na, uri, b in
163 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; 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