aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/coq_omega.ml584
-rw-r--r--plugins/omega/g_omega.ml47
-rw-r--r--plugins/omega/omega.ml16
3 files changed, 337 insertions, 270 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index cefd48538..9cb94b68d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -13,13 +13,15 @@
(* *)
(**************************************************************************)
+open API
open CErrors
open Util
open Names
open Nameops
open Term
-open Tacticals
-open Tacmach
+open EConstr
+open Tacticals.New
+open Tacmach.New
open Tactics
open Logic
open Libnames
@@ -27,19 +29,21 @@ open Globnames
open Nametab
open Contradiction
open Misctypes
-open Proofview.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
open OmegaSolver
(* Added by JCF, 09/03/98 *)
let elim_id id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- simplest_elim (Tacmach.New.pf_global id gl)
- end }
-let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
+ Proofview.Goal.enter begin fun gl ->
+ simplest_elim (mkVar id)
+ end
+let resolve_id id = Proofview.Goal.enter begin fun gl ->
+ apply (mkVar id)
+end
let timing timer_name f arg = f arg
@@ -67,8 +71,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega system time displaying flag";
optkey = ["Omega";"System"];
optread = read display_system_flag;
@@ -76,8 +79,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega action display flag";
optkey = ["Omega";"Action"];
optread = read display_action_flag;
@@ -85,8 +87,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega old style flag";
optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
@@ -94,8 +95,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "Omega automatic reset of generated names";
optkey = ["Stable";"Omega"];
optread = read reset_flag;
@@ -144,14 +144,14 @@ let intern_id,unintern_id,reset_intern_tables =
Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
(fun () -> cpt := 0; Hashtbl.clear table)
-let mk_then = tclTHENLIST
+let mk_then tacs = tclTHENLIST tacs
let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
let generalize_tac t = generalize t
let elim t = simplest_elim t
-let exact t = Tacmach.refine t
let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
+let pf_nf gl c = pf_apply Tacred.simpl gl c
let rev_assoc k =
let rec loop = function
@@ -171,8 +171,8 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
let hide_constr,find_constr,clear_constr_tables,dump_tables =
let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
(fun h id eg b -> l := (h,(id,eg,b)):: !l),
- (fun h ->
- try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"),
+ (fun sigma h ->
+ try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"),
(fun () -> l := []),
(fun () -> !l)
@@ -196,6 +196,7 @@ let coq_modules =
init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
@ [["Coq"; "omega"; "OmegaLemmas"]]
+let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
let init_constant = gen_constant_in_modules "Omega" init_modules
let constant = gen_constant_in_modules "Omega" coq_modules
@@ -347,14 +348,21 @@ let coq_not_iff = lazy (constant "not_iff")
let coq_not_not = lazy (constant "not_not")
let coq_imp_simp = lazy (constant "imp_simp")
let coq_iff = lazy (constant "iff")
+let coq_not = lazy (init_constant "not")
+let coq_and = lazy (init_constant "and")
+let coq_or = lazy (init_constant "or")
+let coq_eq = lazy (init_constant "eq")
+let coq_ex = lazy (init_constant "ex")
+let coq_False = lazy (init_constant "False")
+let coq_True = lazy (init_constant "True")
(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
(* For unfold *)
-let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
+let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
| Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
EvalConstRef kn
- | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant"))
+ | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc)
let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
@@ -363,21 +371,21 @@ 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 sp_not = lazy (evaluable_ref_of_constr "not" coq_not)
let mk_var v = mkVar (Id.of_string v)
let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+let mk_eq t1 t2 = mkApp (Lazy.force coq_eq,
[| Lazy.force coq_Z; t1; t2 |])
let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
-let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |])
-let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |])
-let mk_not t = mkApp (build_coq_not (), [| t |])
-let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |])
+let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |])
+let mk_not t = mkApp (Lazy.force coq_not, [| t |])
+let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq,
[| Lazy.force coq_comparison; t1; t2 |])
let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
@@ -419,22 +427,23 @@ type result =
the term parts that we manipulate, but rather Var's.
Said otherwise: all constr manipulated here are closed *)
-let destructurate_prop t =
- let c, args = decompose_app t in
- match kind_of_term c, args with
- | _, [_;_;_] when is_global (build_coq_eq ()) c -> Kapp (Eq,args)
+let destructurate_prop sigma t =
+ let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+ let c, args = decompose_app sigma t in
+ match EConstr.kind sigma c, args with
+ | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args)
| _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args)
- | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args)
- | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args)
+ | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args)
| _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args)
- | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args)
- | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args)
- | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args)
+ | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args)
+ | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args)
+ | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args)
| _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args)
| _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
| _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
@@ -447,19 +456,21 @@ let destructurate_prop t =
Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
| Var id,[] -> Kvar id
| Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
- | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+ | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
| _ -> Kufo
-let destructurate_type t =
- let c, args = decompose_app t in
- match kind_of_term c, args with
+let destructurate_type sigma t =
+ let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+ let c, args = decompose_app 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)
| _ -> Kufo
-let destructurate_term t =
- let c, args = decompose_app t in
- match kind_of_term c, args with
+let destructurate_term sigma t =
+ let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+ let c, args = decompose_app sigma t in
+ match EConstr.kind sigma c, args with
| _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args)
| _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args)
@@ -479,15 +490,16 @@ let destructurate_term t =
| Var id,[] -> Kvar id
| _ -> Kufo
-let recognize_number t =
+let recognize_number sigma t =
+ let eq_constr c1 c2 = eq_constr sigma c1 c2 in
let rec loop t =
- match decompose_app t with
+ match decompose_app sigma t with
| f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t
| f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t
| f, [] when eq_constr f (Lazy.force coq_xH) -> one
| _ -> failwith "not a number"
in
- match decompose_app t with
+ match decompose_app sigma t with
| f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t
| f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t)
| f, [] when eq_constr f (Lazy.force coq_Z0) -> zero
@@ -503,9 +515,9 @@ type constr_path =
| P_ARITY
| P_ARG
-let context operation path (t : constr) =
+let context sigma operation path (t : constr) =
let rec loop i p0 t =
- match (p0,kind_of_term t) with
+ match (p0,EConstr.kind sigma t) with
| (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
| ([], _) -> operation i t
| ((P_APP n :: p), App (f,v)) ->
@@ -516,7 +528,7 @@ let context operation path (t : constr) =
let v' = Array.copy v in
v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
| ((P_ARITY :: p), App (f,l)) ->
- appvect (loop i p f,l)
+ mkApp (loop i p f,l)
| ((P_ARG :: p), App (f,v)) ->
let v' = Array.copy v in
v'.(0) <- loop i p v'.(0); mkApp (f,v')
@@ -541,8 +553,8 @@ let context operation path (t : constr) =
in
loop 1 path t
-let occurrence path (t : constr) =
- let rec loop p0 t = match (p0,kind_of_term t) with
+let occurrence sigma path (t : constr) =
+ let rec loop p0 t = match (p0,EConstr.kind sigma t) with
| (p, Cast (c,_,_)) -> loop p c
| ([], _) -> t
| ((P_APP n :: p), App (f,v)) -> loop p v.(pred n)
@@ -561,14 +573,17 @@ let occurrence path (t : constr) =
in
loop path t
-let abstract_path typ path t =
+let abstract_path sigma typ path t =
let term_occur = ref (mkRel 0) in
- let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
+ let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in
mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
-let focused_simpl path gl =
- let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
- Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
+let focused_simpl path =
+ let open Tacmach.New in
+ Proofview.Goal.nf_enter begin fun gl ->
+ let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+ convert_concl_no_check newc DEFAULTcast
+ end
let focused_simpl path = focused_simpl path
@@ -615,7 +630,7 @@ let compile name kind =
let id = new_id () in
tag_hypothesis name id;
{kind = kind; body = List.rev accu; constant = n; id = id}
- | _ -> anomaly (Pp.str "compile_equation")
+ | _ -> anomaly (Pp.str "compile_equation.")
in
loop []
@@ -626,11 +641,18 @@ let decompile af =
in
loop af.body
-let mkNewMeta () = mkMeta (Evarutil.new_meta())
+(** 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
+ Evarutil.new_evar env sigma c
-let clever_rewrite_base_poly typ p result theorem gl =
+let clever_rewrite_base_poly typ p result theorem =
+ let open Tacmach.New in
+ Proofview.Goal.nf_enter begin fun gl ->
let full = pf_concl gl in
- let (abstracted,occ) = abstract_path typ (List.rev p) full in
+ let env = pf_env gl in
+ let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
+ Refine.refine begin fun sigma ->
let t =
applist
(mkLambda
@@ -643,13 +665,17 @@ let clever_rewrite_base_poly typ p result theorem gl =
[| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
[abstracted])
in
- exact (applist(t,[mkNewMeta()])) gl
+ let argt = mkApp (abstracted, [|result|]) in
+ let (sigma, hole) = new_hole env sigma argt in
+ (sigma, applist (t, [hole]))
+ end
+ end
-let clever_rewrite_base p result theorem gl =
- clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+let clever_rewrite_base p result theorem =
+ clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
-let clever_rewrite_base_nat p result theorem gl =
- clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+let clever_rewrite_base_nat p result theorem =
+ clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem
let clever_rewrite_gen p result (t,args) =
let theorem = applist(t, args) in
@@ -659,12 +685,28 @@ let clever_rewrite_gen_nat p result (t,args) =
let theorem = applist(t, args) in
clever_rewrite_base_nat p result theorem
-let clever_rewrite p vpath t gl =
+(** Solve using the term the term [t _] *)
+let refine_app gl t =
+ let open Tacmach.New in
+ Refine.refine begin fun sigma ->
+ let env = pf_env gl in
+ let ht = match EConstr.kind sigma (pf_get_type_of gl t) with
+ | Prod (_, t, _) -> t
+ | _ -> assert false
+ in
+ let (sigma, hole) = new_hole env sigma ht in
+ (sigma, applist (t, [hole]))
+ end
+
+let clever_rewrite p vpath t =
+ let open Tacmach.New in
+ Proofview.Goal.nf_enter begin fun gl ->
let full = pf_concl gl in
- let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
- let vargs = List.map (fun p -> occurrence p occ) vpath in
+ let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
+ let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
let t' = applist(t, (vargs @ [abstracted])) in
- exact (applist(t',[mkNewMeta()])) gl
+ refine_app gl t'
+ end
(** simpl_coeffs :
The subterm at location [path_init] in the current goal should
@@ -676,14 +718,16 @@ let clever_rewrite p vpath t gl =
for instance when the atom is an evaluable definition
(see #4132). *)
-let simpl_coeffs path_init path_k gl =
+let simpl_coeffs path_init path_k =
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = project gl in
let rec loop n t =
if Int.equal n 0 then pf_nf gl t
else
(* t should be of the form ((v * c) + ...) *)
- match kind_of_term t with
+ match EConstr.kind sigma t with
| App(f,[|t1;t2|]) ->
- (match kind_of_term t1 with
+ (match EConstr.kind sigma t1 with
| App (g,[|v;c|]) ->
let c' = pf_nf gl c in
let t2' = loop (pred n) t2 in
@@ -692,9 +736,10 @@ let simpl_coeffs path_init path_k gl =
| _ -> assert false
in
let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
- let newc = context (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
+ let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
in
- Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
+ convert_concl_no_check newc DEFAULTcast
+ end
let rec shuffle p (t1,t2) =
match t1,t2 with
@@ -877,7 +922,7 @@ let rec scalar p n = function
(Lazy.force coq_fast_Zmult_assoc_reverse);
focused_simpl (P_APP 2 :: p)],
Otimes(t1,Oz (n*x))
- | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+ | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
| (Oatom _ as t) -> [], Otimes(t,Oz n)
| Oz i -> [focused_simpl p],Oz(n*i)
| Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
@@ -929,17 +974,17 @@ let rec negate p = function
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
(Lazy.force coq_fast_Zopp_mult_distr_r);
focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
- | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+ | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
| (Oatom _ as t) ->
let r = Otimes(t,Oz(negone)) in
[clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
| Oz i -> [focused_simpl p],Oz(neg i)
| Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
-let rec transform p t =
+let rec transform sigma p t =
let default isnat t' =
try
- let v,th,_ = find_constr t' in
+ let v,th,_ = find_constr sigma t' in
[clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
with e when CErrors.noncritical e ->
let v = new_identifier_var ()
@@ -947,29 +992,29 @@ let rec transform p t =
hide_constr t' v th isnat;
[clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
in
- try match destructurate_term t with
+ try match destructurate_term sigma t with
| Kapp(Zplus,[t1;t2]) ->
- let tac1,t1' = transform (P_APP 1 :: p) t1
- and tac2,t2' = transform (P_APP 2 :: p) t2 in
+ let tac1,t1' = transform sigma (P_APP 1 :: p) t1
+ and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
let tac,t' = shuffle p (t1',t2') in
tac1 @ tac2 @ tac, t'
| Kapp(Zminus,[t1;t2]) ->
let tac,t =
- transform p
+ transform sigma p
(mkApp (Lazy.force coq_Zplus,
[| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
- Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
+ unfold sp_Zminus :: tac,t
| Kapp(Zsucc,[t1]) ->
- let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+ let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
[| t1; mk_integer one |])) in
- Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
+ unfold sp_Zsucc :: tac,t
| Kapp(Zpred,[t1]) ->
- let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+ let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
[| t1; mk_integer negone |])) in
- Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
+ unfold sp_Zpred :: tac,t
| Kapp(Zmult,[t1;t2]) ->
- let tac1,t1' = transform (P_APP 1 :: p) t1
- and tac2,t2' = transform (P_APP 2 :: p) t2 in
+ let tac1,t1' = transform sigma (P_APP 1 :: p) t1
+ and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
begin match t1',t2' with
| (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
| (Oz n,_) ->
@@ -980,11 +1025,11 @@ let rec transform p t =
| _ -> default false t
end
| Kapp((Zpos|Zneg|Z0),_) ->
- (try ([],Oz(recognize_number t))
+ (try ([],Oz(recognize_number sigma t))
with e when CErrors.noncritical e -> default false t)
| Kvar s -> [],Oatom s
| Kapp(Zopp,[t]) ->
- let tac,t' = transform (P_APP 1 :: p) t in
+ let tac,t' = transform sigma (P_APP 1 :: p) t in
let tac',t'' = negate p t' in
tac @ tac', t''
| Kapp(Z_of_nat,[t']) -> default true t'
@@ -1012,7 +1057,7 @@ let shrink_pair p f1 f2 =
| t1,t2 ->
begin
oprint t1; print_newline (); oprint t2; print_newline ();
- flush Pervasives.stdout; error "shrink.1"
+ flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1")
end
let reduce_factor p = function
@@ -1024,10 +1069,10 @@ let reduce_factor p = function
let rec compute = function
| Oz n -> n
| Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
- | _ -> error "condense.1"
+ | _ -> CErrors.user_err Pp.(str "condense.1")
in
[focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
- | t -> oprint t; error "reduce_factor.1"
+ | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1")
let rec condense p = function
| Oplus(f1,(Oplus(f2,r) as t)) ->
@@ -1084,7 +1129,7 @@ let replay_history tactic_normalisation =
| HYP e :: l ->
begin
try
- Tacticals.New.tclTHEN
+ tclTHEN
(Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
(loop l)
with Not_found -> loop l end
@@ -1096,16 +1141,16 @@ let replay_history tactic_normalisation =
let k = if b then negone else one in
let p_initial = [P_APP 1;P_TYPE] in
let tac= shuffle_mult_right p_initial e1.body k e2.body in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
generalize_tac
[mkApp (Lazy.force coq_OMEGA17, [|
val_of eq1;
val_of eq2;
mk_integer k;
mkVar id1; mkVar id2 |])];
- Proofview.V82.tactic (mk_then tac);
+ mk_then tac;
(intros_using [aux]);
- Proofview.V82.tactic (resolve_id aux);
+ resolve_id aux;
reflexivity
]
| CONTRADICTION (e1,e2) :: l ->
@@ -1114,14 +1159,14 @@ let replay_history tactic_normalisation =
let p_initial = [P_APP 2;P_TYPE] in
let tac = shuffle_cancel p_initial e1.body in
let solve_le =
- let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()),
+ let not_sup_sup = mkApp (Lazy.force coq_eq,
[|
Lazy.force coq_comparison;
Lazy.force coq_Gt;
Lazy.force coq_Gt |])
in
- Tacticals.New.tclTHENS
- (Tacticals.New.tclTHENLIST [
+ tclTHENS
+ (tclTHENLIST [
unfold sp_Zle;
simpl_in_concl;
intro;
@@ -1134,7 +1179,7 @@ let replay_history tactic_normalisation =
mkVar (hyp_of_tag e1.id);
mkVar (hyp_of_tag e2.id) |])
in
- Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
+ Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le
| DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
let id = hyp_of_tag e1.id in
let eq1 = val_of(decompile e1)
@@ -1144,10 +1189,10 @@ let replay_history tactic_normalisation =
let rhs = mk_plus (mk_times eq2 kk) dd in
let state_eg = mk_eq eq1 rhs in
let tac = scalar_norm_add [P_APP 3] e2.body in
- Tacticals.New.tclTHENS
+ tclTHENS
(cut state_eg)
- [ Tacticals.New.tclTHENS
- (Tacticals.New.tclTHENLIST [
+ [ tclTHENS
+ (tclTHENLIST [
(intros_using [aux]);
(generalize_tac
[mkApp (Lazy.force coq_OMEGA1,
@@ -1155,9 +1200,9 @@ let replay_history tactic_normalisation =
(clear [aux;id]);
(intros_using [id]);
(cut (mk_gt kk dd)) ])
- [ Tacticals.New.tclTHENS
+ [ tclTHENS
(cut (mk_gt kk izero))
- [ Tacticals.New.tclTHENLIST [
+ [ tclTHENLIST [
(intros_using [aux1; aux2]);
(generalize_tac
[mkApp (Lazy.force coq_Zmult_le_approx,
@@ -1165,13 +1210,13 @@ let replay_history tactic_normalisation =
(clear [aux1;aux2;id]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(unfold sp_Zgt);
simpl_in_concl;
reflexivity ] ];
- Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
+ tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
];
- Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+ tclTHEN (mk_then tac) reflexivity ]
| NOT_EXACT_DIVIDE (e1,k) :: l ->
let c = floor_div e1.constant k in
@@ -1182,10 +1227,10 @@ let replay_history tactic_normalisation =
let kk = mk_integer k
and dd = mk_integer d in
let tac = scalar_norm_add [P_APP 2] e2.body in
- Tacticals.New.tclTHENS
+ tclTHENS
(cut (mk_gt dd izero))
- [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
- [Tacticals.New.tclTHENLIST [
+ [ tclTHENS (cut (mk_gt kk dd))
+ [tclTHENLIST [
(intros_using [aux2;aux1]);
(generalize_tac
[mkApp (Lazy.force coq_OMEGA4,
@@ -1193,14 +1238,14 @@ let replay_history tactic_normalisation =
(clear [aux1;aux2]);
unfold sp_not;
(intros_using [aux]);
- Proofview.V82.tactic (resolve_id aux);
- Proofview.V82.tactic (mk_then tac);
+ resolve_id aux;
+ mk_then tac;
assumption ] ;
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
reflexivity ] ];
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
reflexivity ] ]
@@ -1213,9 +1258,9 @@ let replay_history tactic_normalisation =
let state_eq = mk_eq eq1 (mk_times eq2 kk) in
if e1.kind == DISE then
let tac = scalar_norm [P_APP 3] e2.body in
- Tacticals.New.tclTHENS
+ tclTHENS
(cut state_eq)
- [Tacticals.New.tclTHENLIST [
+ [tclTHENLIST [
(intros_using [aux1]);
(generalize_tac
[mkApp (Lazy.force coq_OMEGA18,
@@ -1223,14 +1268,14 @@ let replay_history tactic_normalisation =
(clear [aux1;id]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+ tclTHEN (mk_then tac) reflexivity ]
else
let tac = scalar_norm [P_APP 3] e2.body in
- Tacticals.New.tclTHENS (cut state_eq)
+ tclTHENS (cut state_eq)
[
- Tacticals.New.tclTHENS
+ tclTHENS
(cut (mk_gt kk izero))
- [Tacticals.New.tclTHENLIST [
+ [tclTHENLIST [
(intros_using [aux2;aux1]);
(generalize_tac
[mkApp (Lazy.force coq_OMEGA3,
@@ -1238,11 +1283,11 @@ let replay_history tactic_normalisation =
(clear [aux1;aux2;id]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
reflexivity ] ];
- Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+ tclTHEN (mk_then tac) reflexivity ]
| (MERGE_EQ(e3,e1,e2)) :: l ->
let id = new_identifier () in
tag_hypothesis id e3;
@@ -1255,16 +1300,16 @@ let replay_history tactic_normalisation =
(Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
scalar_norm [P_APP 3] e1.body
in
- Tacticals.New.tclTHENS
+ tclTHENS
(cut (mk_eq eq1 (mk_inv eq2)))
- [Tacticals.New.tclTHENLIST [
+ [tclTHENLIST [
(intros_using [aux]);
(generalize_tac [mkApp (Lazy.force coq_OMEGA8,
[| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
(clear [id1;id2;aux]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
+ tclTHEN (mk_then tac) reflexivity]
| STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
let id = new_identifier ()
@@ -1274,7 +1319,7 @@ let replay_history tactic_normalisation =
and eq2 = val_of(decompile orig) in
let vid = unintern_id v in
let theorem =
- mkApp (build_coq_ex (), [|
+ mkApp (Lazy.force coq_ex, [|
Lazy.force coq_Z;
mkLambda
(Name vid,
@@ -1288,9 +1333,9 @@ let replay_history tactic_normalisation =
[[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
shuffle_mult_right p_initial
orig.body m ({c= negone;v= v}::def.body) in
- Tacticals.New.tclTHENS
+ tclTHENS
(cut theorem)
- [Tacticals.New.tclTHENLIST [
+ [tclTHENLIST [
(intros_using [aux]);
(elim_id aux);
(clear [aux]);
@@ -1298,11 +1343,11 @@ let replay_history tactic_normalisation =
(generalize_tac
[mkApp (Lazy.force coq_OMEGA9,
[| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
- Proofview.V82.tactic (mk_then tac);
+ mk_then tac;
(clear [aux]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
+ tclTHEN (exists_tac eq1) reflexivity ]
| SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
let id1 = new_identifier ()
and id2 = new_identifier () in
@@ -1311,10 +1356,10 @@ let replay_history tactic_normalisation =
let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
let eq = val_of(decompile e) in
- Tacticals.New.tclTHENS
+ tclTHENS
(simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
- [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ];
- Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+ [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ];
+ tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]]
| SUM(e3,(k1,e1),(k2,e2)) :: l ->
let id = new_identifier () in
tag_hypothesis id e3;
@@ -1333,10 +1378,10 @@ let replay_history tactic_normalisation =
let p_initial =
if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
- Proofview.V82.tactic (mk_then tac);
+ mk_then tac;
(intros_using [id]);
(loop l)
]
@@ -1345,10 +1390,10 @@ let replay_history tactic_normalisation =
and kk2 = mk_integer k2 in
let p_initial = [P_APP 2;P_TYPE] in
let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
- Tacticals.New.tclTHENS (cut (mk_gt kk1 izero))
- [Tacticals.New.tclTHENS
+ tclTHENS (cut (mk_gt kk1 izero))
+ [tclTHENS
(cut (mk_gt kk2 izero))
- [Tacticals.New.tclTHENLIST [
+ [tclTHENLIST [
(intros_using [aux2;aux1]);
(generalize_tac
[mkApp (Lazy.force coq_OMEGA7, [|
@@ -1356,102 +1401,106 @@ let replay_history tactic_normalisation =
mkVar aux1;mkVar aux2;
mkVar id1;mkVar id2 |])]);
(clear [aux1;aux2]);
- Proofview.V82.tactic (mk_then tac);
+ mk_then tac;
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
reflexivity ] ];
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
reflexivity ] ]
| CONSTANT_NOT_NUL(e,k) :: l ->
- Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+ tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
| CONSTANT_NUL(e) :: l ->
- Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
+ tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
| CONSTANT_NEG(e,k) :: l ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac [mkVar (hyp_of_tag e)]);
unfold sp_Zle;
simpl_in_concl;
unfold sp_not;
(intros_using [aux]);
- Proofview.V82.tactic (resolve_id aux);
+ resolve_id aux;
reflexivity
]
| _ -> Proofview.tclUNIT ()
in
loop
-let normalize p_initial t =
- let (tac,t') = transform p_initial t in
+let normalize sigma p_initial t =
+ let (tac,t') = transform sigma p_initial t in
let (tac',t'') = condense p_initial t' in
let (tac'',t''') = clear_zero p_initial t'' in
tac @ tac' @ tac'' , t'''
-let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
+let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
let p_initial = [P_APP pos ;P_TYPE] in
- let (tac,t') = normalize p_initial t in
+ let (tac,t') = normalize sigma p_initial t in
let shift_left =
tclTHEN
- (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
- (tclTRY (Proofview.V82.of_tactic (clear [id])))
+ (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+ (tclTRY (clear [id]))
in
if not (List.is_empty tac) then
let id' = new_identifier () in
- ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ]))
+ ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ]))
:: tactic,
compile id' flag t' :: 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
if String.equal (atompart_of_id id) "State" then
tac_def
else
- try match destructurate_prop c with
+ try match destructurate_prop sigma c with
| Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
+ when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
let t = mk_plus t1 (mk_inv t2) in
- normalize_equation
+ normalize_equation sigma
id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
| Kapp(Zne,[t1;t2]) ->
let t = mk_plus t1 (mk_inv t2) in
- normalize_equation
+ normalize_equation sigma
id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
| Kapp(Zle,[t1;t2]) ->
let t = mk_plus t2 (mk_inv t1) in
- normalize_equation
+ normalize_equation sigma
id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
| Kapp(Zlt,[t1;t2]) ->
let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
- normalize_equation
+ normalize_equation sigma
id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
| Kapp(Zge,[t1;t2]) ->
let t = mk_plus t1 (mk_inv t2) in
- normalize_equation
+ normalize_equation sigma
id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
| Kapp(Zgt,[t1;t2]) ->
let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
- normalize_equation
+ normalize_equation sigma
id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
| _ -> tac_def
with e when catchable_exception e -> tac_def
let reintroduce id =
(* [id] cannot be cleared if dependent: protect it by a try *)
- Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id)
+ tclTHEN (tclTRY (clear [id])) (intro_using id)
open Proofview.Notations
let coq_omega =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = Tacmach.New.of_old destructure_omega gl in
+ let destructure_omega = destructure_omega gl in
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1461,7 +1510,7 @@ let coq_omega =
let id = new_identifier () in
let i = new_id () in
tag_hypothesis id i;
- (Tacticals.New.tclTHENLIST [
+ (tclTHENLIST [
(simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
(intros_using [v; id]);
(elim_id id);
@@ -1472,7 +1521,7 @@ let coq_omega =
body = [{v=intern_id v; c=one}];
constant = zero; id = i} :: sys
else
- (Tacticals.New.tclTHENLIST [
+ (tclTHENLIST [
(simplest_elim (applist (Lazy.force coq_new_var, [t])));
(intros_using [v;th]);
tac ]),
@@ -1488,94 +1537,96 @@ let coq_omega =
with UNSOLVABLE ->
let _,path = depend [] [] (history ()) in
if !display_action_flag then display_action display_var path;
- (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path))
+ (tclTHEN prelude (replay_history tactic_normalisation path))
end else begin
try
let path = simplify_strong (new_id,new_var_num,display_var) system in
if !display_action_flag then display_action display_var path;
- Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
- with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
+ tclTHEN prelude (replay_history tactic_normalisation path)
+ with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
+ end
end
- end }
let coq_omega = coq_omega
let nat_inject =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
let rec explore p t : unit Proofview.tactic =
- try match destructurate_term t with
+ Proofview.tclEVARMAP >>= fun sigma ->
+ try match destructurate_term sigma t with
| Kapp(Plus,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+ tclTHENLIST [
+ (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
((Lazy.force coq_inj_plus),[t1;t2]));
(explore (P_APP 1 :: p) t1);
(explore (P_APP 2 :: p) t2)
]
| Kapp(Mult,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+ tclTHENLIST [
+ (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
((Lazy.force coq_inj_mult),[t1;t2]));
(explore (P_APP 1 :: p) t1);
(explore (P_APP 2 :: p) t2)
]
| Kapp(Minus,[t1;t2]) ->
let id = new_identifier () in
- Tacticals.New.tclTHENS
- (Tacticals.New.tclTHEN
+ tclTHENS
+ (tclTHEN
(simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
(intros_using [id]))
[
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (clever_rewrite_gen p
+ tclTHENLIST [
+ (clever_rewrite_gen p
(mk_minus (mk_inj t1) (mk_inj t2))
((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
(loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
(explore (P_APP 1 :: p) t1);
(explore (P_APP 2 :: p) t2) ];
- (Tacticals.New.tclTHEN
- (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero)
- ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])))
+ (tclTHEN
+ (clever_rewrite_gen p (mk_integer zero)
+ ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
(loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
]
| Kapp(S,[t']) ->
let rec is_number t =
- try match destructurate_term t with
+ try match destructurate_term sigma t with
Kapp(S,[t]) -> is_number t
| Kapp(O,[]) -> true
| _ -> false
with e when catchable_exception e -> false
in
let rec loop p t : unit Proofview.tactic =
- try match destructurate_term t with
+ try match destructurate_term sigma t with
Kapp(S,[t]) ->
- (Tacticals.New.tclTHEN
- (Proofview.V82.tactic (clever_rewrite_gen p
+ (tclTHEN
+ (clever_rewrite_gen p
(mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
- ((Lazy.force coq_inj_S),[t])))
+ ((Lazy.force coq_inj_S),[t]))
(loop (P_APP 1 :: p) t))
| _ -> explore p t
with e when catchable_exception e -> explore p t
in
- if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t
+ if is_number t' then focused_simpl p else loop p t
| Kapp(Pred,[t]) ->
let t_minus_one =
mkApp (Lazy.force coq_minus, [| t;
mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
- Tacticals.New.tclTHEN
- (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
- ((Lazy.force coq_pred_of_minus),[t])))
+ tclTHEN
+ (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
+ ((Lazy.force coq_pred_of_minus),[t]))
(explore p t_minus_one)
- | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p)
+ | Kapp(O,[]) -> focused_simpl p
| _ -> Proofview.tclUNIT ()
with e when catchable_exception e -> Proofview.tclUNIT ()
and loop = function
| [] -> Proofview.tclUNIT ()
| (i,t)::lit ->
- begin try match destructurate_prop t with
+ Proofview.tclEVARMAP >>= fun sigma ->
+ begin try match destructurate_prop sigma t with
Kapp(Le,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
@@ -1584,7 +1635,7 @@ let nat_inject =
(loop lit)
]
| Kapp(Lt,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
@@ -1593,7 +1644,7 @@ let nat_inject =
(loop lit)
]
| Kapp(Ge,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
@@ -1602,7 +1653,7 @@ let nat_inject =
(loop lit)
]
| Kapp(Gt,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
@@ -1611,7 +1662,7 @@ let nat_inject =
(loop lit)
]
| Kapp(Neq,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 1; P_TYPE] t1);
@@ -1621,7 +1672,7 @@ let nat_inject =
]
| Kapp(Eq,[typ;t1;t2]) ->
if is_conv typ (Lazy.force coq_nat) then
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
(explore [P_APP 2; P_TYPE] t1);
@@ -1635,7 +1686,7 @@ let nat_inject =
in
let hyps_types = Tacmach.New.pf_hyps_types gl in
loop (List.rev hyps_types)
- end }
+ end
let dec_binop = function
| Zne -> coq_dec_Zne
@@ -1670,7 +1721,8 @@ let not_binop = function
exception Undecidable
let rec decidability gl t =
- match destructurate_prop t with
+ let open Tacmach.New in
+ match destructurate_prop (project gl) t with
| Kapp(Or,[t1;t2]) ->
mkApp (Lazy.force coq_dec_or, [| t1; t2;
decidability gl t1; decidability gl t2 |])
@@ -1688,7 +1740,7 @@ let rec decidability gl t =
| Kapp(Not,[t1]) ->
mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
| Kapp(Eq,[typ;t1;t2]) ->
- begin match destructurate_type (pf_nf gl typ) with
+ begin match destructurate_type (project gl) (pf_nf gl 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
@@ -1700,59 +1752,68 @@ let rec decidability gl t =
| Kapp(True,[]) -> Lazy.force coq_dec_True
| _ -> raise Undecidable
+let fresh_id avoid id gl =
+ fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
let onClearedName id tac =
(* We cannot ensure that hyps can be cleared (because of dependencies), *)
(* so renaming may be necessary *)
- Tacticals.New.tclTHEN
- (Tacticals.New.tclTRY (clear [id]))
- (Proofview.Goal.nf_enter { enter = begin fun gl ->
- let id = Tacmach.New.of_old (fresh_id [] id) gl in
- Tacticals.New.tclTHEN (introduction id) (tac id)
- end })
+ tclTHEN
+ (tclTRY (clear [id]))
+ (Proofview.Goal.nf_enter begin fun gl ->
+ let id = fresh_id [] id gl in
+ tclTHEN (introduction id) (tac id)
+ end)
let onClearedName2 id tac =
- Tacticals.New.tclTHEN
- (Tacticals.New.tclTRY (clear [id]))
- (Proofview.Goal.nf_enter { enter = begin fun gl ->
- let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
- let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
- Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
- end })
+ tclTHEN
+ (tclTRY (clear [id]))
+ (Proofview.Goal.nf_enter begin fun gl ->
+ let id1 = fresh_id [] (add_suffix id "_left") gl in
+ let id2 = fresh_id [] (add_suffix id "_right") gl in
+ tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
+ end)
+
+let rec is_Prop sigma c = match EConstr.kind sigma c with
+ | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
+ | Cast (c,_,_) -> is_Prop sigma c
+ | _ -> false
let destructure_hyps =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let decidability = Tacmach.New.of_old decidability gl in
- let pf_nf = Tacmach.New.of_old pf_nf gl in
+ let decidability = decidability gl in
+ let pf_nf = pf_nf gl in
let rec loop = function
- | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
+ | [] -> (tclTHEN nat_inject coq_omega)
| decl::lit ->
- let (i,_,t) = to_tuple decl in
- begin try match destructurate_prop t with
+ let i = NamedDecl.get_id decl in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ begin try match destructurate_prop sigma (NamedDecl.get_type decl) with
| Kapp(False,[]) -> elim_id i
| Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
| Kapp(Or,[t1;t2]) ->
- (Tacticals.New.tclTHENS
+ (tclTHENS
(elim_id i)
[ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit)));
onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ])
| Kapp(And,[t1;t2]) ->
- Tacticals.New.tclTHEN
+ tclTHEN
(elim_id i)
(onClearedName2 i (fun i1 i2 ->
loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit)))
| Kapp(Iff,[t1;t2]) ->
- Tacticals.New.tclTHEN
+ tclTHEN
(elim_id i)
(onClearedName2 i (fun i1 i2 ->
loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit)))
| Kimp(t1,t2) ->
(* t1 and t2 might be in Type rather than Prop.
For t1, the decidability check will ensure being Prop. *)
- if is_Prop (type_of t2)
+ if is_Prop sigma (type_of t2)
then
let d1 = decidability t1 in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac [mkApp (Lazy.force coq_imp_simp,
[| t1; t2; d1; mkVar i|])]);
(onClearedName i (fun i ->
@@ -1761,9 +1822,9 @@ let destructure_hyps =
else
loop lit
| Kapp(Not,[t]) ->
- begin match destructurate_prop t with
+ begin match destructurate_prop sigma t with
Kapp(Or,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
(onClearedName i (fun i ->
@@ -1771,7 +1832,7 @@ let destructure_hyps =
]
| Kapp(And,[t1;t2]) ->
let d1 = decidability t1 in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_and,
[| t1; t2; d1; mkVar i |])]);
@@ -1781,7 +1842,7 @@ let destructure_hyps =
| Kapp(Iff,[t1;t2]) ->
let d1 = decidability t1 in
let d2 = decidability t2 in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_iff,
[| t1; t2; d1; d2; mkVar i |])]);
@@ -1793,7 +1854,7 @@ let destructure_hyps =
(* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
For t1, being decidable implies being Prop. *)
let d1 = decidability t1 in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_imp,
[| t1; t2; d1; mkVar i |])]);
@@ -1802,7 +1863,7 @@ let destructure_hyps =
]
| Kapp(Not,[t]) ->
let d = decidability t in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
(onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
@@ -1810,7 +1871,7 @@ let destructure_hyps =
| Kapp(op,[t1;t2]) ->
(try
let thm = not_binop op in
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
@@ -1818,16 +1879,16 @@ let destructure_hyps =
with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
- match destructurate_type (pf_nf typ) with
+ match destructurate_type sigma (pf_nf typ) with
| Kapp(Nat,_) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(simplest_elim
(mkApp
(Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Z,_) ->
- Tacticals.New.tclTHENLIST [
+ tclTHENLIST [
(simplest_elim
(mkApp
(Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
@@ -1835,16 +1896,16 @@ let destructure_hyps =
]
| _ -> loop lit
end else begin
- match destructurate_type (pf_nf typ) with
+ match destructurate_type sigma (pf_nf typ) with
| Kapp(Nat,_) ->
- (Tacticals.New.tclTHEN
- (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
- decl))
+ (tclTHEN
+ (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+ decl))
(loop lit))
| Kapp(Z,_) ->
- (Tacticals.New.tclTHEN
- (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
- decl))
+ (tclTHEN
+ (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+ decl))
(loop lit))
| _ -> loop lit
end
@@ -1858,34 +1919,39 @@ let destructure_hyps =
in
let hyps = Proofview.Goal.hyps gl in
loop hyps
- end }
+ end
let destructure_goal =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let decidability = Tacmach.New.of_old decidability gl in
+ let decidability = decidability gl in
let rec loop t =
- match destructurate_prop t with
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
+ Proofview.V82.wrap_exceptions prop >>= fun prop ->
+ match prop with
| Kapp(Not,[t]) ->
- (Tacticals.New.tclTHEN
- (Tacticals.New.tclTHEN (unfold sp_not) intro)
+ (tclTHEN
+ (tclTHEN (unfold sp_not) intro)
destructure_hyps)
- | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
+ | Kimp(a,b) -> (tclTHEN intro (loop b))
| Kapp(False,[]) -> destructure_hyps
| _ ->
let goal_tac =
try
let dec = decidability t in
- Tacticals.New.tclTHEN
- (Proofview.V82.tactic (Tacmach.refine
- (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+ tclTHEN
+ (Proofview.Goal.nf_enter begin fun gl ->
+ refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
+ end)
intro
- with Undecidable -> Tactics.elim_type (build_coq_False ())
+ with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
+ | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
- Tacticals.New.tclTHEN goal_tac destructure_hyps
+ tclTHEN goal_tac destructure_hyps
in
(loop concl)
- end }
+ end
let destructure_goal = destructure_goal
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 5647fbf9f..8cea98783 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -15,11 +15,14 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open API
+
DECLARE PLUGIN "omega_plugin"
+open Ltac_plugin
open Names
open Coq_omega
-open Constrarg
+open Stdarg
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
@@ -34,7 +37,7 @@ let omega_tactic l =
| "positive" -> eval_tactic "zify_positive"
| "N" -> eval_tactic "zify_N"
| "Z" -> eval_tactic "zify_op"
- | s -> CErrors.error ("No Omega knowledge base for type "^s))
+ | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s)))
(Util.List.sort_uniquize String.compare l)
in
Tacticals.New.tclTHEN
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index bd991a955..2a018fa3f 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -96,7 +96,7 @@ type afine = {
type state_action = {
st_new_eq : afine;
- st_def : afine;
+ st_def : afine; (* /!\ this represents [st_def = st_var] *)
st_orig : afine;
st_coef : bigint;
st_var : int }
@@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
let e = original.body in
let sigma = new_var_id () in
+ if e == [] then begin
+ display_system print_var [original] ; failwith "TL"
+ end;
let smallest,var =
- try
- List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
- (abs (List.hd e).c, (List.hd e).v) (List.tl e)
- with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+ List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
+ (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+ in
let m = smallest + one in
let new_eq =
{ constant = omega_mod original.constant m;
@@ -585,10 +587,6 @@ let rec depend relie_on accu = function
end
| [] -> relie_on, accu
-let solve (new_eq_id,new_eq_var,print_var) system =
- try let _ = simplify new_eq_id false system in failwith "no contradiction"
- with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
-
let negation (eqs,ineqs) =
let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
let normal = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 15:10:22 +0000