lem homs and type headers

1 files changed, 44 insertions, 44 deletions

diff --git a/language/l2.ml b/language/l2.ml
index 1ee2b64e..02b5276a 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -40,7 +40,7 @@ kind_aux =  (* kinds *)
 
 
 type 
-nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
+nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
    Nexp_var of kid (* variable *)
  | Nexp_constant of int (* constant *)
  | Nexp_times of nexp * nexp (* product *)
@@ -57,30 +57,6 @@ kind =
 
 
 type 
-n_constraint_aux =  (* constraint over kind $_$ *)
-   NC_fixed of nexp * nexp
- | NC_bounded_ge of nexp * nexp
- | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of kid * (int) list
-
-
-type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
-
-
-type 
-n_constraint = 
-   NC_aux of n_constraint_aux * l
-
-
-type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
 base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
@@ -92,29 +68,18 @@ base_effect_aux =  (* effect *)
 
 
 type 
-quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
-   QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of n_constraint (* A constraint for this type *)
-
-
-type 
 base_effect = 
    BE_aux of base_effect_aux * l
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * l
-
-
-type 
-effect_aux =  (* effect set, of kind $_$ *)
+effect_aux =  (* effect set, of kind Effects *)
    Effect_var of kid
  | Effect_set of (base_effect) list (* effect set *)
 
 
 type 
-order_aux =  (* vector order specifications, of kind $_$ *)
+order_aux =  (* vector order specifications, of kind Order *)
    Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
@@ -127,12 +92,6 @@ id_aux =  (* Identifier *)
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type 
 effect = 
    Effect_aux of effect_aux * l
 
@@ -148,6 +107,47 @@ id =
 
 
 type 
+n_constraint_aux =  (* constraint over kind $_$ *)
+   NC_fixed of nexp * nexp
+ | NC_bounded_ge of nexp * nexp
+ | NC_bounded_le of nexp * nexp
+ | NC_nat_set_bounded of kid * (int) list
+
+
+type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type 
+n_constraint = 
+   NC_aux of n_constraint_aux * l
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of n_constraint (* A constraint for this type *)
+
+
+type 
+quant_item = 
+   QI_aux of quant_item_aux * l
+
+
+type 
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)