From 4a5311d795b19019a675f60c33710301873f646c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Sep 2003 12:34:07 +0000 Subject: [PATCH] Notation for Rdiv and Rminus. --- .../cic_transformations/cexpr2pres_hashtbl.ml | 31 ++++++++++++++++++- .../content_expressions.ml | 15 +++++++++ 2 files changed, 45 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml index 657464270..676b55dc4 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres_hashtbl.ml @@ -415,5 +415,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,"/")))) ;; diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 717b4e925..22f959927 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -235,6 +235,21 @@ Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" None, Some "cic:/Coq/Arith/Minus/mult.con")) :: List.map acic2cexpr args));; +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "minus", + None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con")) + :: List.map acic2cexpr args));; + +(* div *) +Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "div", + None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con")) + :: List.map acic2cexpr args));; + -- 2.39.2