diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 83 |
1 files changed, 51 insertions, 32 deletions
diff --git a/library/declare.ml b/library/declare.ml index c0c4dd571..452504bf0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,36 +44,40 @@ let if_xml f x = if !Flags.xml_export then f x else () type section_variable_entry = | SectionLocalDef of definition_entry - | SectionLocalAssum of types * bool (* Implicit status *) + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with - | Inl cst -> Global.add_constraints cst + | Inl ctx -> Global.push_context_set ctx | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - let impl,opaq,cst = match d with (* Fails if not well-typed *) - | SectionLocalAssum (ty, impl) -> - let cst = Global.push_named_assum (id,ty) in - let impl = if impl then Implicit else Explicit in - impl, true, cst - | SectionLocalDef de -> - let cst = Global.push_named_def (id,de) in - Explicit, de.const_entry_opaque, cst in + + let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum ((ty,ctx),poly,impl) -> + let () = Global.push_named_assum ((id,ty),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx + | SectionLocalDef (de) -> + let () = Global.push_named_def (id,de) in + Explicit, de.const_entry_opaque, de.const_entry_polymorphic, + (Univ.ContextSet.of_context de.const_entry_universes) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl; + add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id (p,opaq,cst,mk) + add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> Some (Inl (variable_constraints id)) + | Inr (id,_) -> + if variable_polymorphic id then None + else Some (Inl (variable_context id)) | Inl _ -> Some o type variable_obj = - (Univ.constraints, Id.t * variable_declaration) union + (Univ.ContextSet.t, Id.t * variable_declaration) union let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with @@ -139,7 +143,8 @@ let cache_constant ((sp,kn), obj) = let kn' = Global.add_constant dir id obj.cst_decl in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); - add_section_constant kn' (Global.lookup_constant kn').const_hyps; + let cst = Global.lookup_constant kn' in + add_section_constant (cst.const_proj <> None) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -150,16 +155,18 @@ let discharged_hyps kn sechyps = let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in + let from = Global.lookup_constant con in let modlist = replacement_context () in - let hyps = section_segment_of_constant con in + let hyps,uctx = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in - let abstract = named_of_variable_context hyps in + let abstract = (named_of_variable_context hyps, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) +let dummy_constant_entry = + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -187,6 +194,18 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c +let definition_entry ?(opaque=false) ?types + ?(poly=false) ?(univs=Univ.UContext.empty) body = + { const_entry_body = Future.from_val (body,Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = types; + const_entry_proj = None; + const_entry_polymorphic = poly; + const_entry_universes = univs; + const_entry_opaque = opaque; + const_entry_feedback = None; + const_entry_inline_code = false} + let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f let declare_sideff se = @@ -203,8 +222,7 @@ let declare_sideff se = in let ty_of cb = match cb.Declarations.const_type with - | Declarations.NonPolymorphicType t -> Some t - | _ -> None in + | (* Declarations.NonPolymorphicType *)t -> Some t in let cst_of cb = let pt, opaque = pt_opaque_of cb in let ty = ty_of cb in @@ -215,6 +233,9 @@ let declare_sideff se = const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = Future.join cb.const_universes; + const_entry_proj = None; }); cst_hyps = [] ; cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; @@ -252,16 +273,11 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - id ?types body = + ?(poly=false) id ?types (body,ctx) = let cb = - { Entries.const_entry_body = body; - const_entry_type = types; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_secctx = None; - const_entry_feedback = None } + definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -311,7 +327,8 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let _,dir,_ = repr_kn kn in let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); - add_section_kn kn' (Global.lookup_mind kn').mind_hyps; + let mind = Global.lookup_mind kn' in + add_section_kn kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -319,9 +336,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps = section_segment_of_mutual_inductive mind in + let sechyps,uctx = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps) repl mie) + Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -335,7 +352,9 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = false; mind_entry_finite = true; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; + mind_entry_polymorphic = false; + mind_entry_universes = Univ.UContext.empty }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry |