#ifndef bci_base_h__
#define bci_base_h__
#include <inttypes.h>
#include "stack.h"

#define BCI_CORE_NUM_REG 40

// Note that void * state will later be casted to
// machine_state_t.
typedef char (* bci_core_method_t)(uint8_t small_arg
				, void * state);


#define BCI_CORE_RESULT_RESERVED_BITS    0b11000000
#define BCI_CORE_RESULT_APPLICATION_BITS 0b00111111

#define BCI_CORE_SMALL_ARG_MASK 0b0000000000111111
#define BCI_CORE_OPCODE_MASK    0b1111111111000000

#endif