[vernac] Cleanup on interface of Vernacentries

1 files changed, 40 insertions, 0 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f530dad4fd..283e5ff50a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -577,3 +577,43 @@ let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite =
   List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
+
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
+
+(*
+
+  HH notes in PR #679:
+
+  The Show Match could also be made more robust, for instance in the
+  presence of let in the branch of a constructor. A
+  decompose_prod_assum would probably suffice for that, but then, it
+  is a Context.Rel.Declaration.t which needs to be matched and not
+  just a pair (name,type).
+
+  Otherwise, this is OK. After all, the API on inductive types is not
+  so canonical in general, and in this simple case, working at the
+  low-level of mind_nf_lc seems reasonable (compared to working at the
+  higher-level of Inductiveops).
+
+*)
+
+let make_cases ind =
+  let open Declarations in
+  let mib, mip = Global.lookup_inductive ind in
+  Util.Array.fold_right_i
+    (fun i (ctx, _) l ->
+       let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
+       let rec rename avoid = function
+         | [] -> []
+         | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+         | RelDecl.LocalAssum (n, _)::l ->
+           let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
+           Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+       let al' = rename Id.Set.empty al in
+       let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+       (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
+    mip.mind_nf_lc []