Merge PR #830: Moving assert (the "Cut" rule) to new proof engine

11 files changed, 139 insertions, 113 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2afc12cd3..339c6a248 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -412,6 +412,14 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
+let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
+  let instance =
+    match filter with
+    | None -> instance
+    | Some filter -> Filter.filter_list filter instance in
+  new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a8b6b5861..14173e774 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -21,6 +21,13 @@ val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
+
+val new_evar_from_context :
+  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * EConstr.t
+
 val new_evar :
   env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
diff --git a/printing/printer.ml b/printing/printer.ml
index e9d104b49..28b10c781 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -846,15 +846,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 17128b92e..20d075ae1 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
@@ -282,6 +264,10 @@ let move_hyp_in_named_context sigma hfrom hto sign =
     split_sign hfrom hto (named_context_of_val sign) in
   move_hyp sigma toleft (left,declfrom,right) hto
 
+let insert_decl_in_named_context sigma decl hto sign =
+  let open EConstr in
+  move_hyp sigma false ([],decl,named_context_of_val sign) hto
+
 (**********************************************************************)
 
 
@@ -535,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/logic.mli b/proofs/logic.mli
index 84a21044b..9d0756b33 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -52,6 +52,8 @@ type refiner_error =
 
 exception RefinerError of refiner_error
 
+val error_no_such_hypothesis : Id.t -> 'a
+
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
@@ -59,3 +61,7 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
 
 val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
+
+val insert_decl_in_named_context : Evd.evar_map ->
+  EConstr.named_declaration -> Id.t Misctypes.move_location ->
+  Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 11f1a13e6..2ad5f607f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -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 2ed9416d1..a4d662e0a 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 40b6573a1..93bf428fd 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 062040df6..67bc55d3f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -436,19 +436,85 @@ let find_name mayrepl decl naming gl = match naming with
       id
 
 (**************************************************************)
+(*   Computing position of hypotheses for replacing           *)
+(**************************************************************)
+
+let get_next_hyp_position id =
+  let rec aux = function
+  | [] -> error_no_such_hypothesis id
+  | decl :: right ->
+    if Id.equal (NamedDecl.get_id decl) id then
+      match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst
+    else
+      aux right
+  in
+  aux
+
+let get_previous_hyp_position id =
+  let rec aux dest = function
+  | [] -> error_no_such_hypothesis id
+  | decl :: right ->
+      let hyp = NamedDecl.get_id decl in
+      if Id.equal hyp id then dest else aux (MoveAfter hyp) right
+  in
+  aux MoveLast
+
+(**************************************************************)
 (*            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 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_next_hyp_position 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 +529,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
 
@@ -999,29 +1061,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   in
   aux n []
 
-let get_next_hyp_position id gl =
-  let rec aux = function
-  | [] -> raise (RefinerError (NoSuchHyp id))
-  | decl :: right ->
-    if Id.equal (NamedDecl.get_id decl) id then
-      match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast
-    else
-      aux right
-  in
-  aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-
-let get_previous_hyp_position id gl =
-  let rec aux dest = function
-  | [] -> raise (RefinerError (NoSuchHyp id))
-  | decl :: right ->
-      let hyp = NamedDecl.get_id decl in
-      if Id.equal hyp id then dest else aux (MoveAfter hyp) right
-  in
-  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
-  let next_hyp = get_next_hyp_position id gl in
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let next_hyp = get_next_hyp_position id hyps in
   Tacticals.New.tclTHENLIST [
     clear_for_replacing [id];
     introduction id;
@@ -1040,7 +1083,8 @@ let intro_replacing id =
 let intros_possibly_replacing ids =
   let suboptimal = true in
   Proofview.Goal.enter begin fun gl ->
-    let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
 	Tacticals.New.tclTRY (clear_for_replacing [id]))
@@ -1053,7 +1097,8 @@ let intros_possibly_replacing ids =
 (* This version assumes that replacement is actually possible *)
 let intros_replacing ids =
   Proofview.Goal.enter begin fun gl ->
-    let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
     Tacticals.New.tclTHEN
       (clear_for_replacing ids)
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
@@ -2578,7 +2623,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   Proofview.Goal.enter begin fun gl ->
   let destopt =
     if with_evars then MoveLast (* evars would depend on the whole context *)
-    else get_previous_hyp_position id gl in
+    else
+      get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in
   let naming,ipat_tac =
     prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
@@ -3809,11 +3855,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
@@ -3856,16 +3903,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.
+
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 1d35f1ef6..29e373eaa 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -337,3 +337,14 @@ Goal True.
 evar (0=0).
 Abort.
 
+(* Test location of hypothesis in "symmetry in H". This was broken in
+   8.6 where H, when the oldest hyp, was moved at the place of most
+   recent hypothesis *)
+
+Goal 0=1 -> True -> True.
+intros H H0.
+symmetry in H.
+(* H should be the first hypothesis *)
+match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
+exact (eq_refl H0).
+Abort.