diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 10 | ||||
| -rw-r--r-- | tactics/declare.mli | 5 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 2 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 233 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 21 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
7 files changed, 141 insertions, 134 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 5e6f78be6f..324007930a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -187,14 +187,14 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - proof_entry_secctx = None; +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); + proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; proof_entry_opaque = opaque; - proof_entry_feedback = None; + proof_entry_feedback = feedback_id; proof_entry_inline_code = inline} let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types diff --git a/tactics/declare.mli b/tactics/declare.mli index 0068b9842a..615cffeae7 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -59,9 +59,14 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool + -> ?feedback_id:Stateid.t + -> ?section_vars:Id.Set.t -> ?types:types -> ?univs:Entries.universes_entry -> ?eff:Evd.side_effects + -> ?univsbody:Univ.ContextSet.t + (** Universe-constraints attached to the body-only, used in + vio-delayed opaque constants and private poly universes *) -> constr -> Evd.side_effects proof_entry diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index b228a04298..22d0ce5328 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -122,7 +122,7 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sig let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in let pf, status = by tac pf in let open Proof_global in - let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in match entries with | [entry] -> entry, status, uctx diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 623e6b8a42..d7dcc13e79 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -18,9 +18,9 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t + (* [name] only used in the STM *) ; entries : Evd.side_effects Declare.proof_entry list ; uctx: UState.t - ; udecl : UState.universe_decl } type opacity_flag = Opaque | Transparent @@ -118,8 +118,7 @@ let set_used_variables ps l = Environ.fold_named_context aux env ~init:(ctx,ctx_set) in if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); - (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) } + ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in @@ -141,110 +140,8 @@ let private_poly_univs = in fun () -> !b -let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now - (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in - let opaque = match opaque with Opaque -> true | Transparent -> false in - let constrain_variables ctx = - UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx - in - let fpl, univs = Future.split2 fpl in - let uctx = if poly || now then Future.force univs else initial_euctx in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst uctx) in - - let make_body = - if poly || now then - let make_body t (c, eff) = - let body = c in - let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) - in - let typ = if allow_deferred then t else nf t in - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - if allow_deferred then - let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables uctx in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body udecl in - (initunivs, typ), ((body, univs), eff) - else if poly && opaque && private_poly_univs () then - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict uctx used_univs in - let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - (udecl, typ), ((body, ubody), eff) - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict uctx used_univs in - let univs = UState.check_univ_decl ~poly ctx udecl in - (univs, typ), ((body, Univ.ContextSet.empty), eff) - in - fun t p -> Future.split2 (Future.chain p (make_body t)) - else - fun t p -> - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false uctx in - let t = nf t in - Future.from_val (univctx, t), - Future.chain p (fun (pt,eff) -> - (* Deferred proof, we already checked the universe declaration with - the initial universes, ensure that the final universes respect - the declaration as well. If the declaration is non-extensible, - this will prevent the body from adding universes and constraints. *) - let univs = Future.force univs in - let univs = constrain_variables univs in - let used_univs = Univ.LSet.union - (Vars.universes_of_constr t) - (Vars.universes_of_constr pt) - in - let univs = UState.restrict univs used_univs in - let univs = UState.check_mono_univ_decl univs udecl in - (pt,univs),eff) - in - let entry_fn p (_, t) = - let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body - in - let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; uctx; udecl } - -let return_proof ?(allow_partial=false) ps = - let { proof } = ps in - if allow_partial then begin - let proofs = Proof.partial_proof proof in - let Proof.{sigma=evd} = Proof.data proof in - let eff = Evd.eval_side_effects evd in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) - let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in - proofs, Evd.evar_universe_context evd - end else +(* XXX: This is still separate from close_proof below due to drop_pt in the STM *) +let return_proof { proof } = let Proof.{name=pid;entry} = Proof.data proof in let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in @@ -266,16 +163,122 @@ let return_proof ?(allow_partial=false) ps = code-paths that generate several proof entries are derive and equations and so far there is no code in the CI that will actually call those and do a side-effect, TTBOMK *) - let proofs = - List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in - proofs, Evd.evar_universe_context evd + (* EJGA: likely the right solution is to attach side effects to the first constant only? *) + let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in + proofs, Evd.evar_universe_context evd -let close_future_proof ~opaque ~feedback_id ps proof = - close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps +let close_proof ~opaque ~keep_body_ucst_separate ps = + let elist, uctx = return_proof ps in + let { section_vars; proof; udecl; initial_euctx } = ps in + let { Proof.name; poly; entry; sigma } = Proof.data proof in + let opaque = match opaque with Opaque -> true | Transparent -> false in + + (* Because of dependent subgoals at the beginning of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in -let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = - close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof ps)) ps + let make_entry (body, eff) (_, typ) = + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + in + (* EJGA: Why are we doing things this way? *) + let typ = EConstr.Unsafe.to_constr typ in + let typ = if allow_deferred then typ else nf typ in + (* EJGA: End "Why are we doing things this way?" *) + + let used_univs_body = Vars.universes_of_constr body in + let used_univs_typ = Vars.universes_of_constr typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let utyp, ubody = + if allow_deferred then + let utyp = UState.univ_entry ~poly initial_euctx in + let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in + (* For vi2vo compilation proofs are computed now but we need to + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let uctx_body = UState.restrict uctx used_univs in + let ubody = UState.check_mono_univ_decl uctx_body udecl in + utyp, ubody + else if poly && opaque && private_poly_univs () then + let universes = UState.restrict uctx used_univs in + let typus = UState.restrict universes used_univs_typ in + let utyp = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + utyp, ubody + else + (* Since the proof is computed now, we can simply have 1 set of + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) + let ctx = UState.restrict uctx used_univs in + let utyp = UState.check_univ_decl ~poly ctx udecl in + utyp, Univ.ContextSet.empty + in + Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body + in + let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in + { name; entries; uctx } + +let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = + let { section_vars; proof; udecl; initial_euctx } = ps in + let { Proof.name; poly; entry; sigma } = Proof.data proof in + + (* We don't allow poly = true in this path *) + if poly then + CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants."); + + let fpl, uctx = Future.split2 fpl in + (* Because of dependent subgoals at the beginning of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in + + (* We only support opaque proofs, this will be enforced by using + different entries soon *) + let opaque = true in + let make_entry p (_, types) = + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univs = UState.univ_entry ~poly:false initial_euctx in + let types = nf (EConstr.Unsafe.to_constr types) in + + Future.chain p (fun (pt,eff) -> + (* Deferred proof, we already checked the universe declaration with + the initial universes, ensure that the final universes respect + the declaration as well. If the declaration is non-extensible, + this will prevent the body from adding universes and constraints. *) + let uctx = Future.force uctx in + let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in + let used_univs = Univ.LSet.union + (Vars.universes_of_constr types) + (Vars.universes_of_constr pt) + in + let univs = UState.restrict uctx used_univs in + let univs = UState.check_mono_univ_decl univs udecl in + (pt,univs),eff) + |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types + in + let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in + { name; entries; uctx = initial_euctx } + +let close_future_proof = close_proof_delayed + +let return_partial_proof { proof } = + let proofs = Proof.partial_proof proof in + let Proof.{sigma=evd} = Proof.data proof in + let eff = Evd.eval_side_effects evd in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in + proofs, Evd.evar_universe_context evd let update_global_env = map_proof (fun p -> diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index e1c75c0649..874708ded8 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -33,8 +33,6 @@ type proof_object = (** list of the proof terms (in a form suitable for definitions). *) ; uctx: UState.t (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) } type opacity_flag = Opaque | Transparent @@ -69,7 +67,7 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -77,11 +75,13 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future. type closed_proof_output -(* If allow_partial is set (default no) then an incomplete proof - * is allowed (no error), and a warn is given if the proof is complete. *) -val return_proof : ?allow_partial:bool -> t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> proof_object +(** Requires a complete proof. *) +val return_proof : t -> closed_proof_output + +(** An incomplete proof is allowed (no error), and a warn is given if + the proof is complete. *) +val return_partial_proof : t -> closed_proof_output +val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object val get_open_goals : t -> int @@ -93,7 +93,6 @@ val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t (** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies and let-ins covered by it) + a list of - * ids to be cleared *) + * (w.r.t. type dependencies and let-ins covered by it) *) val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t + Names.Id.t list -> Constr.named_context * t diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 250c80d9a5..db09a2e69e 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -37,7 +37,7 @@ let warn_native_compute_disabled = strbrk "native_compute disabled at configure time; falling back to vm_compute.") let cbv_native env sigma c = - if Coq_config.native_compiler then + if Flags.get_native_compiler () then let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 30ca024a2f..c79aca3d3c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1223,7 +1223,7 @@ let rec intros_move = function or a term with bindings *) let tactic_infer_flags with_evar = { - Pretyping.use_typeclasses = true; + Pretyping.use_typeclasses = Pretyping.UseTC; Pretyping.solve_unification_constraints = true; Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true; |