Syntax changes per discussion with Peter, as well as L2.ott document clean up.

Could not at this time return lists to [| |] from [|| ||] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [|3|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.

1 files changed, 74 insertions, 89 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 177f73cc..8e56f69e 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -22,73 +22,70 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
+type kid =  (* variables with kind, ticked to differntiate from program variables *)
+ | Var of x
+
+
 type base_kind =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
  | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
-type var =  (* variables with kind, ticked to differntiate from program variables *)
- | Var of x
-
-
-type kind =  (* kinds *)
- | K_kind of list base_kind
+ | BK_effect (* kind of effect sets *)
 
 
 type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
- | Nexp_id of id (* identifier *)
- | Nexp_var of var (* variable *)
+ | Nexp_var of kid (* variable *)
  | Nexp_constant of nat (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_exp of nexp (* exponential *)
 
 
-type efct =  (* effect *)
- | Effect_rreg (* read register *)
- | Effect_wreg (* write register *)
- | Effect_rmem (* read memory *)
- | Effect_wmem (* write memory *)
- | Effect_undef (* undefined-instruction exception *)
- | Effect_unspec (* unspecified values *)
- | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
+type kind =  (* kinds *)
+ | K_kind of list base_kind
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of var (* identifier *)
- | KOpt_kind of kind * var (* kind-annotated variable *)
+type base_effect =  (* effect *)
+ | BE_rreg (* read register *)
+ | BE_wreg (* write register *)
+ | BE_rmem (* read memory *)
+ | BE_wmem (* write memory *)
+ | BE_undef (* undefined-instruction exception *)
+ | BE_unspec (* unspecified values *)
+ | BE_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
-type nexp_constraint =  (* constraint over kind $Nat$ *)
+type n_constraint =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of id * list nat
+ | NC_nat_set_bounded of kid * list nat
+
+
+type kinded_id =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
 type order =  (* vector order specifications, of kind $Order$ *)
- | Ord_id of id (* identifier *)
- | Ord_var of var (* variable *)
+ | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type effects =  (* effect set, of kind $Effects$ *)
- | Effects_id of id
- | Effects_var of var
- | Effects_set of list efct (* effect set *)
+type effect =  (* effect set, of kind $Effects$ *)
+ | Effect_var of kid
+ | Effect_set of list base_effect (* effect set *)
+
+
+type id =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
 
 
 type quant_item =  (* 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 *)
+ | QI_const of n_constraint (* A constraint for this type *)
 
 
 type lit =  (* Literal constant *)
@@ -107,8 +104,8 @@ type lit =  (* Literal constant *)
 type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
- | Typ_var of var (* Type variable *)
- | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *)
+ | Typ_var of kid (* Type variable *)
+ | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
  | Typ_tup of list typ (* Tuple type *)
  | Typ_app of id * list typ_arg (* type constructor application *)
 
@@ -116,7 +113,7 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
  | Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
- | Typ_arg_effects of effects
+ | Typ_arg_effect of effect
 
 
 type typquant =  (* type quantifiers and constraints *)
@@ -173,7 +170,7 @@ type exp =  (* Expression *)
 
 and lexp =  (* lvalue expression *)
  | LEXP_id of id (* identifier *)
- | LEXP_memory of id * exp (* memory write via function call *)
+ | LEXP_memory of id * list exp (* memory write via function call *)
  | LEXP_vector of lexp * exp (* vector element *)
  | LEXP_vector_range of lexp * exp * exp (* subvector *)
  | LEXP_field of lexp * id (* struct field *)
@@ -192,15 +189,25 @@ and letbind =  (* Let binding *)
  | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
 
 
-type effects_opt =  (* Optional effect annotation for functions *)
- | Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+type type_union =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
 
 
 type funcl =  (* Function clause *)
  | FCL_Funcl of id * pat * exp
 
 
+type effect_opt =  (* Optional effect annotation for functions *)
+ | Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type name_scm_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
+
+
 type rec_opt =  (* Optional recursive annotation for functions *)
  | Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
@@ -210,42 +217,41 @@ type tannot_opt =  (* Optional type annotation for functions *)
  | Typ_annot_opt_some of typquant * typ
 
 
-type type_union =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
-
-
-type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
-
-
 type index_range =  (* index specification, for bitfields in register types *)
  | BF_single of nat (* single index *)
  | BF_range of nat * nat (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 
-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 * var
- | DT_typ of typschm * id
-
-
 type val_spec =  (* Value type specification *)
  | VS_val_spec of typschm * id
  | VS_extern_no_rename of typschm * id
  | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
 
 
+type scattered_def =  (* Function and type union definitions that can be spread across
+         a file. Each one must end in $id$ *)
+ | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of funcl (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type fundef =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list funcl
+
+
+type default_spec =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * kid
+ | DT_typ of typschm * id
+
+
 type type_def =  (* Type definition body *)
- | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
@@ -254,34 +260,13 @@ type def =  (* Top-level definition *)
  | DEF_fundef of fundef (* function definition *)
  | DEF_val of letbind (* value definition *)
  | DEF_spec of val_spec (* top-level type constraint *)
- | DEF_default of default_typing_spec (* default kind and type assumptions *)
+ | DEF_default of default_spec (* default kind and type assumptions *)
+ | DEF_scattered of scattered_def (* scattered function and type definition *)
  | DEF_reg_dec of typ * id (* register declaration *)
- | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of funcl (* scattered function definition clause *)
- | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *)
- | DEF_scattered_end of id (* scattered definition end *)
 
 
 type defs =  (* Definition sequence *)
  | Defs of list def
 
 
-type typ_lib =  (* library types and syntactic sugar for them *)
- | Typ_lib_unit (* unit type with value $()$ *)
- | Typ_lib_bool (* booleans $true$ and $false$ *)
- | Typ_lib_bit (* pure bit values (not mutable bits) *)
- | Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
- | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
- | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
- | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
- | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *)
- | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *)
- | Typ_lib_list of typ (* list of typ *)
- | Typ_lib_set of typ (* finite set of typ *)
- | Typ_lib_reg of typ (* mutable register components holding typ *)
-
-