]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/applyTransformation.ml
freescale porting, work in progress
[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 module GE = GrafiteEngine
45 module LS = LibrarySync
46 module Ds = CicDischarge
47 module PO = ProceduralOptimizer
48 module N = CicNotationPt
49 module A2P = Acic2Procedural
50
51 let mpres_document pres_box =
52   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
53
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)
57   =
58     Cic2acic.asequent_of_sequent metasenv sequent
59   in
60   let content_sequent = Acic2content.map_sequent asequent in 
61   let pres_sequent = 
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,
65    unsh_sequent,
66    (asequent,
67     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
68
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 
72   let pres_sequent = 
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
76
77 let mml_of_cic_object obj =
78   let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
79     ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
80   =
81     Cic2acic.acic_object_of_cic_object obj
82   in
83   let content = 
84     Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj
85   in
86   let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
87   let xmlpres = mpres_document pres in
88   let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
89   (mathml,(annobj,
90    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
91   ids_to_inner_sorts,ids_to_inner_types)))
92
93 let nmml_of_cic_object status obj =
94  let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in 
95  let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
96  let xmlpres = mpres_document pres_sequent in
97   Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
98 ;;
99
100 let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
101   let unsh_sequent,(asequent,ids_to_terms,
102     ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
103   =
104     Cic2acic.asequent_of_sequent metasenv sequent
105   in
106   let content_sequent = Acic2content.map_sequent asequent in 
107   let pres_sequent = 
108    CicNotationPres.mpres_of_box
109     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
110   in
111   BoxPp.render_to_string ~map_unicode_to_tex
112     (function x::_ -> x | _ -> assert false) size pres_sequent
113
114 let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
115  metasenv sequent =
116   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
117     Cic2acic.asequent_of_sequent metasenv sequent 
118   in
119   let _,_,_,t = Acic2content.map_sequent asequent in 
120   let t, ids_to_uris =
121    TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
122   let t = TermContentPres.pp_ast t in
123   let t =
124    CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) t
125   in
126    BoxPp.render_to_string ~map_unicode_to_tex
127     (function x::_ -> x | _ -> assert false) size t
128
129 let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = 
130  let fake_sequent = (-1,context,t) in
131   txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
132    metasenv fake_sequent 
133 ;;
134
135 ignore (
136  CicMetaSubst.set_ppterm_in_context
137   (fun ~metasenv subst term context ->
138     try
139      let context' = CicMetaSubst.apply_subst_context subst context in
140      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
141      let term' = CicMetaSubst.apply_subst subst term in
142      let res =
143       txt_of_cic_term
144        ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
145        30 metasenv context' term' in
146       if String.contains res '\n' then
147        "\n" ^ res ^ "\n"
148       else
149        res
150     with
151        Sys.Break as exn -> raise exn
152      | exn ->
153         "[[ Exception raised during pretty-printing: " ^
154          (try
155            Printexc.to_string exn
156           with
157              Sys.Break as exn -> raise exn
158            | _ -> "<<exception raised pretty-printing the exception>>"
159          ) ^ " ]] " ^
160         (CicMetaSubst.use_low_level_ppterm_in_context := true;
161          try
162           let res =
163            CicMetaSubst.ppterm_in_context ~metasenv subst term context
164           in
165            CicMetaSubst.use_low_level_ppterm_in_context := false;
166            res
167          with
168           exc -> 
169            CicMetaSubst.use_low_level_ppterm_in_context := false;
170            raise exc))
171 );;
172
173 (****************************************************************************)
174 (* txt_of_cic_object: IMPROVE ME *)
175
176 let remove_closed_substs s =
177     Pcre.replace ~pat:"{...}" ~templ:"" s
178
179 let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = 
180    let ast, ids_to_uris = 
181     TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
182    let bobj =
183     CicNotationPres.box_of_mpres (
184      CicNotationPres.render ~prec:90
185       ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
186       (TermContentPres.pp_ast ast)) in
187    let render = function _::x::_ -> x | _ -> assert false in
188    let mpres = CicNotationPres.mpres_of_box bobj in
189    let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
190    remove_closed_substs s
191
192 let enable_notations = function
193    | true -> 
194       CicNotation.set_active_notations
195          (List.map fst (CicNotation.get_all_notations ()))
196    | false ->
197       CicNotation.set_active_notations []
198
199 let txt_of_cic_object 
200  ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj 
201 =
202   let get_aobj obj = 
203      try   
204         let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
205             Cic2acic.acic_object_of_cic_object obj
206         in
207         aobj, ids_to_inner_sorts, ids_to_inner_types
208      with 
209         | E.Object_not_found uri -> 
210              let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
211              failwith msg
212         | e                     ->
213              let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
214              failwith msg
215   in
216   if List.mem G.IPProcedural params then begin
217
218      Procedural2.debug := A2P.is_debug 1 params;
219      PO.debug := A2P.is_debug 2 params;
220 (*     
221      PO.critical := false;
222      A2P.tex_formatter := Some Format.std_formatter;    
223      let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
224 *)      
225      let obj, info = PO.optimize_obj obj in
226 (*      
227      let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
228 *)      
229      let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
230      let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
231      let lazy_term_pp = term_pp in
232      let obj_pp = CicNotationPp.pp_obj term_pp in
233      let stm_pp =             
234         GrafiteAstPp.pp_statement
235            ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp
236      in
237      let aux = function
238         | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _)))
239         | G.Executable (_, G.Command (_, G.Obj (_, N.Record _))) as stm
240               ->           
241            let hc = !Acic2content.hide_coercions in
242            if List.mem G.IPCoercions params then 
243               Acic2content.hide_coercions := false;
244            enable_notations false;
245            let str = stm_pp stm in 
246            enable_notations true;
247            Acic2content.hide_coercions := hc;
248            str
249 (* FG: we disable notation for inductive types to avoid recursive notation *) 
250         | G.Executable (_, G.Tactic _) as stm -> 
251            let hc = !Acic2content.hide_coercions in
252            Acic2content.hide_coercions := false;
253            let str = stm_pp stm in
254            Acic2content.hide_coercions := hc;
255            str
256 (* FG: we show coercion because the reconstruction is not aware of them *)
257         | stm -> 
258            let hc = !Acic2content.hide_coercions in
259            if List.mem G.IPCoercions params then 
260               Acic2content.hide_coercions := false;
261            let str = stm_pp stm in
262            Acic2content.hide_coercions := hc;
263            str
264      in
265      let script = 
266         A2P.procedural_of_acic_object 
267            ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj 
268      in
269      String.concat "" (List.map aux script) ^ "\n\n"
270   end else
271      let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
272      let cobj = 
273        Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj 
274      in
275      let bobj = 
276         Content2pres.content2pres 
277            ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
278      in
279      remove_closed_substs (
280         BoxPp.render_to_string ~map_unicode_to_tex
281            (function _::x::_ -> x | _ -> assert false) n
282            (CicNotationPres.mpres_of_box bobj)
283         ^ "\n\n"
284      )
285
286 let cic_prefix = Str.regexp_string "cic:/"
287 let matita_prefix = Str.regexp_string "cic:/matita/"
288 let suffixes = [".ind"; "_rec.con"; "_rect.con"; "_ind.con"; ".con"]
289
290 let replacements = 
291    let map s = String.length s, s, Str.regexp_string s, "_discharged" ^ s in 
292    List.map map suffixes
293
294 let replacement (ok, u) (l, s, x, t) =
295    if ok then ok, u else
296    if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u
297
298 let discharge_uri params uri =
299    let template = 
300       if List.mem G.IPProcedural params then "cic:/matita/procedural/"
301       else "cic:/matita/declarative/"
302    in
303    let s = UM.string_of_uri uri in
304    if Str.string_match matita_prefix s 0 then uri else
305    let s = Str.replace_first cic_prefix template s in
306    let _, s = List.fold_left replacement (false, s) replacements in 
307    UM.uri_of_string s
308
309 let discharge_name s = s ^ "_discharged"
310
311 let txt_of_inline_uri ~map_unicode_to_tex params suri =
312 (*   
313    Ds.debug := true;
314 *)
315    let print_exc = function
316       | ProofEngineHelpers.Bad_pattern s as e ->
317            Printexc.to_string e ^ " " ^ Lazy.force s
318       | e -> Printexc.to_string e
319    in
320    let dbd = LibraryDb.instance () in   
321    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
322    let error uri e =
323       let msg  = 
324          Printf.sprintf 
325             "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
326             (UM.string_of_uri uri) e
327       in
328       Printf.eprintf "%s\n" msg;
329       GrafiteTypes.command_error msg
330    in
331    let map uri =
332       Librarian.time_stamp "AT: BEGIN MAP";
333       try
334 (* FG: for now the explicit variables must be discharged *)
335         let do_it obj =
336            let r = txt_of_cic_object ~map_unicode_to_tex 78 params obj in
337            Librarian.time_stamp "AT: END MAP  "; r
338         in
339         let obj, real = 
340            let s = UM.string_of_uri uri in
341            if Str.string_match matita_prefix s 0 then begin
342               Librarian.time_stamp "AT: GETTING OBJECT";
343               let obj, _ = E.get_obj Un.default_ugraph uri in
344               Librarian.time_stamp "AT: DONE          ";
345               obj, true
346            end else
347               Ds.discharge_uri discharge_name (discharge_uri params) uri
348         in
349         if real then do_it obj else
350         let newuri = discharge_uri params uri in
351         let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
352         do_it obj
353       with
354          | TC.TypeCheckerFailure s ->
355             error uri ("failure  : " ^ Lazy.force s)
356          | TC.AssertFailure s      ->
357             error uri ("assert   : " ^ Lazy.force s)
358          | E.Object_not_found u    ->
359             error uri ("not found: " ^ UM.string_of_uri u)
360          | e                       -> error uri (print_exc e)
361    in
362    String.concat "" (List.map map sorted_uris)
363
364 let txt_of_inline_macro ~map_unicode_to_tex params name =
365    let suri = 
366       if Librarian.is_uri name then name else
367       let include_paths = 
368          Helm_registry.get_list Helm_registry.string "matita.includes"
369       in
370       let _, baseuri, _, _ = 
371          Librarian.baseuri_of_script ~include_paths name
372       in
373       baseuri ^ "/"
374    in
375    txt_of_inline_uri ~map_unicode_to_tex params suri
376
377 (****************************************************************************)
378 (* procedural_txt_of_cic_term *)
379
380 let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term =
381   let term, _info = PO.optimize_term context term in
382   let annterm, ids_to_inner_sorts, ids_to_inner_types = 
383      try Cic2acic.acic_term_of_cic_term context term
384      with e -> 
385         let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
386         failwith msg
387   in
388   let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
389   let lazy_term_pp = term_pp in
390   let obj_pp = CicNotationPp.pp_obj term_pp in
391   let aux = GrafiteAstPp.pp_statement
392      ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
393   let script = 
394      A2P.procedural_of_acic_term 
395         ~ids_to_inner_sorts ~ids_to_inner_types params context annterm 
396   in
397   String.concat "" (List.map aux script)
398 ;;
399
400 (****************************************************************************)
401
402 let txt_of_macro ~map_unicode_to_tex metasenv context m =
403    GrafiteAstPp.pp_macro
404      ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context) 
405      ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
406         let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
407         txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)
408      m
409 ;;
410
411