From 1f121ebf2990dc25899f2f3eb138eddd147483cf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 May 2020 02:42:38 +0200 Subject: [declare] Refactor constant information into a record. This improves the interface, and allows even more sealing of the API. This is yet work in progress. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 4 +- plugins/ltac/rewrite.ml | 3 +- vernac/classes.ml | 11 +- vernac/comDefinition.ml | 4 +- vernac/comDefinition.mli | 2 +- vernac/comFixpoint.ml | 5 +- vernac/comProgramFixpoint.ml | 4 +- vernac/declare.ml | 139 ++++++++++++------------ vernac/declare.mli | 78 +++++++------ vernac/obligations.ml | 41 +++---- vernac/obligations.mli | 4 +- vernac/vernacentries.ml | 1 + 12 files changed, 156 insertions(+), 140 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index e9e866c5fb..5431a21b53 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -2,5 +2,5 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl - ~opaque:false ~poly ~types:None ~body sigma + let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in + Declare.declare_definition ~name ~info ~types:None ~body sigma diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 914dc96648..67d09acfda 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1902,8 +1902,9 @@ let declare_projection name instance_id r = let types = Some (it_mkProd_or_LetIn typ ctx) in let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in + let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in let _r : GlobRef.t = - Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma + Declare.declare_definition ~name ~info ~types ~body sigma in () let build_morphism_signature env sigma m = diff --git a/vernac/classes.ml b/vernac/classes.ml index f7d8a4b42f..c4c6a0fa33 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -311,12 +311,12 @@ let instance_hook info global ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = +let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let scope = Declare.Global Declare.ImportDefaultBehavior in - let kn = Declare.declare_definition ~name ~kind ~scope ~impargs - ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - instance_hook info global ?hook kn + let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in + let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in + instance_hook iinfo global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 @@ -344,7 +344,8 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in + let scope, kind = Declare.Global Declare.ImportDefaultBehavior, + Decls.IsDefinition Decls.Instance in let _ : Declare.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index a791e67bb1..c89de88e95 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -116,9 +116,9 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let kind = Decls.IsDefinition kind in + let info = Declare.CInfo.make ~scope ~kind ?hook ~opaque:false ~impargs ~udecl ~poly () in let _ : Names.GlobRef.t = - Declare.declare_definition ~name ~scope ~kind ?hook ~impargs - ~opaque:false ~poly evd ~udecl ~types ~body + Declare.declare_definition ~name ~info ~types ~body evd in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 2e8fe16252..2b846f17e0 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -32,7 +32,7 @@ val do_definition_program -> name:Id.t -> scope:Declare.locality -> poly:bool - -> kind:Decls.definition_object_kind + -> kind:Decls.logical_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 5bf3350777..925a2d8389 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -283,9 +283,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in + let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in let _ : GlobRef.t list = - Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration + Declare.declare_mutually_recursive ~info ~uctx + ~possible_indexes:indexes ~ntns ~rec_declaration fixitems in () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4aa46e0a86..e51a786cb0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint - | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.(IsDefinition Fixpoint) + | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint) in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind diff --git a/vernac/declare.ml b/vernac/declare.ml index ebea919f64..5c5e03fd89 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1037,6 +1037,26 @@ let declare_universe_context = DeclareUctx.declare_universe_context type locality = Locality.locality = | Discharge | Global of import_status +module CInfo = struct + + type t = + { poly : bool + ; opaque : bool + ; inline : bool + ; kind : Decls.logical_kind + ; udecl : UState.universe_decl + ; scope : locality + ; impargs : Impargs.manual_implicits + ; hook : Hook.t option + } + + let make ?(poly=false) ?(opaque=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition)) + ?(udecl=UState.default_univ_decl) ?(scope=Global ImportNeedQualified) ?(impargs=[]) + ?hook () = + { poly; opaque; inline; kind; udecl; scope; impargs; hook } + +end + (* Locality stuff *) let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = let should_suggest = @@ -1077,7 +1097,8 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = let vars = Vars.universes_of_constr (List.hd fixdecls) in vars, fixdecls, None -let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = +let declare_mutually_recursive_core ~info ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = + let { CInfo.poly; udecl; opaque; scope; kind; _ } = info in let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in let uctx, univs = @@ -1127,20 +1148,21 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = (* Preparing proof entries *) -let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = +let prepare_definition ~info ~types ~body sigma = + let { CInfo.poly; udecl; opaque; inline; _ } = info in let env = Global.env () in Pretyping.check_evars_are_solved ~program_mode:false env sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ?opaque ?inline ?types ~univs body in + let entry = definition_entry ~opaque ~inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx -let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ~obls ~poly ?inline ~types ~body sigma = - let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in +let declare_definition_core ~name ~info ~obls ~types ~body sigma = + let entry, uctx = prepare_definition ~info ~types ~body sigma in + let { CInfo.scope; kind; impargs; hook; _ } = info in declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry let declare_definition = declare_definition_core ~obls:[] @@ -1196,37 +1218,32 @@ type obligations = {obls : Obligation.t array; remaining : int} type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint module ProgramDecl = struct + type t = { prg_name : Id.t + ; prg_info : CInfo.t ; prg_body : constr ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl + ; prg_uctx : UState.t ; prg_obligations : obligations ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : locality - ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : Hook.t option - ; prg_opaque : bool } + } open Obligation - let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b - t deps fixkind notations obls reduce = - let obls', b = - match b with + let make prg_name ~info ~ntns ~reduce ~deps ~uctx ~types ~body fixkind obls = + let obls', body = + match body with | None -> assert (Int.equal (Array.length obls) 0); - let n = Nameops.add_suffix n "_obligation" in + let n = Nameops.add_suffix prg_name "_obligation" in ( [| { obl_name = n ; obl_body = None ; obl_location = Loc.tag Evar_kinds.InternalHole - ; obl_type = t + ; obl_type = types ; obl_status = (false, Evar_kinds.Expand) ; obl_deps = Int.Set.empty ; obl_tac = None } |] @@ -1244,25 +1261,23 @@ module ProgramDecl = struct obls , b ) in - let ctx = UState.make_flexible_nonalgebraic uctx in - { prg_name = n - ; prg_body = b - ; prg_type = reduce t - ; prg_ctx = ctx - ; prg_univdecl = udecl + let prg_uctx = UState.make_flexible_nonalgebraic uctx in + { prg_name + ; prg_info = info + ; prg_body = body + ; prg_type = reduce types + ; prg_uctx ; prg_obligations = {obls = obls'; remaining = Array.length obls'} ; prg_deps = deps ; prg_fixkind = fixkind - ; prg_notations = notations - ; prg_implicits = impargs - ; prg_poly = poly - ; prg_scope = scope - ; prg_kind = kind - ; prg_reduce = reduce - ; prg_hook = hook - ; prg_opaque = opaque } - - let set_uctx ~uctx prg = {prg with prg_ctx = uctx} + ; prg_notations = ntns + ; prg_reduce = reduce } + + module Internal = struct + let get_uctx prg = prg.prg_uctx + let get_poly prg = prg.prg_info.CInfo.poly + let set_uctx ~uctx prg = {prg with prg_uctx = uctx} + end end open Obligation @@ -1349,14 +1364,15 @@ let get_hide_obligations = ~value:false let declare_obligation prg obl ~uctx ~types ~body = - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let poly = prg.prg_info.CInfo.poly in + let univs = UState.univ_entry ~poly uctx in let body = prg.prg_reduce body in let types = Option.map prg.prg_reduce types in match obl.obl_status with | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) | force, Evar_kinds.Define opaque -> let opaque = (not force) && opaque in - let poly = prg.prg_poly in + let poly = prg.prg_info.CInfo.poly in let ctx, body, ty, args = if not poly then shrink_body body types else ([], body, types, [||]) @@ -1562,25 +1578,13 @@ let subst_prog subst prg = let declare_definition prg = let varsubst = obligation_substitution true prg in - let sigma = Evd.from_ctx prg.prg_ctx in + let sigma = Evd.from_ctx prg.prg_uctx in let body, types = subst_prog varsubst prg in let body, types = EConstr.(of_constr body, Some (of_constr types)) in - (* All these should be grouped into a struct a some point *) - let opaque, poly, udecl, hook = - (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook) - in - let name, scope, kind, impargs = - ( prg.prg_name - , prg.prg_scope - , Decls.(IsDefinition prg.prg_kind) - , prg.prg_implicits ) - in + let name, info = prg.prg_name, prg.prg_info in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let kn = - declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls - ~opaque ~poly ~udecl ~types ~body sigma - in + let kn = declare_definition_core ~name ~info ~obls ~types ~body sigma in let pm = progmap_remove !State.prg_ref prg in State.prg_ref := pm; kn @@ -1611,7 +1615,7 @@ let declare_mutual_definition l = let oblsubst = obligation_substitution true x in let subs, typ = subst_prog oblsubst x in let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in + let sigma = Evd.from_ctx x.prg_uctx in let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) @@ -1621,7 +1625,7 @@ let declare_mutual_definition l = in let term = EConstr.to_constr sigma term in let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_info.CInfo.impargs) in let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in (def, oblsubst) in @@ -1654,24 +1658,22 @@ let declare_mutual_definition l = | IsCoFixpoint -> None in (* In the future we will pack all this in a proper record *) - let poly, scope, ntns, opaque = - (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque) - in - let kind = + (* XXX: info refactoring *) + let _kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in + let scope = first.prg_info.CInfo.scope in (* Declare the recursive definitions *) - let udecl = UState.default_univ_decl in let kns = - declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns - ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations + ~uctx:first.prg_uctx ~rec_declaration ~possible_indexes ~restrict_ucontext:false fixitems in (* Only for the first constant *) let dref = List.hd kns in Hook.( - call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref}); + call ?hook:first.prg_info.CInfo.hook {S.uctx = first.prg_uctx; obls; scope; dref}); let pm = List.fold_left progmap_remove !State.prg_ref l in State.prg_ref := pm; dref @@ -1711,7 +1713,7 @@ let dependencies obls n = let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = let obls = Array.copy obls in let () = obls.(num) <- obl in - let prg = {prg with prg_ctx = uctx} in + let prg = {prg with prg_uctx = uctx} in let _progress = update_obls prg obls (pred rem) in let () = if pred rem > 0 then @@ -1746,14 +1748,15 @@ let obligation_terminator entries uctx {name; num; auto} = | (_, status), false -> status in let obl = {obl with obl_status = (false, status)} in - let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in + let poly = prg.prg_info.CInfo.poly in + let uctx = if poly then uctx else UState.union prg.prg_uctx uctx in let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in let prg_ctx = - if prg.prg_poly then + if poly then (* Polymorphic *) (* We merge the new universes and constraints of the polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx uctx + UState.union prg.prg_uctx uctx else if (* The first obligation, if defined, declares the univs of the constant, @@ -1790,7 +1793,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref = | _ -> () in let inst, ctx' = - if not prg.prg_poly (* Not polymorphic *) then + if not prg.prg_info.CInfo.poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) let ctx = UState.from_env (Global.env ()) in diff --git a/vernac/declare.mli b/vernac/declare.mli index 55c6175371..30db26e693 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -354,6 +354,28 @@ val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit type locality = Locality.locality = Discharge | Global of import_status +(** Information for a constant *) +module CInfo : sig + + type t + + val make : + ?poly:bool + -> ?opaque : bool + -> ?inline : bool + -> ?kind : Decls.logical_kind + (** Theorem, etc... *) + -> ?udecl : UState.universe_decl + -> ?scope : locality + (** locality *) + -> ?impargs : Impargs.manual_implicits + -> ?hook : Hook.t + (** Callback to be executed after saving the constant *) + -> unit + -> t + +end + (** XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead *) @@ -375,14 +397,7 @@ val declare_entry 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 - -> poly:bool - -> ?inline:bool + -> info:CInfo.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map @@ -398,13 +413,9 @@ val declare_assumption -> GlobRef.t val declare_mutually_recursive - : opaque:bool - -> scope:locality - -> kind:Decls.logical_kind - -> poly:bool - -> uctx:UState.t - -> udecl:UState.universe_decl + : info:CInfo.t -> ntns:Vernacexpr.decl_notation list + -> uctx:UState.t -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option -> Recthm.t list @@ -453,42 +464,37 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint module ProgramDecl : sig type t = private { prg_name : Id.t + ; prg_info : CInfo.t ; prg_body : constr ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl + ; prg_uctx : UState.t ; prg_obligations : obligations ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : locality - ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : Hook.t option - ; prg_opaque : bool } + } val make : - ?opaque:bool - -> ?hook:Hook.t - -> Names.Id.t - -> udecl:UState.universe_decl + Names.Id.t + -> info:CInfo.t + -> ntns:Vernacexpr.decl_notation list + -> reduce:(Constr.constr -> Constr.constr) + -> deps:Names.Id.t list -> uctx:UState.t - -> impargs:Impargs.manual_implicits - -> poly:bool - -> scope:locality - -> kind:Decls.definition_object_kind - -> Constr.constr option - -> Constr.types - -> Names.Id.t list + -> types:Constr.types + -> body:Constr.constr option -> fixpoint_kind option - -> Vernacexpr.decl_notation list -> RetrieveObl.obligation_info - -> (Constr.constr -> Constr.constr) -> t - val set_uctx : uctx:UState.t -> t -> t + (* This is internal, only here as obligations get merged into the + regular declaration path *) + module Internal : sig + val get_poly : t -> bool + val get_uctx : t -> UState.t + val set_uctx : uctx:UState.t -> t -> t + end end (** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 62fdbf50ad..83ea6c21f0 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -95,7 +95,7 @@ let warn_solve_errored = ; fnl () ; str "This will become an error in the future" ]) -let solve_by_tac ?loc name evi t poly uctx = +let solve_by_tac ?loc name evi t ~poly ~uctx = (* the status is dropped. *) try let env = Global.env () in @@ -137,7 +137,7 @@ let rec solve_obligation prg num tac = let obl = subst_deps_obl obls obl in let scope = Declare.(Global Declare.ImportNeedQualified) in let kind = kind_of_obligation (snd obl.obl_status) in - let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.from_ctx prg.prg_uctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = @@ -145,7 +145,7 @@ let rec solve_obligation prg num tac = {Declare.name = prg.prg_name; num; auto} in let info = Declare.Info.make ~proof_ending ~scope ~kind () in - let poly = prg.prg_poly in + let poly = Internal.get_poly prg in let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~udecl:UState.default_univ_decl ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Declare.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in @@ -177,21 +177,20 @@ and solve_obligation_by_tac prg obls i tac = | Some t -> t | None -> !default_tactic in - let evd = Evd.from_ctx prg.prg_ctx in - let evd = Evd.update_sigma_env evd (Global.env ()) in - match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac - prg.prg_poly (Evd.evar_universe_context evd) with + let uctx = Internal.get_uctx prg in + let uctx = UState.update_sigma_env uctx (Global.env ()) in + let poly = Internal.get_poly prg in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with | None -> None | Some (t, ty, uctx) -> - let prg = ProgramDecl.set_uctx ~uctx prg in - (* Why is uctx not used above? *) + let prg = ProgramDecl.Internal.set_uctx ~uctx prg in let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in obls.(i) <- obl'; - if def && not prg.prg_poly then ( + if def && not poly then ( (* Declare the term constraints with the first obligation only *) let uctx_global = UState.from_env (Global.env ()) in let uctx = UState.merge_subst uctx_global (UState.subst uctx) in - Some (ProgramDecl.set_uctx ~uctx prg)) + Some (ProgramDecl.Internal.set_uctx ~uctx prg)) else Some prg else None @@ -313,9 +312,12 @@ let msg_generating_obl name obls = let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) ?(impargs = []) ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior) - ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook + ?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook ?(opaque = false) obls = - let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in + let prg = + let info = Declare.CInfo.make ~poly ~opaque ~udecl ~impargs ~scope ~kind ?hook () in + ProgramDecl.make name ~info ~body:term ~types:t ~uctx ~reduce ~ntns:[] ~deps:[] None obls + in let {obls;_} = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose (msg_generating_obl name) obls; @@ -333,16 +335,16 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl) ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior) - ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false) + ?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false) notations fixkind = let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in let pm = List.fold_left (fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) -> + let info = Declare.CInfo.make ~impargs ~poly ~scope ~kind ~opaque ~udecl ?hook () in let prg = - ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps - (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce - ?hook + ProgramDecl.make name ~info ~body:(Some b) ~types:typ ~uctx ~deps + (Some fixkind) ~ntns:notations obls ~reduce in State.add name prg) () l @@ -371,9 +373,10 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = UState.univ_entry ~poly:false prg.prg_ctx in + let uctx = Internal.get_uctx prg in + let univs = UState.univ_entry ~poly:false uctx in let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified - (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural) + (Declare.ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural) in Declare.assumption_message x.obl_name; obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f0a8e9bea1..76e2f5cb2c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -78,7 +78,7 @@ val add_definition : -> ?impargs:Impargs.manual_implicits -> poly:bool -> ?scope:Declare.locality - -> ?kind:Decls.definition_object_kind + -> ?kind:Decls.logical_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> ?hook:Declare.Hook.t @@ -97,7 +97,7 @@ val add_mutual_definitions : -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:Declare.locality - -> ?kind:Decls.definition_object_kind + -> ?kind:Decls.logical_kind -> ?reduce:(constr -> constr) -> ?hook:Declare.Hook.t -> ?opaque:bool diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1ada477d07..f7da2000e3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -577,6 +577,7 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in if program_mode then + let kind = Decls.IsDefinition kind in ComDefinition.do_definition_program ~name:name.v ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook else -- cgit v1.2.3