#include <gc.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <stdbool.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;

static const bool MEET = false;

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 BB = 8;  /* 0b1000 */
const u64 BF = 9;  /* 0b1001 */
const u64 FB = 10; /* 0b1010 */
const u64 FF = 11; /* 0b1011 */

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
*/
typedef struct {
  ev_t ev;
  u64 len;
  u64 *vals;
} tuple_t;

typedef struct {
  u64 captured_vals[];
} free_vars_t;

typedef struct {
  ev_t ev;
  u64 fptr;
  free_vars_t *free_vars;
} closure_t;

typedef struct {
  ev_t ev;
  u64 size;
  u64 *vals;
} 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;
  double float_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;
}

double print_float(double val) {
  printf("%g", val);
  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 == FF || ev.imm == BB || ev.imm == FB) {
      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 == FF) {
      printf("FF");
    } else if (ev.imm == BF) {
      printf("BF");
    } else if (ev.imm == FB) {
      printf("FB");
    } else if (ev.imm == BB) {
      printf("BB");
    } 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;
      for (size_t i = 1; i < len; ++i) {
        debug_print_ev(ev.arrow_ev->evs[i]);
        printf(" -> ");
      }
      debug_print_ev(ev.arrow_ev->evs[0]);
    } else if (id == Vec) {
      printf("vec[");
      debug_print_ev(ev.vec_ev->ev);
      printf("]");
    } else {
      printf("unexpected evidence: '%" PRIx64 "'", ev.imm);
    }
  }
  fflush(stdout);
}

void debug_print(val_t val) {
  if (val.imm & INT_MASK) {
    print_int(val.imm);
  } else if ((val.imm & BOOL_TAG) == BOOL_TAG) {
    print_bool(val.imm);
  } else {
    ev_t ev = val.header->ev;
    if (ev.imm == FF || ev.imm == BB || ev.imm == FB) {
      print_float(val.imm);
    } else if (ev.imm < MAX_EV_ID) {
      printf("variant (id = %d, case_id = %d)", (int)val.variant->ev.imm,
             (int)val.variant->case_id);
    } else if (ev.header_ev->id == Vec) {
      u64 len = val.vec->size;
      printf("[");
      debug_print((val_t)val.vec->vals[0]);
      for (size_t i = 0; i < len; ++i) {
        printf(", ");
        debug_print((val_t)val.vec->vals[i]);
      }
      printf("]");
    } else if (ev.header_ev->id == Arrow) {
      printf("closure (");
      debug_print_ev(ev);
      printf(")");
    } else if (ev.header_ev->id == Tuple) {
      u64 len = ev.tuple_ev->len;
      printf("(");
      debug_print((val_t)val.tuple->vals[0]);
      for (size_t i = 0; i < len; ++i) {
        printf(", ");
        debug_print((val_t)val.tuple->vals[i]);
      }
      printf(")");
    } else {
      printf("'%" PRIx64 "'", val.imm);
      error(UnexpectedValue);
    }
  }
  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;
  }
}

u64 make_vector(u64 size, u64 initial_value, u64 ev) {
  u64 size_untagged = size >> 1;
  // 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.imm = ev;
  vec->size = size_untagged;
  vec->vals = (u64 *)vals;
  return (u64)vec;
}

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 = BB;
  ptr->val = f;
  return (u64)ptr;
}

val_t box_float(double f) {
  float_t *ptr = (float_t *)malloc(sizeof(float_t));
  ptr->ev.imm = BB;
  ptr->val = f;
  return (val_t)ptr;
}

double unbox_float(val_t val) { return val.float_->val; }

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;
}

void fill_tuple_ev(val_t tuple, ev_t ev) { tuple.tuple->ev = ev; }

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

double read_float() {
  double val;
  scanf("%lf", &val);
  return 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];
}

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;
}

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);
}

ev_t make_germ(ev_t boxed_ev) {
  ev_t ev;
  u32 id = boxed_ev.header_ev->id;
  if (id == Vec) {
    struct vec_ev *ptr = malloc(sizeof(struct vec_ev));
    *ptr = (struct vec_ev){
        .id = Vec,
        .ev = Any,
    };
    ev.vec_ev = ptr;
  } else if (id == Arrow) {
    u64 len = boxed_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] = (ev_t)Any;
    }
    ev.arrow_ev = ptr;
  } else if (id == Tuple) {
    u64 len = boxed_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] = (ev_t)Any;
    }
    ev.tuple_ev = ptr;
  }
  return ev;
}

