gkp

2 files changed, 226 insertions, 228 deletions

diff --git a/language/l2.ott b/language/l2.ott
index d1bf5793..031cfb5a 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -291,7 +291,7 @@ base_kind :: 'BK_' ::=
   | Endian                                     :: :: endian
   | Effects                                    :: :: effects
 
-kind :: '' ::=  
+kind :: 'K_' ::=  
   {{ com kinds}}
   {{ aux _ l }}
   | base_kind1 -> ... -> base_kindn            :: :: kind
@@ -305,7 +305,7 @@ nexp :: 'Nexp_' ::=
   | num                                 :: :: constant
   | nexp1 * nexp2                       :: :: times {{ com must be linear after normalisation... except for the type of *, ahem }}
   | nexp1 + nexp2                       :: :: sum
-  | 2 ^ nexp                            :: :: exp
+  | 2 ** nexp                            :: :: exp
   | ( nexp )                            :: S :: paren  {{ icho [[nexp]] }}
 
 endian :: 'End_' ::=  
@@ -380,11 +380,11 @@ typ_sugar :: 'Typ_sugar_' ::=
   | [ nexp '..' nexp' ]  :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
 % use .. not - to avoid ambiguity with nexp -
 % total maps and vectors indexed by finite subranges of nat
-  | enummap nexp1 nexp2 endian typ :: :: enummap 
-% probably some sugar for enummap types, using [ ] similarly to enums:
+  | vector nexp1 nexp2 endian typ :: :: vector 
+% probably some sugar for vector types, using [ ] similarly to enums:
 % (but with .. not : in the former, to avoid confusion...)
-  | typ [ nexp ]  :: :: enummap2
-  | typ [ nexp : nexp' ] :: :: enummap3
+  | typ [ nexp ]  :: :: vector2
+  | typ [ nexp : nexp' ] :: :: vector3
 % ...so bit [ nexp ] etc is just an instance of that
   | list typ :: :: list
   | set typ  :: :: set
@@ -414,27 +414,25 @@ nexp_constraint :: 'NC_' ::=
 % Note only id on the left and constants on the right in a
 % finite-set-bound, as we don't think we need anything more
 
-opt_kind :: 'ki_ant_' ::=
+kinded_id :: 'KOpt_' ::=
   {{ com optionally kind-annotated identifier }}
   | id	 	    		   	      :: :: none
-  | id : kind				      :: :: kind
-  | ( opt_kind ) 			      :: S :: paren {{ icho [[opt_kind]] }}
+  | kind id				      :: :: kind
+  | ( kinded_id ) 			      :: S :: paren {{ icho [[kinded_id]] }}
 
-typquant :: 'TQ_' ::= 
+typquant :: 'TypQ_' ::= 
   {{ aux _ l }}
-  | forall opt_kind1 ... opt_kindn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }}
-
-% TODO those ids have to have optional kind annotations
+  | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }}
 
 % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
 
-  | forall opt_kind1 ... opt_kindn . ::  ::  Ts_no_constraint {{ com sugar }}
-  |                           ::  ::  Ts_no_forall     {{ com sugar }}
+  | forall kinded_id1 ... kinded_idn . ::  ::  no_constraint {{ com sugar }}
+  |                           ::  ::  no_forall     {{ com sugar }}
 
-typschm :: 'TS_' ::=
+typschm :: 'TypSchm_' ::=
     {{ com Type schemes  }}
   {{ aux _ l }}
-  |  typquant typ                                                       :: :: Ts
+  |  typquant typ                                                       :: :: ts
 
 
 
@@ -443,43 +441,43 @@ typschm :: 'TS_' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 grammar
-ctor_def :: '' ::=
+ctor_def :: 'CT_' ::=
   {{ com Datatype definition clauses }}
-  | id : typschm                                       :: :: Cte
+  | id : typschm                                       :: :: ct
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that
 
-enum_opt :: 'Enum_' ::=
+enum_opt :: 'EnumOpt_' ::=
   |      :: :: empty
   | enum :: :: enum
 
