#include <alloca.h>
#include <gc.h>
#include <inttypes.h>
#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <time.h>

#define malloc GC_malloc

typedef uint64_t u64;
typedef uint32_t u32;
typedef int64_t i64;

static const u64 INT_MASK = 0b1;
static const u64 INT_ZERO = INT_MASK;

static const u64 BOXED_MASK = 0b11;
static const u64 MAX_EV_ID = 128;

static const u64 BOOL_FALSE = 0b010;
static const u64 BOOL_TRUE = 0b110;
static const u64 BOOL_TAG = 0b010;
static const u64 BOOL_MASK = 0b111;

enum error {
  NotImplemented = 10,
  ArrayIndexOutOfBounds = 11,
  TypeMismatch = 12,
  UnexpectedValue = 13,
  EvidenceNotJustify = 14,
  UnexpectedVariantCase = 15
};

#define is_imm(val) (((val) & BOXED_MASK) != 0)

/*
Evidence
*/
const u64 Any = 0;
const u64 Int = 1;
const u64 Bool = 2;
const u64 Vec = 3;
const u64 Arrow = 4;
const u64 Tuple = 5;
const u64 Float = 6;

struct arrow_ev;
struct tuple_ev;
struct vec_ev;
struct header_ev;

typedef union ev {
  u64 imm;
  struct arrow_ev *arrow_ev;
  struct tuple_ev *tuple_ev;
  struct vec_ev *vec_ev;
  struct header_ev *header_ev;
} ev_t;

struct arrow_ev {
  u64 id;
  u64 len;
  ev_t evs[];
};

struct tuple_ev {
  u64 id;
  u64 len;
  ev_t evs[];
};

struct vec_ev {
  u64 id;
  ev_t ev;
};

struct header_ev {
  u64 id;
};

/*
Values
*/

// set a default that will be overriden at compile time
#if !defined(PROXY_VALUES) && !defined(MONO_VALUES)
#define PROXY_VALUES
#endif

#if !defined(PROXY_CLOSURES) && !defined(MONO_CLOSURES)
#define PROXY_CLOSURES
#endif

typedef struct {
  ev_t ev;
  u64 len;
#if defined(PROXY_VALUES)
  u64 *vals;
#elif defined(MONO_VALUES)
  u64 vals[];
#endif
} tuple_t;

#if defined(PROXY_VALUES)
typedef struct {
  u64 captured_vals[];
} free_vars_t;
#endif

typedef struct {
  ev_t ev;
  u64 fptr;
#if defined(PROXY_CLOSURES)
  free_vars_t *free_vars;
#elif defined(MONO_CLOSURES)
  u64 captured_vals[];
#endif
} closure_t;

typedef struct {
  ev_t ev;
  u64 size;
#if defined(PROXY_VALUES)
  u64 *vals;
#elif defined(MONO_VALUES)
  u64 vals[];
#endif
} vec_t;

typedef struct {
  ev_t ev;
  u64 case_id;
  u64 vals[];
} variant_t;

typedef struct {
  ev_t ev;
  double val;
} float_t;

typedef struct {
  ev_t ev;
} header_t;

typedef union value {
  uint64_t imm;
  tuple_t *tuple;
  closure_t *closure;
  vec_t *vec;
  variant_t *variant;
  float_t *float_;
  header_t *header;
} val_t;

u64 print(u64 value);

__attribute__((noreturn)) void error(enum error e) {
  printf("Runtime error, ");
  switch (e) {
  case NotImplemented:
    printf("not implemented\n");
    break;
  case ArrayIndexOutOfBounds:
    printf("array index out of bounds\n");
    break;
  case TypeMismatch:
    printf("type mismatch\n");
    break;
  case UnexpectedValue:
    printf("unexpected value\n");
    break;
  case EvidenceNotJustify:
    printf("evidence does not justify the typing judgement\n");
    break;
  case UnexpectedVariantCase:
    printf("unexpected variant case\n");
    break;
  default:
    printf("unknown error code %d\n", (int)e);
    break;
  };
  exit(e);
}

