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