1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 open CicTextualParser2
31 [ t1 = term; SYMBOL "+"; t2 = term ->
32 return_term loc (CicAst.Appl [CicAst.Symbol ("plus", 0); t1; t2])
33 | t1 = term; SYMBOL "-"; t2 = term ->
34 return_term loc (CicAst.Appl [CicAst.Symbol ("minus", 0); t1; t2])
39 [ t1 = term; SYMBOL "*"; t2 = term ->
40 return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2])
41 | t1 = term; SYMBOL "/"; t2 = term ->
42 return_term loc (CicAst.Appl [CicAst.Symbol ("divide", 0); t1; t2])
47 [ SYMBOL "-"; t = term ->
48 return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t])
53 [ t1 = term; SYMBOL <:unicode<leq>> (* ≤ *); t2 = term ->
54 return_term loc (CicAst.Appl [CicAst.Symbol ("leq", 0); t1; t2])
55 | t1 = term; SYMBOL <:unicode<geq>> (* ≥ *); t2 = term ->
56 return_term loc (CicAst.Appl [CicAst.Symbol ("geq", 0); t1; t2])
57 | t1 = term; SYMBOL "<"; t2 = term ->
58 return_term loc (CicAst.Appl [CicAst.Symbol ("lt", 0); t1; t2])
59 | t1 = term; SYMBOL ">"; t2 = term ->
60 return_term loc (CicAst.Appl [CicAst.Symbol ("gt", 0); t1; t2])
61 | t1 = term; SYMBOL <:unicode<ne>> (* ≠ *); t2 = term ->
62 return_term loc (CicAst.Appl [CicAst.Symbol ("neq", 0); t1; t2])
68 let const s = Cic.Const (s, []) in
69 let mutind s = Cic.MutInd (s, 0, []) in
71 DisambiguateChoices.add_num_choice
73 (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
74 DisambiguateChoices.add_num_choice
76 (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
78 DisambiguateChoices.add_binary_op "plus" "natural plus"
79 HelmLibraryObjects.Peano.plus;
80 DisambiguateChoices.add_binary_op "plus" "real plus"
81 HelmLibraryObjects.Reals.rplus;
82 DisambiguateChoices.add_binary_op "minus" "natural minus"
83 (const HelmLibraryObjects.Peano.minus_URI);
84 DisambiguateChoices.add_binary_op "minus" "real minus"
85 (const HelmLibraryObjects.Reals.rminus_URI);
86 DisambiguateChoices.add_binary_op "times" "natural times"
87 (const HelmLibraryObjects.Peano.mult_URI);
88 DisambiguateChoices.add_binary_op "times" "real times"
89 (const HelmLibraryObjects.Reals.rmult_URI);
90 DisambiguateChoices.add_binary_op "divide" "real divide"
91 (const HelmLibraryObjects.Reals.rdiv_URI);
92 DisambiguateChoices.add_unary_op "uminus" "real unary minus"
93 (const HelmLibraryObjects.Reals.ropp_URI);
95 DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'"
96 (mutind HelmLibraryObjects.Peano.le_URI);
97 DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'"
98 (const HelmLibraryObjects.Reals.rle_URI);
99 DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'"
100 (const HelmLibraryObjects.Peano.ge_URI);
101 DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'"
102 (const HelmLibraryObjects.Reals.rge_URI);
103 DisambiguateChoices.add_binary_op "lt" "natural 'less than'"
104 (const HelmLibraryObjects.Peano.lt_URI);
105 DisambiguateChoices.add_binary_op "lt" "real 'less than'"
106 (const HelmLibraryObjects.Reals.rlt_URI);
107 DisambiguateChoices.add_binary_op "gt" "natural 'greater than'"
108 (const HelmLibraryObjects.Peano.gt_URI);
109 DisambiguateChoices.add_binary_op "gt" "real 'greater than'"
110 (const HelmLibraryObjects.Reals.rgt_URI);
111 DisambiguateChoices.add_symbol_choice "neq"
112 ("not equal to (leibnitz)",
117 | _ -> raise DisambiguateChoices.Invalid_choice
119 Cic.Appl [ const HelmLibraryObjects.Logic.not_URI;
121 Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
122 Cic.Implicit (Some `Type); t1; t2 ] ]));