(* generated by Ott 0.22 from: l2.ott *)




type text = string (* was Ulib.Text.t *)

type 'a l = 'a
(*
  | Unknown
  | Trans of string * l option
  | Range of Lexing.position * Lexing.position
*)
exception Parse_error_locn of string l * string

type ml_comment = 
  | Chars of text
  | Comment of ml_comment list

type lex_skip =
  | Com of ml_comment
  | Ws of text
  | Nl

type lex_skips = lex_skip list option

(*
let pp_lex_skips ppf sk = 
  match sk with
    | None -> ()
    | Some(sks) ->
        List.iter
          (fun sk ->
             match sk with
               | Com(ml_comment) ->
                   (* TODO: fix? *)
                   Format.fprintf ppf "(**)"
               | Ws(r) ->
                   Format.fprintf ppf "%s" (Ulib.Text.to_string r)
               | Nl -> Format.fprintf ppf "\\n")
          sks

let combine_lex_skips s1 s2 =
  match (s1,s2) with
    | (None,_) -> s2
    | (_,None) -> s1
    | (Some(s1),Some(s2)) -> Some(s2@s1)
*)
type terminal = lex_skips


type x = terminal * text (* identifier *)
type ix = terminal * text (* infix identifier *)

type 
'a base_kind_aux =  (* base kind *)
   BK_type of terminal (* kind of types *)
 | BK_nat of terminal (* kind of natural number size expressions *)
 | BK_order of terminal (* kind of vector order specifications *)
 | BK_effects of terminal (* kind of effect sets *)


type 
'a id_aux =  (* Identifier *)
   Id of x
 | DeIid of terminal * x * terminal (* remove infix status *)


type 
'a base_kind = 
   BK_aux of 'a base_kind_aux * 'a l


type 
'a id = 
   Id_aux of 'a id_aux * 'a l


type 
'a kind_aux =  (* kinds *)
   K_kind of ('a base_kind * terminal) list


type 
'a 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 
'a nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
   Nexp_id of 'a id (* identifier *)
 | Nexp_constant of terminal * int (* constant *)
 | Nexp_times of 'a nexp * terminal * 'a nexp (* product *)
 | Nexp_sum of 'a nexp * terminal * 'a nexp (* sum *)
 | Nexp_exp of terminal * terminal * 'a nexp (* exponential *)

and 'a nexp = 
   Nexp_aux of 'a nexp_aux * 'a l


type 
'a kind = 
   K_aux of 'a kind_aux * 'a l


type 
'a effect = 
   Effect_aux of 'a effect_aux * 'a l


type 
'a nexp_constraint_aux =  (* constraint over kind $_$ *)
   NC_fixed of 'a nexp * terminal * 'a nexp
 | NC_bounded_ge of 'a nexp * terminal * 'a nexp
 | NC_bounded_le of 'a nexp * terminal * 'a nexp
 | NC_nat_set_bounded of 'a id * terminal * terminal * (terminal * int * terminal) list * terminal


type 
'a kinded_id_aux =  (* optionally kind-annotated identifier *)
   KOpt_none of 'a id (* identifier *)
 | KOpt_kind of 'a kind * 'a id (* kind-annotated variable *)


type 
'a order_aux =  (* vector order specifications, of kind $_$ *)
   Ord_id of 'a id (* identifier *)
 | Ord_inc of terminal (* increasing (little-endian) *)
 | Ord_dec of terminal (* decreasing (big-endian) *)


type 
'a effects_aux =  (* effect set, of kind $_$ *)
   Effects_var of 'a id
 | Effects_set of terminal * ('a effect * terminal) list * terminal (* effect set *)


type 
'a nexp_constraint = 
   NC_aux of 'a nexp_constraint_aux * 'a l


type 
'a kinded_id = 
   KOpt_aux of 'a kinded_id_aux * 'a l


type 
'a order = 
   Ord_aux of 'a order_aux * 'a l


type 
'a effects = 
   Effects_aux of 'a effects_aux * 'a l


type 
'a typquant_aux =  (* type quantifiers and constraints *)
   TypQ_tq of terminal * ('a kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal
 | TypQ_no_constraint of terminal * ('a kinded_id) list * terminal (* sugar, omitting constraints *)
 | TypQ_no_forall (* sugar, omitting quantifier and constraints *)


type 
'a typ_aux =  (* Type expressions, of kind $_$ *)
   Typ_wild of terminal (* Unspecified type *)
 | Typ_var of 'a id (* Type variable *)
 | Typ_fn of 'a typ * terminal * 'a typ * 'a effects (* Function type (first-order only in user code) *)
 | Typ_tup of ('a typ * terminal) list (* Tuple type *)
 | Typ_app of 'a id * (typ_arg) list (* type constructor application *)

and 'a typ = 
   Typ_aux of 'a typ_aux * 'a l

and typ_arg_aux =  (* Type constructor arguments of all kinds *)
   Typ_arg_nexp of 'a nexp
 | Typ_arg_typ of 'a typ
 | Typ_arg_order of 'a order
 | Typ_arg_effects of 'a effects

and typ_arg = 
   Typ_arg_aux of typ_arg_aux * 'a l


type 
'a typquant = 
   TypQ_aux of 'a typquant_aux * 'a l


type 
'a typschm_aux =  (* type scheme *)
   TypSchm_ts of 'a typquant * 'a typ


type 
lit =  (* Literal constant *)
   L_unit of terminal * terminal (* $() : _$ *)
 | L_zero of terminal (* $_ : _$ *)
 | L_one of terminal (* $_ : _$ *)
 | L_true of terminal (* $_ : _$ *)
 | L_false of terminal (* $_ : _$ *)
 | L_num of terminal * int (* natural number constant *)
 | L_hex of terminal * string (* bit vector constant, C-style *)
 | L_bin of terminal * string (* bit vector constant, C-style *)
 | L_string of terminal * Ulib.UTF8.t (* string constant *)


type 
'a typschm = 
   TypSchm_aux of 'a typschm_aux * 'a l


type 
'a pat_aux =  (* Pattern *)
   P_lit of lit (* literal constant pattern *)
 | P_wild of terminal (* wildcard *)
 | P_as of terminal * 'a pat * terminal * 'a id * terminal (* named pattern *)
 | P_typ of terminal * 'a typ * 'a pat * terminal (* typed pattern *)
 | P_id of 'a id (* identifier *)
 | P_app of 'a id * ('a pat) list (* union constructor pattern *)
 | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
 | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *)
 | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
 | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *)
 | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *)
 | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *)