u64 print_int(u64 val) {
  printf("%" PRIi64, (((i64)val) >> 1));
  return val;
}

u64 print_bool(u64 val) {
  if (val == BOOL_FALSE) {
    printf("false");
  } else if (val == BOOL_TRUE) {
    printf("true");
  } else {
    printf("'%" PRIx64 "'", val);
    error(UnexpectedValue);
  }
  return val;
}

u64 print_vec(u64 val) {
  struct vec *vec = (struct vec *)val;
  printf("<vec>");
  return val;
}

u64 print_closure(u64 val) {
  struct closure *closure_ptr = (struct closure *)val;
  printf("<closure>");
  return val;
}

u64 print_tuple(u64 val) {
  tuple_t *tuple_ptr = (tuple_t *)val;
  u64 length = tuple_ptr->len;
  printf("(");
  for (size_t i = 0; i < length; i++) {
    print(tuple_ptr->vals[i]);
    if (i < length - 1) {
      printf(", ");
    }
  }
  printf(")");
  return val;
}

u64 print_float(u64 val) {
  float_t *flt_ptr = (float_t *)val;
  double value = flt_ptr->val;
  printf("%g", (double)value);
  return val;
}

u64 print_variant(u64 val) {
  struct variant *variant_ptr = (struct variant *)val;
  printf("<variant>");
  return val;
}

u64 print_char(u64 val) {
  char c = (char)val;
  printf("%c", c);
  return val;
}

u64 print(u64 value) {
  val_t val = (val_t)value;
  if (val.imm & INT_MASK) {
    print_int(value);
  } else if ((val.imm & BOOL_TAG) == BOOL_TAG) {
    print_bool(value);
  } else {
    ev_t ev = val.header->ev;
    if (ev.imm == Float) {
      print_float(value);
    } else if (ev.imm < MAX_EV_ID) {
      print_variant(value);
    } else if (ev.header_ev->id == Vec) {
      print_vec(value);
    } else if (ev.header_ev->id == Arrow) {
      print_closure(value);
    } else if (ev.header_ev->id == Tuple) {
      print_tuple(value);
    } else {
      printf("'%" PRIx64 "'", value);
      error(UnexpectedValue);
    }
  }
  printf("\n");
  return value;
}

void debug_print_ev(ev_t evidence) {
  ev_t ev = (ev_t)evidence;
  if (ev.imm < MAX_EV_ID) {
    // Evidence is unboxed
    if (ev.imm == Any) {
      printf("?");
    } else if (ev.imm == Int) {
      printf("int");
    } else if (ev.imm == Bool) {
      printf("bool");
    } else if (ev.imm == Float) {
      printf("float");
    } else {
      printf("variant (id=%d)", (int)ev.imm);
    }
  } else {
    // Evidence is boxed
    u64 id = ev.header_ev->id;
    if (id == Tuple) {
      u64 len = ev.tuple_ev->len;
      debug_print_ev(ev.tuple_ev->evs[0]);
      for (size_t i = 1; i < len; ++i) {
        printf(" * ");
        debug_print_ev(ev.tuple_ev->evs[i]);
      }
    } else if (id == Arrow) {
      u64 len = ev.arrow_ev->len;
      debug_print_ev(ev.arrow_ev->evs[0]);
      for (size_t i = 1; i < len; ++i) {
        printf(" -> ");
        debug_print_ev(ev.arrow_ev->evs[i]);
      }
    } else {
      printf("unexpected evidence: '%" PRIx64 "'", ev.imm);
    }
  }
  fflush(stdout);
}

ev_t ev_of_value(u64 value) {
  if (value & INT_MASK) {
    return (ev_t){.imm = Int};
  } else if ((value & BOOL_TAG) == BOOL_TAG) {
    return (ev_t){.imm = Bool};
  } else {
    val_t val = (val_t)value;
    return val.header->ev;
  }
}

