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)));
77 DisambiguateChoices.add_num_choice
78 ("binary positive number",
80 let num = int_of_string num in
82 raise DisambiguateChoices.Invalid_choice
84 HelmLibraryObjects.build_bin_pos num));
85 DisambiguateChoices.add_num_choice
86 ("binary integer number",
88 let num = int_of_string num in
90 HelmLibraryObjects.BinInt.z0
93 HelmLibraryObjects.BinInt.zpos;
94 HelmLibraryObjects.build_bin_pos num ]
98 DisambiguateChoices.add_binary_op "plus" "natural plus"
99 HelmLibraryObjects.Peano.plus;
100 DisambiguateChoices.add_binary_op "plus" "real plus"
101 HelmLibraryObjects.Reals.rplus;
102 DisambiguateChoices.add_binary_op "plus" "binary integer plus"
103 HelmLibraryObjects.BinInt.zplus;
104 DisambiguateChoices.add_binary_op "plus" "binary positive plus"
105 HelmLibraryObjects.BinPos.pplus;
106 DisambiguateChoices.add_binary_op "minus" "natural minus"
107 (const HelmLibraryObjects.Peano.minus_URI);
108 DisambiguateChoices.add_binary_op "minus" "real minus"
109 (const HelmLibraryObjects.Reals.rminus_URI);
110 DisambiguateChoices.add_binary_op "minus" "binary integer minus"
111 HelmLibraryObjects.BinInt.zminus;
112 DisambiguateChoices.add_binary_op "minus" "binary positive minus"
113 HelmLibraryObjects.BinPos.pminus;
114 DisambiguateChoices.add_binary_op "times" "natural times"
115 (const HelmLibraryObjects.Peano.mult_URI);
116 DisambiguateChoices.add_binary_op "times" "real times"
117 (const HelmLibraryObjects.Reals.rmult_URI);
118 DisambiguateChoices.add_binary_op "times" "binary positive times"
119 HelmLibraryObjects.BinPos.pmult;
120 DisambiguateChoices.add_binary_op "divide" "real divide"
121 (const HelmLibraryObjects.Reals.rdiv_URI);
122 DisambiguateChoices.add_unary_op "uminus" "real unary minus"
123 (const HelmLibraryObjects.Reals.ropp_URI);
124 DisambiguateChoices.add_unary_op "uminus" "binary integer negative sign"
125 (HelmLibraryObjects.BinInt.zneg);
126 DisambiguateChoices.add_unary_op "uminus" "binary integer unary minus"
127 (HelmLibraryObjects.BinInt.zopp);
129 DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'"
130 (mutind HelmLibraryObjects.Peano.le_URI);
131 DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'"
132 (const HelmLibraryObjects.Reals.rle_URI);
133 DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'"
134 (const HelmLibraryObjects.Peano.ge_URI);
135 DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'"
136 (const HelmLibraryObjects.Reals.rge_URI);
137 DisambiguateChoices.add_binary_op "lt" "natural 'less than'"
138 (const HelmLibraryObjects.Peano.lt_URI);
139 DisambiguateChoices.add_binary_op "lt" "real 'less than'"
140 (const HelmLibraryObjects.Reals.rlt_URI);
141 DisambiguateChoices.add_binary_op "gt" "natural 'greater than'"
142 (const HelmLibraryObjects.Peano.gt_URI);
143 DisambiguateChoices.add_binary_op "gt" "real 'greater than'"
144 (const HelmLibraryObjects.Reals.rgt_URI);
145 DisambiguateChoices.add_symbol_choice "neq"
146 ("not equal to (leibnitz)",
151 | _ -> raise DisambiguateChoices.Invalid_choice
153 Cic.Appl [ const HelmLibraryObjects.Logic.not_URI;
155 Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
156 Cic.Implicit (Some `Type); t1; t2 ] ]));
158 (* vim:set encoding=utf8: *)