From 1c82abbdec8df7cccc886db74ca1c9f596302ce1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 18 Sep 2018 20:40:51 +0200 Subject: [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. --- vernac/classes.ml | 339 ++++++++++++++++++++++++++--------------------------- vernac/classes.mli | 2 +- 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. *) -- cgit v1.2.3