#if defined(MONO_VALUES)
u64 fill_tuple_ev(u64 tuple) {
  tuple_t *tuple_ptr = (tuple_t *)tuple;
  u64 len = tuple_ptr->len;
  // allocate evidence block
  struct tuple_ev *ev_ptr =
      malloc(sizeof(struct tuple_ev) + sizeof(ev_t) * len);
  tuple_ptr->ev.tuple_ev = ev_ptr;
  ev_ptr->id = Tuple;
  ev_ptr->len = len;
  // fill with the evidence extracted from each value
  for (size_t i = 0; i < len; ++i) {
    ev_ptr->evs[i] = ev_of_value(tuple_ptr->vals[i]);
  }
  return tuple;
}
#endif

#if defined(PROXY_VALUES)
u64 make_vector(u64 size, u64 initial_value) {
  u64 size_untagged = size >> 1;
  // init ev
  struct vec_ev *ev = (struct vec_ev *)malloc(sizeof(struct vec_ev));
  ev->id = Vec;
  ev->ev = ev_of_value(initial_value);
  // init vals
  val_t *vals = malloc(size_untagged * sizeof(val_t));
  for (u32 i = 0; i < size_untagged; ++i) {
    vals[i].imm = initial_value;
  }
  // init vec
  vec_t *vec = malloc(sizeof(vec_t));
  vec->ev.vec_ev = ev;
  vec->size = size_untagged;
  vec->vals = (u64 *)vals;
  return (u64)vec;
}
#elif defined(MONO_VALUES)
u64 make_vector(u64 size, u64 initial_value) {
  u64 size_untagged = size >> 1;
  vec_t *ptr = (vec_t *)malloc(sizeof(vec_t) + size_untagged * sizeof(u64 *));
  ptr->ev.vec_ev = (struct vec_ev *)malloc(sizeof(struct vec_ev));
  ptr->ev.vec_ev->id = Vec;
  ptr->ev.vec_ev->ev = ev_of_value(initial_value);
  ptr->size = size_untagged;
  for (size_t i = 0; i < size_untagged; ++i) {
    ptr->vals[i] = initial_value;
  }
  return (u64)ptr;
}
#endif

u64 vector_get(u64 vector, u64 idx) {
  vec_t *vec = (vec_t *)vector;
  u64 idx_untagged = idx >> 1;
  if (idx_untagged < 0 || idx_untagged >= vec->size) {
    error(ArrayIndexOutOfBounds);
  }
  return vec->vals[idx_untagged];
}

u64 vector_set(u64 vector, u64 idx, u64 val) {
  vec_t *vec = (vec_t *)vector;
  u64 idx_untagged = idx >> 1;
  if (idx_untagged < 0 || idx_untagged >= vec->size) {
    error(ArrayIndexOutOfBounds);
  }
  vec->vals[idx_untagged] = val;
  return vector;
}

u64 vector_length(u64 vector) {
  vec_t *vec = (vec_t *)vector;
  u64 size_tagged = (vec->size << 1) | INT_MASK;
  return size_tagged;
}

u64 make_variant(u64 id, u64 case_id, u64 num_args) {
  variant_t *variant = (variant_t *)malloc(sizeof(variant_t) +
                                           sizeof(variant->vals[0]) * num_args);
  variant->ev.imm = id;
  variant->case_id = case_id;
  return (u64)variant;
}

u64 make_float(double f) {
  float_t *ptr = (float_t *)malloc(sizeof(float_t));
  ptr->ev.imm = Float;
  ptr->val = f;
  return (u64)ptr;
}

#if defined(PROXY_VALUES)
u64 make_tuple(u64 ev, u64 len, u64 *vals) {
  // allocate tuple
  tuple_t *tuple = (tuple_t *)malloc(sizeof(tuple_t));
  tuple->ev.imm = ev;
  tuple->len = len;
  tuple->vals = vals;
  return (u64)tuple;
}

