Core.fm

Core.Bind: Type
  List(Pair(String)(Core)) -> Core

Core.Comp.check: Core -> Core -> Core.Defs -> Nat -> Maybe(Pair(Comp)(Core))
  (term) (type) (defs) (ctx)
  def Par = Pair(Comp)(Core)
  def par = Pair.new<Comp><Core>
  def bnd = Maybe.bind<Par><Par>
  def err = Maybe.none<Par>
  def ret = Maybe.some<Par>
  def Ret = Maybe(Par)
  def cmp = Pair.fst<Comp><Core>
  def typ = Pair.snd<Comp><Core>
  let con = String.concat
  term<() Ret>
  |#var# () () ()
    Core.Comp.check(term)(type)(defs)(ctx);
  |#ref# ()
    Core.Comp.check(term)(type)(defs)(ctx);
  |#typ#
    Core.Comp.check(term)(type)(defs)(ctx);
  |#all# () () () () ()
    Core.Comp.check(term)(type)(defs)(ctx);
  |#lam# (term.eras) (term.name) (term.body)
    let typv = Core.reduce(type)(defs)
    Core.if_all(typv)<() Ret>
    |#none# err;
    |#some# (got) got<Ret>
      | (typv.eras) (typv.self) (typv.name) (typv.bind) (typv.body)
      let self_var = Core.ann(Bool.true)(term)(type)
      let name_var = Core.ann(Bool.true)(Core.var(term.name)(Nat.succ(ctx))(Bool.false))(typv.bind)
      let body_typ = typv.body(self_var)(name_var)
      let body_ctx = Nat.succ(ctx)
      use body_res = bnd(Core.Comp.check(term.body(name_var))(body_typ)(defs)(body_ctx))
      let comp     = Comp.lam(term.name)(cmp(body_res))
      ret(par(comp)(type));;;
  |#app# () () ()
    Core.Comp.check(term)(type)(defs)(ctx);
  |#let# (term.name) (term.expr) (term.body)
    use expr_res = bnd(Core.Comp.infer(term.expr)(defs)(ctx))
    let expr_var = Core.ann(Bool.true)(term.expr)(typ(expr_res))
    let body_ctx = Nat.succ(ctx)
    use body_res = bnd(Core.Comp.check(term.body(expr_var))(type)(defs)(Nat.succ(ctx)))
    let comp     = Comp.let(term.name)(cmp(expr_res))(cmp(body_res))
    let type     = typ(body_res)
    ret(par(comp)(type));
  |#ann# () () ()
    Core.Comp.check(term)(type)(defs)(ctx);

Core.Comp.infer: Core -> Core.Defs -> Nat -> Maybe(Pair(Comp)(Core))
  (term) (defs) (ctx)
  def Par = Pair(Comp)(Core)
  def par = Pair.new<Comp><Core>
  def bnd = Maybe.bind<Par><Par>
  def err = Maybe.none<Par>
  def ret = Maybe.some<Par>
  def Ret = Maybe(Par)
  def cmp = Pair.fst<Comp><Core>
  def typ = Pair.snd<Comp><Core>
  term<() Ret>
  |#var# (term.name) (term.indx) (term.flip)
    let comp = Comp.var(term.name)
    let type = Core.var(term.name)(term.indx)(term.flip)
    ret(par(comp)(type));
  |#ref# (term.name)
    Core.Defs.get_type(defs)(term.name)<() Ret>
    |#none# err;
    |#some# (type)
      let comp = Comp.var(term.name)
      ret(par(comp)(type));;
  |#typ#
    let comp = Comp.fal
    let type = Core.typ
    ret(par(comp)(type));
  |#all# (term.eras) (term.self) (term.name) (term.bind) (term.body)
    let comp = Comp.fal
    let type = Core.typ
    ret(par(comp)(type));
  |#lam# (term.eras) (term.name) (term.body)
    err;
  |#app# (term.eras) (term.func) (term.argm)
    bnd(Core.Comp.infer(term.func)(defs)(ctx)) | (func_res)
    let func_typ = Core.reduce(typ(func_res))(defs)
    Core.if_all(func_typ)<() Ret>
    |#none# err;
    |#some# (got) got<Ret>
      |#new# (func_typ.eras) (func_typ.self) (func_typ.name) (func_typ.bind) (func_typ.body)
        let self_var = Core.ann(Bool.true)(term.func)(func_typ)
        let name_var = Core.ann(Bool.true)(term.argm)(func_typ.bind)
        use argm_res = bnd(Core.Comp.check(term.argm)(func_typ.bind)(defs)(ctx))
        let term_typ = func_typ.body(self_var)(name_var)
        let comp     = Comp.app(cmp(func_res))(cmp(argm_res))
        let type     = term_typ
        ret(par(comp)(type));;;;
  |#let# (term.name) (term.expr) (term.body)
    use expr_res = bnd(Core.Comp.infer(term.expr)(defs)(ctx))
    let expr_var = Core.ann(Bool.true)(term.expr)(typ(expr_res))
    use body_res = bnd(Core.Comp.infer(term.body(expr_var))(defs)(Nat.succ(ctx)))
    let comp     = Comp.let(term.name)(cmp(expr_res))(cmp(body_res))
    let type     = typ(body_res)
    ret(par(comp)(type));
  |#ann# (term.done) (term.expr) (term.type)
    Core.Comp.check(term.expr)(term.type)(defs)(ctx);

