summaryrefslogtreecommitdiff
path: root/src/jib.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib.lem')
-rw-r--r--src/jib.lem140
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
-
-
-