]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/applyTransformation.ml
natural number => Coq natural number
[helm.git] / helm / software / matita / applyTransformation.ml
1 (* Copyright (C) 2000-2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (***************************************************************************)
27 (*                                                                         *)
28 (*                               PROJECT HELM                              *)
29 (*                                                                         *)
30 (*                   Andrea Asperti <asperti@cs.unibo.it>                  *)
31 (*                                21/11/2003                               *)
32 (*                                                                         *)
33 (*                                                                         *)
34 (***************************************************************************)
35
36 (* $Id$ *)
37
38 module G = GrafiteAst
39
40 let mpres_document pres_box =
41   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
42
43 let mml_of_cic_sequent metasenv sequent =
44   let unsh_sequent,(asequent,ids_to_terms,
45     ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
46   =
47     Cic2acic.asequent_of_sequent metasenv sequent
48   in
49   let content_sequent = Acic2content.map_sequent asequent in 
50   let pres_sequent = 
51     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
52   in
53   let xmlpres = mpres_document pres_sequent in
54   (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
55    unsh_sequent,
56    (asequent,
57     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
58
59 let mml_of_cic_object obj =
60   let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
61     ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
62   =
63     Cic2acic.acic_object_of_cic_object obj
64   in
65   let content = 
66     Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
67   in
68   let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
69   let xmlpres = mpres_document pres in
70   let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
71   (mathml,(annobj,
72    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
73   ids_to_inner_sorts,ids_to_inner_types)))
74
75 let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
76   let unsh_sequent,(asequent,ids_to_terms,
77     ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
78   =
79     Cic2acic.asequent_of_sequent metasenv sequent
80   in
81   let content_sequent = Acic2content.map_sequent asequent in 
82   let pres_sequent = 
83    CicNotationPres.mpres_of_box
84     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
85   in
86   BoxPp.render_to_string ~map_unicode_to_tex
87     (function x::_ -> x | _ -> assert false) size pres_sequent
88
89 let txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv sequent =
90   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
91     Cic2acic.asequent_of_sequent metasenv sequent 
92   in
93   let _,_,_,t = Acic2content.map_sequent asequent in 
94   let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
95   let t = TermContentPres.pp_ast t in
96   let t = CicNotationPres.render ids_to_uris t in
97   BoxPp.render_to_string ~map_unicode_to_tex
98     (function x::_ -> x | _ -> assert false) size t
99
100 let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = 
101   let fake_sequent = (-1,context,t) in
102   txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv fake_sequent 
103 ;;
104
105 ignore (
106  CicMetaSubst.set_ppterm_in_context
107   (fun ~metasenv subst term context ->
108     try
109      let context' = CicMetaSubst.apply_subst_context subst context in
110      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
111      let term' = CicMetaSubst.apply_subst subst term in
112      let res =
113       txt_of_cic_term
114        ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
115        30 metasenv context' term' in
116       if String.contains res '\n' then
117        "\n" ^ res ^ "\n"
118       else
119        res
120     with
121        Sys.Break as exn -> raise exn
122      | exn ->
123         "[[ Exception raised during pretty-printing: " ^
124          (try
125            Printexc.to_string exn
126           with
127              Sys.Break as exn -> raise exn
128            | _ -> "<<exception raised pretty-printing the exception>>"
129          ) ^ " ]] " ^
130         (CicMetaSubst.use_low_level_ppterm_in_context := true;
131          try
132           let res =
133            CicMetaSubst.ppterm_in_context ~metasenv subst term context
134           in
135            CicMetaSubst.use_low_level_ppterm_in_context := false;
136            res
137          with
138           exc -> 
139            CicMetaSubst.use_low_level_ppterm_in_context := false;
140            raise exc))
141 );;
142
143 (****************************************************************************)
144 (* txt_of_cic_object: IMPROVE ME *)
145
146 let remove_closed_substs s =
147     Pcre.replace ~pat:"{...}" ~templ:"" s
148
149 let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = 
150    let ast, ids_to_uris = 
151       TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
152    in
153    let bobj =
154       CicNotationPres.box_of_mpres (
155          CicNotationPres.render ~prec:90 ids_to_uris 
156             (TermContentPres.pp_ast ast)
157       )
158    in
159    let render = function _::x::_ -> x | _ -> assert false in
160    let mpres = CicNotationPres.mpres_of_box bobj in
161    let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
162    remove_closed_substs s
163
164 let txt_of_cic_object 
165  ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj 
166 =
167   let get_aobj obj = 
168      try   
169         let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
170             Cic2acic.acic_object_of_cic_object obj
171         in
172         aobj, ids_to_inner_sorts, ids_to_inner_types
173      with e -> 
174         let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
175         failwith msg
176   in
177   match style with
178      | G.Declarative      ->
179         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
180         let cobj = 
181           Acic2content.annobj2content 
182             ids_to_inner_sorts ids_to_inner_types aobj 
183         in
184         let bobj = 
185           Content2pres.content2pres 
186             ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
187         in
188         remove_closed_substs ("\n\n" ^
189            BoxPp.render_to_string ~map_unicode_to_tex
190             (function _::x::_ -> x | _ -> assert false) n
191             (CicNotationPres.mpres_of_box bobj)
192         )
193      | G.Procedural depth ->
194         let obj = ProceduralOptimizer.optimize_obj obj in
195         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
196         let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
197         let lazy_term_pp = term_pp in
198         let obj_pp = CicNotationPp.pp_obj term_pp in
199         let aux = GrafiteAstPp.pp_statement
200          ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
201         let script = 
202     Acic2Procedural.acic2procedural 
203            ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj 
204   in
205         String.concat "" (List.map aux script) ^ "\n\n"
206
207 let txt_of_inline_macro ~map_unicode_to_tex style suri prefix =
208    let print_exc = function
209       | ProofEngineHelpers.Bad_pattern s as e ->
210            Printexc.to_string e ^ " " ^ Lazy.force s
211       | e -> Printexc.to_string e
212    in
213    let dbd = LibraryDb.instance () in   
214    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
215    let map uri =
216       try 
217         txt_of_cic_object 
218           ~map_unicode_to_tex 78 style prefix
219           (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
220       with
221          | e -> 
222             Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
223             (UriManager.string_of_uri uri) (print_exc e)
224    in
225    String.concat "" (List.map map sorted_uris)