Core.Ctx.ext: String -> Core -> Core.Ctx -> Core.Ctx
  (str) (trm) List.cons<Pair(String)(Core)>(Pair.new<String><Core>(str)(trm))

Core.Ctx: Type
  List(Pair(String)(Core))

Core.Ctx.nil: Core.Ctx
  List.nil<Pair(String)(Core)>

Core.Def : Type
  Pair(Core)(Core)

Core.Defs: Type
  Map(Core.Def)

Core.Defs.get: Core.Defs -> String -> Maybe(Core.Def)
  (defs) (name)
  Map.get<Core.Def>(String.to_bits(name))(defs)

Core.Defs.get_term: Core.Defs -> String -> Maybe(Core)
  (defs) (name)
  Maybe.map<Core.Def><Core>(Pair.snd<Core><Core>)(Core.Defs.get(defs)(name))

Core.Defs.get_type: Core.Defs -> String -> Maybe(Core)
  (defs) (name)
  Maybe.map<Core.Def><Core>(Pair.fst<Core><Core>)(Core.Defs.get(defs)(name))

Core.Defs.new: Map(Pair(Core)(Core))
  Map.new<Pair(Core)(Core)>
  

Core.Defs.set: String -> Core.Def -> Core.Defs -> Core.Defs
  (name) (val) (defs)
  let key = String.to_bits(name)
  Map.set<Core.Def>(key)(val)(defs)

Core.Defs.term: Core.Defs -> String -> Core
  (defs) (name)
  case Core.Defs.get_term(defs)(name):
  | Core.ref("<undefined>");
  | (term) term;

Core.Defs.type: Core.Defs -> String -> Core
  (defs) (name)
  Core.Defs.get_type(defs)(name)<() Core>
  | Core.ref("<undefined>");
  | (type) type;

Core.Read.Reply: (A: Type) -> Type
  (A) Maybe(Pair(A)(String))

Core.Read.all: Core.Read(Core.Bind)
  use self = Core.Read.seek<Text><Core.Bind>(Core.Read.nam)
  use eras = Core.Read.bind<Bool><Core.Bind>(Core.Read.one("(")("<"))
  use name = Core.Read.seek<Text><Core.Bind>(Core.Read.nam)          
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt(":"))     
  use bind = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)     
  use skip = Core.Read.seek<Bool><Core.Bind>(Core.Read.one(")")(">"))
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("->"))    
  use body = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)     
  use ctx  = Core.Read.done<Core.Bind>                               
  Core.all(eras)(self)(name)
  | bind(ctx);
  | (s) (x) body(Core.Ctx.ext(name)(x)(Core.Ctx.ext(self)(s)(ctx)));

Core.Read.ann: Core.Bind -> Core.Read(Core.Bind)
  (expr)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("::"))
  use type = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm) 
  use ctx  = Core.Read.done<Core.Bind>                           
  Core.ann(Bool.false)(expr(ctx))(type(ctx))

Core.Read.app: Core.Bind -> Core.Read(Core.Bind)
  (func)
  use eras = Core.Read.bind<Bool><Core.Bind>(Core.Read.one("(")("<"))
  use argm = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)     
  use skip = Core.Read.seek<Bool><Core.Bind>(Core.Read.one(")")(">"))
  use ctx  = Core.Read.done<Core.Bind>                               
  Core.app(eras)(func(ctx))(argm(ctx))

Core.Read.arr: Core.Bind -> Core.Read(Core.Bind)
  (bind)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("->"))
  use body = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm) 
  use ctx = Core.Read.done<Core.Bind>                           
  Core.all(Bool.false)("")("")
  | bind(ctx);
  | (s) (x) body(Core.Ctx.ext("")(x)(Core.Ctx.ext("")(s)(ctx)));

Core.Read.bind
  : <A: Type> ->
    <B: Type> ->
    Core.Read(A) ->
    (A -> Core.Read(B)) ->
    Core.Read(B)
  <A> <B> (ra) (rb) (code)
  ra(code)<() Core.Read.Reply(B)>
  | Core.Read.fail<B>;
  | (got) got<() Core.Read.Reply(B)>(rb);

Core.Read.def: Core.Read(Pair(String)(Core.Def))
  use name = Core.Read.seek<Text><Pair(String)(Core.Def)>(Core.Read.nam)     
  use skip = Core.Read.seek<Unit><Pair(String)(Core.Def)>(Core.Read.txt(":"))
  use type = Core.Read.seek<Core.Bind><Pair(String)(Core.Def)>(Core.Read.trm)
  use term = Core.Read.seek<Core.Bind><Pair(String)(Core.Def)>(Core.Read.trm)
  let term = term(Core.Ctx.nil)
  let type = type(Core.Ctx.nil)
  let pair = Pair.new<Core><Core>(type)(term)
  let pair = Pair.new<String><Core.Def>(name)(pair)
  Core.Read.done<Pair(String)(Core.Def)>(pair)

Core.Read.defs: Core.Read(Core.Defs)
  Core.Read.defs.go(Core.Defs.new)

