open Js
Console.log("hellosu")

// Disable warning about the same constructor for different types
@@warning("-30")
type rec term =
  | Unit // ()
  | Var(string) // x
  | Lam(string, term) // λx.e
  | App(term, term) // e e
  | Annot(term, typ) // (e : A)
and typ =
  | Unit // 1
  | Var(string) // α
  | Existential(string) // â
  | Polytype(string, typ) // ∀α.A
  | Arrow(typ, typ) // A -> B
and monotyp =
  // Unit monotype
  | Unit // 1
  | Var(string) // α
  | Existential(string) // â
  | Arrow(monotyp, monotyp) // τ -> σ
type rec contextEntry =
  | TypeVar(string) // Γ,α
  | TermAnnot(string, typ) // Γ,x:A
  | ExistentialVar(string) // Γ,â
  | ExistentialSolved(string, monotyp) // Γ,â=τ
  | Marker(string) // Γ,🢒â
type rec completeContextEntry =
  | TypeVar(string) // Ω,α
  | TermAnnot(string, typ) // Ω,x:A
  | ExistentialSolved(string, monotyp) // Ω,â=τ
  | Marker(string) // Ω,🢒â
type context = list<contextEntry>
@@warning("+30")
/** Context lookup */
let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): typ => {
  switch ctx {
  | list{} => failwith("L")
  | list{TermAnnot(n, t), ..._} if n == name => t
  | list{_, ...rest} => lookupTypeVariable(rest, name)
  }
}

open Belt
open Data
let _genSymCtr = ref(0)
let genSym = (~prefix="var", ()): string => {
  let num = _genSymCtr.contents
  _genSymCtr := num + 1
  `${prefix}${Int.toString(num)}`
}
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
  | (Unit, Unit) => Ok(ctx)
  // ∀I rule
  | (e, Polytype(x, tyA)) => failwith("TODO")
  // →I rule
  | (Lam(x, e), Arrow(tyA, tyB)) =>
    let augmentedCtx = ctx->List.add(TermAnnot(x, tyA))
    typecheck(augmentedCtx, e, tyB)->Result.map(_ => ctx)
  // Sub rule
  // TODO: Subtyping rule???
  | (Var(_) | Lam(_, _) | App(_, _) | Annot(_, _), _) => failwith("TODO")
  | _ => Error("could not resolve")
  }
}
and synthesize = (ctx: context, term: term): result<(typ, context), string> => {
  switch term {
  // Var rule
  | Var(name) => Ok(lookupTypeVariable(ctx, name), ctx)
  // 1I⇒ rule
  | Unit => Ok(Unit, ctx)
  // 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", ())
    Ok(Arrow(Existential(exA), Existential(exB)), ctx)
  // →E rule
  | App(e1, e2) => failwith("TODO")
  }
}
and appSynthesize = (ctx: context, funTy: typ, term: term): result<(typ, context), string> => {
  switch (funTy, term) {
  // →App rule
  | (Arrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx))
  // ∀App rule
  | (Polytype(a, tyA), e) => failwith("TODO")
  // âApp rule
  | (Existential(_), _) => failwith("TODO")
  | (Unit | Var(_), _) => Error("trying to appSynthesize with a non-function type")
  }
}
// Figure 8. Applying a context, as a substitution, to a type
let rec applyContext = (ctx: context, typ: typ): typ => {
  switch typ {
  | Unit => Unit
  | Var(x) => Var(x)
  | Existential(_) => failwith("TODO")
  | Polytype(_) => failwith("TODO")
  | Arrow(a, b) => Arrow(applyContext(ctx, a), applyContext(ctx, b))
  }
}

{
  "scripts": {
    "res:build": "rescript",
    "res:dev": "rescript build -w"
  },
  "devDependencies": {
    "rescript": "^10.1.4"
  }
}

{
  "name": "your-project-name",
  "sources": [
    {
      "dir": "src",
      "subdirs": true
    }
  ],
  "package-specs": [
    {
      "module": "es6",
      "in-source": true
    }
  ],
  "suffix": ".bs.js",
  "bs-dependencies": []
}

_build

_build
*.bs.js
node_modules
lib/bs