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
44 module GE = GrafiteEngine
45 module LS = LibrarySync
46 module Ds = CicDischarge
47 module PO = ProceduralOptimizer
48 module N = CicNotationPt
49 module A2P = Acic2Procedural
51 let mpres_document pres_box =
52 Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
54 let mml_of_cic_sequent metasenv sequent =
55 let unsh_sequent,(asequent,ids_to_terms,
56 ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
58 Cic2acic.asequent_of_sequent metasenv sequent
60 let content_sequent = Acic2content.map_sequent asequent in
62 Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
63 let xmlpres = mpres_document pres_sequent in
64 (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
67 (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
69 let nmml_of_cic_sequent status metasenv subst sequent =
70 let content_sequent,ids_to_refs =
71 NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in
73 Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
74 let xmlpres = mpres_document pres_sequent in
75 Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
77 let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent =
78 let content_sequent,ids_to_refs =
79 NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in
81 Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
82 let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
83 BoxPp.render_to_string ~map_unicode_to_tex
84 (function x::_ -> x | _ -> assert false) size pres_sequent
86 let mml_of_cic_object obj =
87 let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
88 ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
90 Cic2acic.acic_object_of_cic_object obj
93 Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
95 let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
96 let xmlpres = mpres_document pres in
97 let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
99 (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
100 ids_to_inner_sorts,ids_to_inner_types)))
102 let nmml_of_cic_object status obj =
103 let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in
104 let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
105 let xmlpres = mpres_document pres_sequent in
106 Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
109 let ntxt_of_cic_object ~map_unicode_to_tex size status obj =
110 let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in
111 let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
112 let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
113 BoxPp.render_to_string ~map_unicode_to_tex
114 (function x::_ -> x | _ -> assert false) size pres_sequent
117 let txt_of_cic_sequent_all ~map_unicode_to_tex size metasenv sequent =
118 let unsh_sequent,(asequent,ids_to_terms,
119 ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
121 Cic2acic.asequent_of_sequent metasenv sequent
123 let content_sequent = Acic2content.map_sequent asequent in
125 CicNotationPres.mpres_of_box
126 (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
128 BoxPp.render_to_string ~map_unicode_to_tex
129 (function x::_ -> x | _ -> assert false) size pres_sequent
134 (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
136 let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
137 let txt,_,_ = txt_of_cic_sequent_all ~map_unicode_to_tex size metasenv sequent
141 let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
143 let _,(asequent,_,_,ids_to_inner_sorts,_) =
144 Cic2acic.asequent_of_sequent metasenv sequent
146 let _,_,_,t = Acic2content.map_sequent asequent in
148 TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
149 let t = TermContentPres.pp_ast t in
151 CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) t
153 BoxPp.render_to_string ~map_unicode_to_tex
154 (function x::_ -> x | _ -> assert false) size t
156 let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
157 let fake_sequent = (-1,context,t) in
158 txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
159 metasenv fake_sequent
163 CicMetaSubst.set_ppterm_in_context
164 (fun ~metasenv subst term context ->
166 let context' = CicMetaSubst.apply_subst_context subst context in
167 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
168 let term' = CicMetaSubst.apply_subst subst term in
171 ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
172 30 metasenv context' term' in
173 if String.contains res '\n' then
178 Sys.Break as exn -> raise exn
180 "[[ Exception raised during pretty-printing: " ^
182 Printexc.to_string exn
184 Sys.Break as exn -> raise exn
185 | _ -> "<<exception raised pretty-printing the exception>>"
187 (CicMetaSubst.use_low_level_ppterm_in_context := true;
190 CicMetaSubst.ppterm_in_context ~metasenv subst term context
192 CicMetaSubst.use_low_level_ppterm_in_context := false;
196 CicMetaSubst.use_low_level_ppterm_in_context := false;
200 (****************************************************************************)
201 (* txt_of_cic_object: IMPROVE ME *)
203 let remove_closed_substs s =
204 Pcre.replace ~pat:"{...}" ~templ:"" s
206 let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm =
207 let ast, ids_to_uris =
208 TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
210 CicNotationPres.box_of_mpres (
211 CicNotationPres.render ~prec:90
212 ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
213 (TermContentPres.pp_ast ast)) in
214 let render = function _::x::_ -> x | _ -> assert false in
215 let mpres = CicNotationPres.mpres_of_box bobj in
216 let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
217 remove_closed_substs s
219 let enable_notations = function
221 CicNotation.set_active_notations
222 (List.map fst (CicNotation.get_all_notations ()))
224 CicNotation.set_active_notations []
226 let txt_of_cic_object_all
227 ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
232 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses =
233 Cic2acic.acic_object_of_cic_object obj
235 aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
236 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses
238 | E.Object_not_found uri ->
239 let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
242 let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
246 if List.mem G.IPProcedural params then begin
248 Procedural2.debug := A2P.is_debug 1 params;
249 PO.debug := A2P.is_debug 2 params;
251 PO.critical := false;
252 A2P.tex_formatter := Some Format.std_formatter;
253 let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
255 let obj, info = PO.optimize_obj obj in
257 let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
259 let aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
260 ids_to_inner_types,ids_to_conjectures,ids_to_hypothesis = get_aobj obj in
261 let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
262 let lazy_term_pp = term_pp in
263 let obj_pp = CicNotationPp.pp_obj term_pp in
265 GrafiteAstPp.pp_statement
266 ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp
269 | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _)))
270 | G.Executable (_, G.Command (_, G.Obj (_, N.Record _))) as stm
272 let hc = !Acic2content.hide_coercions in
273 if List.mem G.IPCoercions params then
274 Acic2content.hide_coercions := false;
275 enable_notations false;
276 let str = stm_pp stm in
277 enable_notations true;
278 Acic2content.hide_coercions := hc;
280 (* FG: we disable notation for inductive types to avoid recursive notation *)
281 | G.Executable (_, G.Tactic _) as stm ->
282 let hc = !Acic2content.hide_coercions in
283 Acic2content.hide_coercions := false;
284 let str = stm_pp stm in
285 Acic2content.hide_coercions := hc;
287 (* FG: we show coercion because the reconstruction is not aware of them *)
289 let hc = !Acic2content.hide_coercions in
290 if List.mem G.IPCoercions params then
291 Acic2content.hide_coercions := false;
292 let str = stm_pp stm in
293 Acic2content.hide_coercions := hc;
297 A2P.procedural_of_acic_object
298 ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj
300 String.concat "" (List.map aux script) ^ "\n\n"
302 let aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
303 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses = get_aobj obj in
305 Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj
308 Content2pres.content2pres
309 ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj
312 remove_closed_substs (
313 BoxPp.render_to_string ~map_unicode_to_tex
314 (function _::x::_ -> x | _ -> assert false) n
315 (CicNotationPres.mpres_of_box bobj)
320 (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
321 ids_to_inner_sorts,ids_to_inner_types)))
323 let txt_of_cic_object
324 ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
326 let txt,_ = txt_of_cic_object_all
327 ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
330 let cic_prefix = Str.regexp_string "cic:/"
331 let matita_prefix = Str.regexp_string "cic:/matita/"
332 let suffixes = [".ind"; "_rec.con"; "_rect.con"; "_ind.con"; ".con"]
335 let map s = String.length s, s, Str.regexp_string s, "_discharged" ^ s in
336 List.map map suffixes
338 let replacement (ok, u) (l, s, x, t) =
339 if ok then ok, u else
340 if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u
342 let discharge_uri params uri =
344 if List.mem G.IPProcedural params then "cic:/matita/procedural/"
345 else "cic:/matita/declarative/"
347 let s = UM.string_of_uri uri in
348 if Str.string_match matita_prefix s 0 then uri else
349 let s = Str.replace_first cic_prefix template s in
350 let _, s = List.fold_left replacement (false, s) replacements in
353 let discharge_name s = s ^ "_discharged"
355 let txt_of_inline_uri ~map_unicode_to_tex params suri =
359 let print_exc = function
360 | ProofEngineHelpers.Bad_pattern s as e ->
361 Printexc.to_string e ^ " " ^ Lazy.force s
362 | e -> Printexc.to_string e
364 let dbd = LibraryDb.instance () in
365 let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
369 "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s"
370 (UM.string_of_uri uri) e
372 Printf.eprintf "%s\n" msg;
373 GrafiteTypes.command_error msg
376 Librarian.time_stamp "AT: BEGIN MAP";
378 (* FG: for now the explicit variables must be discharged *)
380 let r = txt_of_cic_object ~map_unicode_to_tex 78 params obj in
381 Librarian.time_stamp "AT: END MAP "; r
384 let s = UM.string_of_uri uri in
385 if Str.string_match matita_prefix s 0 then begin
386 Librarian.time_stamp "AT: GETTING OBJECT";
387 let obj, _ = E.get_obj Un.default_ugraph uri in
388 Librarian.time_stamp "AT: DONE ";
391 Ds.discharge_uri discharge_name (discharge_uri params) uri
393 if real then do_it obj else
394 let newuri = discharge_uri params uri in
395 let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
398 | TC.TypeCheckerFailure s ->
399 error uri ("failure : " ^ Lazy.force s)
400 | TC.AssertFailure s ->
401 error uri ("assert : " ^ Lazy.force s)
402 | E.Object_not_found u ->
403 error uri ("not found: " ^ UM.string_of_uri u)
404 | e -> error uri (print_exc e)
406 String.concat "" (List.map map sorted_uris)
408 let txt_of_inline_macro ~map_unicode_to_tex params name =
410 if Librarian.is_uri name then name else
412 Helm_registry.get_list Helm_registry.string "matita.includes"
414 let _, baseuri, _, _ =
415 Librarian.baseuri_of_script ~include_paths name
419 txt_of_inline_uri ~map_unicode_to_tex params suri
421 (****************************************************************************)
422 (* procedural_txt_of_cic_term *)
424 let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term =
425 let term, _info = PO.optimize_term context term in
426 let annterm, ids_to_inner_sorts, ids_to_inner_types =
427 try Cic2acic.acic_term_of_cic_term context term
429 let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
432 let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
433 let lazy_term_pp = term_pp in
434 let obj_pp = CicNotationPp.pp_obj term_pp in
435 let aux = GrafiteAstPp.pp_statement
436 ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
438 A2P.procedural_of_acic_term
439 ~ids_to_inner_sorts ~ids_to_inner_types params context annterm
441 String.concat "" (List.map aux script)
444 (****************************************************************************)
446 let txt_of_macro ~map_unicode_to_tex metasenv context m =
447 GrafiteAstPp.pp_macro
448 ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context)
449 ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
450 let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
451 txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)