diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 43 | ||||
-rw-r--r-- | library/declare.mli | 13 | ||||
-rw-r--r-- | library/decls.ml | 16 | ||||
-rw-r--r-- | library/decls.mli | 6 | ||||
-rw-r--r-- | library/kindops.ml | 4 | ||||
-rw-r--r-- | library/lib.ml | 22 | ||||
-rw-r--r-- | library/lib.mli | 8 |
7 files changed, 48 insertions, 64 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5c6543e28..cc8415cf4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,9 +44,7 @@ let if_xml f x = if !Flags.xml_export then f x else () type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; - polymorphic : bool; - implicit_status : implicit_status } + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -58,22 +56,19 @@ let cache_variable ((sp,_),o) = if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum { type_context = (ty,ctx); polymorphic; implicit_status } -> - let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in - implicit_status, true, polymorphic, ctx + 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,poly),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl ~polymorphic ctx; + add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id { dir_path = p; - opaque; - universe_context_set = ctx; - polymorphic; - kind = mk } + add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with | Inr (id,_) -> @@ -241,11 +236,11 @@ let declare_constant_common id cst = c let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(polymorphic=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; - const_entry_polymorphic = polymorphic; + const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; @@ -277,9 +272,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(polymorphic=false) id ?types (body,ctx) = + ?(poly=false) id ?types (body,ctx) = let cb = - definition_entry ?types ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + 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) @@ -463,10 +458,10 @@ let input_universes : universe_decl -> Libobject.obj = discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); classify_function = (fun a -> Keep a) } -let do_universe ~polymorphic l = +let do_universe poly l = let in_section = Lib.sections_are_opened () in let () = - if polymorphic && not in_section then + if poly && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in @@ -475,7 +470,7 @@ let do_universe ~polymorphic l = let lev = Universes.new_univ_level (Global.current_dirpath ()) in (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (polymorphic, l)) + Lib.add_anonymous_leaf (input_universes (poly, l)) type constraint_decl = polymorphic * Univ.constraints @@ -495,7 +490,7 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint ~polymorphic l = +let do_constraint poly l = let u_of_id = let names, _ = Universes.global_universe_names () in fun (loc, id) -> @@ -505,12 +500,12 @@ let do_constraint ~polymorphic l = in let in_section = Lib.sections_are_opened () in let () = - if polymorphic && not in_section then + if poly && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = - if polymorphic then () + if poly then () else if p || p' then let loc = if p then loc else loc' in user_err ~loc ~hdr:"Constraint" @@ -524,4 +519,4 @@ let do_constraint ~polymorphic l = Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (polymorphic, constraints)) + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index a0ec26444..7824506da 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,9 +23,7 @@ open Decl_kinds type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; - polymorphic : bool; - implicit_status : implicit_status } + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -44,7 +42,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?polymorphic:bool -> ?univs:Univ.universe_context -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -58,7 +56,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?polymorphic:bool -> Id.t -> ?types:constr -> + ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant (** Since transparent constants' side effects are globally declared, we @@ -91,6 +89,5 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -val do_universe : polymorphic:bool -> Id.t Loc.located list -> unit -val do_constraint : polymorphic:bool -> - (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/decls.ml b/library/decls.ml index 1e9afe968..2952c258a 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,22 +19,18 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - { dir_path : DirPath.t; - opaque : bool; - universe_context_set : Univ.universe_context_set; - polymorphic : bool; - kind : logical_kind } + DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = (Id.Map.find id !vartab).dir_path -let variable_opacity id = (Id.Map.find id !vartab).opaque -let variable_kind id = (Id.Map.find id !vartab).kind -let variable_context id = (Id.Map.find id !vartab).universe_context_set -let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic +let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq +let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k +let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx +let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in diff --git a/library/decls.mli b/library/decls.mli index e84a6376b..1ca7f8946 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -17,11 +17,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - { dir_path : DirPath.t; - opaque : bool; - universe_context_set : Univ.universe_context_set; - polymorphic : bool; - kind : logical_kind } + DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t diff --git a/library/kindops.ml b/library/kindops.ml index 3d737e5ac..21b1bec33 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,9 +24,9 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - let locality = def.locality in + let (locality, poly, kind) = def in let error () = CErrors.anomaly (Pp.str "Internal definition kind") in - match def.object_kind with + match kind with | Definition -> begin match locality with | Discharge -> "Let" diff --git a/library/lib.ml b/library/lib.ml index 13921610d..749cc4ff3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -391,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.implicit_status * + | Variable of (Names.Id.t * Decl_kinds.binding_kind * Decl_kinds.polymorphic * Univ.universe_context_set) | Context of Univ.universe_context_set @@ -416,12 +416,12 @@ let check_same_poly p vars = if List.exists pred vars then error "Cannot mix universe polymorphic and monomorphic declarations in sections." -let add_section_variable id impl ~polymorphic ctx = +let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; - sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -450,11 +450,11 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst -let add_section_replacement f g ~polymorphic hyps = +let add_section_replacement f g poly hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly polymorphic vars in + let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -462,13 +462,13 @@ let add_section_replacement f g ~polymorphic hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn ~polymorphic kn = +let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f ~polymorphic + add_section_replacement f f poly -let add_section_constant ~polymorphic kn = +let add_section_constant poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f ~polymorphic + add_section_replacement f f poly let replacement_context () = pi2 (List.hd !sectab) diff --git a/library/lib.mli b/library/lib.mli index 51c74d395..092643c2d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,7 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -176,11 +176,11 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.implicit_status -> polymorphic:bool -> Univ.universe_context_set -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : polymorphic:bool -> +val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Context.Named.t -> unit -val add_section_kn : polymorphic:bool -> +val add_section_kn : Decl_kinds.polymorphic -> Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list |