diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
commit | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch) | |
tree | 0dd3a804e1924862390a7f78abc9a8a119127f9c /library | |
parent | ceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff) | |
parent | 1bc1cba7a759a285131a3ed6ea8979716700b856 (diff) |
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
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, 64 insertions, 48 deletions
diff --git a/library/declare.ml b/library/declare.ml index cc8415cf4..5c6543e28 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,7 +44,9 @@ 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 types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; + polymorphic : bool; + implicit_status : implicit_status } type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -56,19 +58,22 @@ let cache_variable ((sp,_),o) = if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - 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 + 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 | 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 poly ctx; + add_section_variable id impl ~polymorphic ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id (p,opaq,ctx,poly,mk) + add_variable_data id { dir_path = p; + opaque; + universe_context_set = ctx; + polymorphic; + kind = mk } let discharge_variable (_,o) = match o with | Inr (id,_) -> @@ -236,11 +241,11 @@ let declare_constant_common id cst = c let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + ?(polymorphic=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 = poly; + const_entry_polymorphic = polymorphic; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; @@ -272,9 +277,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(poly=false) id ?types (body,ctx) = + ?(polymorphic=false) id ?types (body,ctx) = let cb = - definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + definition_entry ?types ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -458,10 +463,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 poly l = +let do_universe ~polymorphic l = let in_section = Lib.sections_are_opened () in let () = - if poly && not in_section then + if polymorphic && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in @@ -470,7 +475,7 @@ let do_universe poly l = let lev = Universes.new_univ_level (Global.current_dirpath ()) in (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (poly, l)) + Lib.add_anonymous_leaf (input_universes (polymorphic, l)) type constraint_decl = polymorphic * Univ.constraints @@ -490,7 +495,7 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint poly l = +let do_constraint ~polymorphic l = let u_of_id = let names, _ = Universes.global_universe_names () in fun (loc, id) -> @@ -500,12 +505,12 @@ let do_constraint poly l = in let in_section = Lib.sections_are_opened () in let () = - if poly && not in_section then + if polymorphic && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = - if poly then () + if polymorphic then () else if p || p' then let loc = if p then loc else loc' in user_err ~loc ~hdr:"Constraint" @@ -519,4 +524,4 @@ let do_constraint poly l = Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) + Lib.add_anonymous_leaf (input_constraints (polymorphic, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 7824506da..a0ec26444 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,7 +23,9 @@ open Decl_kinds type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; + polymorphic : bool; + implicit_status : implicit_status } type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -42,7 +44,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 -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?polymorphic:bool -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -56,7 +58,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> + ?local:bool -> ?polymorphic:bool -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant (** Since transparent constants' side effects are globally declared, we @@ -89,5 +91,6 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -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 +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 diff --git a/library/decls.ml b/library/decls.ml index 2952c258a..1e9afe968 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,18 +19,22 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind + { dir_path : DirPath.t; + opaque : bool; + universe_context_set : Univ.universe_context_set; + polymorphic : bool; + kind : 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 = 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_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_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 1ca7f8946..e84a6376b 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -17,7 +17,11 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind + { dir_path : DirPath.t; + opaque : bool; + universe_context_set : Univ.universe_context_set; + polymorphic : bool; + kind : 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 21b1bec33..3d737e5ac 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, poly, kind) = def in + let locality = def.locality in let error () = CErrors.anomaly (Pp.str "Internal definition kind") in - match kind with + match def.object_kind with | Definition -> begin match locality with | Discharge -> "Let" diff --git a/library/lib.ml b/library/lib.ml index 749cc4ff3..13921610d 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.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status 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.binding_kind * + | Variable of (Names.Id.t * Decl_kinds.implicit_status * 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 poly ctx = +let add_section_variable id impl ~polymorphic ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (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 + List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; + sectab := (Variable (id,impl,polymorphic,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 poly hyps = +let add_section_replacement f g ~polymorphic hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in + let () = check_same_poly polymorphic 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 poly hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn poly kn = +let add_section_kn ~polymorphic kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic -let add_section_constant poly kn = +let add_section_constant ~polymorphic kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic let replacement_context () = pi2 (List.hd !sectab) diff --git a/library/lib.mli b/library/lib.mli index 092643c2d..51c74d395 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.binding_kind +type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status 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.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.implicit_status -> polymorphic:bool -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : Decl_kinds.polymorphic -> +val add_section_constant : polymorphic:bool -> Names.constant -> Context.Named.t -> unit -val add_section_kn : Decl_kinds.polymorphic -> +val add_section_kn : polymorphic:bool -> Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list |