(* generated by Ott 0.23 from: l2.ott *)
open import Pervasives

open import Map
open import Maybe
open import Set_extra

type l =
  | Unknown
  | Trans of string * maybe l
  | Range of nat * nat

val duplicates : forall 'a. list 'a -> list 'a

val set_from_list : forall 'a. list 'a -> set 'a

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_effect (* kind of effect sets *)


type nexp =  (* expression of kind Nat, for vector sizes and origins *)
 | 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 kind =  (* kinds *)
 | K_kind of list base_kind


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 order =  (* vector order specifications, of kind Order *)
 | Ord_var of kid (* variable *)
 | Ord_inc (* increasing (little-endian) *)
 | Ord_dec (* decreasing (big-endian) *)


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

let effect_union e1 e2 = 
  match (e1,e2) with
  | (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
  end


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 kid * list nat


type kinded_id =  (* optionally kind-annotated identifier *)
 | KOpt_none of kid (* identifier *)
 | KOpt_kind of kind * kid (* kind-annotated variable *)


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 n_constraint (* A constraint for this type *)


type lit =  (* Literal constant *)
 | L_unit (* $() : unit$ *)
 | L_zero (* $bitzero : bit$ *)
 | L_one (* $bitone : bit$ *)
 | L_true (* $true : bool$ *)
 | L_false (* $false : bool$ *)
 | L_num of nat (* natural number constant *)
 | L_hex of string (* bit vector constant, C-style *)
 | L_bin of string (* bit vector constant, C-style *)
 | L_undef (* constant representing undefined values *)
 | L_string of string (* string constant *)


type typ =  (* Type expressions, of kind $Type$ *)
 | Typ_wild (* Unspecified type *)
 | Typ_id of id (* Defined type *)
 | 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 *)

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_effect of effect


type typquant =  (* type quantifiers and constraints *)
 | TypQ_tq of list quant_item
 | TypQ_no_forall (* sugar, omitting quantifier and constraints *)


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

and fpat =  (* Field pattern *)
 | FP_Fpat of id * pat


type typschm =  (* type scheme *)
 | TypSchm_ts of typquant * typ


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

and lexp =  (* lvalue expression *)
 | LEXP_id of id (* identifier *)
 | 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 *)

and fexp =  (* Field-expression *)
 | FE_Fexp of id * exp

and fexps =  (* Field-expression list *)
 | FES_Fexps of list fexp * bool

and pexp =  (* Pattern match *)
 | Pat_exp of pat * exp

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


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


type tannot_opt =  (* Optional type annotation for functions *)
 | Typ_annot_opt_some of typquant * typ


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


type def =  (* Top-level definition *)
 | DEF_type of type_def (* 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_spec (* default kind and type assumptions *)
 | DEF_scattered of scattered_def (* scattered function and type definition *)
 | DEF_reg_dec of typ * id (* register declaration *)


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