matitaB/components/content_pres/cicNotationPres.ml

   1 (* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 module A = NotationPt
  29
  30 type markup = string Box.box
  31
  32 let to_unicode = Utf8Macro.unicode_of_tex
  33
  34 let open_paren    = Box.Text ([], "(")
  35 let closed_paren  = Box.Text ([], ")")
  36 let semicolon     = Box.Text ([], ";")
  37
  38 let toggle_action children =
  39   Box.Action ([None, "actiontype", "toggle"], children)
  40
  41 type child_pos = [ `Left | `Right | `Inner ]
  42
  43 let pp_assoc =
  44   function
  45   | Gramext.LeftA -> "LeftA"
  46   | Gramext.RightA -> "RightA"
  47   | Gramext.NonA -> "NonA"
  48
  49 let rec is_atomic = function
  50   | Box.Space _
  51   | Box.Ink _
  52   | Box.Text _
  53   | Box.Object _ -> true
  54   | Box.H (_, [box])
  55   | Box.V (_, [box])
  56   | Box.HV (_, [box])
  57   | Box.HOV (_, [box])
  58   | Box.Action (_, [box]) -> is_atomic box
  59   | _ -> false
  60
  61 let add_parens child_prec curr_prec t =
  62   if is_atomic t then
  63     ((*prerr_endline ("NOT adding parens around ATOMIC: "^
  64       BoxPp.render_to_string (function x::_->x|_->assert false)
  65         ~map_unicode_to_tex:false 80 t);*)t)
  66   else if child_prec >= 0 && child_prec < curr_prec then
  67     begin
  68     (*prerr_endline ("adding parens around: "^
  69       BoxPp.render_to_string (function x::_->x|_->assert false)
  70         ~map_unicode_to_tex:false 80 t);*)
  71       Box.H ([], [ open_paren; t; closed_paren ])
  72   end else
  73     ((*prerr_endline ("NOT adding parens around: "^
  74       BoxPp.render_to_string (function x::_->x|_->assert false)
  75         ~map_unicode_to_tex:false 80 t);*)t)
  76
  77 let render status ?(prec=(-1)) =
  78   let rec aux prec t =
  79     match t with
  80     | A.AttributedTerm _ ->
  81         aux_attributes [] ""  prec t
  82     | A.Num (literal, _) -> Box.Text ([], literal)
  83     | A.Symbol (literal, _) -> Box.Text ([], literal)
  84     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
  85     | A.Meta(n, l) ->
  86         let local_context =
  87           Box.Text ([], "[")::
  88             (NotationUtil.dress (Box.Text ([],  ";"))
  89               (List.map
  90                 (function
  91                 | None -> Box.Text ([],  "_")
  92                 | Some t -> aux prec t) l)) @
  93             [Box.Text ([], "]")]
  94         in
  95         Box.H ([],
  96           (Box.Text ([], "?"^string_of_int n)::
  97             (if (l <> []) then [Box.H ([],local_context)] else [])))
  98     | A.Literal l -> aux_literal prec l
  99     | A.UserInput -> Box.Text ([], "%")
 100     | A.Layout l -> aux_layout prec l
 101     | A.Magic _
 102     | A.Variable _ -> assert false  (* should have been instantiated *)
 103     | t ->
 104         prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
 105         assert false
 106
 107   and aux_attributes xmlattrs xref  prec t =
 108     let reset = ref false in
 109     let inferred_level = ref None in
 110     let expected_level = ref None in
 111     let new_xref = ref [] in
 112     let new_xmlattrs = ref [] in
 113     let rec aux_attribute =
 114       function
 115       | A.AttributedTerm (attr, t) ->
 116           (match attr with
 117           | `Loc _
 118           | `Raw _ -> ()
 119           | `Level (-1) -> reset := true
 120           | `Level child_prec ->
 121 (*               assert (!expected_level = None); *)
 122               expected_level := !inferred_level;
 123               inferred_level := Some child_prec
 124           | `IdRef xref -> new_xref := xref :: !new_xref
 125           | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
 126           aux_attribute t
 127       | t ->
 128           let prec =
 129             match !expected_level with
 130             | None -> prec
 131             | Some prec -> prec
 132           in
 133           (match !inferred_level with
 134           | None -> aux prec t
 135           | Some child_prec ->
 136               let t' = aux child_prec t in
 137               (*prerr_endline
 138                 ("inferred: "^string_of_int child_prec^
 139                  " exp: "^string_of_int prec ^
 140                  " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
 141                     (function x::_->x|_->assert false) 80 t');*)
 142               if !reset
 143               then ((*prerr_endline "reset";*)t')
 144               else add_parens child_prec prec t')
 145     in
 146 (*     prerr_endline (NotationPp.pp_term t); *)
 147     aux_attribute t
 148
 149   and aux_literal prec l =
 150     (match l with
 151     | `Symbol s -> Box.Text ([], to_unicode s)
 152     | `Keyword s -> Box.Text ([], to_unicode s)
 153     | `Number s  -> Box.Text ([], to_unicode s))
 154
 155   and aux_layout prec l =
 156     let attrs = [] in
 157     let invoke' t = aux prec t in
 158       (* use the one below to reset precedence and associativity *)
 159     let invoke_reinit t = aux ~-1 t in
 160     match l with
 161     | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
 162     | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
 163       -> assert false
 164     | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
 165     | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
 166     | A.Below (t1, t2) -> assert false
 167     | A.Above (t1, t2) -> assert false
 168     | A.Frac (t1, t2)
 169     | A.Over (t1, t2) -> assert false
 170     | A.Atop (t1, t2) -> assert false
 171     | A.InfRule (t1, t2, t3) -> assert false
 172     | A.Sqrt t -> assert false
 173     | A.Root (t1, t2) -> assert false
 174     | A.Box (a, terms) ->
 175         let children = List.map (aux prec) terms in
 176         Box.H([],children)
 177     | A.Mstyle (l,terms) -> assert false
 178     | A.Mpadded (l,terms) -> assert false
 179     | A.Maction alternatives ->
 180          toggle_action (List.map invoke_reinit alternatives)
 181     | A.Group terms -> assert false
 182     | A.Break -> Box.Space []
 183   in
 184   aux prec
 185
 186 (* let render_to_boxml id_to_uri t =
 187   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
 188   Xml.add_xml_declaration xml_stream *)
 189
 190 let render_context_entry status name = function
 191   | A.Decl t ->
 192       Box.H ([],
 193              [Box.Text([],name); Box.Text([],":");
 194               render status (TermContentPres.pp_ast status t)])
 195   | A.Def (t,ty) ->
 196       Box.H ([],
 197               [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def");
 198                render status (TermContentPres.pp_ast status t)])
 199
 200 let render_context status context =
 201   Box.V ([],
 202          List.map
 203            (fun (name,entry) ->
 204               render_context_entry status (to_unicode name) entry) context)
 205
 206 let render_sequent status (i,context,ty) =
 207   Box.V ([],
 208          [render_context status context;
 209           Box.Ink [None,"width","4cm"; None,"height","2px"];
 210           render status (TermContentPres.pp_ast status ty)])
 211
 212