u64 make_tuple_ev(u64 len, u64 *vals) {
  // allocate evidence block
  struct tuple_ev *ev_ptr =
      malloc(sizeof(struct tuple_ev) + sizeof(ev_t) * len);
  ev_ptr->id = Tuple;
  ev_ptr->len = len;
  // fill with the evidence extracted from each value
  for (size_t i = 0; i < len; ++i) {
    ev_ptr->evs[i] = ev_of_value(vals[i]);
  }
  return (u64)ev_ptr;
}
#endif

u64 read_int() {
  i64 val;
  scanf("%" SCNi64, &val);
  return (val << 1) | INT_MASK;
}

u64 read_float() {
  double val;
  scanf("%lf", &val);
  return make_float(val);
}

u64 read_char() {
  char c;
  scanf(" %c", &c);
  return (u64)c << 1 | INT_MASK;
}

u64 tuple_get(u64 value, int64_t idx) {
  val_t val = (val_t)value;
  return val.tuple->vals[idx];
}

#if defined(PROXY_CLOSURES)
u64 allocate_closure(void *fptr, u64 ev, u64 num_captured_vals) {
  free_vars_t *free_vars = NULL;
  // allocate free vars
  if (num_captured_vals > 0) {
    free_vars = (free_vars_t *)malloc(sizeof(free_vars_t) +
                                      num_captured_vals *
                                          sizeof(free_vars->captured_vals[0]));
  }
  // allocate closure
  closure_t *closure = (closure_t *)malloc(sizeof(closure_t));
  closure->ev.imm = ev;
  closure->fptr = (u64)fptr;
  closure->free_vars = free_vars;
  return (u64)closure;
}
#elif defined(MONO_CLOSURES)
u64 allocate_closure(void *fptr, u64 ev, u64 num_captured_vals) {
  closure_t *closure_ptr = (closure_t *)malloc(
      sizeof(closure_t) +
      sizeof(closure_ptr->captured_vals[0]) * num_captured_vals);
  closure_ptr->fptr = (u64)fptr;
  closure_ptr->ev.imm = ev;
  return (u64)closure_ptr;
}
#endif

ev_t copy(ev_t ev) {
  if (ev.imm < MAX_EV_ID) {
    return ev;
  }
  u64 id = ev.vec_ev->id;
  if (id == Vec) {
    struct vec_ev *ptr = malloc(sizeof(struct vec_ev));
    *ptr = (struct vec_ev){
        .id = Vec,
        .ev = copy(ev.vec_ev->ev),
    };
    return (ev_t){.vec_ev = ptr};
  } else if (id == Arrow) {
    u64 len = ev.arrow_ev->len;
    struct arrow_ev *ptr = malloc(sizeof(struct arrow_ev) + sizeof(ev_t) * len);
    *ptr = (struct arrow_ev){
        .id = Arrow,
        .len = len,
    };
    for (size_t i = 0; i < len; ++i) {
      ptr->evs[i] = copy(ev.arrow_ev->evs[i]);
    }
    return (ev_t){.arrow_ev = ptr};
  } else if (id == Tuple) {
    u64 len = ev.tuple_ev->len;
    struct tuple_ev *ptr = malloc(sizeof(struct tuple_ev) + sizeof(ev_t) * len);
    *ptr = (struct tuple_ev){
        .id = Tuple,
        .len = len,
    };
    for (size_t i = 0; i < len; ++i) {
      ptr->evs[i] = copy(ev.tuple_ev->evs[i]);
    }
    return (ev_t){.tuple_ev = ptr};
  }
  exit(-1);
}

/**
 * Calculates consistent transitivity of two evidences or fails with an error.
 * 
 * Sets changed to true when the result is different from either ev1 or ev2.
 * 
 */
