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 --- API/API.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index 69278e7c9f..e2c43dab82 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1094,6 +1094,7 @@ sig mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; mind_universes : Univ.UContext.t; + mind_subtyping : Univ.universe_context; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- 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. --- API/API.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index e2c43dab82..cea879ba3c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -86,6 +86,8 @@ sig type universe_context = UContext.t [@@ocaml.deprecated "alias of API.Names.UContext.t"] + type universe_info_ind = Univ.UInfoInd.t + module LSet : module type of struct include Univ.LSet end module ContextSet : sig @@ -1093,8 +1095,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; - mind_universes : Univ.UContext.t; - mind_subtyping : Univ.universe_context; + mind_universes : Univ.universe_info_ind; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3 From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- API/API.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index cea879ba3c..a4ae6347c0 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1124,6 +1124,11 @@ sig | SFBmodtype of module_type_body end +module Univops : sig + val universes_of_constr : Term.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t +end + module Environ : sig type env = Prelude.env @@ -2651,8 +2656,6 @@ sig val new_Type : Names.DirPath.t -> Term.types val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr - val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t -- 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 --- API/API.mli | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index a4ae6347c0..a993b0277c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1095,6 +1095,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; + mind_cumulative : bool; mind_universes : Univ.universe_info_ind; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; @@ -1907,6 +1908,7 @@ end module Decl_kinds : sig type polymorphic = bool + type cumulative_inductive_flag = bool type recursivity_kind = Decl_kinds.recursivity_kind = | Finite | CoFinite @@ -2388,7 +2390,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of @@ -4743,7 +4745,9 @@ sig type one_inductive_impls = Command.one_inductive_impls val do_mutual_inductive : - (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> + (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> @@ -4767,7 +4771,9 @@ sig structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list val interp_mutual_inductive : - structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic -> + structured_inductive_expr -> Vernacexpr.decl_notation list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list -- 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 --- API/API.mli | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index a993b0277c..ecce22c1de 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,9 +84,11 @@ sig end type universe_context = UContext.t - [@@ocaml.deprecated "alias of API.Names.UContext.t"] + [@@ocaml.deprecated "alias of API.Univ.UContext.t"] - type universe_info_ind = Univ.UInfoInd.t + type abstract_universe_context = Univ.AUContext.t + type cumulativity_info = Univ.CumulativityInfo.t + type abstract_cumulativity_info = Univ.ACumulativityInfo.t module LSet : module type of struct include Univ.LSet end module ContextSet : @@ -1047,12 +1049,12 @@ sig proj_body : Term.constr; } type typing_flags = Declarations.typing_flags + type constant_body = Declarations.constant_body = { const_hyps : Context.Named.t; const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -1085,6 +1087,13 @@ sig | MEident of Names.ModPath.t | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration + + type abstrac_inductive_universes = Declarations.abstrac_inductive_universes = + | Monomorphic_ind of Univ.UContext.t + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + + type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1094,9 +1103,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_polymorphic : bool; - mind_cumulative : bool; - mind_universes : Univ.universe_info_ind; + mind_universes : abstrac_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- 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 --- API/API.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index ecce22c1de..899bafa1fd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1088,12 +1088,11 @@ sig | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration - type abstrac_inductive_universes = Declarations.abstrac_inductive_universes = + type abstract_inductive_universes = Declarations.abstract_inductive_universes = | Monomorphic_ind of Univ.UContext.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info - type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1103,7 +1102,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_universes : abstrac_inductive_universes; + mind_universes : Declarations.abstract_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3