aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--printing/printer.ml3
-rw-r--r--proofs/logic.ml40
-rw-r--r--proofs/proof_type.ml1
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/tacmach.ml5
-rw-r--r--proofs/tacmach.mli1
-rw-r--r--tactics/tacinterp.ml5
-rw-r--r--tactics/tactics.ml63
-rw-r--r--tactics/tactics.mli2
10 files changed, 58 insertions, 65 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b5566127f..8f20cea6b 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -222,7 +222,7 @@ let add_justification_hyps keep items gls =
let id=pf_get_new_id local_hyp_prefix gls in
keep:=Id.Set.add id !keep;
tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
- (Proofview.V82.of_tactic (clear_body [id])) gls in
+ (thin_body [id]) gls in
tclMAP add_aux items gls
let prepare_goal items gls =
diff --git a/printing/printer.ml b/printing/printer.ml
index f105e8031..8c7dbac33 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -663,6 +663,9 @@ let pr_prim_rule = function
| Thin ids ->
(str"clear " ++ pr_sequence pr_id ids)
+ | ThinBody ids ->
+ (str"clearbody " ++ pr_sequence pr_id ids)
+
| Move (withdep,id1,id2) ->
(str (if withdep then "dependent " else "") ++
str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b9cff0527..a7538193b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -113,6 +113,35 @@ let clear_hyps2 sigma ids sign t cl =
(* The ClearBody tactic *)
+let recheck_typability (what,id) env sigma t =
+ try check_typability env sigma t
+ with e when Errors.noncritical e ->
+ let s = match what with
+ | None -> "the conclusion"
+ | Some id -> "hypothesis "^(Id.to_string id) in
+ error
+ ("The correctness of "^s^" relies on the body of "^(Id.to_string id))
+
+let remove_hyp_body env sigma id =
+ let sign =
+ apply_to_hyp_and_dependent_on (named_context_val env) id
+ (fun (_,c,t) _ ->
+ match c with
+ | None -> error ((Id.to_string id)^" is not a local definition.")
+ | Some c ->(id,None,t))
+ (fun (id',c,t as d) sign ->
+ (if !check then
+ begin
+ let env = reset_with_named_context sign env in
+ match c with
+ | None -> recheck_typability (Some id',id) env sigma t
+ | Some b ->
+ let b' = mkCast (b,DEFAULTcast, t) in
+ recheck_typability (Some id',id) env sigma b'
+ end;d))
+ in
+ reset_with_named_context sign env
+
(* Reordering of the context *)
(* faire le minimum d'echanges pour que l'ordre donne soit un *)
@@ -679,6 +708,17 @@ let prim_refiner r sigma goal =
let sigma = Goal.V82.partial_solution sigma goal ev in
([gl], sigma)
+ | ThinBody ids ->
+ let clear_aux env id =
+ let env' = remove_hyp_body env sigma id in
+ if !check then recheck_typability (None,id) env' sigma cl;
+ env'
+ in
+ let sign' = named_context_val (List.fold_left clear_aux env ids) in
+ let (sg,ev,sigma) = mk_goal sign' cl in
+ let sigma = Goal.V82.partial_solution sigma goal ev in
+ ([sg], sigma)
+
| Move (withdep, hfrom, hto) ->
let (left,right,declfrom,toleft) =
split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 76459a59a..7297706e1 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -35,6 +35,7 @@ type prim_rule =
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
| Thin of Id.t list
+ | ThinBody of Id.t list
| Move of bool * Id.t * Id.t move_location
| Rename of Id.t * Id.t
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index bbb2c8e09..0aadd862b 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -27,6 +27,7 @@ type prim_rule =
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
| Thin of Id.t list
+ | ThinBody of Id.t list
| Move of bool * Id.t * Id.t move_location
| Rename of Id.t * Id.t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6c72009d4..f87d03183 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -127,6 +127,10 @@ let convert_hyp_no_check d gl =
let thin_no_check ids gl =
if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
+(* This does not check dependencies *)
+let thin_body_no_check ids gl =
+ if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl
+
let move_hyp_no_check with_dep id1 id2 gl =
refiner (Move (with_dep,id1,id2)) gl
@@ -151,6 +155,7 @@ let refine c = with_check (refine_no_check c)
let convert_concl d sty = with_check (convert_concl_no_check d sty)
let convert_hyp d = with_check (convert_hyp_no_check d)
let thin c = with_check (thin_no_check c)
+let thin_body c = with_check (thin_body_no_check c)
let move_hyp b id id' = with_check (move_hyp_no_check b id id')
let rename_hyp l = with_check (rename_hyp_no_check l)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cebe78ed0..c7729e416 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -100,6 +100,7 @@ val refine : constr -> tactic
val convert_concl : types -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
val thin : Id.t list -> tactic
+val thin_body : Id.t list -> tactic
val move_hyp : bool -> Id.t -> Id.t move_location -> tactic
val rename_hyp : (Id.t*Id.t) list -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 12a8c4ae9..16e785180 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1928,9 +1928,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
if b then Tactics.keep l gl else Tactics.clear l gl
end
| TacClearBody l ->
- Proofview.Goal.raw_enter begin fun gl ->
- let hyps = interp_hyp_list ist (Tacmach.New.pf_env gl) l in
- Tactics.clear_body hyps
+ Proofview.V82.tactic begin fun gl ->
+ Tactics.clear_body (interp_hyp_list ist (pf_env gl) l) gl
end
| TacMove (dep,id1,id2) ->
Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 353d35f6a..932bfc5fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -138,6 +138,7 @@ let introduction = Tacmach.introduction
let refine = Tacmach.refine
let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
+let thin_body = Tacmach.thin_body
let convert_gen pb x y =
Proofview.Goal.raw_enter begin fun gl ->
@@ -1466,65 +1467,7 @@ let assumption =
let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
if List.is_empty ids then tclIDTAC else thin ids
-let on_the_bodies = function
-| [] -> assert false
-| [id] -> str " depends on the body of " ++ pr_id id
-| l -> str " depends on the bodies of " ++ pr_sequence pr_id l
-
-let check_is_type env ty msg =
- Proofview.tclEVARMAP >>= fun sigma ->
- let evdref = ref sigma in
- try
- let _ = Typing.sort_of env evdref ty in
- Proofview.V82.tclEVARS !evdref
- with e when Errors.noncritical e ->
- msg e
-
-let clear_body ids =
- Proofview.Goal.raw_enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
- let ctx = named_context env in
- let map (id, body, t as decl) = match body with
- | None ->
- let () = if List.mem_f Id.equal id ids then
- errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
- in
- decl
- | Some _ ->
- if List.mem_f Id.equal id ids then (id, None, t) else decl
- in
- let ctx = List.map map ctx in
- let filter = function
- | (id, None, _) -> Some (mkVar id)
- | _ -> None
- in
- let base_env = reset_context env in
- let env = push_named_context ctx base_env in
- let check_hyps =
- let check env (id, _, t as decl) =
- let msg _ = Tacticals.New.tclZEROMSG
- (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids)
- in
- check_is_type env t msg <*> Proofview.tclUNIT (push_named decl env)
- in
- let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in
- Proofview.tclIGNORE checks
- in
- let check_concl =
- let msg _ = Tacticals.New.tclZEROMSG
- (str "Conclusion" ++ on_the_bodies ids)
- in
- check_is_type env concl msg
- in
- check_hyps <*> check_concl <*>
- Proofview.Refine.refine ~unsafe:true begin fun h ->
- let args = Array.of_list (List.map_filter filter ctx) in
- let (h, c) = Proofview.Refine.new_evar h env concl in
- let c = it_mkNamedLambda_or_LetIn c ctx in
- (h, mkApp (c, args))
- end
- end
+let clear_body = thin_body
let clear_wildcards ids =
Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
@@ -2015,7 +1958,7 @@ let letin_tac_gen with_eq abs ty =
sigma, term,
Tacticals.New.tclTHEN
(intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
- (clear_body [heq;id])
+ (Proofview.V82.tactic (thin_body [heq;id]))
| None ->
(Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
Tacticals.New.tclTHEN
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 349e828a1..d7a88787b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -163,7 +163,7 @@ val unfold_constr : global_reference -> tactic
(** {6 Modification of the local context. } *)
val clear : Id.t list -> tactic
-val clear_body : Id.t list -> unit Proofview.tactic
+val clear_body : Id.t list -> tactic
val keep : Id.t list -> tactic
val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 18:08:13 +0000