HVM3 CoC Superposer / Enumerator - nice state

coc_superposer.hvml

// Extending the CoC enumerator with more types (WIP)

data List {
  #Nil
  #Cons{head tail}
}

data Bits {
  #O{pred}
  #I{pred}
  #E
}

data Term {
  #Var{idx}     // Variable: `x`
  #Pol{bod}     // Polymorphic Type: `∀x bod`
  #All{inp bod} // Pi Type: `Π(x: inp) bod`
  #Lam{bod}     // Lambda: `λx(bod)`
  #App{fun arg} // Application: `(fun arg)`
  #U32          // Number Type: `U32`
  #Num{val}     // Number Value: `#123`
  #Emp          // Empty Type: `⊥`
  #Uni          // Unit Type: `⊤`
  #One          // Unit Value: `()`
  #Par{fst snd} // Pair Type: `&(fst snd)`
  #Tup{fst snd} // Pair Tuple: `[fst snd]`
  #Get{val bod} // Pair Projection: `! [x y] = val bod`
  #Eit{lft rgt} // Either Type: `|(lft rgt)`
  #Inl{val}     // Either Left: `#L{fst}`
  #Inr{val}     // Either Right: `#R{snd}`
  #Mat{val l r} // Either Match: `~ val { #L{x}:l #R{y}:r }`
}

data Pair {
  #Pair{fst snd}
}

data Maybe {
  #None
  #Some{value}
}

// Prelude
// -------

@if(c t f) = ~ c {
  0: f
  p: t
}

@when(c t) = ~ c {
  0: *
  p: t
}

@tail(xs) = ~ xs {
  #Nil: *
  #Cons{h t}: t
}

@and(a b) = ~ a !b {
  0: 0
  p: b
}

@unwrap(mb) = ~mb {
  #None: *
  #Some{x}: x
}

@seq(str) = ~ str {
  #Nil: #Nil
  #Cons{h t}:
    !! h = h
    !! t = @seq(t)
    #Cons{h t}
}

@tm0(x) = !&0{a b}=x a
@tm1(x) = !&0{a b}=x b

// Stringification
// ---------------

@show_nat(nat) = ~nat { 
  0: λk #Cons{'Z' k}
  p: λk #Cons{'S' (@show_nat(p) k)}
}

