From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/reduction.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6ced5c4985..a22f3730e9 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -30,7 +30,7 @@ exception NotConvertibleVect of int type 'a conversion_function = env -> 'a -> 'a -> unit type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit +type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function @@ -47,10 +47,10 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit + env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit (* val sort_cmp : *) (* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) -- cgit v1.2.3 From 0f74b3df6e64dc069e53c4afcd6f46129b211d09 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 14 Oct 2015 13:50:55 +0200 Subject: Remove reference to default conversion function inside the kernel. --- kernel/reduction.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6ced5c4985..90c008b19d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -93,7 +93,6 @@ val set_nat_conv : (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function -val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function -- cgit v1.2.3 From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Oct 2015 18:06:55 +0200 Subject: Fix #4346 1/2: native casts were not inferring universe constraints. --- kernel/reduction.mli | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 90c008b19d..b71356d033 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -49,14 +49,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints -val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit +val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> + 'a * 'a universe_compare -> 'a * 'a universe_compare -(* val sort_cmp : *) -(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) - -(* val conv_sort : sorts conversion_function *) -(* val conv_sort_leq : sorts conversion_function *) +val checked_universes : Univ.universes universe_compare +val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -77,22 +74,20 @@ val conv_leq : val conv_leq_vecti : ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +(** These conversion functions are used by module subtyping, which needs to infer + universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function -val generic_conv : conv_pb -> bool -> (existential->constr option) -> +val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_nat_conv : - (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit -val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function -- cgit v1.2.3 From d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Oct 2015 13:20:19 +0200 Subject: Remove left2right reference from the kernel. Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable. --- kernel/reduction.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b71356d033..c3cc7b2b69 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -10,8 +10,6 @@ open Term open Context open Environ -val left2right : bool ref - (*********************************************************************** s Reduction functions *) -- cgit v1.2.3 From 90dfacaacfec8265b11dc9291de9510f515c0081 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Oct 2015 23:59:05 +0100 Subject: Conversion of polymorphic inductive types was incomplete in VM and native. Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with a polymorphic prod. --- kernel/reduction.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c3cc7b2b69..0df26d6276 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool (* Instance of a flexible constant? *) -> + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(* [flex] should be true for constants, false for inductive types and +constructors. *) +val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> + 'a * 'a universe_compare -> 'a * 'a universe_compare + val checked_universes : Univ.universes universe_compare val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare -- cgit v1.2.3 From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:11:39 +0100 Subject: Unifying betazeta_applist and prod_applist into a clearer interface. - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. --- kernel/reduction.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ef764f34f9..7db7e57bb5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -96,15 +96,20 @@ val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) +(** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + (** Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(** Builds an application node, reducing the [n] first beta-zeta redexes. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -- cgit v1.2.3 From 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 9 Dec 2015 12:30:32 +0100 Subject: CLEANUP: in the Reduction module --- kernel/reduction.mli | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7db7e57bb5..304046a1dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -27,7 +27,7 @@ exception NotConvertible exception NotConvertibleVect of int type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function +type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function @@ -58,25 +58,14 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare -val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function -val trans_conv : +val conv : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function -val trans_conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val trans_conv_universes : +val conv_universes : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val trans_conv_leq_universes : +val conv_leq_universes : ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function -val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function -val conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function -val conv_leq_vecti : - ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function - (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> -- cgit v1.2.3 From 672f8ee0c96584735294641bb4b8760e25197b80 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 14 Dec 2015 12:52:49 +0100 Subject: CLEANUP: in the Reduction module --- kernel/reduction.mli | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 304046a1dc..f7a8d88c27 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -26,11 +26,11 @@ val nf_betaiota : env -> constr -> constr exception NotConvertible exception NotConvertibleVect of int -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function +type 'a kernel_conversion_function = env -> 'a -> 'a -> unit +type 'a extended_conversion_function = + ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit type conv_pb = CONV | CUMUL @@ -58,13 +58,9 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function +val conv : constr extended_conversion_function -val conv_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val conv_leq_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function +val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) @@ -77,11 +73,11 @@ val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) -val set_vm_conv : (conv_pb -> types conversion_function) -> unit -val vm_conv : conv_pb -> types conversion_function +val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit +val vm_conv : conv_pb -> types kernel_conversion_function -val default_conv : conv_pb -> ?l2r:bool -> types conversion_function -val default_conv_leq : ?l2r:bool -> types conversion_function +val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function +val default_conv_leq : ?l2r:bool -> types kernel_conversion_function (************************************************************************) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/reduction.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index f7a8d88c27..35daff7b59 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Environ (*********************************************************************** @@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> rel_context * types -val dest_prod_assum : env -> types -> rel_context * types -val dest_lam_assum : env -> types -> rel_context * types +val dest_prod : env -> types -> Context.Rel.t * types +val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/reduction.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0df26d6276..9a83ca7098 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*