-tdefbody :: 'Te_' ::=
-  {{ com Type definition bodies }}
-  | typschm                                                     :: :: abbrev
-    {{ com Type abbreviations }}
-  | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
-    {{ com Record types }}
-  | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
-    {{ com Variant types }}
-
-naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::=
-  {{ com Optional variable-naming-scheme specification for variables of defined type }} 
-  |                                                   :: :: none
-  | [ name = regexp ]                                 :: :: some
-
-type_def :: '' ::=
-  {{ com Type definitions }}
-  | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
-%  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
-% the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
-
+%% tdefbody :: 'TD_' ::=
+%%   {{ com Type definition bodies }}
+%%   | typschm                                                     :: :: abbrev
+%%     {{ com Type abbreviations }}
+%%   | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
+%%     {{ com Record types }}
+%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
+%%     {{ com Variant types }}
+%% 
+%% naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::=
+%%   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
+%%   |                                                   :: :: none
+%%   | [ name = regexp ]                                 :: :: some
+%% 
+%% type_def :: '' ::=
+%%   {{ com Type definitions }}
+%%   | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
+%% %  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
+%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
+%% 
 
 % TODO: do we need mutually recursive type definitions?  
 
 
 %%% OR, IN C STYLE
 
-c_tdefbody :: 'C_Te_' ::=
+tdef :: 'TD_' ::=
   {{ com Type definition bodies }}
   | typedef id naming_scheme_opt = typschm                                        :: :: abbrev
     {{ com Type abbreviations }}
@@ -570,8 +568,8 @@ pat :: 'P_' ::=
     {{ com Single variable and constructor patterns }}
 % OR?  do we invent something ghastly including a union keyword?  Perhaps not...
 
-  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
-    {{ com Record patterns }}
+%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
+%    {{ com Record patterns }}
 % OR
   | struct { fpat1 ; ... ; fpatn semi_opt }                  :: :: c_record
     {{ com C-style struct patterns }}
@@ -579,10 +577,14 @@ pat :: 'P_' ::=
 %Patterns for vectors
 %Should these be the same since vector syntax has changed, and lists have also changed?
 
-  | [| pat1 ; .. ; patn semi_opt |]                     :: :: vector
+  | [ pat1 , .. , patn  ]                     :: :: vector
+   {{ com Vector patterns }}
+
+  | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
    {{ com Vector patterns }}
 
-  | [| pat1 .. patn |]                                  :: :: vector_concat
+% cf ntoes for this
+  |  pat1 : .. : patn                                   :: :: vector_concat
   {{ com Concatenated vector patterns }} 
 
   | ( pat1 , .... , patn )                              :: :: tup
@@ -590,10 +592,10 @@ pat :: 'P_' ::=
   | [| pat1 , .. , patn |]	                        :: :: list
     {{ com List patterns }}
   | ( pat )                                             :: :: paren
-  | pat1 '::' pat2                                      :: :: cons
-    {{ com Cons patterns }}
-  | id '+' num                                         :: :: num_add
-    {{ com constant addition patterns }}
+%  | pat1 '::' pat2                                      :: :: cons
+%    {{ com Cons patterns }}
+%  | id '+' num                                         :: :: num_add
+%    {{ com constant addition patterns }}
   | lit                                                 :: :: lit
     {{ com Literal constant patterns }}
 
@@ -640,28 +642,30 @@ exp :: 'E_' ::=
 
 
 
-% enummaps
-  | [ exp1 , ... , expn ]                             :: :: enummap
+% vectors
+  | [ exp1 , ... , expn ]                             :: :: vector
+% endianness comes from global command-line option???
 
-  | [ num1 = exp1 , ... , numn = expn ]               :: :: enummap_e
+  | [ num1 = exp1 , ... , numn = expn ]               :: :: vector_indexed
+% num1 .. numn must be a consecutive list of naturals
 
-% we pick [ ] not { } for enummap literals for consistency with their
+% we pick [ ] not { } for vector literals for consistency with their
 % array-like access syntax, in contrast to the C which has funny
 % syntax for array literals.  We don't have to preserve [ ] for lists
 % as we don't expect to use lists very much. 
 
