]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/applyTransformation.ml
applyTransformation: variable discharging in procedural/declarative script
[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 UM = UriManager
39 module C  = Cic
40 module Un = CicUniv
41 module E  = CicEnvironment
42 module TC = CicTypeChecker
43 module G  = GrafiteAst
44
45 let mpres_document pres_box =
46   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
47
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)
51   =
52     Cic2acic.asequent_of_sequent metasenv sequent
53   in
54   let content_sequent = Acic2content.map_sequent asequent in 
55   let pres_sequent = 
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,
59    unsh_sequent,
60    (asequent,
61     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
62
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)
66   =
67     Cic2acic.acic_object_of_cic_object obj
68   in
69   let content = 
70     Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
71   in
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
75   (mathml,(annobj,
76    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
77   ids_to_inner_sorts,ids_to_inner_types)))
78
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)
82   =
83     Cic2acic.asequent_of_sequent metasenv sequent
84   in
85   let content_sequent = Acic2content.map_sequent asequent in 
86   let pres_sequent = 
87    CicNotationPres.mpres_of_box
88     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
89   in
90   BoxPp.render_to_string ~map_unicode_to_tex
91     (function x::_ -> x | _ -> assert false) size pres_sequent
92
93 let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
94  metasenv sequent =
95   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
96     Cic2acic.asequent_of_sequent metasenv sequent 
97   in
98   let _,_,_,t = Acic2content.map_sequent asequent in 
99   let t, ids_to_uris =
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
105
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 
110 ;;
111
112 ignore (
113  CicMetaSubst.set_ppterm_in_context
114   (fun ~metasenv subst term context ->
115     try
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
119      let res =
120       txt_of_cic_term
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
124        "\n" ^ res ^ "\n"
125       else
126        res
127     with
128        Sys.Break as exn -> raise exn
129      | exn ->
130         "[[ Exception raised during pretty-printing: " ^
131          (try
132            Printexc.to_string exn
133           with
134              Sys.Break as exn -> raise exn
135            | _ -> "<<exception raised pretty-printing the exception>>"
136          ) ^ " ]] " ^
137         (CicMetaSubst.use_low_level_ppterm_in_context := true;
138          try
139           let res =
140            CicMetaSubst.ppterm_in_context ~metasenv subst term context
141           in
142            CicMetaSubst.use_low_level_ppterm_in_context := false;
143            res
144          with
145           exc -> 
146            CicMetaSubst.use_low_level_ppterm_in_context := false;
147            raise exc))
148 );;
149
150 (****************************************************************************)
151 (* txt_of_cic_object: IMPROVE ME *)
152
153 let remove_closed_substs s =
154     Pcre.replace ~pat:"{...}" ~templ:"" s
155
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
159    let bobj =
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
167
168 let txt_of_cic_object 
169  ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
170  n style ?flavour prefix obj 
171 =
172   let get_aobj obj = 
173      try   
174         let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
175             Cic2acic.acic_object_of_cic_object obj
176         in
177         aobj, ids_to_inner_sorts, ids_to_inner_types
178      with 
179         | E.Object_not_found uri -> 
180              let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
181              failwith msg
182         | e                     ->
183              let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
184              failwith msg
185   in
186   match style with
187      | G.Declarative      ->
188         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
189         let cobj = 
190           Acic2content.annobj2content 
191             ids_to_inner_sorts ids_to_inner_types aobj 
192         in
193         let bobj = 
194           Content2pres.content2pres 
195             ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
196         in
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)
201         )
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
210         let script = 
211            Acic2Procedural.procedural_of_acic_object 
212               ~ids_to_inner_sorts ~ids_to_inner_types 
213               ?depth ?flavour prefix aobj 
214   in
215         "\n\n" ^ String.concat "" (List.map aux script)
216
217 let cic_prefix = Str.regexp_string "cic:/"
218
219 let matita_prefix = Str.regexp_string "cic:/matita/"
220
221 let discharge_uri style uri =
222    let template = match style with
223       | G.Declarative  -> "cic:/matita/declarative/"   
224       | G.Procedural _ -> "cic:/matita/procedural/"
225    in
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
229    UM.uri_of_string s
230
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
236    in
237    let dbd = LibraryDb.instance () in   
238    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
239    let map uri =
240       try
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
251       with
252          | e -> 
253             let msg = 
254                Printf.sprintf 
255                   "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
256                   (UM.string_of_uri uri) (print_exc e)
257             in
258             Printf.eprintf "%s\n" msg;
259             GrafiteTypes.command_error msg
260    in
261    String.concat "" (List.map map sorted_uris)
262
263 let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
264    let suri = 
265       if Librarian.is_uri name then name else
266       let include_paths = 
267          Helm_registry.get_list Helm_registry.string "matita.includes"
268       in
269       let _, baseuri, _, _ = 
270          Librarian.baseuri_of_script ~include_paths name
271       in
272       baseuri ^ "/"
273    in
274    txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri
275
276 (****************************************************************************)
277 (* procedural_txt_of_cic_term *)
278
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
282      with e -> 
283         let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
284         failwith msg
285   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
291   let script = 
292      Acic2Procedural.procedural_of_acic_term 
293         ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm 
294   in
295   String.concat "" (List.map aux script)