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 uri s = UriManager.uri_of_string s in
69 let const s = Cic.Const (uri s, []) in
70 let mutind s = Cic.MutInd (uri s, 0, []) in
72 DisambiguateChoices.add_num_choice
74 (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
75 DisambiguateChoices.add_num_choice
77 (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
79 DisambiguateChoices.add_binary_op "plus" "natural plus"
80 HelmLibraryObjects.Peano.plus;
81 DisambiguateChoices.add_binary_op "plus" "real plus"
82 HelmLibraryObjects.Reals.rplus;
83 DisambiguateChoices.add_binary_op "minus" "natural minus"
84 (const "cic:/Coq/Arith/Minus/minus.con");
85 DisambiguateChoices.add_binary_op "minus" "real minus"
86 (const "cic:/Coq/Reals/Rdefinitions/Rminus.con");
87 DisambiguateChoices.add_binary_op "times" "natural times"
88 (const "cic:/Coq/Init/Peano/mult.con");
89 DisambiguateChoices.add_binary_op "times" "real times"
90 (const "cic:/Coq/Reals/Rdefinitions/Rmult.con");
91 DisambiguateChoices.add_binary_op "divide" "real divide"
92 (const "cic:/Coq/Reals/Rdefinitions/Rdiv.con");
93 DisambiguateChoices.add_unary_op "uminus" "real unary minus"
94 (const "cic:/Coq/Reals/Rdefinitions/Ropp.con");
96 DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'"
97 (mutind "cic:/Coq/Init/Peano/le.ind");
98 DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'"
99 (const "cic:/Coq/Reals/Rdefinitions/Rle.con");
100 DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'"
101 (const "cic:/Coq/Init/Peano/ge.con");
102 DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'"
103 (const "cic:/Coq/Reals/Rdefinitions/Rge.con");
104 DisambiguateChoices.add_binary_op "lt" "natural 'less than'"
105 (const "cic:/Coq/Init/Peano/lt.con");
106 DisambiguateChoices.add_binary_op "lt" "real 'less than'"
107 (const "cic:/Coq/Reals/Rdefinitions/Rlt.con");
108 DisambiguateChoices.add_binary_op "gt" "natural 'greater than'"
109 (const "cic:/Coq/Init/Peano/gt.con");
110 DisambiguateChoices.add_binary_op "gt" "real 'greater than'"
111 (const "cic:/Coq/Reals/Rdefinitions/Rgt.con");
112 DisambiguateChoices.add_symbol_choice "neq"
113 ("not equal to (leibnitz)",
118 | _ -> raise DisambiguateChoices.Invalid_choice
120 Cic.Appl [ const "cic:/Coq/Init/Logic/not.con";
122 Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
123 Cic.Implicit (Some `Type); t1; t2 ] ]));
124 DisambiguateChoices.add_symbol_choice "neq"
125 ("not equal to (sort Type)",
130 | _ -> raise DisambiguateChoices.Invalid_choice
132 Cic.Appl [ const "cic:/Coq/Init/Logic/not.con";
134 Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
135 Cic.Implicit (Some `Type); t1; t2 ] ]));