diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 34 | ||||
| -rw-r--r-- | vernac/command.ml | 15 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 19 | ||||
| -rw-r--r-- | vernac/obligations.ml | 45 | ||||
| -rw-r--r-- | vernac/record.ml | 36 |
6 files changed, 95 insertions, 60 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 6f5f96ee2..c99eba2cc 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -200,16 +200,22 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let nf, subst = Evarutil.e_nf_evars_and_universes evars in let termtype = let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - nf t - in - Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); + nf t + in + Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); let ctx = Evd.check_univ_decl !evars decl in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in + let ctx = if poly + then Polymorphic_const_entry ctx + else + (* FIXME be smarter about this *) + Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); - instance_hook k pri global imps ?hook (ConstRef cst); id + instance_hook k pri global imps ?hook (ConstRef cst); id end else ( let props = @@ -384,14 +390,20 @@ let context poly l = 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 ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) + let univs = !uctx in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context univs) + else Monomorphic_const_entry univs + in + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + (* FIXME be smarter about this *) + let univs = Univ.ContextSet.to_context univs in + let entry = Declare.definition_entry ~poly ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in diff --git a/vernac/command.ml b/vernac/command.ml index 80599c534..06d0c8470 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -197,8 +197,11 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in + let ctx = if p + then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) + else Monomorphic_const_entry ctx + in + let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -206,9 +209,9 @@ match local with let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = - if p (* polymorphic *) then Univ.UContext.instance ctx - else Univ.Instance.empty + let inst = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -606,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx else - Monomorphic_ind_entry uctx + Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) in (* Build the mutual inductive entry *) let mind_ent = diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c728c2671..e4ca98749 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,10 +109,10 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.to_universe_context ctx in let univs = - if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if Flags.is_universe_polymorphism () + then Polymorphic_const_entry (Evd.to_universe_context ctx) + else Monomorphic_const_entry (Evd.universe_context_set ctx) in let kn = f id (DefinitionEntry diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 71d80c4db..f59b5fcae 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -242,7 +242,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let ctx = if p + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let decl = (ParameterEntry (None,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -491,9 +495,12 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.context (fst universes) in + let ctx = if pi2 k (* polymorphic *) + then Polymorphic_const_entry (UState.context (fst universes)) + else Monomorphic_const_entry (UState.context_set (fst universes)) + in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in @@ -516,8 +523,12 @@ let save_proof ?proof = function let evd = Evd.from_ctx universes in let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in + let ctx = if poly + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in let binders = if poly then Some (UState.universe_binders universes) else None in - Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 43af8968f..a9110c76c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -633,12 +633,11 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_universes = univs; + const_entry_universes = uctx; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; @@ -647,13 +646,15 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - true, { obl with obl_body = - if poly then - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - else - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } + if not opaque then add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = match uctx with + | Polymorphic_const_entry uctx -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_const_entry _ -> + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) + in + true, { obl with obl_body = body } let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind notations obls impls kind reduce hook = @@ -855,7 +856,10 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = UState.context ctx in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -967,13 +971,16 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.context ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in + 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 evd = Evd.from_env (Global.env ()) in @@ -1121,9 +1128,9 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = UState.context prg.prg_ctx in + let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in let kn = Declare.declare_constant x.obl_name ~local:true - (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) + (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/record.ml b/vernac/record.ml index 0819dadb4..faf277d86 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -270,7 +270,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let u = Univ.UContext.instance ctx in + let u = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry ctx -> Univ.Instance.empty + in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in let r = mkIndU (indsp,u) in @@ -327,16 +330,12 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let univs = - if poly then Polymorphic_const_entry ctx - else Monomorphic_const_entry ctx - in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_universes = univs; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -391,11 +390,14 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let poly, ctx = + let template, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty - | Polymorphic_ind_entry ctx -> true, ctx - | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_ind_entry ctx -> + template, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + false, Polymorphic_const_entry ctx + | Cumulative_ind_entry cumi -> + false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -405,7 +407,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let mie_ind = { mind_entry_typename = id; mind_entry_arity = arity; - mind_entry_template = not poly && template; + mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in @@ -419,14 +421,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t } in let mie = - if poly then - begin + match ctx with + | Polymorphic_const_entry ctx -> let env = Global.env () in let env' = Environ.push_context ctx env in let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie - end - else + | Monomorphic_const_entry _ -> mie in let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in @@ -434,6 +435,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); rsp @@ -499,7 +501,7 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -626,7 +628,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs |