Supporting all expressions, although vector cacentation pattern matching can only match simple patterns (until type information is available).

1 files changed, 33 insertions, 37 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 20d5c7b7..51bad620 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -108,11 +108,6 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
  | Typ_arg_effects of effects
 
 
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
 type lit =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
@@ -126,8 +121,9 @@ type lit =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
+type typquant =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type pat =  (* Pattern *)
@@ -148,6 +144,10 @@ and fpat =  (* Field pattern *)
  | FP_Fpat of id * pat
 
 
+type typschm =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
 type ne =  (* internal numeric expressions *)
  | Ne_var of id
  | Ne_const of num
@@ -157,11 +157,7 @@ type ne =  (* internal numeric expressions *)
  | Ne_unary of ne
 
 
-type letbind =  (* Let binding *)
- | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
-
-and exp =  (* Expression *)
+type exp =  (* Expression *)
  | E_block of list exp (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
@@ -202,6 +198,10 @@ and fexps =  (* Field-expression list *)
 and pexp =  (* Pattern match *)
  | Pat_exp of pat * exp
 
+and letbind =  (* Let binding *)
+ | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
 
 type k =  (* Internal kinds *)
  | Ki_typ
@@ -213,15 +213,13 @@ type k =  (* Internal kinds *)
  | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
-type index_range =  (* index specification, for bitfields in register types *)
- | BF_single of num (* single index *)
- | BF_range of num * num (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
+type tannot_opt =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
 
 
-type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
+type effects_opt =  (* Optional effect annotation for functions *)
+ | Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
 
 
 type rec_opt =  (* Optional recursive annotation for functions *)
@@ -229,26 +227,23 @@ type rec_opt =  (* Optional recursive annotation for functions *)
  | Rec_rec (* recursive *)
 
 
-type effects_opt =  (* Optional effect annotation for functions *)
- | Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
-
-
 type funcl =  (* Function clause *)
  | FCL_Funcl of id * pat * exp
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type index_range =  (* index specification, for bitfields in register types *)
+ | BF_single of num (* single index *)
+ | BF_range of num * num (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 
-type default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
+type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
 
 
-type val_spec =  (* Value type specification *)
- | VS_val_spec of typschm * id
+type fundef =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
 
 
 type type_def =  (* Type definition body *)
@@ -259,8 +254,13 @@ type type_def =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type fundef =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
+type default_typing_spec =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * id
+ | DT_typ of typschm * id
+
+
+type val_spec =  (* Value type specification *)
+ | VS_val_spec of typschm * id
 
 
 type def =  (* Top-level definition *)
@@ -294,10 +294,6 @@ type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_reg of typ (* mutable register components holding typ *)
 
 
-type ctor_def =  (* Datatype constructor definition clause *)
- | CT_ct of id * typschm
-
-
 type defs =  (* Definition sequence *)
  | Defs of list def