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

5 files changed, 166 insertions, 190 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
 
diff --git a/language/l2.ml b/language/l2.ml
index 786d04ab..c5cfd00b 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -20,14 +20,19 @@ base_kind_aux =  (* base kind *)
 
 
 type 
+base_kind = 
+   BK_aux of base_kind_aux * l
+
+
+type 
 id_aux =  (* Identifier *)
    Id of x
  | DeIid of x (* remove infix status *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
@@ -36,8 +41,8 @@ id =
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
+kind = 
+   K_aux of kind_aux * l
 
 
 type 
@@ -53,8 +58,9 @@ and nexp =
 
 
 type 
-kind = 
-   K_aux of kind_aux * l
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
 
 
 type 
@@ -66,22 +72,6 @@ nexp_constraint_aux =  (* constraint over kind $_$ *)
 
 
 type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
-
-
-type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -93,9 +83,13 @@ efct_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 nexp_constraint (* A constraint for this type *)
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
 
 
 type 
@@ -104,8 +98,9 @@ efct =
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * l
+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 nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -122,9 +117,8 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+quant_item = 
+   QI_aux of quant_item_aux * l
 
 
 type 
@@ -138,22 +132,9 @@ order =
 
 
 type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type 
-typquant = 
-   TypQ_aux of typquant_aux * l
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
@@ -178,8 +159,22 @@ and typ_arg =
 
 
 type 
-lit = 
-   L_aux of lit_aux * l
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
 
 
 type 
@@ -188,6 +183,16 @@ typschm_aux =  (* type scheme *)
 
 
 type 
+lit = 
+   L_aux of lit_aux * l
+
+
+type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -213,11 +218,6 @@ and 'a fpat =
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
-
-
-type 
 'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -283,14 +283,9 @@ and 'a letbind =
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
@@ -305,19 +300,29 @@ type
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
+
+
+type 
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
@@ -331,28 +336,27 @@ type
 
 
 type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
 type 
@@ -362,12 +366,8 @@ type
 
 
 type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
 
 
 type 
@@ -381,13 +381,13 @@ ne =  (* internal numeric expressions *)
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
@@ -396,8 +396,8 @@ type
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
@@ -427,8 +427,8 @@ type
 
 
 type 
-'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
+'a def = 
+   DEF_aux of 'a def_aux * 'a annot
 
 
 type 
@@ -450,13 +450,8 @@ type
 
 
 type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
-
-
-type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
+'a defs =  (* Definition sequence *)
+   Defs of ('a def) list
 
 
 type 
@@ -464,9 +459,4 @@ type
    Typ_lib_aux of 'a typ_lib_aux * l
 
 
-type 
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
-
-
 
diff --git a/language/l2.ott b/language/l2.ott
index 3b1e95b7..69b2bf9c 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -380,10 +380,10 @@ typschm :: 'TypSchm_' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 grammar
-ctor_def :: 'CT_' ::=
-  {{ com Datatype constructor definition clause }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id : typschm                                       :: :: ct
+%ctor_def :: 'CT_' ::=
+%  {{ com Datatype constructor definition clause }}
+%  {{ aux _ annot }} {{ auxparam 'a }}
+%  | id : typschm                                       :: :: ct
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that
 
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index b12651c0..703fc49e 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -248,26 +248,26 @@ naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for va
 
 
 type 
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of typquant * atyp
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of atyp
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
+effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of atyp
 
 
 type 
@@ -286,28 +286,29 @@ naming_scheme_opt =
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
-funcl = 
-   FCL_aux of funcl_aux * l
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -320,9 +321,8 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
@@ -331,8 +331,8 @@ fundef_aux =  (* Function definition *)
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
@@ -341,8 +341,8 @@ type_def =
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
@@ -371,11 +371,6 @@ def =
 
 
 type 
-ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
-type 
 typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -410,11 +405,6 @@ defs =  (* Definition sequence *)
 
 
 type 
-ctor_def = 
-   CT_aux of ctor_def_aux * l
-
-
-type 
 typ_lib = 
    Typ_lib_aux of typ_lib_aux * l
 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index ab8d5d80..1da173e1 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -276,10 +276,10 @@ typschm :: 'TypSchm_' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 grammar
-ctor_def :: 'CT_' ::=
-  {{ com Datatype constructor definition clause }}
-  {{ aux _ l }}
-  | id : typschm                                       :: :: ct
+%ctor_def :: 'CT_' ::=
+%  {{ com Datatype constructor definition clause }}
+%  {{ aux _ l }}
+%  | id : typschm                                       :: :: ct
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that