// Types
// -----

data Maybe
  = (Some value)
  | None

data Bool
  = False
  | True

data Term
  = (All inp bod)
  | (Lam bod)
  | (App fun arg)
  | (Ann val typ)
  | (Slf bod)
  | (Ins val)
  | (Ref nam val)
  | (Set)
  | (Var idx) 

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

(And a b) = match a {
  True: b
  False: False
}

(Or a b) = match a {
  True: True
  False: b
}

(U60.show n) = (U60.show.go n SNil)
(U60.show.go n res) = match k = (< n 10) {
  0: (U60.show.go (/ n 10) (SCons (+ '0' (% n 10)) res))
  +: (SCons (+ '0' n) res)
}

(Same SNil         SNil)         = 1
(Same SNil         (SCons y ys)) = 0
(Same (SCons x xs) SNil)         = 0
(Same (SCons x xs) (SCons y ys)) = (& (== x y) (Same xs ys))

(Find name LNil)                   = None
(Find name (LCons (nam,val) tail)) = match (Same nam name) { True: (Some val); False: (Find name tail) }

(Concat SNil         ys) = ys
(Concat (SCons x xs) ys) = (SCons x (Concat xs ys))

(Join LNil)         = ""
(Join (LCons x xs)) = (Concat x (Join xs))

(Fst (fst,snd)) = fst
(Snd (fst,snd)) = snd

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

(Reduce x) = match x {
  App: (APP x.fun x.arg)
  Ann: (Reduce x.val)
  Ins: (Reduce x.val)
  Ref: (Reduce x.val)
  val: val
}

(APP fun arg) = match fun = (Reduce fun) {
  Lam: (Reduce (fun.bod arg))
  fun: (App fun arg)
}

(Normal term dep) = (Normal.go (Reduce term) dep)

(Normal.go term dep) = match term {
  All: (All (Normal term.inp dep) λx (Normal (term.bod (Var dep)) (+ dep 1)))
  Lam: (Lam λx (Normal (term.bod (Var dep)) (+ 1 dep)))
  App: (App (Normal term.fun dep) (Normal term.arg dep))
  Ann: (Ann (Normal term.val dep) (Normal term.typ dep))
  Slf: (Slf λx (Normal (term.bod (Var dep)) (+ 1 dep)))
  Ins: (Ins (Normal term.val dep))
  Ref: (Ref term.nam (Normal term.val dep))
  Set: Set
  Var: (Var term.idx)
}

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

// This linear equality attempts to avoid reducing the term to normal form, and
// cloning it, while still being able to identify as many terms as possible.

(Equal a b dep) = match a {
  All: match b {
    All: (And (Equal a.inp b.inp dep) (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep)))
    Ann: (Equal (All a.inp a.bod) b.val dep)
    Ref: (Equal (All a.inp a.bod) b.val dep)
    App: (Equal (App b.fun b.arg) (All a.inp a.bod) dep)
    exp: 0
  }
  Lam: match b {
    Lam: (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep))
    Ann: (Equal (Lam a.bod) b.val dep)
    Ref: (Equal (Lam a.bod) b.val dep)
    App: (Equal (App b.fun b.arg) (Lam a.bod) dep)
    exp: 0
  }
  App: match a = (APP a.fun a.arg) {
    App: match b {
      App: (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
      Ann: (Equal (App a.fun a.arg) b.val dep)
      Ref: (Equal (App a.fun a.arg) b.val dep)
      exp: 0
    }
    exp: (Equal exp b dep)
  }
  Ann: (Equal a.val b dep)
  Slf: match b {
    Slf: (Equal (a.bod (Var dep)) (b.bod (Var dep)) (+ 1 dep))
    Ann: (Equal (Slf a.bod) b.val dep)
    Ref: (Equal (Slf a.bod) b.val dep)
    App: (Equal (App b.fun b.arg) (Slf a.bod) dep)
    exp: 0
  }
  Ins: match b {
    Ins: (Equal a.val b.val dep)
    Ann: (Equal (Ins a.val) b.val dep)
    Ref: (Equal (Ins a.val) b.val dep)
    App: (Equal (App b.fun b.arg) (Ins a.val) dep)
    exp: 0
  }
  Ref: match b {
    Ref: (Same a.nam b.nam) // TODO: use uids
    Ann: (Equal (Ref a.nam a.val) b.val dep)
    App: (Equal (App b.fun b.arg) (Ref a.nam a.val) dep)
    exp: (Equal a.val exp dep)
  }
  Set: match b {
    Set: True
    Ann: (Equal Set b.val dep)
    Ref: (Equal Set b.val dep)
    App: (Equal (App b.fun b.arg) Set dep)
    exp: 0
  }
  Var: match b {
    Var: (== a.idx b.idx)
    Ann: (Equal (Var a.idx) b.val dep)
    Ref: (Equal (Var a.idx) b.val dep)
    App: (Equal (App b.fun b.arg) (Var a.idx) dep)
    exp: 0
  }
}