Core.Read.defs.go: Core.Defs -> Core.Read(Core.Defs)
  (defs) (code)
  Core.Read.def(code)<() Core.Read.Reply(Core.Defs)>
  | Core.Read.done<Core.Defs>(defs)(code);
  | (got) got<() Core.Read.Reply(Core.Defs)>
    | (pair) (code)
      pair<() Core.Read.Reply(Core.Defs)>
      | (name) (def)
        let defs = Core.Defs.set(name)(def)(defs)
        Core.Read.defs.go(defs)(code)
      ;
    ;
  ;

Core.Read.done: <A: Type> -> A -> String -> Core.Read.Reply(A)
  <A> (x) (code)
  Maybe.some<Pair(A)(String)>(Pair.new<A><String>(x)(code))

Core.Read.fail: <A: Type> -> Core.Read.Reply(A)
  <A> Maybe.none<Pair(A)(String)>

Core.Read.first_of: <A: Type> -> List(Core.Read(A)) -> Core.Read(A)
  <A> (reads) (code)
  reads<() Core.Read.Reply(A)>
  | Core.Read.fail<A>;
  | (reads.head) (reads.tail)
    reads.head(code)<() Core.Read.Reply(A)>
    | Core.Read.first_of<A>(reads.tail)(code);
    | Maybe.some<Pair(A)(String)>;
  ;

Core.Read: Type -> Type
  (A) String -> Core.Read.Reply(A)

Core.Read.fst: List(String) -> Core.Read(Nat)
  (txts)
  let reads
    = List.imap<String><Core.Read(Nat)>
    | (i) (str)
      Core.Read.bind<Unit><Nat>
      | Core.Read.txt(str);
      | () Core.Read.done<Nat>(i);;
    | txts;
  Core.Read.first_of<Nat>(reads)

Core.Read.is_name: Char -> Bool
  (chr) Set.get(U16.to_bits(chr))(Core.Read.is_name.set)

Core.Read.is_name.set: Map(Unit)
  String.to_set(".0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ_abcdefghijklmnopqrstuvwxyz")

Core.Read.is_space: Char -> Bool
  (chr)
  Bool.or
  | U16.eql(chr)(' ');
  | U16.eql(chr)(Char.newline);

Core.Read.lam: Core.Read(Core.Bind)
  use eras = Core.Read.seek<Bool><Core.Bind>(Core.Read.one("(")("<"))
  use name = Core.Read.seek<Text><Core.Bind>(Core.Read.nam)          
  use skip = Core.Read.seek<Bool><Core.Bind>(Core.Read.one(")")(">"))
  use body = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)     
  use ctx  = Core.Read.done<Core.Bind>                               
  Core.lam(eras)(name)((x) body(Core.Ctx.ext(name)(x)(ctx)))

Core.Read.let: Core.Read(Core.Bind)
  use eras = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("let "))
  use name = Core.Read.seek<Text><Core.Bind>(Core.Read.wrd)        
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("="))
  use expr = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)   
  use skip = Core.Read.seek<Bool><Core.Bind>(Core.Read.opt(";"))
  use body = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)   
  use ctx  = Core.Read.done<Core.Bind>                             
  Core.let(name)(expr(ctx))((x) body(Core.Ctx.ext(name)(x)(ctx)))

Core.Read.nam: Core.Read(String)
  (code)
  code<() Core.Read.Reply(String)>
  | Core.Read.done<String>(String.nil)(String.nil);
  | (code.head) (code.tail)
    Core.Read.is_name(code.head)<() Core.Read.Reply(String)>
    | Core.Read.nam(code.tail)<() Core.Read.Reply(String)>
      | Core.Read.fail<String>;
      | (got) got<() Core.Read.Reply(String)>
        | (str) Core.Read.done<String>(String.cons(code.head)(str));
      ;
    ;
    | Core.Read.done<String>(String.nil)(code);
  ;

Core.Read.next: String -> String
  (str)
  let str = String.drop_while(Core.Read.is_space)(str)
  str<() String>
  | String.nil;
  | (str.head) (str.tail)
    // Drops single-line comments
    U16.eql('/')(str.head)<() String>
    | Core.Read.next
      | String.tail
      | String.drop_until(U16.eql(Char.newline))
      | str.tail;;;
    ;

    // Drops multi-line comments
    | U16.eql('#')(str.head)<() String>
      | Core.Read.next
        | String.tail
        | String.drop_until(U16.eql('#'))
        | str.tail;;;
      ;
      | str;
    ;
  ;

Core.Read.one: String -> String -> Core.Read(Bool)
  (chr0) (chr1)
  let list
    = List.cons<String>(chr0)
    | List.cons<String>(chr1)
    | List.nil<String>;;
  Core.Read.bind<Nat><Bool>(Core.Read.fst(list)) | (idx)
  Core.Read.done<Bool>(Bool.not(Nat.is_zero(idx)));

Core.Read.opt: String -> Core.Read(Bool)
  (str) (code)
  Core.Read.txt(str)(code)<() Core.Read.Reply(Bool)>
  | Core.Read.done<Bool>(Bool.false)(code);
  | (got) got<() Core.Read.Reply(Bool)>
    | () (code) Core.Read.done<Bool>(Bool.true)(code);
  ;

Core.Read.par: Core.Read(Core.Bind)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("("))
  use term = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt(")"))
  Core.Read.done<Core.Bind>(term)

Core.Read.pip: Core.Bind -> Core.Read(Core.Bind)
  (func)
  use eras = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("|"))
  use argm = Core.Read.bind<Core.Bind><Core.Bind>(Core.Read.trm)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt(";"))
  use ctx  = Core.Read.done<Core.Bind>                          
  Core.app(Bool.false)(func(ctx))(argm(ctx))


