[funind] Port invfun to the new tactic engine.

3 files changed, 112 insertions, 138 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 430fb2dee3..d625cdcc67 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -64,7 +64,7 @@ END
 TACTIC EXTEND newfuninv
 | [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
      {
-       Proofview.V82.tactic (Invfun.invfun hyp fname)
+       Invfun.invfun hyp fname
      }
 END
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1407585bff..38fdd789a3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -8,27 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Util
 open Names
 open Constr
 open EConstr
-open Pp
-open Tacticals
+open Tacmach.New
 open Tactics
-open Indfun_common
-open Tacmach
-open Tactypes
-
-let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
-
-(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
-(* let id_to_constr id = *)
-(*   try *)
-(*     Constrintern.global_reference id *)
-(*   with Not_found -> *)
-(*     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *)
+open Tacticals.New
 
+open Indfun_common
 
 (***********************************************)
 
@@ -38,38 +26,35 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
-let revert_graph kn post_tac hid g =
-    let sigma = project g in
-    let typ = pf_unsafe_type_of g (mkVar hid) in
-    match EConstr.kind sigma typ with
-      | App(i,args) when isInd sigma i ->
-          let ((kn',num) as ind'),u = destInd sigma i in
-          if MutInd.equal kn kn'
-          then (* We have generated a graph hypothesis so that we must change it if we can *)
-            let info =
-              try find_Function_of_graph ind'
-              with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-                anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
-            in
-            (* if we can find a completeness lemma for this function
-               then we can come back to the functional form. If not, we do nothing
-            *)
-            match info.completeness_lemma with
-              | None -> tclIDTAC g
-              | Some f_complete ->
-                  let f_args,res = Array.chop (Array.length args - 1) args in
-                  tclTHENLIST
-                    [
-                      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
-                      thin [hid];
-                      Proofview.V82.of_tactic (Simple.intro hid);
-                      post_tac hid
-                    ]
-                    g
-
-          else tclIDTAC g
-      | _ -> tclIDTAC g
-
+let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
+  let sigma = project gl in
+  let typ = pf_unsafe_type_of gl (mkVar hid) in
+  match EConstr.kind sigma typ with
+  | App(i,args) when isInd sigma i ->
+    let ((kn',num) as ind'),u = destInd sigma i in
+    if MutInd.equal kn kn'
+    then (* We have generated a graph hypothesis so that we must change it if we can *)
+      let info =
+        try find_Function_of_graph ind'
+        with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+          CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
+      in
+      (* if we can find a completeness lemma for this function
+         then we can come back to the functional form. If not, we do nothing
+      *)
+      match info.completeness_lemma with
+      | None -> tclIDTAC
+      | Some f_complete ->
+        let f_args,res = Array.chop (Array.length args - 1) args in
+        tclTHENLIST
+          [ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]
+          ; clear [hid]
+          ; Simple.intro hid
+          ; post_tac hid
+          ]
+    else tclIDTAC
+  | _ -> tclIDTAC
+  )
 
 (*
    [functional_inversion hid fconst f_correct ] is the functional version of [inversion]
@@ -88,102 +73,91 @@ let revert_graph kn post_tac hid g =
    \end{enumerate}
 *)
 
-let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
-  fun g ->
-    let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let sigma = project g in
-    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
-    match EConstr.kind sigma type_of_h with
-      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
-          let pre_tac,f_args,res =
-            match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
-              | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
-                  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-              |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
-                 ((fun hid -> tclIDTAC),f_args,args.(1))
-              | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
-          in
-          tclTHENLIST [
-            pre_tac hid;
-            Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
-            thin [hid];
-            Proofview.V82.of_tactic (Simple.intro hid);
-            Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
-            (fun g ->
-               let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
-               tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
-            );
-          ] g
-      | _ -> tclFAIL 1 (mt ()) g
-
-
-let error msg = user_err Pp.(str msg)
+let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
+  let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps gl) Id.Set.empty in
+  let sigma = project gl in
+  let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+  match EConstr.kind sigma type_of_h with
+  | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
+    let pre_tac,f_args,res =
+      match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
+      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
+        ((fun hid -> intros_symmetry (Locusops.onHyp hid))),f_args,args.(2)
+      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
+        ((fun hid -> tclIDTAC),f_args,args.(1))
+      | _ -> (fun hid -> tclFAIL 1 Pp.(mt ())),[||],args.(2)
+    in
+    tclTHENLIST
+      [ pre_tac hid
+      ; generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]
+      ; clear [hid]
+      ; Simple.intro hid
+      ; Inv.inv Inv.FullInversion None (Tactypes.NamedHyp hid)
+      ; Proofview.Goal.enter (fun gl ->
+            let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps gl) in
+            tclMAP (revert_graph kn pre_tac)  (hid::new_ids)
+          )
+      ]
+  | _ -> tclFAIL 1 Pp.(mt ())
+  )
 
 let invfun qhyp f  =
   let f =
     match f with
