(* generated by Ott 0.29 from: ../language/jib.ott *)
open import Pervasives


open import Ast
open import Value2



type name = 
 | Name of id * nat
 | Have_exception of nat
 | Current_exception of nat
 | Return of nat


type ctyp =  (* C type *)
 | CT_lint
 | CT_fint of nat
 | CT_constant of integer
 | CT_lbits of bool
 | CT_sbits of nat * bool
 | CT_fbits of nat * bool
 | CT_unit
 | CT_bool
 | CT_bit
 | CT_string
 | CT_real
 | CT_tup of list ctyp
 | CT_enum of id * list id
 | CT_struct of id * list (uid * ctyp)
 | CT_variant of id * list (uid * ctyp)
 | CT_vector of bool * ctyp
 | CT_list of ctyp
 | CT_ref of ctyp
 | CT_poly

and uid = id * list ctyp

type op = 
 | Bnot
 | Bor
 | Band
 | List_hd
 | List_tl
 | Bit_to_bool
 | Eq
 | Neq
 | Ilt
 | Ilteq
 | Igt
 | Igteq
 | Iadd
 | Isub
 | Unsigned of nat
 | Signed of nat
 | Bvnot
 | Bvor
 | Bvand
 | Bvxor
 | Bvadd
 | Bvsub
 | Bvaccess
 | Concat
 | Zero_extend of nat
 | Sign_extend of nat
 | Slice of nat
 | Sslice of nat
 | Set_slice
 | Replicate of nat


type clexp = 
 | CL_id of name * ctyp
 | CL_rmw of name * name * ctyp
 | CL_field of clexp * uid
 | CL_addr of clexp
 | CL_tuple of clexp * nat
 | CL_void


type cval = 
 | V_id of name * ctyp
 | V_ref of name * ctyp
 | V_lit of vl * ctyp
 | V_struct of list (uid * cval) * ctyp
 | V_ctor_kind of cval * id * list ctyp * ctyp
 | V_ctor_unwrap of id * cval * list ctyp * ctyp
 | V_tuple_member of cval * nat * nat
 | V_call of op * list cval
 | V_field of cval * uid
 | V_poly of cval * ctyp


type iannot = nat * nat * nat


type instr_aux = 
 | I_decl of ctyp * name
 | I_init of ctyp * name * cval
 | I_jump of cval * string
 | I_goto of string
 | I_label of string
 | I_funcall of clexp * bool * uid * list cval
 | I_copy of clexp * cval
 | I_clear of ctyp * name
 | I_undefined of ctyp
 | I_match_failure
 | I_end of name
 | I_if of cval * list instr * list instr * ctyp
 | I_block of list instr
 | I_try_block of list instr
 | I_throw of cval
 | I_comment of string
 | I_raw of string
 | I_return of cval
 | I_reset of ctyp * name
 | I_reinit of ctyp * name * cval

and instr = 
 | I_aux of instr_aux * iannot


type ctype_def =  (* C type definition *)
 | CTD_enum of id * list id
 | CTD_struct of id * list (uid * ctyp)
 | CTD_variant of id * list (uid * ctyp)


type cdef = 
 | CDEF_reg_dec of id * ctyp * list instr
 | CDEF_type of ctype_def
 | CDEF_let of nat * list (id * ctyp) * list instr
 | CDEF_spec of id * list ctyp * ctyp
 | CDEF_fundef of id * maybe id * list id * list instr
 | CDEF_startup of id * list instr
 | CDEF_finish of id * list instr