diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-21 13:32:57 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 10:00:45 +0100 |
commit | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (patch) | |
tree | 01fcd6c92e5f1227b756bb624a8377b8d045ac1f | |
parent | 8a4a8758075e09da298762da1a035a5afac4d88b (diff) |
COMMENTS: of "Constr.case_info" type were updated.
-rw-r--r-- | kernel/constr.ml | 20 | ||||
-rw-r--r-- | kernel/constr.mli | 20 |
2 files changed, 27 insertions, 13 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c3aebada2..3e7d888ed 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -41,15 +41,23 @@ type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *) style : case_style } + +(* 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 *) } diff --git a/kernel/constr.mli b/kernel/constr.mli index edd4eb231..ada268606 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 *) } |