summaryrefslogtreecommitdiff
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/rules.ml')
-rw-r--r--plugins/firstorder/rules.ml102
1 files changed, 52 insertions, 50 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b043ba5f..382d5409 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,22 +1,24 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Errors
open Util
open Names
open Term
+open Vars
open Tacmach
open Tactics
open Tacticals
open Termops
-open Declarations
open Formula
open Sequent
-open Libnames
+open Globnames
+open Locus
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
@@ -25,13 +27,13 @@ type lseqtac= global_reference -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq gls=
- check_for_interrupt ();
+ Control.check_for_interrupt ();
let nc=pf_hyps gls in
let env=pf_env gls in
let rec aux i nc ctx=
if i<=0 then seq else
match nc with
- []->anomaly "Not the expected number of hyps"
+ []->anomaly (Pp.str "Not the expected number of hyps")
| ((id,_,typ) as nd)::q->
if occur_var env id (pf_concl gls) ||
List.exists (occur_var_in_decl env id) ctx then
@@ -51,38 +53,38 @@ let clear_global=function
VarRef id->clear [id]
| _->tclIDTAC
-
(* connection rules *)
let axiom_tac t seq=
- try exact_no_check (constr_of_global (find_left t seq))
+ try pf_constr_of_global (find_left t seq) exact_no_check
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
tclIFTHENELSE
(try
tclTHENLIST
- [generalize [mkApp(constr_of_global id,
- [|constr_of_global (find_left a seq)|])];
+ [pf_constr_of_global (find_left a seq) (fun left ->
+ pf_constr_of_global id (fun id ->
+ generalize [mkApp(id, [|left|])]));
clear_global id;
- intro]
+ Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
(wrap 1 false continue seq) backtrack
(* right connectives rules *)
let and_tac backtrack continue seq=
- tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
+ tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack
let or_tac backtrack continue seq=
tclORELSE
- (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
+ (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq))))))
backtrack
let arrow_tac backtrack continue seq=
- tclIFTHENELSE intro (wrap 1 true continue seq)
+ tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq)
(tclORELSE
- (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
+ (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq)))
backtrack)
(* left connectives rules *)
@@ -90,9 +92,9 @@ let left_and_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
(tclTHENLIST
- [simplest_elim (constr_of_global id);
+ [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
clear_global id;
- tclDO n intro])
+ tclDO n (Proofview.V82.of_tactic intro)])
(wrap n false continue seq)
backtrack gls
@@ -101,59 +103,58 @@ let left_or_tac ind backtrack id continue seq gls=
let f n=
tclTHENLIST
[clear_global id;
- tclDO n intro;
+ tclDO n (Proofview.V82.of_tactic intro);
wrap n false continue seq] in
tclIFTHENSVELSE
- (simplest_elim (constr_of_global id))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
(Array.map f v)
backtrack gls
let left_false_tac id=
- simplest_elim (constr_of_global id)
+ Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
(* left arrow connective rules *)
(* We use this function for false, and, or, exists *)
-let ll_ind_tac ind largs backtrack id continue seq gl=
- let rcs=ind_hyps 0 ind largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
+ let rcs=ind_hyps 0 indu largs gl in
let vargs=Array.of_list largs in
- (* construire le terme H->B, le generaliser etc *)
- let myterm i=
+ (* construire le terme H->B, le generaliser etc *)
+ let myterm idc i=
let rc=rcs.(i) in
let p=List.length rc in
- let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
+ let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
- let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
- it_mkLambda_or_LetIn head rc in
+ let head=mkApp ((lift p idc),[|capply|]) in
+ it_mkLambda_or_LetIn head rc in
let lp=Array.length rcs in
- let newhyps=list_tabulate myterm lp in
+ let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
(tclTHENLIST
- [generalize newhyps;
+ [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
clear_global id;
- tclDO lp intro])
+ tclDO lp (Proofview.V82.of_tactic intro)])
(wrap lp false continue seq) backtrack gl
let ll_arrow_tac a b c backtrack id continue seq=
let cc=mkProd(Anonymous,a,(lift 1 b)) in
- let d=mkLambda (Anonymous,b,
- mkApp ((constr_of_global id),
- [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+ let d idc =mkLambda (Anonymous,b,
+ mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclORELSE
- (tclTHENS (cut c)
+ (tclTHENS (Proofview.V82.of_tactic (cut c))
[tclTHENLIST
- [introf;
+ [Proofview.V82.of_tactic introf;
clear_global id;
wrap 1 false continue seq];
- tclTHENS (cut cc)
- [exact_no_check (constr_of_global id);
+ tclTHENS (Proofview.V82.of_tactic (cut cc))
+ [pf_constr_of_global id exact_no_check;
tclTHENLIST
- [generalize [d];
+ [pf_constr_of_global id (fun idc -> generalize [d idc]);
clear_global id;
- introf;
- introf;
+ Proofview.V82.of_tactic introf;
+ Proofview.V82.of_tactic introf;
tclCOMPLETE (wrap 2 true continue seq)]]])
backtrack
@@ -161,9 +162,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
let forall_tac backtrack continue seq=
tclORELSE
- (tclIFTHENELSE intro (wrap 0 true continue seq)
+ (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq)
(tclORELSE
- (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+ (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq)))
backtrack))
(if !qflag then
tclFAIL 0 (Pp.str "reversible in 1st order mode")
@@ -173,24 +174,25 @@ let forall_tac backtrack continue seq=
let left_exists_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
- (simplest_elim (constr_of_global id))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
(tclTHENLIST [clear_global id;
- tclDO n intro;
+ tclDO n (Proofview.V82.of_tactic intro);
(wrap (n-1) false continue seq)])
backtrack
gls
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
- (tclTHENS (cut prod)
+ (tclTHENS (Proofview.V82.of_tactic (cut prod))
[tclTHENLIST
- [intro;
+ [Proofview.V82.of_tactic intro;
+ pf_constr_of_global id (fun idc ->
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
- let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls);
+ let term=mkApp(idc,[|mkVar(id0)|]) in
+ tclTHEN (generalize [term]) (clear [id0]) gls));
clear_global id;
- intro;
+ Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
tclCOMPLETE (wrap 0 true continue (deepen seq))])
backtrack
@@ -202,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
let defined_connectives=lazy
- [all_occurrences,EvalConstRef (destConst (constant "not"));
- all_occurrences,EvalConstRef (destConst (constant "iff"))]
+ [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
+ AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
let normalize_evaluables=
onAllHypsAndConcl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 08:05:57 +0000