aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--printing/printer.ml9
-rw-r--r--proofs/logic.ml46
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/tacmach.ml10
-rw-r--r--proofs/tacmach.mli3
-rw-r--r--tactics/tactics.ml87
-rw-r--r--test-suite/success/forward.v11
7 files changed, 79 insertions, 89 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 3b0b6d5d2..6c571f424 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -845,15 +845,6 @@ let pr_goal_by_uid uid =
(* Elementary tactics *)
let pr_prim_rule = function
- | Cut (b,replace,id,t) ->
- if b then
- (* TODO: express "replace" *)
- (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
- else
- let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
- (str"cut " ++ pr_constr t ++
- str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
-
| Refine c ->
(** FIXME *)
str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0621af4e8..db9e847c0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -22,7 +22,6 @@ open Proof_type
open Type_errors
open Retyping
open Misctypes
-open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
@@ -93,15 +92,6 @@ let check_typability env sigma c =
(* Implementation of the structural rules (moving and deleting
hypotheses around) *)
-(* The Clear tactic: it scans the context for hypotheses to be removed
- (instead of iterating on the list of identifier to be removed, which
- forces the user to give them in order). *)
-
-let clear_hyps2 env sigma ids sign t cl =
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
- (hyps, t, cl, !evdref)
-
(* The ClearBody tactic *)
(* Reordering of the context *)
@@ -200,14 +190,6 @@ let move_location_eq m1 m2 = match m1, m2 with
| MoveFirst, MoveFirst -> true
| _ -> false
-let rec get_hyp_after h = function
- | [] -> error_no_such_hypothesis h
- | d :: right ->
- if Id.equal (NamedDecl.get_id d) h then
- match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst
- else
- get_hyp_after h right
-
let split_sign hfrom hto l =
let rec splitrec left toleft = function
| [] -> error_no_such_hypothesis hfrom
@@ -539,37 +521,9 @@ let convert_hyp check sign sigma d =
(* Primitive tactics are handled here *)
let prim_refiner r sigma goal =
- let env = Goal.V82.env sigma goal in
- let sign = Goal.V82.hyps sigma goal in
let cl = Goal.V82.concl sigma goal in
- let mk_goal hyps concl =
- Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
- in
- let open EConstr in
match r with
(* Logical rules *)
- | Cut (b,replace,id,t) ->
-(* if !check && not (Retyping.get_sort_of env sigma t) then*)
- let t = EConstr.of_constr t in
- let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
- let sign,t,cl,sigma =
- if replace then
- let nexthyp = get_hyp_after id (named_context_of_val sign) in
- let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
- move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign)
- nexthyp,
- t,cl,sigma
- else
- (if !check && mem_named_context_val id sign then
- user_err ~hdr:"Logic.prim_refiner"
- (str "Variable " ++ pr_id id ++ str " is already declared.");
- push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
- let (sg2,ev2,sigma) =
- Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
- let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in
- let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
- if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
-
| Refine c ->
let cl = EConstr.Unsafe.to_constr cl in
check_meta_variables c;
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index e59db9e42..ec4af86b9 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -9,14 +9,12 @@
(** Legacy proof engine. Do not use in newly written code. *)
open Evd
-open Names
open Term
(** This module defines the structure of proof tree and the tactic type. So, it
is used by [Proof_tree] and [Refiner] *)
type prim_rule =
- | Cut of bool * bool * Id.t * types
| Refine of constr
(** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f9d9f25cc..bdfa399aa 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -115,22 +115,12 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c
let refiner = refiner
-let internal_cut_no_check replace id t gl =
- let t = EConstr.Unsafe.to_constr t in
- refiner (Cut (true,replace,id,t)) gl
-
-let internal_cut_rev_no_check replace id t gl =
- let t = EConstr.Unsafe.to_constr t in
- refiner (Cut (false,replace,id,t)) gl
-
let refine_no_check c gl =
let c = EConstr.Unsafe.to_constr c in
refiner (Refine c) gl
(* Versions with consistency checks *)
-let internal_cut b d t = with_check (internal_cut_no_check b d t)
-let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
let refine c = with_check (refine_no_check c)
(* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 3d2fa72c1..aac7b90ee 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -84,13 +84,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
(** {6 The most primitive tactics. } *)
val refiner : rule -> tactic
-val internal_cut_no_check : bool -> Id.t -> types -> tactic
val refine_no_check : constr -> tactic
(** {6 The most primitive tactics with consistency and type checking } *)
-val internal_cut : bool -> Id.t -> types -> tactic
-val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
(** {6 Pretty-printing functions (debug only). } *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 689cc48aa..061eca10b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -439,16 +439,66 @@ let find_name mayrepl decl naming gl = match naming with
(* Cut rule *)
(**************************************************************)
+let clear_hyps2 env sigma ids sign t cl =
+ try
+ let evdref = ref (Evd.clear_metas sigma) in
+ let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
+ (hyps, t, cl, !evdref)
+ with Evarutil.ClearDependencyError (id,err) ->
+ error_replacing_dependency env sigma id err
+
+let rec get_hyp_after h = function
+ | [] -> error_no_such_hypothesis h
+ | d :: right ->
+ if Id.equal (NamedDecl.get_id d) h then
+ match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst
+ else
+ get_hyp_after h right
+
+let internal_cut_gen ?(check=true) dir replace id t =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let concl = Proofview.Goal.concl gl in
+ let store = Proofview.Goal.extra gl in
+ let sign = named_context_val env in
+ let sign',t,concl,sigma =
+ if replace then
+ let nexthyp = get_hyp_after id (named_context_of_val sign) in
+ let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+ let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
+ sign',t,concl,sigma
+ else
+ (if check && mem_named_context_val id sign then
+ user_err (str "Variable " ++ pr_id id ++ str " is already declared.");
+ push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in
+ let nf_t = nf_betaiota sigma t in
+ Proofview.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (Refine.refine ~typecheck:false begin fun sigma ->
+ let (sigma,ev,ev') =
+ if dir then
+ let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ (sigma,ev,ev')
+ else
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
+ (sigma,ev,ev') in
+ let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
+ (sigma, term)
+ end)
+ end
+
+let internal_cut ?(check=true) = internal_cut_gen ~check true
+let internal_cut_rev ?(check=true) = internal_cut_gen ~check false
+
let assert_before_then_gen b naming t tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
Tacticals.New.tclTHENLAST
- (Proofview.V82.tactic
- (fun gl ->
- try Tacmach.internal_cut b id t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency (pf_env gl) (project gl) id err))
+ (internal_cut b id t)
(tac id)
end
@@ -463,11 +513,7 @@ let assert_after_then_gen b naming t tac =
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
Tacticals.New.tclTHENFIRST
- (Proofview.V82.tactic
- (fun gl ->
- try Tacmach.internal_cut_rev b id t gl
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency (pf_env gl) (project gl) id err))
+ (internal_cut_rev b id t)
(tac id)
end
@@ -3805,11 +3851,12 @@ let compare_upto_variables sigma x y =
in
compare x y
-let specialize_eqs id gl =
+let specialize_eqs id =
let open Context.Rel.Declaration in
- let env = Tacmach.pf_env gl in
- let ty = Tacmach.pf_get_hyp_typ gl id in
- let evars = ref (project gl) in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let ty = Tacmach.New.pf_get_hyp_typ id gl in
+ let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
in
@@ -3852,16 +3899,18 @@ let specialize_eqs id gl =
and acc' = Tacred.whd_simpl env !evars acc' in
let ty' = Evarutil.nf_evar !evars ty' in
if worked then
- tclTHENFIRST (Tacmach.internal_cut true id ty')
- (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
- else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
-
+ Tacticals.New.tclTHENFIRST
+ (internal_cut true id ty')
+ (exact_no_check ((* refresh_universes_strict *) acc'))
+ else
+ Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id)
+ end
let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
let msg = str "Specialization not allowed on dependent hypotheses" in
Proofview.tclOR (clear [id])
(fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
- Proofview.V82.tactic (specialize_eqs id)
+ specialize_eqs id
end
let occur_rel sigma n c =
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
index 0ed5b524f..4e36dec15 100644
--- a/test-suite/success/forward.v
+++ b/test-suite/success/forward.v
@@ -16,3 +16,14 @@ eremember (S (S ?[x])).
instantiate (x:=0).
reflexivity.
Qed.
+
+(* Don't know if it is good or not but the compatibility tells that
+ the asserted goal to prove is subject to beta-iota but not the
+ asserted hypothesis *)
+
+Goal True.
+assert ((fun x => x) False).
+Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *)
+2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *)
+Abort.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 15:22:58 +0000