Core.Read.seek
  : <A: Type> ->
    <B: Type> ->
    Core.Read(A) ->
    (A -> Core.Read(B)) ->
    Core.Read(B)
  <A> <B> (ra) (rb) (code)
  Core.Read.bind<A><B>(ra)(rb)(Core.Read.next(code))

Core.Read.trm.base: Core.Read(Core.Bind)
  let nil = List.nil<Core.Read(Core.Bind)>
  let ext = List.cons<Core.Read(Core.Bind)>
  let bases
    = ext(Core.Read.all)
    | ext(Core.Read.lam)
    | ext(Core.Read.let)
    | ext(Core.Read.par)
    | ext(Core.Read.typ)
    //| ext(Core.Read.chr)
    //| ext(Core.Read.str)
    | ext(Core.Read.var)
    | nil;;;;;;
  Core.Read.first_of<Core.Bind>(bases)

Core.Read.trm: Core.Read(Core.Bind)
  Core.Read.seek<Core.Bind><Core.Bind>
  | Core.Read.trm.base;
  | Core.Read.trm.post;

Core.Read.trm.post: Core.Bind -> Core.Read(Core.Bind)
  (base) (code)
  let nil = List.nil<Core.Read(Core.Bind)>
  let ext = List.cons<Core.Read(Core.Bind)>
  let posts
    = ext(Core.Read.app(base))
    | ext(Core.Read.pip(base))
    | ext(Core.Read.arr(base))
    | ext(Core.Read.ann(base))
    | nil;;;;
  Core.Read.first_of<Core.Bind>(posts)(code)<() Core.Read.Reply(Core.Bind)>
  | Core.Read.done<Core.Bind>(base)(code);
  | (got) got<() Core.Read.Reply(Core.Bind)>
    | (post) (code) Core.Read.trm.post(post)(code);
  ;

Core.Read.txt: String -> Core.Read(Unit)
  (str) (code)
  str<() Core.Read.Reply(Unit)>
  | Core.Read.done<Unit>(Unit.new)(code);
  | (str.head) (str.tail)
    code<() Core.Read.Reply(Unit)>
    | Core.Read.fail<Unit>;
    | (code.head) (code.tail)
      U16.eql(str.head)(code.head)<() Core.Read.Reply(Unit)>
      | Core.Read.txt(str.tail)(code.tail);
      | Core.Read.fail<Unit>;
    ;
  ;

Core.Read.typ: Core.Read(Core.Bind)
  use skip = Core.Read.seek<Unit><Core.Bind>(Core.Read.txt("Type"))
  use ctx  = Core.Read.done<Core.Bind>                             
  Core.typ

Core.Read.var: Core.Read(Core.Bind)
  use name = Core.Read.seek<Text><Core.Bind>(Core.Read.nam)
  use ctx  = Core.Read.done<Core.Bind>                     
  let find_var
    = ((var) var<() Bool>((var_name) () String.eql(name)(var_name)))
    :: Pair(String)(Core) -> Bool
  let found_var
    = List.find<Pair(String)(Core)>(find_var)(ctx)
  found_var<() Core>
  | Core.ref(name);
  | (var) var<() Core>((name) (term) term);

Core.Read.wrd: Core.Read(String)
  Core.Read.bind<String><String>(Core.Read.nam)
  | (nam) (code) String.is_empty(nam)<() Core.Read.Reply(String)>
    | Core.Read.fail<String>;
    | Core.Read.done<String>(nam)(code);
  ;


Core.all.Tuple: Type
  <P: Type> -> 
  (all:
    (eras: Bool) -> 
    (self: String) ->
    (name: String) ->
    (bind: Core) ->
    (body: Core -> Core -> Core) ->
    P) ->
  P



Core.all: Bool -> String -> String -> Core -> (Core -> Core -> Core) -> Core
  (eras) (self) (name) (bind) (body)
  <> () () () (all) () () () ()
  all(eras)(self)(name)(bind)(body)

Core.ann: Bool -> Core -> Core -> Core
  (done) (expr) (type)
  <> () () () () () () () (ann)
  ann(done)(expr)(type)

Core.app: Bool -> Core -> Core -> Core
  (eras) (func) (argm)
  <> () () () () () (app) () ()
  app(eras)(func)(argm)

Core.eql: Core -> Core -> Core.Defs -> Bool
  (a) (b) (defs)
  Core.eql.go(a)(b)(defs)(Set.new)(Nat.zero)

