matita/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 let use_high_level_pretty_printer = ref true;;
  39
  40 let to_text to_content to_pres lowlevel ~map_unicode_to_tex size status t =
  41  if !use_high_level_pretty_printer then
  42   let content,ids_to_nrefs = to_content status t in
  43   let pres = to_pres status ~ids_to_nrefs content in
  44   let pres = CicNotationPres.mpres_of_box pres in
  45    BoxPp.render_to_string ~map_unicode_to_tex
  46     (function x::_ -> x | _ -> assert false) size pres
  47  else
  48   [],lowlevel t
  49
  50 let ntxt_of_cic_sequent ~metasenv ~subst =
  51  to_text (Interpretations.nmap_sequent ~metasenv ~subst)
  52   Content2pres.nsequent2pres
  53   (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq])
  54
  55 let ntxt_of_cic_object ~map_unicode_to_tex =
  56  to_text Interpretations.nmap_cobj Content2pres.nobj2pres ~map_unicode_to_tex
  57   (new NCicPp.status)#ppobj
  58
  59 let ntxt_of_cic_term ~metasenv ~subst ~context =
  60  to_text (Interpretations.nmap_term ~metasenv ~subst ~context)
  61   (Content2pres.nterm2pres ?prec:None)
  62   ((new NCicPp.status)#ppterm ~metasenv ~subst ~context)
  63
  64 let ntxt_of_cic_context ~metasenv ~subst =
  65  to_text (Interpretations.nmap_context ~metasenv ~subst)
  66   Content2pres.ncontext2pres
  67   ((new NCicPp.status)#ppcontext ~metasenv ~subst)
  68
  69 let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst =
  70  [],
  71  "<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
  72   (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
  73
  74 class status =
  75  object(self)
  76   inherit Interpretations.status
  77   inherit TermContentPres.status
  78   method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t =
  79    snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
  80     ~context t)
  81
  82   method ppcontext ?sep:(_) ~subst ~metasenv context =
  83    snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
  84     context)
  85
  86   method ppsubst ~metasenv ?use_subst subst =
  87    snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
  88     subst)
  89
  90   method ppmetasenv ~subst metasenv =
  91    String.concat "\n"
  92     (List.map
  93       (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:false 80 self
  94         ~metasenv ~subst m)) metasenv)
  95
  96   method ppobj obj =
  97    snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj)
  98  end
  99
 100 let notation_pp_term status term =
 101   let to_pres = Content2pres.nterm2pres ?prec:None in
 102   let content = term in
 103   let size = 80 in
 104   let ids_to_nrefs = Hashtbl.create 1 in
 105   let pres = to_pres status ~ids_to_nrefs content in
 106   let pres = CicNotationPres.mpres_of_box pres in
 107    BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
 108     (function x::_ -> x | _ -> assert false) size pres
 109
 110 let _ = NotationPp.set_pp_term (fun status y -> snd (notation_pp_term (Obj.magic status) y))