// Logger
// -------

//Logger r = ∀(logs: [String]) ([String], (Maybe r))

(pure x) = λlogs (logs, (Some x))

(bind a b) = λlogs
  let (a_logs, a_result) = (a logs)
  match a_result {
    None: (a_logs, None)
    Some: (b a_result.value a_logs)
  }

(exit) = λlogs (logs, None)

(log msg) = λlogs ((LCons msg logs), (Some 0))

// Type-Checking
// -------------

(Infer term dep) =
  //(bind (log (Join ["Infer: " (Show term dep)])) λx
  match term {
    All:
      (bind (Check term.inp Set dep) λinp_ty
      (bind (Check (term.bod (Ann (Var dep) term.inp)) Set (+ 1 dep)) λbod_ty
      (pure Set)))
    Lam:
      exit
    App:
      (bind (Infer term.fun dep) λfun_ty
      match fun_ty = (Reduce fun_ty) {
        All:
          (bind (Check term.arg fun_ty.inp dep) λval_ty
          (pure (fun_ty.bod term.arg)))
        Val:
          exit
      })
    Ann: (pure term.typ)
    Slf:
      (bind (Check (term.bod (Ann (Var dep) (Slf term.bod))) Set (+ dep 1)) λslf
      (pure Set))
    Ins:
      (bind (Infer term.val dep) λval_ty
      match val_ty = (Reduce val_ty) {
        Slf: (val_ty.bod (Ins term.va))
        var: exit
      })
    Ref: (Infer term.val dep)
    Set: (pure Set)
    Var: exit
  }
  //)

(Check term type dep) =
  (bind (log (Join ["Check: " (Show term dep) " :: " (Show type dep)])) λx
  match term {
    Lam: match type = (Reduce type) {
      All:
        let ann  = (Ann (Var dep) type.inp)
        let term = (term.bod ann)
        let type = (type.bod ann)
        (Check term type (+ dep 1))
      val:
        exit
    }
    Ins: match type = (Reduce type) {
      Slf: (Check term.val (type.bod (Ins term.val)) dep)
      val: exit
    }
    Ref: (Check term.val type dep)
    val: 
      (bind (Infer val dep) λinfer
      (bind (log (Join ["Equal: " (Show type dep) " == " (Show infer dep) " at " (U60.show dep)])) λx
      match (Equal type infer dep) {
      //match 1 {
        0: exit
        +: (pure (Ref "OK" (Var 0)))
      }))
  }
  )

// Syntax
// ------