Core.eql.go: Core -> Core -> Core.Defs -> Set -> Nat -> Bool
  (a) (b) (defs) (eql) (dep)
  let a = Core.reduce(a)(defs)
  let b = Core.reduce(b)(defs) 
  let x = Core.to_uid(a)
  let y = Core.to_uid(b)
  let h = Bits.concat(x)(y)
  Bool.or(Bits.eql(x)(y))(Set.get(h)(eql))<() Unit -> Bool>
  | () Bool.true;
  | () let eql = Set.set(h)(eql)
    a<() Bool>
    |#var# () () () Bool.false;
    |#ref# (a.name) Bool.false;
    |#typ# Bool.false;
    |#all# (a.eras) (a.self) (a.name) (a.bind) (a.body)
      b<() Bool>
      |#var# () () () Bool.false;
      |#ref# () Bool.false;
      |#typ# Bool.false;
      |#all# (b.eras) (b.self) (b.name) (b.bind) (b.body)
        let s_vari = Core.var("")(dep)(Bool.false)
        let n_vari = Core.var("")(Nat.succ(dep))(Bool.false)
        let a_body = a.body(s_vari)(n_vari)
        let b_body = b.body(s_vari)(n_vari)
        let e_eras = Bool.eql(a.eras)(b.eras)
        let e_self = String.eql(a.self)(b.self)
        let e_bind = Core.eql.go(a.bind)(b.bind)(defs)(eql)(dep)
        let e_body = Core.eql.go(a_body)(b_body)(defs)(eql)(dep)
        Bool.and(e_eras)(Bool.and(e_self)(Bool.and(e_bind)(e_body)));
      |#lam# () () () Bool.false;
      |#app# () () () Bool.false;
      |#let# () () () Bool.false;
      |#ann# () () () Bool.false;;
    |#lam# (a.eras) (a.name) (a.body)
      b<() Bool>
      |#var# () () () Bool.false;
      |#ref# () Bool.false;
      |#typ# Bool.false;
      |#all# () () () () () Bool.false;
      |#lam# (b.eras) (b.name) (b.body)
        let n_vari = Core.var("")(dep)(Bool.false)
        let a_body = a.body(n_vari)
        let b_body = b.body(n_vari)
        let e_eras = Bool.eql(a.eras)(b.eras)
        let e_body = Core.eql.go(a_body)(b_body)(defs)(eql)(dep)
        Bool.and(e_eras)(e_body);
      |#app# () () () Bool.false;
      |#let# () () () Bool.false;
      |#ann# () () () Bool.false;;
    |#app# (a.eras) (a.func) (a.argm)
      b<() Bool>
      |#var# () () () Bool.false;
      |#ref# () Bool.false;
      |#typ# Bool.false;
      |#all# () () () () () Bool.false;
      |#lam# () () () Bool.false;
      |#app# (b.eras) (b.func) (b.argm)
        let e_eras = Bool.eql(a.eras)(b.eras)
        let e_func = Core.eql.go(a.func)(b.func)(defs)(eql)(dep)
        let e_argm = Core.eql.go(a.argm)(b.argm)(defs)(eql)(dep)
        Bool.and(e_eras)(Bool.and(e_func)(e_argm));
      |#let# () () () Bool.false;
      |#ann# () () () Bool.false;;
    |#let# (a.name) (a.expr) (a.body)
      b<() Bool>
      |#var# () () () Bool.false;
      |#ref# () Bool.false;
      |#typ# Bool.false;
      |#all# () () () () () Bool.false;
      |#lam# () () () Bool.false;
      |#app# () () () Bool.false;
      |#let# (b.name) (b.expr) (b.body)
        let n_vari = Core.var("")(dep)(Bool.false)
        let a_body = a.body(n_vari)
        let b_body = b.body(n_vari)
        let e_expr = Core.eql.go(a.expr)(b.expr)(defs)(eql)(dep)
        let e_body = Core.eql.go(a_body)(b_body)(defs)(eql)(dep)
        Bool.eql(e_expr)(e_body);
      |#ann# () () () Bool.false;;
    |#ann# (a.done) (a.expr) (a.type)
      b<() Bool>
      |#var# () () () Bool.false;
      |#ref# () Bool.false;
      |#typ# Bool.false;
      |#all# () () () () () Bool.false;
      |#lam# () () () Bool.false;
      |#app# () () () Bool.false;
      |#let# () () () Bool.false;
      |#ann# (b.done) (b.expr) (b.type)
        let e_expr = Core.eql.go(a.expr)(b.expr)(defs)(eql)(dep)
        e_expr;;;
  | Unit.new;

Core: Type
  core<P: Core -> Type> ->
  (var:
    (name: String) -> 
    (indx: Nat) ->
    (flip: Bool) ->
    P(Core.var(name)(indx)(flip))) ->
  (ref:
    (name: String) ->
    P(Core.ref(name))) ->
  (typ:
    P(Core.typ)) ->
  (all:
    (eras: Bool) ->
    (self: String) ->
    (name: String) ->
    (bind: Core) ->
    (body: Core -> Core -> Core) ->
    P(Core.all(eras)(self)(name)(bind)(body))) ->
  (lam:
    (eras: Bool) ->
    (name: String) ->
    (body: Core -> Core) ->
    P(Core.lam(eras)(name)(body))) ->
  (app:
    (eras: Bool) ->
    (func: Core) ->
    (argm: Core) ->
    P(Core.app(eras)(func)(argm))) ->
  (let:
    (name: String) ->
    (expr: Core) ->
    (body: Core -> Core) ->
    P(Core.let(name)(expr)(body))) ->
  (ann:
    (done: Bool) ->
    (expr: Core) ->
    (type: Core) ->
    P(Core.ann(done)(expr)(type))) ->
  P(core)