-  | exp [ exp' ]                                      :: :: enummap_access
-  {{ com enummap access }}
+  | exp [ exp' ]                                      :: :: vector_access
+  {{ com vector access }}
 
-  | exp [ exp1 '..' exp2 ]                            :: :: enummap_subrange
-  {{ com Subenummap extraction }}
+  | exp [ exp1 : exp2 ]                            :: :: vector_subrange
+  {{ com Subvector extraction }}
   % do we want to allow a comma-separated list of such thingies?  
 
-  | [ exp with exp1 = exp2 ]                          :: :: enummap_update 
-  {{ com enummap functional update }}
+  | [ exp with exp1 = exp2 ]                          :: :: vector_update 
+  {{ com vector functional update }}
 
-  | [ exp with exp1 .. exp2 = exp3 ]                          :: :: enummap_update_range
-  {{ com enummap functional subrange update (with another enummap)}}
+  | [ exp with exp1 : exp2 = exp3 ]                          :: :: vector_update_range
+  {{ com vector functional subrange update (with another vector)}}
   % do we want a functional update form with a comma-separated list of such?
 
 
@@ -702,7 +706,7 @@ exp :: 'E_' ::=
     {{ com Pattern matching expressions }}
 %  | ( typ ) exp                                      :: :: Typed
 %    {{ com Type-annotated expressions }}
-  | c_letbind in exp                                  :: :: let
+  | letbind in exp                                  :: :: let
     {{ com Let expressions }}
 
   | lexp := exp                                      :: :: assign
@@ -711,8 +715,8 @@ exp :: 'E_' ::=
 lexp :: 'LEXP_' ::=
     | id                                                  :: :: ident
     {{ com Identifiers }}
-    | lexp [ exp ]  :: ::                         enummap
-    | lexp [ exp1 '..' exp2 ]  :: ::              enummap_range
+    | lexp [ exp ]  :: ::                         vector
+    | lexp [ exp1 : exp2 ]  :: ::              vector_range
     % maybe comma-sep such lists too
     | lexp . id :: :: field  
 
@@ -804,43 +808,43 @@ grammar
 
 %%%%% C-ish style %%%%%%%%%%
 
-c_tannot_opt :: 'C_typ_annot_' ::=
+tannot_opt :: 'Typ_annot_opt_' ::=
   {{ com Optional type annotations }}
   |                                             :: :: none
   | typ_quant typ                               :: :: some 
 
-c_funcl :: 'C_FCL_' ::=
+funcl :: 'FCL_' ::=
   {{ com Function clauses }}
   {{ aux _ l }}
   | id pat = exp                   :: :: Funcl
 
-c_rec_opt :: '' ::=
+rec_opt :: 'Rec_' ::=
   {{ aux _ l }}
   |                                             :: :: nonrec
   | rec                                         :: :: rec
 
-c_effects_opt :: '' ::=
+effects_opt :: 'Effects_opt_' ::=
   {{ aux _ l }}
   |                                             :: :: pure {{ com sugar for pure }}
   | effects                                     :: :: nonpure
 
-c_fundef :: 'C_FD_' ::=
+fundef :: 'FD_' ::=
   {{ com Function definition}}
   {{ aux _ l }}
-  | function c_rec_opt c_tannot_opt c_effects_opt c_funcl1 and ... and c_funcln :: :: function {{ texlong }}  {{ com function definition }}
-% TODO note that the typ in the c_tannot_opt is the *result* type, not
+  | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }}  {{ com function definition }}
+% TODO note that the typ in the tannot_opt is the *result* type, not
 %  the type of the whole function.  The argument type comes from the
-%  pattern in the c_funcl
+%  pattern in the funcl
 % TODO the above is ok for single functions, but not for mutually
-%  recursive functions - the c_tannot_opt scopes over all the c_funcli,
+%  recursive functions - the tannot_opt scopes over all the funcli,
 %  which is ok for the typ_quant part but not for the typ part
 
-c_letbind :: 'LB_' ::=
+letbind :: 'LB_' ::=
   {{ com Let bindings }}
   {{ aux _ l }}
-  | typschm id = exp                                :: :: val_exp
+  | typschm id = exp                                :: :: val_explicit
     {{ com Value binding }}
-  | let id = exp                                    :: :: val_imp
+  | let id = exp                                    :: :: val_implicit
     {{ com value binding with implicit type }}
 
 
