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

1 files changed, 92 insertions, 43 deletions

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 =