From 7a5688f6e2421a706c16e23e445d42f39a82e74b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 07:18:22 +0100 Subject: [vernac] Split `command.ml` into separate files. Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413. --- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 8 ++++---- plugins/funind/merge.ml | 6 +++--- 3 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa4353630..889c064b2 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 357755e46..158eb9646 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -406,7 +406,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +426,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +616,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff3..9fcb35f89 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) -- cgit v1.2.3 From 1172b52735a299dfc91aee36b30b576dfeff581c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 21:26:48 +0100 Subject: [flags] Make program_mode a parameter for commands in vernac. This is useful as it allows to reflect program_mode behavior as an attribute. --- API/API.mli | 5 ++++- plugins/funind/indfun.ml | 1 + plugins/ltac/rewrite.ml | 11 +++++++---- vernac/classes.ml | 8 ++++---- vernac/classes.mli | 1 + vernac/comDefinition.ml | 4 ++-- vernac/comDefinition.mli | 3 ++- vernac/obligations.ml | 1 - vernac/vernacentries.ml | 6 ++++-- 9 files changed, 25 insertions(+), 15 deletions(-) (limited to 'plugins/funind') diff --git a/API/API.mli b/API/API.mli index 838613352..ce33e9029 100644 --- a/API/API.mli +++ b/API/API.mli @@ -6052,7 +6052,9 @@ end module ComDefinition : sig - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> + val do_definition : + program_mode:bool -> + Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit end @@ -6134,6 +6136,7 @@ sig ?abstract:bool -> ?global:bool -> ?refine:bool -> + program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 158eb9646..071599d9c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -407,6 +407,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..7faf8f669 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1781,7 +1781,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/vernac/classes.ml b/vernac/classes.ml index 3d9c7defa..c2e9a5ab4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -130,7 +130,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t id let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - poly ctx (instid, bk, cl) props ?(generalize=true) + ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ((loc, instid), pl) = instid in @@ -215,7 +215,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Some (Inl fs) | Some (_, t) -> Some (Inr t) | None -> - if Flags.is_program_mode () then Some (Inl []) + if program_mode then Some (Inl []) else None in let subst, sigma = @@ -297,9 +297,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) 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 Flags.is_program_mode () || refine || Option.is_empty term then begin + 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 Flags.is_program_mode () then + 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]; diff --git a/vernac/classes.mli b/vernac/classes.mli index c0f03227c..d47c6a6f8 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -41,6 +41,7 @@ val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) + program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> Vernacexpr.typeclass_constraint -> diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index c8b289c9d..883121479 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -104,11 +104,11 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd Evd.empty; ce -let do_definition ident k univdecl bl red_option c ctypopt hook = +let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in - if Flags.is_program_mode () then + if program_mode then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Safe_typing.empty_private_constants = sideff); diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 8dcd31f25..4a65c1e91 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -14,7 +14,8 @@ open Constrexpr (** {6 Definitions/Let} *) -val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> +val do_definition : program_mode:bool -> + Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 181068089..58e4b00fc 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1185,7 +1185,6 @@ let init_program () = Coqlib.check_required_library ["Coq";"Init";"Specif"]; Coqlib.check_required_library ["Coq";"Program";"Tactics"] - let set_program_mode c = if c then if !Flags.program_mode then () diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f6e812168..f5aa15e75 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -478,6 +478,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in + let program_mode = Flags.is_program_mode () in (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) @@ -488,7 +489,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Some r -> let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) + ComDefinition.do_definition ~program_mode id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in @@ -841,7 +842,8 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri) + let program_mode = Flags.is_program_mode () in + ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) let vernac_context ~atts l = if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom -- cgit v1.2.3