helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml

   1 (* Copyright (C) 2000, 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 (*                             28/6/2003                                   *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35 module C2P = Cexpr2pres;;
  36 module P = Mpresentation;;
  37
  38 let binary f =
  39  function
  40     [a;b] -> f a b
  41   | _ -> assert false
  42 ;;
  43
  44 let unary f =
  45  function
  46     [a] -> f a
  47   | _ -> assert false
  48 ;;
  49
  50 let m_open_fence = P.Mtext([], "(")
  51 let b_open_fence = Box.b_text [] "("
  52 (*
  53 let m_close_fence = P.Mtext([], ")")
  54 let b_close_fence = Box.b_text [] ")"
  55 *)
  56
  57 let b_h_with_open_fence attrs a b op =
  58   Box.b_h attrs [ b_open_fence; a; Box.b_object op; b ]
  59 let b_h_without_open_fence attrs a b op =
  60   Box.b_h attrs [ a; Box.b_object op; b ]
  61 let b_v_with_open_fence attrs a b op =
  62   Box.b_v attrs [
  63     Box.b_h [] [ b_open_fence; a];
  64     Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
  65   ]
  66 let b_v_without_open_fence attrs a b op =
  67   Box.b_v attrs [
  68     a;
  69     Box.b_indent (Box.b_h [] [ Box.b_object op; b ])
  70   ]
  71
  72 let m_row_with_open_fence = P.row_with_brackets
  73 let m_row_without_open_fence = P.row_without_brackets
  74
  75 let m_close_fence = ")"
  76 let b_close_fence = ")"
  77
  78 let init
  79  ~(cexpr2pres:
  80    ?priority:int ->
  81    ?assoc:bool ->
  82    ?tail:string list ->
  83    Content_expressions.cexpr ->
  84    Mpresentation.mpres)
  85  ~(cexpr2pres_charcount:
  86    ?priority:int ->
  87    ?assoc:bool ->
  88    ?tail:string list ->
  89    Content_expressions.cexpr ->
  90    Mpresentation.mpres Box.box)
  91 =
  92
  93 (* arrow *)
  94 Hashtbl.add C2P.symbol_table "arrow" (binary
  95   (fun a b ~priority ~assoc ~tail aattr sattr ->
  96      if (priority > 5) || (priority = 5 && assoc) then
  97        m_row_with_open_fence aattr
  98          (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
  99          (cexpr2pres ~priority:5 ~assoc:true
 100             ~tail:((m_close_fence)::tail) b)
 101          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
 102      else
 103        m_row_without_open_fence aattr
 104          (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
 105          (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b)
 106          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
 107
 108 Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
 109   (fun a b ~priority ~assoc ~tail aattr sattr ->
 110      if (priority > 40) || (priority = 40 && assoc) then
 111        b_v_with_open_fence aattr
 112          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a)
 113          (cexpr2pres_charcount ~priority:40 ~assoc:true
 114            ~tail:(b_close_fence::tail) b)
 115          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
 116      else
 117        b_v_without_open_fence aattr
 118          (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a)
 119          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b)
 120          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
 121
 122 (* eq *)
 123 Hashtbl.add C2P.symbol_table "eq" (binary
 124   (fun a b ~priority ~assoc ~tail aattr sattr ->
 125      if (priority > 40) || (priority = 40 && assoc) then
 126        m_row_with_open_fence aattr
 127          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 128          (cexpr2pres ~priority:40 ~assoc:false
 129             ~tail:(m_close_fence::tail) b)
 130          (P.Mo(sattr,"="))
 131      else
 132        m_row_without_open_fence aattr
 133          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 134          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 135          (P.Mo(sattr,"="))));
 136
 137 Hashtbl.add C2P.symbol_table_charcount "eq" (binary
 138   (fun a b ~priority ~assoc ~tail aattr sattr ->
 139      if (priority > 40) || (priority = 40 && assoc) then
 140        b_v_with_open_fence aattr
 141          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 142          (cexpr2pres_charcount ~priority:40 ~assoc:false
 143            ~tail:(b_close_fence::tail) b)
 144          (P.Mo(sattr,"="))
 145      else
 146        b_v_without_open_fence aattr
 147          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 148          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 149          (P.Mo(sattr,"="))));
 150
 151 (* and *)
 152 Hashtbl.add C2P.symbol_table "and" (binary
 153   (fun a b ~priority ~assoc ~tail aattr sattr ->
 154      if (priority > 20) || (priority = 20 && assoc) then
 155        m_row_with_open_fence aattr
 156          (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
 157          (cexpr2pres ~priority:20 ~assoc:false
 158             ~tail:(m_close_fence::tail) b)
 159          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
 160      else
 161        m_row_without_open_fence aattr
 162          (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
 163          (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b)
 164          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
 165
 166 Hashtbl.add C2P.symbol_table_charcount "and" (binary
 167   (fun a b ~priority ~assoc ~tail aattr sattr ->
 168      if (priority > 20) || (priority = 20 && assoc) then
 169        b_v_with_open_fence aattr
 170          (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
 171          (cexpr2pres_charcount ~priority:20 ~assoc:false
 172            ~tail:(b_close_fence::tail) b)
 173          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
 174      else
 175        b_v_without_open_fence aattr
 176          (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
 177          (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b)
 178          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
 179
 180 (* or *)
 181 Hashtbl.add C2P.symbol_table "or" (binary
 182   (fun a b ~priority ~assoc ~tail aattr sattr ->
 183      if (priority > 10) || (priority = 10 && assoc) then
 184        m_row_with_open_fence aattr
 185          (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
 186          (cexpr2pres ~priority:10 ~assoc:false
 187             ~tail:(m_close_fence::tail) b)
 188          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
 189      else
 190        m_row_without_open_fence aattr
 191          (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
 192          (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b)
 193          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
 194
 195 Hashtbl.add C2P.symbol_table_charcount "or" (binary
 196   (fun a b ~priority ~assoc ~tail aattr sattr ->
 197      if (priority > 10) || (priority = 10 && assoc) then
 198        b_v_with_open_fence aattr
 199          (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
 200          (cexpr2pres_charcount ~priority:10 ~assoc:false
 201            ~tail:(b_close_fence::tail) b)
 202          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
 203      else
 204        b_v_without_open_fence aattr
 205          (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
 206          (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b)
 207          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
 208
 209 (* iff *)
 210 Hashtbl.add C2P.symbol_table "iff" (binary
 211   (fun a b ~priority ~assoc ~tail aattr sattr ->
 212      if (priority > 5) || (priority = 5 && assoc) then
 213        m_row_with_open_fence aattr
 214          (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
 215          (cexpr2pres ~priority:5 ~assoc:false
 216             ~tail:(m_close_fence::tail) b)
 217          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
 218      else
 219        m_row_without_open_fence aattr
 220          (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
 221          (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b)
 222          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
 223
 224 Hashtbl.add C2P.symbol_table_charcount "iff" (binary
 225   (fun a b ~priority ~assoc ~tail aattr sattr ->
 226      if (priority > 5) || (priority = 5 && assoc) then
 227        b_v_with_open_fence aattr
 228          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
 229          (cexpr2pres_charcount ~priority:5 ~assoc:false
 230            ~tail:(b_close_fence::tail) b)
 231          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
 232      else
 233        b_v_without_open_fence aattr
 234          (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
 235          (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b)
 236          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
 237
 238 (* not *)
 239 Hashtbl.add C2P.symbol_table "not" (unary
 240   (fun a ~priority ~assoc ~tail attr sattr ->
 241      (P.Mrow([], [
 242        m_open_fence; P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
 243        cexpr2pres a; P.Mtext ([], m_close_fence)])))) ;
 244
 245 (* inv *)
 246 Hashtbl.add C2P.symbol_table "inv" (unary
 247   (fun a ~priority ~assoc ~tail attr sattr ->
 248     P.Msup([],
 249       P.Mrow([],[
 250         m_open_fence;
 251         cexpr2pres a;
 252         P.Mtext ([], m_close_fence)]),
 253       P.Mrow([],[
 254         P.Mo([],"-");
 255         P.Mn([],"1")]))));
 256
 257 (* opp *)
 258 Hashtbl.add C2P.symbol_table "opp" (unary
 259   (fun a ~priority ~assoc ~tail attr sattr ->
 260     P.Mrow([],[
 261       P.Mo([],"-");
 262       m_open_fence;
 263       cexpr2pres a;
 264       P.Mtext ([], m_close_fence)])));
 265
 266 (* leq *)
 267 Hashtbl.add C2P.symbol_table "leq" (binary
 268   (fun a b ~priority ~assoc ~tail aattr sattr ->
 269      if (priority > 40) || (priority = 40 && assoc) then
 270        m_row_with_open_fence aattr
 271          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 272          (cexpr2pres ~priority:40 ~assoc:false
 273             ~tail:(m_close_fence::tail) b)
 274          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
 275      else
 276        m_row_without_open_fence aattr
 277          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 278          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 279          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
 280
 281 Hashtbl.add C2P.symbol_table_charcount "leq" (binary
 282   (fun a b ~priority ~assoc ~tail aattr sattr ->
 283      if (priority > 40) || (priority = 40 && assoc) then
 284        b_v_with_open_fence aattr
 285          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 286          (cexpr2pres_charcount ~priority:40 ~assoc:false
 287            ~tail:(b_close_fence::tail) b)
 288          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
 289      else
 290        b_v_without_open_fence aattr
 291          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 292          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 293          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
 294
 295 (* lt *)
 296 Hashtbl.add C2P.symbol_table "lt" (binary
 297   (fun a b ~priority ~assoc ~tail aattr sattr ->
 298      if (priority > 40) || (priority = 40 && assoc) then
 299        m_row_with_open_fence aattr
 300          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 301          (cexpr2pres ~priority:40 ~assoc:false
 302             ~tail:(m_close_fence::tail) b)
 303          (P.Mo(sattr,"&lt;"))
 304      else
 305        m_row_without_open_fence aattr
 306          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 307          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 308          (P.Mo(sattr,"&lt;"))));
 309
 310 Hashtbl.add C2P.symbol_table_charcount "lt" (binary
 311   (fun a b ~priority ~assoc ~tail aattr sattr ->
 312      if (priority > 40) || (priority = 40 && assoc) then
 313        b_v_with_open_fence aattr
 314          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 315          (cexpr2pres_charcount ~priority:40 ~assoc:false
 316            ~tail:(b_close_fence::tail) b)
 317          (P.Mo(sattr,"&lt;"))
 318      else
 319        b_v_without_open_fence aattr
 320          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 321          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 322          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 323
 324 (* geq *)
 325 Hashtbl.add C2P.symbol_table "geq" (binary
 326   (fun a b ~priority ~assoc ~tail aattr sattr ->
 327      if (priority > 40) || (priority = 40 && assoc) then
 328        m_row_with_open_fence aattr
 329          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 330          (cexpr2pres ~priority:40 ~assoc:false
 331             ~tail:(m_close_fence::tail) b)
 332          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
 333      else
 334        m_row_without_open_fence aattr
 335          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 336          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 337          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 338
 339 Hashtbl.add C2P.symbol_table_charcount "geq" (binary
 340   (fun a b ~priority ~assoc ~tail aattr sattr ->
 341      if (priority > 40) || (priority = 40 && assoc) then
 342        b_v_with_open_fence aattr
 343          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 344          (cexpr2pres_charcount ~priority:40 ~assoc:false
 345            ~tail:(b_close_fence::tail) b)
 346          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
 347      else
 348        b_v_without_open_fence aattr
 349          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 350          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 351          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 352
 353 (* gt *)
 354 Hashtbl.add C2P.symbol_table "gt" (binary
 355   (fun a b ~priority ~assoc ~tail aattr sattr ->
 356      if (priority > 40) || (priority = 40 && assoc) then
 357        m_row_with_open_fence aattr
 358          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 359          (cexpr2pres ~priority:40 ~assoc:false
 360             ~tail:(m_close_fence::tail) b)
 361          (P.Mo(sattr,">"))
 362      else
 363        m_row_without_open_fence aattr
 364          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 365          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 366          (P.Mo(sattr,">"))));
 367
 368 Hashtbl.add C2P.symbol_table_charcount "gt" (binary
 369   (fun a b ~priority ~assoc ~tail aattr sattr ->
 370      if (priority > 40) || (priority = 40 && assoc) then
 371        b_v_with_open_fence aattr
 372          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 373          (cexpr2pres_charcount ~priority:40 ~assoc:false
 374            ~tail:(b_close_fence::tail) b)
 375          (P.Mo(sattr,">"))
 376      else
 377        b_v_without_open_fence aattr
 378          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 379          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 380          (P.Mo(sattr,">"))));
 381
 382 (* plus *)
 383 Hashtbl.add C2P.symbol_table "plus" (binary
 384   (fun a b ~priority ~assoc ~tail aattr sattr ->
 385      if (priority > 60) || (priority = 60 && assoc) then
 386        m_row_with_open_fence aattr
 387          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 388          (cexpr2pres ~priority:60 ~assoc:false
 389             ~tail:(m_close_fence::tail) b)
 390          (P.Mo(sattr,"+"))
 391      else
 392        m_row_without_open_fence aattr
 393          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 394          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
 395          (P.Mo(sattr,"+"))));
 396
 397 Hashtbl.add C2P.symbol_table_charcount "plus" (binary
 398   (fun a b ~priority ~assoc ~tail aattr sattr ->
 399      if (priority > 60) || (priority = 60 && assoc) then
 400        b_v_with_open_fence aattr
 401          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 402          (cexpr2pres_charcount ~priority:60 ~assoc:false
 403            ~tail:(b_close_fence::tail) b)
 404          (P.Mo(sattr,"+"))
 405      else
 406        b_v_without_open_fence aattr
 407          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 408          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
 409          (P.Mo(sattr,"+"))));
 410
 411 (* times *)
 412 Hashtbl.add C2P.symbol_table "times" (binary
 413   (fun a b ~priority ~assoc ~tail aattr sattr ->
 414      if (priority > 70) || (priority = 70 && assoc) then
 415        m_row_with_open_fence aattr
 416          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
 417          (cexpr2pres ~priority:70 ~assoc:false
 418             ~tail:(m_close_fence::tail) b)
 419          (P.Mo(sattr,"*"))
 420      else
 421        m_row_without_open_fence aattr
 422          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
 423          (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
 424          (P.Mo(sattr,"*"))));
 425
 426 Hashtbl.add C2P.symbol_table_charcount "times" (binary
 427   (fun a b ~priority ~assoc ~tail aattr sattr ->
 428      if (priority > 70) || (priority = 70 && assoc) then
 429        b_v_with_open_fence aattr
 430          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
 431          (cexpr2pres_charcount ~priority:70 ~assoc:false
 432            ~tail:(b_close_fence::tail) b)
 433          (P.Mo(sattr,"*"))
 434      else
 435        b_v_without_open_fence aattr
 436          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
 437          (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
 438          (P.Mo(sattr,"*"))));
 439
 440 (* minus *)
 441 Hashtbl.add C2P.symbol_table "minus" (binary
 442   (fun a b ~priority ~assoc ~tail aattr sattr ->
 443      if (priority > 60) || (priority = 60 && assoc) then
 444        m_row_with_open_fence aattr
 445          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 446          (cexpr2pres ~priority:60 ~assoc:false
 447             ~tail:(m_close_fence::tail) b)
 448          (P.Mo(sattr,"-"))
 449      else
 450        m_row_without_open_fence aattr
 451          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 452          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
 453          (P.Mo(sattr,"-"))));
 454
 455 Hashtbl.add C2P.symbol_table_charcount "minus" (binary
 456   (fun a b ~priority ~assoc ~tail aattr sattr ->
 457      if (priority > 60) || (priority = 60 && assoc) then
 458        b_v_with_open_fence aattr
 459          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 460          (cexpr2pres_charcount ~priority:60 ~assoc:false
 461            ~tail:(b_close_fence::tail) b)
 462          (P.Mo(sattr,"-"))
 463      else
 464        b_v_without_open_fence aattr
 465          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 466          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
 467          (P.Mo(sattr,"-"))));
 468
 469 (* div *)
 470 Hashtbl.add C2P.symbol_table "div" (binary
 471   (fun a b ~priority ~assoc ~tail aattr sattr ->
 472      if (priority > 60) || (priority = 60 && assoc) then
 473        m_row_with_open_fence aattr
 474          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 475          (cexpr2pres ~priority:60 ~assoc:false
 476             ~tail:(m_close_fence::tail) b)
 477          (P.Mo(sattr,"/"))
 478      else
 479        m_row_without_open_fence aattr
 480          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 481          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
 482          (P.Mo(sattr,"/"))));
 483
 484 Hashtbl.add C2P.symbol_table_charcount "div" (binary
 485   (fun a b ~priority ~assoc ~tail aattr sattr ->
 486      if (priority > 60) || (priority = 60 && assoc) then
 487        b_v_with_open_fence aattr
 488          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 489          (cexpr2pres_charcount ~priority:60 ~assoc:false
 490            ~tail:(b_close_fence::tail) b)
 491          (P.Mo(sattr,"/"))
 492      else
 493        b_v_without_open_fence aattr
 494          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 495          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
 496          (P.Mo(sattr,"/"))))
 497 ;;