@@ -868,24 +872,33 @@ default_typing_spec :: 'DT_' ::=
 def :: 'DEF_' ::=
   {{ com Top-level definitions }}
   {{ aux _ l }}
-  | type_def                                                    :: :: type_def
+  | type_def                                                    :: :: type
     {{ com Type definition }}
-  | c_fundef                                                   :: :: fun_def
+  | fundef                                                   :: :: fundef
     {{ com Function definition }}
-  | c_letbind                                                   :: :: val_def
+  | letbind                                                   :: :: val
     {{ com Value definition }}
-  | val_spec                                                    :: :: spec_def
+  | val_spec                                                    :: :: spec
     {{ com Top-level type constraint }}
-  | default_typing_spec                                         :: :: default_def
+  | default_typing_spec                                         :: :: default
     {{ com default kind and type assumptions }}
   | register typ id                                   :: :: reg_dec
     {{ com Register declaration }}
 
+  | split function rec_opt tannot_opt effects_opt id   :: :: split_function
+
+  | function clause funcl  :: :: split_funcl
+
+  | end id  :: :: split_end
+
+  | split typedef id naming_scheme_opt = const union typquant :: :: split_variant
+
+  | union member id =  typ id'  :: :: split_unioncl
 
 defs :: '' ::=
   {{ com Definition sequences }}
   {{ aux _ l }}
-  | def1  .. defn                  :: :: Defs
+  | def1  .. defn                 :: :: Defs
 
 
 
diff --git a/src/ast.ml b/src/ast.ml
index e39f1931..b6ae031a 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.21.2 from: l2.ott *)
+(* generated by Ott 0.22 from: l2.ott *)
 
 
 type text = Ulib.Text.t
@@ -49,6 +49,12 @@ type x = terminal * text (* Variables *)
 type ix = terminal * text (* Variables *)
 
 type 
+id_aux =  (* identifiers *)
+   Id of x
+ | DeIId of terminal * x * terminal (* remove infix status *)
+
+
+type 
 base_kind_aux =  (* base kinds *)
    BK_type of terminal
  | BK_nat of terminal
@@ -57,9 +63,8 @@ base_kind_aux =  (* base kinds *)
 
 
 type 
-id_aux =  (* identifiers *)
-   Id of x
- | DeIId of terminal * x * terminal (* remove infix status *)
+id = 
+   Id_aux of id_aux * l
 
 
 type 
@@ -68,13 +73,14 @@ base_kind =
 
 
 type 
-id = 
-   Id_aux of id_aux * l
-
-
-type 
-kind_aux =  (* kinds *)
-   Kind of (base_kind * terminal) list
+effect_aux =  (* effect *)
+   Effect_rreg of terminal (* read register *)
+ | Effect_wreg of terminal (* write register *)
+ | Effect_rmem of terminal (* read memory *)
+ | Effect_wmem of terminal (* write memory *)
+ | Effect_undef of terminal (* undefined-instruction exception *)
+ | Effect_unspec of terminal (* unspecified values *)
+ | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *)
 
 
 type 
@@ -90,19 +96,13 @@ and nexp =
 
 
 type 
-effect_aux =  (* effect *)
-   Effect_rreg of terminal (* read register *)
- | Effect_wreg of terminal (* write register *)
- | Effect_rmem of terminal (* read memory *)
- | Effect_wmem of terminal (* write memory *)
- | Effect_undef of terminal (* undefined-instruction exception *)
- | Effect_unspec of terminal (* unspecified values *)
- | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *)
+kind_aux =  (* kinds *)
+   K_kind of (base_kind * terminal) list
 
 
 type 
-kind = 
-   Kind_aux of kind_aux * l
+effect = 
+   Effect_aux of effect_aux * l
 
 
 type 
@@ -114,19 +114,8 @@ nexp_constraint_aux =  (* contraints over kind Nat *)
 
 
 type 
-effect = 
-   Effect_aux of effect_aux * l
-
-
-type 
-opt_kind =  (* optionally kind-annotated identifier *)
-   Ki_ant_none of id
- | Ki_ant_kind of id * terminal * kind
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
+kind = 
+   K_aux of kind_aux * l
 
 
 type 
@@ -143,10 +132,14 @@ effects_aux =  (* effect set *)
 
 
 type 
