From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Mar 2020 05:35:41 -0400 Subject: [declare] Fuse prepare and declare for the non-interactive path. This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 5 ++- plugins/funind/gen_principle.ml | 5 ++- vernac/classes.ml | 5 ++- vernac/comAssumption.ml | 7 ++-- vernac/comDefinition.ml | 4 +-- vernac/declareDef.ml | 28 ++++++--------- vernac/declareDef.mli | 47 ++++++++++++++----------- vernac/declareObl.ml | 7 ++-- vernac/lemmas.ml | 3 +- 9 files changed, 55 insertions(+), 56 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index a2783d80e8..8c4dc0e8a6 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,7 +1,6 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - let ce = DeclareDef.prepare_definition - ~opaque ~poly sigma ~udecl ~types:tyopt ~body in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook + ~opaque ~poly ~udecl ~types:tyopt ~body sigma let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ebd280ecf6..45c46c56f4 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -290,13 +290,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in - let _ : Names.GlobRef.t = DeclareDef.declare_definition + let _ : Names.GlobRef.t = DeclareDef.declare_entry ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] - entry in + ~uctx entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) diff --git a/vernac/classes.ml b/vernac/classes.ml index 40c1a5d97d..6e929de581 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,10 +313,9 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let entry = DeclareDef.prepare_definition - ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 4a82696ea6..47ae03e0a3 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -205,9 +205,10 @@ let context_insection sigma ~poly ctx = let entry = Declare.definition_entry ~univs ~types:t b in (* XXX Fixme: Use DeclareDef.prepare_definition *) let uctx = Evd.evar_universe_context sigma in - let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in - let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry + let kind = Decls.(IsDefinition Definition) in + let _ : GlobRef.t = + DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge + ~kind ~impargs:[] ~uctx entry in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index bf4567e57f..3532d16315 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -74,10 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in let kind = Decls.IsDefinition kind in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + ~opaque:false ~poly evd ~udecl ~types ~body in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 14d3daf453..356e8f091e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -37,19 +37,8 @@ module Hook = struct end -module ClosedDef = struct - - type t = - { entry : Evd.side_effects Declare.proof_entry - ; uctx : UState.t - } - - let of_proof_entry ~uctx entry = { entry; uctx } -end - (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce = - let { ClosedDef.entry; uctx } = ce in +let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = let should_suggest = entry.Declare.proof_entry_opaque && Option.is_empty entry.Declare.proof_entry_secctx in let ubind = UState.universe_binders uctx in @@ -70,9 +59,9 @@ let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce = Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref -let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce = - let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in - try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce +let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = + let fix_exn = Declare.Internal.get_fix_exn entry in + try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry with exn -> let exn = Exninfo.capture exn in Exninfo.iraise (fix_exn exn) @@ -120,7 +109,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re let csts = CList.map2 (fun Recthm.{ name; typ; impargs } body -> let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx }) + declare_entry ~name ~scope ~kind ~impargs ~uctx entry) fixitems fixdecls in let isfix = Option.is_empty possible_indexes in @@ -167,7 +156,12 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma let univs = Evd.check_univ_decl ~poly sigma udecl in let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in - { ClosedDef.entry; uctx } + entry, uctx + +let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ?obls ~poly ?inline ~types ~body ?fix_exn sigma = + let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 8f3db59ba9..3bc1e25f19 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -39,23 +39,39 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end -module ClosedDef : sig - type t - - (* Don't use for non-interactive proofs *) - val of_proof_entry - : uctx:UState.t - -> Evd.side_effects Declare.proof_entry -> t -end +(** Declare an interactively-defined constant *) +val declare_entry + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Evd.side_effects Declare.proof_entry + -> GlobRef.t +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl -> ?hook:Hook.t -> ?obls:(Id.t * Constr.t) list - -> impargs:Impargs.manual_implicits - -> ClosedDef.t + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map -> GlobRef.t val declare_assumption @@ -97,17 +113,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -val prepare_definition - : ?opaque:bool - -> ?inline:bool - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> ClosedDef.t - val prepare_obligation : ?opaque:bool -> ?inline:bool diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 4c62582c23..bba3687256 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -371,9 +371,12 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let ce = DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in let () = progmap_remove prg in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ce + let kn = + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + kn let rec lam_index n t acc = match Constr.kind t with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ee4fc4334e..feedf4d71d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -238,8 +238,7 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - let pe = DeclareDef.ClosedDef.of_proof_entry ~uctx pe in - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs pe + DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe let declare_mutdef ~info ~uctx const = let pe = match info.Info.compute_guard with -- cgit v1.2.3