From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- kernel/declarations.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19c..9536407d38 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -190,6 +190,8 @@ type mutual_inductive_body = { mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- kernel/declarations.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9536407d38..1bb1e885f2 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,9 +188,7 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) - mind_universes : Univ.universe_context; (** Local universe variables and constraints *) - - mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- kernel/declarations.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1bb1e885f2..ae47324560 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,6 +188,8 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) + mind_cumulative : bool; (** Is it cumulative or not *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- kernel/declarations.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ae47324560..f3b7ae2b24 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -64,7 +64,9 @@ type constant_def = | Def of constr Mod_subst.substituted (** or a transparent global definition *) | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) -type constant_universes = Univ.universe_context +type constant_universes = + | Monomorphic_const of Univ.universe_context + | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -83,7 +85,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -168,6 +169,11 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } +type abstrac_inductive_universes = + | Monomorphic_ind of Univ.universe_context + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) @@ -186,11 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_polymorphic : bool; (** Is it polymorphic or not *) - - mind_cumulative : bool; (** Is it cumulative or not *) - - mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) + mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -- cgit v1.2.3 From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 14 Jun 2017 16:32:47 +0200 Subject: A short cleanup --- kernel/declarations.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f3b7ae2b24..21651b3e21 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -169,7 +169,7 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } -type abstrac_inductive_universes = +type abstract_inductive_universes = | Monomorphic_ind of Univ.universe_context | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info @@ -192,7 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -- cgit v1.2.3