-typquant_aux = 
-   TQ_Ts of terminal * (opt_kind) list * terminal * (nexp_constraint * terminal) list * terminal
- | TQ_Ts_no_constraint of terminal * (opt_kind) list * terminal (* sugar *)
- | TQ_Ts_no_forall (* sugar *)
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
+
+
+type 
+kinded_id =  (* optionally kind-annotated identifier *)
+   KOpt_none of id
+ | KOpt_kind of kind * id
 
 
 type 
@@ -160,8 +153,10 @@ effects =
 
 
 type 
-typquant = 
-   TQ_aux of typquant_aux * l
+typquant_aux = 
+   TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal
+ | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar *)
+ | TypQ_no_forall (* sugar *)
 
 
 type 
@@ -180,6 +175,16 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
+typschm_aux =  (* Type schemes *)
+   TypSchm_ts of typquant * typ
+
+
+type 
 lit =  (* Literal constants *)
    L_true of terminal
  | L_false of terminal
@@ -193,8 +198,8 @@ lit =  (* Literal constants *)
 
 
 type 
-typschm_aux =  (* Type schemes *)
-   TS_Ts of typquant * typ
+typschm = 
+   TypSchm_aux of typschm_aux * l
 
 
 type 
@@ -203,15 +208,13 @@ pat_aux =  (* Patterns *)
  | P_as of terminal * pat * terminal * id * terminal (* Named patterns *)
  | P_typ of terminal * typ * pat * terminal (* Typed patterns *)
  | P_app of id * (pat) list (* Single variable and constructor patterns *)
- | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* Record patterns *)
  | P_c_record of terminal * terminal * (fpat * terminal) list * terminal * bool * terminal (* C-style struct patterns *)
- | P_vector of terminal * (pat * terminal) list * terminal * bool * terminal (* Vector patterns *)
- | P_vector_concat of terminal * (pat) list * terminal (* Concatenated vector patterns *)
+ | P_vector of terminal * (pat * terminal) list * terminal (* Vector patterns *)
+ | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* Vector patterns *)
+ | P_vector_concat of (pat * terminal) list (* Concatenated vector patterns *)
  | P_tup of terminal * (pat * terminal) list * terminal (* Tuple patterns *)
  | P_list of terminal * (pat * terminal) list * terminal (* List patterns *)
  | P_paren of terminal * pat * terminal
- | P_cons of pat * terminal * pat (* Cons patterns *)
- | P_num_add of id * terminal * terminal * int (* constant addition patterns *)
  | P_lit of lit (* Literal constant patterns *)
 
 and pat = 
@@ -225,11 +228,6 @@ and fpat =
 
 
 type 
-typschm = 
-   TS_aux of typschm_aux * l
-
-
-type 
 exp_aux =  (* Expressions *)
    E_block of terminal * (exp * terminal) list * terminal
  | E_ident of id (* Identifiers *)
@@ -238,19 +236,19 @@ exp_aux =  (* Expressions *)
  | E_infix of exp * id * exp (* Infix applications *)
  | E_tup of terminal * (exp * terminal) list * terminal (* Tuples *)
  | E_if of terminal * exp * terminal * exp * terminal * exp (* Conditionals *)
- | E_enummap of terminal * (exp * terminal) list * terminal
- | E_enummap_e of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal
- | E_enummap_access of exp * terminal * exp * terminal (* enummap access *)
- | E_enummap_subrange of exp * terminal * exp * terminal * exp * terminal (* Subenummap extraction *)
- | E_enummap_update of terminal * exp * terminal * exp * terminal * exp * terminal (* enummap functional update *)
- | E_enummap_update_range of terminal * exp * terminal * (exp) list * terminal * exp * terminal (* enummap functional subrange update (with another enummap) *)
+ | E_vector of terminal * (exp * terminal) list * terminal
+ | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal
+ | E_vector_access of exp * terminal * exp * terminal (* vector access *)
+ | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* Subvector extraction *)
+ | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *)
+ | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional subrange update (with another vector) *)
  | E_list of terminal * (exp * terminal) list * terminal (* list *)
  | E_cons of exp * terminal * exp (* Cons expressions *)
  | E_record of terminal * fexps * terminal (* Records *)
  | E_recup of terminal * exp * terminal * fexps * terminal (* Functional update for records *)
  | E_field of exp * terminal * id (* Field projection for records *)
  | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* Pattern matching expressions *)
