open Belt
open Data
let _genSymCtr = ref(0)
let genSym = (~prefix="var", ()): string => {
  let num = _genSymCtr.contents
  _genSymCtr := num + 1
}
let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result<context, string> => {
  switch (tyA, tyB) {
  | (_, _) => failwith("TODO")
  }
}
and typecheck = (ctx: context, term: term, typ: typ): result<context, string> => {
  switch (term, typ) {
  // 1I rule
  // ∀I rule
  // →I rule
    let augmentedCtx = ctx->List.add(TermAnnot(x, tyA))
    typecheck(augmentedCtx, e, tyB)->Result.map(_ => ctx)
  // Sub rule
  }
}
and synthesize = (ctx: context, term: term): result<(typ, context), string> => {
  switch term {
  // Var rule
  // 1I⇒ rule
  // Anno rule
  | Annot(e, tyA) => typecheck(ctx, e, tyA)->Result.map(ctx => (tyA, ctx))
  // →I⇒ rule
  | Lam(x, e) =>
    // TODO: Check x and e
    let exA = genSym(~prefix="ex", ())
    let exB = genSym(~prefix="ex", ())
  // →E rule
  }
}
and appSynthesize = (ctx: context, funTy: typ, term: term): result<(typ, context), string> => {
  switch (funTy, term) {
  // →App rule
  // ∀App rule
  // âApp rule
  }
}
// Figure 8. Applying a context, as a substitution, to a type
  switch typ {
  }
}
  | TUnit => TUnit
  | TVar(x) => TVar(x)
  | TExistential(_) => failwith("TODO")
  | TPolytype(_) => failwith("TODO")
  | TArrow(a, b) => TArrow(applyContext(ctx, a), applyContext(ctx, b))
and applyContext = (ctx: context, typ: typ): typ => {
  | (TUnit | TVar(_), _) => Error("trying to appSynthesize with a non-function type")
  | (TExistential(_), _) => failwith("TODO")
  | (TPolytype(a, tyA), e) => failwith("TODO")
  | (TArrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))
  | App(e1, e2) => synthesize(ctx, e1)->Result.flatMap(((tyA, ctx)) => appSynthesize(ctx, tyA, e2))
    let augmentedCtx = list{TermAnnot(x, TVar(exA)), TypeVar(exB), TypeVar(exA), ...ctx}
    typecheck(augmentedCtx, e, TVar(exB))->Result.map(_ => (
      TArrow(TExistential(exA), TExistential(exB)),
      ctx,
    ))
  | Unit => Ok(TUnit, ctx)
  | Var(name) => lookupTypeVariable(ctx, name)->Result.map(ty => (ty, ctx))
  | (_, _) =>
    let tyA = synthesize(ctx, term)
    let tyA' = applyContext(ctx, tyA)
  | (Lam(x, e), TArrow(tyA, tyB)) =>
  | (e, TPolytype(x, tyA)) => failwith("TODO ∀I-rule")
  | (Unit, TUnit) => Ok(ctx)
  `${prefix}${num->Int.toString}`

type rec term =
  | Unit // ()
  | Var(string) // x
  | Lam(string, term) // λx.e
  | App(term, term) // e e
  | Annot(term, typ) // (e : A)
and typ =
and monotyp =
  // Unit monotype
type rec contextEntry =
  | TypeVar(string) // Γ,α
  | TermAnnot(string, typ) // Γ,x:A
  | ExistentialVar(string) // Γ,â
  | ExistentialSolved(string, monotyp) // Γ,â=τ
  | Marker(string) // Γ,🢒â
type rec completeContextEntry =
type context = list<contextEntry>
/** Context lookup */
  switch ctx {
  | list{_, ...rest} => lookupTypeVariable(rest, name)
  }
}
  | list{} => Error(`could not find name ${name}`)
  | list{TermAnnot(n, t), ..._} if n == name => Ok(t)
let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): result<typ, string> => {
  | CCTypeVar(string) // Ω,α
  | CCTermAnnot(string, typ) // Ω,x:A
  | CCExistentialSolved(string, monotyp) // Ω,â=τ
  | CCMarker(string) // Ω,🢒â
  | MUnit // 1
  | MVar(string) // α
  | MExistential(string) // â
  | MArrow(monotyp, monotyp) // τ -> σ
  | TUnit // 1
  | TVar(string) // α
  | TExistential(string) // â
  | TPolytype(string, typ) // ∀α.A
  | TArrow(typ, typ) // A -> B

open Js
Console.log("hellosu")

J : {A : Set}
  → (C : (x y : A) → x ≡ y → Set)
  → (c : (x : A) → C x x refl)
  → (x y : A) → (p : x ≡ y) → C x y p
J C c x x refl = c x
inv : {A : Set} {a b : A}
  → (d : a ≡ b)
  → sym (sym d) ≡ d
inv {A} {a} {b} d = 
    J (λ x y p → sym (sym p) ≡ p  ) (λ x → refl) a b d
-- Problem 2
assoc : {A : Set} {a b c d : A}
  → (e : a ≡ b)
  → (f : b ≡ c)
  → (g : c ≡ d)
  → trans (trans e f) g ≡ trans e (trans f g)
assoc {a} {b} {c} {d} e f g =
  let whatever = J {!   !} {!   !} {!   !} {!   !} {!   !} in
  {!   !}
-- Problem 6
-- id : {A : Set} → (a : A) → a ≡ a
-- id a = refl
-- interchange : {A : Set}
--   → (a : A)
--   → (d : id a ≡ id a)
--   → (e : id a ≡ id a)
--   → trans d e ≡ trans e d
-- interchange a d e =
--   let transde = trans d e in
--   let transed = trans e d in
--   let tmpl = J (λ x y p → {!   !}) (λ x → {!   !}) (id a) (id a) transde in
--   {!   !}