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 small_skip    = Box.Text ([], " ")
  35 let open_paren    = Box.Text ([], "(")
  36 let closed_paren  = Box.Text ([], ")")
  37 let semicolon     = Box.Text ([], ";")
  38
  39 let toggle_action children =
  40   Box.Action ([None, "actiontype", "toggle"], children)
  41
  42 type child_pos = [ `Left | `Right | `Inner ]
  43
  44 let pp_assoc =
  45   function
  46   | Gramext.LeftA -> "LeftA"
  47   | Gramext.RightA -> "RightA"
  48   | Gramext.NonA -> "NonA"
  49
  50 let rec is_atomic = function
  51   | Box.Space _
  52   | Box.Ink _
  53   | Box.Text _
  54   | Box.Object _ -> true
  55   | Box.H (_, [box])
  56   | Box.V (_, [box])
  57   | Box.HV (_, [box])
  58   | Box.HOV (_, [box])
  59   | Box.Action (_, [box]) -> is_atomic box
  60   | _ -> false
  61
  62 let add_parens child_prec curr_prec t =
  63   if is_atomic t then
  64     ((*prerr_endline ("NOT adding parens around ATOMIC: "^
  65       BoxPp.render_to_string (function x::_->x|_->assert false)
  66         ~map_unicode_to_tex:false 80 t);*)t)
  67   else if child_prec >= 0 && child_prec < curr_prec then
  68     begin
  69     (*prerr_endline ("adding parens around: "^
  70       BoxPp.render_to_string (function x::_->x|_->assert false)
  71         ~map_unicode_to_tex:false 80 t);*)
  72       Box.H ([], [ open_paren; t; closed_paren ])
  73   end else
  74     ((*prerr_endline ("NOT adding parens around: "^
  75       BoxPp.render_to_string (function x::_->x|_->assert false)
  76         ~map_unicode_to_tex:false 80 t);*)t)
  77
  78 let box_of spec attrs children =
  79   match children with
  80     | [t] -> t
  81     | _ ->
  82         let kind, spacing, indent = spec in
  83         let dress children =
  84           if spacing then
  85             NotationUtil.dress small_skip children
  86           else
  87             children
  88         in
  89         let attrs' =
  90           (if spacing then [None, "spacing", "0.5em"] else [])
  91           @ (if indent then [None, "indent", "0.5em"] else [])
  92           @ attrs
  93         in
  94           match kind with
  95             | A.H -> Box.H (attrs',children)
  96             | A.V -> Box.V (attrs',children)
  97             | A.HV -> Box.HV (attrs',children)
  98             | A.HOV -> Box.HOV (attrs',children)
  99
 100 let render status ?(prec=(-1)) =
 101   let rec aux prec t =
 102     match t with
 103     | A.AttributedTerm _ ->
 104         aux_attributes [] ""  prec t
 105     | A.Num (literal, _) -> Box.Text ([], literal)
 106     | A.Symbol (literal, Some (None,desc)) ->
 107         let literal = to_unicode literal in
 108         let attr = [ None, "title", desc ] in
 109           Box.Text (attr, literal)
 110     | A.Symbol (literal, Some (Some u,desc)) ->
 111         let literal = to_unicode literal in
 112         let attr = [ None, "title", desc; None, "href", u ] in
 113         Box.Text (attr, literal)
 114     | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
 115     | A.Ident (literal, `Uri u) ->
 116         let attr = [ None, "href", u ] in
 117         let literal = to_unicode literal in
 118         Box.Text (attr,literal)
 119     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
 120     | A.Meta(n, l) ->
 121         let local_context =
 122           Box.Text ([], "[")::
 123             (NotationUtil.dress (Box.Text ([],  ";"))
 124               (List.map
 125                 (function
 126                 | None -> Box.Text ([],  "_")
 127                 | Some t -> aux prec t) l)) @
 128             [Box.Text ([], "]")]
 129         in
 130         Box.H ([],
 131           (Box.Text ([], "?"^string_of_int n)::
 132             (if (l <> []) then [Box.H ([],local_context)] else [])))
 133     | A.Literal (`Symbol (s,x))
 134     | A.Literal (`Keyword (s,x))
 135     | A.Literal (`Number (s,x)) ->
 136        let attr =
 137          match x with
 138          | None, None -> []
 139          | Some u, None -> [ None, "href", u ]
 140          | None, Some d -> [ None, "title", d ]
 141          | Some u, Some d -> [ None, "href", u; None, "title", d ]
 142        in
 143        Box.Text (attr, to_unicode s)
 144     | A.UserInput -> Box.Text ([], "%")
 145     | A.Layout l -> aux_layout prec l
 146     | A.Magic _
 147     | A.Variable _ -> assert false  (* should have been instantiated *)
 148     | t ->
 149         prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
 150         assert false
 151
 152   and aux_attributes xmlattrs xref  prec t =
 153     let reset = ref false in
 154     let inferred_level = ref None in
 155     let expected_level = ref None in
 156     let new_xref = ref [] in
 157     let new_xmlattrs = ref [] in
 158     let rec aux_attribute =
 159       function
 160       | A.AttributedTerm (attr, t) ->
 161           (match attr with
 162           | `Loc _
 163           | `Raw _ -> ()
 164           | `Level (-1) -> reset := true
 165           | `Level child_prec ->
 166 (*               assert (!expected_level = None); *)
 167               expected_level := !inferred_level;
 168               inferred_level := Some child_prec
 169           | `IdRef xref -> new_xref := xref :: !new_xref
 170           | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
 171           aux_attribute t
 172       | t ->
 173           let prec =
 174             match !expected_level with
 175             | None -> prec
 176             | Some prec -> prec
 177           in
 178           (match !inferred_level with
 179           | None -> aux prec t
 180           | Some child_prec ->
 181               let t' = aux child_prec t in
 182               (*prerr_endline
 183                 ("inferred: "^string_of_int child_prec^
 184                  " exp: "^string_of_int prec ^
 185                  " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
 186                     (function x::_->x|_->assert false) 80 t');*)
 187               if !reset
 188               then ((*prerr_endline "reset";*)t')
 189               else add_parens child_prec prec t')
 190     in
 191 (*     prerr_endline (NotationPp.pp_term t); *)
 192     aux_attribute t
 193
 194   and aux_layout prec l =
 195     let attrs = [] in
 196     let invoke' t = aux prec t in
 197       (* use the one below to reset precedence and associativity *)
 198     let invoke_reinit t = aux ~-1 t in
 199     match l with
 200     | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
 201     | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
 202       -> assert false
 203     | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
 204     | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
 205     | A.Below (t1, t2) -> assert false
 206     | A.Above (t1, t2) -> assert false
 207     | A.Frac (t1, t2)
 208     | A.Over (t1, t2) -> assert false
 209     | A.Atop (t1, t2) -> assert false
 210     | A.InfRule (t1, t2, t3) -> assert false
 211     | A.Sqrt t -> assert false
 212     | A.Root (t1, t2) -> assert false
 213     | A.Box ((_,spacing,_) as kind, terms) ->
 214         let children =
 215           aux_children spacing prec
 216             (NotationUtil.ungroup terms)
 217         in
 218         box_of kind attrs children
 219     | A.Mstyle (l,terms) -> assert false
 220     | A.Mpadded (l,terms) -> assert false
 221     | A.Maction alternatives ->
 222          toggle_action (List.map invoke_reinit alternatives)
 223     | A.Group terms -> assert false
 224     | A.Break -> Box.Space []
 225   and aux_children spacing prec terms =
 226     let find_clusters =
 227       let rec aux_list first clusters acc =
 228         function
 229             [] when acc = [] -> List.rev clusters
 230           | [] -> aux_list first (List.rev acc :: clusters) [] []
 231           | (A.Layout A.Break) :: tl when acc = [] ->
 232               aux_list first clusters [] tl
 233           | (A.Layout A.Break) :: tl ->
 234               aux_list first (List.rev acc :: clusters) [] tl
 235           | [hd] ->
 236                 aux_list false clusters
 237                   (aux prec hd :: acc) []
 238           | hd :: tl ->
 239                 aux_list false clusters
 240                   (aux prec hd :: acc) tl
 241       in
 242         aux_list true [] []
 243     in
 244     let boxify_pres =
 245       function
 246           [t] -> t
 247         | tl -> box_of (A.H, spacing, false) [] tl
 248     in
 249       List.map boxify_pres (find_clusters terms)
 250   in
 251   (fun t ->
 252    (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
 253   aux prec t)
 254
 255 (* let render_to_boxml id_to_uri t =
 256   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
 257   Xml.add_xml_declaration xml_stream *)
 258
 259 let render_context_entry status name = function
 260   | A.Decl t ->
 261       Box.H ([],
 262              [Box.Text([],name); Box.Text([],":");
 263               render status (TermContentPres.pp_ast status t)])
 264   | A.Def (t,ty) ->
 265       Box.H ([],
 266               [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def");
 267                render status (TermContentPres.pp_ast status t)])
 268
 269 let render_context status context =
 270   Box.V ([],
 271          Box.Space [None, "width", "0.5em"]::
 272          List.map
 273            (fun (name,entry) ->
 274               render_context_entry status (to_unicode name) entry) context)
 275
 276 let render_sequent status (i,context,ty) =
 277   Box.V ([],
 278          [render_context status (List.rev context);
 279           Box.Ink [None,"width","4cm"; None,"height","2px"];
 280           render status (TermContentPres.pp_ast status ty)])
 281
 282