and 'a pat = 
   P_aux of 'a pat_aux * 'a l

and 'a fpat_aux =  (* Field pattern *)
   FP_Fpat of 'a id * terminal * 'a pat

and 'a fpat = 
   FP_aux of 'a fpat_aux * 'a l


type 
'a exp_aux =  (* Expression *)
   E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
 | E_id of 'a id (* identifier *)
 | E_lit of lit (* literal constant *)
 | E_cast of terminal * 'a typ * terminal * 'a exp (* cast *)
 | E_app of 'a exp * ('a exp) list (* function application *)
 | E_app_infix of 'a exp * 'a id * 'a exp (* infix function application *)
 | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *)
 | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *)
 | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *)
 | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *)
 | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *)
 | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *)
 | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *)
 | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *)
 | E_list of terminal * ('a exp * terminal) list * terminal (* list *)
 | E_cons of 'a exp * terminal * 'a exp (* cons *)
 | E_record of terminal * 'a fexps * terminal (* struct *)
 | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *)
 | E_field of 'a exp * terminal * 'a id (* field projection from struct *)
 | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *)
 | E_let of 'a letbind * terminal * 'a exp (* let expression *)
 | E_assign of lexp * terminal * 'a exp (* imperative assignment *)

and 'a exp = 
   E_aux of 'a exp_aux * 'a l

and lexp =  (* lvalue expression *)
   LEXP_id of 'a id (* identifier *)
 | LEXP_vector of lexp * terminal * 'a exp * terminal (* vector element *)
 | LEXP_vector_range of lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *)
 | LEXP_field of lexp * terminal * 'a id (* struct field *)

and 'a fexp_aux =  (* Field-expression *)
   FE_Fexp of 'a id * terminal * 'a exp

and 'a fexp = 
   FE_aux of 'a fexp_aux * 'a l

and 'a fexps_aux =  (* Field-expression list *)
   FES_Fexps of ('a fexp * terminal) list * terminal * bool

and 'a fexps = 
   FES_aux of 'a fexps_aux * 'a l

and 'a pexp_aux =  (* Pattern match *)
   Pat_exp of 'a pat * terminal * 'a exp

and 'a pexp = 
   Pat_aux of 'a pexp_aux * 'a l

and 'a letbind_aux =  (* Let binding *)
   LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *)
 | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *)

and 'a letbind = 
   LB_aux of 'a letbind_aux * 'a l


type 
'a rec_opt_aux =  (* Optional recursive annotation for functions *)
   Rec_nonrec (* non-recursive *)
 | Rec_rec of terminal (* recursive *)


