X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Farit_notation.ml;h=780fed363d575f473f6056607970cdc39e127ccd;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=b249427755ba71065e4482cc5b5739671c3394f8;hpb=45586ab88c026e6a21927654387b6df266a44700;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index b24942775..780fed363 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -42,6 +42,12 @@ EXTEND return_term loc (CicAst.Appl [CicAst.Symbol ("divide", 0); t1; t2]) ] ]; + term: LEVEL "power" + [ + [ t1 = term; SYMBOL "^"; t2 = term -> + return_term loc (CicAst.Appl [CicAst.Symbol ("power", 0); t1; t2]) + ] + ]; term: LEVEL "inv" [ [ SYMBOL "-"; t = term -> @@ -65,9 +71,8 @@ EXTEND END let _ = - let uri s = UriManager.uri_of_string s in - let const s = Cic.Const (uri s, []) in - let mutind s = Cic.MutInd (uri s, 0, []) in + let const s = Cic.Const (s, []) in + let mutind s = Cic.MutInd (s, 0, []) in DisambiguateChoices.add_num_choice ("natural number", @@ -75,40 +80,80 @@ let _ = DisambiguateChoices.add_num_choice ("real number", (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); + DisambiguateChoices.add_num_choice + ("binary positive number", + (fun _ num _ -> + let num = int_of_string num in + if num = 0 then + raise DisambiguateChoices.Invalid_choice + else + HelmLibraryObjects.build_bin_pos num)); + DisambiguateChoices.add_num_choice + ("binary integer number", + (fun _ num _ -> + let num = int_of_string num in + if num = 0 then + HelmLibraryObjects.BinInt.z0 + else if num > 0 then + Cic.Appl [ + HelmLibraryObjects.BinInt.zpos; + HelmLibraryObjects.build_bin_pos num ] + else + assert false)); DisambiguateChoices.add_binary_op "plus" "natural plus" HelmLibraryObjects.Peano.plus; DisambiguateChoices.add_binary_op "plus" "real plus" HelmLibraryObjects.Reals.rplus; + DisambiguateChoices.add_binary_op "plus" "binary integer plus" + HelmLibraryObjects.BinInt.zplus; + DisambiguateChoices.add_binary_op "plus" "binary positive plus" + HelmLibraryObjects.BinPos.pplus; DisambiguateChoices.add_binary_op "minus" "natural minus" - (const "cic:/Coq/Arith/Minus/minus.con"); + (const HelmLibraryObjects.Peano.minus_URI); DisambiguateChoices.add_binary_op "minus" "real minus" - (const "cic:/Coq/Reals/Rdefinitions/Rminus.con"); + (const HelmLibraryObjects.Reals.rminus_URI); + DisambiguateChoices.add_binary_op "minus" "binary integer minus" + HelmLibraryObjects.BinInt.zminus; + DisambiguateChoices.add_binary_op "minus" "binary positive minus" + HelmLibraryObjects.BinPos.pminus; DisambiguateChoices.add_binary_op "times" "natural times" - (const "cic:/Coq/Init/Peano/mult.con"); + (const HelmLibraryObjects.Peano.mult_URI); DisambiguateChoices.add_binary_op "times" "real times" - (const "cic:/Coq/Reals/Rdefinitions/Rmult.con"); + (const HelmLibraryObjects.Reals.rmult_URI); + DisambiguateChoices.add_binary_op "times" "binary positive times" + HelmLibraryObjects.BinPos.pmult; + DisambiguateChoices.add_binary_op "times" "binary integer times" + HelmLibraryObjects.BinInt.zmult; + DisambiguateChoices.add_binary_op "power" "real power" + (const HelmLibraryObjects.Reals.pow_URI); + DisambiguateChoices.add_binary_op "power" "integer power" + (const HelmLibraryObjects.BinInt.zpower_URI); DisambiguateChoices.add_binary_op "divide" "real divide" - (const "cic:/Coq/Reals/Rdefinitions/Rdiv.con"); + (const HelmLibraryObjects.Reals.rdiv_URI); DisambiguateChoices.add_unary_op "uminus" "real unary minus" - (const "cic:/Coq/Reals/Rdefinitions/Ropp.con"); + (const HelmLibraryObjects.Reals.ropp_URI); + DisambiguateChoices.add_unary_op "uminus" "binary integer negative sign" + (HelmLibraryObjects.BinInt.zneg); + DisambiguateChoices.add_unary_op "uminus" "binary integer unary minus" + (HelmLibraryObjects.BinInt.zopp); DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'" - (mutind "cic:/Coq/Init/Peano/le.ind"); + (mutind HelmLibraryObjects.Peano.le_URI); DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'" - (const "cic:/Coq/Reals/Rdefinitions/Rle.con"); + (const HelmLibraryObjects.Reals.rle_URI); DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'" - (const "cic:/Coq/Init/Peano/ge.con"); + (const HelmLibraryObjects.Peano.ge_URI); DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'" - (const "cic:/Coq/Reals/Rdefinitions/Rge.con"); + (const HelmLibraryObjects.Reals.rge_URI); DisambiguateChoices.add_binary_op "lt" "natural 'less than'" - (const "cic:/Coq/Init/Peano/lt.con"); + (const HelmLibraryObjects.Peano.lt_URI); DisambiguateChoices.add_binary_op "lt" "real 'less than'" - (const "cic:/Coq/Reals/Rdefinitions/Rlt.con"); + (const HelmLibraryObjects.Reals.rlt_URI); DisambiguateChoices.add_binary_op "gt" "natural 'greater than'" - (const "cic:/Coq/Init/Peano/gt.con"); + (const HelmLibraryObjects.Peano.gt_URI); DisambiguateChoices.add_binary_op "gt" "real 'greater than'" - (const "cic:/Coq/Reals/Rdefinitions/Rgt.con"); + (const HelmLibraryObjects.Reals.rgt_URI); DisambiguateChoices.add_symbol_choice "neq" ("not equal to (leibnitz)", (fun env _ args -> @@ -117,20 +162,9 @@ let _ = | [t1; t2] -> t1, t2 | _ -> raise DisambiguateChoices.Invalid_choice in - Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; + Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 ] ])); - DisambiguateChoices.add_symbol_choice "neq" - ("not equal to (sort Type)", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); - Cic.Implicit (Some `Type); t1; t2 ] ])); +(* vim:set encoding=utf8: *)