Core.if_all: Core -> Maybe(Core.all.Tuple)
  (term)
  term<() Maybe(Core.all.Tuple)>
  |#var# () () () Maybe.none<Core.all.Tuple>;
  |#ref# () Maybe.none<Core.all.Tuple>;
  |#typ# Maybe.none<Core.all.Tuple>;
  |#all# (eras) (name) (self) (bind) (body)
    Maybe.some<Core.all.Tuple>
    | <P> (func) func(eras)(name)(self)(bind)(body);;
  |#lam# () () () Maybe.none<Core.all.Tuple>;
  |#app# () () () Maybe.none<Core.all.Tuple>;
  |#let# () () () Maybe.none<Core.all.Tuple>;
  |#ann# () () () Maybe.none<Core.all.Tuple>;

Core.is_all: Core -> Bool
  (term)
  term<() Bool>
  | (name) (indx) (flip) Bool.false;
  | (name) Bool.false;
  | Bool.false;
  | (eras) (self) (name) (bind) (body) Bool.true;
  | (eras) (name) (body) Bool.false;
  | (eras) (func) (argm) Bool.false;
  | (name) (expr) (body) Bool.false;
  | (done) (expr) (type) Bool.false;

Core.is_lam: Core -> Bool
  (term)
  term<() Bool>
  | (name) (indx) (flip) Bool.false;
  | (name) Bool.false;
  | Bool.false;
  | (eras) (self) (name) (bind) (body) Bool.false;
  | (eras) (name) (body) Bool.true;
  | (eras) (func) (argm) Bool.false;
  | (name) (expr) (body) Bool.false;
  | (done) (expr) (type) Bool.false;

Core.lam: Bool -> String -> (Core -> Core) -> Core
  (eras) (name) (body)
  <> () () () () (lam) () () ()
  lam(eras)(name)(body)

Core.let: String -> Core -> (Core -> Core) -> Core
  (name) (expr) (body)
  <> () () () () () () (Let) ()
  Let(name)(expr)(body)

Core.normalize: Core -> Core.Defs -> Core
  (term) (defs)
  Core.reduce(term)(defs)<() Core>
  | (name) (indx) Core.var(name)(indx);
  | (name) Core.ref(name);
  | Core.typ;
  | (eras) (self) (name) (bind) (body)
    let bind = Core.normalize(bind)(defs)
    let body = ((s) (x) Core.normalize(body(s)(x))(defs)) :: Core -> Core -> Core
    Core.all(eras)(self)(name)(bind)(body);
  | (eras) (name) (body)
    let body = ((x) Core.normalize(body(x))(defs)) :: Core -> Core
    Core.lam(eras)(name)(body);
  | (eras) (func) (argm)
    let func = Core.normalize(func)(defs)
    let argm = Core.normalize(argm)(defs)
    Core.app(eras)(func)(argm);
  | (name) (expr) (body)
    Core.normalize(body(expr))(defs);
  | (done) (expr) (type)
    Core.normalize(expr)(defs);

Core.parse: String -> Core
  (code)
  Core.Read.trm(code)<() Core>
  | Core.ref("<error>");
  | (got) got<() Core>((term) () term(Core.Ctx.nil));

Core.parse_defs: String -> Core.Defs
  (code)
  Core.Read.defs(code)<() Core.Defs>
  | Core.Defs.new;
  | (got) got<() Core.Defs>((defs) () defs);

Core.reduce: Core -> Core.Defs -> Core
  (term) (defs)
  term<() Core>
  | (indx) (name) (flip) Core.var(indx)(name)(flip);
  | (name) Core.Defs.get_term(defs)(name)<() Core>
    | Core.ref(name);
    | (term) Core.reduce(term)(defs);;
  | Core.typ;
  | (eras) (self) (name) (bind) (body)
    Core.all(eras)(self)(name)(bind)(body);
  | (eras) (name) (body)
    eras<() Core>
    | Core.reduce(body(Core.ref("-")))(defs);
    | Core.lam(eras)(name)(body);;
  | (eras) (func) (argm)
    eras<() Core>
    | Core.reduce(func)(defs);
    | Core.reduce(func)(defs)<() Core -> Core>
      | (findx) (fname) (fflip)
        Core.app(eras)(Core.var(findx)(fname)(fflip));
      | (fname)
        Core.app(eras)(Core.ref(fname));
      | Core.app(eras)(Core.typ);
      | (feras) (fself) (fname) (fbind) (fbody)
        Core.app(eras)(Core.all(feras)(fself)(fname)(fbind)(fbody));
      | (feras) (fname) (fbody)
        (term.argm) Core.reduce(fbody(term.argm))(defs);
      | (feras) (ffunc) (fargm)
        Core.app(eras)(Core.app(feras)(ffunc)(fargm));
      | (fname) (fexpr) (fbody)
        Core.app(eras)(Core.let(fname)(fexpr)(fbody));
      | (fdone) (fexpr) (ftype)
        Core.app(eras)(Core.ann(fdone)(fexpr)(ftype));
      | argm;;;
  | (name) (expr) (body) Core.reduce(body(expr))(defs);
  | (done) (expr) (type) Core.reduce(expr)(defs);

Core.ref: String -> Core
  (name)
  <> () (ref) () () () () () ()
  ref(name)

Core.stringify: Core -> String
  (term) Core.stringify.go(term)("")

