1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (***************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
34 (***************************************************************************)
38 module UM = UriManager
41 module E = CicEnvironment
42 module TC = CicTypeChecker
45 let mpres_document pres_box =
46 Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
48 let mml_of_cic_sequent metasenv sequent =
49 let unsh_sequent,(asequent,ids_to_terms,
50 ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
52 Cic2acic.asequent_of_sequent metasenv sequent
54 let content_sequent = Acic2content.map_sequent asequent in
56 Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
57 let xmlpres = mpres_document pres_sequent in
58 (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
61 (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
63 let mml_of_cic_object obj =
64 let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
65 ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
67 Cic2acic.acic_object_of_cic_object obj
70 Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
72 let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
73 let xmlpres = mpres_document pres in
74 let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
76 (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
77 ids_to_inner_sorts,ids_to_inner_types)))
79 let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
80 let unsh_sequent,(asequent,ids_to_terms,
81 ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
83 Cic2acic.asequent_of_sequent metasenv sequent
85 let content_sequent = Acic2content.map_sequent asequent in
87 CicNotationPres.mpres_of_box
88 (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
90 BoxPp.render_to_string ~map_unicode_to_tex
91 (function x::_ -> x | _ -> assert false) size pres_sequent
93 let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
95 let _,(asequent,_,_,ids_to_inner_sorts,_) =
96 Cic2acic.asequent_of_sequent metasenv sequent
98 let _,_,_,t = Acic2content.map_sequent asequent in
100 TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
101 let t = TermContentPres.pp_ast t in
102 let t = CicNotationPres.render ids_to_uris t in
103 BoxPp.render_to_string ~map_unicode_to_tex
104 (function x::_ -> x | _ -> assert false) size t
106 let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
107 let fake_sequent = (-1,context,t) in
108 txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
109 metasenv fake_sequent
113 CicMetaSubst.set_ppterm_in_context
114 (fun ~metasenv subst term context ->
116 let context' = CicMetaSubst.apply_subst_context subst context in
117 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
118 let term' = CicMetaSubst.apply_subst subst term in
121 ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
122 30 metasenv context' term' in
123 if String.contains res '\n' then
128 Sys.Break as exn -> raise exn
130 "[[ Exception raised during pretty-printing: " ^
132 Printexc.to_string exn
134 Sys.Break as exn -> raise exn
135 | _ -> "<<exception raised pretty-printing the exception>>"
137 (CicMetaSubst.use_low_level_ppterm_in_context := true;
140 CicMetaSubst.ppterm_in_context ~metasenv subst term context
142 CicMetaSubst.use_low_level_ppterm_in_context := false;
146 CicMetaSubst.use_low_level_ppterm_in_context := false;
150 (****************************************************************************)
151 (* txt_of_cic_object: IMPROVE ME *)
153 let remove_closed_substs s =
154 Pcre.replace ~pat:"{...}" ~templ:"" s
156 let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm =
157 let ast, ids_to_uris =
158 TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
160 CicNotationPres.box_of_mpres (
161 CicNotationPres.render ~prec:90 ids_to_uris
162 (TermContentPres.pp_ast ast)) in
163 let render = function _::x::_ -> x | _ -> assert false in
164 let mpres = CicNotationPres.mpres_of_box bobj in
165 let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
166 remove_closed_substs s
168 let txt_of_cic_object
169 ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
170 n style ?flavour prefix obj
174 let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
175 Cic2acic.acic_object_of_cic_object obj
177 aobj, ids_to_inner_sorts, ids_to_inner_types
179 | E.Object_not_found uri ->
180 let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
183 let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
188 let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
190 Acic2content.annobj2content
191 ids_to_inner_sorts ids_to_inner_types aobj
194 Content2pres.content2pres
195 ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj
197 remove_closed_substs ("\n\n" ^
198 BoxPp.render_to_string ~map_unicode_to_tex
199 (function _::x::_ -> x | _ -> assert false) n
200 (CicNotationPres.mpres_of_box bobj)
202 | G.Procedural depth ->
203 let obj = ProceduralOptimizer.optimize_obj obj in
204 let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
205 let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
206 let lazy_term_pp = term_pp in
207 let obj_pp = CicNotationPp.pp_obj term_pp in
208 let aux = GrafiteAstPp.pp_statement
209 ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
211 Acic2Procedural.procedural_of_acic_object
212 ~ids_to_inner_sorts ~ids_to_inner_types
213 ?depth ?flavour prefix aobj
215 "\n\n" ^ String.concat "" (List.map aux script)
217 let cic_prefix = Str.regexp_string "cic:/"
219 let matita_prefix = Str.regexp_string "cic:/matita/"
221 let discharge_uri style uri =
222 let template = match style with
223 | G.Declarative -> "cic:/matita/declarative/"
224 | G.Procedural _ -> "cic:/matita/procedural/"
226 let s = UM.string_of_uri uri in
227 if Str.string_match matita_prefix s 0 then uri else
228 let s = Str.replace_first cic_prefix template s in
231 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
232 let print_exc = function
233 | ProofEngineHelpers.Bad_pattern s as e ->
234 Printexc.to_string e ^ " " ^ Lazy.force s
235 | e -> Printexc.to_string e
237 let dbd = LibraryDb.instance () in
238 let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
241 (* FG: for now the explicit variables must be discharged *)
242 let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
243 match CicDischarge.discharge_uri (discharge_uri style) uri with
244 | C.InductiveDefinition _ as obj', false ->
245 let uri' = discharge_uri style uri in
246 TC.typecheck_obj uri' obj';
247 (* we loose the sharing in this case *)
248 let obj'', _ = E.get_obj Un.default_ugraph uri' in
249 let s = do_it obj'' in begin E.remove_obj uri'; s end
250 | obj, _ -> do_it obj
255 "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s"
256 (UM.string_of_uri uri) (print_exc e)
258 Printf.eprintf "%s\n" msg;
259 GrafiteTypes.command_error msg
261 String.concat "" (List.map map sorted_uris)
263 let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
265 if Librarian.is_uri name then name else
267 Helm_registry.get_list Helm_registry.string "matita.includes"
269 let _, baseuri, _, _ =
270 Librarian.baseuri_of_script ~include_paths name
274 txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri
276 (****************************************************************************)
277 (* procedural_txt_of_cic_term *)
279 let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
280 let annterm, ids_to_inner_sorts, ids_to_inner_types =
281 try Cic2acic.acic_term_of_cic_term context term
283 let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
286 let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
287 let lazy_term_pp = term_pp in
288 let obj_pp = CicNotationPp.pp_obj term_pp in
289 let aux = GrafiteAstPp.pp_statement
290 ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
292 Acic2Procedural.procedural_of_acic_term
293 ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
295 String.concat "" (List.map aux script)