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


type text = Ulib.Text.t

type l =
  | Unknown
  | Trans of string * l option
  | Range of Lexing.position * Lexing.position

exception Parse_error_locn of l * string

type ml_comment = 
  | Chars of Ulib.Text.t
  | Comment of ml_comment list

type lex_skip =
  | Com of ml_comment
  | Ws of Ulib.Text.t
  | 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 (* Variables *)
type ix = terminal * text (* Variables *)

type 
base_kind_aux =  (* base kinds *)
   BK_type of terminal
 | BK_nat of terminal
 | BK_endian of terminal
 | BK_effects of terminal


type 
id_aux =  (* identifiers *)
   Id of x
 | DeIId of terminal * x * terminal (* remove infix status *)


type 
base_kind = 
   BK_aux of base_kind_aux * l


type 
id = 
   Id_aux of id_aux * l


type 
kind_aux =  (* kinds *)
   Kind of (base_kind * terminal) list


type 
nexp_aux =  (* expressions of kind Nat, for vector lengths *)
   Nexp_var of id
 | Nexp_constant of terminal * int
 | Nexp_times of nexp * terminal * nexp (* must be linear after normalisation... except for the type of *, ahem *)
 | Nexp_sum of nexp * terminal * nexp
 | Nexp_exp of terminal * terminal * nexp

and nexp = 
   Nexp_aux of nexp_aux * l


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 *)


type 
kind = 
   Kind_aux of kind_aux * l


type 
nexp_constraint_aux =  (* contraints over kind Nat *)
   NC_fixed of nexp * terminal * nexp
 | NC_bounded_ge of nexp * terminal * nexp
 | NC_bounded_le of nexp * terminal * nexp
 | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal


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


type 
endian_aux =  (* endianness specifications *)
   End_var of id
 | End_inc of terminal
 | End_dec of terminal


type 
effects_aux =  (* effect set *)
   Effects_var of id
 | Effects_set of terminal * (effect * terminal) list * terminal (* 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 *)


type 
endian = 
   End_aux of endian_aux * l


type 
effects = 
   Effects_aux of effects_aux * l


type 
typquant = 
   TQ_aux of typquant_aux * l


type 
typ =  (* Constructors of kind Type *)
   Typ_wild of terminal (* Unspecified type *)
 | Typ_var of id (* Type variables *)
 | Typ_fn of typ * terminal * typ * effects (* Function types -- first-order only *)
 | Typ_tup of (typ * terminal) list (* Tuple types *)
 | Typ_app of id * (typ_arg) list (* type constructor applications *)

and typ_arg =  (* Type constructor arguments of all kinds *)
   Typ_arg_nexp of nexp
 | Typ_arg_typ of typ
 | Typ_arg_endian of endian
 | Typ_arg_effects of effects


type 
lit =  (* Literal constants *)
   L_true of terminal
 | L_false of terminal
 | L_num of terminal * int
 | L_hex of terminal * string (* hex and bin are constant bit vectors, entered as C-style hex or binaries *)
 | L_bin of terminal * string
 | L_string of terminal * Ulib.UTF8.t
 | L_unit of terminal * terminal
 | L_zero of terminal (* bitzero and bitone are constant bits, if commonly used we will consider overloading 0 and 1 *)
 | L_one of terminal


type 
typschm_aux =  (* Type schemes *)
   TS_Ts of typquant * typ


type 
pat_aux =  (* Patterns *)
   P_wild of terminal (* Wildcards *)
 | 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_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 = 
   P_aux of pat_aux * l

and fpat_aux =  (* Field patterns *)
   FP_Fpat of id * terminal * pat

and fpat = 
   FP_aux of fpat_aux * l


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 *)
 | E_lit of lit (* Literal constants *)
 | E_app of exp * exp (* Function applications *)
 | 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_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_assign of lexp * terminal * exp

and exp = 
   E_aux of exp_aux * l

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_field of lexp * terminal * id

and fexp_aux =  (* Field-expressions *)
   FE_Fexp of id * terminal * exp

and fexp = 
   FE_aux of fexp_aux * l

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

and fexps = 
   FES_aux of fexps_aux * l

and pexp_aux =  (* Pattern matches *)
   Pat_exp of pat * terminal * exp

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


type 
c_rec_opt_aux = 
   Nonrec
 | Rec of terminal


type 
c_funcl_aux =  (* Function clauses *)
   C_FCL_Funcl of id * pat * terminal * exp


type 
c_effects_opt_aux = 
   Pure (* sugar for pure *)
 | Nonpure of effects


type 
ctor_def =  (* Datatype definition clauses *)
   Cte of id * terminal * typschm


type 
c_rec_opt = 
   C_rec_opt_aux of c_rec_opt_aux * l


type 
c_tannot_opt =  (* Optional type annotations *)
   C_typ_annot_none
 | C_typ_annot_some of terminal * typ


type 
c_funcl = 
   C_FCL_aux of c_funcl_aux * l


type 
c_effects_opt = 
   C_effects_opt_aux of c_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


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 *)


type 
default_typing_spec_aux =  (* default kinding and typing assumptions *)
   DT_kind of terminal * base_kind * terminal * string
 | DT_typ of terminal * typschm * terminal * string


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


type 
val_spec = 
   VS_aux of val_spec_aux * l


type 
c_fundef = 
   C_FD_aux of c_fundef_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_reg_dec of terminal * typ * id (* Register declaration *)


type 
def = 
   DEF_aux of def_aux * l


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
 | Typ_sugar_bit of terminal (* pure bits, not mutable bits! *)
 | Typ_sugar_nat of terminal
 | Typ_sugar_string of terminal * Ulib.UTF8.t
 | 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_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 *)


type 
enum_opt = 
   Enum_empty
 | Enum_enum of terminal


type 
defs = 
   Defs_aux of defs_aux * l


type 
typ_sugar = 
   Typ_sugar_aux of typ_sugar_aux * l