From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 May 2019 05:33:10 +0200 Subject: [proof] Remove duplicated universe polymorphic from decl_kinds This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits. --- library/decl_kinds.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 0e2ef95739..4b20016ab2 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -67,7 +67,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = locality * goal_object_kind (** Kinds used in library *) -- cgit v1.2.3 From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 06:09:24 +0200 Subject: [lemmas] [proof] Split proof kinds into per-layer components. We split `{goal,declaration,assumption}_kind` into their components. This makes sense as each part of this triple is handled by a different layer, namely: - `polymorphic` status: necessary for the lower engine layers; - `locality`: only used in `vernac` top-level constants - `kind`: merely used for cosmetic purposes [could indeed be removed / pushed upwards] We also profit from this refactoring to add some named parameters to the top-level definition API which is quite parameter-hungry. More refactoring is possible and will come in further commits, in particular this is a step towards unifying the definition / lemma save path. --- library/decl_kinds.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 4b20016ab2..9fed8b7829 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -58,17 +58,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind - (** Kinds used in proofs *) type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind - (** Kinds used in library *) type logical_kind = -- cgit v1.2.3 From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 13:21:48 +0200 Subject: [api] Move `locality` from `library` to `vernac`. This datatype does belong to this layer. --- library/decl_kinds.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 9fed8b7829..57612c3735 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -12,10 +12,6 @@ type discharge = DoDischarge | NoDischarge -type import_status = ImportDefaultBehavior | ImportNeedQualified - -type locality = Discharge | Global of import_status - type binding_kind = Explicit | Implicit type polymorphic = bool -- cgit v1.2.3 From 9d65c49f05f946557df4c67b6e752f978e1e9352 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 15:10:50 +0200 Subject: [api] Remove `polymorphic` type alias, use labels instead. This is more in-line with attributes and the rest of the API, and makes some code significantly clearer (as in `foo true false false`, etc...) --- library/decl_kinds.ml | 2 -- library/decls.ml | 2 +- library/decls.mli | 4 ++-- library/lib.ml | 12 ++++++------ library/lib.mli | 8 +++----- 5 files changed, 12 insertions(+), 16 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 57612c3735..2735a9118e 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -14,8 +14,6 @@ type discharge = DoDischarge | NoDischarge type binding_kind = Explicit | Implicit -type polymorphic = bool - type private_flag = bool type cumulative_inductive_flag = bool diff --git a/library/decls.ml b/library/decls.ml index ef60a44ac7..104eb37011 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -18,7 +18,7 @@ open Libnames (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind + DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" diff --git a/library/decls.mli b/library/decls.mli index 0d09499b51..93298c0bc4 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -19,7 +19,7 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind + DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t @@ -27,7 +27,7 @@ val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool val variable_context : variable -> Univ.ContextSet.t -val variable_polymorphic : variable -> polymorphic +val variable_polymorphic : variable -> bool val variable_exists : variable -> bool (** Registration and access to the table of constants *) diff --git a/library/lib.ml b/library/lib.ml index ae657dbd70..e4054d58cc 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -411,8 +411,8 @@ type abstr_info = { type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.ContextSet.t) + | Variable of (Names.Id.t * Decl_kinds.binding_kind * bool * Univ.ContextSet.t) + (** (name, kind, poly, univs) *) | Context of Univ.ContextSet.t let sectab = @@ -428,12 +428,12 @@ let check_same_poly p vars = if List.exists pred vars then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") -let add_section_variable id impl poly ctx = +let add_section_variable ~name ~kind ~poly 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 + sectab := (Variable (name,kind,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -509,11 +509,11 @@ let add_section_replacement f g poly hyps = } in sectab := (vars,f (inst,args) exps, g info abs) :: sl -let add_section_kn poly 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 poly -let add_section_constant poly 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 poly diff --git a/library/lib.mli b/library/lib.mli index f6bd61e2da..2cd43b66b3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit -val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Constr.named_context -> unit -val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Constr.named_context -> unit +val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit +val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list val is_polymorphic_univ : Univ.Level.t -> bool -- cgit v1.2.3 From da5bbda84bd22b87a6057175c9d4d2391808e294 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 17:28:26 +0200 Subject: [api] [proof] Move `discharge` type to vernac_ast where it is used. This seems like the right location, a bit more refactoring should be possible. --- library/decl_kinds.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 2735a9118e..6eb582baef 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -10,8 +10,6 @@ (** Informal mathematical status of declarations *) -type discharge = DoDischarge | NoDischarge - type binding_kind = Explicit | Implicit type private_flag = bool -- cgit v1.2.3 From 5f190f9e12f42a0ff6b5275c8087852a87aff47b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 21 Jun 2019 13:55:03 +0200 Subject: Use named records instead of tuples where `polymorphic` used to be. Followup on "[api] Remove `polymorphic` type alias, use labels instead." --- library/decls.ml | 19 ++++++++++++------- library/decls.mli | 9 +++++++-- library/lib.ml | 26 +++++++++++++++----------- 3 files changed, 34 insertions(+), 20 deletions(-) (limited to 'library') diff --git a/library/decls.ml b/library/decls.ml index 104eb37011..5cb35323dd 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -17,19 +17,24 @@ open Libnames (** Datas associated to section variables and local definitions *) -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind +type variable_data = { + path:DirPath.t; + opaque:bool; + univs:Univ.ContextSet.t; + poly: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 = let {path} = Id.Map.find id !vartab in path +let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque +let variable_kind id = let {kind} = Id.Map.find id !vartab in kind +let variable_context id = let {univs} = Id.Map.find id !vartab in univs +let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly 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 93298c0bc4..f88958bb04 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -18,8 +18,13 @@ open Decl_kinds (** Registration and access to the table of variable *) -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind +type variable_data = { + path:DirPath.t; + opaque:bool; + univs:Univ.ContextSet.t; + poly:bool; + kind:logical_kind; +} val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t diff --git a/library/lib.ml b/library/lib.ml index e4054d58cc..3eb74808e4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -411,8 +411,12 @@ type abstr_info = { type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * bool * Univ.ContextSet.t) - (** (name, kind, poly, univs) *) + | Variable of { + id:Names.Id.t; + kind:Decl_kinds.binding_kind; + poly:bool; + univs:Univ.ContextSet.t; + } | Context of Univ.ContextSet.t let sectab = @@ -424,16 +428,16 @@ let add_section () = (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab let check_same_poly p vars = - let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + let pred = function Context _ -> p = false | Variable {poly} -> p != poly in if List.exists pred vars then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") -let add_section_variable ~name ~kind ~poly ctx = +let add_section_variable ~name ~kind ~poly univs = 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 (name,kind,poly,ctx)::vars,repl,abs)::sl + sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -448,7 +452,7 @@ let is_polymorphic_univ u = let open Univ in List.iter (fun (vars,_,_) -> List.iter (function - | Variable (_,_,poly,(univs,_)) -> + | Variable {poly;univs=(univs,_)} -> if LSet.mem u univs then raise (PolyFound poly) | Context (univs,_) -> if LSet.mem u univs then raise (PolyFound true) @@ -459,12 +463,12 @@ let is_polymorphic_univ u = let extract_hyps (secs,ohyps) = let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r - | (Variable (_,_,poly,ctx)::idl,hyps) -> + (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r + | (Variable {poly;univs}::idl,hyps) -> let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r ctx else r + l, if poly then Univ.ContextSet.union r univs else r | (Context ctx :: idl, hyps) -> let l, r = aux (idl, hyps) in l, Univ.ContextSet.union r ctx @@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr = let section_instance = function | VarRef id -> let eq = function - | Variable (id',_,_,_) -> Names.Id.equal id id' + | Variable {id=id'} -> Names.Id.equal id id' | Context _ -> false in if List.exists eq (pi1 (List.hd !sectab)) -- cgit v1.2.3