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 i = f a (D.TLRef (a, i))
43 let mk_gref f a uri = f a (D.TGRef (a, uri))
45 let get err f e i = match D.get e i with
46 | _, _, D.Void -> err ()
47 | _, a, _ -> mk_lref f a i
49 let resolve_gref err f st id =
51 let a, uri = KH.find henv id in f a 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 a = E.node_attrs ~main:(h, 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 a tt = f a (D.TCast (a, 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 a tt = f a (D.TAppl (a, 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 a tt = f a (D.TProj (a, 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 E.empty_node st.ext vv e in
94 xlate_term f st lenv v
96 let f e a tt = f a (D.TProj (a, 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 a b lenv = D.push_bind (f lenv) a b e in
103 let f a b = D.push_bind (f a b) a b lenv in
105 | T.Abst (n, id, r, w) ->
107 let a = {a with E.n_name = name_of_id ~r id} in
108 f a (D.Abst (false, n, ww))
110 xlate_term f st lenv w
113 let a = {a with E.n_name = name_of_id id} in
116 xlate_term f st lenv v
118 let a = E.node_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
157 print_newline (); CrgOutput.pp_term print_string tt;
159 let na = {na with E.n_apix = st.line} in
160 KH.add henv id (na, uri);
161 let meta, b = mk_contents main kind tt 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
167 xlate_term g st D.empty_lenv t
171 (* Interface functions ******************************************************)
173 let initial_status () =
175 path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
178 let refresh_status st = {st with
179 mk_uri = G.get_mk_uri ()
182 let crg_of_txt = xlate_entity