(Show term dep) = match term {
  All: (Join ["∀(x" (U60.show dep) ":" (Show term.inp dep) ") " (Show (term.bod (Var dep)) (+ dep 1))])
  Lam: (Join ["λx" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
  App: (Join ["(" (Show term.fun dep) " " (Show term.arg dep) ")"])
  Ann: (Join ["{" (Show term.val dep) ":" (Show term.typ dep) "}"])
  Slf: (Join ["$x" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
  Ins: (Join ["~" (Show term.val dep)])
  Ref: term.nam
  Set: (Join ["*"])
  Var: (Join ["x" (U60.show term.idx)])
}

(Char.is_space chr) =
  (| (== chr ' ') (== chr '\n'))

(Char.is_name chr) =
  (| (& (>= chr 'a') (<= chr 'z'))
  (| (& (>= chr 'A') (<= chr 'Z'))
  (| (& (>= chr '0') (<= chr '9'))
  (| (== chr '_') (== chr '.')))))

(Parse.skip code) = match code {
  SNil: SNil
  SCons: match is_space = (Char.is_space code.head) {
    0: (SCons code.head code.tail)
    +: (Parse.skip code.tail)
  }
}

(Parse.name code) =
  (Parse.name.go (Parse.skip code))

(Parse.name.go code) = match code {
  SNil: ("", "")
  SCons: match isnm = (Char.is_name code.head) {
    0: ((SCons code.head code.tail), "")
    +: 
      let (code, name) = (Parse.name.go code.tail)
      (code, (SCons code.head name))
  }
}

(Parse.text code text) =
  let code = (Parse.skip code)
  match text {
    SNil: (code, True)
    SCons: match code {
      SNil: ("", False)
      SCons: match ok = (== text.head code.head) {
        0: ("", False)
        +: (Parse.text code.tail text.tail)
      }
    }
  }

(Parse.header code headers default) =
  match code {
    SNil: (default SNil)
    SCons: (Parse.header.go code.head (SCons code.head code.tail) headers default)
  }

(Parse.header.go char code headers default) =
  match headers {
    LNil: (default code)
    LCons: 
      let (sym, fun) = headers.head
      match is_correct = (== char sym) {
        +: (fun code)
        0: (Parse.header.go char code headers.tail default)
      }
  }

(Parse.term code) =
  let headers =
    (LCons ('∀',Parse.term.all)
    (LCons ('λ',Parse.term.lam)
    (LCons ('(',Parse.term.app)
    (LCons ('{',Parse.term.ann)
    (LCons ('*',Parse.term.set)
    LNil)))))
  let default = Parse.term.var
  (Parse.header (Parse.skip code) headers default)

(Parse.term.all code) =
  let (code, x)   = (Parse.text code "∀")
  let (code, x)   = (Parse.text code "(")
  let (code, nam) = (Parse.name code)
  let (code, x)   = (Parse.text code ":")
  let (code, inp) = (Parse.term code)
  let (code, x)   = (Parse.text code ")")
  let (code, bod) = (Parse.term code)
  (code, λctx (All (inp ctx) λx(bod (LCons (nam,x) ctx))))

(Parse.term.lam code) =
  let (code, x)   = (Parse.text code "λ")
  let (code, nam) = (Parse.name code)
  let (code, bod) = (Parse.term code)
  (code, λctx (Lam λx(bod (LCons (nam,x) ctx))))

(Parse.term.app code) =
  let (code, x)   = (Parse.text code "(")
  let (code, fun) = (Parse.term code)
  let (code, arg) = (Parse.term code)
  let (code, x)   = (Parse.text code ")")
  (code, λctx (App (fun ctx) (arg ctx)))

(Parse.term.ann code) =
  let (code, x)   = (Parse.text code "{")
  let (code, val) = (Parse.term code)
  let (code, x)   = (Parse.text code ":")
  let (code, typ) = (Parse.term code)
  let (code, x)   = (Parse.text code "}")
  (code, λctx (Ann (val ctx) (typ ctx)))

(Parse.term.set code) =
  let (code, x) = (Parse.text code "*")
  (code, λctx Set)

(Parse.term.var code) =
  let (code, nam) = (Parse.name code)
  (code, λctx match found = (Find nam ctx) {
    None: 0 // TODO: turn into Ref
    Some: found.value
  })

(Parse.term.do code) =
  let (code, parsed) = (Parse.term code)
  (parsed LNil)

// Search
// ------

//(Fix f) = (f (Fix f))

//(Superpose LNil)           = 0
//(Superpose (LCons x LNil)) = x
//(Superpose (LCons x xs))   = {x (Superpose xs)}

//(Compact LNil)                = LNil
//(Compact (LCons None     xs)) = (Compact xs)
//(Compact (LCons (Some x) xs)) = (LCons x (Compact xs))

//(Enum (Slf bod)     ctx dep) = (Ins (Enum (bod Set) ctx dep))
//(Enum (All inp out) ctx dep) = (Lam λx(Enum (out (Var dep)) (LCons (x,inp) ctx) (+ dep 1)))
//(Enum (Ann val typ) ctx dep) = (Enum val ctx dep)
//(Enum (Ref nam val) ctx dep) = (Enum val ctx dep)
//(Enum goal          ctx dep) = (Superpose (Compact (Pick goal ctx λx(x) dep)))

//(Pick goal LNil             lft dep) = LNil
////(Pick goal (LCons (x,t) xs) lft dep) = (LCons (Call goal x t (lft xs) dep) (Pick goal xs λk(lft (LCons (x,t) k)) dep))
//(Pick goal (LCons (x,t) xs) lft dep) = (LCons goal (Pick goal xs λk(lft (LCons (x,t) k)) dep))

////(Call goal fn (All inp out) ctx dep) = let arg = (Enum inp ctx); (Call goal (App fn arg) (out arg) ctx dep)
////(Call goal fn typ           ctx dep) = match (Equal typ goal dep) { True: (Some fn); False: None }

// API
// ---

(Checker def) = match def {
  Ref: (Checker def.val)
  Ann:
    let (logs, result) = ((Check def.val def.typ 0) [])
    match result {
      None: [logs, 0]
      Some: [logs, 1]
    }
  val: "untyped"
}

// Tests
// -----

//c4  = (Lam λf(Lam λx(App f (App f (App f (App f x))))))
//add = (Lam λn(Lam λm(Lam λs(Lam λz(App (App n s) (App (App m s) z))))))
//mul = (Lam λn(Lam λm(Lam λs(App n (App m s)))))

//bool =
  //let type = Set
  //let term = (Slf λself(All (All bool λx(Set)) λP(All (App P true) λt(All (App P false) λf(App P self)))))
  //(Ref "bool" (Ann term type))

//true =
  //let type = bool
  //let term = (Ins (Lam λP(Lam λt(Lam λf(t)))))
  //(Ref "true" (Ann term type))

//false =
  //let type = bool
  //let term = (Ins (Lam λP(Lam λt(Lam λf(f)))))
  //(Ref "false" (Ann term type))

//not =
  //let type = (All bool λx(bool))
  //let term = (Lam λb(Lam λP(Lam λt(Lam λf(App (App (App b P) f) t)))))
  //(Ref "not" (Ann term type))
  
//nat =
  //let type = Set
  //let term = (All Set λP(All (All P λx(P)) λt(All P λf(P))))
  //(Ref "nat" (Ann term type))

//zero =
  //let type = nat
  //let term = (Lam λP(Lam λs(Lam λz(z))))
  //(Ref "zero" (Ann term type))

//succ =
  //let type = (All nat λx(nat))
  //let term = (Lam λn(Lam λP(Lam λs(Lam λz(App s (App (App (App n P) s) z))))))
  //(Ref "succ" (Ann term type))

//// Eq
//// : ∀(A: *) ∀(a: A) ∀(b: A) *
//// = λP λa λb
////   ∀(P: ∀(x: A) *) ∀(x: (P a)) (P b)
//eq =
  //let type = (All Set λA (All A λa (All A λb Set)))
  //let term = (Lam λA (Lam λa (Lam λb (All (All A λx(Set)) λP (All (App P a) λx (App P b))))))
  //(Ann term type)

//// Refl
//// : ∀(A: *) ∀(x: A) (eq A x x)
//// = λA λx λP λrefl refl
//refl =
  //let type = (All Set λA (All A λx (App (App (App eq A) x) x)))
  //let term = (Lam λA (Lam λx (Lam λP (Lam λrefl refl))))
  //(Ann term type)

//// Exists
//// : ∀(A: *) ∀(B: A -> *) *
//// = λA λB
////   ∀(P: *) ∀(it: ∀(x: A) ∀(y: B x) P) P
//ex =
  //let type = (All Set λA (All (All A λx(Set)) λB Set))
  //let term = (Lam λA (Lam λB (All Set λP (All (All A λx(All (App B x) λy(P))) λit P))))
  //(Ann term type)

//// It
//// : ∀(A: *) ∀(B: A -> *) ∀(x: A) ∀(y: (B x)) (Ex A B)
//// = λA λB λx λy λP λit (it x y)
//it =
  //let type = (All Set λA (All (All A λx(Set)) λB (All A λx (All (App B x) λy (App (App ex A) B)))))
  //let term = (Lam λA (Lam λB (Lam λx (Lam λy (Lam λP (Lam λit (App (App it x) y)))))))
  //(Ann term type)

//// FOO
//// : ∀(A: *) ∀(B: *) ∀(aa: ∀(x: A) A) ∀(ab: ∀(x: B) A) ∀(ba: ∀(x: B) A) ∀(bb: ∀(x: B) B) ∀(a: A) ∀(b: B) A
//// = λA λB λaa λab λba λbb λa λb (aa (aa (aa b)))
//foo = 
  //let type = (All Set λA (All Set λB (All (All A λx(A)) λaa (All (All A λx(B)) λab (All (All B λx(A)) λba (All (All B λx(B)) λbb (All A λa (All B λb A))))))))
  //let term = (Lam λA (Lam λB (Lam λaa (Lam λab (Lam λba (Lam λbb (Lam λa (Lam λb (App aa (App aa (App aa a)))))))))))
  //(Ann term type)

//// N2
//// : Nat
//// = (succ (succ zero))
//n2 =
  //let type = nat
  //let term = (App succ (App succ zero))
  //(Ann term type)

//main = (Checker true)


//T = (Lam λt (Lam λf (t)))
//F = (Lam λt (Lam λf (f)))

//main = (Equal F F 0)