From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/omega/Omega.v | 4 +- plugins/omega/OmegaPlugin.v | 2 +- plugins/omega/PreOmega.v | 5 +- plugins/omega/coq_omega.ml | 777 ++++++++++++++++++++++---------------------- plugins/omega/g_omega.ml4 | 21 +- plugins/omega/omega.ml | 106 +++--- 6 files changed, 456 insertions(+), 459 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 0192528c..7400d462 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* abstract omega: zarith. Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith. Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith. -Hint Extern 10 False => abstract omega: zarith. \ No newline at end of file +Hint Extern 10 False => abstract omega: zarith. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index d23e3d13..9e5c1484 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + simplest_elim (Tacmach.New.pf_global id gl) + end +let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl let timing timer_name f arg = f arg @@ -51,20 +48,15 @@ let old_style_flag = ref false (* Should we reset all variable labels between two runs of omega ? *) -let reset_flag = ref false +let reset_flag = ref true -(* Historical version of Coq do not perform such resets, and this - implies that omega is slightly non-deterministic: successive runs of - omega on the same problem may lead to distinct proof-terms. - At the very least, these terms will differ on the inner +(* Coq < 8.5 was not performing such resets, hence omega was slightly + non-deterministic: successive runs of omega on the same problem may + lead to distinct proof-terms. + At the very least, these terms differed on the inner variable names, but they could even be non-convertible : the OmegaSolver relies on Hashtbl.iter, it can hence find a different - solution when variable indices differ. - - Starting from Coq 8.4pl4, omega may be made stable via the option - [Set Stable Omega]. In the 8.4 branch, this option is unset by default - for compatibility. In Coq >= 8.5, this option is set by default. -*) + solution when variable indices differ. *) let read f () = !f let write f x = f:=x @@ -101,19 +93,12 @@ let _ = let _ = declare_bool_option { optsync = true; - optdepr = false; + optdepr = true; optname = "Omega automatic reset of generated names"; optkey = ["Stable";"Omega"]; optread = read reset_flag; optwrite = write reset_flag } -let all_time = timing "Omega " -let solver_time = timing "Solver " -let exact_time = timing "Rewrites " -let elim_time = timing "Elim " -let simpl_time = timing "Simpl " -let generalize_time = timing "Generalize" - let intref, reset_all_references = let refs = ref [] in (fun n -> let r = ref n in refs := (r,n) :: !refs; r), @@ -121,7 +106,7 @@ let intref, reset_all_references = let new_identifier = let cpt = intref 0 in - (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s) + (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) let new_identifier_state = let cpt = intref 0 in @@ -129,7 +114,7 @@ let new_identifier_state = let new_identifier_var = let cpt = intref 0 in - (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) + (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) let new_id = let cpt = intref 0 in fun () -> incr cpt; !cpt @@ -145,7 +130,7 @@ let display_var i = Printf.sprintf "X%d" i let intern_id,unintern_id,reset_intern_tables = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in - (fun (name : identifier) -> + (fun (name : Id.t) -> try Hashtbl.find table name with Not_found -> let idx = !cpt in Hashtbl.add table name idx; @@ -159,30 +144,33 @@ let intern_id,unintern_id,reset_intern_tables = let mk_then = tclTHENLIST -let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c]) +let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) -let generalize_tac t = generalize_time (generalize t) -let elim t = elim_time (simplest_elim t) -let exact t = exact_time (Tactics.refine t) -let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s] +let generalize_tac t = generalize t +let elim t = simplest_elim t +let exact t = Tactics.refine t +let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = let rec loop = function - | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l + | [] -> raise Not_found + | (v,k')::_ when Int.equal k k' -> v + | _ :: l -> loop l in loop let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = - let l = ref ([]:(identifier * int) list) in + let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun () -> l := []) let hide_constr,find_constr,clear_constr_tables,dump_tables = - let l = ref ([]:(constr * (identifier * identifier * bool)) list) in + 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 h !l with Not_found -> failwith "find_contr"), + (fun h -> + try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -230,8 +218,6 @@ 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") @@ -318,10 +304,10 @@ let coq_le = lazy (init_constant "le") let coq_lt = lazy (init_constant "lt") let coq_ge = lazy (init_constant "ge") let coq_gt = lazy (init_constant "gt") -let coq_minus = lazy (init_constant "minus") -let coq_plus = lazy (init_constant "plus") -let coq_mult = lazy (init_constant "mult") -let coq_pred = lazy (init_constant "pred") +let coq_minus = lazy (init_constant "Nat.sub") +let coq_plus = lazy (init_constant "Nat.add") +let coq_mult = lazy (init_constant "Nat.mul") +let coq_pred = lazy (init_constant "Nat.pred") let coq_nat = lazy (init_constant "nat") let coq_S = lazy (init_constant "S") let coq_O = lazy (init_constant "O") @@ -363,11 +349,10 @@ let coq_iff = lazy (constant "iff") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -open Closure let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with - | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> + | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn - | _ -> anomaly ("Coq_omega: "^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) @@ -378,19 +363,20 @@ 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) +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 (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |]) +let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_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 (build_coq_eq (), - [| Lazy.force coq_comparison; t1; t2 |]) +let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), + [| Lazy.force coq_comparison; t1; t2 |]) let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -419,7 +405,7 @@ type omega_proposition = | Kn type result = - | Kvar of identifier + | Kvar of Id.t | Kapp of omega_constant * constr list | Kimp of constr * constr | Kufo @@ -434,7 +420,7 @@ type result = let destructurate_prop t = let c, args = decompose_app t in match kind_of_term c, args with - | _, [_;_;_] when eq_constr c (build_coq_eq ()) -> Kapp (Eq,args) + | _, [_;_;_] when is_global (build_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) @@ -451,11 +437,11 @@ let destructurate_prop t = | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) - | Const sp, args -> + | Const (sp,_), args -> Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) - | Construct csp , args -> + | Construct (csp,_) , args -> Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) - | Ind isp, args -> + | Ind (isp,_), args -> Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) @@ -549,7 +535,6 @@ let context operation path (t : constr) = | ((P_TYPE :: p), LetIn (n,b,t,c)) -> (mkLetIn (n,b,loop i p t,c)) | (p, _) -> - ppnl (Printer.pr_lconstr t); failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t @@ -570,7 +555,6 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term | (p, _) -> - ppnl (Printer.pr_lconstr t); failwith ("occurence " ^ string_of_int(List.length p)) in loop path t @@ -578,19 +562,19 @@ let occurence path (t : constr) = let abstract_path typ path t = let term_occur = ref (mkRel 0) in let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur + 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 - convert_concl_no_check newc DEFAULTcast gl + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl -let focused_simpl path = simpl_time (focused_simpl path) +let focused_simpl path = focused_simpl path type oformula = | Oplus of oformula * oformula | Oinv of oformula | Otimes of oformula * oformula - | Oatom of identifier + | Oatom of Id.t | Oz of bigint | Oufo of constr @@ -602,7 +586,7 @@ let rec oprint = function | Otimes (t1,t2) -> print_string "("; oprint t1; print_string "*"; oprint t2; print_string ")" - | Oatom s -> print_string (string_of_id s) + | Oatom s -> print_string (Id.to_string s) | Oz i -> print_string (string_of_bigint i) | Oufo f -> print_string "?" @@ -629,11 +613,11 @@ let compile name kind = let id = new_id () in tag_hypothesis name id; {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly "compile_equation" + | _ -> anomaly (Pp.str "compile_equation") in loop [] -let rec decompile af = +let decompile af = let rec loop = function | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) | [] -> Oz af.constant @@ -648,10 +632,10 @@ let clever_rewrite_base_poly typ p result theorem gl = let t = applist (mkLambda - (Name (id_of_string "P"), + (Name (Id.of_string "P"), mkArrow typ mkProp, mkLambda - (Name (id_of_string "H"), + (Name (Id.of_string "H"), applist (mkRel 1,[result]), mkApp (Lazy.force coq_eq_ind_r, [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), @@ -724,10 +708,10 @@ let rec shuffle p (t1,t2) = Oplus(t2,t1) else [],Oplus(t1,t2) -let rec shuffle_mult p_init k1 e1 k2 e2 = +let shuffle_mult p_init k1 e1 k2 e2 = let rec loop p = function | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if v1 = v2 then + if Int.equal v1 v2 then let tac = clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; @@ -781,10 +765,10 @@ let rec shuffle_mult p_init k1 e1 k2 e2 = in loop p_init (e1,e2) -let rec shuffle_mult_right p_init e1 k2 e2 = +let shuffle_mult_right p_init e1 k2 e2 = let rec loop p = function | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if v1 = v2 then + if Int.equal v1 v2 then let tac = clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1]; @@ -866,7 +850,7 @@ let rec scalar p n = function | Oz i -> [focused_simpl p],Oz(n*i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) -let rec scalar_norm p_init = +let scalar_norm p_init = let rec loop p = function | [] -> [focused_simpl p_init] | (_::l) -> @@ -877,7 +861,7 @@ let rec scalar_norm p_init = in loop p_init -let rec norm_add p_init = +let norm_add p_init = let rec loop p = function | [] -> [focused_simpl p_init] | _:: l -> @@ -887,7 +871,7 @@ let rec norm_add p_init = in loop p_init -let rec scalar_norm_add p_init = +let scalar_norm_add p_init = let rec loop p = function | [] -> [focused_simpl p_init] | _ :: l -> @@ -1015,7 +999,7 @@ let reduce_factor p = function let rec condense p = function | Oplus(f1,(Oplus(f2,r) as t)) -> - if weight f1 = weight f2 then begin + if Int.equal (weight f1) (weight f2) then begin let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in let assoc_tac = clever_rewrite p @@ -1031,7 +1015,7 @@ let rec condense p = function | Oplus(f1,Oz n) -> let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) | Oplus(f1,f2) -> - if weight f1 = weight f2 then begin + if Int.equal (weight f1) (weight f2) then begin let tac_shrink,t = shrink_pair p f1 f2 in let tac,t' = condense p t in tac_shrink :: tac,t' @@ -1059,17 +1043,17 @@ let rec clear_zero p = function | t -> [],t let replay_history tactic_normalisation = - let aux = id_of_string "auxiliary" in - let aux1 = id_of_string "auxiliary_1" in - let aux2 = id_of_string "auxiliary_2" in + let aux = Id.of_string "auxiliary" in + let aux1 = Id.of_string "auxiliary_1" in + let aux2 = Id.of_string "auxiliary_2" in let izero = mk_integer zero in - let rec loop t = + let rec loop t : unit Proofview.tactic = match t with | HYP e :: l -> begin try - tclTHEN - (List.assoc (hyp_of_tag e.id) tactic_normalisation) + Tacticals.New.tclTHEN + (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end | NEGATE_CONTRADICT (e2,e1,b) :: l -> @@ -1080,16 +1064,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 - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; mkVar id1; mkVar id2 |])]); - (mk_then tac); + Proofview.V82.tactic (mk_then tac); (intros_using [aux]); - (resolve_id aux); + Proofview.V82.tactic (resolve_id aux); reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1098,15 +1082,16 @@ 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 (build_coq_eq (), [| + let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()), + [| Lazy.force coq_comparison; Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - tclTHENS - (tclTHENLIST [ - (unfold sp_Zle); - (simpl_in_concl); + Tacticals.New.tclTHENS + (Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zle); + Proofview.V82.tactic (simpl_in_concl); intro; (absurd not_sup_sup) ]) [ assumption ; reflexivity ] @@ -1117,7 +1102,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le) + Proofview.tclTHEN (Proofview.V82.tactic (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) @@ -1127,34 +1112,34 @@ 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 - tclTHENS + Tacticals.New.tclTHENS (cut state_eg) - [ tclTHENS - (tclTHENLIST [ + [ Tacticals.New.tclTHENS + (Tacticals.New.tclTHENLIST [ (intros_using [aux]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA1, [| eq1; rhs; mkVar aux; mkVar id |])]); - (clear [aux;id]); + Proofview.V82.tactic (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) - [ tclTHENS + [ Tacticals.New.tclTHENS (cut (mk_gt kk izero)) - [ tclTHENLIST [ + [ Tacticals.New.tclTHENLIST [ (intros_using [aux1; aux2]); - (generalize_tac + (Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, - [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); - (clear [aux1;aux2;id]); + [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])])); + Proofview.V82.tactic (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - (simpl_in_concl); + Tacticals.New.tclTHENLIST [ + (Proofview.V82.tactic (unfold sp_Zgt)); + (Proofview.V82.tactic simpl_in_concl); reflexivity ] ]; - tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] + Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in @@ -1165,27 +1150,27 @@ 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 - tclTHENS + Tacticals.New.tclTHENS (cut (mk_gt dd izero)) - [ tclTHENS (cut (mk_gt kk dd)) - [tclTHENLIST [ + [ Tacticals.New.tclTHENS (cut (mk_gt kk dd)) + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); - (clear [aux1;aux2]); - (unfold sp_not); + Proofview.V82.tactic (clear [aux1;aux2]); + Proofview.V82.tactic (unfold sp_not); (intros_using [aux]); - (resolve_id aux); - (mk_then tac); + Proofview.V82.tactic (resolve_id aux); + Proofview.V82.tactic (mk_then tac); assumption ] ; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ] | EXACT_DIVIDE (e1,k) :: l -> let id = hyp_of_tag e1.id in @@ -1194,38 +1179,38 @@ let replay_history tactic_normalisation = and eq2 = val_of(decompile e2) in let kk = mk_integer k in let state_eq = mk_eq eq1 (mk_times eq2 kk) in - if e1.kind = DISE then + if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS + Tacticals.New.tclTHENS (cut state_eq) - [tclTHENLIST [ + [Tacticals.New.tclTHENLIST [ (intros_using [aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA18, [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); - (clear [aux1;id]); + Proofview.V82.tactic (clear [aux1;id]); (intros_using [id]); (loop l) ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS (cut state_eq) + Tacticals.New.tclTHENS (cut state_eq) [ - tclTHENS + Tacticals.New.tclTHENS (cut (mk_gt kk izero)) - [tclTHENLIST [ + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); - (clear [aux1;aux2;id]); + Proofview.V82.tactic (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1238,16 +1223,16 @@ let replay_history tactic_normalisation = (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: scalar_norm [P_APP 3] e1.body in - tclTHENS + Tacticals.New.tclTHENS (cut (mk_eq eq1 (mk_inv eq2))) - [tclTHENLIST [ + [Tacticals.New.tclTHENLIST [ (intros_using [aux]); - (generalize_tac [mkApp (Lazy.force coq_OMEGA8, + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); - (clear [id1;id2;aux]); + Proofview.V82.tactic (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; - tclTHEN (mk_then tac) reflexivity] + Tacticals.New.tclTHEN (Proofview.V82.tactic (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 () @@ -1271,21 +1256,21 @@ 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 - tclTHENS + Tacticals.New.tclTHENS (cut theorem) - [tclTHENLIST [ + [Tacticals.New.tclTHENLIST [ (intros_using [aux]); (elim_id aux); - (clear [aux]); + Proofview.V82.tactic (clear [aux]); (intros_using [vid; aux]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - (mk_then tac); - (clear [aux]); + Proofview.V82.tactic (mk_then tac); + Proofview.V82.tactic (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac eq1) reflexivity ] + Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1294,10 +1279,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 - tclTHENS + Tacticals.New.tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ]; - tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]] + [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) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1305,7 +1290,7 @@ let replay_history tactic_normalisation = and id2 = hyp_of_tag e2.id in let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in - if k1 =? one & e2.kind = EQUA then + if k1 =? one && e2.kind == EQUA then let tac_thm = match e1.kind with | EQUA -> Lazy.force coq_OMEGA5 @@ -1314,12 +1299,12 @@ let replay_history tactic_normalisation = in let kk = mk_integer k2 in let p_initial = - if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in + 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 - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - (mk_then tac); + Proofview.V82.tactic (mk_then tac); (intros_using [id]); (loop l) ] @@ -1328,43 +1313,43 @@ 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 - tclTHENS (cut (mk_gt kk1 izero)) - [tclTHENS + Tacticals.New.tclTHENS (cut (mk_gt kk1 izero)) + [Tacticals.New.tclTHENS (cut (mk_gt kk2 izero)) - [tclTHENLIST [ + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| eq1;eq2;kk1;kk2; mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); - (clear [aux1;aux2]); - (mk_then tac); + Proofview.V82.tactic (clear [aux1;aux2]); + Proofview.V82.tactic (mk_then tac); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl + Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> - tclTHEN (resolve_id (hyp_of_tag e)) reflexivity + Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity | CONSTANT_NEG(e,k) :: l -> - tclTHENLIST [ - (generalize_tac [mkVar (hyp_of_tag e)]); - (unfold sp_Zle); - simpl_in_concl; - (unfold sp_not); + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]); + Proofview.V82.tactic (unfold sp_Zle); + Proofview.V82.tactic simpl_in_concl; + Proofview.V82.tactic (unfold sp_not); (intros_using [aux]); - (resolve_id aux); + Proofview.V82.tactic (resolve_id aux); reflexivity ] - | _ -> tclIDTAC + | _ -> Proofview.tclUNIT () in loop @@ -1382,21 +1367,21 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) (tclTRY (clear [id])) in - if tac <> [] then + if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ])) + ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) else (tactic,defs) let destructure_omega gl tac_def (id,c) = - if atompart_of_id id = "State" then + if String.equal (atompart_of_id id) "State" then tac_def else try match destructurate_prop c with | Kapp(Eq,[typ;t1;t2]) - when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) -> + when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end -> let t = mk_plus t1 (mk_inv t2) in normalize_equation id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def @@ -1425,12 +1410,18 @@ let destructure_omega gl tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - tclTHEN (tclTRY (clear [id])) (intro_using id) + Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id) + -let coq_omega gl = +open Proofview.Notations + +let coq_omega = + Proofview.Goal.nf_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 tactic_normalisation, system = - List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in + List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = List.fold_left (fun (tac,sys) (t,(v,th,b)) -> @@ -1438,78 +1429,81 @@ let coq_omega gl = let id = new_identifier () in let i = new_id () in tag_hypothesis id i; - (tclTHENLIST [ + (Tacticals.New.tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); - (clear [id]); + Proofview.V82.tactic (clear [id]); (intros_using [th;id]); tac ]), {kind = INEQ; body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else - (tclTHENLIST [ + (Tacticals.New.tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), sys) - (tclIDTAC,[]) (dump_tables ()) + (Proofview.tclUNIT (),[]) (dump_tables ()) in let system = system @ sys in if !display_system_flag then display_system display_var system; if !old_style_flag then begin try let _ = simplify (new_id,new_var_num,display_var) false system in - tclIDTAC gl + Proofview.tclUNIT () with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) gl + (Tacticals.New.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; - (tclTHEN prelude (replay_history tactic_normalisation path)) gl - with NO_CONTRADICTION -> error "Omega can't solve this system" + Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) + with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) + end end -let coq_omega = solver_time coq_omega +let coq_omega = coq_omega -let nat_inject gl = - let rec explore p t = +let nat_inject = + Proofview.Goal.nf_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 | Kapp(Plus,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (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]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (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 - tclTHENS - (tclTHEN + Tacticals.New.tclTHENS + (Tacticals.New.tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ - tclTHENLIST [ - (clever_rewrite_gen p + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (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) ]; - (tclTHEN - (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (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']) -> @@ -1520,37 +1514,37 @@ let nat_inject gl = | _ -> false with e when catchable_exception e -> false in - let rec loop p t = + let rec loop p t : unit Proofview.tactic = try match destructurate_term t with Kapp(S,[t]) -> - (tclTHEN - (clever_rewrite_gen p + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (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 focused_simpl p else loop p t + if is_number t' then Proofview.V82.tactic (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 - tclTHEN - (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t])) + Tacticals.New.tclTHEN + (Proofview.V82.tactic (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,[]) -> focused_simpl p - | _ -> tclIDTAC - with e when catchable_exception e -> tclIDTAC + | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p) + | _ -> Proofview.tclUNIT () + with e when catchable_exception e -> Proofview.tclUNIT () and loop = function - | [] -> tclIDTAC + | [] -> Proofview.tclUNIT () | (i,t)::lit -> begin try match destructurate_prop t with Kapp(Le,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1558,8 +1552,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Lt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1567,8 +1561,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Ge,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1576,8 +1570,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Gt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1585,8 +1579,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Neq,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1594,9 +1588,9 @@ let nat_inject gl = (loop lit) ] | Kapp(Eq,[typ;t1;t2]) -> - if pf_conv_x gl typ (Lazy.force coq_nat) then - tclTHENLIST [ - (generalize_tac + if is_conv typ (Lazy.force coq_nat) then + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); (explore [P_APP 3; P_TYPE] t2); @@ -1607,7 +1601,9 @@ let nat_inject gl = | _ -> loop lit with e when catchable_exception e -> loop lit end in - loop (List.rev (pf_hyps_types gl)) gl + let hyps_types = Tacmach.New.pf_hyps_types gl in + loop (List.rev hyps_types) + end let dec_binop = function | Zne -> coq_dec_Zne @@ -1675,51 +1671,57 @@ let rec decidability gl t = let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) - tclTHEN - (tclTRY (clear [id])) - (fun gl -> - let id = fresh_id [] id gl in - tclTHEN (introduction id) (tac id) gl) + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclTRY (clear [id]))) + (Proofview.Goal.nf_enter begin fun gl -> + let id = Tacmach.New.of_old (fresh_id [] id) gl in + Tacticals.New.tclTHEN (introduction id) (tac id) + end) let onClearedName2 id tac = - tclTHEN - (tclTRY (clear [id])) - (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 ] gl) - -let destructure_hyps gl = - let rec loop = function - | [] -> (tclTHEN nat_inject coq_omega) - | (i,body,t)::lit -> - begin try match destructurate_prop t with + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclTRY (clear [id]))) + (Proofview.Goal.nf_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) + +let destructure_hyps = + Proofview.Goal.nf_enter begin fun gl -> + let type_of = Tacmach.New.pf_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 rec loop = function + | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) + | (i,body,t)::lit -> + begin try match destructurate_prop t with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> - (tclTHENS - (elim_id i) - [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); - onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) + (Tacticals.New.tclTHENS + (elim_id i) + [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); + onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> - tclTHEN + Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop ((i1,None,t1)::(i2,None,t2)::lit))) | Kapp(Iff,[t1;t2]) -> - tclTHEN + Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop ((i1,None,mkArrow t1 t2)::(i2,None,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 (pf_type_of gl t2) + if is_Prop (type_of t2) then - let d1 = decidability gl t1 in - tclTHENLIST [ - (generalize_tac [mkApp (Lazy.force coq_imp_simp, - [| t1; t2; d1; mkVar i|])]); + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp, + [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> (loop ((i,None,mk_or (mk_not t1) t2)::lit)))) ] @@ -1727,135 +1729,138 @@ let destructure_hyps gl = loop lit | Kapp(Not,[t]) -> begin match destructurate_prop t with - Kapp(Or,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) - ] - | Kapp(And,[t1;t2]) -> - let d1 = decidability gl t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_and, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))) - ] - | Kapp(Iff,[t1;t2]) -> - let d1 = decidability gl t1 in - let d2 = decidability gl t2 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_iff, - [| t1; t2; d1; d2; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None, - mk_or (mk_and t1 (mk_not t2)) - (mk_and (mk_not t1) t2))::lit)))) - ] - | Kimp(t1,t2) -> + Kapp(Or,[t1;t2]) -> + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) + ] + | Kapp(And,[t1;t2]) -> + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_and, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))) + ] + | Kapp(Iff,[t1;t2]) -> + let d1 = decidability t1 in + let d2 = decidability t2 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_iff, + [| t1; t2; d1; d2; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None, + mk_or (mk_and t1 (mk_not t2)) + (mk_and (mk_not t1) t2))::lit)))) + ] + | Kimp(t1,t2) -> (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. For t1, being decidable implies being Prop. *) - let d1 = decidability gl t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_imp, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) - ] - | Kapp(Not,[t]) -> - let d = decidability gl t in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop ((i,None,t)::lit)))) - ] - | Kapp(op,[t1;t2]) -> - (try - let thm = not_binop op in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); - (onClearedName i (fun _ -> loop lit)) - ] - with Not_found -> loop lit) - | Kapp(Eq,[typ;t1;t2]) -> - if !old_style_flag then begin - match destructurate_type (pf_nf gl typ) with - | Kapp(Nat,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | Kapp(Z,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | _ -> loop lit - end else begin - match destructurate_type (pf_nf gl typ) with - | Kapp(Nat,_) -> - (tclTHEN - (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|])))) - (loop lit)) - | Kapp(Z,_) -> - (tclTHEN - (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) - (loop lit)) - | _ -> loop lit - end - | _ -> loop lit + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_imp, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) + ] + | Kapp(Not,[t]) -> + let d = decidability t in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); + (onClearedName i (fun i -> (loop ((i,None,t)::lit)))) + ] + | Kapp(op,[t1;t2]) -> + (try + let thm = not_binop op in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + with Not_found -> loop lit) + | Kapp(Eq,[typ;t1;t2]) -> + if !old_style_flag then begin + match destructurate_type (pf_nf typ) with + | Kapp(Nat,_) -> + Tacticals.New.tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Z,_) -> + Tacticals.New.tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | _ -> loop lit + end else begin + match destructurate_type (pf_nf typ) with + | Kapp(Nat,_) -> + (Tacticals.New.tclTHEN + (convert_hyp_no_check + (i,body, + (mkApp (Lazy.force coq_neq, [| t1;t2|])))) + (loop lit)) + | Kapp(Z,_) -> + (Tacticals.New.tclTHEN + (convert_hyp_no_check + (i,body, + (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) + (loop lit)) + | _ -> loop lit + end + | _ -> loop lit end | _ -> loop lit - with - | Undecidable -> loop lit - | e when catchable_exception e -> loop lit - end - in - loop (pf_hyps gl) gl + with + | Undecidable -> loop lit + | e when catchable_exception e -> loop lit + end + in + let hyps = Proofview.Goal.hyps gl in + loop hyps + end -let destructure_goal gl = - let concl = pf_concl gl in - let rec loop t = - match destructurate_prop t with +let destructure_goal = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let decidability = Tacmach.New.of_old decidability gl in + let rec loop t = + match destructurate_prop t with | Kapp(Not,[t]) -> - (tclTHEN - (tclTHEN (unfold sp_not) intro) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro) destructure_hyps) - | Kimp(a,b) -> (tclTHEN intro (loop b)) + | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> - let goal_tac = - try - let dec = decidability gl t in - tclTHEN - (Tactics.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))) - intro - with Undecidable -> Tactics.elim_type (build_coq_False ()) - in - tclTHEN goal_tac destructure_hyps - in - (loop concl) gl + let goal_tac = + try + let dec = decidability t in + Tacticals.New.tclTHEN + (Proofview.V82.tactic (Tactics.refine + (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) + intro + with Undecidable -> Tactics.elim_type (build_coq_False ()) + in + Tacticals.New.tclTHEN goal_tac destructure_hyps + in + (loop concl) + end -let destructure_goal = all_time (destructure_goal) +let destructure_goal = destructure_goal -let omega_solver gl = +let omega_solver = + Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *) Coqlib.check_required_library ["Coq";"omega";"Omega"]; reset_all (); - let result = destructure_goal gl in - (* if !display_time_flag then begin text_time (); - flush Pervasives.stdout end; *) - result + destructure_goal diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index b2a5b5dc..46bbe2fd 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Tacinterp.interp <:tactic> | "N" -> Tacinterp.interp <:tactic> | "Z" -> Tacinterp.interp <:tactic> - | s -> Util.error ("No Omega knowledge base for type "^s)) - (Util.list_uniquize (List.sort compare l)) + | s -> Errors.error ("No Omega knowledge base for type "^s)) + (Util.List.sort_uniquize String.compare l) in - tclTHEN - (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) - omega_solver + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) + (omega_solver) TACTIC EXTEND omega @@ -39,7 +40,7 @@ END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.string_of_id l) ] + [ omega_tactic (List.map Names.Id.to_string l) ] | [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 94ce4d50..67a1ff96 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* bigint -> bool val less_than : bigint -> bigint -> bool val add : bigint -> bigint -> bigint val sub : bigint -> bigint -> bigint @@ -34,26 +33,26 @@ end let debug = ref false -module MakeOmegaSolver (Int:INT) = struct - -type bigint = Int.bigint -let (?) x y = Int.less_than y x -let (>=?) x y = Int.less_than y x or x = y -let (=?) = (=) -let (+) = Int.add -let (-) = Int.sub -let ( * ) = Int.mult -let (/) x y = fst (Int.euclid x y) -let (mod) x y = snd (Int.euclid x y) -let zero = Int.zero -let one = Int.one +module MakeOmegaSolver (I:INT) = struct + +type bigint = I.bigint +let (=?) = I.equal +let (?) x y = I.less_than y x +let (>=?) x y = I.less_than y x || x = y +let (+) = I.add +let (-) = I.sub +let ( * ) = I.mult +let (/) x y = fst (I.euclid x y) +let (mod) x y = snd (I.euclid x y) +let zero = I.zero +let one = I.one let two = one + one -let negone = Int.neg one -let abs x = if Int.less_than x zero then Int.neg x else x -let string_of_bigint = Int.to_string -let neg = Int.neg +let negone = I.neg one +let abs x = if I.less_than x zero then I.neg x else x +let string_of_bigint = I.to_string +let neg = I.neg (* To ensure that polymorphic (<) is not used mistakenly on big integers *) (* Warning: do not use (=) either on big int *) @@ -241,7 +240,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = Sort.list (fun x y -> x.v > y.v) +let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) @@ -303,16 +302,16 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = end end else let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA & x mod gcd <> zero then begin + if eq_flag=EQUA && x mod gcd <> zero then begin add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE & x mod gcd <> zero then begin + end else if eq_flag=DISE && x mod gcd <> zero then begin add_event (FORGET_C eq.id); [] end else if gcd <> one then begin let c = floor_div x gcd in let d = x - c * gcd in let new_eq = {id=id; kind=eq_flag; constant=c; body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd) + add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); [new_eq] end else [eq] @@ -352,11 +351,11 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let new_eq = List.hd (normalize new_eq) in let eliminated_var, def = chop_var var new_eq.body in let other_equations = - Util.list_map_append + Util.List.map_append (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in let inequations = - Util.list_map_append + Util.List.map_append (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in @@ -368,9 +367,9 @@ let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e, if !debug then display_system print_var (e::other); try let v,def = chop_factor_1 e.body in - (Util.list_map_append + (Util.List.map_append (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, - Util.list_map_append + Util.List.map_append (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) with FACTOR1 -> eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) @@ -474,7 +473,7 @@ let select_variable system = Hashtbl.iter (fun v ({contents = c}) -> incr var_cpt; - if c add_event (HYP e)) system; - let system = Util.list_map_append normalize system in + let system = Util.List.map_append normalize system in let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in let system = (eqs @ simp_eq,simp_ineq) in @@ -547,30 +546,30 @@ let rec depend relie_on accu = function | act :: l -> begin match act with | DIVIDE_AND_APPROX (e,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | EXACT_DIVIDE (e,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | WEAKEN (e,_) -> - if List.mem e relie_on then depend relie_on (act::accu) l + if Int.List.mem e relie_on then depend relie_on (act::accu) l else depend relie_on accu l | SUM (e,(_,e1),(_,e2)) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2.id::relie_on) (act::accu) l else depend relie_on accu l | STATE {st_new_eq=e;st_orig=o} -> - if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l + if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l else depend relie_on accu l | HYP e -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | FORGET_C _ -> depend relie_on accu l | FORGET _ -> depend relie_on accu l | FORGET_I _ -> depend relie_on accu l | MERGE_EQ (e,e1,e2) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2::relie_on) (act::accu) l else depend relie_on accu l @@ -586,15 +585,6 @@ let rec depend relie_on accu = function end | [] -> relie_on, accu -(* -let depend relie_on accu trace = - Printf.printf "Longueur de la trace initiale : %d\n" - (trace_length trace + trace_length accu); - let rel',trace' = depend relie_on accu trace in - Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace'); - rel',trace' -*) - 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 ()))) @@ -658,7 +648,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = | ([],ineqs,expl_map) -> ineqs,expl_map in try - let system = Util.list_map_append normalize system in + let system = Util.List.map_append normalize system in let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in @@ -674,7 +664,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = try let _ = loop2 sys in raise NO_CONTRADICTION with UNSOLVABLE -> let relie_on,path = depend [] [] (history ()) in - let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in + let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in let red = List.map (fun (x,_,_) -> x) dc in (red,relie_on,decomp,path)) sys_exploded @@ -699,14 +689,16 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = | [] -> failwith "solve" in let s1,s2 = List.partition (fun (_,_,decomp,_) -> sign decomp) systems in - let s1' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in - let s2' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in + let remove_int (dep,ro,dc,pa) = + (Util.List.except Int.equal id dep,ro,dc,pa) + in + let s1' = List.map remove_int s1 in + let s2' = List.map remove_int s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in - let (eq,id1,id2) = List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2 + let (eq,id1,id2) = Int.List.assoc id explode_map in + [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], + eq.id :: Util.List.union Int.equal relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) in let act,relie_on = solve all_solutions in -- cgit v1.2.3