type 
'a effects_opt_aux =  (* Optional effect annotation for functions *)
   Effects_opt_pure (* sugar for empty effect set *)
 | Effects_opt_effects of 'a effects


type 
'a funcl_aux =  (* Function clause *)
   FCL_Funcl of 'a id * 'a pat * terminal * 'a exp


type 
tannot_opt =  (* Optional type annotation for functions *)
   Typ_annot_opt_none
 | Typ_annot_opt_some of terminal * 'a typ


type 
'a rec_opt = 
   Rec_aux of 'a rec_opt_aux * 'a l


type 
'a effects_opt = 
   Effects_opt_aux of 'a effects_opt_aux * 'a l


type 
'a funcl = 
   FCL_aux of 'a funcl_aux * 'a 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


type 
index_range =  (* index specification, for bitfields in register types *)
   BF_single of terminal * int (* single index *)
 | BF_range of terminal * int * terminal * terminal * int (* index range *)
 | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *)


type 
'a fundef_aux =  (* Function definition *)
   FD_function of terminal * 'a rec_opt * tannot_opt * 'a effects_opt * ('a funcl * terminal) list


type 
'a val_spec_aux =  (* Value type specification *)
   VS_val_spec of terminal * 'a typschm * 'a id


type 
'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
   DT_kind of terminal * 'a base_kind * 'a id
 | DT_typ of terminal * 'a typschm * 'a id


type 
type_def =  (* Type definition body *)
   TD_abbrev of terminal * 'a id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *)
 | TD_record of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* struct type definition *)
 | TD_variant of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* union type definition *)
 | TD_enum of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * ('a id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
 | TD_register of terminal * 'a id * terminal * terminal * terminal * terminal * 'a nexp * terminal * 'a nexp * terminal * terminal * ((index_range * terminal * 'a id) * terminal) list * terminal (* register mutable bitfield type definition *)


type 
'a fundef = 
   FD_aux of 'a fundef_aux * 'a l


type 
'a val_spec = 
   VS_aux of 'a val_spec_aux * 'a l


type 
'a default_typing_spec = 
   DT_aux of 'a default_typing_spec_aux * 'a l


type 
'a def_aux =  (* Top-level definition *)
   DEF_type of type_def (* type definition *)
 | DEF_fundef of 'a fundef (* function definition *)
 | DEF_val of 'a letbind (* value definition *)
 | DEF_spec of 'a val_spec (* top-level type constraint *)
 | DEF_default of 'a default_typing_spec (* default kind and type assumptions *)
 | DEF_reg_dec of terminal * 'a typ * 'a id (* register declaration *)
 | DEF_scattered_function of terminal * terminal * 'a rec_opt * tannot_opt * 'a effects_opt * 'a id (* scattered function definition header *)
 | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *)
 | DEF_scattered_variant of terminal * terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *)
 | DEF_scattered_unioncl of terminal * 'a id * terminal * 'a typ * 'a id (* scattered union definition member *)
 | DEF_scattered_end of terminal * 'a id (* scattered definition end *)


type 
'a typ_lib_aux =  (* library types and syntactic sugar for them *)
   Typ_lib_unit of terminal (* unit type with value $()$ *)
 | Typ_lib_bool of terminal (* booleans $_$ and $_$ *)
 | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *)
 | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *)
 | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *)
 | Typ_lib_enum of terminal * 'a nexp * 'a nexp * 'a order (* natural numbers 'a nexp .. 'a nexp+'a nexp-1, ordered by 'a order *)
 | Typ_lib_enum1 of terminal * 'a nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *)
 | Typ_lib_enum2 of terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
 | Typ_lib_vector of terminal * 'a nexp * 'a nexp * 'a order * 'a typ (* vector of 'a typ, indexed by natural range *)
 | Typ_lib_vector2 of 'a typ * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp ] *)
 | Typ_lib_vector3 of 'a typ * terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp..'a nexp ] *)
 | Typ_lib_list of terminal * 'a typ (* list of 'a typ *)
 | Typ_lib_set of terminal * 'a typ (* finite set of 'a typ *)
 | Typ_lib_reg of terminal * 'a typ (* mutable register components holding 'a typ *)


type 
'a def = 
   DEF_aux of 'a def_aux * 'a l


type 
'a typ_lib = 
   Typ_lib_aux of 'a typ_lib_aux * 'a l


type 
ctor_def =  (* Datatype constructor definition clause *)
   CT_ct of 'a id * terminal * 'a typschm


type 
defs =  (* Definition sequence *)
   Defs of ('a def) list