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

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

#define is_imm(val) (((val) & BOXED_MASK) != 0)
#define is_float_ev(ev) ((ev).imm == FF || (ev).imm == BF || (ev).imm == FB || (ev).imm == BB)
#define bfloat_left(ev) ev.imm & 0b10 >> 1
#define bfloat_right(ev) ev.imm & 0b01
/*
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 */

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;
  union ev evs[];
};

struct tuple_ev {
  u64 id;
  u64 len;
  union ev 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 {
  ev_t ev;
  u64 fptr;
  u64 captured_vals[];
} closure_t;

typedef struct vec {
  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) {
  variant_t *variant_ptr = (variant_t *)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) {
      print_float(val.float_->val);
    } 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("float");
    } 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);
}

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

u64 make_vector(u64 size, u64 initial_value, u64 ev) {
  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.imm = ev;
  ptr->size = size_untagged;
  for (size_t i = 0; i < size_untagged; ++i) {
    ptr->vals[i] = initial_value;
  }
  return (u64)ptr;
}

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

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

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

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

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

ev_t copy(ev_t ev) {
  if (ev.imm < MAX_EV_ID) {
    return ev;
  }
  u64 imm = ev.vec_ev->id;
  if (imm == 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 (imm == 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 (imm == 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);
}

void meet(ev_t ev1, ev_t ev2, ev_t *ev_res);
/*
void meet_mono(ev_t ev1, ev_t ev2, ev_t *ev_res, bool variance) {
  if (ev1.imm < MAX_EV_ID) {
    if (ev2.imm < MAX_EV_ID) {
      if(variance){ // covariant
        if (ev1.imm == Any ) {
          if (ev2.imm == FB || ev2.imm == BB) {
            *ev_res = (ev_t){.imm = BB};
            return;
          } else if (ev2.imm == BF || ev2.imm == FF) {
            *ev_res = (ev_t){.imm = BF};
            return;
          } else {
            return meet(ev1, ev2, ev_res);
          }
        } else if (ev2.imm == Any) {
            *ev_res = (ev_t){.imm = ev1.imm};
            return;
        } else if (ev1.imm == FF || ev1.imm == BF) {
          if (is_float_ev(ev2)) {
            *ev_res = (ev_t){.imm = ev1.imm};
            return;
          } else {
            error(EvidenceNotJustify);
            exit(-1);
          }
        }else if (ev1.imm == FB || ev1.imm == BB) {
          if(is_float_ev(ev2)) {
            *ev_res = (ev_t){.imm = (ev1.imm & (-1 << 1)) | bfloat_right(ev2)};
            return;
          } else {
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else return meet(ev1, ev2, ev_res);
      } else { //contravariant
        if (ev1.imm == Any ) {
          *ev_res = (ev_t){.imm = ev2.imm};
            return;          
        } else if (ev2.imm == Any) {
            if (ev1.imm == BF || ev1.imm == BB) {
            *ev_res = (ev_t){.imm = BB};
            return;
          } else if (ev1.imm == FB || ev1.imm == FF) {
            *ev_res = (ev_t){.imm = FB};
            return;
          } else {
            return meet(ev1, ev2, ev_res);
          }
        } else if (ev2.imm == FF || ev2.imm == FB) {
          if (is_float_ev(ev1)) {
            *ev_res = (ev_t){.imm = ev1.imm};
            return;
          } else {
            error(EvidenceNotJustify);
            exit(-1);
          }
        }else if (ev2.imm == BF || ev2.imm == BB) {
          if(is_float_ev(ev1)) {
            *ev_res = (ev_t){.imm = (ev1.imm & (-1 << 1)) | bfloat_right(ev2)};
            return;
          } else {
            error(EvidenceNotJustify);
            exit(-1);
          }
        } else return meet(ev1, ev2, ev_res);
      }
    } else {
      //ev 2 is a pointer
      if (ev1.imm == Any) {
        if (ev2.header_ev->id == Vec) {
          //TODO: we dot know if this works!
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          return meet_mono(ev, ev2, ev_res, variance);
        } else if (ev2.header_ev->id == Arrow) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = ev2.arrow_ev->len;
          for (size_t i = 0; i < ev2.arrow_ev->len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          return meet_mono(ev, ev2, ev_res, variance);
        } else if (ev2.header_ev->id == Tuple) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev2.tuple_ev->len;
          for (size_t i = 0; i < ev2.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          return meet_mono(ev, ev2, ev_res, variance);
          
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
          error(EvidenceNotJustify);
          exit(-1);
      }
    }
  } else{
    if (ev2.imm < MAX_EV_ID) {
      if (ev2.imm == Any) {
        if (ev1.header_ev->id == Vec) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          return meet_mono(ev1, ev, ev_res, variance);
        } else if (ev1.header_ev->id == Arrow) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = ev1.arrow_ev->len;
          for (size_t i = 0; i < ev1.arrow_ev->len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          return meet_mono(ev1, ev, ev_res, variance);
          
        } else if (ev1.header_ev->id == Tuple) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev1.tuple_ev->len;
          for (size_t i = 0; i < ev1.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          return meet_mono(ev1, ev, ev_res, variance);
          
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
          error(EvidenceNotJustify);
          exit(-1);
      }
    } else{
      // both of them are pointers
      if(ev1.header_ev->id == Vec && ev2.header_ev->id == Vec) {
        meet_mono(ev1.vec_ev->ev, ev2.vec_ev->ev, &ev1.vec_ev->ev, variance);
        return;
      } else if (ev1.header_ev->id == Arrow && ev2.header_ev->id == Arrow && ev1.arrow_ev->len == ev2.arrow_ev->len) {
        u64 len = ev1.arrow_ev->len;
        //cod case
        meet_mono(ev1.arrow_ev->evs[0], ev2.arrow_ev->evs[0], &ev1.arrow_ev->evs[0], variance); //flag
        for (size_t i = 0; i < len; ++i) {
          meet_mono(ev2.arrow_ev->evs[i], ev1.arrow_ev->evs[i], &ev1.arrow_ev->evs[i], !variance);
        }
        return;             
      } else if (ev1.header_ev->id == Tuple && ev2.header_ev->id == Tuple && ev1.tuple_ev->len == ev2.tuple_ev->len) {
        u64 len = ev1.tuple_ev->len;
        for (size_t i = 0; i < len; ++i) {
          meet_mono(ev1.tuple_ev->evs[i], ev2.tuple_ev->evs[i], &ev1.tuple_ev->evs[i], variance);
        }
        return;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    }

  }
}
*/


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;
  meet(ev1.arrow_ev->evs[0], ev2.arrow_ev->evs[0], &ev_res->arrow_ev->evs[0]);
  for (size_t i = 1; i < len; ++i) {
    meet(ev2.arrow_ev->evs[i], ev1.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) {
  /*debug_print_ev(ev1);
  printf(" ∩ ");
  debug_print_ev(ev2);
  printf("\n");*/
  if (ev2.imm < MAX_EV_ID) {
    // Evidence is unboxed
    if (ev1.imm == FF) {
      switch (ev2.imm) {
      case Any:
        ev_res->imm = FB;
        return;
      case FF:
        ev_res->imm = FF;
        return;
      case FB:
        ev_res->imm = FB;
        return;
      default:
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else if (ev1.imm == FB) {
      switch (ev2.imm) {
      case Any:
        ev_res->imm = FB;
        return;
      case BF:
        ev_res->imm = FF;
        return;
      case BB:
        ev_res->imm = FB;
        return;
      default:
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else if (ev1.imm == BF) {
      switch (ev2.imm) {
      case FF:
        ev_res->imm = BF;
        return;
      case FB:
        ev_res->imm = BB;
        return;
      default:
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else if (ev1.imm == BB) {
      switch (ev2.imm) {
      case Any:
        *ev_res = (ev_t){.imm = BB};
        return;
      case BF:
        *ev_res = (ev_t){.imm = BF};
        return;
      case BB:
        *ev_res = (ev_t){.imm = BB};
        return;
      default:
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else 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 {
    // TODO: Verify that this is correct
    // ev2 is boxed
    if (ev1.imm == Any) {
      *ev_res = copy(ev2);
      return;
    }
    // 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);
    }
  }
}

void meet_sound(ev_t ev1, ev_t ev2, ev_t *ev_res) {
  if (ev2.imm < MAX_EV_ID) {
    // Evidence is unboxed
    if(ev1.imm < MAX_EV_ID){
      // both are unboxed
      if (ev1.imm == FF) {
        switch (ev2.imm) {
        case Any:
          ev_res->imm = FB;
          return;
        case FF:
          ev_res->imm = FF;
          return;
        case FB:
          ev_res->imm = FB;
          return;
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == FB) {
        switch (ev2.imm) {
        case Any:
          ev_res->imm = FB;
          return;
        case BF:
          ev_res->imm = FF;
          return;
        case BB:
          ev_res->imm = FB;
          return;
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == BF) {
        switch (ev2.imm) {
        case FF:
          ev_res->imm = BF;
          return;
        case FB:
          ev_res->imm = BB;
          return;
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev1.imm == BB) {
        switch (ev2.imm) {
        case Any:
          *ev_res = (ev_t){.imm = BB};
          return;
        case BF:
          *ev_res = (ev_t){.imm = BF};
          return;
        case BB:
          *ev_res = (ev_t){.imm = BB};
          return;
        default:
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else if (ev2.imm == Any) {
          *ev_res = ev1;
          return;
      } else if (ev1.imm == ev2.imm) {
        *ev_res = ev2;
        return;
      } else if (ev1.imm == Any) {
        *ev_res = copy(ev2);
        return;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else{
      // ev1 is boxed
      if(ev2.imm == Any) { 
        u64 ev1_id = ev1.vec_ev->id;
        if(ev1_id == Vec) {
          ev_t ev = {.vec_ev = malloc(sizeof(struct vec_ev))};
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          ev2 = ev;
          return meet(ev1, ev2, ev_res);
        } else if(ev1_id == Arrow) {
          u64 len = ev1.arrow_ev->len;
          ev_t ev = {.arrow_ev = malloc(sizeof(struct arrow_ev) + sizeof(ev_t) * len)};
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = len;
          for (size_t i = 0; i < len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          ev2 = ev;
          return meet(ev1, ev2, ev_res);
        } else if(ev1_id == Tuple) {
          ev_t ev = {.vec_ev = malloc(sizeof(struct tuple_ev))};
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev1.tuple_ev->len;
          for (size_t i = 0; i < ev1.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          ev2 = ev;
          return meet(ev1, ev2, ev_res);
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
        error(EvidenceNotJustify);
        exit(-1);
      }
    }
  } else {
    // TODO: Verify that this is correct
    // ev2 is boxed
    if(ev1.imm < MAX_EV_ID){
      if (ev1.imm == Any) {
        u64 ev2_id = ev2.vec_ev->id;
        if(ev2_id == Vec) {
          ev_t ev = {.vec_ev = malloc(sizeof(struct vec_ev))};
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          ev1 = ev;
          return meet(ev1, ev2, ev_res);
        } else if(ev2_id == Arrow) {
          u64 len = ev2.arrow_ev->len;
          ev_t ev = {.arrow_ev = malloc(sizeof(struct arrow_ev) + sizeof(ev_t) * len)};
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = len;
          for (size_t i = 0; i < len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          ev1 = ev;
          return meet(ev1, ev2, ev_res);
        } else if(ev2_id == Tuple) {
          ev_t ev = {.vec_ev = malloc(sizeof(struct tuple_ev))};
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev2.tuple_ev->len;
          for (size_t i = 0; i < ev2.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          ev1 = ev;
          return meet(ev1, ev2, ev_res);
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
        error(EvidenceNotJustify);
        exit(-1);
      }
    } else{
      // both are boxed
      // 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);
      }
    }
  }
}

ev_t invert_ev(ev_t ev) {
  if (ev.imm < MAX_EV_ID) {
    switch (ev.imm) {  
    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();
}

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

/**
 * Ascribe an arbitrary value with evidence known to correspond to a vec
 */
u64 ascribe_vec(u64 value, u64 ev) {
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  meet_vec(val.header->ev, (ev_t)ev, &val.header->ev);
  return value;
}

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

/**
 * Ascribe an arbitrary value with evidence known to correspond to a closure
 */
u64 ascribe_closure(u64 value, u64 ev) {
  val_t val = (val_t)value;
  if (is_imm(val.imm)) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  meet_arrow(val.header->ev, (ev_t)ev, &val.header->ev);
  return value;
}

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

/**
 * Ascribe an arbitrary value with evidence known to correspond to a tuple
 */
u64 ascribe_tuple(u64 value, u64 ev) {
  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;
}

/**
 * Ascribe an arbitrary value to a dyn tuple of the specified length
 */
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) {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return value;
}

u64 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)).imm;
};

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

u64 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.imm;
}

u64 ascribe(u64 value, u64 ev) {
  val_t val = (val_t)value;
  if (ev < MAX_EV_ID) {
    // Evidence is unboxed
    if (ev == Any) {
      return value;
    } else if (ev == Int) {
      return ascribe_int(value);
    } else if (ev == Bool) {
      return ascribe_bool(value);
    } else if (ev == FF) {
      return value;
    } else if (ev == BF) {
      return ascribe_float_of_box(val);
    } else if (ev == FB) {
      return ascribe_box_of_float(val);
    } else if (ev == BB) {
      return ascribe_boxed_float(val);
    } else {
      return ascribe_imm_evidence(value, ev);
    }
  }
  // Evidence is boxed
  ev_t ev1 = val.header->ev;
  ev_t ev2 = (ev_t)ev;
  if (ev2.header_ev->id == Vec) {
    meet_vec(ev1, ev2, &ev1);
  } else if (ev2.header_ev->id == Arrow) {
    meet_arrow(ev1, ev2, &ev1);
  } else if (ev2.header_ev->id == Tuple) {
    meet_tuple(ev1, ev2, &ev1);
  } else {
    error(EvidenceNotJustify);
    exit(-1);
  }
  return val.imm;
}

void fill_tuple_ev(val_t tuple, ev_t ev) {
  tuple.tuple->ev = ev;
  u32 len = ev.arrow_ev->len;
  for (size_t i = 0; i < len; ++i) {
    tuple.tuple->vals[i] =
        ascribe(tuple.tuple->vals[i], ev.tuple_ev->evs[i].imm);
  }
}

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

u64 print_time(u64 *ptr) {
  closure_t *closure_ptr = (closure_t *)ptr;
  u64 (*fptr)(u64 *, u64) = (u64 (*)(u64 *, u64))closure_ptr->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;
}


/*

void interior_special(ev_t ev1, ev_t ev2, ev_t *ev_res) {
  if (ev1.imm < MAX_EV_ID) {
    if (ev2.imm < MAX_EV_ID) {
      if(ev1.imm == ev2.imm){
        *ev_res = (ev_t){.imm = ev1.imm};
        return;
      } else if ((ev1.imm == BF || ev1.imm == FF) && (ev2.imm == Any || ev2.imm == BF || ev2.imm == BB))  {
        *ev_res = (ev_t){.imm = FB};
        return;
      } else if ((ev1.imm == BF || ev1.imm == FF) && (ev2.imm == FF || ev2.imm == FB))  {
        *ev_res = (ev_t){.imm = FF};
        return;
      } else if ((ev1.imm == BB || ev1.imm == FB || ev2.imm == Any ) && (ev2.imm == Any || ev2.imm == BF || ev2.imm == BB))  {
        *ev_res = (ev_t){.imm = Any};
        return;
      } else if ((ev1.imm == BB || ev1.imm == FB || ev2.imm == Any ) && (ev2.imm == FF || ev2.imm == FB))  {
        *ev_res = (ev_t){.imm = BF};  
        return;
      } else {
        return meet(ev1, ev2, ev_res);
      }
    } else {
      //ev 2 is a pointer
      if (ev1.imm == Any) {
        if (ev2.header_ev->id == Vec) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          return interior_special(ev, ev2, ev_res);
        } else if (ev2.header_ev->id == Arrow) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = ev2.arrow_ev->len;
          for (size_t i = 0; i < ev2.arrow_ev->len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          return interior_special(ev, ev2, ev_res);
        } else if (ev2.header_ev->id == Tuple) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev2.tuple_ev->len;
          for (size_t i = 0; i < ev2.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          return interior_special(ev, ev2, ev_res);
          
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
          error(EvidenceNotJustify);
          exit(-1);
      }
    }
  } else{
    if (ev2.imm < MAX_EV_ID) {
      if (ev2.imm == Any) {
        if (ev1.header_ev->id == Vec) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.vec_ev->id = Vec;
          ev.vec_ev->ev.imm = Any;
          return interior_special(ev1, ev, ev_res);
        } else if (ev1.header_ev->id == Arrow) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.arrow_ev->id = Arrow;
          ev.arrow_ev->len = ev1.arrow_ev->len;
          for (size_t i = 0; i < ev1.arrow_ev->len; ++i) {
            ev.arrow_ev->evs[i].imm = Any;
          }
          return interior_special(ev1, ev, ev_res);
          
        } else if (ev1.header_ev->id == Tuple) {
          ev_t ev = (ev_t)malloc(sizeof(struct vec_ev));
          ev.tuple_ev->id = Tuple;
          ev.tuple_ev->len = ev1.tuple_ev->len;
          for (size_t i = 0; i < ev1.tuple_ev->len; ++i) {
            ev.tuple_ev->evs[i].imm = Any;
          }
          return interior_special(ev1, ev, ev_res);
          
        } else {
          error(EvidenceNotJustify);
          exit(-1);
        }
      } else{
          error(EvidenceNotJustify);
          exit(-1);
      }
    } else{
      // both of them are pointers
      if(ev1.header_ev->id == Vec && ev2.header_ev->id == Vec) {
        interior_special(ev1.vec_ev->ev, ev2.vec_ev->ev, &ev1.vec_ev->ev);
        return;
      } else if (ev1.header_ev->id == Arrow && ev2.header_ev->id == Arrow && ev1.arrow_ev->len == ev2.arrow_ev->len) {
        u64 len = ev1.arrow_ev->len;
        //cod case
        interior_special(ev1.arrow_ev->evs[0], ev2.arrow_ev->evs[0], &ev1.arrow_ev->evs[0]); //flag
        for (size_t i = 0; i < len; ++i) {
          interior_special(ev2.arrow_ev->evs[i], ev1.arrow_ev->evs[i], &ev1.arrow_ev->evs[i]);
        }
        return;             
      } else if (ev1.header_ev->id == Tuple && ev2.header_ev->id == Tuple && ev1.tuple_ev->len == ev2.tuple_ev->len) {
        u64 len = ev1.tuple_ev->len;
        for (size_t i = 0; i < len; ++i) {
          interior_special(ev1.tuple_ev->evs[i], ev2.tuple_ev->evs[i], &ev1.tuple_ev->evs[i]);
        }
        return;
      } else {
        error(EvidenceNotJustify);
        exit(-1);
      }
    }

  }
}*/