Source file jib.ml

(*Generated by Lem from jib.lem.*)
(* generated by Ott 0.34 from: ../../language/jib.ott *)
open Lem_pervasives


open Ast
open Value2

type iannot = int * Parse_ast.l



type chan = 
 | Chan_stdout
 | Chan_stderr


type ctyp =  (* C type *)
 | CT_lint
 | CT_fint of int
 | CT_constant of Nat_big_num.num
 | CT_lbits
 | CT_sbits of int
 | CT_fbits of int
 | CT_unit
 | CT_bool
 | CT_bit
 | CT_string
 | CT_real
 | CT_float of int
 | CT_rounding_mode
 | CT_tup of ctyp list
 | CT_enum of id * id list
 | CT_struct of id * (id * ctyp) list
 | CT_variant of id * (id * ctyp) list
 | CT_fvector of int * ctyp
 | CT_vector of ctyp
 | CT_list of ctyp
 | CT_ref of ctyp
 | CT_poly of kid


type name = 
 | Name of id * int
 | Have_exception of int
 | Current_exception of int
 | Throw_location of int
 | Channel of chan * int
 | Return of int


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


type clexp = 
 | CL_id of name * ctyp
 | CL_rmw of name * name * ctyp
 | CL_field of clexp * id
 | CL_addr of clexp
 | CL_tuple of clexp * int
 | CL_void


type cval = 
 | V_id of name * ctyp
 | V_member of id * ctyp
 | V_lit of vl * ctyp
 | V_tuple of cval list * ctyp
 | V_struct of (id * cval) list * ctyp
 | V_ctor_kind of cval * (id * ctyp list) * ctyp
 | V_ctor_unwrap of cval * (id * ctyp list) * ctyp
 | V_tuple_member of cval * int * int
 | V_call of op * cval list
 | V_field of cval * id


type creturn = 
 | CR_one of clexp
 | CR_multi of clexp list


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


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 creturn * bool * (id * ctyp list) * cval list
 | I_copy of clexp * cval
 | I_clear of ctyp * name
 | I_undefined of ctyp
 | I_exit of string
 | I_end of name
 | I_if of cval * instr list * instr list * ctyp
 | I_block of instr list
 | I_try_block of instr list
 | 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 cdef_aux = 
 | CDEF_register of id * ctyp * instr list
 | CDEF_type of ctype_def
 | CDEF_let of int * (id * ctyp) list * instr list
 | CDEF_val of id *  string option * ctyp list * ctyp
 | CDEF_fundef of id *  id option * id list * instr list
 | CDEF_startup of id * instr list
 | CDEF_finish of id * instr list
 | CDEF_pragma of string * string


type cdef = 
 | CDEF_aux of cdef_aux * unit def_annot