bool ev_equals(ev_t ev1, ev_t ev2) {
  if (ev1.imm < MAX_EV_ID && ev2.imm < MAX_EV_ID) {
    // Both are immediate
    return ev1.imm == ev2.imm;
  } else if (ev1.imm >= MAX_EV_ID && ev2.imm >= MAX_EV_ID) {
    // Both are boxed
    u64 id1 = ev1.header_ev->id;
    u64 id2 = ev2.header_ev->id;
    
    if (id1 != id2) {
      return false;
    }
    
    if (id1 == Vec) {
      return ev_equals(ev1.vec_ev->ev, ev2.vec_ev->ev);
    } else if (id1 == Arrow) {
      if (ev1.arrow_ev->len != ev2.arrow_ev->len) {
        return false;
      }
      u64 len = ev1.arrow_ev->len;
      for (size_t i = 0; i < len; ++i) {
        if (!ev_equals(ev1.arrow_ev->evs[i], ev2.arrow_ev->evs[i])) {
          return false;
        }
      }
      return true;
    } else if (id1 == Tuple) {
      if (ev1.tuple_ev->len != ev2.tuple_ev->len) {
        return false;
      }
      u64 len = ev1.tuple_ev->len;
      for (size_t i = 0; i < len; ++i) {
        if (!ev_equals(ev1.tuple_ev->evs[i], ev2.tuple_ev->evs[i])) {
          return false;
        }
      }
      return true;
    }
    return false;
  } else {
    // One is immediate and one is boxed - they are not equal
    return false;
  }
}

void meet(ev_t *ev1, ev_t *ev2, bool right);

/*void meet_(ev_t *ev1, ev_t *ev2, bool right) {
  debug_print_ev(*ev1);
  printf(" ∩ ");
  debug_print_ev(*ev2);
  printf("\n");
  meet2(ev1, ev2, right);
  printf("= ");
  if (right) {
    debug_print_ev(*ev2);
  } else {
    debug_print_ev(*ev1);
  }
  printf("\n");
}*/