@show_dec(n r) =
  ! &{n n0} = n
  ! &{n n1} = n
  ! chr = (+ (% n 10) '0')
  ~ (< n0 10) !chr !r {
    0: @show_dec((/ n1 10) #Cons{chr r})
    t: #Cons{chr r}
  }

@do_show_dec(n) = @show_dec(n #Nil)

@show_bits(bits) = ~bits {
  #O{pred}: λk #Cons{'#' #Cons{'O' #Cons{'{' (@show_bits(pred) #Cons{'}' k})}}}
  #I{pred}: λk #Cons{'#' #Cons{'I' #Cons{'{' (@show_bits(pred) #Cons{'}' k})}}}
  #E: λk #Cons{'#' #Cons{'E' k}}
}

@do_show_bits(bits) = (@show_bits(bits) #Nil)

// Note: we currently use bruijn levels on the stringifier.
// So, for example, `λx λy x` is stringified as `λλ0` .
// And `Π(x: A) (B x)`  is stringified as `Π(A) (B x)`.
@show_term(term &dep) = ~term {
  #Var{idx}: λk
    @show_dec(idx k)
  #Pol{bod}: λk
    #Cons{'∀'
    (@show_term((bod #Var{&dep}) (+ &dep 1))
    k)}
  #All{inp bod}: λk
    #Cons{'Π'
    #Cons{'('
    (@show_term(inp &dep)
    #Cons{')'
    (@show_term((bod #Var{&dep}) (+ &dep 1))
    k)})}}
  #Lam{bod}: λk
    #Cons{'λ' (@show_term((bod #Var{&dep}) (+ &dep 1))
    k)}
  #App{fun arg}: λk
    #Cons{'('
    (@show_term(fun &dep)
    #Cons{' '
    (@show_term(arg &dep)
    #Cons{')'
    k})})}
  #U32: λk
    #Cons{'U'
    k}
  #Num{val}: λk
    #Cons{'#'
    @show_dec(val
    k)}
  #Emp: λk
    #Cons{'⊥' k}
  #Uni: λk
    #Cons{'⊤' k}
  #One: λk
    #Cons{'#'
    k}
  #Par{fst snd}: λk
    #Cons{'&'
    #Cons{'('
    (@show_term(fst &dep)
    #Cons{' '
    (@show_term(snd &dep)
    #Cons{')'
    k})})}}
  #Tup{fst snd}: λk
    #Cons{'['
    (@show_term(fst &dep)
    #Cons{' '
    (@show_term(snd &dep)
    #Cons{']'
    k})})}
  #Get{val bod}: λk
    #Cons{'!'
    (@show_term(val &dep)
    #Cons{' '
    (@show_term((bod #Var{&dep} #Var{(+ &dep 1)}) (+ &dep 2))
    k)})}
  #Eit{lft rgt}: λk
    #Cons{'|'
    #Cons{'('
    (@show_term(lft &dep)
    #Cons{' '
    (@show_term(rgt &dep)
    #Cons{')'
    k})})}}
  #Inl{val}: λk
    #Cons{'<'
    (@show_term(val &dep)
    k)}
  #Inr{val}: λk
    #Cons{'>'
    (@show_term(val &dep)
    k)}
  #Mat{val l r}: λk
    #Cons{'~'
    (@show_term(val &dep)
    #Cons{'{'
    (@show_term((l #Var{&dep}) (+ &dep 1))
    #Cons{'|'
    (@show_term((r #Var{&dep}) (+ &dep 1))
    #Cons{'}'
    k})})})}
}