// TODO this is a WIP
Core.stringify.go: Core -> Stringifier
  (term)
  let lit = String.to_stringifier
  term<() Stringifier>
  | (name) (indx) (flip) (x) lit(name)(x);
  | (name) (x) lit(name)(x);
  | (x) lit("Type")(x);
  | (eras) (self) (name) (bind) (body) (x)
    let svar = Core.var(self)(Nat.zero)(Bool.false)
    let nvar = Core.var(name)(Nat.zero)(Bool.false)
    let body = body(svar)(nvar)
    let self = lit(self)
    let lpar = lit("(")
    let name = lit(name)
    let colo = lit(": ")
    let bind = Core.stringify.go(bind)
    let rpar = lit(") -> ")
    let body = Core.stringify.go(body)
    self(lpar(name(colo(bind(rpar(body(x)))))));
  | (eras) (name) (body) (x)
    let nvar = Core.var(name)(Nat.zero)(Bool.false)
    let body = body(nvar)
    let lpar = lit("(")
    let name = lit(name)
    let rpar = lit(")")
    let spac = lit(" ")
    let body = Core.stringify.go(body)
    lpar(name(rpar(spac(body(x)))));
  | (eras) (func) (argm) (x)
    let wrap = Bool.or(Core.is_lam(func))(Core.is_all(func))
    let inif = wrap<() Stringifier>(lit("("))(lit(""))
    let func = Core.stringify.go(func)
    let endf = wrap<() Stringifier>(lit(")"))(lit(""))
    let lpar = lit("(")
    let argm = Core.stringify.go(argm)
    let rpar = lit(")")
    inif(func(endf(lpar(argm(rpar(x))))));
  | (name) (expr) (body) (x)
    let nvar = Core.var(name)(Nat.zero)(Bool.false)
    let body = body(nvar)
    let lets = lit("let ")
    let name = lit(name)
    let eqls = lit(" = ")
    let expr = Core.stringify.go(expr)
    let spac = lit("; ")
    let body = Core.stringify.go(body)
    lets(name(eqls(expr(spac(body(x))))));
  | (done) (expr) (type) (x)
    let expr = Core.stringify.go(expr)
    let colo = lit(" :: ")
    let type = Core.stringify.go(type)
    expr(colo(type(x)));

Core.to_bits: Core -> Bits
  (term) Core.to_bits.go(term)(Nat.0)(Bool.false)(Bits.nil)

Core.to_bits.go: Core -> Nat -> Bool -> Bits -> Bits
  (term) (dep) (hash)
  term<() Bits -> Bits>
  | (name) (indx) (flip) (x) 
    let indx
      = flip<() Bits>
      | Nat.to_bits(Nat.sub(indx)(Nat.succ(dep)));
      | Nat.to_bits(indx);
    Bits.0(Bits.0(Bits.0(Bits.0(Bits.concat(indx)(x)))));
  | (name) (x) Bits.0(Bits.0(Bits.1(Bits.concat(String.to_bits(name))(x))));
  | (x) Bits.0(Bits.1(Bits.0(x)));
  | (eras) (self) (name) (bind) (body) (x)
    let bind = Core.to_bits.go(bind)(dep)(hash)
    let body = Core.to_bits.go
      | let svar = Core.var("")(dep)(hash)
        let nvar = Core.var("")(Nat.succ(dep))(hash)
        body(svar)(nvar);
      | Nat.succ(Nat.succ(dep));
      | hash;
    Bits.0(Bits.1(Bits.1(bind(body(x)))));
  | (eras) (name) (body) (x)
    let nvar = Core.var("")(dep)(hash)
    let body = Core.to_bits.go(body(nvar))(Nat.succ(dep))(hash)
    Bits.1(Bits.0(Bits.0(body(x))));
  | (eras) (func) (argm) (x)
    let func = Core.to_bits.go(func)(dep)(hash)
    let argm = Core.to_bits.go(argm)(dep)(hash)
    Bits.1(Bits.0(Bits.1(func(argm(x)))));
  | (name) (expr) (body) (x)
    let nvar = Core.var("")(dep)(hash)
    let expr = Core.to_bits.go(expr)(dep)(hash)
    let body = Core.to_bits.go(body(nvar))(Nat.succ(dep))(hash)
    Bits.1(Bits.1(Bits.0(expr(body(x)))));
  | (done) (expr) (type) (x)
    hash<() Bits>
    | Core.to_bits.go(expr)(dep)(hash)(x);
    | let expr = Core.to_bits.go(expr)(dep)(hash)
      let type = Core.to_bits.go(type)(dep)(hash)
      Bits.1(Bits.1(Bits.1(expr(type(x)))));;

Core.to_uid: Core -> Bits
  (term) Core.to_bits.go(term)(Nat.0)(Bool.true)(Bits.nil)

Core.typ: Core
  <> () () (typ) () () () () ()
  typ

