// Types
// -----

//data Maybe
  //= (Some value)
  //| None

//data Bool
  //= False
  //| True

//data Pair
  //= (Pair fst snd)

//data Term
  //= (All nam inp bod)
  //| (Lam nam bod)
  //| (App fun arg)
  //| (Ann val typ)
  //| (Slf nam bod)
  //| (Ins val)
  //| (Ref nam val)
  //| (Let nam val bod)
  //| (Set)
  //| (U60)
  //| (Num val)
  //| (Op2 opr fst snd)
  //| (Mat nam x z s p)
  //| (Txt txt)
  //| (Hol nam ctx val)
  //| (Var nam idx) 

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

(Debug dep []  value) = value
(Debug dep msg value) = (HVM.print (Join msg) value)
//(Debug dep []  value) = value
//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (Join msg) value))

(NewLine) = (String.cons 10 String.nil)
(Quote)   = (String.cons 34 String.nil)

(And True  b) = b
(And False b) = False

(Or True  b) = True
(Or False b) = b

(If 0 t f) = f
(If 1 t f) = t

(When None       some none) = none
(When (Some val) some none) = (some val)

(U60.show n)                = (U60.show.go n String.nil)
(U60.show.go n res)         = (U60.show.go.match (< n 10) n res)
(U60.show.go.match 0 n res) = (U60.show.go (/ n 10) (String.cons (+ '0' (% n 10)) res))
(U60.show.go.match i n res) = (String.cons (+ '0' n) res)

(U60.name n)    = (U60.name.go (+ n 1))
(U60.name.go 0) = ""
(U60.name.go n) = (String.cons (+ 97 (% (- n 1) 26)) (U60.name.go (/ (- n 1) 26)))

(Same String.nil         String.nil)         = 1
(Same String.nil         (String.cons y ys)) = 0
(Same (String.cons x xs) String.nil)         = 0
(Same (String.cons x xs) (String.cons y ys)) = (& (== x y) (Same xs ys))

(Find name List.nil)                        = None
(Find name (List.cons (Pair nam val) tail)) = (If (Same nam name) (Some val) (Find name tail))

(Concat String.nil         ys) = ys
(Concat (String.cons x xs) ys) = (String.cons x (Concat xs ys))

(Join List.nil)         = ""
(Join (List.cons x xs)) = (Concat x (Join xs))

(Fst (Pair fst snd)) = fst
(Snd (Pair fst snd)) = snd

(Get (Pair fst snd) fun) = (fun fst snd)

(Pure x) = (Some x)

(Bind a b) = (Bind.match a b)

(Bind.match None     b) = None
(Bind.match (Some a) b) = (b a)

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

(Reduce r (App fun arg))     = (Reduce.app r (Reduce r fun) arg)
(Reduce r (Ann val typ))     = (Reduce r val)
(Reduce r (Ins val))         = (Reduce r val)
(Reduce 1 (Ref nam val))     = (Reduce 1 val)
(Reduce r (Let nam val bod)) = (Reduce r (bod val))
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 r opr fst snd)
(Reduce r (Mat nam x z s p)) = (Reduce.mat r nam x z s p)
(Reduce 1 (Txt txt))         = (Reduce.txt 1 txt)
(Reduce r val)               = val

(Reduce.app r (Lam nam bod)     arg) = (Reduce r (bod (Reduce r arg)))
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
(Reduce.app r fun               arg) = (App fun arg)

(Reduce.op2 r ADD (Num fst) (Num snd)) = (Num (+ fst snd))
(Reduce.op2 r SUB (Num fst) (Num snd)) = (Num (- fst snd))
(Reduce.op2 r MUL (Num fst) (Num snd)) = (Num (* fst snd))
(Reduce.op2 r DIV (Num fst) (Num snd)) = (Num (/ fst snd))
(Reduce.op2 r MOD (Num fst) (Num snd)) = (Num (% fst snd))
(Reduce.op2 r EQ  (Num fst) (Num snd)) = (Num (== fst snd))
(Reduce.op2 r NE  (Num fst) (Num snd)) = (Num (!= fst snd))
(Reduce.op2 r LT  (Num fst) (Num snd)) = (Num (< fst snd))
(Reduce.op2 r GT  (Num fst) (Num snd)) = (Num (> fst snd))
(Reduce.op2 r LTE (Num fst) (Num snd)) = (Num (<= fst snd))
(Reduce.op2 r GTE (Num fst) (Num snd)) = (Num (>= fst snd))
(Reduce.op2 r AND (Num fst) (Num snd)) = (Num (& fst snd))
(Reduce.op2 r OR  (Num fst) (Num snd)) = (Num (| fst snd))
(Reduce.op2 r XOR (Num fst) (Num snd)) = (Num (^ fst snd))
(Reduce.op2 r LSH (Num fst) (Num snd)) = (Num (<< fst snd))
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
(Reduce.op2 r opr fst snd)             = (Op2 opr fst snd)

