diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 59 |
1 files changed, 31 insertions, 28 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d7dfe149..028ef95d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -170,6 +170,9 @@ let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]] +let zbase_constant = + gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]] + (* Zarith *) let coq_xH = lazy (constant "xH") @@ -181,20 +184,20 @@ let coq_Zneg = lazy (constant "Zneg") let coq_Z = lazy (constant "Z") let coq_comparison = lazy (constant "comparison") let coq_Gt = lazy (constant "Gt") -let coq_Zplus = lazy (constant "Zplus") -let coq_Zmult = lazy (constant "Zmult") -let coq_Zopp = lazy (constant "Zopp") -let coq_Zminus = lazy (constant "Zminus") -let coq_Zsucc = lazy (constant "Zsucc") -let coq_Zpred = lazy (constant "Zpred") -let coq_Zgt = lazy (constant "Zgt") -let coq_Zle = lazy (constant "Zle") -let coq_Z_of_nat = lazy (constant "Z_of_nat") -let coq_inj_plus = lazy (constant "inj_plus") -let coq_inj_mult = lazy (constant "inj_mult") -let coq_inj_minus1 = lazy (constant "inj_minus1") +let coq_Zplus = lazy (zbase_constant "Z.add") +let coq_Zmult = lazy (zbase_constant "Z.mul") +let coq_Zopp = lazy (zbase_constant "Z.opp") +let coq_Zminus = lazy (zbase_constant "Z.sub") +let coq_Zsucc = lazy (zbase_constant "Z.succ") +let coq_Zpred = lazy (zbase_constant "Z.pred") +let coq_Zgt = lazy (zbase_constant "Z.gt") +let coq_Zle = lazy (zbase_constant "Z.le") +let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat") +let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add") +let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul") +let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub") let coq_inj_minus2 = lazy (constant "inj_minus2") -let coq_inj_S = lazy (z_constant "inj_S") +let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ") let coq_inj_le = lazy (z_constant "Znat.inj_le") let coq_inj_lt = lazy (z_constant "Znat.inj_lt") let coq_inj_ge = lazy (z_constant "Znat.inj_ge") @@ -250,10 +253,10 @@ let coq_Zle_left = lazy (constant "Zle_left") let coq_new_var = lazy (constant "new_var") let coq_intro_Z = lazy (constant "intro_Z") -let coq_dec_eq = lazy (constant "dec_eq") +let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable") let coq_dec_Zne = lazy (constant "dec_Zne") -let coq_dec_Zle = lazy (constant "dec_Zle") -let coq_dec_Zlt = lazy (constant "dec_Zlt") +let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable") +let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable") let coq_dec_Zgt = lazy (constant "dec_Zgt") let coq_dec_Zge = lazy (constant "dec_Zge") @@ -265,10 +268,10 @@ let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt") let coq_Znot_gt_le = lazy (constant "Znot_gt_le") let coq_neq = lazy (constant "neq") let coq_Zne = lazy (constant "Zne") -let coq_Zle = lazy (constant "Zle") -let coq_Zgt = lazy (constant "Zgt") -let coq_Zge = lazy (constant "Zge") -let coq_Zlt = lazy (constant "Zlt") +let coq_Zle = lazy (zbase_constant "Z.le") +let coq_Zgt = lazy (zbase_constant "Z.gt") +let coq_Zge = lazy (zbase_constant "Z.ge") +let coq_Zlt = lazy (zbase_constant "Z.lt") (* Peano/Datatypes *) let coq_le = lazy (init_constant "le") @@ -326,13 +329,13 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with EvalConstRef kn | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant") -let sp_Zsucc = lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc) -let sp_Zpred = lazy (evaluable_ref_of_constr "Zpred" coq_Zpred) -let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus) -let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle) -let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt) -let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge) -let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt) +let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) +let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) +let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) +let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) +let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) +let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) +let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ()))) let mk_var v = mkVar (id_of_string v) |