ev_t trans(ev_t ev1, ev_t ev2, bool *changed) {
  *changed = false;
  // TODO: compare performance checking for structural equality first
  // if(ev_equals(ev1, ev2))
  //   return ev1;
  if (ev1.imm == Any) {
    *changed = true;
    return ev2;
  } else if (ev2.imm == Any)
    return ev1;
  else if (ev1.imm < MAX_EV_ID) {
    // ev1 is immediate
    if (ev2.imm < MAX_EV_ID) {
      // ev1 and ev2 are immediate
      if (ev1.imm == Any) {
        *changed = true;
        return ev2;
      } else if (ev2.imm == Any || ev1.imm == ev2.imm) {
        return ev1;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else {
      // ev1 is immediate, ev2 is boxed
      if (ev1.imm == Any) {
        *changed = true;
        return ev2;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    }
  } else {
    // ev1 is boxed
    if (ev2.imm < MAX_EV_ID) {
      // ev1 is boxed and ev2 is immediate
      if (ev2.imm == Any) {
        return ev1;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else {
      // ev1 is boxed and ev2 is boxed
      u64 id1 = ev1.vec_ev->id;
      u64 id2 = ev2.vec_ev->id;
      if (id1 == Vec && id2 == Vec) {
        bool inner_changed = false;
        ev_t inner_result =
            trans(ev1.vec_ev->ev, ev2.vec_ev->ev, &inner_changed);
        if (!inner_changed) {
          return ev1;
        }
        *changed = true;
        struct vec_ev *ptr = malloc(sizeof(struct vec_ev));
        *ptr = (struct vec_ev){
            .id = Vec,
            .ev = inner_result,
        };
        return (ev_t){.vec_ev = ptr};
      } else if (id1 == Arrow && id2 == Arrow &&
                 ev1.arrow_ev->len == ev2.arrow_ev->len) {
        u64 len = ev1.arrow_ev->len;
        bool any_changed = false;

        // We don't need to worry about variance since consistent transitivity
        // is symmetric for this backend.
        ev_t *temp_evs = alloca(sizeof(ev_t) * len);
        for (size_t i = 0; i < len; ++i) {
          bool elem_changed = false;
          temp_evs[i] =
              trans(ev2.arrow_ev->evs[i], ev1.arrow_ev->evs[i], &elem_changed);
          any_changed |= elem_changed;
        }

        if (!any_changed) {
          return ev1;
        }

        *changed = true;
        struct arrow_ev *ptr =
            malloc(sizeof(struct arrow_ev) + sizeof(ev_t) * len);
        *ptr = (struct arrow_ev){
            .id = Arrow,
            .len = len,
        };
        for (size_t i = 0; i < len; ++i) {
          ptr->evs[i] = temp_evs[i];
        }
        return (ev_t){.arrow_ev = ptr};
      } else if (id1 == Tuple && id2 == Tuple &&
                 ev1.tuple_ev->len == ev2.tuple_ev->len) {
        u64 len = ev1.tuple_ev->len;
        bool any_changed = false;
        ev_t *temp_evs = alloca(sizeof(ev_t) * len);

        for (size_t i = 0; i < len; ++i) {
          bool elem_changed = false;
          temp_evs[i] =
              trans(ev1.tuple_ev->evs[i], ev2.tuple_ev->evs[i], &elem_changed);
          any_changed |= elem_changed;
        }

        if (!any_changed) {
          return ev1;
        }

        *changed = true;
        struct tuple_ev *ptr =
            malloc(sizeof(struct tuple_ev) + sizeof(ev_t) * len);
        *ptr = (struct tuple_ev){
            .id = Tuple,
            .len = len,
        };
        for (size_t i = 0; i < len; ++i) {
          ptr->evs[i] = temp_evs[i];
        }
        return (ev_t){.tuple_ev = ptr};
      }
      error(EvidenceNotJustify);
      exit(-1);
    }
  }
}

void meet(ev_t ev1, ev_t ev2, ev_t *ev_res);

void meet_vec(ev_t ev1, ev_t ev2, ev_t *ev_res) {
  if (ev1.vec_ev->id != Vec) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  meet(ev1.vec_ev->ev, ev2.vec_ev->ev, &ev_res->vec_ev->ev);
}

void meet_arrow(ev_t ev1, ev_t ev2, ev_t *ev_res) {
  if (ev1.arrow_ev->id != Arrow || ev1.arrow_ev->len != ev2.arrow_ev->len) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  u64 len = ev1.arrow_ev->len;
  for (size_t i = 0; i < len; ++i) {
    meet(ev1.arrow_ev->evs[i], ev2.arrow_ev->evs[i], &ev_res->arrow_ev->evs[i]);
  }
}

void meet_tuple(ev_t ev1, ev_t ev2, ev_t *ev3) {
  if (ev1.tuple_ev->id != Tuple || ev1.tuple_ev->len != ev2.tuple_ev->len) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  u64 len = ev1.tuple_ev->len;
  for (size_t i = 0; i < len; ++i) {
    meet(ev1.tuple_ev->evs[i], ev2.tuple_ev->evs[i], &ev3->tuple_ev->evs[i]);
  }
}

void meet(ev_t ev1, ev_t ev2, ev_t *ev_res) {
  if (ev2.imm < MAX_EV_ID) {
    // Evidence is unboxed
    if (ev2.imm == Any) {
      *ev_res = ev1;
    } else if (ev1.imm == ev2.imm) {
      *ev_res = ev2;
    } else if (ev1.imm == Any) {
      *ev_res = copy(ev2);
    } else {
      error(EvidenceNotJustify);
      exit(-1);
    }
  } else {
    // Evidence is boxed
    u64 ev2_id = ev2.vec_ev->id;
    if (ev2_id == Vec) {
      meet_vec(ev1, ev2, ev_res);
    } else if (ev2_id == Arrow) {
      meet_arrow(ev1, ev2, ev_res);
    } else if (ev2_id == Tuple) {
      meet_tuple(ev1, ev2, ev_res);
    } else {
      error(EvidenceNotJustify);
      exit(-1);
    }
  }
}

u64 ascribe_int(u64 value) {
  if (value & INT_MASK) {
    return value;
  } else {
    error(EvidenceNotJustify);
    exit(-1);
  }
}

u64 ascribe_bool(u64 value) {
  if ((value & BOOL_TAG) == BOOL_TAG) {
    return value;
  } else {
    error(EvidenceNotJustify);
    exit(-1);
  }
}

/**
 * Ascribe an arbitrary value with evidence known to be immediate (e.g. variant
 * or float)
 */
u64 ascribe_imm_evidence(u64 value, u64 tag) {
  val_t val = (val_t)value;
  if (is_imm(val.imm) || val.header->ev.imm != tag) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

u64 ascribe_vec(u64 value, u64 ev) {
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
#if defined(PROXY_VALUES)
  bool changed = false;
  ev_t new_ev = trans(val.header->ev, (ev_t) ev, &changed);
  if (!changed)
    return value;
  vec_t *new_vec = malloc(sizeof(vec_t));
  *new_vec = *val.vec;
  new_vec->ev = new_ev;
  return (u64)new_vec;
#elif defined(MONO_VALUES)
  meet_vec(val.header->ev, (ev_t)ev, &val.header->ev);
  return value;
#endif
}

/**
 * Ascribe an arbitrary value to a dyn vec
 */
u64 ascribe_vec_dyn(u64 value) {
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

u64 ascribe_closure(u64 value, u64 ev) {
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
#if defined(PROXY_CLOSURES)
  bool changed = false;
  ev_t new_ev = trans(val.header->ev, (ev_t) ev, &changed);
  if (!changed)
    return value;
  closure_t *new_closure = malloc(sizeof(closure_t));
  *new_closure = *val.closure;
  new_closure->ev = new_ev;
  return (u64)new_closure;
#elif defined(MONO_CLOSURES)
  meet_arrow(val.header->ev, (ev_t)ev, &val.header->ev);
  return value;
#endif
}

/**
 * Ascribe an arbitrary value to a dyn closure of the specified length (arity
 * + 1)
 */
u64 ascribe_closure_dyn(u64 value, u64 len) {
  val_t val = (val_t)value;
  if (is_imm(val.imm) || val.header->ev.header_ev->id != Arrow ||
      val.header->ev.arrow_ev->len != len) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

u64 ascribe_tuple(u64 value, u64 ev) {
#if defined(PROXY_VALUES)
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  bool changed = false;
  ev_t new_ev = trans(val.header->ev, (ev_t) ev, &changed);
  if (!changed)
    return value;
  tuple_t *new_tuple = malloc(sizeof(tuple_t));
  *new_tuple = *val.tuple;
  new_tuple->ev = new_ev;
  return (u64)new_tuple;
#elif defined(MONO_VALUES)
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  meet_tuple(val.header->ev, (ev_t)ev, &val.header->ev);
  return value;
#endif
}

u64 ascribe_tuple_dyn(u64 value, u64 len) {
  val_t val = (val_t)value;

  if (is_imm(val.imm) || val.header->ev.header_ev->id != Tuple ||
      val.header->ev.tuple_ev->len != len) {
    if (is_imm(val.imm))
      printf("Value is immediate\n");
    else if (val.header->ev.header_ev->id != Tuple)
      printf("Value is boxed with id=%" PRIu64 "\n",
             val.header->ev.header_ev->id);
    else {
      printf("Value is tuple but with len=%" PRIu64
             " instead of expected len=%" PRIu64 "\n",
             val.header->ev.tuple_ev->len, len);
    }
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

u64 ascribe(u64 value, u64 evidence) {
  val_t val = (val_t)value;
  ev_t ev = (ev_t)evidence;
  if (ev.imm < MAX_EV_ID) {
    // Evidence is unboxed
    if (ev.imm == Any) {
      return value;
    } else if (ev.imm == Int) {
      return ascribe_int(value);
    } else if (ev.imm == Bool) {
      return ascribe_bool(value);
    } else {
      return ascribe_imm_evidence(value, ev.imm);
    }
  }
  // Evidence is boxed
  u64 id = ev.header_ev->id;
  ev_t ev1 = val.header->ev;
  ev_t ev2 = (ev_t)ev;
  if (id == Vec) {
#if defined(PROXY_VALUES)
    return ascribe_vec(value, ev.imm);
#elif defined(MONO_VALUES)
    meet_vec(ev1, ev2, &ev1);
    return val.imm;
#endif
  } else if (id == Arrow) {
#if defined(PROXY_CLOSURES)
    return ascribe_closure(value, ev.imm);
#elif defined(MONO_CLOSURES)
    meet_arrow(ev1, ev2, &ev1);
    return val.imm;
#endif
  } else if (id == Tuple) {
#if defined(PROXY_VALUES)
    return ascribe_tuple(value, ev.imm);
#elif defined(MONO_VALUES)
    meet_tuple(ev1, ev2, &ev1);
    return val.imm;
#endif
  }
  __builtin_unreachable();
}

u64 print_time(u64 *ptr) {
  closure_t *closure = (closure_t *)ptr;
  u64 (*fptr)(u64 *, u64) = (u64 (*)(u64 *, u64))closure->fptr;

  struct timespec start, end;
  clock_gettime(CLOCK_MONOTONIC, &start);

  fptr(ptr, INT_ZERO);

  clock_gettime(CLOCK_MONOTONIC, &end);

  double elapsed =
      (end.tv_sec - start.tv_sec) + (end.tv_nsec - start.tv_nsec) / 1e9;
  fprintf(stderr, "Execution time: %.6f seconds\n", elapsed);

  return INT_ZERO;
}
