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/constr.mli | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
(limited to 'kernel/constr.mli')
diff --git a/kernel/constr.mli b/kernel/constr.mli
index e6a3e71f89..5a370d31d8 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -205,19 +205,19 @@ val equal : constr -> constr -> bool
(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
application grouping and the universe equalities in [u]. *)
-val eq_constr_univs : constr Univ.check_function
+val eq_constr_univs : constr UGraph.check_function
(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs : constr Univ.check_function
+val leq_constr_univs : constr UGraph.check_function
(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
application grouping and the universe equalities in [u]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and ignoring universe instances. *)
--
cgit v1.2.3
From 98065338c54717fd2d7aa887e8693acdc1cff5ba Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 12:33:58 +0100
Subject: COMMENTS: added to some variants of the "Constr.kind_of_term" type.
---
kernel/constr.mli | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
(limited to 'kernel/constr.mli')
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 5a370d31d8..70f1699314 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -93,8 +93,9 @@ val mkLambda : Name.t * types * constr -> constr
(** Constructs the product [let x = t1 : t2 in t3] *)
val mkLetIn : Name.t * constr * types * constr -> constr
-(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
- {% $(f~t_1~\dots~t_n)$ %}. *)
+(** [mkApp (f, [|t1; ...; tN|]] constructs the application
+ {%html:(f t1 ... tn)%}
+ {%latex:$(f~t_1\dots f_n)$%}. *)
val mkApp : constr * constr array -> constr
val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
@@ -181,10 +182,13 @@ type ('constr, 'types) kind_of_term =
| Evar of 'constr pexistential
| Sort of Sorts.t
| Cast of 'constr * cast_kind * 'types
- | Prod of Name.t * 'types * 'types
- | Lambda of Name.t * 'types * 'constr
- | LetIn of Name.t * 'constr * 'types * 'constr
- | App of 'constr * 'constr array
+ | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *)
+ | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *)
+ | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *)
+ | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])].
+ The {!mkApp} constructor also enforces the following invariant:
+ - [F] itself is not {!App}
+ - and [[|P1;..;Pn|]] is not empty. *)
| Const of constant puniverses
| Ind of inductive puniverses
| Construct of constructor puniverses
--
cgit v1.2.3
From b88929d9d8de179a7e356cf9cbe2afef76f905a3 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 18 Dec 2015 10:07:53 +0100
Subject: COMMENTS: added to the "Constr.case_info" type.
---
kernel/constr.mli | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
(limited to 'kernel/constr.mli')
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 70f1699314..edd4eb2310 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -32,11 +32,15 @@ type case_printing =
(** the integer is the number of real args, needed for reduction *)
type case_info =
- { ci_ind : inductive;
- ci_npar : int;
- ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
- ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
- ci_pp_info : case_printing (** not interpreted by the kernel *)
+ { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *)
+ ci_npar : int; (* number of parameters of the above inductive type *)
+ ci_cstr_ndecls : int array; (* number of arguments of individual constructors
+ (numbers of parameters of the inductive type are excluded from the count)
+ (with let's) *)
+ ci_cstr_nargs : int array; (* number of arguments of individual constructors
+ (numbers of parameters of the inductive type are excluded from the count)
+ (w/o let's) *)
+ ci_pp_info : case_printing (* not interpreted by the kernel *)
}
(** {6 The type of constructions } *)
--
cgit v1.2.3
From f8eb2ed4ddbe2199187696f51c42734014f4d9d0 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 21 Dec 2015 13:32:57 +0100
Subject: COMMENTS: of "Constr.case_info" type were updated.
---
kernel/constr.mli | 20 +++++++++++++-------
1 file changed, 13 insertions(+), 7 deletions(-)
(limited to 'kernel/constr.mli')
diff --git a/kernel/constr.mli b/kernel/constr.mli
index edd4eb2310..ada2686063 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -30,16 +30,22 @@ type case_printing =
cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
style : case_style }
-(** the integer is the number of real args, needed for reduction *)
+(* INVARIANT:
+ * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs
+ * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)),
+ * ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i)
+ *)
type case_info =
{ ci_ind : inductive; (* inductive type to which belongs the value that is being matched *)
ci_npar : int; (* number of parameters of the above inductive type *)
- ci_cstr_ndecls : int array; (* number of arguments of individual constructors
- (numbers of parameters of the inductive type are excluded from the count)
- (with let's) *)
- ci_cstr_nargs : int array; (* number of arguments of individual constructors
- (numbers of parameters of the inductive type are excluded from the count)
- (w/o let's) *)
+ ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines
+ the number of values that can be bound in a match-construct.
+ NOTE: parameters of the inductive type are therefore excluded from the count *)
+ ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines
+ the number of values that can be applied to the constructor,
+ in addition to the parameters of the related inductive type
+ NOTE: "lets" are therefore excluded from the count
+ NOTE: parameters of the inductive type are also excluded from the count *)
ci_pp_info : case_printing (* not interpreted by the kernel *)
}
--
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/constr.mli | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
(limited to 'kernel/constr.mli')
diff --git a/kernel/constr.mli b/kernel/constr.mli
index e6a3e71f89..c3118cdf7e 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*