Core.typecheck: Core -> Core -> Core.Defs -> Nat -> Either(String)(Core)
  (term) (type) (defs) (ctx)
  def bnd = Either.bind<Text><Core><Core>
  def err = Either.left<Text><Core>
  def ret = Either.right<Text><Core>
  def Ret = Either(Text)(Core)
  term<() Ret>
  |#var# () () ()
    Core.typecomp(term)(type)(defs)(ctx);
  |#ref# ()
    Core.typecomp(term)(type)(defs)(ctx);
  |#typ#
    Core.typecomp(term)(type)(defs)(ctx);
  |#all# () () () () ()
    Core.typecomp(term)(type)(defs)(ctx);
  |#lam# (term.eras) (term.name) (term.body)
    let typv = Core.reduce(type)(defs)
    Core.if_all(typv)<() Ret>
    |#none# err("Non-function application.");
    |#some# (got) got<Ret>
      | (typv.eras) (typv.self) (typv.name) (typv.bind) (typv.body)
      let self_var = Core.ann(Bool.true)(term)(type)
      let name_var = Core.ann(Bool.true)(Core.var(term.name)(Nat.succ(ctx))(Bool.false))(typv.bind)
      let body_typ = typv.body(self_var)(name_var)
      let body_ctx = Nat.succ(ctx)
      use _        = bnd(Core.typecheck(term.body(name_var))(body_typ)(defs)(body_ctx))
      ret(type);;;
  |#app# () () ()
    Core.typecomp(term)(type)(defs)(ctx);
  |#let# (term.name) (term.expr) (term.body)
    use expr_typ = bnd(Core.typeinfer(term.expr)(defs)(ctx))
    let expr_var = Core.ann(Bool.true)(term.expr)(expr_typ)
    let body_ctx = Nat.succ(ctx)
    Core.typecheck(term.body(expr_var))(type)(defs)(body_ctx);
  |#ann# () () ()
    Core.typecomp(term)(type)(defs)(ctx);

Core.typecomp: Core -> Core -> Core.Defs -> Nat -> Either(String)(Core)
  (term) (type) (defs) (ctx)
  let bnd = Either.bind<Text><Core><Core>
  let err = Either.left<Text><Core>
  let ret = Either.right<Text><Core>
  let Ret = Either(Text)(Core)
  bnd(Core.typeinfer(term)(defs)(ctx)) | (infr)
  Core.eql(type)(infr)(defs)<() Either(Text)(Core)>
  | ret(type);
  | let type_str = Core.stringify(Core.normalize(type)(Core.Defs.new))
    let infr_str = Core.stringify(Core.normalize(infr)(Core.Defs.new))
    let erro_str = "Type mismatch.\n"
    let erro_str = String.concat(erro_str)("Found type... \x1b[2m")
    let erro_str = String.concat(erro_str)(infr_str)
    let erro_str = String.concat(erro_str)("\x1b[0m\n")
    let erro_str = String.concat(erro_str)("Instead of... \x1b[2m")
    let erro_str = String.concat(erro_str)(type_str)
    let erro_str = String.concat(erro_str)("\x1b[0m\n")
    err(erro_str);;

Core.typeinfer: Core -> Core.Defs -> Nat -> Either(Text)(Core)
  (term) (defs) (ctx)
  def bnd = Either.bind<Text><Core><Core>
  def err = Either.left<Text><Core>
  def ret = Either.right<Text><Core>
  def Ret = Either(Text)(Core)
  term<() Ret>
  |#var# (term.name) (term.indx) (term.flip)
    ret(Core.var(term.name)(term.indx)(term.flip));
  |#ref# (term.name)
    Core.Defs.get_type(defs)(term.name)<() Ret>
    |#none# err(String.concat("Undefined reference: ")(term.name));
    |#some# (type) ret(type);;
  |#typ#
    ret(Core.typ);
  |#all# (term.eras) (term.self) (term.name) (term.bind) (term.body)
    let self_var = Core.ann(Bool.true)
      | Core.var(term.self)(ctx)(Bool.false);
      | term;
    let name_var = Core.ann(Bool.true)
      | Core.var(term.name)(Nat.succ(ctx))(Bool.false);
      | term.bind;
    let body_ctx = Nat.succ(ctx)
    let body_ctx = Nat.succ(ctx)
    let term_body = term.body(self_var)(name_var)
    use bind_typ = bnd(Core.typecheck(term.bind)(Core.typ)(defs)(ctx))
    use body_typ = bnd(Core.typecheck(term_body)(Core.typ)(defs)(ctx))
    ret(Core.typ);
  |#lam# (term.eras) (term.name) (term.body)
    err("Can't infer type.");
  |#app# (term.eras) (term.func) (term.argm)
    use func_typ = bnd(Core.typeinfer(term.func)(defs)(ctx))
    let func_typ = Core.reduce(func_typ)(defs)
    Core.if_all(func_typ)<() Ret>
    |#none# err("Non-function application.");
    |#some# (got) got<Ret>
      |#new# (func_typ.eras) (func_typ.self) (func_typ.name) (func_typ.bind) (func_typ.body)
        let self_var = Core.ann(Bool.true)(term.func)(func_typ)
        let name_var = Core.ann(Bool.true)(term.argm)(func_typ.bind)
        use bind_typ = bnd(Core.typecheck(term.argm)(func_typ.bind)(defs)(ctx))
        let term_typ = func_typ.body(self_var)(name_var)
        // TODO: check erasure
        ret(term_typ);;;
  |#let# (term.name) (term.expr) (term.body)
    use expr_typ = bnd(Core.typeinfer(term.expr)(defs)(ctx))
    let expr_var = Core.ann(Bool.true)(term.expr)(expr_typ)
    let body_ctx = Nat.succ(ctx)
    use body_typ = bnd(Core.typeinfer(term.body(expr_var))(defs)(body_ctx))
    ret(body_typ);
  |#ann# (term.done) (term.expr) (term.type)
    term.done<() Ret>
    | ret(term.type);
    | Core.typeinfer(term.expr)(defs)(ctx);;

Core.var: String -> Nat -> Bool -> Core
  (name) (indx) (flip)
  <> (var) () () () () () () ()
  var(name)(indx)(flip)