gkp

1 files changed, 131 insertions, 146 deletions

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