diff options
81 files changed, 525 insertions, 358 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7800dff01..53316a2cb 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -28,7 +28,7 @@ let check_constant_declaration env kn cb = (* let env = add_constraints cb.const_constraints env in*) (match cb.const_type with ty -> - let env' = add_constraints (Future.force cb.const_constraints) env in + let env' = add_constraints cb.const_constraints env in (*MS: FIXME*) let _ = infer_type env' ty in (match body_of_constant cb with | Some bd -> diff --git a/dev/include b/dev/include index a8c4e1d49..4a025d077 100644 --- a/dev/include +++ b/dev/include @@ -35,6 +35,7 @@ #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; #install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverse;; #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ec7716356..c35d04e9d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -179,7 +179,7 @@ let pppftreestate p = pp(print_pftreestate p) let ppuni u = pp(pr_uni u) let ppuni_level u = pp (Level.pr u) -let ppuniverses u = pp (str"[" ++ Universe.pr u ++ str"]") +let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]") let ppuniverse_set l = pp (LSet.pr l) let ppuniverse_instance l = pp (Instance.pr l) @@ -195,6 +195,7 @@ let ppuniverseconstraints c = pp (UniverseConstraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx +let ppuniverses u = pp (Univ.pr_universes u) let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9ce6ec779..1331fd968 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -91,13 +91,13 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** Main interpretation functions expecting evars to be all resolved *) val interp_constr : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> constr Univ.in_universe_context_set + constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types -> constr Univ.in_universe_context_set + constr_expr -> types -> constr Evd.in_evar_universe_context val interp_type : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types Univ.in_universe_context_set + constr_expr -> types Evd.in_evar_universe_context (** Main interpretation function expecting evars to be all resolved *) @@ -142,7 +142,8 @@ val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) -val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types Univ.in_universe_context_set +val interp_binder : evar_map -> env -> Name.t -> constr_expr -> + types Evd.in_evar_universe_context val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 4363ec442..55868097f 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -47,12 +47,14 @@ let constraints_of_constant cb = Univ.Constraint.union (match cb.const_body with | Undef _ -> Univ.empty_constraint | Def c -> Univ.empty_constraint - | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o)) + | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o)) let universes_of_constant cb = match cb.const_body with | Undef _ | Def _ -> cb.const_universes - | OpaqueDef o -> Opaqueproof.force_constraints o + | OpaqueDef o -> + Univ.UContext.union cb.const_universes + (Univ.ContextSet.to_context (Opaqueproof.force_constraints o)) let universes_of_polymorphic_constant cb = if cb.const_polymorphic then universes_of_constant cb diff --git a/kernel/entries.mli b/kernel/entries.mli index 001a1e4b3..07c18d5e3 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,7 +50,7 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr * Declareops.side_effects +type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects type const_entry_body = proof_output Future.computation type projection = mutual_inductive * int * int * types diff --git a/kernel/environ.ml b/kernel/environ.ml index dd4237b22..7a90f3675 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -311,17 +311,21 @@ let evaluable_constant kn env = | OpaqueDef _ -> false | Undef _ -> false -let template_polymorphic_constant (cst,u) env = - if not (Univ.Instance.is_empty u) then false - else - match (lookup_constant cst env).const_type with - | TemplateArity _ -> true - | RegularArity _ -> false +let polymorphic_constant cst env = + (lookup_constant cst env).const_polymorphic -let polymorphic_constant (cst,u) env = +let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false - else - (lookup_constant cst env).const_polymorphic + else polymorphic_constant cst env + +let template_polymorphic_constant cst env = + match (lookup_constant cst env).const_type with + | TemplateArity _ -> true + | RegularArity _ -> false + +let template_polymorphic_pconstant (cst,u) env = + if not (Univ.Instance.is_empty u) then false + else template_polymorphic_constant cst env let lookup_projection cst env = match (lookup_constant cst env).const_proj with @@ -336,17 +340,21 @@ let is_projection cst env = (* Mutual Inductives *) let lookup_mind = lookup_mind -let template_polymorphic_ind ((mind,i),u) env = - if not (Univ.Instance.is_empty u) then false - else - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity _ -> true - | RegularArity _ -> false +let polymorphic_ind (mind,i) env = + (lookup_mind mind env).mind_polymorphic -let polymorphic_ind ((mind,i),u) env = +let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false - else - (lookup_mind mind env).mind_polymorphic + else polymorphic_ind ind env + +let template_polymorphic_ind (mind,i) env = + match (lookup_mind mind env).mind_packets.(i).mind_arity with + | TemplateArity _ -> true + | RegularArity _ -> false + +let template_polymorphic_pind (ind,u) env = + if not (Univ.Instance.is_empty u) then false + else template_polymorphic_ind ind env let add_mind_key kn mind_key env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in diff --git a/kernel/environ.mli b/kernel/environ.mli index 28eecc7ef..61a4f7327 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -128,10 +128,12 @@ val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool (** New-style polymorphism *) -val polymorphic_constant : pconstant -> env -> bool +val polymorphic_constant : constant -> env -> bool +val polymorphic_pconstant : pconstant -> env -> bool (** Old-style polymorphism *) -val template_polymorphic_constant : pconstant -> env -> bool +val template_polymorphic_constant : constant -> env -> bool +val template_polymorphic_pconstant : pconstant -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if @@ -173,10 +175,12 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env val lookup_mind : mutual_inductive -> env -> mutual_inductive_body (** New-style polymorphism *) -val polymorphic_ind : pinductive -> env -> bool +val polymorphic_ind : inductive -> env -> bool +val polymorphic_pind : pinductive -> env -> bool (** Old-style polymorphism *) -val template_polymorphic_ind : pinductive -> env -> bool +val template_polymorphic_ind : inductive -> env -> bool +val template_polymorphic_pind : pinductive -> env -> bool (** {5 Modules } *) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index bb5695885..6d48aaa4e 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -384,11 +384,11 @@ let rec execute env cstr = let argst = execute_array env args in let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_ind ind env -> + | Ind ind when Environ.template_polymorphic_pind ind env -> (* Template sort-polymorphism of inductive types *) let args = Array.map (fun t -> lazy t) argst in judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_constant cst env -> + | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Template sort-polymorphism of constants *) let args = Array.map (fun t -> lazy t) argst in judge_of_constant_knowing_parameters env cst args diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 73fdaa81f..0f9c7421f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -193,6 +193,34 @@ let cumulate_arity_large_levels env sign = let is_impredicative env u = is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet) +let param_ccls params = + let has_some_univ u = function + | Some v when Universe.equal u v -> true + | _ -> false + in + let remove_some_univ u = function + | Some v when Universe.equal u v -> None + | x -> x + in + let fold l (_, b, p) = match b with + | None -> + (* Parameter contributes to polymorphism only if explicit Type *) + let c = strip_prod_assum p in + (* Add Type levels to the ordered list of parameters contributing to *) + (* polymorphism unless there is aliasing (i.e. non distinct levels) *) + begin match kind_of_term c with + | Sort (Type u) -> + if List.exists (has_some_univ u) l then + None :: List.map (remove_some_univ u) l + else + Some u :: l + | _ -> + None :: l + end + | _ -> l + in + List.fold_left fold [] params + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -215,7 +243,7 @@ let typecheck_inductive env ctx mie = List.fold_left (fun (env_ar,l) ind -> (* Arities (without params) are typed-checked here *) - let arity = + let arity, expltype = if isArity ind.mind_entry_arity then let (ctx,s) = destArity ind.mind_entry_arity in match s with @@ -226,11 +254,12 @@ let typecheck_inductive env ctx mie = let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in let (cctx, _) = destArity proparity.utj_val in (* Any universe is well-formed, we don't need to check [s] here *) - mkArity (cctx, s) - | _ -> let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val + mkArity (cctx, s), not (Sorts.is_small s) + | _ -> + let arity = infer_type env_params ind.mind_entry_arity in + arity.utj_val, not (Sorts.is_small s) else let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val + arity.utj_val, false in let (sign, deflev) = dest_arity env_params arity in let inflev = @@ -249,7 +278,7 @@ let typecheck_inductive env ctx mie = let env_ar' = push_rel (Name id, None, full_arity) env_ar in (* (add_constraints cst2 env_ar) in *) - (env_ar', (id,full_arity,sign @ params,deflev,inflev)::l)) + (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l)) (env',[]) mie.mind_entry_inds in @@ -277,30 +306,60 @@ let typecheck_inductive env ctx mie = (* Compute/check the sorts of the inductive types *) let inds = - Array.map (fun ((id,full_arity,sign,def_level,inf_level),cn,lc,(is_unit,clev)) -> - let defu = Term.univ_of_sort def_level in - let infu = - (** Inferred level, with parameters and constructors. *) - match inf_level with - | Some alev -> Universe.sup clev alev - | None -> clev + Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev)) -> + let full_polymorphic () = + let defu = Term.univ_of_sort def_level in + let infu = + (** Inferred level, with parameters and constructors. *) + match inf_level with + | Some alev -> Universe.sup clev alev + | None -> clev + in + let is_natural = + check_leq (universes env') infu defu && + not (is_type0m_univ defu && not is_unit) + in + let _ = + (** Impredicative sort, always allow *) + if is_impredicative env defu then () + else (** Predicative case: the inferred level must be lower or equal to the + declared level. *) + if not is_natural then + anomaly ~label:"check_inductive" + (Pp.str"Incorrect universe " ++ + Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " + ++ Universe.pr infu) + in + RegularArity (not is_natural,full_arity,defu) in - let is_natural = - check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit) + let template_polymorphic () = + let sign, s = + try dest_arity env full_arity + with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) + in + match s with + | Type u when expltype (* Explicitly polymorphic *) -> + (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *) + (* The polymorphic level is a function of the level of the *) + (* conclusions of the parameters *) + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + let b = check_leq (universes env') clev u in + if not b then + anomaly ~label:"check_inductive" + (Pp.str"Incorrect universe " ++ + Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " + ++ Universe.pr clev) + else + TemplateArity (param_ccls params, clev) + | _ (* Not an explicit occurrence of Type *) -> + full_polymorphic () in - let _ = - (** Impredicative sort, always allow *) - if is_impredicative env defu then () - else (** Predicative case: the inferred level must be lower or equal to the - declared level. *) - if not is_natural then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu) + let arity = + if mie.mind_entry_polymorphic then full_polymorphic () + else template_polymorphic () in - (id,cn,lc,(sign,RegularArity (not is_natural,full_arity,defu)))) + (id,cn,lc,(sign,arity))) inds in (env_arities, params, inds) @@ -617,7 +676,7 @@ let allowed_sorts is_smashed s = let arity_conclusion = function | RegularArity (_, c, _) -> c - | TemplateArity s -> mkType s.template_level + | TemplateArity (_, s) -> mkType s let fold_inductive_blocks f = Array.fold_left (fun acc (_,_,lc,(arsign,ar)) -> @@ -681,7 +740,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re (* Elimination sorts *) let arkind,kelim = match ar_kind with - | TemplateArity ar -> TemplateArity ar, all_sorts + | TemplateArity (paramlevs, lev) -> + let ar = {template_param_levels = paramlevs; template_level = lev} in + TemplateArity ar, all_sorts | RegularArity (info,ar,defs) -> let s = sort_of_univ defs in let kelim = allowed_sorts info s in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 73d5c5db2..7aed4bf50 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; abstract : Context.named_context in_universe_context } -type proofterm = (constr * Univ.universe_context) Future.computation +type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) | Direct of cooking_info list * proofterm @@ -99,7 +99,7 @@ let force_constraints = function | NoIndirect(_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> match !get_univ dp i with - | None -> Univ.UContext.empty + | None -> Univ.ContextSet.empty | Some u -> Future.force u let get_constraints = function diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index fee15e405..3e45f65b4 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -19,7 +19,7 @@ open Mod_subst When it is [turn_indirect] the data is relocated to an opaque table and the [opaque] is turned into an index. *) -type proofterm = (constr * Univ.universe_context) Future.computation +type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque (** From a [proofterm] to some [opaque]. *) @@ -31,9 +31,9 @@ val turn_indirect : opaque -> opaque (** From a [opaque] back to a [constr]. This might use the indirect opaque accessor configured below. *) val force_proof : opaque -> constr -val force_constraints : opaque -> Univ.universe_context +val force_constraints : opaque -> Univ.universe_context_set val get_proof : opaque -> Term.constr Future.computation -val get_constraints : opaque -> Univ.universe_context Future.computation option +val get_constraints : opaque -> Univ.universe_context_set Future.computation option val subst_opaque : substitution -> opaque -> opaque val iter_direct_opaque : (constr -> unit) -> opaque -> opaque @@ -66,7 +66,7 @@ val set_indirect_creator : val set_indirect_opaque_accessor : (DirPath.t -> int -> Term.constr Future.computation) -> unit val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.universe_context Future.computation option) -> unit + (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit val reset_indirect_creator : unit -> unit diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index deabf1bcf..960fb1f45 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -200,6 +200,9 @@ let add_constraints cst senv = env = Environ.add_constraints cst senv.env; univ = Univ.Constraint.union cst senv.univ } +let add_constraints_list cst senv = + List.fold_right add_constraints cst senv + let push_context_set ctx = add_constraints (Now (Univ.ContextSet.constraints ctx)) let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx)) @@ -298,11 +301,12 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = let c,typ,univs = Term_typing.translate_local_def senv.env id de in - let c, univs = match c with - | Def c -> Mod_subst.force_constr c, univs - | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o - | _ -> assert false in let senv' = push_context univs senv in + let c, senv' = match c with + | Def c -> Mod_subst.force_constr c, senv' + | OpaqueDef o -> Opaqueproof.force_proof o, + push_context_set (Opaqueproof.force_constraints o) senv' + | _ -> assert false in let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} @@ -330,30 +334,32 @@ let labels_of_mib mib = let globalize_constant_universes cb = if cb.const_polymorphic then - Now Univ.Constraint.empty + [Now Univ.Constraint.empty] else - match cb.const_body with - | (Undef _ | Def _) -> Now (Univ.UContext.constraints cb.const_universes) - | OpaqueDef lc -> - match Opaqueproof.get_constraints lc with - | None -> Now (Univ.UContext.constraints cb.const_universes) - | Some fc -> - match Future.peek_val fc with - | None -> Later (Future.chain ~pure:true fc Univ.UContext.constraints) - | Some c -> Now (Univ.UContext.constraints c) + let cstrs = Univ.UContext.constraints cb.const_universes in + Now cstrs :: + (match cb.const_body with + | (Undef _ | Def _) -> [] + | OpaqueDef lc -> + match Opaqueproof.get_constraints lc with + | None -> [] + | Some fc -> + match Future.peek_val fc with + | None -> [Later (Future.chain ~pure:true fc Univ.ContextSet.constraints)] + | Some c -> [Now (Univ.ContextSet.constraints c)]) let globalize_mind_universes mb = if mb.mind_polymorphic then - Now Univ.Constraint.empty + [Now Univ.Constraint.empty] else - Now (Univ.UContext.constraints mb.mind_universes) + [Now (Univ.UContext.constraints mb.mind_universes)] let constraints_of_sfb sfb = match sfb with | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib - | SFBmodtype mtb -> Now mtb.typ_constraints - | SFBmodule mb -> Now mb.mod_constraints + | SFBmodtype mtb -> [Now mtb.typ_constraints] + | SFBmodule mb -> [Now mb.mod_constraints] (* let add_constraints cst senv = *) (* { senv with *) @@ -384,7 +390,7 @@ let add_field ((l,sfb) as field) gn senv = check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty) in let cst = constraints_of_sfb sfb in - let senv = add_constraints cst senv in + let senv = add_constraints_list cst senv in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env @@ -757,7 +763,7 @@ let import lib cst vodigest senv = let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.add_constraints mb.mod_constraints senv.env in - let env = Environ.push_context cst env in + let env = Environ.push_context_set cst env in (mp, lib.comp_natsymbs), { senv with env = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5b5457c38..429597f90 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -140,7 +140,7 @@ val export : module_path * compiled_library * native_library (* Constraints are non empty iff the file is a vi2vo *) -val import : compiled_library -> Univ.universe_context -> vodigest -> +val import : compiled_library -> Univ.universe_context_set -> vodigest -> (module_path * Nativecode.symbol array) safe_transformer (** {6 Safe typing judgments } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 780c14a20..0959fa703 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -57,6 +57,8 @@ let local_constrain_type env j = function (* Insertion of constants and parameters in environment. *) +let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff + let handle_side_effects env body side_eff = let handle_sideff t se = let cbl = match se with @@ -127,13 +129,14 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) -> + Future.chain ~greedy:true ~pure:true body (fun ((body, ctx), side_eff) -> let body = handle_side_effects env body side_eff in - let j = infer env body in + let env' = push_context_set ctx env in + let j = infer env' body in let j = hcons_j j in - let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in + let _typ = constrain_type env' j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in feedback_completion_typecheck feedback_id; - j.uj_val, Univ.UContext.empty) in + j.uj_val, ctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, @@ -142,7 +145,8 @@ let infer_declaration env kn dcl = let env = push_context c.const_entry_universes env in let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in - let body, side_eff = Future.join body in + let (body, ctx), side_eff = Future.join body in + let env = push_context_set ctx env in let body = handle_side_effects env body side_eff in let def, typ, proj = match c.const_entry_proj with @@ -168,9 +172,12 @@ let infer_declaration env kn dcl = let def = Def (Mod_subst.from_val j.uj_val) in def, typ, None in + let univs = Univ.UContext.union c.const_entry_universes + (Univ.ContextSet.to_context ctx) + in feedback_completion_typecheck feedback_id; def, typ, proj, c.const_entry_polymorphic, - c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx + univs, c.const_entry_inline_code, c.const_entry_secctx let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -281,6 +288,6 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true - ce.const_entry_body (fun (body, side_eff) -> - handle_side_effects env body side_eff, Declareops.no_seff); + ce.const_entry_body (fun ((body, ctx), side_eff) -> + (handle_side_effects env body side_eff, ctx), Declareops.no_seff); } diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index a2a35492e..8be1c76e0 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,6 +18,8 @@ val translate_local_def : env -> Id.t -> definition_entry -> val translate_local_assum : env -> types -> types +val mk_pure_proof : constr -> proof_output + (* returns the same definition_entry but with side effects turned into * let-ins or beta redexes. it is meant to get a term out of a not yet * type checked proof *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1a7d96b55..c6355b3ea 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -427,11 +427,11 @@ let rec execute env cstr = let jl = execute_array env args in let j = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_ind ind env -> + | Ind ind when Environ.template_polymorphic_pind ind env -> (* Sort-polymorphism of inductive types *) let args = Array.map (fun j -> lazy j.uj_type) jl in judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_constant cst env -> + | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Sort-polymorphism of constant *) let args = Array.map (fun j -> lazy j.uj_type) jl in judge_of_constant_knowing_parameters env cst args diff --git a/kernel/univ.ml b/kernel/univ.ml index 3d66b01cf..d931626e4 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -680,7 +680,10 @@ struct external node : node -> data = "%identity" let hash = ExprHash.hash let uid = hash - let equal x y = x == y + let equal x y = x == y || + (let (u,n) = x and (v,n') = y in + Int.equal n n' && Level.equal u v) + let stats _ = () let init _ = () end @@ -716,9 +719,9 @@ struct | (l, 0) -> Level.is_small l | _ -> false - (* let equal (u,n) (v,n') = *) - (* Int.equal n n' && Level.equal u v *) - let equal x y = x == y + let equal x y = x == y || + (let (u,n) = x and (v,n') = y in + Int.equal n n' && Level.equal u v) let leq (u,n) (v,n') = let cmp = Level.compare u v in @@ -1244,18 +1247,6 @@ let check_eq_univs g l1 l2 = Huniv.for_all (fun x1 -> exists x1 l2) l1 && Huniv.for_all (fun x2 -> exists x2 l1) l2 - (* let exists x1 l = Huniv.exists_remove (fun x2 -> f x1 x2) l in *) - (* try *) - (* let l2' = *) - (* Huniv.fold (fun x1 acc -> *) - (* let l2' = exists x1 l2 in *) - (* if l2 == l2' then raise Neq *) - (* else l2') l1 l2 *) - (* in *) - (* if Huniv.is_nil l2' then true *) - (* else false (\* l2' has universes that are not equal to any in l1 *\) *) - (* with Neq -> false *) - (** [check_eq] is also used in [Evd.set_eq_sort], hence [Evarconv] and [Unification]. In this case, it seems that the Atom/Max case may occur, @@ -1561,6 +1552,8 @@ module UniverseConstraints = struct include S let add (l,d,r as cst) s = + if (Option.is_empty (Universe.level r)) then + prerr_endline "Algebraic universe on the right"; if Universe.equal l r then s else add cst s @@ -2345,7 +2338,9 @@ let remove_large_constraint u v min = let is_direct_constraint u v = match Universe.level v with | Some u' -> Level.equal u u' - | None -> Huniv.mem (Universe.Expr.make u) v + | None -> + let expr = Universe.Expr.make u in + Universe.exists (Universe.Expr.equal expr) v (* Solve a system of universe constraint of the form @@ -2388,9 +2383,9 @@ let solve_constraints_system levels level_bounds level_min = let subst_large_constraint u u' v = match level u with | Some u -> - if is_direct_constraint u v then + (* if is_direct_constraint u v then *) Universe.sup u' (remove_large_constraint u v type0m_univ) - else v + (* else v *) | _ -> anomaly (Pp.str "expect a universe level") @@ -2477,7 +2472,7 @@ let hcons_universe_set = let hcons_universe_context_set (v, c) = (hcons_universe_set v, hcons_constraints c) -let hcons_univ x = x (* Universe.hcons (Huniv.node x) *) +let hcons_univ x = Universe.hcons (Huniv.node x) let explain_universe_inconsistency (o,u,v,p) = let pr_rel = function diff --git a/kernel/univ.mli b/kernel/univ.mli index ea3ab16a5..20ee554f1 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -433,6 +433,8 @@ val check_constraints : constraints -> universes -> bool val solve_constraints_system : universe option array -> universe array -> universe array -> universe array +val remove_large_constraint : universe_level -> universe -> universe -> universe + val subst_large_constraint : universe -> universe -> universe -> universe val subst_large_constraints : diff --git a/library/declare.ml b/library/declare.ml index 97445755f..e92225637 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -126,7 +126,7 @@ let open_constant i ((sp,kn), obj) = | (Def _ | Undef _) -> () | OpaqueDef lc -> match Opaqueproof.get_constraints lc with - | Some f when Future.is_val f -> Global.push_context (Future.force f) + | Some f when Future.is_val f -> Global.push_context_set (Future.force f) | _ -> () let exists_name id = @@ -196,7 +196,7 @@ let declare_constant_common id cst = let definition_entry ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = - { const_entry_body = Future.from_val (body,eff); + { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; const_entry_proj = None; @@ -216,8 +216,9 @@ let declare_sideff se = let id_of c = Names.Label.to_id (Names.Constant.label c) in let pt_opaque_of cb = match cb with - | { const_body = Def sc } -> Mod_subst.force_constr sc, false - | { const_body = OpaqueDef fc } -> Opaqueproof.force_proof fc, true + | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false + | { const_body = OpaqueDef fc } -> + (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true | { const_body = Undef _ } -> anomaly(str"Undefined side effect") in let ty_of cb = diff --git a/library/declaremods.mli b/library/declaremods.mli index a25247891..c5dc5a7f5 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -73,7 +73,7 @@ type library_objects val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.universe_context -> unit + Univ.universe_context_set -> unit val get_library_symbols_tbl : library_name -> Nativecode.symbol array diff --git a/library/global.ml b/library/global.ml index 74a2a1c0e..6c088e542 100644 --- a/library/global.ml +++ b/library/global.ml @@ -189,18 +189,38 @@ let type_of_global_in_context env r = let inst = Univ.UContext.instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs +let universes_of_global env r = + let open Declarations in + match r with + | VarRef id -> Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + Declareops.universes_of_constant cb + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + mib.mind_universes + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + mib.mind_universes + +let universes_of_global gr = + universes_of_global (env ()) gr + let is_polymorphic r = let env = env() in match r with | VarRef id -> false - | ConstRef c -> - let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic - | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in - mib.Declarations.mind_polymorphic - | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - mib.Declarations.mind_polymorphic + | ConstRef c -> Environ.polymorphic_constant c env + | IndRef ind -> Environ.polymorphic_ind ind env + | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env + +let is_template_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.template_polymorphic_constant c env + | IndRef ind -> Environ.template_polymorphic_ind ind env + | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) diff --git a/library/global.mli b/library/global.mli index 5995ff03f..de19e888c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -94,7 +94,7 @@ val start_library : DirPath.t -> module_path val export : DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : - Safe_typing.compiled_library -> Univ.universe_context -> Safe_typing.vodigest -> + Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> module_path * Nativecode.symbol array (** {6 Misc } *) @@ -107,11 +107,15 @@ val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : unit -> unit val is_polymorphic : Globnames.global_reference -> bool +val is_template_polymorphic : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val universes_of_global : Globnames.global_reference -> Univ.universe_context + (** {6 Retroknowledge } *) val register : diff --git a/library/library.ml b/library/library.ml index dc712ce02..d48f3b525 100644 --- a/library/library.ml +++ b/library/library.ml @@ -39,7 +39,7 @@ type library_t = { library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_imports : compilation_unit_name array; library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.universe_context; + library_extra_univs : Univ.universe_context_set; } module LibraryOrdered = DirPath @@ -329,7 +329,7 @@ type 'a table_status = let opaque_tables = ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t) let univ_tables = - ref (LibraryMap.empty : (Univ.universe_context table_status) LibraryMap.t) + ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -362,7 +362,7 @@ let access_univ_table dp i = module OpaqueTables = struct let a_constr = Future.from_val (Term.mkRel 1) - let a_univ = Future.from_val Univ.UContext.empty + let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : Opaqueproof.cooking_info list = [] let local_opaque_table = ref (Array.make 100 a_constr) @@ -440,7 +440,7 @@ let () = type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.universe_context Future.computation array * Univ.universe_context * bool + Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array @@ -466,13 +466,13 @@ let intern_from_file f = add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); let open Safe_typing in match univs with - | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty + | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> add_univ_table lmd.md_name (Fetched utab); mk_library lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty + mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -731,7 +731,7 @@ let save_library_to ?todo dir f = | Some d -> assert(!Flags.compilation_mode = Flags.BuildVi); f ^ "i", (fun x -> Some (d x)), - (fun x -> Some (x,Univ.UContext.empty,false)), (fun x -> Some x) in + (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in Opaqueproof.reset_indirect_creator (); let cenv, seg, ast = Declaremods.end_library dir in let opaque_table, univ_table, disch_table, f2t_map = diff --git a/library/library.mli b/library/library.mli index fc043aab6..0f6f510d8 100644 --- a/library/library.mli +++ b/library/library.mli @@ -31,7 +31,7 @@ val require_library_from_file : (** Segments of a library *) type seg_lib type seg_univ = (* cst, all_cst, finished? *) - Univ.universe_context Future.computation array * Univ.universe_context * bool + Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array diff --git a/library/universes.ml b/library/universes.ml index 138a248f0..5996d7a80 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -594,13 +594,12 @@ let normalize_context_set ctx us algs = let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) global cstrs + Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + cstrs in - (** Should this really happen? *) - let subst' = LSet.fold (fun f -> LMap.add f canon) - (LSet.union rigid flexible) LMap.empty + let subst = LSet.fold (fun f -> LMap.add f canon) + flexible subst in - let subst = LMap.union subst' subst in (subst, cstrs)) (LMap.empty, Constraint.empty) partition in diff --git a/library/universes.mli b/library/universes.mli index ab217e872..3b951997a 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -149,6 +149,9 @@ val constr_of_global : Globnames.global_reference -> constr anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context +(** Returns the type of the global reference, by creating a fresh instance of polymorphic + references and computing their instantiated universe context. (side-effect on the + universe counter, use with care). *) val type_of_global : Globnames.global_reference -> types in_universe_context_set (** Full universes substitutions into terms *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 783abc5d8..b85b7995c 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -395,7 +395,7 @@ let discriminate_tac (cstr,u as cstru) p = let neweq=new_app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_tac (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt exact_check)]) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) end (* wrap everything *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8a9c7d2e7..a8876c75b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -554,7 +554,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in - let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*) + let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = List.map (* we can now compute the other principles *) @@ -597,7 +597,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis in {const with Entries.const_entry_body = - (Future.from_val (princ_body,Declareops.no_seff)); + (Future.from_val (Term_typing.mk_pure_proof princ_body)); Entries.const_entry_type = Some scheme_type } ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b68d9762e..072b1ce00 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.of_list (List.map (fun entry -> - (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type ) + (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type ) ) (make_scheme (Array.map_to_list (fun const -> const,GType None) funs)) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8496bbbb3..439014361 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1376,7 +1376,7 @@ let com_terminate start_proof ctx tclIDTAC tclIDTAC; try let sigma, new_goal_type = build_new_goal_type () in - open_new_goal start_proof (Evd.get_universe_context_set sigma) + open_new_goal start_proof (Evd.universe_context_set sigma) using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 689462704..3fa9e02cf 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -210,10 +210,15 @@ let rec mk_nat = function (* Lists *) -let mkListConst c u = - Term.mkConstructU (Globnames.destConstructRef - (Coqlib.gen_reference "" ["Init";"Datatypes"] c), - Univ.Instance.of_array [|u|]) +let mkListConst c = + let r = + Coqlib.gen_reference "" ["Init";"Datatypes"] c + in + let inst = + if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] + else fun _ -> Univ.Instance.empty + in + fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u) let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index de308c296..85fd81026 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -113,28 +113,6 @@ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef. Proof. generalize (CRmorph.(morph_eq) c c'). destruct (c =? c')%coef; auto. -<<<<<<< HEAD -======= -||||||| merged common ancestors -destruct (c ?= c')%coef; auto. -======= -destruct (c ?= c')%coef; auto. -<<<<<<< HEAD -======= -intros. -generalize (fun h => X (morph_eq CRmorph _ _ h)). -case (ceqb c1 c2); auto. ->>>>>>> .merge_file_U4r9lJ ->>>>>>> This commit adds full universe polymorphism and fast projections to Coq. -||||||| merged common ancestors -======= -intros. -generalize (fun h => X (morph_eq CRmorph _ _ h)). -case (ceqb c1 c2); auto. ->>>>>>> .merge_file_U4r9lJ -======= ->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with ->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with Qed. (* Power coefficients : Cpow *) @@ -301,24 +279,6 @@ apply radd_ext. [ ring | now rewrite rdiv_simpl ]. Qed. -<<<<<<< HEAD -Theorem rdiv3 r1 r2 r3 r4 : - ~ r2 == 0 -> - ~ r4 == 0 -> - r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). -Proof. -intros H2 H4. -assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). -transitivity (r1 / r2 + - (r3 / r4)); auto. -transitivity (r1 / r2 + - r3 / r4); auto. -transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)). -apply rdiv2; auto. -f_equiv. -transitivity (r1 * r4 + - (r3 * r2)); auto. -Qed. - -======= ->>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with Theorem rdiv5 a b : - (a / b) == - a / b. Proof. now rewrite !rdiv_def, ropp_mul_l. diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 52e37e611..7fa11a918 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -273,6 +273,7 @@ type evar_universe_context = can be instantiated with algebraic universes as they appear in types and universe instances only. *) uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) + uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) } let empty_evar_universe_context = @@ -280,11 +281,13 @@ let empty_evar_universe_context = uctx_postponed = Univ.UniverseConstraints.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; - uctx_universes = Univ.initial_universes } + uctx_universes = Univ.initial_universes; + uctx_initial_universes = Univ.initial_universes } let evar_universe_context_from e c = - {empty_evar_universe_context with - uctx_local = c; uctx_universes = universes e} + let u = universes e in + {empty_evar_universe_context with + uctx_local = c; uctx_universes = u; uctx_initial_universes = u} let is_empty_evar_universe_context ctx = Univ.ContextSet.is_empty ctx.uctx_local && @@ -305,11 +308,12 @@ let union_evar_universe_context ctx ctx' = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; + uctx_initial_universes = ctx.uctx_initial_universes; uctx_universes = if local == ctx.uctx_local then ctx.uctx_universes else let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - Univ.merge_constraints cstrsr ctx.uctx_universes} + Univ.merge_constraints cstrsr ctx.uctx_universes } (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) (* let union_evar_universe_context = *) @@ -325,7 +329,8 @@ let diff_evar_universe_context ctx' ctx = Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables; uctx_univ_algebraic = Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic; - uctx_universes = Univ.empty_universes } + uctx_universes = Univ.empty_universes; + uctx_initial_universes = ctx.uctx_initial_universes } (* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *) (* let diff_evar_universe_context = *) @@ -334,6 +339,7 @@ let diff_evar_universe_context ctx' ctx = type 'a in_evar_universe_context = 'a * evar_universe_context let evar_universe_context_set ctx = ctx.uctx_local +let evar_universe_context_constraints ctx = snd ctx.uctx_local let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } let evar_universe_context_subst ctx = ctx.uctx_univ_variables @@ -916,7 +922,7 @@ let univ_flexible_alg = UnivFlexible true let evar_universe_context d = d.universes -let get_universe_context_set d = d.universes.uctx_local +let universe_context_set d = d.universes.uctx_local let universes evd = evd.universes.uctx_universes @@ -1148,7 +1154,7 @@ let normalize_evar_universe_context_variables uctx = in let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in (* let univs = subst_univs_universes subst uctx.uctx_universes in *) - let ctx_local', univs = Universes.refresh_constraints (Global.universes ()) ctx_local in + let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in subst, { uctx with uctx_local = ctx_local'; uctx_univ_variables = normalized_variables; uctx_universes = univs } @@ -1191,7 +1197,8 @@ let refresh_undefined_univ_variables uctx = let uctx' = {uctx_local = ctx'; uctx_postponed = Univ.UniverseConstraints.empty;(*FIXME*) uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = Univ.initial_universes} in + uctx_universes = Univ.initial_universes; + uctx_initial_universes = uctx.uctx_initial_universes } in uctx', subst let refresh_undefined_universes evd = @@ -1218,7 +1225,7 @@ let normalize_evar_universe_context uctx = if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then uctx else - let us', universes = Universes.refresh_constraints (Global.universes ()) us' in + let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in (* let universes = subst_univs_opt_universes vars' uctx.uctx_universes in *) let postponed = Univ.subst_univs_universe_constraints (Universes.make_opt_subst vars') @@ -1229,7 +1236,8 @@ let normalize_evar_universe_context uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_postponed = postponed; - uctx_universes = universes} + uctx_universes = universes; + uctx_initial_universes = uctx.uctx_initial_universes } in fixpoint uctx' in fixpoint uctx @@ -1254,6 +1262,7 @@ let nf_constraints = else nf_constraints let universes evd = evd.universes.uctx_universes +let constraints evd = evd.universes.uctx_universes (* Conversion w.r.t. an evar map and its local universes. *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 020f0a7b4..9be18bc8a 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -415,6 +415,7 @@ type evar_universe_context type 'a in_evar_universe_context = 'a * evar_universe_context val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set +val evar_universe_context_constraints : evar_universe_context -> Univ.constraints val evar_context_universe_context : evar_universe_context -> Univ.universe_context val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context val empty_evar_universe_context : evar_universe_context @@ -427,6 +428,7 @@ val universes : evar_map -> Univ.universes val add_constraints_context : evar_universe_context -> Univ.constraints -> evar_universe_context + val normalize_evar_universe_context_variables : evar_universe_context -> Univ.universe_subst in_evar_universe_context @@ -458,7 +460,7 @@ val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context -val get_universe_context_set : evar_map -> Univ.universe_context_set +val universe_context_set : evar_map -> Univ.universe_context_set val universe_context : evar_map -> Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> Univ.universes diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3f14de282..18b96e765 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -875,7 +875,7 @@ let understand_judgment_tcc evdref env c = let ise_pretype_gen_ctx flags sigma env lvar kind c = let evd, c = ise_pretype_gen flags sigma env lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in - f c, Evd.get_universe_context_set evd + f c, Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 79b051845..72e9971d6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -81,7 +81,7 @@ val understand_ltac : inference_flags -> (** Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - evar_map -> env -> glob_constr -> constr Univ.in_universe_context_set + evar_map -> env -> glob_constr -> constr Evd.in_evar_universe_context (** Idem but returns the judgment of the understood term *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 676fc4f3a..b64156649 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -815,6 +815,9 @@ let local_whd_state_gen flags sigma = whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (n,m,p) :: s') -> whrec (Stack.nth args (n+m), s') + |args, (Stack.Fix (f,s',cst)::s'') -> + let x' = Stack.zip(x,args) in + whrec (contract_fix f cst, s' @ (Stack.append_app [|x'|] s'')) |_ -> s else s diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 27c1d252d..d728f1bff 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -870,8 +870,8 @@ let isGlobalRef c = let is_template_polymorphic env f = match kind_of_term f with - | Ind ind -> Environ.template_polymorphic_ind ind env - | Const c -> Environ.template_polymorphic_constant c env + | Ind ind -> Environ.template_polymorphic_pind ind env + | Const c -> Environ.template_polymorphic_pconstant c env | _ -> false let base_sort_cmp pb s0 s1 = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 6ef3d11da..8b4d02e04 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -194,7 +194,7 @@ val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> Reduction.conv_pb -> constr -> constr -> bool val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool -val eq_constr : constr -> constr -> bool +val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 339ca19fb..5cd05c58d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -207,12 +207,12 @@ let rec execute env evdref cstr = let jl = execute_array env evdref args in let j = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_ind ind env -> + | Ind ind when Environ.template_polymorphic_pind ind env -> (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind (Evarutil.jv_nf_evar !evdref jl)) - | Const cst when Environ.template_polymorphic_constant cst env -> + | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3bb3aa9ba..9e662150e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -603,7 +603,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag expand curenvnb pb b wt substn cM f1 l1 cN f2 l2 and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN = - if not (subterm_restriction b flags) && use_full_betaiota flags then + if use_full_betaiota flags && not (subterm_restriction b flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (eq_constr cM cM') then unirec_rec curenvnb pb b wt substn cM' cN diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e36019887..7c386da8e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -72,7 +72,9 @@ let print_ref reduce ref = let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ in it_mkProd_or_LetIn ccl ctx else typ in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) + let univs = Global.universes_of_global ref in + hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ + Printer.pr_universe_ctx univs) (********************************) (** Printing implicit arguments *) @@ -193,7 +195,17 @@ let print_opacity ref = (*******************) (* *) +let print_polymorphism ref = + let poly = Global.is_polymorphic ref in + let template_poly = Global.is_template_polymorphic ref in + pr_global ref ++ str " is " ++ str + (if poly then "universe polymorphic" + else if template_poly then + "template universe polymorphic" + else "monomorphic") + let print_name_infos ref = + let poly = print_polymorphism ref in let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = @@ -205,6 +217,7 @@ let print_name_infos ref = print_ref true ref; blankline] else [] in + poly :: type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ diff --git a/proofs/logic.ml b/proofs/logic.ml index 47645d295..8b4865594 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -340,6 +340,15 @@ let check_conv_leq_goal env sigma arg ty conclty = else raise (RefinerError (BadType (arg,ty,conclty))) else sigma +exception Stop of constr list +let meta_free_prefix a = + try + let _ = Array.fold_left (fun acc a -> + if occur_meta a then raise (Stop acc) + else a :: acc) [] a + in a + with Stop acc -> Array.rev_of_list acc + let goal_type_of env sigma c = if !check then type_of env sigma c else Retyping.get_type_of env sigma c @@ -442,10 +451,10 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if isInd f || isConst f - && not (Array.exists occur_meta l) (* we could be finer *) + if is_template_polymorphic env f then - (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) + let l' = meta_free_prefix l in + (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 22262036e..eeb577025 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -160,7 +160,8 @@ let solve_by_implicit_tactic env sigma evk = (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try - let (ans, _, _) = build_by_tactic env (evi.evar_concl, Evd.get_universe_context_set sigma) tac in - ans + let (ans, _, _) = + build_by_tactic env (evi.evar_concl, Evd.universe_context_set sigma) tac in + fst ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 3efc644e0..e3df619f8 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -152,7 +152,7 @@ val build_constant_by_tactic : types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst val build_by_tactic : env -> ?poly:polymorphic -> types Univ.in_universe_context_set -> unit Proofview.tactic -> - constr * bool * Universes.universe_opt_subst + constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst (** Declare the default tactic to fill implicit arguments *) @@ -162,4 +162,5 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) +(* FIXME: interface: it may incur some new universes etc... *) val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9be159640..12700851a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -265,7 +265,7 @@ let get_open_goals () = List.length shelf let nf_body nf b = - let aux (c, t) = (nf c, t) in + let aux ((c, ctx), t) = ((nf c, ctx), t) in Future.chain ~pure:true b aux let close_proof ?feedback_id ~now fpl = @@ -333,12 +333,13 @@ let return_proof () = let eff = Evd.eval_side_effects evd in let evd = Evd.nf_constraints evd in let subst = Evd.universe_subst evd in - let ctx = Evd.universe_context evd in + let ctx = Evd.universe_context_set 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, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in - proofs, (subst, ctx) + let proofs = + List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, ctx), eff)) initial_goals in + proofs, (subst, Univ.ContextSet.to_context ctx) let close_future_proof ~feedback_id proof = close_proof ~feedback_id ~now:false proof diff --git a/stm/lemmas.ml b/stm/lemmas.ml index e9831f834..9cbd89e8b 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -49,7 +49,7 @@ let adjust_guardness_conditions const = function let env = Global.env() in { const with const_entry_body = Future.chain ~greedy:true ~pure:true const.const_entry_body - (fun (body, eff) -> + (fun ((body, ctx), eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = @@ -60,8 +60,8 @@ let adjust_guardness_conditions const = function let indexes = search_guard Loc.ghost env possible_indexes fixdecls in - mkFix ((indexes,0),fixdecls), eff - | _ -> body, eff) } + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) } let find_mutually_recursive_statements thms = let n = List.length thms in @@ -409,7 +409,7 @@ let start_proof_com kind thms hook = thms in let recguard,thms,snl = look_for_possibly_mutual_statements thms in let evd, nf = Evarutil.nf_evars_and_universes !evdref in - let ctxset = Evd.get_universe_context_set evd in + let ctxset = Evd.universe_context_set evd in let thms = List.map (fun (n, (t, info)) -> (n, ((nf t, ctxset), info))) thms in diff --git a/stm/stm.ml b/stm/stm.ml index 8c034c030..0136e5210 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -808,7 +808,7 @@ end = struct | Declarations.OpaqueDef lc -> let uc = Option.get (Opaqueproof.get_constraints lc) in let uc = - Future.chain ~greedy:true ~pure:true uc Univ.hcons_universe_context in + Future.chain ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in let pr = Opaqueproof.get_proof lc in let pr = Future.chain ~greedy:true ~pure:true pr discharge in let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in @@ -816,7 +816,7 @@ end = struct let extra = Future.join uc in u.(bucket) <- uc; p.(bucket) <- pr; - u, Univ.UContext.union cst extra, false + u, Univ.ContextSet.union cst extra, false | _ -> assert false let check_task name l i = diff --git a/tactics/auto.ml b/tactics/auto.ml index 0f296c6af..ab2a16575 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -922,7 +922,7 @@ let prepare_hint check env init (sigma,c) = let c' = iter c in if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c'; let diff = Evd.diff sigma init in - IsConstr (c', Evd.get_universe_context_set diff) + IsConstr (c', Evd.universe_context_set diff) let interp_hints poly = fun h -> @@ -1164,12 +1164,18 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - let c' = + let ctx, c' = if poly then let evd', subst = Evd.refresh_undefined_universes clenv.evd in - subst_univs_level_constr subst c - else c - in exact_check c' + let ctx = Evd.evar_universe_context evd' in + ctx, subst_univs_level_constr subst c + else + let ctx = Evd.evar_universe_context clenv.evd in + ctx, c + in + fun gl -> + tclTHEN (Refiner.tclEVARS (Evd.merge_universe_context (project gl) ctx)) + (exact_check c') gl (* Util *) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 328d45991..96258a84b 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -125,7 +125,7 @@ let e_exact poly flags (c,clenv) = let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst - in e_give_exact ~flags (Vars.subst_univs_level_constr subst c) + in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) let rec e_trivial_fail_db db_list local_db goal = let tacl = diff --git a/tactics/equality.ml b/tactics/equality.ml index eb8d27f25..e91c21293 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1371,7 +1371,10 @@ let swapEquandsInConcl = let (lbeq,u,eq_args) = find_eq_data (pf_nf_concl gl) in let args = swap_equality_args eq_args @ [Evarutil.mk_new_meta ()] in pf_constr_of_global lbeq.sym (fun sym_equal -> - Proofview.V82.tactic (refine (applist (sym_equal, args)))) + Proofview.V82.tactic (fun gls -> + let c = applist (sym_equal, args) in + let sigma, cty = pf_apply Typing.e_type_of gl c in + refine (applist (c,[Evarutil.mk_new_meta()])) {gls with sigma})) end (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) @@ -1383,10 +1386,12 @@ let bareRevSubstInConcl (lbeq,u) body (t,e1,e2) = let eq_elim, effs = find_elim eq (Some false) false None None gl in (* build substitution predicate *) let p = lambda_create (Proofview.Goal.env gl) (t,body) in + let sigma, pty = pf_apply Typing.e_type_of gl p in (* apply substitution scheme *) let args = [t; e1; p; Evarutil.mk_new_meta (); e2; Evarutil.mk_new_meta ()] in - pf_constr_of_global (ConstRef eq_elim) (fun c -> - Proofview.V82.tactic (refine (applist (c, args)))) + Proofview.V82.tclEVARS sigma <*> + (pf_constr_of_global (ConstRef eq_elim) (fun c -> + Proofview.V82.tactic (refine (applist (c, args))))) end (* [subst_tuple_term dep_pair B] @@ -1456,7 +1461,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let expected_goal = beta_applist (abst_B,List.map fst e2_list) in (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) let expected_goal = nf_betaiota sigma expected_goal in - pred_body,expected_goal + (* Retype to get universes right *) + let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in + sigma,pred_body,expected_goal (* Like "replace" but decompose dependent equalities *) @@ -1466,11 +1473,12 @@ let cutSubstInConcl_RL eqn = Proofview.Goal.raw_enter begin fun gl -> let (lbeq,u,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in let concl = pf_nf_concl gl in - let body,expected_goal = pf_apply subst_tuple_term gl e2 e1 concl in + let sigma,body,expected_goal = pf_apply subst_tuple_term gl e2 e1 concl in if not (dependent (mkRel 1) body) then raise NothingToRewrite; - tclTHENFIRST - (bareRevSubstInConcl (lbeq,u) body eq) - (Proofview.V82.tactic (fun gl -> convert_concl expected_goal DEFAULTcast gl)) + Proofview.V82.tclEVARS sigma <*> + tclTHENFIRST + (bareRevSubstInConcl (lbeq,u) body eq) + (Proofview.V82.tactic (fun gl -> convert_concl expected_goal DEFAULTcast gl)) end (* |- (P e1) @@ -1488,11 +1496,12 @@ let cutSubstInHyp_LR eqn id = Proofview.Goal.enter begin fun gl -> let (lbeq,u,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in let idtyp = pf_get_hyp_typ id gl in - let body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in + let sigma,body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in if not (dependent (mkRel 1) body) then raise NothingToRewrite; let refine = Proofview.V82.tactic (fun gl -> Tacmach.refine_no_check (mkVar id) gl) in let subst = Proofview.V82.of_tactic (tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine) in - Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl) + Proofview.V82.tclEVARS sigma <*> + Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl) end let cutSubstInHyp_RL eqn id = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bda217566..e87c665d0 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -256,8 +256,11 @@ let add_rewrite_hint bases ort t lcsr = let f ce = let c, ctx = Constrintern.interp_constr sigma env ce in let ctx = - if poly then ctx - else (Global.add_constraints (snd ctx); Univ.ContextSet.empty) + if poly then + Evd.evar_universe_context_set ctx + else + let cstrs = Evd.evar_universe_context_constraints ctx in + (Global.add_constraints cstrs; Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in let eqs = List.map f lcsr in @@ -619,7 +622,7 @@ let hResolve id c occ t gl = resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in tclTHEN (Refiner.tclEVARS sigma) (change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl))) gl diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 81bc6a256..a10ad1e2b 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start Evd.empty [invEnv,(invGoal,get_universe_context_set sigma)] in + let pf = Proof.start Evd.empty [invEnv,(invGoal,universe_context_set sigma)] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) @@ -236,10 +236,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op = * inv_op = InvNoThining (derives de semi inversion lemma) *) let add_inversion_lemma_exn na com comsort bool tac = - let env = Global.env () and sigma = Evd.empty in - let c,ctx = Constrintern.interp_type sigma env com in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let sigma, sort = Pretyping.interp_sort sigma comsort in + let env = Global.env () and evd = ref Evd.empty in + let c = Constrintern.interp_type_evars evd env com in + let sigma, sort = Pretyping.interp_sort !evd comsort in try add_inversion_lemma na env sigma c sort bool tac with diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index cbf33fdb4..c6c404992 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -587,7 +587,7 @@ let solve_remaining_by by env prf = List.fold_right (fun mv evd -> let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in let c,_,_ = Pfedit.build_by_tactic env.env (ty,Univ.ContextSet.empty) (Tacticals.New.tclCOMPLETE tac) in - meta_assign mv (c, (Conv,TypeNotProcessed)) evd) + meta_assign mv (fst c (*FIXME*), (Conv,TypeNotProcessed)) evd) indep env.evd in { env with evd = evd' }, prf @@ -1526,7 +1526,8 @@ let newtactic_init_setoid () = with e when Errors.noncritical e -> Proofview.tclZERO e let tactic_init_setoid () = - init_setoid (); tclIDTAC + try init_setoid (); tclIDTAC + with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded") let cl_rewrite_clause_new_strat ?abs strat clause = Proofview.tclTHEN (newtactic_init_setoid ()) @@ -1534,10 +1535,9 @@ let cl_rewrite_clause_new_strat ?abs strat clause = with RewriteFailure s -> newfail 0 (str"setoid rewrite failed: " ++ s)) -(* let cl_rewrite_clause_newtac' l left2right occs clause = *) -(* Proof_global.run_tactic *) -(* (Proofview.tclFOCUS 1 1 *) -(* (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)) *) +let cl_rewrite_clause_newtac' l left2right occs clause = + Proofview.tclFOCUS 1 1 + (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause) let cl_rewrite_clause_strat strat clause = tclTHEN (tactic_init_setoid ()) @@ -1765,7 +1765,7 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr Evd.empty env m in - let sigma = Evd.from_env ~ctx env in + let sigma = Evd.from_env ~ctx:(Evd.evar_universe_context_set ctx) env in let t = Typing.type_of env sigma m in let cstrs = let rec aux t = @@ -1969,12 +1969,15 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = (pf_env gl,project gl, Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) +open Proofview.Notations + let general_s_rewrite_clause x = - init_setoid (); - fun b occs cl ~new_goals -> match x with - | None -> Proofview.V82.tactic (general_s_rewrite None b occs cl ~new_goals) - | Some id -> Proofview.V82.tactic (general_s_rewrite (Some id) b occs cl ~new_goals) + | None -> general_s_rewrite None + | Some id -> general_s_rewrite (Some id) +let general_s_rewrite_clause x y z w ~new_goals = + newtactic_init_setoid () <*> + Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals) let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause @@ -1989,25 +1992,39 @@ let setoid_proof ty fn fallback = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in - try - let rel, args = decompose_app_rel env sigma concl in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env sigma rel)))) in - Proofview.V82.tactic (fn env sigma car rel) - with e when Errors.noncritical e -> - Proofview.tclORELSE fallback (function - | Hipattern.NoEquationFound -> - let e = Errors.push e in - begin match e with - | Not_found -> - let rel, args = decompose_app_rel env sigma concl in - not_declared env ty rel - | _ -> raise e - end - | e -> Proofview.tclZERO e) + Proofview.tclORELSE + begin + try + let rel, args = decompose_app_rel env sigma concl in + let evm = sigma in + let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in + fn env sigma car rel + with e -> Proofview.tclZERO e + end + begin function + | e -> + Proofview.tclORELSE + fallback + begin function + | Hipattern.NoEquationFound -> + (* spiwack: [Errors.push] here is unlikely to do what + it's intended to, or anything meaningful for that + matter. *) + let e = Errors.push e in + begin match e with + | Not_found -> + let rel, args = decompose_app_rel env sigma concl in + not_declared env ty rel + | _ -> Proofview.tclZERO e + end + | e' -> Proofview.tclZERO e' + end + end end let tac_open ((evm,_), c) tac = - tclTHEN (Refiner.tclEVARS evm) (tac c) + Proofview.V82.tactic + (tclTHEN (Refiner.tclEVARS evm) (tac c)) let poly_proof getp gett env evm car rel = if Sorts.is_prop (sort_of_rel env evm rel) then @@ -2024,18 +2041,20 @@ let setoid_reflexivity = let setoid_symmetry = setoid_proof "symmetric" (fun env evm car rel -> - tac_open (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof - env evm car rel) apply) + tac_open + (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof + env evm car rel) + apply) (symmetry_red true) - + let setoid_transitivity c = setoid_proof "transitive" (fun env evm car rel -> - let proof = poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof - env evm car rel in - match c with - | None -> tac_open proof eapply - | Some c -> tac_open proof (fun t -> apply_with_bindings (t,ImplicitBindings [ c ]))) + tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof + env evm car rel) + (fun proof -> match c with + | None -> eapply proof + | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ]))) (transitivity_red true c) let setoid_symmetry_in id = diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 9bdfc08d2..0f155c8bb 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -41,6 +41,10 @@ val cl_rewrite_clause : interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> bool -> Locus.occurrences -> Id.t option -> tactic +val cl_rewrite_clause_newtac' : + interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> + bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic + val is_applied_rewrite_relation : env -> evar_map -> Context.rel_context -> constr -> types option @@ -57,6 +61,12 @@ val add_morphism_infer : bool -> constr_expr -> Id.t -> unit val add_morphism : bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit +val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr + +val get_symmetric_proof : env -> evar_map -> constr -> constr -> evar_map * constr + +val get_transitive_proof : env -> evar_map -> constr -> constr -> evar_map * constr + val default_morphism : (types * constr option) option list * (types * types option) option -> constr -> constr * constr diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 128d8ea87..f32c06ba4 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2145,7 +2145,7 @@ let _ = if has_type arg (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - let ctx = Evd.get_universe_context_set sigma in + let ctx = Evd.universe_context_set sigma in let prf = Proof.start sigma [env, (ty, ctx)] in let (prf, _) = try Proof.run_tactic env tac prf diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cc1096e7c..024165fd0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1224,7 +1224,7 @@ let vm_cast_no_check c gl = let exact_proof c gl = let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) - in tclPUSHCONTEXT Evd.univ_flexible ctx (refine_no_check c) gl + in tclTHEN (tclPUSHEVARUNIVCONTEXT ctx) (refine_no_check c) gl let assumption = let rec arec gl only_eq = function @@ -1237,12 +1237,14 @@ let assumption = let concl = Proofview.Goal.concl gl in let sigma = Proofview.Goal.sigma gl in let (sigma, is_same_type) = - if only_eq then (sigma, eq_constr t concl) + if only_eq then (sigma, Constr.equal t concl) else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then Proofview.Refine.refine (fun h -> (h, mkVar id)) + if is_same_type then + (Proofview.V82.tclEVARS sigma) <*> + Proofview.Refine.refine (fun h -> (h, mkVar id)) else arec gl only_eq rest in let assumption_tac gl = @@ -3743,7 +3745,7 @@ let abstract_subproof id tac = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) let evd, nf = nf_evars_and_universes (Proofview.Goal.sigma gl) in - let ctx = Evd.get_universe_context_set evd in + let ctx = Evd.universe_context_set evd in evd, ctx, nf concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 73be830a4..cbde5f9ab 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -62,7 +62,7 @@ Instance snd_measure : @Measure (A * B) B Snd. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) -Polymorphic Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := +Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2). Infix "*" := RelProd : signature_scope. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cc46fe617..9b5d7ffb0 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -143,7 +143,7 @@ Arguments S _%nat. (********************************************************************) (** * Container datatypes *) -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (** [option A] is the extension of [A] with an extra element [None] *) @@ -250,7 +250,7 @@ Definition app (A : Type) : list A -> list A -> list A := Infix "++" := app (right associativity, at level 60) : list_scope. -Unset Universe Polymorphism. +(* Unset Universe Polymorphism. *) (********************************************************************) (** * The comparison datatype *) diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index f534dd6c6..1ddb59cf4 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -21,19 +21,19 @@ Require Import Logic. Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset of elements of the type [A] which satisfy both [P] and [Q]. *) -Polymorphic Inductive sig (A:Type) (P:A -> Prop) : Type := +(* Polymorphic *) Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. -Polymorphic Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := +(* Polymorphic *) Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) -Polymorphic Inductive sigT (A:Type) (P:A -> Type) : Type := +(* Polymorphic *) Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. -Polymorphic Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := +(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. (* Notations *) @@ -65,7 +65,7 @@ Add Printing Let sigT2. [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Section Subset_projections. Variable A : Type. @@ -215,7 +215,7 @@ Add Printing If sumor. Arguments inleft {A B} _ , [A] B _. Arguments inright {A B} _ , A [B] _. -Unset Universe Polymorphism. +(* Unset Universe Polymorphism. *) (** Various forms of the axiom of choice for specifications *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index f6a0382c2..2062f3861 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -10,7 +10,7 @@ Require Import Le Gt Minus Bool. Require Setoid. Set Implicit Arguments. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (******************************************************************) (** * Basics: definition of polymorphic lists and some operations *) @@ -2036,4 +2036,4 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes v62. (* end hide *) -Unset Universe Polymorphism. +(* Unset Universe Polymorphism. *) diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index ba62fa7fd..644d479c6 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -11,7 +11,7 @@ Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (** * Logical relations over lists with respect to a setoid equality or ordering. *) diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index 05f03ea56..afc7c25bd 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -7,7 +7,7 @@ (***********************************************************************) Require Import SetoidList. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 57a82161d..d8416b3e2 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -100,7 +100,7 @@ Local Unset Intuition Negation Unfolding. so they require polymorphism otherwise their first application (e.g. to an existential in [Set]) will fix the level of [A]. *) -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Section ChoiceSchemes. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index bd6e2ca8f..2f61e0e29 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -52,7 +52,7 @@ Table of contents: Import EqNotations. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Section Dependent_Equality. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index e4db81faf..0758bd1f9 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -35,7 +35,7 @@ Table of contents: (** * Streicher's K and injectivity of dependent pair hold on decidable types *) Set Implicit Arguments. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Section EqdepDec. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index d8f675ade..ed09030cb 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -1047,7 +1047,7 @@ Qed. (** ** Filter *) -Polymorphic Lemma filter_app A f (l l':list A) : +Lemma filter_app A f (l l':list A) : List.filter f (l ++ l') = List.filter f l ++ List.filter f l'. Proof. induction l as [|x l IH]; simpl; trivial. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index ab1eccee2..a86ae783e 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,7 +15,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (** The polymorphic identity function is defined in [Datatypes]. *) diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 899acfc64..a7eddd9f0 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -16,7 +16,7 @@ Require Import List Setoid Compare_dec Morphisms FinFun. Import ListNotations. (* For notations [] and [a;b;c] *) Set Implicit Arguments. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) Section Permutation. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 5b52c6ec9..beed92b84 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -20,7 +20,7 @@ Require Import List Relations Relations_1. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (** Preambule *) diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index f12aa0b87..6d2146b8e 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -21,7 +21,7 @@ Require Vectors.Fin. Import EqNotations. Local Open Scope nat_scope. -Set Universe Polymorphism. +(* Set Universe Polymorphism. *) (** A vector is a list of size n whose elements belong to a set A. *) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 1a1a4dfe7..5129beeab 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -645,7 +645,7 @@ let make_bl_scheme mind = let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (bl_goal, ctx) (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in - ([|ans|], Evd.empty_evar_universe_context), eff + ([|fst ans (*FIXME univs*)|], Evd.empty_evar_universe_context), eff let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme @@ -766,7 +766,7 @@ let make_lb_scheme mind = let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (lb_goal,Univ.ContextSet.empty) (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in - ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), eff + ([|fst ans|], Evd.empty_evar_universe_context (* FIXME *)), eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -939,7 +939,7 @@ let make_eq_decidability mind = (compute_dec_goal (ind,u) lnamesparrec nparrec, Univ.ContextSet.empty) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff + ([|fst ans (*FIXME*)|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 35ad31f0a..b9c4a4294 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -294,14 +294,14 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in obls, Some constr, typ | None -> [||], None, termtype in - let ctx = Evd.get_universe_context_set evm in + let ctx = Evd.universe_context_set evm in ignore (Obligations.add_definition id ?term:constr typ ctx ~kind:(Global,poly,Instance) ~hook obls); id else (Flags.silently (fun () -> - Lemmas.start_proof id kind (termtype, Evd.get_universe_context_set evm) + Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm) (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 @@ -335,7 +335,7 @@ let context l = with e when Errors.noncritical e -> error "Anonymous variables not allowed in contexts." in - let uctx = Evd.get_universe_context_set !evars in + let uctx = Evd.universe_context_set !evars in let fn status (id, b, t) = (* let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in *) if Lib.is_modtype () && not (Lib.sections_are_opened ()) then diff --git a/toplevel/command.ml b/toplevel/command.ml index 22830eb6d..4a26b7502 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -70,9 +70,9 @@ let red_constant_entry n ce = function let proof_out = ce.const_entry_body in let env = Global.env () in { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out - (fun (body,eff) -> - under_binders env - (fst (reduction_of_red_expr env red)) n body,eff) } + (fun ((body,ctx),eff) -> + (under_binders env + (fst (reduction_of_red_expr env red)) n body,ctx),eff) } let interp_definition bl p red_option c ctypopt = let env = Global.env() in @@ -90,7 +90,7 @@ let interp_definition bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Universes.universes_of_constr body in let ctx = Universes.restrict_universe_context - (Evd.get_universe_context_set !evdref) vars in + (Evd.universe_context_set !evdref) vars in imps1@(Impargs.lift_implicits nb_args imps2), definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body | Some ctyp -> @@ -116,7 +116,7 @@ let interp_definition bl p red_option c ctypopt = let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Universes.restrict_universe_context - (Evd.get_universe_context_set !evdref) vars in + (Evd.universe_context_set !evdref) vars in imps1@(Impargs.lift_implicits nb_args impsty), definition_entry ~types:typ ~poly:p ~univs:(Univ.ContextSet.to_context ctx) body @@ -171,8 +171,9 @@ let do_definition ident k bl red_option c ctypopt hook = let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in - let c,sideff = Future.force ce.const_entry_body in + let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty sideff); + assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t | None -> Retyping.get_type_of env evd c @@ -181,7 +182,7 @@ let do_definition ident k bl red_option c ctypopt hook = let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in - let ctx = Evd.get_universe_context_set evd in + let ctx = Evd.universe_context_set evd in ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in ignore(declare_definition ident k ce imps @@ -228,7 +229,7 @@ let interp_assumption evdref env bl c = let c = prod_constr_expr c bl in let ty, impls = interp_type_evars_impls evdref env c in let evd, nf = nf_evars_and_universes !evdref in - let ctx = Evd.get_universe_context_set evd in + let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) let declare_assumptions idl is_coe k c imps impl_is_on nl = @@ -659,7 +660,7 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix (_,poly,_ as kind) ctx f (def,eff) t imps = +let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps = let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in declare_definition f kind ce imps (fun _ r -> r) @@ -873,7 +874,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp in - let ctx = Evd.get_universe_context_set !evdref in + let ctx = Evd.universe_context_set !evdref in ignore(Obligations.add_definition recname ~term:evars_def evars_typ ctx evars ~hook) @@ -939,12 +940,12 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = let interp_fixpoint l ntns = let (env,_,evd),fix,info = interp_recursive true l ntns in check_recursive true env evd fix; - (fix,Evd.get_universe_context_set evd,info) + (fix,Evd.universe_context_set evd,info) let interp_cofixpoint l ntns = let (env,_,evd),fix,info = interp_recursive false l ntns in check_recursive false env evd fix; - fix,Evd.get_universe_context_set evd,info + fix,Evd.universe_context_set evd,info let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then @@ -968,7 +969,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let fixdecls = List.map (fun c -> c, Declareops.no_seff) fixdecls in + let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let ctx = Univ.ContextSet.to_context ctx in ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); @@ -996,7 +997,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let fixdecls = List.map (fun c-> c,Declareops.no_seff) fixdecls in + let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let ctx = Univ.ContextSet.to_context ctx in ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) @@ -1071,7 +1072,7 @@ let do_program_recursive local p fixkind fixl ntns = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl end in - let ctx = Evd.get_universe_context_set evd in + let ctx = Evd.universe_context_set evd in let kind = match fixkind with | Obligations.IsFixpoint _ -> (local, p, Fixpoint) | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 5d0bcd78b..3015eab25 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -70,20 +70,17 @@ let abstract_inductive hyps nparams inds = let refresh_polymorphic_type_of_inductive (_,mip) = match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, Univ.ContextSet.empty + | RegularArity s -> s.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - let univ, uctx = Universes.new_global_univ () in - mkArity (List.rev ctx, Type univ), uctx + mkArity (List.rev ctx, Type ar.template_level) let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in - let univctx = ref Univ.ContextSet.empty in let inds = Array.map_to_list (fun mip -> - let ty, uctx = refresh_polymorphic_type_of_inductive (mib,mip) in - let () = univctx := Univ.ContextSet.union uctx !univctx in + let ty = refresh_polymorphic_type_of_inductive (mib,mip) in let arity = expmod_constr modlist ty in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, @@ -93,10 +90,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let univs = Univ.UContext.union abs_ctx - (Univ.UContext.union (Univ.ContextSet.to_context !univctx) - mib.mind_universes) - in + let univs = Univ.UContext.union abs_ctx mib.mind_universes in { mind_entry_record = mib.mind_record <> None; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 2a408e03d..1ee2adcd8 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -123,7 +123,7 @@ let define internal id c p univs = let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in let entry = { - const_entry_body = Future.from_val (c,Declareops.no_seff); + const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_proj = None; diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 57b428b5c..ac3bf5929 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -361,7 +361,7 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) - let proof_output = Future.from_val (decl,Declareops.no_seff) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in let cst = define fi UserVerbose sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -459,7 +459,7 @@ let do_combined_scheme name schemes = schemes in let body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val (body,Declareops.no_seff) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 97c95bfd8..d45c2af3e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -560,6 +560,8 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx +let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff) + let declare_mutual_definition l = let len = List.length l in let first = List.hd l in @@ -589,11 +591,11 @@ let declare_mutual_definition l = possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> - mkFix ((indexes,i),fixdecls),Declareops.no_seff) 0 l + mk_proof (mkFix ((indexes,i),fixdecls))) 0 l | IsCoFixpoint -> None, List.map_i (fun i _ -> - mkCoFix (i,fixdecls),Declareops.no_seff) 0 l + mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) let ctx = Univ.ContextSet.to_context first.prg_ctx in @@ -630,7 +632,7 @@ let declare_obligation prg obl body uctx = shrink_body body else [], body, [||] in let ce = - { const_entry_body = Future.from_val(body,Declareops.no_seff); + { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then Some ty else None; const_entry_proj = None; @@ -796,8 +798,8 @@ let solve_by_tac name evi t poly subst ctx = let entry = Term_typing.handle_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); - Inductiveops.control_only_guard (Global.env ()) body; - body, subst, entry.Entries.const_entry_universes + Inductiveops.control_only_guard (Global.env ()) (fst body) (*FIXME ignoring the context...*); + (fst body), subst, entry.Entries.const_entry_universes (* try *) (* let substref = ref (Univ.LMap.empty, Univ.UContext.empty) in *) diff --git a/toplevel/record.ml b/toplevel/record.ml index af7f364f3..c4a4951b3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -258,7 +258,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls in let cie = { const_entry_body = - Future.from_val (proj,Declareops.no_seff); + Future.from_val (Term_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ca31d1f2e..0dbc77b83 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1411,11 +1411,12 @@ let vernac_declare_reduction locality s r = (* The same but avoiding the current goal context if any *) let vernac_global_check c = - let evmap = Evd.empty in let env = Global.env() in + let evmap = Evd.from_env env in let c,ctx = interp_constr evmap env c in let senv = Global.safe_env() in - let senv = Safe_typing.add_constraints (snd ctx) senv in + let cstrs = snd (Evd.evar_universe_context_set ctx) in + let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in msg_notice (print_safe_judgment env j) |