@do_show_term(term) = (@show_term(term 0) #Nil)

// Equality
// --------

@eq(a b &dep) = ~ @wnf(a) !b {
  #Var{a_idx}: ~ @wnf(b) {
    #Var{b_idx}:
      (== a_idx b_idx)
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Pol{a_bod}: ~ @wnf(b) {
    #Pol{b_bod}:
      ! e_bod = @eq(
        (a_bod #Var{&dep})
        (b_bod #Var{&dep})
        (+ &dep 1))
      e_bod
    #Var{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #All{a_inp a_bod}: ~ @wnf(b) {
    #All{b_inp b_bod}:
      ! e_inp = @eq(a_inp b_inp &dep)
      ! e_bod = @eq(
        (a_bod #Var{&dep})
        (b_bod #Var{&dep})
        (+ &dep 1))
      @and(e_inp e_bod)
    #Var{_}     : 0
    #Pol{_}     : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Lam{a_bod}: ~ @wnf(b) {
    #Lam{b_bod}:
      ! e_bod = @eq(
        (a_bod #Var{&dep})
        (b_bod #Var{&dep})
        (+ &dep 1))
      e_bod
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #App{a_fun a_arg}: ~ @wnf(b) {
    #App{b_fun b_arg}:
      ! e_fun = @eq(a_fun b_fun &dep)
      ! e_arg = @eq(a_arg b_arg &dep)
      @and(e_fun e_arg)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #U32: ~ @wnf(b) {
    #U32:
      1
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Num{a_val}: ~ @wnf(b) {
    #Num{b_val}:
      (== a_val b_val)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Par{a_fst a_snd}: ~ @wnf(b) {
    #Par{b_fst b_snd}:
      ! e_fst = @eq(a_fst b_fst &dep)
      ! e_snd = @eq(a_snd b_snd &dep)
      @and(e_fst e_snd)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Emp: ~ @wnf(b) {
    #Emp: 1
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Uni: ~ @wnf(b) {
    #Uni: 1
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #One: ~ @wnf(b) {
    #One: 1
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Tup{a_fst a_snd}: ~ @wnf(b) {
    #Tup{b_fst b_snd}:
      ! e_fst = @eq(a_fst b_fst &dep)
      ! e_snd = @eq(a_snd b_snd &dep)
      @and(e_fst e_snd)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Get{a_val a_bod}: ~ @wnf(b) {
    #Get{b_val b_bod}:
      ! e_val = @eq(a_val b_val &dep)
      ! e_bod = @eq(
        (a_bod #Var{&dep} #Var{(+ &dep 1)})
        (b_bod #Var{&dep} #Var{(+ &dep 1)})
        (+ &dep 2))
      @and(e_val e_bod)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Eit{a_lft a_rgt}: ~ @wnf(b) {
    #Eit{b_lft b_rgt}:
      ! e_lft = @eq(a_lft b_lft &dep)
      ! e_rgt = @eq(a_rgt b_rgt &dep)
      @and(e_lft e_rgt)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Inl{a_val}: ~ @wnf(b) {
    #Inl{b_val}:
      @eq(a_val b_val &dep)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inr{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Inr{a_val}: ~ @wnf(b) {
    #Inr{b_val}:
      @eq(a_val b_val &dep)
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Mat{_ _ _} : 0
  }
  #Mat{a_val a_l a_r}: ~ @wnf(b) {
    #Mat{b_val b_l b_r}:
      ! e_val = @eq(a_val b_val &dep)
      ! e_l = @eq((a_l #Var{&dep}) (b_l #Var{&dep}) (+ &dep 1))
      ! e_r = @eq((a_r #Var{&dep}) (b_r #Var{&dep}) (+ &dep 1))
      @and(e_val @and(e_l e_r))
    #Var{_}     : 0
    #Pol{_}     : 0
    #All{_ _}   : 0
    #Lam{_}     : 0
    #App{_ _}   : 0
    #U32        : 0
    #Num{_}     : 0
    #Emp        : 0
    #Uni        : 0
    #One        : 0
    #Par{_ _}   : 0
    #Tup{_ _}   : 0
    #Get{_ _}   : 0
    #Eit{_ _}   : 0
    #Inl{_}     : 0
    #Inr{_}     : 0
  }
}

// Evaluation
// ----------

@wnf(term) = ~ term { 
  #Var{idx}: #Var{idx}
  #Pol{bod}: #Pol{bod}
  #All{inp bod}: #All{inp bod}
  #Lam{bod}: #Lam{bod}
  #App{fun arg}: @wnf_app(@wnf(fun) arg)
  #U32: #U32
  #Num{val}: #Num{val}
  #Emp: #Emp
  #Uni: #Uni
  #One: #One
  #Par{fst snd}: #Par{fst snd}
  #Tup{fst snd}: #Tup{fst snd}
  #Get{val bod}: @wnf_get(@wnf(val) bod)
  #Eit{lft rgt}: #Eit{lft rgt}
  #Inl{val}: #Inl{val}
  #Inr{val}: #Inr{val}
  #Mat{val l r}: @wnf_mat(@wnf(val) l r)
}

@wnf_app(f x) = ~ f !x {
  #Var{idx}: #App{#Var{idx} x}
  #Pol{bod}: #App{#Pol{bod} x}
  #All{inp bod}: #App{#All{inp bod} x}
  #Lam{bod}: @wnf((bod @wnf(x)))
  #App{fun arg}: #App{#App{fun arg} x}
  #U32: #U32
  #Num{val}: #App{#Num{val} x}
  #Emp: #App{#Emp x}
  #Uni: #App{#Uni x}
  #One: #App{#One x}
  #Par{fst snd}: #App{#Par{fst snd} x}
  #Tup{fst snd}: #App{#Tup{fst snd} x}
  #Get{val bod}: #App{#Get{val bod} x}
  #Eit{lft rgt}: #App{#Eit{lft rgt} x}
  #Inl{val}: #App{#Inl{val} x}
  #Inr{val}: #App{#Inr{val} x}
  #Mat{val l r}: #App{#Mat{val l r} x}
}

@wnf_get(v b) = ~ v !b {
  #Tup{fst snd}: @wnf((b fst snd))
  #Var{idx}: #Get{#Var{idx} b}
  #Pol{bod}: #Get{#Pol{bod} b}
  #All{inp bod}: #Get{#All{inp bod} b}
  #Lam{bod}: #Get{#Lam{bod} b}
  #App{fun arg}: #Get{#App{fun arg} b}
  #U32: #Get{#U32 b}
  #Num{val}: #Get{#Num{val} b}
  #Emp: #Get{#Emp b}
  #Uni: #Get{#Uni b}
  #One: #Get{#One b}
  #Par{fst snd}: #Get{#Par{fst snd} b}
  #Get{val bod}: #Get{#Get{val bod} b}
  #Eit{lft rgt}: #Get{#Eit{lft rgt} b}
  #Inl{val}: #Get{#Inl{val} b}
  #Inr{val}: #Get{#Inr{val} b}
  #Mat{val l r}: #Get{#Mat{val l r} b}
}

@wnf_mat(v l r) = ~ v !l !r {
  #Inl{val}: @wnf((l val))
  #Inr{val}: @wnf((r val))
  #Var{idx}: #Mat{#Var{idx} l r}
  #Pol{bod}: #Mat{#Pol{bod} l r}
  #All{inp bod}: #Mat{#All{inp bod} l r}
  #Lam{bod}: #Mat{#Lam{bod} l r}
  #App{fun arg}: #Mat{#App{fun arg} l r}
  #U32: #Mat{#U32 l r}
  #Num{val}: #Mat{#Num{val} l r}
  #Emp: #Mat{#Emp l r}
  #Uni: #Mat{#Uni l r}
  #One: #Mat{#One l r}
  #Par{fst snd}: #Mat{#Par{fst snd} l r}
  #Tup{fst snd}: #Mat{#Tup{fst snd} l r}
  #Get{val bod}: #Mat{#Get{val bod} l r}
  #Eit{lft rgt}: #Mat{#Eit{lft rgt} l r}
  #Mat{val l2 r2}: #Mat{#Mat{val l2 r2} l r}
}

// Normalization
// -------------

@nf(t &dep) = ~ @wnf(t) {
  #Var{idx}: #Var{idx}
  #Pol{bod}: #Pol{λx @nf((bod #Var{&dep}) (+ &dep 1))}
  #All{inp bod}: #All{@nf(inp &dep) λx @nf((bod #Var{&dep}) (+ &dep 1))}
  #Lam{bod}: #Lam{λx @nf((bod #Var{&dep}) (+ &dep 1))}
  #App{fun arg}: #App{@nf(fun &dep) @nf(arg &dep)}
  #U32: #U32
  #Num{val}: #Num{val}
  #Emp: #Emp
  #Uni: #Uni
  #One: #One
  #Par{fst snd}: #Par{@nf(fst &dep) @nf(snd &dep)}
  #Tup{fst snd}: #Tup{@nf(fst &dep) @nf(snd &dep)}
  #Get{val bod}: #Get{@nf(val &dep) λx λy @nf((bod #Var{&dep} #Var{(+ &dep 1)}) (+ &dep 2))}
  #Eit{lft rgt}: #Eit{@nf(lft &dep) @nf(rgt &dep)}
  #Inl{val}: #Inl{@nf(val &dep)}
  #Inr{val}: #Inr{@nf(val &dep)}
  #Mat{val l r}: #Mat{@nf(val &dep) λx @nf((l #Var{&dep}) (+ &dep 1)) λx @nf((r #Var{&dep}) (+ &dep 1))}
}

// Enumeration
// -----------

@all(&L typ &dep ctx) =
  !&L{typL typR} = typ
  !&L{ctxL ctxR} = ctx
  &L{
    @intr(&L typL &dep ctxL)
    @pick(&L typR &dep ctxR λk(k))
  }

@intr(&L typ &dep ctx) = 
//! &{typD typ} = typ
//! &{ctxD ctx} = ctx
//!! typD = typD
//!! &dep = &dep
//!! @LOG([1 typD &dep ctxD])
~ typ !ctx {
  #Pol{t_bod}:
    @intr(&L (t_bod #Var{&dep}) (+ &dep 1) ctx)
  #All{t_inp t_bod}: 
    !&0{ctx bod} = @all(&L (t_bod #Var{&dep}) (+ &dep 1) #Cons{#Some{&0{$x t_inp}} ctx})
    &0{@tail(ctx) #Lam{λ$x(bod)}}
  #Uni:
    &0{ctx #One}
  #Par{fst snd}:
    !&0{ctx tm0} = @all((+(*&L 2)0) fst &dep ctx)
    !&0{ctx tm1} = @all((+(*&L 2)1) snd &dep ctx)
    &0{ ctx #Tup{tm0 tm1} }
  #Eit{lft rgt}:
    !&L{ctxL ctxR} = ctx
    !&0{ctxL valL} = @all(&L lft &dep ctxL)
    !&0{ctxR valR} = @all(&L rgt &dep ctxR)
    &L{
      &0{ ctxL #Inl{valL} }
      &0{ ctxR #Inr{valR} }
    }
  #U32: *
  #Var{idx}: *
  #App{fun arg}: *
  #Emp: *
  #Lam{_}: *
  #Num{_}: *
  #Tup{_ _}: *
  #Get{_ _}: *
  #Inl{_}: *
  #Inr{_}: *
  #Mat{_ _ _}: *
  #One: *
}

@pick(&L typ &dep ctx rem) = 
//! &{typD typ} = typ
//! &{ctxD ctx} = ctx
//!! typD = typD
//!! &dep = &dep
//!! @LOG([2 typD &dep ctxD])
~ ctx {
  #Nil: *
  #Cons{ann ctx}:
    ! &L{typL typR} = typ
    ! &L{remL remR} = rem
    ! &L{annL annR} = ann
    ! &L{ctxL ctxR} = ctx
    &L{
      @open(&L typL &dep (remL #Cons{#None ctxL}) annL)
      @pick(&L typR &dep ctxR λk(remR #Cons{annR k}))
    }
}

@open(&L typ &dep ctx ann) = ~ ann {
  #None: *
  #Some{ann}:
    ! &0{xtm  xty}  = ann
    ! &L{typ  typE} = typ
    ! &L{xty  xtyE} = xty
    ! &L{ctxL ctxR} = ctx
    ! &L{xtmL xtmR} = xtm
    &L{
      @when(@eq(typE xtyE &dep) &0{ctxL xtmL})
      @elim(&L typ &dep ctxR xtmR xty)
    }
}

@elim(&L typ &dep ctx xtm xty) = ~ xty !typ !ctx !xtm {
  #Pol{xty_bod}:
    ! &{typ0 typ1} = typ
    @open(&L typ0 &dep ctx #Some{&0{xtm (xty_bod typ1)}})
  #All{xty_inp xty_bod}:
    ! &0{ctx arg} = @all((+ (* &L 2)1) xty_inp &dep ctx)
    ! &{arg0 arg1} = arg
    @open((+(*&L 2)0) typ &dep ctx #Some{&0{#App{xtm arg0} (xty_bod arg1)}})
  #Par{xty_fst xty_snd}:
    ! ctx = #Cons{#Some{&0{$y xty_snd}} #Cons{#Some{&0{$x xty_fst}} ctx}}
    ! &0{ctx bod} = @all(&L typ (+ &dep 2) ctx)
    &0{@tail(@tail(ctx)) #Get{xtm λ$x λ$y (bod)}}
  #Eit{xty_lft xty_rgt}:
    ! &{typ0 typ1} = typ
    ! &0{ctx l} = @all((+(*&L 2)0) typ0 (+ &dep 1) #Cons{#Some{&0{$xl xty_lft}} ctx})
    ! &0{ctx r} = @all((+(*&L 2)1) typ1 (+ &dep 1) #Cons{#Some{&0{$xr xty_rgt}} @tail(ctx)}) // <- subtle
    &0{@tail(ctx) #Mat{xtm λ$xl(l) λ$xr(r)}}
  #Uni: *
  #Emp: *
  #U32: *
  #Var{idx}: *
  #App{fun arg}: *
  #Get{val bod}: *
  #Mat{val l r}: *
  #One: *
  #Tup{fst snd}: *
  #Inl{val}: *
  #Inr{val}: *
  #Lam{_}: *
  #Num{_}: *
}

@enum(t) = @tm1(@all(1 t 0 #Nil))

// Tests
// -----

// A -> B
@Fun(A B) = #All{A λx(B)}

// T0 = Π(x:U32) Π(y:U32) Π(z:U32) U32
@T0 =
  #All{#U32 λx
  #All{#U32 λy
  #All{#U32 λz
  #U32}}}

// CBool = ∀P Π(x:P) Π(y:P) P
@CBool =
  #Pol{λp
  !&{p p0}=p
  !&{p p1}=p
  !&{p p2}=p
  #All{p0 λx
  #All{p1 λy
  p2}}}

// CT = λt λf t
@CT =
  #Lam{λt
  #Lam{λf
  t}}

// CF = λt λf f
@CF =
  #Lam{λt
  #Lam{λf
  f}}

// Tup(A B) = ∀P Π(p: Π(x:A) Π(y:B) P) P
@Tup(A B) =
  #Pol{λp
  !&{p p0}=p
  !&{p p1}=p
  #All{
    #All{A λx
    #All{B λy
    p0}} λp
  p1}}

// TupF = ∀A Π(x: (Tup A A)) (Tup A A)
@TupF =
  #Pol{λA
  #Pol{λB
  !&{A A0}=A
  !&{A A1}=A
  !&{A A2}=A
  !&{A A3}=A
  #All{@Tup(A0 A1) λx
  @Tup(A2 A3)}}}

// Solves for `?X` in `(?X λt(t A B)) == λt(t B A)`. (3k interactions)
//@A    = #Lam{λt #App{#App{t #Num{1}} #Num{2}}}
//@B    = #Lam{λt #App{#App{t #Num{2}} #Num{1}}}
//@R    = #Lam{λx #App{x #Lam{λa #Lam{λb #Lam{λt #App{#App{t b} a}}}}}}
//@T    = @TupF
//@X    = @enum(@T)
//@main = @when(@eq(#App{@X @A} @B 0) @do_show_term(@X))

//@main = @do_show_term(@enum(@Tup(@CBool @CBool)))

//@main = @do_show_term(@enum(
  //#All{@CBool λx
  //#All{@CBool λy
  //#All{@CBool λz
  //@CBool}}}))

@Bit = #Eit{#Uni #Uni}
@B0  = #Inl{#One}
@B1  = #Inr{#One}
@Not = #Lam{λx #Mat{x λx(@B1) λx(@B0)}}

@Bit2 = #Par{@Bit @Bit}
@Bit4 = #Par{@Bit2 @Bit2}

// Natural Numbers
@Nat = #Eit{#Uni @Nat}

//@Term = @Fun(@Bit @Bit)
@Term = @Fun(@Bit @Fun(#Uni @Fun(@Bit @Bit)))
//@Term = @Fun(#Uni @Fun(#Uni #Uni))



// MAIN
@main = @do_show_term(@enum(@Nat))
//@main = @enum(@Term)



//@main = @eq(@enum(@Term) #Lam{0} 0)