indexvar n , m , i , j ::=
  {{ phantom }}
  {{ com Index variables for meta-lists }}

metavar nat ::=
  {{ phantom }}
  {{ ocaml int }}
  {{ lem nat }}

metavar id ::=
  {{ phantom }}
  {{ ocaml id }}
  {{ lem id }}

metavar mid ::=
  {{ phantom }}
  {{ ocaml id option }}
  {{ lem maybe id }}

metavar string ::=
  {{ phantom }}
  {{ ocaml string }}
  {{ lem string }}

metavar op ::=
  {{ phantom }}
  {{ ocaml string }}
  {{ lem string }}

metavar bool ::=
  {{ phantom }}
  {{ ocaml bool }}
  {{ lem bool }}

metavar value ::=
  {{ phantom }}
  {{ lem vl }}
  {{ ocaml vl }}

embed
{{ lem

open import Ast
open import Value2

}}

grammar

% Fragments are small pure snippets of (abstract) C code, mostly
% expressions, used by the aval and cval types.
fragment :: 'F_' ::=
  | id                                     :: :: id
  | '&' id                                 :: :: ref
  | value                                  :: :: lit
  | have_exception                         :: :: have_exception
  | current_exception                      :: :: current_exception
  | fragment op fragment'                  :: :: op
  | op fragment                            :: :: unary
  | string ( fragment0 , ... , fragmentn ) :: :: call
  | fragment . string                      :: :: field
  | string                                 :: :: raw
  | poly fragment                          :: :: poly

% init / clear -> create / kill

ctyp :: 'CT_' ::=
  {{ com C type }}
  | mpz_t                     :: :: int
% Arbitrary precision GMP integer, mpz_t in C.
  | bv_t ( bool )             :: :: lbits
% Variable length bitvector - flag represents direction, true - dec or false - inc
  | sbv_t ( bool )            :: :: sbits
% Small variable length bitvector - less than 64 bits
  | 'uint64_t' ( nat , bool ) :: :: fbits
% Fixed length bitvector that fits within a 64-bit word. - int
% represents length, and flag is the same as CT_bv.
  | 'int64_t'                 :: :: int64
% Used for (signed) integers that fit within 64-bits.
  | unit_t                    :: :: unit
% unit is a value in sail, so we represent it as a one element type
% here too for clarity but we actually compile it to an int which is
% always 0.
  | bool_t                    :: :: bool
  | real_t                    :: :: real
  | bit_t                     :: :: bit
% The real type in sail. Abstract here, but implemented using either
% GMP rationals or high-precision floating point.
  | ( ctyp0 , ... , ctypn )   :: :: tup
  | string_t                  :: :: string
  | enum id ( id0 , ... , idn )                    :: :: enum
  | struct id ( id0 * ctyp0 , ... , idn * ctypn )  :: :: struct
  | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant
% Abstractly represent how all the Sail user defined types get mapped
% into C. We don't fully worry about precise implementation details at
% this point, as C doesn't have variants or tuples natively, but these
% need to be encoded.
  | vector ( bool , ctyp )         :: :: vector
  | list ( ctyp )                  :: :: list
% A vector type for non-bit vectors, and a list type.
  | ref ( ctyp )                   :: :: ref
  | poly                           :: :: poly

cval :: 'CV_' ::=
  {{ ocaml fragment * ctyp }}
  {{ lem fragment * ctyp }}

clexp :: 'CL_' ::=
  | id : ctyp                :: :: id
  | clexp . string           :: :: field
  | * clexp                  :: :: addr
  | clexp . nat              :: :: tuple
  | current_exception : ctyp :: :: current_exception
  | have_exception           :: :: have_exception

ctype_def :: 'CTD_' ::=
  {{ com C type definition }}
  | enum id = id0 '|' ... '|' idn                     :: :: enum
  | struct id = { id0 : ctyp0 , ... , idn : ctypn }   :: :: struct
  | variant id  = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant

iannot :: 'IA_' ::=
  {{ lem nat * nat * nat }}
  {{ ocaml int * int * int }}

instr :: 'I_' ::=
  {{ aux _ iannot }}
  | ctyp id                                        :: :: decl
  | ctyp id = cval                                 :: :: init
  | if ( cval ) { instr0 ; ... ; instrn }
    else { instr0 ; ... ; instrm } : ctyp          :: :: if
  | jump ( cval ) string                           :: :: jump
  | clexp = bool id ( cval0 , ... , cvaln )        :: :: funcall
  | clexp = cval                                   :: :: copy
  | alias clexp = cval                             :: :: alias
  | clear ctyp id                                  :: :: clear
  | return cval                                    :: :: return
  | { instr0 ; ... ; instrn }                      :: :: block
  | try { instr0 ; ... ; instrn }                  :: :: try_block
  | throw cval                                     :: :: throw
  | '//' string                                    :: :: comment
  | C string                                       :: :: raw % only used for GCC attributes
  | string :                                       :: :: label
  | goto string                                    :: :: goto
  | undefined ctyp                                 :: :: undefined
  | match_failure                                  :: :: match_failure

% For optimising away allocations.
  | reset ctyp id                             :: :: reset
  | ctyp id = cval                            :: :: reinit

cdef :: 'CDEF_' ::=
  | register id : ctyp = {
      instr0 ; ... ; instrn
    } :: :: reg_dec
  | ctype_def          :: :: type
  | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = {
      instr0 ; ... ; instrm
    } :: :: let
% The first list of instructions creates up the global letbinding, the
% second kills it.
  | val id ( ctyp0 , ... , ctypn ) -> ctyp
      :: :: spec
  | function id mid ( id0 , ... , idn ) {
      instr0 ; ... ; instrm
    } :: :: fundef
  | startup id {
      instr0 ; ... ; instrn
    } :: :: startup
  | finish id {
      instr0 ; ... ; instrn
    } :: :: finish