diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 10 | ||||
| -rw-r--r-- | toplevel/classes.ml | 15 | ||||
| -rw-r--r-- | toplevel/command.ml | 34 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 25 | ||||
| -rw-r--r-- | toplevel/record.ml | 92 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
7 files changed, 106 insertions, 80 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 4122487e2..8ac273c84 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -304,7 +304,7 @@ let build_beq_scheme mode kn = raise (NonSingletonProp (kn,i)); let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), - Evd.empty_evar_universe_context (* FIXME *)), + Evd.make_evar_universe_context (Global.env ()) None), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -641,7 +641,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) @@ -764,12 +764,12 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = Evd.empty_evar_universe_context in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in - ([|ans|], ctx (* FIXME *)), eff + ([|ans|], ctx), eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -934,7 +934,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = Evd.empty_evar_universe_context (* FIXME *)in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7fe79d948..805a29e39 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -347,7 +347,7 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in - let evars = ref Evd.empty in + let evars = ref (Evd.from_env env) in let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.map_rel_context subst fullctx in @@ -358,11 +358,13 @@ let context poly l = with e when Errors.noncritical e -> error "Anonymous variables not allowed in contexts." in - let uctx = Evd.universe_context_set !evars in + let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let uctx = Univ.ContextSet.to_context uctx in - let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in + let ctx = Univ.ContextSet.to_context !uctx in + (* Declare the universe context once *) + let () = uctx := Univ.ContextSet.empty in + let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> @@ -379,8 +381,9 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] impl Vernacexpr.NoInline (Loc.ghost, id)) in - status && nstatus + let () = uctx := Univ.ContextSet.empty in + status && nstatus in List.fold_left fn true (List.rev ctx) diff --git a/toplevel/command.ml b/toplevel/command.ml index e2e5d8704..b65ff73fe 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -241,11 +241,14 @@ let interp_assumption evdref env impls bl c = 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 = - let refs, status = - List.fold_left (fun (refs,status) id -> - let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in - (ref',u')::refs, status' && status) ([],true) idl in +let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = + let refs, status, _ = + List.fold_left (fun (refs,status,ctx) id -> + let ref',u',status' = + declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in + (ref',u')::refs, status' && status, Univ.ContextSet.empty) + ([],true,ctx) idl + in List.rev refs, status let do_assumptions (_, poly, _ as kind) nl l = @@ -467,16 +470,17 @@ let inductive_levels env evdref poly arities inds = Evd.set_leq_sort env evd (Prop Pos) du else evd in - (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *) - let duu = Sorts.univ_of_sort du in - let evd = - if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then - if is_flexible_sort evd duu then - Evd.set_eq_sort env evd (Prop Null) du - else evd - else Evd.set_eq_sort env evd (Type cu) du - in - (evd, arity :: arities)) + let duu = Sorts.univ_of_sort du in + let evd = + if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then + if is_flexible_sort evd duu then + if Evd.check_leq evd Univ.type0_univ duu then + evd + else Evd.set_eq_sort env evd (Prop Null) du + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) (!evdref,[]) (Array.to_list levels') destarities sizes in evdref := evd; List.rev arities diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 452d5fbe5..ae8ee7670 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -423,7 +423,7 @@ let fold_left' f = function let build_combined_scheme env schemes = let defs = List.map (fun cst -> (* FIXME *) - let evd, c = Evd.fresh_constant_instance env Evd.empty cst in + let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in (c, Typeops.type_of_constant_in env c)) schemes in (* let nschemes = List.length schemes in *) let find_inductive ty = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 0b15ecf33..d2bd2c07b 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -625,7 +625,7 @@ let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in match obl.obl_status with - | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) } + | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let poly = pi2 prg.prg_kind in @@ -649,7 +649,7 @@ let declare_obligation prg obl body ty uctx = in if not opaque then add_hint false prg constant; definition_message obl.obl_name; - { obl with obl_body = + true, { obl with obl_body = if poly then Some (DefinedObl constant) else @@ -798,9 +798,9 @@ let solve_by_tac name evi t poly ctx = let entry = Term_typing.handle_entry_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); - assert(Univ.ContextSet.is_empty (snd body)); + let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, ctx' + (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' let obligation_terminator name num guard hook pf = let open Proof_global in @@ -824,7 +824,7 @@ let obligation_terminator name num guard hook pf = let obls, rem = prg.prg_obligations in let obl = obls.(num) in let ctx = Evd.evar_context_universe_context uctx in - let obl = declare_obligation prg obl body ty ctx in + let (_, obl) = declare_obligation prg obl body ty ctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in try ignore (update_obls prg obls (pred rem)) @@ -847,9 +847,9 @@ let obligation_hook prg obl num auto ctx' _ gr = let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' + (* The universe context was declared globally, we continue + from the new global environment. *) + Evd.evar_universe_context (Evd.from_env (Global.env ())) else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -922,8 +922,13 @@ and solve_obligation_by_tac prg obls i tac = (pi2 !prg.prg_kind) !prg.prg_ctx in let uctx = Evd.evar_context_universe_context ctx in - prg := {!prg with prg_ctx = ctx}; - obls.(i) <- declare_obligation !prg obl t ty uctx; + let () = prg := {!prg with prg_ctx = ctx} in + let def, obl' = declare_obligation !prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 !prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + prg := {!prg with prg_ctx = ctx'}); true else false with e when Errors.noncritical e -> diff --git a/toplevel/record.ml b/toplevel/record.ml index e214f9ca7..60fe76bb8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -131,14 +131,21 @@ let typecheck_params_and_fields def id pl t ps nots fs = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in - let evars = + let arity, evars = let _, univ = compute_constructor_level evars env_ar newfs in let ctx, aritysort = Reduction.dest_arity env0 arity in assert(List.is_empty ctx); (* Ensured by above analysis *) if Sorts.is_prop aritysort || (Sorts.is_set aritysort && is_impredicative_set env0) then - evars - else Evd.set_leq_sort env_ar evars (Type univ) aritysort + arity, evars + else + let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in + if Univ.is_small_univ univ then + (* We can assume that the level aritysort is not constrained + and clear it. *) + mkArity (ctx, Sorts.sort_of_univ univ), + Evd.set_eq_sort env_ar evars (Prop Pos) aritysort + else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in @@ -233,7 +240,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (mib,mip) = Global.lookup_inductive indsp in let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in + let poly = mib.mind_polymorphic in + let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in @@ -293,7 +301,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = + if poly then ctx else Univ.UContext.empty; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -397,44 +406,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let impl, projs = match fields with | [(Name proj_name, _, field)] when def -> - let class_body = it_mkLambda_or_LetIn field params in - let _class_type = it_mkProd_or_LetIn arity params in - let class_entry = - Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in - let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref [paramimpls]; - Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None - in - cref, [Name proj_name, sub, Some proj_cst] + let class_body = it_mkLambda_or_LetIn field params in + let _class_type = it_mkProd_or_LetIn arity params in + let class_entry = + Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in + let proj_entry = + Declare.definition_entry ~types:proj_type ~poly + ~univs:(if poly then ctx else Univ.UContext.empty) proj_body + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = match List.hd coers with + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None + in + cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign - in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> - if b then Backward, pri else Forward, pri) coe) + in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> + if b then Backward, pri else Forward, pri) coe) coers priorities - in - IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y)) - (List.rev fields) coers (Recordops.lookup_projections ind)) + in + let l = List.map3 (fun (id, _, _) b y -> (id, b, y)) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l in let ctx_context = List.map (fun (na, b, t) -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ae6ac2bc..c07c756c0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -76,9 +76,8 @@ let show_universes () = let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -1185,8 +1184,9 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let env = Global.env() in - let t,ctx = Constrintern.interp_type env Evd.empty c in - let t = Detyping.detype false [] env Evd.empty t in + let sigma = Evd.from_env env in + let t,ctx = Constrintern.interp_type env sigma c in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |