Reimplementing the clearbody tactic.

3 files changed, 63 insertions, 4 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 16e7851802..12a8c4ae96 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1928,8 +1928,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         if b then Tactics.keep l gl else Tactics.clear l gl
       end
   | TacClearBody l ->
-      Proofview.V82.tactic begin fun gl ->
-        Tactics.clear_body (interp_hyp_list ist (pf_env gl) l) gl
+      Proofview.Goal.raw_enter begin fun gl ->
+        let hyps = interp_hyp_list ist (Tacmach.New.pf_env gl) l in
+        Tactics.clear_body hyps
       end
   | TacMove (dep,id1,id2) ->
       Proofview.V82.tactic begin fun gl -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 932bfc5fe7..c7eb811832 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1467,7 +1467,65 @@ let assumption =
 let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
   if List.is_empty ids then tclIDTAC else thin ids
 
-let clear_body = thin_body
+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_wildcards ids =
   Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d7a88787b1..349e828a19 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 -> tactic
+val clear_body    : Id.t list -> unit Proofview.tactic
 val keep          : Id.t list -> tactic
 val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic