X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres_hashtbl.ml;h=79c9943c9985fc3b9839a3aa823a10e2701d2eba;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=657464270b727a8421c2f747a225127eabbbe423;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
index 657464270..79c9943c9 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml
@@ -214,6 +214,27 @@ Hashtbl.add C2P.symbol_table "not" (unary
        P.Mtext([],"(");P.Mo([],Netconversion.ustring_of_uchar `Enc_utf8 0xAC);
        cexpr2pres a;P.Mtext([],")")])));
 
+(* inv *)
+Hashtbl.add C2P.symbol_table "inv" (unary
+  (fun a ~priority ~assoc ~tail attr sattr ->
+    P.Msup([],
+      P.Mrow([],[
+        P.Mtext([],"(");
+        cexpr2pres a;
+        P.Mtext([],")")]),
+      P.Mrow([],[
+        P.Mo([],"-");
+        P.Mn([],"1")]))));
+
+(* opp *)
+Hashtbl.add C2P.symbol_table "opp" (unary
+  (fun a ~priority ~assoc ~tail attr sattr ->
+    P.Mrow([],[
+      P.Mo([],"-");
+      P.Mtext([],"(");
+      cexpr2pres a;
+      P.Mtext([],")")])));
+
 (* leq *)
 Hashtbl.add C2P.symbol_table "leq" (binary
   (fun a b ~priority ~assoc ~tail aattr sattr ->
@@ -415,5 +436,34 @@ Hashtbl.add C2P.symbol_table_charcount "minus" (binary
        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,"-"))))
+         (P.Mo(sattr,"-"))));
+
+(* div *)
+Hashtbl.add C2P.symbol_table "div" (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 "div" (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,"/"))))
 ;;