aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar SimonBoulier <simon.boulier@ens-rennes.fr>2018-05-30 11:33:37 +0200
committerGravatar SimonBoulier <simon.boulier@ens-rennes.fr>2018-06-05 15:54:12 +0200
commitb0dee52bfa97405adc7c0dbffa0f3558f349659e (patch)
tree673c1cbbb05521972da10945d184c1585dd3f8b4 /kernel
parent00a01f65be79bef8592928941646750968dbe648 (diff)
Define rec_declaration in terms of prec_declaration.
And similarly for fixpoint and cofixpoint.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml16
-rw-r--r--kernel/constr.mli30
2 files changed, 25 insertions, 21 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c11b9ebf4..418229330 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term
type constr = t
type existential = existential_key * constr array
-type rec_declaration = Name.t array * constr array * constr array
-type fixpoint = (int array * int) * rec_declaration
- (* The array of [int]'s tells for each component of the array of
- mutual fixpoints the number of lambdas to skip before finding the
- recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
- (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
- the recursive argument);
- The second component [int] tells which component of the block is
- returned *)
-type cofixpoint = int * rec_declaration
- (* The component [int] tells which component of the block of
- cofixpoint is returned *)
type types = constr
+type rec_declaration = (constr, types) prec_declaration
+type fixpoint = (constr, types) pfixpoint
+type cofixpoint = (constr, types) pcofixpoint
+
(*********************)
(* Term constructors *)
(*********************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 742a13919..bf7b5e87b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr
where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
+type ('constr, 'types) prec_declaration =
+ Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+ (int array * int) * ('constr, 'types) prec_declaration
+ (* The array of [int]'s tells for each component of the array of
+ mutual fixpoints the number of lambdas to skip before finding the
+ recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+ (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+ the recursive argument);
+ The second component [int] tells which component of the block is
+ returned *)
+
+type ('constr, 'types) pcofixpoint =
+ int * ('constr, 'types) prec_declaration
+ (* The component [int] tells which component of the block of
+ cofixpoint is returned *)
+
+type rec_declaration = (constr, types) prec_declaration
+
+type fixpoint = (constr, types) pfixpoint
val mkFix : fixpoint -> constr
(** If [funnames = [|f1,.....fn|]]
@@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr
...
with fn = bn.]
*)
-type cofixpoint = int * rec_declaration
+type cofixpoint = (constr, types) pcofixpoint
val mkCoFix : cofixpoint -> constr
@@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr
(** [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
type 'constr pexistential = Evar.t * 'constr array
-type ('constr, 'types) prec_declaration =
- Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
- (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
- int * ('constr, 'types) prec_declaration
type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)