diff options
Diffstat (limited to 'src/jib.lem')
| -rw-r--r-- | src/jib.lem | 140 |
1 files changed, 0 insertions, 140 deletions
diff --git a/src/jib.lem b/src/jib.lem deleted file mode 100644 index c8959d10..00000000 --- a/src/jib.lem +++ /dev/null @@ -1,140 +0,0 @@ -(* 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 - - - |
