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