void meet(ev_t *ev1, ev_t *ev2, bool right){
  

  if(ev_equals(*ev1, *ev2))
    return;
  
  else
    if (ev1->imm < MAX_EV_ID) {
      // ev1 is immediate
      if (ev2->imm < MAX_EV_ID) {
        // ev1 and ev2 are immediate
        ev_t result;
        if (ev1->imm == FF) {
          switch (ev2->imm) {
          case Any:
            result.imm = FB;
            break;
          case FF:
            result.imm = FF;
            break;
          case FB:
            result.imm = FB;
            break;
          default:
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else if (ev1->imm == FB) {
          switch (ev2->imm) {
          case Any:
            result.imm = FB;
            break;
          case BF:
            result.imm = FF;
            break;
          case BB:
            result.imm = FB;
            break;
          case FB:
            result.imm = FB;
            break;
          default:
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else if (ev1->imm == BB) {
          switch (ev2->imm) {
          case Any:
            result.imm = BB;
            break;
          case BF:
            result.imm = BF;
            break;
          case BB:
            result.imm = BB;
            break;
          default:
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else if (ev1->imm == BF) {
          switch (ev2->imm) {
          case Any:
            result.imm = BF;
            break;
          case FF:
            result.imm = BF;
            break;
          case FB:
            result.imm = BB;
            break;
          case BF:
            result.imm = BF;
            break;
          default:
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else if (ev1->imm == Any) {
          switch (ev2->imm) {
          case Any:
            result.imm = Any;
            break;
          case FF:
            result.imm = BF;
            break;
          case FB:
            error(EvidenceNotJustify);
            exit(-1);
          case BF:
            result.imm = BF;
            break;
          case BB:
            result.imm = BB;
            break;
          default:
            result = *ev2;
            break;
          }
        } else if (ev1->imm == Any) {
          result = *ev2;
        } else if (ev2->imm == Any || ev1->imm == ev2->imm) {
          result = *ev1;
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
        
        if (right) {
          *ev2 = result;
        } else {
          *ev1 = result;
        }
      } else {
        // ev1 is immediate, ev2 is boxed
        if (ev1->imm == Any) {
          if (right) {
            // ev2 is already the result (boxed)
          } else {
            // Need to mutate ev1, but it should remain as ev2
            *ev1 = *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) {
          if (right) {
            // ev2 is immediate Any and we need to store boxed result in ev2
            // Must malloc as in make_germ
            u32 id = ev1->header_ev->id;
            if (id == Vec) {
              struct vec_ev *ptr = malloc(sizeof(struct vec_ev));
              *ptr = (struct vec_ev){
                  .id = Vec,
                  .ev = ev1->vec_ev->ev,
              };
              ev2->vec_ev = ptr;
            } else if (id == Arrow) {
              u64 len = ev1->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] = ev1->arrow_ev->evs[i];
              }
              ev2->arrow_ev = ptr;
            } else if (id == Tuple) {
              u64 len = ev1->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] = ev1->tuple_ev->evs[i];
              }
              ev2->tuple_ev = ptr;
            }
          } else {
            // ev1 is already the result (boxed)
          }
        } 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) {
          meet(&ev1->vec_ev->ev, &ev2->vec_ev->ev, right);
        } else if (id1 == Arrow && id2 == Arrow &&
                  ev1->arrow_ev->len == ev2->arrow_ev->len) {
          u64 len = ev1->arrow_ev->len;
          meet(&ev1->arrow_ev->evs[0], &ev2->arrow_ev->evs[0], right);
          for (size_t i = 1; i < len; ++i) {
            meet(&ev2->arrow_ev->evs[i], &ev1->arrow_ev->evs[i], !right);
          }
        } else if (id1 == Tuple && id2 == Tuple &&
                  ev1->tuple_ev->len == ev2->tuple_ev->len) {

          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]), right);
          }
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      }
    }
}

ev_t interior(ev_t ev1, ev_t ev2, bool *changed) {
  *changed = false;
  
  if(ev_equals(ev1, ev2))
    return ev1;
  else 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 == FF) {
        switch (ev2.imm) {
        case Any:
          *changed = true;
          return (ev_t){.imm = FB};
        case FF:
          return (ev_t){.imm = FF};
        case FB:
          *changed = true;
          return (ev_t){.imm = FB};
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == FB) {
        switch (ev2.imm) {
        case Any:
          return (ev_t){.imm = FB};
        case BF:
          *changed = true;
          return (ev_t){.imm = FF};
        case BB:
          *changed = true;
          return (ev_t){.imm = FB};
        case FB:
          return (ev_t){.imm = FB};
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == BB) {
        switch (ev2.imm) {
        case Any:
          return (ev_t){.imm = BB};
        case BF:
          *changed = true;
          return (ev_t){.imm = BF};
        case BB:
          return (ev_t){.imm = BB};
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == BF) {
        switch (ev2.imm) {
        case Any:
          return (ev_t){.imm = BF};
        case FF:
          *changed = true;
          return (ev_t){.imm = BF};
        case FB:
          *changed = true;
          return (ev_t){.imm = BB};
        case BF:
          return (ev_t){.imm = BF};
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == Any) {
        switch (ev2.imm) {
        case Any:
          return (ev_t){.imm = Any};
        case FF:
          *changed = true;
          return (ev_t){.imm = BF};
        case FB:
          error(EvidenceNotJustify);
          exit(-1);
        case BF:
          *changed = true;
          return (ev_t){.imm = BF};
        case BB:
          *changed = true;
          return (ev_t){.imm = BB};
        default:
          *changed = true;
          return ev2;
        }
      } else 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 = interior(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;
        
        // Check first element (contravariant)
        bool elem0_changed = false;
        ev_t elem0 = interior(ev1.arrow_ev->evs[0], ev2.arrow_ev->evs[0], &elem0_changed);
        any_changed |= elem0_changed;
        
        // Check remaining elements (covariant)
        ev_t *temp_evs = alloca(sizeof(ev_t) * len);
        temp_evs[0] = elem0;
        for (size_t i = 1; i < len; ++i) {
          bool elem_changed = false;
          temp_evs[i] = interior(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] = interior(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);
    }
  }
}

ev_t invert_ev(ev_t ev) {
  if (ev.imm < MAX_EV_ID) {
    switch (ev.imm) {
    case Any:
    case Int:
    case Bool:
    case FF:
    case BB:
      return ev;
    case FB:
    case BF:
      return (ev_t)(ev.imm ^ 0b11);
    default:
      return ev;
    }
  }
  u64 id = ev.header_ev->id;
  if (id == Vec) {
    struct vec_ev *ptr = malloc(sizeof(struct vec_ev));
    *ptr = (struct vec_ev){
        .id = Vec,
        .ev = invert_ev(ev.vec_ev->ev),
    };
    return (ev_t)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] = invert_ev(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] = invert_ev(ev.tuple_ev->evs[i]);
    }
    return (ev_t){.tuple_ev = ptr};
  }
  __builtin_unreachable();
}

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

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

val_t ascribe_imm_evidence(val_t value, u64 tag) {
  if (is_imm(value.imm) || value.header->ev.imm != tag) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

val_t ascribe_vec(val_t value, ev_t ev) {
  if (is_imm(value.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  ev_t new_ev;
  bool changed = false;
  if(MEET){
    meet(&value.header->ev, &new_ev, true);
  } else
    new_ev = interior(value.header->ev, (ev_t)ev, &changed);
  if (!changed) {
    return value;
  }
  vec_t *new_vec = malloc(sizeof(vec_t));
  *new_vec = *value.vec;
  new_vec->ev = new_ev;
  return (val_t)new_vec;
}

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

val_t ascribe_closure(val_t value, ev_t ev) {
  if (is_imm(value.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  ev_t new_ev;
  bool changed = false;
  if(MEET){
    meet(&value.tuple->ev, &new_ev, true);
  } else
    new_ev = interior(value.header->ev, (ev_t)ev, &changed);
  if (!changed) {
    return value;
  }
  closure_t *new_closure = malloc(sizeof(closure_t));
  *new_closure = *value.closure;
  new_closure->ev = new_ev;
  return (val_t)new_closure;
}

/**
 * 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;
}

val_t ascribe_tuple(val_t value, ev_t ev) {
  if (is_imm(value.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  ev_t new_ev;
  bool changed = false;
  if(MEET){
    meet(&value.tuple->ev, &new_ev, true);
  } else
    new_ev = interior(value.header->ev, (ev_t)ev, &changed);
  if (!changed) {
    return value;
  }
  tuple_t *new_tuple = malloc(sizeof(tuple_t));
  *new_tuple = *value.tuple;
  new_tuple->ev = new_ev;
  return (val_t)new_tuple;
}

/**
 * Ascribe an arbitrary value to a dyn tuple of the specified length
 */
val_t ascribe_tuple_dyn(val_t value, u64 len) {
  if (is_imm(value.imm) || value.header->ev.header_ev->id != Tuple || value.header->ev.tuple_ev->len != len) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

val_t ascribe_float_of_box(val_t val) {
  if (is_imm(val.imm) ||
      (val.header->ev.imm != BB && val.header->ev.imm != FB)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return ((val_t)unbox_float(val));
}

val_t ascribe_box_of_float(val_t val) {
  val_t f = box_float(val.float_imm);
  f.float_->ev.imm = FB;
  return f;
}

val_t ascribe_boxed_float(val_t val) {
  if (is_imm(val.imm) ||
      (val.header->ev.imm != BB && val.header->ev.imm != FB)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return val;
}

val_t ascribe(val_t value, ev_t ev) {
  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 if (ev.imm == FF) {
      return value;
    } else if (ev.imm == BF) {
      return ascribe_float_of_box(value);
    } else if (ev.imm == FB) {
      return ascribe_box_of_float(value);
    } else if (ev.imm == BB) {
      return ascribe_boxed_float(value);
    } else {
      return ascribe_imm_evidence(value, ev.imm);
    }
  }
  // Evidence is boxed
  u64 id = ev.header_ev->id;
  if (id == Vec) {
    return ascribe_vec(value, ev);
  } else if (id == Arrow) {
    return ascribe_closure(value, ev);
  } else if (id == Tuple) {
    return ascribe_tuple(value, ev);
  }
  __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;
}