- | E_let of c_letbind * terminal * exp (* Let expressions *)
+ | E_let of letbind * terminal * exp (* Let expressions *)
  | E_assign of lexp * terminal * exp
 
 and exp = 
@@ -258,8 +256,8 @@ and exp =
 
 and lexp = 
    LEXP_ident of id (* Identifiers *)
- | LEXP_enummap of lexp * terminal * exp * terminal
- | LEXP_enummap_range of lexp * terminal * exp * terminal * exp * terminal
+ | LEXP_vector of lexp * terminal * exp * terminal
+ | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal
  | LEXP_field of lexp * terminal * id
 
 and fexp_aux =  (* Field-expressions *)
@@ -280,68 +278,60 @@ and pexp_aux =  (* Pattern matches *)
 and pexp = 
    Pat_aux of pexp_aux * l
 
-and c_letbind_aux =  (* Let bindings *)
-   LB_val_exp of typschm * id * terminal * exp (* Value binding *)
- | LB_val_imp of terminal * id * terminal * exp (* value binding with implicit type *)
-
-and c_letbind = 
-   LB_aux of c_letbind_aux * l
-
+and letbind_aux =  (* Let bindings *)
+   LB_val_explicit of typschm * id * terminal * exp (* Value binding *)
+ | LB_val_implicit of terminal * id * terminal * exp (* value binding with implicit type *)
 
-type 
-c_rec_opt_aux = 
-   Nonrec
- | Rec of terminal
+and letbind = 
+   LB_aux of letbind_aux * l
 
 
 type 
-c_funcl_aux =  (* Function clauses *)
-   C_FCL_Funcl of id * pat * terminal * exp
+funcl_aux =  (* Function clauses *)
+   FCL_Funcl of id * pat * terminal * exp
 
 
 type 
-c_effects_opt_aux = 
-   Pure (* sugar for pure *)
- | Nonpure of effects
+rec_opt_aux = 
+   Rec_nonrec
+ | Rec_rec of terminal
 
 
 type 
-ctor_def =  (* Datatype definition clauses *)
-   Cte of id * terminal * typschm
+effects_opt_aux = 
+   Effects_opt_pure (* sugar for pure *)
+ | Effects_opt_nonpure of effects
 
 
 type 