-      | GlobRef.ConstRef f -> f
-      | _ -> raise (CErrors.UserError(None,str "Not a function"))
+    | GlobRef.ConstRef f -> f
+    | _ ->
+      CErrors.user_err Pp.(str "Not a function")
   in
   try
     let finfos = find_Function_infos f in
     let f_correct = mkConst(Option.get finfos.correctness_lemma)
-    and kn = fst finfos.graph_ind
-    in
-    Proofview.V82.of_tactic (
-      Tactics.try_intros_until (fun hid -> Proofview.V82.tactic (functional_inversion kn hid (mkConst f)  f_correct)) qhyp
-    )
+    and kn = fst finfos.graph_ind in
+    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
   with
-    | Not_found ->  error "No graph found"
-    | Option.IsNone  -> error "Cannot use equivalence with graph!"
+  | Not_found -> CErrors.user_err (Pp.str "No graph found")
+  | Option.IsNone  -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
 
 exception NoFunction
 
-let invfun qhyp f g =
+let invfun qhyp f =
   match f with
-    | Some f -> invfun qhyp f g
-    | None ->
-       Proofview.V82.of_tactic begin
-        Tactics.try_intros_until
-          (fun hid -> Proofview.V82.tactic begin fun g ->
-            let sigma = project g in
-             let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
-             match EConstr.kind sigma hyp_typ with
-               | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
-                   begin
-                     let f1,_ = decompose_app sigma args.(1) in
-                     try
-                       if not (isConst sigma f1) then raise NoFunction;
-                       let finfos = find_Function_infos (fst (destConst sigma f1)) in
-                       let f_correct = mkConst(Option.get finfos.correctness_lemma)
-                       and kn = fst finfos.graph_ind
-                       in
-                       functional_inversion kn hid f1 f_correct g
-                     with | NoFunction | Option.IsNone | Not_found ->
-                       try
-                         let f2,_ = decompose_app sigma args.(2) in
-                         if not (isConst sigma f2) then raise NoFunction;
-                         let finfos = find_Function_infos (fst (destConst sigma f2)) in
-                         let f_correct = mkConst(Option.get finfos.correctness_lemma)
-                         and kn = fst finfos.graph_ind
-                         in
-                         functional_inversion kn hid  f2 f_correct g
-                       with
-                         | NoFunction ->
-                             user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
-                         | Option.IsNone  ->
-                             if do_observe ()
-                             then
-                               error "Cannot use equivalence with graph for any side of the equality"
-                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-                         | Not_found ->
-                             if do_observe ()
-                             then
-                               error "No graph found for any side of equality"
-                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-                   end
-               | _ -> user_err  (Ppconstr.pr_id hid ++ str " must be an equality ")
-          end)
-          qhyp
-          end
-          g
+  | Some f -> invfun qhyp f
+  | None ->
+    let tac_action hid gl =
+      let sigma = project gl in
+      let hyp_typ = pf_unsafe_type_of gl (mkVar hid)  in
+      match EConstr.kind sigma hyp_typ with
+      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
+        begin
+          let f1,_ = decompose_app sigma args.(1) in
+          try
+            if not (isConst sigma f1) then raise NoFunction;
+            let finfos = find_Function_infos (fst (destConst sigma f1)) in
+            let f_correct = mkConst(Option.get finfos.correctness_lemma)
+            and kn = fst finfos.graph_ind
+            in
+            functional_inversion kn hid f1 f_correct
+          with | NoFunction | Option.IsNone | Not_found ->
+          try
+            let f2,_ = decompose_app sigma args.(2) in
+            if not (isConst sigma f2) then raise NoFunction;
+            let finfos = find_Function_infos (fst (destConst sigma f2)) in
+            let f_correct = mkConst(Option.get finfos.correctness_lemma)
+            and kn = fst finfos.graph_ind
+            in
+            functional_inversion kn hid  f2 f_correct
+          with
+          | NoFunction ->
+            CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+          | Option.IsNone  ->
+            if do_observe ()
+            then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
+            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+          | Not_found ->
+            if do_observe ()
+            then CErrors.user_err (Pp.str "No graph found for any side of equality")
+            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+        end
+      | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
+    in
+    try_intros_until (tac_action %> Proofview.Goal.enter) qhyp
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 6c9baa0162..6b789e1bb2 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val invfun :
-  Tactypes.quantified_hypothesis ->
-  Names.GlobRef.t option ->
-  Evar.t Evd.sigma -> Evar.t list Evd.sigma
+val invfun
+  :  Tactypes.quantified_hypothesis
+  -> Names.GlobRef.t option
+  -> unit Proofview.tactic