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 (* leq *)
 218 Hashtbl.add C2P.symbol_table "leq" (binary
 219   (fun a b ~priority ~assoc ~tail aattr sattr ->
 220      if (priority > 40) || (priority = 40 && assoc) then
 221        P.row_with_brackets aattr
 222          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 223          (cexpr2pres ~priority:40 ~assoc:false
 224             ~tail:(P.Mtext([],")")::tail) b)
 225          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
 226      else
 227        P.row_without_brackets aattr
 228          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 229          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 230          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
 231
 232 Hashtbl.add C2P.symbol_table_charcount "leq" (binary
 233   (fun a b ~priority ~assoc ~tail aattr sattr ->
 234      if (priority > 40) || (priority = 40 && assoc) then
 235        P.two_rows_table_with_brackets aattr
 236          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 237          (cexpr2pres_charcount ~priority:40 ~assoc:false
 238            ~tail:(P.Mtext([],")")::tail) b)
 239          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
 240      else
 241        P.two_rows_table_without_brackets aattr
 242          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 243          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 244          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
 245
 246 (* lt *)
 247 Hashtbl.add C2P.symbol_table "lt" (binary
 248   (fun a b ~priority ~assoc ~tail aattr sattr ->
 249      if (priority > 40) || (priority = 40 && assoc) then
 250        P.row_with_brackets aattr
 251          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 252          (cexpr2pres ~priority:40 ~assoc:false
 253             ~tail:(P.Mtext([],")")::tail) b)
 254          (P.Mo(sattr,"&lt;"))
 255      else
 256        P.row_without_brackets aattr
 257          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 258          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 259          (P.Mo(sattr,"&lt;"))));
 260
 261 Hashtbl.add C2P.symbol_table_charcount "lt" (binary
 262   (fun a b ~priority ~assoc ~tail aattr sattr ->
 263      if (priority > 40) || (priority = 40 && assoc) then
 264        P.two_rows_table_with_brackets aattr
 265          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 266          (cexpr2pres_charcount ~priority:40 ~assoc:false
 267            ~tail:(P.Mtext([],")")::tail) b)
 268          (P.Mo(sattr,"&lt;"))
 269      else
 270        P.two_rows_table_without_brackets aattr
 271          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 272          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 273          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 274
 275 (* geq *)
 276 Hashtbl.add C2P.symbol_table "geq" (binary
 277   (fun a b ~priority ~assoc ~tail aattr sattr ->
 278      if (priority > 40) || (priority = 40 && assoc) then
 279        P.row_with_brackets aattr
 280          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 281          (cexpr2pres ~priority:40 ~assoc:false
 282             ~tail:(P.Mtext([],")")::tail) b)
 283          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
 284      else
 285        P.row_without_brackets aattr
 286          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 287          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 288          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 289
 290 Hashtbl.add C2P.symbol_table_charcount "geq" (binary
 291   (fun a b ~priority ~assoc ~tail aattr sattr ->
 292      if (priority > 40) || (priority = 40 && assoc) then
 293        P.two_rows_table_with_brackets aattr
 294          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 295          (cexpr2pres_charcount ~priority:40 ~assoc:false
 296            ~tail:(P.Mtext([],")")::tail) b)
 297          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
 298      else
 299        P.two_rows_table_without_brackets aattr
 300          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 301          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 302          (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
 303
 304 (* gt *)
 305 Hashtbl.add C2P.symbol_table "gt" (binary
 306   (fun a b ~priority ~assoc ~tail aattr sattr ->
 307      if (priority > 40) || (priority = 40 && assoc) then
 308        P.row_with_brackets aattr
 309          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 310          (cexpr2pres ~priority:40 ~assoc:false
 311             ~tail:(P.Mtext([],")")::tail) b)
 312          (P.Mo(sattr,">"))
 313      else
 314        P.row_without_brackets aattr
 315          (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
 316          (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
 317          (P.Mo(sattr,">"))));
 318
 319 Hashtbl.add C2P.symbol_table_charcount "gt" (binary
 320   (fun a b ~priority ~assoc ~tail aattr sattr ->
 321      if (priority > 40) || (priority = 40 && assoc) then
 322        P.two_rows_table_with_brackets aattr
 323          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 324          (cexpr2pres_charcount ~priority:40 ~assoc:false
 325            ~tail:(P.Mtext([],")")::tail) b)
 326          (P.Mo(sattr,">"))
 327      else
 328        P.two_rows_table_without_brackets aattr
 329          (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
 330          (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
 331          (P.Mo(sattr,">"))));
 332
 333 (* plus *)
 334 Hashtbl.add C2P.symbol_table "plus" (binary
 335   (fun a b ~priority ~assoc ~tail aattr sattr ->
 336      if (priority > 60) || (priority = 60 && assoc) then
 337        P.row_with_brackets aattr
 338          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 339          (cexpr2pres ~priority:60 ~assoc:false
 340             ~tail:(P.Mtext([],")")::tail) b)
 341          (P.Mo(sattr,"+"))
 342      else
 343        P.row_without_brackets aattr
 344          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 345          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
 346          (P.Mo(sattr,"+"))));
 347
 348 Hashtbl.add C2P.symbol_table_charcount "plus" (binary
 349   (fun a b ~priority ~assoc ~tail aattr sattr ->
 350      if (priority > 60) || (priority = 60 && assoc) then
 351        P.two_rows_table_with_brackets aattr
 352          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 353          (cexpr2pres_charcount ~priority:60 ~assoc:false
 354            ~tail:(P.Mtext([],")")::tail) b)
 355          (P.Mo(sattr,"+"))
 356      else
 357        P.two_rows_table_without_brackets aattr
 358          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 359          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
 360          (P.Mo(sattr,"+"))));
 361
 362 (* times *)
 363 Hashtbl.add C2P.symbol_table "times" (binary
 364   (fun a b ~priority ~assoc ~tail aattr sattr ->
 365      if (priority > 70) || (priority = 70 && assoc) then
 366        P.row_with_brackets aattr
 367          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
 368          (cexpr2pres ~priority:70 ~assoc:false
 369             ~tail:(P.Mtext([],")")::tail) b)
 370          (P.Mo(sattr,"*"))
 371      else
 372        P.row_without_brackets aattr
 373          (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
 374          (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
 375          (P.Mo(sattr,"*"))));
 376
 377 Hashtbl.add C2P.symbol_table_charcount "times" (binary
 378   (fun a b ~priority ~assoc ~tail aattr sattr ->
 379      if (priority > 70) || (priority = 70 && assoc) then
 380        P.two_rows_table_with_brackets aattr
 381          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
 382          (cexpr2pres_charcount ~priority:70 ~assoc:false
 383            ~tail:(P.Mtext([],")")::tail) b)
 384          (P.Mo(sattr,"*"))
 385      else
 386        P.two_rows_table_without_brackets aattr
 387          (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
 388          (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
 389          (P.Mo(sattr,"*"))));
 390
 391 (* minus *)
 392 Hashtbl.add C2P.symbol_table "minus" (binary
 393   (fun a b ~priority ~assoc ~tail aattr sattr ->
 394      if (priority > 60) || (priority = 60 && assoc) then
 395        P.row_with_brackets aattr
 396          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 397          (cexpr2pres ~priority:60 ~assoc:false
 398             ~tail:(P.Mtext([],")")::tail) b)
 399          (P.Mo(sattr,"-"))
 400      else
 401        P.row_without_brackets aattr
 402          (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
 403          (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
 404          (P.Mo(sattr,"-"))));
 405
 406 Hashtbl.add C2P.symbol_table_charcount "minus" (binary
 407   (fun a b ~priority ~assoc ~tail aattr sattr ->
 408      if (priority > 60) || (priority = 60 && assoc) then
 409        P.two_rows_table_with_brackets aattr
 410          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 411          (cexpr2pres_charcount ~priority:60 ~assoc:false
 412            ~tail:(P.Mtext([],")")::tail) b)
 413          (P.Mo(sattr,"-"))
 414      else
 415        P.two_rows_table_without_brackets aattr
 416          (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
 417          (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
 418          (P.Mo(sattr,"-"))))
 419 ;;