Moving "assert" (internally "Cut") to the new proof engine.

It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".

7 files changed, 79 insertions, 89 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 3b0b6d5d23..6c571f4240 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 0621af4e80..db9e847c06 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 e59db9e427..ec4af86b9c 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 f9d9f25ccf..bdfa399aa4 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 3d2fa72c17..aac7b90ee4 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 689cc48aa2..061eca10b0 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 0ed5b524f3..4e36dec15b 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.
+