aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/Omega.v10
-rw-r--r--plugins/omega/OmegaLemmas.v16
-rw-r--r--plugins/omega/OmegaPlugin.v10
-rw-r--r--plugins/omega/OmegaTactic.v10
-rw-r--r--plugins/omega/PreOmega.v16
-rw-r--r--plugins/omega/coq_omega.ml66
-rw-r--r--plugins/omega/g_omega.ml412
-rw-r--r--plugins/omega/omega.ml10
8 files changed, 84 insertions, 66 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index a53a38d35b..6c8f23a012 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(**************************************************************************)
(* *)
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index 1872f57662..dc86a98998 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(***********************************************************************)
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
Require Import BinInt Znat.
Local Open Scope Z_scope.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index ce187892d4..3c339c8b8f 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* To strictly import the omega tactic *)
diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v
index ce187892d4..3c339c8b8f 100644
--- a/plugins/omega/OmegaTactic.v
+++ b/plugins/omega/OmegaTactic.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* To strictly import the omega tactic *)
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 8da45e0ad1..59fd9b8017 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Arith Max Min BinInt BinNat Znat Nnat.
@@ -26,7 +28,7 @@ Local Open Scope Z_scope.
- on Z: Z.min, Z.max, Z.abs, Z.sgn are translated in term of <= < =
- on nat: + * - S O pred min max Pos.to_nat N.to_nat Z.abs_nat
- on positive: Zneg Zpos xI xO xH + * - Pos.succ Pos.pred Pos.min Pos.max Pos.of_succ_nat
- - on N: N0 Npos + * - N.succ N.min N.max N.of_nat Z.abs_N
+ - on N: N0 Npos + * - N.pred N.succ N.min N.max N.of_nat Z.abs_N
*)
@@ -391,6 +393,10 @@ Ltac zify_N_op :=
| H : context [ Z.of_N (N.sub ?a ?b) ] |- _ => rewrite (N2Z.inj_sub_max a b) in H
| |- context [ Z.of_N (N.sub ?a ?b) ] => rewrite (N2Z.inj_sub_max a b)
+ (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *)
+ | H : context [ Z.of_N (N.pred ?a) ] |- _ => rewrite (N.pred_sub a) in H
+ | |- context [ Z.of_N (N.pred ?a) ] => rewrite (N.pred_sub a)
+
(* N.succ -> Z.succ *)
| H : context [ Z.of_N (N.succ ?a) ] |- _ => rewrite (N2Z.inj_succ a) in H
| |- context [ Z.of_N (N.succ ?a) ] => rewrite (N2Z.inj_succ a)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ff69ddefb8..51cd665f62 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(**************************************************************************)
(* *)
@@ -466,12 +468,14 @@ let destructurate_prop sigma t =
| Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
| _ -> Kufo
-let destructurate_type sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let c, args = decompose_app sigma t in
+let nf = Tacred.simpl
+
+let destructurate_type env sigma t =
+ let is_conv = Reductionops.is_conv env sigma in
+ let c, args = decompose_app sigma (nf env sigma t) in
match EConstr.kind sigma c, args with
- | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
- | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
+ | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args)
+ | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args)
| _ -> Kufo
let destructurate_term sigma t =
@@ -650,7 +654,7 @@ let decompile af =
(** Backward compat to emulate the old Refine: normalize the goal conclusion *)
let new_hole env sigma c =
- let c = Reductionops.nf_betaiota sigma c in
+ let c = Reductionops.nf_betaiota env sigma c in
Evarutil.new_evar env sigma c
let clever_rewrite_base_poly typ p result theorem =
@@ -1459,17 +1463,13 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
else
(tactic,defs)
-let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
-
-let destructure_omega gl tac_def (id,c) =
- let open Tacmach.New in
- let sigma = project gl in
+let destructure_omega env sigma tac_def (id,c) =
if String.equal (atompart_of_id id) "State" then
tac_def
else
try match destructurate_prop sigma c with
| Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
+ when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end ->
let t = mk_plus t1 (mk_inv t2) in
normalize_equation sigma
id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1507,7 +1507,7 @@ let coq_omega =
Proofview.Goal.enter begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = destructure_omega gl in
+ let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1727,27 +1727,26 @@ let not_binop = function
exception Undecidable
-let rec decidability gl t =
- let open Tacmach.New in
- match destructurate_prop (project gl) t with
+let rec decidability env sigma t =
+ match destructurate_prop sigma t with
| Kapp(Or,[t1;t2]) ->
mkApp (Lazy.force coq_dec_or, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kapp(And,[t1;t2]) ->
mkApp (Lazy.force coq_dec_and, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kapp(Iff,[t1;t2]) ->
mkApp (Lazy.force coq_dec_iff, [| t1; t2;
- decidability gl t1; decidability gl t2 |])
+ decidability env sigma t1; decidability env sigma t2 |])
| Kimp(t1,t2) ->
(* This is the only situation where it's not obvious that [t]
is in Prop. The recursive call on [t2] will ensure that. *)
mkApp (Lazy.force coq_dec_imp,
- [| t1; t2; decidability gl t1; decidability gl t2 |])
+ [| t1; t2; decidability env sigma t1; decidability env sigma t2 |])
| Kapp(Not,[t1]) ->
- mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
+ mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |])
| Kapp(Eq,[typ;t1;t2]) ->
- begin match destructurate_type (project gl) (pf_nf gl typ) with
+ begin match destructurate_type env sigma typ with
| Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
| _ -> raise Undecidable
@@ -1784,15 +1783,16 @@ let onClearedName2 id tac =
let destructure_hyps =
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let decidability = decidability gl in
- let pf_nf = pf_nf gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let decidability = decidability env sigma in
let rec loop = function
| [] -> (tclTHEN nat_inject coq_omega)
| LocalDef (i,body,typ) :: lit when !letin_flag ->
Proofview.tclEVARMAP >>= fun sigma ->
begin
try
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) | Kapp(Z,_) ->
let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in
let hty = mk_gen_eq typ (mkVar i) body in
@@ -1895,7 +1895,7 @@ let destructure_hyps =
with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
tclTHENLIST [
(simplest_elim
@@ -1912,7 +1912,7 @@ let destructure_hyps =
]
| _ -> loop lit
end else begin
- match destructurate_type sigma (pf_nf typ) with
+ match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
(convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
@@ -1940,7 +1940,9 @@ let destructure_hyps =
let destructure_goal =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let decidability = decidability gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let decidability = decidability env sigma in
let rec loop t =
Proofview.tclEVARMAP >>= fun sigma ->
let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 735af6babc..170b937c99 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(**************************************************************************)
(* *)
@@ -13,8 +15,6 @@
(* *)
(**************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
DECLARE PLUGIN "omega_plugin"
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 6a1efe85b9..2510c16934 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(**************************************************************************)
(* *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 17:48:37 +0000