+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(**************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti <asperti@cs.unibo.it> *)
-(* 28/6/2003 *)
-(* *)
-(**************************************************************************)
-
-module C2P = Cexpr2pres;;
-module P = Mpresentation;;
-
-let binary f =
- function
- [a;b] -> f a b
- | _ -> assert false
-;;
-
-let unary f =
- function
- [a] -> f a
- | _ -> assert false
-;;
-
-let init
- ~(cexpr2pres:
- ?priority:int ->
- ?assoc:bool ->
- ?tail:Mpresentation.mpres list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres)
- ~(cexpr2pres_charcount:
- ?priority:int ->
- ?assoc:bool ->
- ?tail:Mpresentation.mpres list ->
- Content_expressions.cexpr ->
- Mpresentation.mpres)
-=
-
-(* arrow *)
-Hashtbl.add C2P.symbol_table "arrow" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:true
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:true ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
-
-Hashtbl.add C2P.symbol_table_charcount "arrow" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:true
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2192))));
-
-(* eq *)
-Hashtbl.add C2P.symbol_table "eq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"="))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"="))));
-
-Hashtbl.add C2P.symbol_table_charcount "eq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"="))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"="))));
-
-(* and *)
-Hashtbl.add C2P.symbol_table "and" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 20) || (priority = 20 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:20 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:20 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
-
-Hashtbl.add C2P.symbol_table_charcount "and" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 20) || (priority = 20 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:20 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:20 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:20 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2227))));
-
-(* or *)
-Hashtbl.add C2P.symbol_table "or" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 10) || (priority = 10 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:10 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:10 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
-
-Hashtbl.add C2P.symbol_table_charcount "or" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 10) || (priority = 10 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:10 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:10 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:10 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2228))));
-
-(* iff *)
-Hashtbl.add C2P.symbol_table "iff" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:5 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
-
-Hashtbl.add C2P.symbol_table_charcount "iff" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 5) || (priority = 5 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:5 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:5 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x21D4))));
-
-(* not *)
-Hashtbl.add C2P.symbol_table "not" (unary
- (fun a ~priority ~assoc ~tail attr sattr ->
- P.Mrow([],[
- P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
- cexpr2pres a;P.Mtext([],")")])));
-
-(* leq *)
-Hashtbl.add C2P.symbol_table "leq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
-
-Hashtbl.add C2P.symbol_table_charcount "leq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2264))));
-
-(* lt *)
-Hashtbl.add C2P.symbol_table "lt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"<"))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"<"))));
-
-Hashtbl.add C2P.symbol_table_charcount "lt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"<"))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-(* geq *)
-Hashtbl.add C2P.symbol_table "geq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-Hashtbl.add C2P.symbol_table_charcount "geq" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,Netconversion.ustring_of_uchar `Enc_utf8 0x2265))));
-
-(* gt *)
-Hashtbl.add C2P.symbol_table "gt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,">"))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,">"))));
-
-Hashtbl.add C2P.symbol_table_charcount "gt" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 40) || (priority = 40 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,">"))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:40 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:40 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,">"))));
-
-(* plus *)
-Hashtbl.add C2P.symbol_table "plus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"+"))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"+"))));
-
-Hashtbl.add C2P.symbol_table_charcount "plus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"+"))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"+"))));
-
-(* times *)
-Hashtbl.add C2P.symbol_table "times" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 70) || (priority = 70 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:70 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"*"))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:70 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"*"))));
-
-Hashtbl.add C2P.symbol_table_charcount "times" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 70) || (priority = 70 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:70 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"*"))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:70 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:70 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"*"))));
-
-(* minus *)
-Hashtbl.add C2P.symbol_table "minus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- P.row_with_brackets aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"-"))
- else
- P.row_without_brackets aattr
- (cexpr2pres ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"-"))));
-
-Hashtbl.add C2P.symbol_table_charcount "minus" (binary
- (fun a b ~priority ~assoc ~tail aattr sattr ->
- if (priority > 60) || (priority = 60 && assoc) then
- P.two_rows_table_with_brackets aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false
- ~tail:(P.Mtext([],")")::tail) b)
- (P.Mo(sattr,"-"))
- else
- P.two_rows_table_without_brackets aattr
- (cexpr2pres_charcount ~priority:60 ~assoc:true ~tail:[] a)
- (cexpr2pres_charcount ~priority:60 ~assoc:false ~tail:tail b)
- (P.Mo(sattr,"-"))))
-;;
projects / helm.git / blobdiff