(Reduce.mat r nam (Num 0) z s p) = (Reduce r z)
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
(Reduce.mat r nam val     z s p) = (Mat nam val z s p)

(Reduce.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
(Reduce.txt r String.nil)         = (Reduce 1 Book.String.nil)
(Reduce.txt r val)                = val

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

(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx(Normal r (bod (Var nam dep)) (+ dep 1)))
(Normal.term r (Lam nam bod)     dep) = (Lam nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
(Normal.term r (App fun arg)     dep) = (App (Normal r fun dep) (Normal r arg dep))
(Normal.term r (Ann val typ)     dep) = (Ann (Normal r val dep) (Normal r typ dep))
(Normal.term r (Slf nam bod)     dep) = (Slf nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
(Normal.term r (Ins val)         dep) = (Ins (Normal r val dep))
(Normal.term r (Ref nam val)     dep) = (Ref nam (Normal r val dep))
(Normal.term r (Let nam val bod) dep) = (Let nam (Normal r val bod) λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
(Normal.term r (Hol nam ctx)     dep) = (Hol nam ctx)
(Normal.term r Set               dep) = Set
(Normal.term r U60               dep) = U60
(Normal.term r (Num val)         dep) = (Num val)
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
(Normal.term r (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (Concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
(Normal.term r (Txt val)         dep) = (Txt val)
(Normal.term r (Var nam idx)     dep) = (Var nam idx)

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

// Check if two terms are identical. If not...
(Equal a b dep) = (Equal.unify.a a λx(x) b dep)
//(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)

// ...
(Equal.unify.a (App a.fun a.arg) as b dep) = (Equal.unify.a a.fun λk(as (App k a.arg)) b dep)
(Equal.unify.a (Hol a.nam a.ctx) as b dep) = (Debug dep ["Found: ?" a.nam " = " (Show b dep)] 1)
(Equal.unify.a a                 as b dep) = (Equal.unify.b (as a) b λx(x) dep)

// ...
(Equal.unify.b a (App b.fun b.arg) bs dep) = (Equal.unify.b a b.fun λk(bs (App k b.arg)) dep)
(Equal.unify.b a (Hol b.nam b.ctx) bs dep) = (Debug dep ["Found: ?" b.nam " = " (Show a dep)] 1)
(Equal.unify.b a b                 bs dep) = let b = (bs b); (Equal.minor (Identical a b dep) a b dep)

// Check if they're identical after a minor weak reduction. If not...
(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
(Equal.minor 1 a b dep) = 1

// Check if they're identical after a major weak reduction. If not...
(Equal.major 0 a b dep) = (Equal.enter (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
(Equal.major 1 a b dep) = 1

// Check if they become identical after reducing fields.
(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) a b dep)
(Equal.enter 1 a b dep) = 1

// Checks if two terms are identical, without reductions.
(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)

// Generic comparer.
(Comparer rec (All a.nam a.inp a.bod)     (All b.nam b.inp b.bod)     dep) = (& (rec a.inp b.inp dep) (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
(Comparer rec (Lam a.nam a.bod)           (Lam b.nam b.bod)           dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
(Comparer rec (App a.fun a.arg)           (App b.fun b.arg)           dep) = (& (rec a.fun b.fun dep) (rec a.arg b.arg dep))
(Comparer rec (Slf a.nam a.bod)           (Slf b.nam b.bod)           dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
(Comparer rec (Ins a.val)                 b                           dep) = (rec a.val b dep)
(Comparer rec a                           (Ins b.val)                 dep) = (rec a b.val dep)
(Comparer rec (Ref a.nam a.val)           (Ref b.nam b.val)           dep) = (Same a.nam b.nam)
(Comparer rec (Let a.nam a.val a.bod)     b                           dep) = (rec (a.bod a.val) b dep)
(Comparer rec a                           (Let b.nam b.val b.bod)     dep) = (rec a (b.bod b.val) dep)
(Comparer rec Set                         Set                         dep) = 1
(Comparer rec (Var a.nam a.idx)           (Var b.nam b.idx)           dep) = (== a.idx b.idx)
(Comparer rec (Ann a.val a.typ)           b                           dep) = (rec a.val b dep)
(Comparer rec a                           (Ann b.val b.typ)           dep) = (rec a b.val dep)
(Comparer rec (Hol a.nam a.ctx)           (Hol b.nam b.ctx)           dep) = (Same a.nam b.nam)
(Comparer rec U60                         U60                         dep) = 1
(Comparer rec (Num a.val)                 (Num b.val)                 dep) = (== a.val b.val)
(Comparer rec (Op2 a.opr a.fst a.snd)     (Op2 b.opr b.fst b.snd)     dep) = (& (rec a.fst a.snd dep) (rec b.fst b.snd dep))
(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (Concat a.nam "-1") dep)) (b.s (Var (Concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
(Comparer rec (Txt a.txt)                 (Txt b.txt)                 dep) = (Same a.txt b.txt)
(Comparer rec a                           b                           dep) = 0

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

(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
(IfAll other             yep nop) = nop

(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
(IfSlf other         yep nop) = nop

//(Infer term dep) = (Debug dep ["Infer: " (Show term dep)] (Infer.match term dep))
(Infer term dep) = (Infer.match term dep)

(Infer.match (All nam inp bod) dep) =
  (Bind (Check inp Set dep) λinp_typ
  (Bind (Check (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
  (Pure Set)))
(Infer.match (Lam nam bod) dep) =
  (Debug dep ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
(Infer.match (App fun arg) dep) =
  (Bind (Infer fun dep) λfun_typ
  ((IfAll (Reduce 1 fun_typ)
    λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
      (Bind (Check arg fun_typ.inp dep) λval_typ
      (Pure (fun_typ.bod arg)))
    λfun λarg
      (Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
    fun arg))
(Infer.match (Ann val typ) dep) =
  (Pure typ)
(Infer.match (Slf nam bod) dep) =
  (Bind (Check (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
  (Pure Set))
(Infer.match (Ins val) dep) =
  (Bind (Infer val dep) λval_typ
  ((IfSlf (Reduce 1 val_typ)
    λval_nam λval_typ.bod λval (Pure (val_typ.bod (Ins val)))
    λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
    val))
(Infer.match (Ref nam val) dep) = 
  (Infer val dep)
(Infer.match (Let nam val bod) dep) =
  (Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
(Infer.match Set dep) =
  (Pure Set)
(Infer.match U60 dep) =
  (Pure Set)
(Infer.match (Num num) dep) =
  (Pure U60)
(Infer.match (Txt txt) dep) =
  (Pure Book.String)
(Infer.match (Op2 opr fst snd) dep) =
  (Bind (Check fst U60 dep) λfst
  (Bind (Check snd U60 dep) λsnd
  (Pure U60)))
// x : U60
// p : ∀(x: U60) *
// z : (p 0)
// s : ∀(x-1 : U60) (p (+ 1 x-1))
// ------------------------------
// (Mat nam x z s p) : (p x)
(Infer.match (Mat nam x z s p) dep) =
  (Bind (Check x U60 dep) λx_typ
  (Bind (Check (p (Ann (Var nam dep) U60)) Set dep) λp_typ
  (Bind (Check z (p (Num 0)) dep) λz_typ
  (Bind (Check (s (Ann (Var (Concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (Concat nam "-1") dep))) (+ dep 1)) λs_typ
  (Pure (p x))))))
(Infer.match (Hol nam ctx) dep) =
  (Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
(Infer.match (Var nam idx) dep) =
  (Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)

//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match term type dep))
(Check term type dep) = (Check.match term type dep)

(Check.match (Lam term.nam term.bod) type dep) =
  ((IfAll (Reduce 1 type)
    λtype.nam λtype.inp λtype.bod λterm.bod
      let ann  = (Ann (Var term.nam dep) type.inp)
      let term = (term.bod ann)
      let type = (type.bod ann)
      (Check term type (+ dep 1))
    λterm.bod
      (Infer (Lam term.nam term.bod) dep))
    term.bod)
(Check.match (Ins term.val) type dep) =
  ((IfSlf (Reduce 1 type)
    λtype.nam λtype.bod λterm.val (Check term.val (type.bod (Ins term.val)) dep)
    λterm.val (Infer (Ins term.val) dep))
    term.val)
(Check.match (Let term.nam term.val term.bod) type dep) =
  (Check (term.bod term.val) type (+ 1 dep))
(Check.match (Hol term.nam term.ctx) type dep) =
  (Debug dep ["HOLE!: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (Context.show term.ctx dep)]
  (Pure 0))
(Check.match (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
  (Check.report (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
//(Check.match (Ref term.nam term.val) type dep) =
  //(Check term.val type dep)
(Check.match term type dep) =
  (Check.verify term type dep)

(Check.verify term type dep) =
  (Bind (Infer term dep) λinfer
  (Check.report (Equal type infer dep) infer type term dep))

(Check.report 0 inferred expected value dep) =
  let inf = (Show (Normal 0 inferred dep) dep)
  let exp = (Show (Normal 0 expected dep) dep)
  let val = (Show (Normal 0 value dep) dep)
  (Debug dep ["Error: " inf NewLine "    != " exp NewLine "    in " val] None)
(Check.report n inferred expected value dep) =
  (Pure 0)

// Syntax
// ------

(Show (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (Lam nam bod)     dep) = (Join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (App fun arg)     dep) = (Join ["(" (Show.prune (Show fun dep)) " " (Show arg dep) ")"])
(Show (Ann val typ)     dep) = (Join ["{" (Show val dep) ": " (Show typ dep) "}"])
(Show (Slf nam bod)     dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
(Show (Ins val)         dep) = (Join ["~" (Show val dep)])
(Show (Ref nam val)     dep) = nam
(Show (Let nam val bod) dep) = (Join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
(Show Set               dep) = (Join ["*"])
(Show U60               dep) = "#U60"
(Show (Num val)         dep) = (Join ["#" (U60.show val)])
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
(Show (Mat nam x z s p) dep) = (Join ["match " nam " = " (Show x dep) " { #0 => " (Show z dep) "; #+ => " (Show (s (Var (Concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
(Show (Txt txt)         dep) = (Join [Quote txt Quote])
(Show (Hol nam ctx)     dep) = (Join ["?" nam])
(Show (Var nam idx)     dep) = (Join [nam])
//(Show (Var nam idx)     dep) = (Join [nam "'" (U60.show idx)])

(Show.many List.nil         dep) = ""
(Show.many (List.cons x xs) dep) = (Join [" " (Show x dep) (Show.many xs dep)])

(Show.trim (String.cons ' ' xs)) = xs
(Show.trim str)                  = str

(Show.prune (String.cons '(' xs)) = (Show.begin xs)
(Show.prune str)                  = str

(Show.begin (String.cons x (String.cons y String.nil))) = (String.cons x String.nil)
(Show.begin (String.cons x xs))                         = (String.cons x (Show.begin xs))
(Show.begin String.nil)                                 = String.nil

(Op2.show ADD) = "+"
(Op2.show SUB) = "-"
(Op2.show MUL) = "*"
(Op2.show DIV) = "/"

(Context.show List.nil         dep) = ""
(Context.show (List.cons x xs) dep) = (Join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])

(Context.show.ann (Ann val typ) dep) = (Join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
(Context.show.ann term          dep) = (Show (Normal 0 term dep) dep)

// Compilation
// -----------

(Compile (All nam inp bod)) = 0
(Compile (Lam nam bod))     = λx(Compile (bod (Var "" x)))
(Compile (App fun arg))     = ((Compile fun) (Compile arg))
(Compile (Ann val typ))     = (Compile val)
(Compile (Slf nam bod))     = 0
(Compile (Ins val))         = (Compile val)
(Compile (Ref nam val))     = (Compile val)
(Compile (Let nam val bod)) = (Compile (bod val))
(Compile Set)               = 0
(Compile U60)               = 0
(Compile (Num val))         = val
(Compile (Op2 opr fst snd)) = (Compile.op2 opr (Compile fst) (Compile snd))
(Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x))))
(Compile (Txt txt))         = (Compile (Compile.txt txt))
(Compile (Hol nam ctx))     = 0
(Compile (Var nam val))     = val

(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
(Compile.txt String.nil)         = Book.String.nil

(Compile.op2 ADD fst snd) = (+ fst snd)
(Compile.op2 SUB fst snd) = (- fst snd)
(Compile.op2 MUL fst snd) = (* fst snd)
(Compile.op2 DIV fst snd) = (/ fst snd)
(Compile.op2 MOD fst snd) = (% fst snd)
(Compile.op2 EQ  fst snd) = (== fst snd)
(Compile.op2 NE  fst snd) = (!= fst snd)
(Compile.op2 LT  fst snd) = (< fst snd)
(Compile.op2 GT  fst snd) = (> fst snd)
(Compile.op2 LTE fst snd) = (<= fst snd)
(Compile.op2 GTE fst snd) = (>= fst snd)
(Compile.op2 AND fst snd) = (& fst snd)
(Compile.op2 OR  fst snd) = (| fst snd)
(Compile.op2 XOR fst snd) = (^ fst snd)
(Compile.op2 LSH fst snd) = (<< fst snd)
(Compile.op2 RSH fst snd) = (>> fst snd)

(Compile.mat 0 z s) = z
(Compile.mat n z s) = (s (- n 1))

// API
// ---

(Read str) = (str 0 λheadλtail(String.cons head (Read tail)) String.nil)

(Normalizer (Ref nam val)) = (Normalizer val)
(Normalizer (Ann val typ)) = (Normalizer val)
(Normalizer val)           = (Read (Compile val)) // compiles to native and reads as string
//(Normalizer val)           = ((Compile val)) // compiles to native and show it
//(Normalizer val)           = (Normal 1 val  1) // uses the normalizer function

(Checker (Ref nam val)) = (Checker val)
(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
(Checker val)           = (Checker.report (Infer val 0))

(Checker.report (Some x)) = (HVM.print "Check!" OK)
(Checker.report None)     = (HVM.print "Error." ERR)