Put the "cofix" tactic in the monad.

2 files changed, 57 insertions, 15 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dc018a6703..c3d6a65eb8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -472,6 +472,14 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
 
+let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
+fun env sigma p -> function
+| [] -> Sigma ([], sigma, p)
+| arg :: rem ->
+  let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in
+  let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
+  Sigma (arg :: rem, sigma, r)
+
 let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
@@ -506,15 +514,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine { run = begin fun sigma ->
-    let rec map : type r s. r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
-    fun sigma p -> function
-    | [] -> Sigma ([], sigma, p)
-    | (_, _, arg) :: rem ->
-      let Sigma (arg, sigma, q) = Evarutil.new_evar nenv sigma arg in
-      let Sigma (rem, sigma, r) = map sigma (p +> q) rem in
-      Sigma (arg :: rem, sigma, r)
-    in
-    let Sigma (evs, sigma, p) = map sigma Sigma.refl all in
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in
     let ids = List.map pi1 all in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
     let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
@@ -536,14 +536,56 @@ let fix ido n = match ido with
   | Some id ->
     mutual_fix id n [] 0
 
+let rec check_is_mutcoind env sigma cl =
+  let b = whd_betadeltaiota env sigma cl in
+  match kind_of_term b with
+  | Prod (na, c1, b) ->
+    let open Context.Rel.Declaration in
+    check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b
+  | _ ->
+    try
+      let _ = find_coinductive env sigma b in ()
+    with Not_found ->
+      error "All methods must construct elements in coinductive types."
+
 (* Refine as a cofixpoint *)
-let mutual_cofix = Tacmach.mutual_cofix
+let mutual_cofix f others j = Proofview.Goal.nf_enter { 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 firsts,lasts = List.chop j others in
+  let all = firsts @ (f, concl) :: lasts in
+  List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all;
+  let rec mk_sign sign = function
+  | [] -> sign
+  | (f, ar) :: oth ->
+    let open Context.Named.Declaration in
+    if mem_named_context f (named_context_of_val sign) then
+      error "Name already used in the environment.";
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+  in
+  let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
+  Refine.refine { run = begin fun sigma ->
+    let (ids, types) = List.split all in
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in
+    let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
+    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    let typarray = Array.of_list types in
+    let bodies = Array.of_list evs in
+    let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in
+    Sigma (oterm, sigma, p)
+  end }
+end }
 
-let cofix ido gl = match ido with
+let cofix ido = match ido with
   | None ->
-      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
+    Proofview.Goal.enter { enter = begin fun gl ->
+      let name = Pfedit.get_current_proof_name () in
+      let id = new_fresh_id [] name gl in
+      mutual_cofix id [] 0
+    end }
   | Some id ->
-      mutual_cofix id [] 0 gl
+      mutual_cofix id [] 0
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 12364d2110..f730dd6c40 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -38,8 +38,8 @@ val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t option -> int -> unit Proofview.tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
-val cofix           : Id.t option -> tactic
+val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
+val cofix           : Id.t option -> unit Proofview.tactic
 
 val convert         : constr -> constr -> unit Proofview.tactic
 val convert_leq     : constr -> constr -> unit Proofview.tactic