X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Farit_notation.ml;fp=helm%2Focaml%2Fcic_disambiguation%2Farit_notation.ml;h=0000000000000000000000000000000000000000;hp=780fed363d575f473f6056607970cdc39e127ccd;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml deleted file mode 100644 index 780fed363..000000000 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ /dev/null @@ -1,170 +0,0 @@ -(* Copyright (C) 2004, 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://helm.cs.unibo.it/ - *) - -open CicTextualParser2 - -EXTEND - term: LEVEL "add" - [ - [ t1 = term; SYMBOL "+"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("plus", 0); t1; t2]) - | t1 = term; SYMBOL "-"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("minus", 0); t1; t2]) - ] - ]; - term: LEVEL "mult" - [ - [ t1 = term; SYMBOL "*"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2]) - | t1 = term; SYMBOL "/"; t2 = term -> - 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 -> - return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t]) - ] - ]; - term: LEVEL "relop" - [ - [ t1 = term; SYMBOL <:unicode> (* ≤ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("leq", 0); t1; t2]) - | t1 = term; SYMBOL <:unicode> (* ≥ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("geq", 0); t1; t2]) - | t1 = term; SYMBOL "<"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("lt", 0); t1; t2]) - | t1 = term; SYMBOL ">"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("gt", 0); t1; t2]) - | t1 = term; SYMBOL <:unicode> (* ≠ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("neq", 0); t1; t2]) - ] - ]; -END - -let _ = - let const s = Cic.Const (s, []) in - let mutind s = Cic.MutInd (s, 0, []) in - - DisambiguateChoices.add_num_choice - ("natural number", - (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); - 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 HelmLibraryObjects.Peano.minus_URI); - DisambiguateChoices.add_binary_op "minus" "real minus" - (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 HelmLibraryObjects.Peano.mult_URI); - DisambiguateChoices.add_binary_op "times" "real times" - (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 HelmLibraryObjects.Reals.rdiv_URI); - DisambiguateChoices.add_unary_op "uminus" "real unary minus" - (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 HelmLibraryObjects.Peano.le_URI); - DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'" - (const HelmLibraryObjects.Reals.rle_URI); - DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'" - (const HelmLibraryObjects.Peano.ge_URI); - DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'" - (const HelmLibraryObjects.Reals.rge_URI); - DisambiguateChoices.add_binary_op "lt" "natural 'less than'" - (const HelmLibraryObjects.Peano.lt_URI); - DisambiguateChoices.add_binary_op "lt" "real 'less than'" - (const HelmLibraryObjects.Reals.rlt_URI); - DisambiguateChoices.add_binary_op "gt" "natural 'greater than'" - (const HelmLibraryObjects.Peano.gt_URI); - DisambiguateChoices.add_binary_op "gt" "real 'greater than'" - (const HelmLibraryObjects.Reals.rgt_URI); - DisambiguateChoices.add_symbol_choice "neq" - ("not equal to (leibnitz)", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - Cic.Implicit (Some `Type); t1; t2 ] ])); - -(* vim:set encoding=utf8: *)