[classes] Split large `new_instance` function up.

`Classes.new_instance` is one of the largest functions of the
codebase; we split it up and reduce indentation.

This will help further cleanups. This PR should introduce no code
changes other than splitting the function up.

2 files changed, 169 insertions, 172 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index e491761aec..c738d14af9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -121,19 +121,167 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
     Evd.restrict_universe_context sigma levels
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
-  let entry = 
-    Declare.definition_entry ~types:termtype ~univs:uctx term
-  in
+  let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
-    Declare.definition_message id;
-    Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
-    instance_hook k info global imps ?hook (ConstRef kn);
-    id
+  Declare.definition_message id;
+  Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
+  instance_hook k info global imps ?hook (ConstRef kn)
+
+let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id =
+  let subst = List.fold_left2
+      (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
+      [] subst (snd k.cl_context)
+  in
+  let (_, ty_constr) = instance_constructor (k,u) subst in
+  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+  let sigma = Evd.minimize_universes sigma in
+  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+  let univs = Evd.check_univ_decl ~poly sigma decl in
+  let termtype = to_constr sigma termtype in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+      (ParameterEntry
+         (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+  in
+  Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
+  instance_hook k pri global imps ?hook (ConstRef cst); id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
-  ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true)
-  ?(tac:unit Proofview.tactic option) ?hook pri =
+let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
+  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  if program_mode then
+    let hook vis gr _ =
+      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+      Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+      let pri = intern_info pri in
+      Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
+    in
+    let obls, constr, typ =
+      match term with
+      | Some t ->
+        let obls, _, constr, typ =
+          Obligations.eterm_obligations env id sigma 0 t termtype
+        in obls, Some constr, typ
+      | None -> [||], None, termtype
+    in
+    let hook = Lemmas.mk_hook hook in
+    let ctx = Evd.evar_universe_context sigma in
+    ignore (Obligations.add_definition id ?term:constr
+              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+  else
+    Flags.silently (fun () ->
+        (* spiwack: it is hard to reorder the actions to do
+           the pretyping after the proof has opened. As a
+           consequence, we use the low-level primitives to code
+           the refinement manually.*)
+        let gls = List.rev (Evd.future_goals sigma) in
+        let sigma = Evd.reset_future_goals sigma in
+        Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+          (Lemmas.mk_hook
+             (fun _ -> instance_hook k pri global imps ?hook));
+        (* spiwack: I don't know what to do with the status here. *)
+        if not (Option.is_empty term) then
+          let init_refine =
+            Tacticals.New.tclTHENLIST [
+              Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+              Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
+              Tactics.New.reduce_after_refine;
+            ]
+          in
+          ignore (Pfedit.by init_refine)
+        else if Flags.is_auto_intros () then
+          ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+        (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
+
+let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len =
+  let props =
+    match props with
+    | Some (true, { CAst.v = CRecord fs }) ->
+      if List.length fs > List.length k.cl_props then
+        mismatched_props env' (List.map snd fs) k.cl_props;
+      Some (Inl fs)
+    | Some (_, t) -> Some (Inr t)
+    | None ->
+      if program_mode then Some (Inl [])
+      else None
+  in
+  let subst, sigma =
+    match props with
+    | None ->
+      (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
+    | Some (Inr term) ->
+      let sigma, c = interp_casted_constr_evars env' sigma term cty in
+      Some (Inr (c, subst)), sigma
+    | Some (Inl props) ->
+      let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
+      let props, rest =
+        List.fold_left
+          (fun (props, rest) decl ->
+             if is_local_assum decl then
+               try
+                 let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
+                   | Name id, {CAst.v=id'} -> Id.equal id id'
+                   | Anonymous, _ -> false
+                 in
+                 let (loc_mid, c) = List.find is_id rest in
+                 let rest' = List.filter (fun v -> not (is_id v)) rest
+                 in
+                 let {CAst.loc;v=mid} = get_id loc_mid in
+                 List.iter (fun (n, _, x) ->
+                     if Name.equal n (Name mid) then
+                       Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
+                 c :: props, rest'
+               with Not_found ->
+                 ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
+             else props, rest)
+          ([], props) k.cl_props
+      in
+      match rest with
+      | (n, _) :: _ ->
+        unbound_method env' k.cl_impl (get_id n)
+      | _ ->
+        let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
+        let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in
+        Some (Inl res), sigma
+  in
+  let term, termtype =
+    match subst with
+    | None -> let termtype = it_mkProd_or_LetIn cty ctx in
+      None, termtype
+    | Some (Inl subst) ->
+      let subst = List.fold_left2
+          (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
+          [] subst (k.cl_props @ snd k.cl_context)
+      in
+      let (app, ty_constr) = instance_constructor (k,u) subst in
+      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+      let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
+      Some term, termtype
+    | Some (Inr (def, subst)) ->
+      let termtype = it_mkProd_or_LetIn cty ctx in
+      let term = it_mkLambda_or_LetIn def ctx in
+      Some term, termtype
+  in
+  let sigma = Evarutil.nf_evar_map sigma in
+  let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
+  (* Try resolving fields that are typeclasses automatically. *)
+  let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
+  let sigma = Evarutil.nf_evar_map_undefined sigma in
+  (* Beware of this step, it is required as to minimize universes. *)
+  let sigma = Evd.minimize_universes sigma in
+  (* Check that the type is free of evars now. *)
+  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+  let termtype = to_constr sigma termtype in
+  let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
+  if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
+    declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
+  else if program_mode || refine || Option.is_empty term then
+    declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype
+  else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
+  id
+
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode
+    poly ctx (instid, bk, cl) props
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -150,9 +298,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	  cl
     | Explicit -> cl, Id.Set.empty
   in
-  let tclass = 
-    if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) 
-    else tclass 
+  let tclass =
+    if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
+    else tclass
   in
   let sigma, k, u, cty, ctx', ctx, len, imps, subst =
     let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
@@ -189,163 +337,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
   let env' = push_rel_context ctx env in
   let sigma = Evarutil.nf_evar_map sigma in
   let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
-    if abstract then
-      begin
-	let subst = List.fold_left2
-	  (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-	  [] subst (snd k.cl_context)
-	in
-	let (_, ty_constr) = instance_constructor (k,u) subst in
-        let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-        let sigma = Evd.minimize_universes sigma in
-        Pretyping.check_evars env (Evd.from_env env) sigma termtype;
-        let univs = Evd.check_univ_decl ~poly sigma decl in
-        let termtype = to_constr sigma termtype in
-        let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-          (ParameterEntry
-            (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-        in
-          Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
-          instance_hook k pri global imps ?hook (ConstRef cst); id
-      end
-    else (
-      let props =
-	match props with
-	| Some (true, { CAst.v = CRecord fs }) ->
-	    if List.length fs > List.length k.cl_props then
-	      mismatched_props env' (List.map snd fs) k.cl_props;
-	    Some (Inl fs)
-	| Some (_, t) -> Some (Inr t)
-	| None -> 
-            if program_mode then Some (Inl [])
-	    else None
-      in
-      let subst, sigma =
-	match props with
-        | None ->
-          (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
-	| Some (Inr term) ->
-            let sigma, c = interp_casted_constr_evars env' sigma term cty in
-            Some (Inr (c, subst)), sigma
-	| Some (Inl props) ->
-            let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
-	    let props, rest =
-	      List.fold_left
-		(fun (props, rest) decl ->
-		  if is_local_assum decl then
-		    try
-		      let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
-                        | Name id, {CAst.v=id'} -> Id.equal id id'
-			| Anonymous, _ -> false
-                      in
-		       let (loc_mid, c) =
-			 List.find is_id rest 
-		       in
-		       let rest' = 
-			 List.filter (fun v -> not (is_id v)) rest 
-		       in
-                       let {CAst.loc;v=mid} = get_id loc_mid in
-			 List.iter (fun (n, _, x) -> 
-				      if Name.equal n (Name mid) then
-					Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x)
-			   k.cl_projs;
-			 c :: props, rest'
-		     with Not_found ->
-                       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
-		   else props, rest)
-		([], props) k.cl_props
-	    in
-              match rest with
-              | (n, _) :: _ ->
-		unbound_method env' k.cl_impl (get_id n)
-              | _ ->
-                let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
-                let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in
-                Some (Inl res), sigma
-      in
-      let term, termtype =
-	match subst with
-	| None -> let termtype = it_mkProd_or_LetIn cty ctx in
-	    None, termtype
-	| Some (Inl subst) ->
-	  let subst = List.fold_left2
-	    (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
-	    [] subst (k.cl_props @ snd k.cl_context)
-	  in
-	  let (app, ty_constr) = instance_constructor (k,u) subst in
-	  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-          let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-	    Some term, termtype
-	| Some (Inr (def, subst)) ->
-	  let termtype = it_mkProd_or_LetIn cty ctx in
-          let term = it_mkLambda_or_LetIn def ctx in
-	    Some term, termtype
-      in
-      let sigma = Evarutil.nf_evar_map sigma in
-      let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
-      (* Try resolving fields that are typeclasses automatically. *)
-      let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
-      let sigma = Evarutil.nf_evar_map_undefined sigma in
-      (* Beware of this step, it is required as to minimize universes. *)
-      let sigma = Evd.minimize_universes sigma in
-      (* Check that the type is free of evars now. *)
-      Pretyping.check_evars env (Evd.from_env env) sigma termtype;
-      let termtype = to_constr sigma termtype in
-      let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
-        if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
-	  declare_instance_constant k pri global imps ?hook id decl
-            poly sigma (Option.get term) termtype
-        else if program_mode || refine || Option.is_empty term then begin
-	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-            if program_mode then
-	      let hook vis gr _ =
-		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-                  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-                  let pri = intern_info pri in
-		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
-	      in
-	      let obls, constr, typ =
-		match term with 
-		| Some t -> 
-		  let obls, _, constr, typ = 
-                    Obligations.eterm_obligations env id sigma 0 t termtype
-		  in obls, Some constr, typ
-		| None -> [||], None, termtype
-	      in
-              let hook = Lemmas.mk_hook hook in
-              let ctx = Evd.evar_universe_context sigma in
-		ignore (Obligations.add_definition id ?term:constr
- 			~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
-		id
-	    else
-	      (Flags.silently 
-	       (fun () ->
-                  (* spiwack: it is hard to reorder the actions to do
-                     the pretyping after the proof has opened. As a
-                     consequence, we use the low-level primitives to code
-                     the refinement manually.*)
-                let gls = List.rev (Evd.future_goals sigma) in
-                let sigma = Evd.reset_future_goals sigma in
-                Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
-		(Lemmas.mk_hook
-                  (fun _ -> instance_hook k pri global imps ?hook));
-                 (* spiwack: I don't know what to do with the status here. *)
-		if not (Option.is_empty term) then
-                  let init_refine =
-                    Tacticals.New.tclTHENLIST [
-                      Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
-                      Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
-                      Tactics.New.reduce_after_refine;
-                    ]
-                  in
-		  ignore (Pfedit.by init_refine)
-		else if Flags.is_auto_intros () then
-		  ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
-		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
-	       id)
-	end
-      else CErrors.user_err Pp.(str "Unsolved obligations remaining."))
-	
+  if abstract then
+    do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
+  else
+    do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+      cty k u ctx ctx' pri decl imps subst id props len
+
 let named_of_rel_context l =
   let open Vars in
   let acc, ctx =
@@ -433,5 +430,5 @@ let context poly l =
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus
-  in 
+  in
   List.fold_left fn true (List.rev ctx)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 9c37364cb0..bb70334342 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -37,7 +37,7 @@ val declare_instance_constant :
   Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Constr.types -> (** type *)
-  Names.Id.t
+  unit
 
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)