-c_rec_opt = 
-   C_rec_opt_aux of c_rec_opt_aux * l
+tannot_opt =  (* Optional type annotations *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of terminal * typ
 
 
 type 
-c_tannot_opt =  (* Optional type annotations *)
-   C_typ_annot_none
- | C_typ_annot_some of terminal * typ
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
-c_funcl = 
-   C_FCL_aux of c_funcl_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-c_effects_opt = 
-   C_effects_opt_aux of c_effects_opt_aux * l
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal
+fundef_aux =  (* Function definition *)
+   FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list (* function definition *)
 
 
 type 
-tdefbody =  (* Type definition bodies *)
-   Te_abbrev of typschm (* Type abbreviations *)
- | Te_record of typquant * terminal * ((id * terminal * typ) * terminal) list * terminal * bool * terminal (* Record types *)
- | Te_variant of terminal * terminal * (ctor_def * terminal) list (* Variant types *)
+val_spec_aux =  (* Value type specifications *)
+   VS_val_spec of terminal * typschm * id
 
 
 type 
@@ -351,23 +341,8 @@ default_typing_spec_aux =  (* default kinding and typing assumptions *)
 
 
 type 
-val_spec_aux =  (* Value type specifications *)
-   VS_val_spec of terminal * typschm * id
-
-
-type 
-c_fundef_aux =  (* Function definition *)
-   C_FD_function of terminal * c_rec_opt * c_tannot_opt * c_effects_opt * (c_funcl * terminal) list (* function definition *)
-
-
-type 
-type_def =  (* Type definitions *)
-   Td of terminal * id * terminal * kind * naming_scheme_opt * terminal * tdefbody
-
-
-type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+fundef = 
+   FD_aux of fundef_aux * l
 
 
 type 
@@ -376,18 +351,23 @@ val_spec =
 
 
 type 
-c_fundef = 
-   C_FD_aux of c_fundef_aux * l
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
 def_aux =  (* Top-level definitions *)
-   DEF_type_def of type_def (* Type definition *)
- | DEF_fun_def of c_fundef (* Function definition *)
- | DEF_val_def of c_letbind (* Value definition *)
- | DEF_spec_def of val_spec (* Top-level type constraint *)
- | DEF_default_def of default_typing_spec (* default kind and type assumptions *)
+   DEF_type of terminal (* Type 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_reg_dec of terminal * typ * id (* Register declaration *)
+ | DEF_split_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id
+ | DEF_split_funcl of terminal * terminal * funcl
+ | DEF_split_end of terminal * id
+ | DEF_split_variant of terminal * terminal * id * terminal * terminal * terminal * terminal * typquant
+ | DEF_split_unioncl of terminal * terminal * id * terminal * typ * id
 
 
 type 
@@ -396,18 +376,6 @@ def =
 
 
 type 
-bitfield = 
-   BF_bit of terminal * int
- | BF_bits of terminal * int * terminal * terminal * int
- | BF_bitfields of bitfield * terminal * bitfield
-
-
-type 
-defs_aux =  (* Definition sequences *)
-   Defs of (def) list
-
-
-type 
 typ_sugar_aux =  (* library types and syntactic sugar *)
    Typ_sugar_unit of terminal
  | Typ_sugar_bool of terminal
@@ -417,37 +385,54 @@ typ_sugar_aux =  (* library types and syntactic sugar *)
  | Typ_sugar_enum of terminal * nexp * nexp * endian (* natural numbers from nexp to nexp+nexp-1, ordered by endian *)
  | Typ_sugar_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *)
  | Typ_sugar_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_sugar_enummap of terminal * nexp * nexp * endian * typ
- | Typ_sugar_enummap2 of typ * terminal * nexp * terminal
- | Typ_sugar_enummap3 of typ * terminal * nexp * terminal * nexp * terminal
+ | Typ_sugar_vector of terminal * nexp * nexp * endian * typ
+ | Typ_sugar_vector2 of typ * terminal * nexp * terminal
+ | Typ_sugar_vector3 of typ * terminal * nexp * terminal * nexp * terminal
  | Typ_sugar_list of terminal * typ
  | Typ_sugar_set of terminal * typ
  | Typ_sugar_reg of terminal * typ (* type of mutable register components *)
 
 
 type 
-c_tdefbody =  (* Type definition bodies *)
-   C_Te_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* Type abbreviations *)
- | C_Te_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Struct type definition *)
- | C_Te_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Union type definition *)
- | C_Te_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
- | C_Te_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((bitfield * terminal * id) * terminal) list * terminal (* register mutable bitfield type *)
+bitfield = 
+   BF_bit of terminal * int
+ | BF_bits of terminal * int * terminal * terminal * int
+ | BF_bitfields of bitfield * terminal * bitfield
+
+
+type 
+defs_aux =  (* Definition sequences *)
+   Defs of (def) list
+
+
+type 
+typ_sugar = 
+   Typ_sugar_aux of typ_sugar_aux * l
+
+
+type 
+ctor_def =  (* Datatype definition clauses *)
+   CT_ct of id * terminal * typschm
 
 
 type 
 enum_opt = 
-   Enum_empty
- | Enum_enum of terminal
+   EnumOpt_empty
+ | EnumOpt_enum of terminal
 
 
 type 
-defs = 
-   Defs_aux of defs_aux * l
+tdef =  (* Type definition bodies *)
+   TD_abbrev of terminal * id * terminal * terminal * typschm (* Type abbreviations *)
+ | TD_record of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Struct type definition *)
+ | TD_variant of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Union type definition *)
+ | TD_enum of terminal * id * terminal * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
+ | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((bitfield * terminal * id) * terminal) list * terminal (* register mutable bitfield type *)
 
 
 type 
-typ_sugar = 
-   Typ_sugar_aux of typ_sugar_aux * l
+defs = 
+   Defs_aux of defs_aux * l