[funind] Port indfun to the new tactic engine.

1 files changed, 104 insertions, 106 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eeb2f246c2..2de7be4c67 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,15 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
-open Sorts
+open Pp
 open Util
+open CErrors
 open Names
+open Sorts
 open Constr
 open EConstr
-open Pp
+
+open Tacmach.New
+open Tacticals.New
+open Tactics
+
 open Indfun_common
-open Tactypes
 
 module RelDecl = Context.Rel.Declaration
 
@@ -37,111 +41,105 @@ let choose_dest_or_ind scheme_info args =
   Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
 
 let functional_induction with_clean c princl pat =
-  let res =
-    fun g ->
-    let sigma = Tacmach.project g in
+  let open Proofview.Notations in
+  Proofview.Goal.enter_one (fun gl ->
+    let sigma = project gl in
     let f,args = decompose_app sigma c in
-    let princ,bindings, princ_type,g' =
-      match princl with
-      | None -> (* No principle is given let's find the good one *)
-         begin
-           match EConstr.kind sigma f with
-           | Const (c',u) ->
-              let princ_option =
-                let finfo = (* we first try to find out a graph on f *)
-                  try find_Function_infos c'
-                  with Not_found ->
-                    user_err  (str "Cannot find induction information on "++
-                                       Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
-                in
-                match Tacticals.elimination_sort_of_goal g with
-                | InSProp -> finfo.sprop_lemma
-                | InProp -> finfo.prop_lemma
-                | InSet -> finfo.rec_lemma
-                | InType -> finfo.rect_lemma
+    match princl with
+    | None -> (* No principle is given let's find the good one *)
+      begin
+        match EConstr.kind sigma f with
+        | Const (c',u) ->
+          let princ_option =
+            let finfo = (* we first try to find out a graph on f *)
+              try find_Function_infos c'
+              with Not_found ->
+                user_err  (str "Cannot find induction information on "++
+                           Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
+            in
+            match elimination_sort_of_goal gl with
+            | InSProp -> finfo.sprop_lemma
+            | InProp -> finfo.prop_lemma
+            | InSet -> finfo.rec_lemma
+            | InType -> finfo.rect_lemma
+          in
+          let princ =  (* then we get the principle *)
+            match princ_option with
+            | Some princ ->
+              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
+              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+              Proofview.tclUNIT princ
+            | None ->
+              (*i If there is not default lemma defined then,
+                      we cross our finger and try to find a lemma named f_ind
+                      (or f_rec, f_rect) i*)
+              let princ_name =
+                Indrec.make_elimination_ident
+                  (Label.to_id (Constant.label c'))
+                  (elimination_sort_of_goal gl)
               in
-              let princ,g' =  (* then we get the principle *)
+              let princ_ref =
                 try
-                  let g',princ =
-                    Tacmach.pf_eapply (Evd.fresh_global) g  (GlobRef.ConstRef (Option.get princ_option )) in
-                  princ,g'
-                with Option.IsNone ->
-                  (*i If there is not default lemma defined then,
-                          we cross our finger and try to find a lemma named f_ind
-                          (or f_rec, f_rect) i*)
-                  let princ_name =
-                    Indrec.make_elimination_ident
-                      (Label.to_id (Constant.label c'))
-                      (Tacticals.elimination_sort_of_goal g)
-                  in
-                  try
-                    let princ_ref = const_of_id princ_name in
-                    let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in
-                    (b,a)
-                    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
-                  with Not_found -> (* This one is neither defined ! *)
-                    user_err  (str "Cannot find induction principle for "
-                                     ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
+                  Constrintern.locate_reference (Libnames.qualid_of_ident princ_name)
+                with
+                | Not_found ->
+                  user_err (str "Cannot find induction principle for "
+                            ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
               in
-              (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
-           | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
-         end
-      | Some ((princ,binding)) ->
-         princ,binding,Tacmach.pf_unsafe_type_of g princ,g
-    in
-    let sigma = Tacmach.project g' in
-    let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
-    let args_as_induction_constr =
-      let c_list =
-        if princ_infos.Tactics.farg_in_concl
-        then [c] else []
-      in
-      if List.length args + List.length c_list = 0
-      then user_err Pp.(str "Cannot recognize a valid functional scheme" );
-      let encoded_pat_as_patlist =
-        List.make (List.length args + List.length c_list - 1) None @ [pat]
-      in
-      List.map2
-        (fun c pat ->
-          ((None,
-            Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
-           (None,pat),
-           None))
-        (args@c_list)
-        encoded_pat_as_patlist
-    in
-    let princ' = Some (princ,bindings) in
-    let princ_vars =
-      List.fold_right
-        (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
-        args
-        Id.Set.empty
+              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
+              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+              Proofview.tclUNIT princ
+          in
+          princ >>= fun princ ->
+          (* We need to refresh gl due to the updated evar_map in princ *)
+          Proofview.Goal.enter_one (fun gl ->
+          Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+        | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
+      end
+    | Some ((princ,binding)) ->
+      Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+    ) >>= fun (princ, bindings, princ_type, args) ->
+  Proofview.Goal.enter (fun gl ->
+  let sigma = project gl in
+  let princ_infos = compute_elim_sig (project gl) princ_type in
+  let args_as_induction_constr =
+    let c_list =
+      if princ_infos.Tactics.farg_in_concl
+      then [c] else []
     in
-    let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in
-    let old_idl = Id.Set.diff old_idl princ_vars in
-    let subst_and_reduce g =
-      if with_clean
-      then
-        let idl =
-          List.filter (fun id -> not (Id.Set.mem id old_idl))
-            (Tacmach.pf_ids_of_hyps g)
-        in
-        let flag =
-          Genredexpr.Cbv
-            {Redops.all_flags
-             with Genredexpr.rDelta = false;
-            }
-        in
-        Tacticals.tclTHEN
-          (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
-          (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
-          g
-      else Tacticals.tclIDTAC g
+    if List.length args + List.length c_list = 0
+    then user_err Pp.(str "Cannot recognize a valid functional scheme" );
+    let encoded_pat_as_patlist =
+      List.make (List.length args + List.length c_list - 1) None @ [pat]
     in
-    Tacticals.tclTHEN
-      (Proofview.V82.of_tactic (choose_dest_or_ind
-         princ_infos
-         (args_as_induction_constr,princ')))
-      subst_and_reduce
-      g'
-  in res
+    List.map2
+      (fun c pat ->
+         ((None, ElimOnConstr (fun env sigma -> (sigma,(c,Tactypes.NoBindings)))),
+          (None,pat), None))
+      (args@c_list)
+      encoded_pat_as_patlist
+  in
+  let princ' = Some (princ,bindings) in
+  let princ_vars =
+    List.fold_right
+      (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
+      args
+      Id.Set.empty
+  in
+  let old_idl = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
+  let old_idl = Id.Set.diff old_idl princ_vars in
+  let subst_and_reduce gl =
+    if with_clean
+    then
+      let idl = List.filter (fun id -> not (Id.Set.mem id old_idl))(pf_ids_of_hyps gl) in
+      let flag = Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false } in
+      tclTHEN
+        (tclMAP (fun id -> tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl)
+        (reduce flag Locusops.allHypsAndConcl)
+    else tclIDTAC
+  in
+  tclTHEN
+    (choose_dest_or_ind
+       princ_infos
+       (args_as_induction_constr,princ'))
+    (Proofview.Goal.enter subst_and_reduce))