diff --git a/Cargo.lock b/Cargo.lock
index 0d47ffbd..dd64cf7a 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,9 +4,9 @@ version = 3
 
 [[package]]
 name = "TSPL"
-version = "0.0.1"
+version = "0.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7f7bc3c167472f0599b71590ead5067418477b7d512ec251b25b4aa78fa808f"
+checksum = "5b8ec3e7412fb948ebd3410595e15e7f80c12bf7958ffb83a7f6ff34942505f9"
 dependencies = [
  "highlight_error",
 ]
@@ -45,6 +45,7 @@ name = "kind2"
 version = "0.1.0"
 dependencies = [
  "TSPL",
+ "highlight_error",
  "im",
 ]
 
diff --git a/Cargo.toml b/Cargo.toml
index 1300c9e6..eb95a811 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,8 +3,11 @@ name = "kind2"
 version = "0.1.0"
 edition = "2021"
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+[[bin]]
+name = "kind2"
+path = "src/main.rs"
 
 [dependencies]
-TSPL = "0.0.1"
+TSPL = "0.0.4"
+highlight_error = "0.1.1"
 im = "15.1.0"
diff --git a/book/.check.hvm1 b/book/.check.hvm1
new file mode 100644
index 00000000..2308369e
--- /dev/null
+++ b/book/.check.hvm1
@@ -0,0 +1,486 @@
+// 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) 
+  //| (Src src val)
+
+// Prelude
+// -------
+
+(Debug dep []  value) = value
+(Debug dep msg value) = (HVM.print (String.join msg) value)
+//(Debug dep []  value) = value
+//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (String.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))
+
+(String.concat String.nil         ys) = ys
+(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
+
+(String.join List.nil)         = ""
+(String.join (List.cons x xs)) = (String.concat x (String.join xs))
+
+(Pair.fst (Pair fst snd)) = fst
+(Pair.snd (Pair fst snd)) = snd
+
+(Pair.get (Pair fst snd) fun) = (fun fst snd)
+
+(Maybe.pure x) = (Some x)
+
+(Maybe.bind a b) = (Maybe.bind.match a b)
+
+(Maybe.bind.match None     b) = None
+(Maybe.bind.match (Some a) b) = (b a)
+
+(String.color RESET)      = (String.cons 27 "[0m")
+(String.color BRIGHT)     = (String.cons 27 "[1m")
+(String.color DIM)        = (String.cons 27 "[2m")
+(String.color UNDERSCORE) = (String.cons 27 "[4m")
+(String.color BLINK)      = (String.cons 27 "[5m")
+(String.color REVERSE)    = (String.cons 27 "[7m")
+(String.color HIDDEN)     = (String.cons 27 "[8m")
+(String.color BLACK)      = (String.cons 27 "[30m")
+(String.color RED)        = (String.cons 27 "[31m")
+(String.color GREEN)      = (String.cons 27 "[32m")
+(String.color YELLOW)     = (String.cons 27 "[33m")
+(String.color BLUE)       = (String.cons 27 "[34m")
+(String.color MAGENTA)    = (String.cons 27 "[35m")
+(String.color CYAN)       = (String.cons 27 "[36m")
+(String.color WHITE)      = (String.cons 27 "[37m")
+(String.color GRAY)       = (String.cons 27 "[90m")
+(String.color BG_BLACK)   = (String.cons 27 "[40m")
+(String.color BG_RED)     = (String.cons 27 "[41m")
+(String.color BG_GREEN)   = (String.cons 27 "[42m")
+(String.color BG_YELLOW)  = (String.cons 27 "[43m")
+(String.color BG_BLUE)    = (String.cons 27 "[44m")
+(String.color BG_MAGENTA) = (String.cons 27 "[45m")
+(String.color BG_CYAN)    = (String.cons 27 "[46m")
+(String.color BG_WHITE)   = (String.cons 27 "[47m")
+(String.color BG_GRAY)    = (String.cons 27 "[100m")
+(String.color x)          = "?"
+
+// 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 (Src src val))     = (Reduce r val)
+(Reduce r val)               = val
+
+(Reduce.app r (Lam nam bod)     arg) = (Reduce r (bod (Reduce 0 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 (Op2 ADD (Num 1) k) z s p) = (Reduce r (s k))
+(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 (String.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)
+(Normal.term r (Src src val)     dep) = (Src src (Normal r val dep))
+
+// Equality
+// --------
+
+// Check if two terms are identical. If not...
+(Equal a b dep) = (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) (Reduce 0 a) (Reduce 0 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)           b                           dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
+(Comparer rec a                           (Hol b.nam b.ctx)           dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
+(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 b.fst dep) (rec a.snd 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 (String.concat a.nam "-1") dep)) (b.s (Var (String.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 (Src a.src a.val)           b                           dep) = (Comparer rec a.val b dep)
+(Comparer rec a                           (Src b.src b.val)           dep) = (Comparer rec a b.val dep)
+(Comparer rec a                           b                           dep) = 0
+//(Comparer rec a                           b                           dep) = (HVM.log (NOP (Show a dep) (Show 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) =
+  (Maybe.bind (Check 0 inp Set dep) λinp_typ
+  (Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
+  (Maybe.pure Set)))
+(Infer.match (Lam nam bod) dep) =
+  (Debug dep ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
+(Infer.match (App fun arg) dep) =
+  (Maybe.bind (Infer fun dep) λfun_typ
+  ((IfAll (Reduce 1 fun_typ)
+    λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
+      (Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
+      (Maybe.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) =
+  (Maybe.pure typ)
+(Infer.match (Slf nam bod) dep) =
+  (Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
+  (Maybe.pure Set))
+(Infer.match (Ins val) dep) =
+  (Maybe.bind (Infer val dep) λval_typ
+  ((IfSlf (Reduce 1 val_typ)
+    λval_nam λval_typ.bod λval (Maybe.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) =
+  (Maybe.pure Set)
+(Infer.match U60 dep) =
+  (Maybe.pure Set)
+(Infer.match (Num num) dep) =
+  (Maybe.pure U60)
+(Infer.match (Txt txt) dep) =
+  (Maybe.pure Book.String)
+(Infer.match (Op2 opr fst snd) dep) =
+  (Maybe.bind (Check 0 fst U60 dep) λfst
+  (Maybe.bind (Check 0 snd U60 dep) λsnd
+  (Maybe.pure U60)))
+(Infer.match (Mat nam x z s p) dep) =
+  (Maybe.bind (Check 0 x U60 dep) λx_typ
+  (Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
+  (Maybe.bind (Check 0 z (p (Num 0)) dep) λz_typ
+  (Maybe.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
+  (Maybe.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)
+(Infer.match (Src src val) dep) =
+  (Infer.match val dep)
+
+//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 term type dep))
+(Check src term type dep) = (Check.match src term type dep)
+
+(Check.match src (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 0 term type (+ dep 1))
+    λterm.bod
+      (Infer (Lam term.nam term.bod) dep))
+    term.bod)
+(Check.match src (Ins term.val) type dep) =
+  ((IfSlf (Reduce 1 type)
+    λtype.nam λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) dep)
+    λterm.val (Infer (Ins term.val) dep))
+    term.val)
+(Check.match src (Let term.nam term.val term.bod) type dep) =
+  (Check 0 (term.bod term.val) type (+ 1 dep))
+(Check.match src (Hol term.nam term.ctx) type dep) =
+  (Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
+  (Maybe.pure 0))
+(Check.match src (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
+  (Check.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
+(Check.match src (Src term.src term.val) type dep) =
+  (Check term.src term.val type dep)
+//(Check.match src (Ref term.nam term.val) type dep) =
+  //(Check term.val type dep)
+(Check.match src term type dep) =
+  (Check.verify src term type dep)
+
+(Check.verify src term type dep) =
+  (Maybe.bind (Infer term dep) λinfer
+  (Check.report src (Equal type infer dep) infer type term dep))
+
+(Check.report src 0 detected expected value dep) =
+  let det = (Show (Normal 0 detected dep) dep)
+  let exp = (Show (Normal 0 expected dep) dep)
+  let val = (Show (Normal 0 value dep) dep)
+  (Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
+    "- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
+    "- detected: " (String.color RESET) (String.color RED)   det NewLine (String.color RESET) (String.color BRIGHT)
+    "- bad_term: " (String.color RESET) (String.color DIM)   val NewLine (String.color RESET)
+    "##LOC{" (U60.show src) "}LOC##" NewLine
+  ] None)
+(Check.report src n inferred expected value dep) =
+  (Maybe.pure 0)
+
+// Syntax
+// ------
+
+(Show (All nam inp bod) dep) = (String.join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (Lam nam bod)     dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (App fun arg)     dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
+(Show (Ann val typ)     dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
+(Show (Slf nam bod)     dep) = (String.join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (Ins val)         dep) = (String.join ["~" (Show val dep)])
+(Show (Ref nam val)     dep) = nam
+(Show (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show Set               dep) = (String.join ["*"])
+(Show U60               dep) = "#U60"
+(Show (Num val)         dep) = (String.join ["#" (U60.show val)])
+(Show (Op2 opr fst snd) dep) = (String.join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
+(Show (Mat nam x z s p) dep) = (String.join ["#match " nam " = " (Show x dep) " { #0: " (Show z dep) " #+: " (Show (s (Var (String.concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
+(Show (Txt txt)         dep) = (String.join [Quote txt Quote])
+(Show (Hol nam ctx)     dep) = (String.join ["?" nam])
+(Show (Var nam idx)     dep) = (String.join [nam])
+(Show (Src src val)     dep) = (Show val dep)
+//(Show (Var nam idx)     dep) = (String.join [nam "'" (U60.show idx)])
+
+(Show.many List.nil         dep) = ""
+(Show.many (List.cons x xs) dep) = (String.join [" " (Show x dep) (Show.many xs dep)])
+
+(Show.trim (String.cons ' ' xs)) = xs
+(Show.trim str)                  = str
+
+(Show.unwrap (String.cons '(' xs)) = (Show.begin xs)
+(Show.unwrap 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) = (String.join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])
+
+(Context.show.ann (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
+(Context.show.ann term          dep) = (Show (Normal 0 term dep) dep)
+//(Context.show.ann val           dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
+
+// Compilation
+// -----------
+
+(Str.view str) = (str 0 λheadλtail(String.cons head (Str.view tail)) String.nil)
+
+(Str.make (String.cons x xs)) = λP λcons λnil (cons x (Str.make xs))
+(Str.make String.nil)         = λP λcons λnil nil
+
+Compile.primitives = [
+  (Pair "HVM.log" λA λB λmsg λret (HVM.log msg ret))
+  (Pair "HVM.print" λA λmsg λret (HVM.print (Str.view msg) ret))
+  (Pair "HVM.save" λA λname λdata λret (HVM.save (Str.view name) (Str.view data) ret))
+  (Pair "HVM.load" λA λname λret (HVM.load (Str.view name) λdata (ret (Str.make data))))
+]
+
+(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.ref Compile.primitives nam 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))         = (Str.make txt)
+(Compile (Hol nam ctx))     = 0
+(Compile (Var nam val))     = val
+(Compile (Src src val))     = (Compile 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))
+
+(Compile.ref (List.cons (Pair prim_name prim_func) prims) nam val) = (If (Same prim_name nam) prim_func (Compile.ref prims nam val))
+(Compile.ref List.nil nam val) = (Compile val)
+
+// API
+// ---
+
+(Normalizer (Ref nam val)) = (Normalizer val)
+(Normalizer (Ann val typ)) = (Normalizer val)
+(Normalizer (Src src val)) = (Normalizer val)
+(Normalizer val)           = (Compile val)
+//(Normalizer val)           = (Str.view (Compile val))
+
+(Checker name (Ref nam val))           = (Checker name val)
+(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
+(Checker name (Src src val))           = (Checker name val)
+(Checker name (Ann val typ))           = (Checker.report name (Check 0 val typ 0))
+(Checker name val)                     = (Checker.report name (Infer val 0))
+
+(Checker.report name (Some x)) = 1
+(Checker.report name None)     = 0
+//(Checker.report name (Some x)) = (HVM.print (String.join [(String.color GREEN) "- " name ": ✔" (String.color RESET)]) 1)
+//(Checker.report name None)     = (HVM.print (String.join [(String.color RED) "- " name ": ✘" (String.color RESET)]) 0)
+
+(Checker.many.go (List.cons (Pair name def) defs)) = (& (Checker name def) (Checker.many.go defs))
+(Checker.many.go List.nil)                         = 1
+
+(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
+
+Book.List.cons = (Ref "List.cons" (Ann (Src 5497633636480 (Lam "T" λ_T (Src 5497637830784 (Lam "head" λ_head (Src 5497645170816 (Lam "tail" λ_tail (Src 5497654608000 (Ins (Src 5497655656576 (Lam "P" λ_P (Src 5497659850880 (Lam "cons" λ_cons (Src 5497667190912 (Lam "nil" λ_nil (Src 5497675579520 (App (App (Src 5497676628085 _cons) (Src 5497681870970 _head)) (Src 5497687113855 _tail))))))))))))))))) (Src 5497570721861 (All "T" (Src 5497578061844 (Set)) λ_T (Src 5497583304773 (All "head" (Src 5497593790499 _T) λ_head (Src 5497599033413 (All "tail" (Src 5497609519161 (App (Src 5497610567734 (Book.List)) (Src 5497615810616 _T))) λ_tail (Src 5497622102085 (App (Src 5497623150658 (Book.List)) (Src 5497628393540 _T)))))))))))
+Book.List.nil = (Ref "List.nil" (Ann (Src 6597105418303 (Lam "T" λ_T (Src 6597111709759 (Ins (Src 6597112758335 (Lam "P" λ_P (Src 6597116952639 (Lam "cons" λ_cons (Src 6597124292671 (Lam "nil" λ_nil (Src 6597132681279 _nil))))))))))) (Src 6597081301023 (All "T" (Src 6597088641043 (Set)) λ_T (Src 6597093883935 (App (Src 6597094932508 (Book.List)) (Src 6597100175390 _T)))))))
+Book.Main = (Ref "Main" (Ann (Src 1099526307866 (Op2 ADD (Src 1099530502165 (Num 12)) (Src 1099534696473 (Num 30)))) (Src 1099518967819 (U60))))
+Book.List = (Ref "List" (Ann (Src 4398070628530 (Lam "T" λ_T (Src 4398076919986 (Slf "self" λ_self (Src 4398085308594 (All "P" (Src 4398092648511 (All "xs" (Src 4398101037116 (App (Src 4398102085689 (Book.List)) (Src 4398107328571 _T))) λ_xs (Src 4398111522879 (Set)))) λ_P (Src 4398116765874 (All "cons" (Src 4398127251593 (All "head" (Src 4398137737304 _T) λ_head (Src 4398140883081 (All "tail" (Src 4398151368812 (App (Src 4398152417385 (Book.List)) (Src 4398157660267 _T))) λ_tail (Src 4398161854601 (App (Src 4398162903152 _P) (Src 4398165000328 (App (App (App (Src 4398166048891 (Book.List.cons)) (Src 4398176534653 _T)) (Src 4398178631810 _head)) (Src 4398183874695 _tail))))))))) λ_cons (Src 4398194360498 (All "nil" (Src 4398203797670 (App (Src 4398204846232 _P) (Src 4398206943397 (App (Src 4398207991970 (Book.List.nil)) (Src 4398217429156 _T))))) λ_nil (Src 4398224769202 (App (Src 4398225817772 _P) (Src 4398227914929 _self))))))))))))) (Src 4398053851156 (All "T" (Src 4398061191183 (Set)) λ_T (Src 4398066434068 (Set))))))
+Book.Char = (Ref "Char" (Ann (Src 3298546417679 (U60)) (Src 3298542223368 (Set))))
+Book.String = (Ref "String" (Ann (Src 2199036887064 (App (Src 2199037935634 (Book.List)) (Src 2199043178519 (Book.Char)))) (Src 2199032692746 (Set))))
+
+Main = (Normalizer Book.Main)
diff --git a/book/BBT.balance.kind2 b/book/BBT.balance.kind2
index f462453a..eea7f251 100644
--- a/book/BBT.balance.kind2
+++ b/book/BBT.balance.kind2
@@ -97,4 +97,4 @@ BBT.balance_rgt_heavier
   // Unreachable case
   // Right can't be a tip and greater than left at the same time
   let tip = (BBT.tip K V)
-  (~rgt P bin tip)
\ No newline at end of file
+  (~rgt P bin tip)
diff --git a/book/BBT.get.kind2 b/book/BBT.get.kind2
index 08256f3b..02a50715 100644
--- a/book/BBT.get.kind2
+++ b/book/BBT.get.kind2
@@ -14,4 +14,4 @@ BBT.get
     let gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
     ((~(cmp key next.key) P ltn eql gtn) cmp key)
   let tip = (Maybe.none V)
-  (~map P bin tip)
\ No newline at end of file
+  (~map P bin tip)
diff --git a/book/BBT.got.kind2 b/book/BBT.got.kind2
index bc12bcf9..bdc6a1ef 100644
--- a/book/BBT.got.kind2
+++ b/book/BBT.got.kind2
@@ -29,4 +29,4 @@ BBT.got
       (~new_pair P new)
     ((~(cmp key next.key) P ltn eql gtn) cmp key)
   let tip = (Pair.new (Maybe V) (BBT K V) (Maybe.none V) (BBT.tip K V))
-  (~map P bin tip)
\ No newline at end of file
+  (~map P bin tip)
diff --git a/book/BBT.singleton.kind2 b/book/BBT.singleton.kind2
index 60ae49bb..e615152d 100644
--- a/book/BBT.singleton.kind2
+++ b/book/BBT.singleton.kind2
@@ -5,4 +5,4 @@ BBT.singleton
   ∀(val: V)
   (BBT K V)
 = λK λV λkey λval
-  (BBT.bin K V #1 key val (BBT.tip K V) (BBT.tip K V))
\ No newline at end of file
+  (BBT.bin K V #1 key val (BBT.tip K V) (BBT.tip K V))
diff --git a/book/Cmp.eql.kind2 b/book/Cmp.eql.kind2
index b478903d..d418abc9 100644
--- a/book/Cmp.eql.kind2
+++ b/book/Cmp.eql.kind2
@@ -1,4 +1,4 @@
 Cmp.eql
 : Cmp
 = ~λP λltn λeql λgtn
-  eql
\ No newline at end of file
+  eql
diff --git a/book/IO.bind.kind2 b/book/IO.bind.kind2
new file mode 100644
index 00000000..befe2183
--- /dev/null
+++ b/book/IO.bind.kind2
@@ -0,0 +1,14 @@
+IO.bind
+: ∀(A: *)
+  ∀(B: *)
+  ∀(a: (IO A))
+  ∀(b: ∀(x: A) (IO B))
+  (IO B)
+= λA λB λa λb
+  let P     = λx ∀(b: ∀(x: A) (IO B)) (IO B)
+  let print = λtext λthen λb (IO.print B text λx(IO.bind A B (then x) b))
+  let load  = λfile λthen λb (IO.load B file λs(IO.bind A B (then s) b))
+  let save  = λfile λdata λthen λb (IO.save B file data λx(IO.bind A B (then Unit.one) b))
+  let done  = λterm λb (b term)
+  ((~a P print load save done) b)
+
diff --git a/book/IO.done.kind2 b/book/IO.done.kind2
new file mode 100644
index 00000000..808bcd01
--- /dev/null
+++ b/book/IO.done.kind2
@@ -0,0 +1,8 @@
+IO.done
+: ∀(A: *)
+  ∀(term: A)
+  (IO A)
+= λA λterm
+  ~λP λprint λload λsave λdone
+  (done term)
+
diff --git a/book/IO.kind2 b/book/IO.kind2
index f5a0a81e..1a4382e9 100644
--- a/book/IO.kind2
+++ b/book/IO.kind2
@@ -8,88 +8,3 @@ IO
   ∀(save: ∀(file: String) ∀(data: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file data then)))
   ∀(done: ∀(term: A) (P (IO.done A term)))
   (P self)
-
-IO.print
-: ∀(A: *)
-  ∀(text: String)
-  ∀(then: ∀(x: Unit) (IO A))
-  (IO A)
-= λA λtext λthen
-  ~λP λprint λload λsave λdone
-  (print text then)
-
-IO.load
-: ∀(A: *)
-  ∀(file: String)
-  ∀(then: ∀(x: String) (IO A))
-  (IO A)
-= λA λfile λthen
-  ~λP λprint λload λsave λdone
-  (load file then)
-
-IO.save
-: ∀(A: *)
-  ∀(file: String)
-  ∀(data: String)
-  ∀(then: ∀(x: Unit) (IO A))
-  (IO A)
-= λA λfile λdata λthen
-  ~λP λprint λload λsave λdone
-  (save file data then)
-
-IO.done
-: ∀(A: *)
-  ∀(term: A)
-  (IO A)
-= λA λterm
-  ~λP λprint λload λsave λdone
-  (done term)
-
-IO.run
-: ∀(A: *)
-  ∀(x: (IO A))
-  (IO A)
-= λA λx
-  let P     = λx(A)
-  let print = λtext λthen (HVM.print A text (IO.run A (then Unit.one)))
-  let load  = λfile λthen (HVM.load A file λs(IO.run A (then s)))
-  let save  = λfile λdata λthen (HVM.save A file data (IO.run A (then Unit.one)))
-  let done  = λterm (IO.done A term)
-  (~x P print load save done)
-
-IO.print.do
-: ∀(text: String)
-  (IO Unit)
-= λtext
-  (IO.print Unit text λx
-  (IO.done Unit x))
-
-IO.load.do
-: ∀(file: String)
-  (IO String)
-= λfile
-  (IO.load String file λx
-  (IO.done String x))
-
-IO.save.do
-: ∀(file: String)
-  ∀(data: String)
-  (IO Unit)
-= λfile λdata
-  (IO.save Unit file data λx
-  (IO.done Unit x))
-
-IO.bind
-: ∀(A: *)
-  ∀(B: *)
-  ∀(a: (IO A))
-  ∀(b: ∀(x: A) (IO B))
-  (IO B)
-= λA λB λa λb
-  let P     = λx ∀(b: ∀(x: A) (IO B)) (IO B)
-  let print = λtext λthen λb (IO.print B text λx(IO.bind A B (then x) b))
-  let load  = λfile λthen λb (IO.load B file λs(IO.bind A B (then s) b))
-  let save  = λfile λdata λthen λb (IO.save B file data λx(IO.bind A B (then Unit.one) b))
-  let done  = λterm λb (b term)
-  ((~a P print load save done) b)
-
diff --git a/book/IO.load.do.kind2 b/book/IO.load.do.kind2
new file mode 100644
index 00000000..cf8c03d9
--- /dev/null
+++ b/book/IO.load.do.kind2
@@ -0,0 +1,7 @@
+IO.load.do
+: ∀(file: String)
+  (IO String)
+= λfile
+  (IO.load String file λx
+  (IO.done String x))
+
diff --git a/book/IO.load.kind2 b/book/IO.load.kind2
new file mode 100644
index 00000000..6ce0b9d0
--- /dev/null
+++ b/book/IO.load.kind2
@@ -0,0 +1,9 @@
+IO.load
+: ∀(A: *)
+  ∀(file: String)
+  ∀(then: ∀(x: String) (IO A))
+  (IO A)
+= λA λfile λthen
+  ~λP λprint λload λsave λdone
+  (load file then)
+
diff --git a/book/IO.print.do.kind2 b/book/IO.print.do.kind2
new file mode 100644
index 00000000..a6dc1082
--- /dev/null
+++ b/book/IO.print.do.kind2
@@ -0,0 +1,7 @@
+IO.print.do
+: ∀(text: String)
+  (IO Unit)
+= λtext
+  (IO.print Unit text λx
+  (IO.done Unit x))
+
diff --git a/book/IO.print.kind2 b/book/IO.print.kind2
new file mode 100644
index 00000000..1831212b
--- /dev/null
+++ b/book/IO.print.kind2
@@ -0,0 +1,9 @@
+IO.print
+: ∀(A: *)
+  ∀(text: String)
+  ∀(then: ∀(x: Unit) (IO A))
+  (IO A)
+= λA λtext λthen
+  ~λP λprint λload λsave λdone
+  (print text then)
+
diff --git a/book/IO.run.kind2 b/book/IO.run.kind2
new file mode 100644
index 00000000..2615b00a
--- /dev/null
+++ b/book/IO.run.kind2
@@ -0,0 +1,12 @@
+IO.run
+: ∀(A: *)
+  ∀(x: (IO A))
+  (IO A)
+= λA λx
+  let P     = λx(IO A)
+  let print = λtext λthen (HVM.print (IO A) text (IO.run A (then Unit.one)))
+  let load  = λfile λthen (HVM.load (IO A) file λs(IO.run A (then s)))
+  let save  = λfile λdata λthen (HVM.save (IO A) file data (IO.run A (then Unit.one)))
+  let done  = λterm (IO.done A term)
+  (~x P print load save done)
+
diff --git a/book/IO.save.do.kind2 b/book/IO.save.do.kind2
new file mode 100644
index 00000000..230c7a18
--- /dev/null
+++ b/book/IO.save.do.kind2
@@ -0,0 +1,8 @@
+IO.save.do
+: ∀(file: String)
+  ∀(data: String)
+  (IO Unit)
+= λfile λdata
+  (IO.save Unit file data λx
+  (IO.done Unit x))
+
diff --git a/book/IO.save.kind2 b/book/IO.save.kind2
new file mode 100644
index 00000000..2cd4e40c
--- /dev/null
+++ b/book/IO.save.kind2
@@ -0,0 +1,10 @@
+IO.save
+: ∀(A: *)
+  ∀(file: String)
+  ∀(data: String)
+  ∀(then: ∀(x: Unit) (IO A))
+  (IO A)
+= λA λfile λdata λthen
+  ~λP λprint λload λsave λdone
+  (save file data then)
+
diff --git a/book/Kind.Scope.find.kind2 b/book/Kind.Scope.find.kind2
index 6ee235fe..d2ec9905 100644
--- a/book/Kind.Scope.find.kind2
+++ b/book/Kind.Scope.find.kind2
@@ -8,4 +8,4 @@ Kind.Scope.find
   let P     = λx(Kind.Term)
   let some  = λbnd (~bnd λx(Kind.Term) λnλt(t))
   let none  = (Kind.ref name Kind.set) // FIXME: handle unbound reference
-  (~found P some none)
\ No newline at end of file
+  (~found P some none)
diff --git a/book/Kind.Scope.kind2 b/book/Kind.Scope.kind2
index 595f3c57..aacebd26 100644
--- a/book/Kind.Scope.kind2
+++ b/book/Kind.Scope.kind2
@@ -1,3 +1,3 @@
 Kind.Scope
 : *
-= (List Kind.Binder)
\ No newline at end of file
+= (List Kind.Binder)
diff --git a/book/Kind.Scope.nil.kind2 b/book/Kind.Scope.nil.kind2
index b637e67a..63d24b3a 100644
--- a/book/Kind.Scope.nil.kind2
+++ b/book/Kind.Scope.nil.kind2
@@ -1,3 +1,3 @@
 Kind.Scope.nil
 : Kind.Scope
-= (List.nil Kind.Binder)
\ No newline at end of file
+= (List.nil Kind.Binder)
diff --git a/book/Kind.Term.parser.app.kind2 b/book/Kind.Term.parser.app.kind2
index 737ae225..78ee53e1 100644
--- a/book/Kind.Term.parser.app.kind2
+++ b/book/Kind.Term.parser.app.kind2
@@ -7,6 +7,6 @@ Kind.Term.parser.app
   (Kind.Term.parser.bind Unit (Parser.text ")") λ_
   (Kind.Term.parser.pure λscp
   (((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term
-  λargλrecλfun(rec (Kind.app fun (arg scp)))
+  λarg λrec λfun (rec (Kind.app fun (arg scp)))
   λfun(fun))
-  (fun scp))))))))
\ No newline at end of file
+  (fun scp))))))))
diff --git a/book/Kind.Term.parser.def.kind2 b/book/Kind.Term.parser.def.kind2
index c4216e4f..015e4657 100644
--- a/book/Kind.Term.parser.def.kind2
+++ b/book/Kind.Term.parser.def.kind2
@@ -7,4 +7,4 @@ Kind.Term.parser.def
   (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser      λval
   (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser      λbod
   (Kind.Term.parser.pure λscp 
-  (Kind.def nam (val scp) λx(bod (Kind.Scope.extend nam x scp))))))))))
\ No newline at end of file
+  (Kind.def nam (val scp) λx(bod (Kind.Scope.extend nam x scp))))))))))
diff --git a/book/Kind.Term.parser.hol.kind2 b/book/Kind.Term.parser.hol.kind2
index 309b8324..57f6ad03 100644
--- a/book/Kind.Term.parser.hol.kind2
+++ b/book/Kind.Term.parser.hol.kind2
@@ -4,4 +4,4 @@ Kind.Term.parser.hol
   (Kind.Term.parser.bind Unit   (Parser.text "?") λ_
   (Kind.Term.parser.bind String Parser.name       λnam
   (Kind.Term.parser.pure λscp
-  (Kind.hol nam (List.nil Kind.Term)))))) // TODO: build context
\ No newline at end of file
+  (Kind.hol nam (List.nil Kind.Term)))))) // TODO: build context
diff --git a/book/Kind.Term.to_hvm.kind2 b/book/Kind.Term.to_hvm.kind2
index 06a3ccd4..894a9111 100644
--- a/book/Kind.Term.to_hvm.kind2
+++ b/book/Kind.Term.to_hvm.kind2
@@ -3,4 +3,4 @@ Kind.Term.to_hvm
   ∀(dep: Nat)
   String
 = λterm λdep
-  (String.Concatenator.build (Kind.Term.to_hvm.go term dep))
+  (String.Concatenator.build (Kind.Term.to_hvm.go term dep Bool.true Nat.zero))
diff --git a/book/Kind.check.kind2 b/book/Kind.check.kind2
index 01902496..e017662f 100644
--- a/book/Kind.check.kind2
+++ b/book/Kind.check.kind2
@@ -55,4 +55,4 @@ Kind.check
     (pure Kind.set)
   let var = λterm.nam λterm.idx λtype λdep
     (Kind.verify (Kind.var term.nam term.idx) type dep)
-  (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var type dep)
\ No newline at end of file
+  (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var type dep)
diff --git a/book/Kind.load.code.kind2 b/book/Kind.load.code.kind2
new file mode 100644
index 00000000..b40d1413
--- /dev/null
+++ b/book/Kind.load.code.kind2
@@ -0,0 +1,8 @@
+// Loads a file into a book
+Kind.load.code
+: ∀(name: String)
+  (IO Kind.Book)
+= λname
+  (IO.load Kind.Book (String.concat name ".kind2") λdata
+  (IO.done Kind.Book (Kind.Book.parse data)))
+
diff --git a/book/Kind.load.dependencies.kind2 b/book/Kind.load.dependencies.kind2
new file mode 100644
index 00000000..216dea74
--- /dev/null
+++ b/book/Kind.load.dependencies.kind2
@@ -0,0 +1,13 @@
+// Loads a list of dependencies
+Kind.load.dependencies
+: ∀(deps: (List String))
+  ∀(book: Kind.Book)
+  (IO Kind.Book)
+= λdeps λbook
+  let P    = λx ∀(book: Kind.Book) (IO Kind.Book)
+  let cons = λdeps.head λdeps.tail λbook
+    (IO.bind Kind.Book Kind.Book (Kind.load.dependency deps.head book) λbook 
+    (Kind.load.dependencies deps.tail book))
+  let nil = λbook (IO.done Kind.Book book)
+  ((~deps P cons nil) book)
+
diff --git a/book/Kind.load.dependency.kind2 b/book/Kind.load.dependency.kind2
new file mode 100644
index 00000000..3375a045
--- /dev/null
+++ b/book/Kind.load.dependency.kind2
@@ -0,0 +1,13 @@
+// Loads a single dependency, if not present
+// FIXME: String.map.has.linear is removing the entry
+Kind.load.dependency
+: ∀(name: String)
+  ∀(book: Kind.Book)
+  (IO Kind.Book)
+= λname λbook
+  let has   = (String.Map.has Kind.Term name book)
+  let P     = λx ∀(book: Kind.Book) (IO Kind.Book)
+  let true  = λbook (IO.done Kind.Book book)
+  let false = λbook (Kind.load.name name book)
+  ((~has P true false) book)
+
diff --git a/book/Kind.load.kind2 b/book/Kind.load.kind2
index d22dc2a8..7c718f71 100644
--- a/book/Kind.load.kind2
+++ b/book/Kind.load.kind2
@@ -4,65 +4,3 @@ Kind.load
 = λname
   let book = (String.Map.new Kind.Term)
   (Kind.load.name name book)
-
-// Loads a file into a book
-Kind.load.code
-: ∀(name: String)
-  (IO Kind.Book)
-= λname
-  (IO.load Kind.Book (String.concat name ".kind2") λdata
-  (IO.done Kind.Book (Kind.Book.parse data)))
-
-// Loads a name into a book; then, load its dependencies
-Kind.load.name
-: ∀(name: String)
-  ∀(book: Kind.Book)
-  (IO Kind.Book)
-= λname λbook
-  (IO.bind Kind.Book Kind.Book (Kind.load.code name) λfile
-  let defs = (String.Map.to_list Kind.Term file)
-  let fold = (List.fold (Pair String Kind.Term) defs)
-  let set2 = λnam λval (String.Map.set Kind.Term nam val book)
-  let setP = λdef λbook (~def λx(Kind.Book) set2)
-  let book = (fold Kind.Book setP book)
-  let deps = (Kind.Book.get_refs file)
-  (Kind.load.dependencies deps book))
-  
-// Loads a list of dependencies
-Kind.load.dependencies
-: ∀(deps: (List String))
-  ∀(book: Kind.Book)
-  (IO Kind.Book)
-= λdeps λbook
-  let P    = λx ∀(book: Kind.Book) (IO Kind.Book)
-  let cons = λdeps.head λdeps.tail λbook
-    (IO.bind Kind.Book Kind.Book (Kind.load.dependency deps.head book) λbook 
-    (Kind.load.dependencies deps.tail book))
-  let nil = λbook (IO.done Kind.Book book)
-  ((~deps P cons nil) book)
-
-// Loads a single dependency, if not present
-// FIXME: String.map.has.linear is removing the entry
-Kind.load.dependency
-: ∀(name: String)
-  ∀(book: Kind.Book)
-  (IO Kind.Book)
-= λname λbook
-  let has   = (String.Map.has Kind.Term name book)
-  let P     = λx ∀(book: Kind.Book) (IO Kind.Book)
-  let true  = λbook (IO.done Kind.Book book)
-  let false = λbook (Kind.load.name name book)
-  ((~has P true false) book)
-
-//Kind.load.dependency
-//: ∀(name: String)
-  //∀(book: Kind.Book)
-  //(IO Kind.Book)
-//= λname λbook
-  //let P    = λx (IO Kind.Book)
-  //let new  = λhas λbook
-    //let P     = λx ∀(book: Kind.Book) (IO Kind.Book)
-    //let true  = λbook (IO.done Kind.Book book)
-    //let false = λbook (Kind.load.name name book)
-    //((~has P true false) book)
-  //(~(String.Map.has.linear Kind.Term name book) P new)
diff --git a/book/Kind.load.name.kind2 b/book/Kind.load.name.kind2
new file mode 100644
index 00000000..86317c63
--- /dev/null
+++ b/book/Kind.load.name.kind2
@@ -0,0 +1,15 @@
+// Loads a name into a book; then, load its dependencies
+Kind.load.name
+: ∀(name: String)
+  ∀(book: Kind.Book)
+  (IO Kind.Book)
+= λname λbook
+  (IO.bind Kind.Book Kind.Book (Kind.load.code name) λfile
+  let defs = (String.Map.to_list Kind.Term file)
+  let fold = (List.fold (Pair String Kind.Term) defs)
+  let set2 = λnam λval (String.Map.set Kind.Term nam val book)
+  let setP = λdef λbook (~def λx(Kind.Book) set2)
+  let book = (fold Kind.Book setP book)
+  let deps = (Kind.Book.get_refs file)
+  (Kind.load.dependencies deps book))
+  
diff --git a/book/Kind.reduce.op2.kind2 b/book/Kind.reduce.op2.kind2
index 948c666f..c675e714 100644
--- a/book/Kind.reduce.op2.kind2
+++ b/book/Kind.reduce.op2.kind2
@@ -13,6 +13,7 @@ Kind.reduce.op2
       let mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val))
       let sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val))
       let div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val))
+      let mod = λfst_val λsnd_val (Kind.num #(% fst_val snd_val))
       let eq  = λfst_val λsnd_val (Kind.num #(== fst_val snd_val))
       let ne  = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val))
       let lt  = λfst_val λsnd_val (Kind.num #(< fst_val snd_val))
@@ -24,8 +25,8 @@ Kind.reduce.op2
       let xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val))
       let lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val))
       let rsh = λfst_val λsnd_val (Kind.num #(>> fst_val snd_val))
-      (~opr P add mul sub div eq ne lt gt lte gte and or xor lsh rsh fst_val snd_val)
+      ((~opr P add mul sub div mod eq ne lt gt lte gte and or xor lsh rsh) fst_val snd_val)
     let N = λsnd λfst_val (Kind.op2 opr (Kind.num fst_val) snd)
     (Kind.if.num snd P Y N fst_val)
   let N = λfst λsnd (Kind.op2 opr fst snd)
-  (Kind.if.num fst P Y N snd)
\ No newline at end of file
+  (Kind.if.num fst P Y N snd)
diff --git a/book/Main.kind2 b/book/Main.kind2
index cafeebf1..60cb14c8 100644
--- a/book/Main.kind2
+++ b/book/Main.kind2
@@ -1,5 +1,16 @@
 Main
-= (Kind.API.to_hvm "Bool")
+: #U60
+= #(+ #12 #30)
+
+//TYPE_MISMATCH
+//- expected: (Pair (Maybe V) (String.Map V))
+//- detected: (Pair (Maybe V) (BBT String V))
+//- bad_term: (BBT.got String V String.cmp key map)
+//./String.Map.kind2
+  //20 |   (BBT.got String V String.cmp key map)
+
+//(List.cons (Pair Char Char) (Pair.new Char Char Char  #8)  // '\b'
+  //(List.nil (Pair Char Char)))
 
 
 //Main
diff --git a/book/String.Map.get.kind2 b/book/String.Map.get.kind2
new file mode 100644
index 00000000..bda45a4a
--- /dev/null
+++ b/book/String.Map.get.kind2
@@ -0,0 +1,8 @@
+String.Map.get
+: ∀(V: *)
+  ∀(key: String)
+  ∀(map: (String.Map V))
+  (Maybe V)
+= λV λkey λmap
+  (BBT.get String V String.cmp key map)
+
diff --git a/book/String.Map.got.kind2 b/book/String.Map.got.kind2
new file mode 100644
index 00000000..b5cac13f
--- /dev/null
+++ b/book/String.Map.got.kind2
@@ -0,0 +1,8 @@
+String.Map.got 
+: ∀(V: *)
+  ∀(key: String)
+  ∀(map: (String.Map V))
+  (Pair (Maybe V) (String.Map V))
+= λV λkey λmap
+  (BBT.got String V String.cmp key map)
+
diff --git a/book/String.Map.kind2 b/book/String.Map.kind2
index 7e141ecd..da3b74ad 100644
--- a/book/String.Map.kind2
+++ b/book/String.Map.kind2
@@ -2,34 +2,3 @@ String.Map
 :  ∀(V: *) 
    *
 = λV (BBT String V)
-
-String.Map.get
-: ∀(V: *)
-  ∀(key: String)
-  ∀(map: (String.Map V))
-  (Maybe V)
-= λV λkey λmap
-  (BBT.get String V String.cmp key map)
-
-String.Map.got 
-: ∀(V: *)
-  ∀(key: String)
-  ∀(map: (String.Map V))
-  (Pair (Maybe V) (String.Map V))
-= λV λkey λmap
-  (BBT.got String V String.cmp key map)
-
-String.Map.set
-: ∀(V: *)
-  ∀(key: String)
-  ∀(val: V)
-  ∀(map: (String.Map V))
-  (String.Map V)
-= λV λkey λval λmap
-  (BBT.set String V String.cmp key val map)
-
-String.Map.new
-:  ∀(V: *)
-  (String.Map V)
-= λV (BBT.tip String V)
-
diff --git a/book/String.Map.new.kind2 b/book/String.Map.new.kind2
new file mode 100644
index 00000000..b31a7859
--- /dev/null
+++ b/book/String.Map.new.kind2
@@ -0,0 +1,5 @@
+String.Map.new
+:  ∀(V: *)
+  (String.Map V)
+= λV (BBT.tip String V)
+
diff --git a/book/String.Map.set.kind2 b/book/String.Map.set.kind2
new file mode 100644
index 00000000..5c30c599
--- /dev/null
+++ b/book/String.Map.set.kind2
@@ -0,0 +1,9 @@
+String.Map.set
+: ∀(V: *)
+  ∀(key: String)
+  ∀(val: V)
+  ∀(map: (String.Map V))
+  (String.Map V)
+= λV λkey λval λmap
+  (BBT.set String V String.cmp key val map)
+
diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2
index 530f233f..b956de2a 100644
--- a/book/U60.cmp.kind2
+++ b/book/U60.cmp.kind2
@@ -4,4 +4,4 @@ U60.cmp
   (Cmp)
 = λa λb
   (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql)
- 
\ No newline at end of file
+ 
diff --git a/book/_check_all.sh b/book/_check_all.sh
new file mode 100755
index 00000000..6eabbafe
--- /dev/null
+++ b/book/_check_all.sh
@@ -0,0 +1,4 @@
+for file in *.kind2; do
+  echo "checking ${file}"
+  kind2 check "${file%.*}"
+done
diff --git a/book/combined_Kind_files.kind2 b/book/combined_Kind_files.kind2
deleted file mode 100644
index 4d417337..00000000
--- a/book/combined_Kind_files.kind2
+++ /dev/null
@@ -1,99 +0,0 @@
-Kind.all
-: ∀(nam: String)
-  ∀(inp: Kind.Term)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λinp λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (all nam inp bod)Kind.ann
-: ∀(val: Kind.Term)
-  ∀(typ: Kind.Term)
-  Kind.Term
-= λval λtyp
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (ann val typ)
-Kind.app
-: ∀(fun: Kind.Term)
-  ∀(arg: Kind.Term)
-  Kind.Term
-= λfun λarg
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (app fun arg)
-Kind.def
-: ∀(nam: String)
-  ∀(val: Kind.Term)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λval λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (def nam val bod)Kind.hol
-: ∀(nam: String)
-  ∀(ctx: (List Kind.Term))
-  Kind.Term
-= λnam λctx
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (hol nam ctx)Kind.ins
-: ∀(val: Kind.Term)
-  Kind.Term
-= λval
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (ins val)Kind.lam
-: ∀(nam: String)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (lam nam bod)
-Kind.mat
-: ∀(nam: String)
-  ∀(x: Kind.Term)
-  ∀(z: Kind.Term)
-  ∀(s: ∀(x: Kind.Term) Kind.Term)
-  ∀(p: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λx λz λs λp
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (mat nam x z s p)Kind.num
-: ∀(val: #U60)
-  Kind.Term
-= λval
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (num val)Kind.op2
-: ∀(opr: Kind.Oper)
-  ∀(fst: Kind.Term)
-  ∀(snd: Kind.Term)
-  Kind.Term
-= λopr λfst λsnd
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (op2 opr fst snd)Kind.ref
-: ∀(nam: String)
-  ∀(val: Kind.Term)
-  Kind.Term
-= λnam λval
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (ref nam val)Kind.set
-: Kind.Term
-= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (set)
-Kind.slf
-: ∀(nam: String)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (slf nam bod)Kind.txt
-: ∀(lit: Kind.Text)
-  Kind.Term
-= λlit
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (txt lit)Kind.u60
-: Kind.Term
-= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  u60
-Kind.var
-: ∀(nam: String)
-  ∀(idx: Nat)
-  Kind.Term
-= λnam λidx
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (var nam idx)
\ No newline at end of file
diff --git a/book/combined_Term_files_specific.kind2 b/book/combined_Term_files_specific.kind2
deleted file mode 100644
index e69de29b..00000000
diff --git a/book/test7.kind2 b/book/test7.kind2
index 8a52bd00..e763fdf6 100644
--- a/book/test7.kind2
+++ b/book/test7.kind2
@@ -1,6 +1,6 @@
 test7.book
 : String
-= `
+= "
 Kind.Term
 : *
 = $self
@@ -22,7 +22,7 @@ Kind.Term
   ∀(hol: ∀(nam: String) ∀(ctx: (List Kind.Term)) (P (Kind.hol nam ctx)))
   ∀(var: ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx)))
   (P self)
-`
+"
 
 test7
 : (IO Unit)
diff --git a/kind2.ts b/kind2.ts
index 911e0556..65ae77c4 100755
--- a/kind2.ts
+++ b/kind2.ts
@@ -408,8 +408,6 @@ export function main() {
   // Runs 'hvm1 kind2.hvm1 -s -L -1'
 
   //const output = execSync("hvm1 run .kind2.hvm1 -s -L -1").toString();
-  
-
 
   //for (let name in book) {
     //console.log("Checking: " + name);
diff --git a/kind2.hvm1 b/src/kind2.hvm1
similarity index 61%
rename from kind2.hvm1
rename to src/kind2.hvm1
index 9f07c172..15b31050 100644
--- a/kind2.hvm1
+++ b/src/kind2.hvm1
@@ -29,14 +29,15 @@
   //| (Txt txt)
   //| (Hol nam ctx val)
   //| (Var nam idx) 
+  //| (Src src val)
 
 // Prelude
 // -------
 
 (Debug dep []  value) = value
-(Debug dep msg value) = (HVM.print (Join msg) value)
+(Debug dep msg value) = (HVM.print (String.join msg) value)
 //(Debug dep []  value) = value
-//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (Join msg) value))
+//(Debug dep msg value) = (If (> dep 10) 1 (HVM.print (String.join msg) value))
 
 (NewLine) = (String.cons 10 String.nil)
 (Quote)   = (String.cons 34 String.nil)
@@ -70,23 +71,50 @@
 (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))
+(String.concat String.nil         ys) = ys
+(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
 
-(Join List.nil)         = ""
-(Join (List.cons x xs)) = (Concat x (Join xs))
+(String.join List.nil)         = ""
+(String.join (List.cons x xs)) = (String.concat x (String.join xs))
 
-(Fst (Pair fst snd)) = fst
-(Snd (Pair fst snd)) = snd
+(Pair.fst (Pair fst snd)) = fst
+(Pair.snd (Pair fst snd)) = snd
 
-(Get (Pair fst snd) fun) = (fun fst snd)
+(Pair.get (Pair fst snd) fun) = (fun fst snd)
 
-(Pure x) = (Some x)
+(Maybe.pure x) = (Some x)
 
-(Bind a b) = (Bind.match a b)
+(Maybe.bind a b) = (Maybe.bind.match a b)
 
-(Bind.match None     b) = None
-(Bind.match (Some a) b) = (b a)
+(Maybe.bind.match None     b) = None
+(Maybe.bind.match (Some a) b) = (b a)
+
+(String.color RESET)      = (String.cons 27 "[0m")
+(String.color BRIGHT)     = (String.cons 27 "[1m")
+(String.color DIM)        = (String.cons 27 "[2m")
+(String.color UNDERSCORE) = (String.cons 27 "[4m")
+(String.color BLINK)      = (String.cons 27 "[5m")
+(String.color REVERSE)    = (String.cons 27 "[7m")
+(String.color HIDDEN)     = (String.cons 27 "[8m")
+(String.color BLACK)      = (String.cons 27 "[30m")
+(String.color RED)        = (String.cons 27 "[31m")
+(String.color GREEN)      = (String.cons 27 "[32m")
+(String.color YELLOW)     = (String.cons 27 "[33m")
+(String.color BLUE)       = (String.cons 27 "[34m")
+(String.color MAGENTA)    = (String.cons 27 "[35m")
+(String.color CYAN)       = (String.cons 27 "[36m")
+(String.color WHITE)      = (String.cons 27 "[37m")
+(String.color GRAY)       = (String.cons 27 "[90m")
+(String.color BG_BLACK)   = (String.cons 27 "[40m")
+(String.color BG_RED)     = (String.cons 27 "[41m")
+(String.color BG_GREEN)   = (String.cons 27 "[42m")
+(String.color BG_YELLOW)  = (String.cons 27 "[43m")
+(String.color BG_BLUE)    = (String.cons 27 "[44m")
+(String.color BG_MAGENTA) = (String.cons 27 "[45m")
+(String.color BG_CYAN)    = (String.cons 27 "[46m")
+(String.color BG_WHITE)   = (String.cons 27 "[47m")
+(String.color BG_GRAY)    = (String.cons 27 "[100m")
+(String.color x)          = "?"
 
 // Evaluation
 // ----------
@@ -99,6 +127,7 @@
 (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 (Src src val))     = (Reduce r val)
 (Reduce r val)               = val
 
 (Reduce.app r (Lam nam bod)     arg) = (Reduce r (bod (Reduce 0 arg)))
@@ -147,27 +176,27 @@
 (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 (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (String.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)
+(Normal.term r (Src src val)     dep) = (Src src (Normal r val dep))
 
 // Equality
 // --------
 
 // Check if two terms are identical. If not...
-//(Equal a b 8)  = 0 // limits depth FIXME: won't be necessary with better ref-ids equality
 (Equal a b dep) = (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) = let a = (Reduce 0 a); let b = (Reduce 0 b); (Equal.major (Identical a b dep) a b dep)
+(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) = let a = (Reduce 1 a); let b = (Reduce 1 b); (Equal.enter (Identical a b dep) a b dep)
+(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 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) (Reduce 0 a) (Reduce 0 b) dep)
 (Equal.enter 1 a b dep) = 1
 
 // Checks if two terms are identical, without reductions.
@@ -193,8 +222,10 @@
 (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 b.fst dep) (rec a.snd 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 (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 (String.concat a.nam "-1") dep)) (b.s (Var (String.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 (Src a.src a.val)           b                           dep) = (Comparer rec a.val b dep)
+(Comparer rec a                           (Src b.src b.val)           dep) = (Comparer rec a b.val dep)
 (Comparer rec a                           b                           dep) = 0
 //(Comparer rec a                           b                           dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
 
@@ -211,29 +242,29 @@
 (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)))
+  (Maybe.bind (Check 0 inp Set dep) λinp_typ
+  (Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
+  (Maybe.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
+  (Maybe.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)))
+      (Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
+      (Maybe.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)
+  (Maybe.pure typ)
 (Infer.match (Slf nam bod) dep) =
-  (Bind (Check (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
-  (Pure Set))
+  (Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
+  (Maybe.pure Set))
 (Infer.match (Ins val) dep) =
-  (Bind (Infer val dep) λval_typ
+  (Maybe.bind (Infer val dep) λval_typ
   ((IfSlf (Reduce 1 val_typ)
-    λval_nam λval_typ.bod λval (Pure (val_typ.bod (Ins val)))
+    λval_nam λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
     λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
     val))
 (Infer.match (Ref nam val) dep) = 
@@ -241,99 +272,103 @@
 (Infer.match (Let nam val bod) dep) =
   (Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
 (Infer.match Set dep) =
-  (Pure Set)
+  (Maybe.pure Set)
 (Infer.match U60 dep) =
-  (Pure Set)
+  (Maybe.pure Set)
 (Infer.match (Num num) dep) =
-  (Pure U60)
+  (Maybe.pure U60)
 (Infer.match (Txt txt) dep) =
-  (Pure Book.String)
+  (Maybe.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)
+  (Maybe.bind (Check 0 fst U60 dep) λfst
+  (Maybe.bind (Check 0 snd U60 dep) λsnd
+  (Maybe.pure U60)))
 (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))))))
+  (Maybe.bind (Check 0 x U60 dep) λx_typ
+  (Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
+  (Maybe.bind (Check 0 z (p (Num 0)) dep) λz_typ
+  (Maybe.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
+  (Maybe.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)
+(Infer.match (Src src val) dep) =
+  (Infer.match val dep)
 
-//(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 term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 term type dep))
+(Check src term type dep) = (Check.match src term type dep)
 
-(Check.match (Lam term.nam term.bod) type dep) =
+(Check.match src (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))
+      (Check 0 term type (+ dep 1))
     λterm.bod
       (Infer (Lam term.nam term.bod) dep))
     term.bod)
-(Check.match (Ins term.val) type dep) =
+(Check.match src (Ins term.val) type dep) =
   ((IfSlf (Reduce 1 type)
-    λtype.nam λtype.bod λterm.val (Check term.val (type.bod (Ins term.val)) dep)
+    λtype.nam λtype.bod λterm.val (Check 0 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.match src (Let term.nam term.val term.bod) type dep) =
+  (Check 0 (term.bod term.val) type (+ 1 dep))
+(Check.match src (Hol term.nam term.ctx) type dep) =
+  (Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
+  (Maybe.pure 0))
+(Check.match src (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
+  (Check.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
+(Check.match src (Src term.src term.val) type dep) =
+  (Check term.src term.val type dep)
+//(Check.match src (Ref term.nam term.val) type dep) =
   //(Check term.val type dep)
-(Check.match term type dep) =
-  (Check.verify term type dep)
+(Check.match src term type dep) =
+  (Check.verify src term type dep)
 
-(Check.verify term type dep) =
-  (Bind (Infer term dep) λinfer
-  (Check.report (Equal type infer dep) infer type term dep))
+(Check.verify src term type dep) =
+  (Maybe.bind (Infer term dep) λinfer
+  (Check.report src (Equal type infer dep) infer type term dep))
 
-(Check.report 0 inferred expected value dep) =
-  let inf = (Show (Normal 0 inferred dep) dep)
+(Check.report src 0 detected expected value dep) =
+  let det = (Show (Normal 0 detected 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)
+  (Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
+    "- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
+    "- detected: " (String.color RESET) (String.color RED)   det NewLine (String.color RESET) (String.color BRIGHT)
+    "- bad_term: " (String.color RESET) (String.color DIM)   val NewLine (String.color RESET)
+    "##LOC{" (U60.show src) "}LOC##" NewLine
+  ] None)
+(Check.report src n inferred expected value dep) =
+  (Maybe.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.unwrap (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 (All nam inp bod) dep) = (String.join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (Lam nam bod)     dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (App fun arg)     dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
+(Show (Ann val typ)     dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
+(Show (Slf nam bod)     dep) = (String.join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show (Ins val)         dep) = (String.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 (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
+(Show Set               dep) = (String.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 (Num val)         dep) = (String.join ["#" (U60.show val)])
+(Show (Op2 opr fst snd) dep) = (String.join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
+(Show (Mat nam x z s p) dep) = (String.join ["#match " nam " = " (Show x dep) " { #0: " (Show z dep) " #+: " (Show (s (Var (String.concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
+(Show (Txt txt)         dep) = (String.join [Quote txt Quote])
+(Show (Hol nam ctx)     dep) = (String.join ["?" nam])
+(Show (Var nam idx)     dep) = (String.join [nam])
+(Show (Src src val)     dep) = (Show val dep)
+//(Show (Var nam idx)     dep) = (String.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.many (List.cons x xs) dep) = (String.join [" " (Show x dep) (Show.many xs dep)])
 
 (Show.trim (String.cons ' ' xs)) = xs
 (Show.trim str)                  = str
@@ -351,11 +386,11 @@
 (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 (List.cons x xs) dep) = (String.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 (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
 (Context.show.ann term          dep) = (Show (Normal 0 term dep) dep)
-//(Context.show.ann val           dep) = (Join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
+//(Context.show.ann val           dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
 
 // Compilation
 // -----------
@@ -388,6 +423,7 @@ Compile.primitives = [
 (Compile (Txt txt))         = (Str.make txt)
 (Compile (Hol nam ctx))     = 0
 (Compile (Var nam val))     = val
+(Compile (Src src val))     = (Compile val)
 
 //(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs))
 //(Compile.txt String.nil)         = Book.String.nil
@@ -420,12 +456,22 @@ Compile.primitives = [
 
 (Normalizer (Ref nam val)) = (Normalizer val)
 (Normalizer (Ann val typ)) = (Normalizer val)
+(Normalizer (Src src val)) = (Normalizer val)
 (Normalizer val)           = (Compile val)
 //(Normalizer val)           = (Str.view (Compile val))
 
-(Checker (Ref nam val)) = (Checker val)
-(Checker (Ann val typ)) = (Checker.report (Check val typ 0))
-(Checker val)           = (Checker.report (Infer val 0))
+(Checker name (Ref nam val))           = (Checker name val)
+(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
+(Checker name (Src src val))           = (Checker name val)
+(Checker name (Ann val typ))           = (Checker.report name (Check 0 val typ 0))
+(Checker name val)                     = (Checker.report name (Infer val 0))
 
-(Checker.report (Some x)) = (HVM.print "Check!" OK)
-(Checker.report None)     = (HVM.print "Error." ERR)
+(Checker.report name (Some x)) = 1
+(Checker.report name None)     = 0
+//(Checker.report name (Some x)) = (HVM.print (String.join [(String.color GREEN) "- " name ": ✔" (String.color RESET)]) 1)
+//(Checker.report name None)     = (HVM.print (String.join [(String.color RED) "- " name ": ✘" (String.color RESET)]) 0)
+
+(Checker.many.go (List.cons (Pair name def) defs)) = (& (Checker name def) (Checker.many.go defs))
+(Checker.many.go List.nil)                         = 1
+
+(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
diff --git a/src/main.rs b/src/main.rs
index ca3514dd..f204674f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -3,6 +3,11 @@
 use TSPL::Parser;
 use std::collections::HashMap;
 use std::collections::HashSet;
+use std::env;
+use std::fs::File;
+use std::io::Write;
+use std::process::Command;
+use highlight_error::highlight_error;
 //use std::fmt;
 
 #[derive(Clone, Copy)]
@@ -31,10 +36,12 @@ enum Term {
   Let { nam: String, val: Box<Term>, bod: Box<Term> },
   Hol { nam: String },
   Var { nam: String },
+  Src { src: u64, val: Box<Term> },
 }
 
 struct Book {
   defs: HashMap<String, Term>,
+  fids: HashMap<String, u64>,
 }
 
 // NOT USED ANYMORE
@@ -49,6 +56,22 @@ struct Book {
   //name
 //}
 
+pub fn new_src(fid: u64, ini: u64, end: u64) -> u64 {
+  (fid << 40) | (ini << 20) | end
+}
+
+pub fn src_fid(src: u64) -> u64 {
+  src >> 40
+}
+
+pub fn src_ini(src: u64) -> u64 {
+  (src >> 20) & 0xFFFFF
+}
+
+pub fn src_end(src: u64) -> u64 {
+  src & 0xFFFFF
+}
+
 pub fn cons<A>(vector: &im::Vector<A>, value: A) -> im::Vector<A> where A: Clone {
   let mut new_vector = vector.clone();
   new_vector.push_back(value);
@@ -117,26 +140,31 @@ impl Term {
       Term::Let { nam, val, bod } => format!("let {} = {} in {}", nam, val.show(), bod.show()),
       Term::Hol { nam } => format!("?{}", nam),
       Term::Var { nam } => nam.clone(),
+      Term::Src { src: _, val } => val.show(),
     }
   }
 
   fn to_hvm1(&self, env: im::Vector<String>) -> String {
+    fn binder(name: &str) -> String {
+      format!("_{}", name.replace("-", "._."))
+    }
     match self {
-      Term::All { nam, inp, bod } => format!("(All \"{}\" {} λ{} {})", nam, inp.to_hvm1(env.clone()), nam, bod.to_hvm1(cons(&env, nam.clone()))),
-      Term::Lam { nam, bod } => format!("(Lam \"{}\" λ{} {})", nam, nam, bod.to_hvm1(cons(&env, nam.clone()))),
+      Term::All { nam, inp, bod } => format!("(All \"{}\" {} λ{} {})", nam, inp.to_hvm1(env.clone()), binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
+      Term::Lam { nam, bod } => format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
       Term::App { fun, arg } => format!("(App {} {})", fun.to_hvm1(env.clone()), arg.to_hvm1(env.clone())),
       Term::Ann { val, typ } => format!("(Ann {} {})", val.to_hvm1(env.clone()), typ.to_hvm1(env.clone())),
-      Term::Slf { nam, bod } => format!("(Slf \"{}\" λ{} {})", nam, nam, bod.to_hvm1(cons(&env, nam.clone()))),
+      Term::Slf { nam, bod } => format!("(Slf \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
       Term::Ins { val } => format!("(Ins {})", val.to_hvm1(env.clone())),
       Term::Set => "(Set)".to_string(),
       Term::U60 => "(U60)".to_string(),
       Term::Num { val } => format!("(Num {})", val),
       Term::Op2 { opr, fst, snd } => format!("(Op2 {} {} {})", opr.to_hvm1(), fst.to_hvm1(env.clone()), snd.to_hvm1(env.clone())),
-      Term::Mat { nam, x, z, s, p } => format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x.to_hvm1(env.clone()), z.to_hvm1(env.clone()), nam, s.to_hvm1(cons(&env, nam.clone())), nam, p.to_hvm1(cons(&env, nam.clone()))),
+      Term::Mat { nam, x, z, s, p } => format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x.to_hvm1(env.clone()), z.to_hvm1(env.clone()), binder(&format!("{}-1",nam)), s.to_hvm1(cons(&env, format!("{}-1",nam))), binder(nam), p.to_hvm1(cons(&env, nam.clone()))),
       Term::Txt { txt } => format!("(Txt \"{}\")", txt),
-      Term::Let { nam, val, bod } => format!("(Let \"{}\" {} λ{} {})", nam, val.to_hvm1(env.clone()), nam, bod.to_hvm1(cons(&env, nam.clone()))),
-      Term::Hol { nam } => format!("(Hol \"{}\" [{}])", nam, env.iter().map(|n| format!("\"{}\"", n)).collect::<Vec<_>>().join(",")),
-      Term::Var { nam } => if env.contains(nam) { nam.clone() } else { format!("(Book.{})", nam) },
+      Term::Let { nam, val, bod } => format!("(Let \"{}\" {} λ{} {})", nam, val.to_hvm1(env.clone()), binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
+      Term::Hol { nam } => format!("(Hol \"{}\" [{}])", nam, env.iter().map(|n| binder(n)).collect::<Vec<_>>().join(",")),
+      Term::Var { nam } => if env.contains(nam) { format!("{}", binder(nam)) } else { format!("(Book.{})", nam) },
+      Term::Src { src, val } => format!("(Src {} {})", src, val.to_hvm1(env)),
     }
   }
 
@@ -173,7 +201,7 @@ impl Term {
       Term::Mat { nam, x, z, s, p } => {
         x.get_free_vars(env.clone(), free);
         z.get_free_vars(env.clone(), free);
-        s.get_free_vars(cons(&env, nam.clone()), free);
+        s.get_free_vars(cons(&env, format!("{}-1",nam)), free);
         p.get_free_vars(cons(&env, nam.clone()), free);
       },
       Term::Txt { txt: _ } => {},
@@ -182,6 +210,9 @@ impl Term {
         bod.get_free_vars(cons(&env, nam.clone()), free);
       },
       Term::Hol { nam: _ } => {},
+      Term::Src { src: _, val } => {
+        val.get_free_vars(env, free);
+      },
       Term::Var { nam } => {
         if !env.contains(nam) {
           free.insert(nam.clone());
@@ -202,120 +233,151 @@ impl<'i> KindParser<'i> {
       Some('*') => { self.advance_one(); Ok(Oper::Mul) }
       Some('/') => { self.advance_one(); Ok(Oper::Div) }
       Some('%') => { self.advance_one(); Ok(Oper::Mod) }
-      Some('=') => { self.consume("=")?; Ok(Oper::Eq) }
+      Some('=') => { self.consume("==")?; Ok(Oper::Eq) }
       Some('!') => { self.consume("!=")?; Ok(Oper::Ne) }
       Some('<') => {
         match self.peek_many(2) {
           Some("<=") => { self.advance_many(2); Ok(Oper::Lte) }
+          Some("<<") => { self.advance_many(2); Ok(Oper::Lsh) }
           _ => { self.advance_one(); Ok(Oper::Lt) }
         }
       }
       Some('>') => {
         match self.peek_many(2) {
           Some(">=") => { self.advance_many(2); Ok(Oper::Gte) }
+          Some(">>") => { self.advance_many(2); Ok(Oper::Rsh) }
           _ => { self.advance_one(); Ok(Oper::Gt) }
         }
       }
       Some('&') => { self.advance_one(); Ok(Oper::And) }
       Some('|') => { self.advance_one(); Ok(Oper::Or) }
       Some('^') => { self.advance_one(); Ok(Oper::Xor) }
-      Some('l') => { self.consume("<<")?; Ok(Oper::Lsh) }
-      Some('r') => { self.consume(">>")?; Ok(Oper::Rsh) }
       _ => self.expected("operator"),
     }
   }
-  
-  fn parse_term(&mut self) -> Result<Term, String> {
+
+  fn parse_term(&mut self, fid: u64) -> Result<Term, String> {
     self.skip_trivia();
     match self.peek_one() {
       Some('∀') => {
+        let ini = *self.index() as u64;
         self.consume("∀")?;
         self.consume("(")?;
         let nam = self.parse_name()?;
         self.consume(":")?;
-        let inp = Box::new(self.parse_term()?);
+        let inp = Box::new(self.parse_term(fid)?);
         self.consume(")")?;
-        let bod = Box::new(self.parse_term()?);
-        Ok(Term::All { nam, inp, bod })
+        let bod = Box::new(self.parse_term(fid)?);
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::All { nam, inp, bod }) })
       }
       Some('λ') => {
+        let ini = *self.index() as u64;
         self.consume("λ")?;
         let nam = self.parse_name()?;
-        let bod = Box::new(self.parse_term()?);
-        Ok(Term::Lam { nam, bod })
+        let bod = Box::new(self.parse_term(fid)?);
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Lam { nam, bod }) })
       }
       Some('(') => {
+        let ini = *self.index() as u64;
         self.consume("(")?;
-        let fun = Box::new(self.parse_term()?);
+        let fun = Box::new(self.parse_term(fid)?);
         let mut args = Vec::new();
         while self.peek_one() != Some(')') {
-          args.push(Box::new(self.parse_term()?));
+          args.push(Box::new(self.parse_term(fid)?));
+          self.skip_trivia();
         }
         self.consume(")")?;
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
         let mut app = fun;
         for arg in args {
           app = Box::new(Term::App { fun: app, arg });
         }
-        Ok(*app)
+        Ok(Term::Src { src, val: app })
       }
       Some('{') => {
+        let ini = *self.index() as u64;
         self.consume("{")?;
-        let val = Box::new(self.parse_term()?);
+        let val = Box::new(self.parse_term(fid)?);
         self.consume(":")?;
-        let typ = Box::new(self.parse_term()?);
+        let typ = Box::new(self.parse_term(fid)?);
         self.consume("}")?;
-        Ok(Term::Ann { val, typ })
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Ann { val, typ }) })
       }
       Some('$') => {
+        let ini = *self.index() as u64;
         self.consume("$")?;
         let nam = self.parse_name()?;
-        let bod = Box::new(self.parse_term()?);
-        Ok(Term::Slf { nam, bod })
+        let bod = Box::new(self.parse_term(fid)?);
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Slf { nam, bod }) })
       }
       Some('~') => {
+        let ini = *self.index() as u64;
         self.consume("~")?;
-        let val = Box::new(self.parse_term()?);
-        Ok(Term::Ins { val })
+        let val = Box::new(self.parse_term(fid)?);
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Ins { val }) })
       }
       Some('*') => {
+        let ini = *self.index() as u64;
         self.consume("*")?;
-        Ok(Term::Set)
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Set) })
       }
       Some('#') => {
+        let ini = *self.index() as u64;
         self.consume("#")?;
         match self.peek_one() {
           Some('U') => {
             self.consume("U60")?;
-            Ok(Term::U60)
+            let end = *self.index() as u64;
+            let src = new_src(fid, ini, end);
+            Ok(Term::Src { src, val: Box::new(Term::U60) })
           }
           Some('(') => {
             self.consume("(")?;
             let opr = self.parse_oper()?;
-            let fst = Box::new(self.parse_term()?);
-            let snd = Box::new(self.parse_term()?);
+            let fst = Box::new(self.parse_term(fid)?);
+            let snd = Box::new(self.parse_term(fid)?);
             self.consume(")")?;
-            Ok(Term::Op2 { opr, fst, snd })
+            let end = *self.index() as u64;
+            let src = new_src(fid, ini, end);
+            Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) })
           }
           Some('m') => {
             self.consume("match")?;
             let nam = self.parse_name()?;
             self.consume("=")?;
-            let x = Box::new(self.parse_term()?);
+            let x = Box::new(self.parse_term(fid)?);
             self.consume("{")?;
             self.consume("#0")?;
             self.consume(":")?;
-            let z = Box::new(self.parse_term()?);
+            let z = Box::new(self.parse_term(fid)?);
             self.consume("#+")?;
             self.consume(":")?;
-            let s = Box::new(self.parse_term()?);
+            let s = Box::new(self.parse_term(fid)?);
             self.consume("}")?;
             self.consume(":")?;
-            let p = Box::new(self.parse_term()?);
-            Ok(Term::Mat { nam, x, z, s, p })
+            let p = Box::new(self.parse_term(fid)?);
+            let end = *self.index() as u64;
+            let src = new_src(fid, ini, end);
+            Ok(Term::Src { src, val: Box::new(Term::Mat { nam, x, z, s, p }) })
           }
           Some(_) => {
             let val = self.parse_u64()?;
-            Ok(Term::Num { val })
+            let end = *self.index() as u64;
+            let src = new_src(fid, ini, end);
+            Ok(Term::Src { src, val: Box::new(Term::Num { val }) })
           }
           _ => {
             self.expected("numeric-expression")
@@ -323,54 +385,69 @@ impl<'i> KindParser<'i> {
         }
       }
       Some('?') => {
+        let ini = *self.index() as u64;
         self.consume("?")?;
         let nam = self.parse_name()?;
-        Ok(Term::Hol { nam })
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Hol { nam }) })
       }
       Some('\'') => {
+        let ini = *self.index() as u64;
         let chr = self.parse_quoted_char()?;
-        Ok(Term::Num { val: chr as u64 })
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Num { val: chr as u64 }) })
       }
       Some('"') => {
+        let ini = *self.index() as u64;
         let txt = self.parse_quoted_string()?;
-        Ok(Term::Txt { txt })
+        let end = *self.index() as u64;
+        let src = new_src(fid, ini, end);
+        Ok(Term::Src { src, val: Box::new(Term::Txt { txt }) })
       }
       _ => {
         if self.peek_many(4) == Some("let ") {
+          let ini = *self.index() as u64;
           self.advance_many(4);
           let nam = self.parse_name()?;
           self.consume("=")?;
-          let val = Box::new(self.parse_term()?);
-          let bod = Box::new(self.parse_term()?);
-          Ok(Term::Let { nam, val, bod })
+          let val = Box::new(self.parse_term(fid)?);
+          let bod = Box::new(self.parse_term(fid)?);
+          let end = *self.index() as u64;
+          let src = new_src(fid, ini, end);
+          Ok(Term::Src { src, val: Box::new(Term::Let { nam, val, bod }) })
         } else {
+          let ini = *self.index() as u64;
           let nam = self.parse_name()?;
-          Ok(Term::Var { nam })
+          let end = *self.index() as u64;
+          let src = new_src(fid, ini, end);
+          Ok(Term::Src { src, val: Box::new(Term::Var { nam }) })
         }
       }
     }
   }
-
-  fn parse_def(&mut self) -> Result<(String, Term), String> {
+  
+  fn parse_def(&mut self, fid: u64) -> Result<(String, Term), String> {
     let nam = self.parse_name()?;
     self.skip_trivia();
     if self.peek_one() == Some(':') {
       self.consume(":")?;
-      let typ = self.parse_term()?;
+      let typ = self.parse_term(fid)?;
       self.consume("=")?;
-      let val = self.parse_term()?;
+      let val = self.parse_term(fid)?;
       Ok((nam, Term::Ann { val: Box::new(val), typ: Box::new(typ) }))
     } else {
       self.consume("=")?;
-      let val = self.parse_term()?;
+      let val = self.parse_term(fid)?;
       Ok((nam, val))
     }
   }
 
-  fn parse_book(&mut self) -> Result<Book, String> {
+  fn parse_book(&mut self, fid: u64) -> Result<Book, String> {
     let mut book = Book::new();
     while *self.index() < self.input().len() {
-      let (name, term) = self.parse_def()?;
+      let (name, term) = self.parse_def(fid)?;
       book.defs.insert(name, term);
       self.skip_trivia();
     }
@@ -383,6 +460,7 @@ impl Book {
   fn new() -> Self {
     Book {
       defs: HashMap::new(),
+      fids: HashMap::new(),
     }
   }
   
@@ -404,48 +482,165 @@ impl Book {
     book_str
   }
 
-  fn load_file(filename: &str) -> Result<Self, String> {
-    std::fs::read_to_string(filename)
-      .map_err(|_| format!("Could not read file: {}", filename))
-      .and_then(|contents| KindParser::new(&contents).parse_book())
-  }
-
   fn load(name: &str) -> Result<Self, String> {
-    fn load_term(name: &str, book: &mut Book) -> Result<(), String> {
+    fn load_go(name: &str, book: &mut Book) -> Result<(), String> {
+      //println!("... {}", name);
       if !book.defs.contains_key(name) {
-        let file = format!("./book/{}.kind2", name);
+        let file = format!("./{}.kind2", name);
         let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?;
-        let defs = KindParser::new(&text).parse_book()?;
+        let fid  = book.get_file_id(&file);
+        //println!("... parsing: {}", name);
+        let defs = KindParser::new(&text).parse_book(fid)?;
+        //println!("... parsed: {}", name);
         for (def_name, def_term) in &defs.defs {
           book.defs.insert(def_name.clone(), def_term.clone());
         }
+        //println!("laoding deps for: {}", name);
         for (_, def_term) in defs.defs.into_iter() {
           let mut dependencies = HashSet::new();
           def_term.get_free_vars(im::Vector::new(), &mut dependencies);
+          //println!("{} deps: {:?}", name, dependencies);
           for ref_name in dependencies {
-            load_term(&ref_name, book)?;
+            load_go(&ref_name, book)?;
           }
         }
       }
       return Ok(());
     }
     let mut book = Book::new();
-    load_term(name, &mut book)?;
+    load_go(name, &mut book)?;
+    load_go("String", &mut book)?;
+    //println!("DONE!");
     Ok(book)
   }
 
+  fn get_file_id(&mut self, name: &str) -> u64 {
+    if let Some(id) = self.fids.get(name) {
+      *id
+    } else {
+      let id = self.fids.len() as u64 + 1;
+      self.fids.insert(name.to_string(), id);
+      id
+    }
+  }
+
+  // FIXME: asymptotics
+  fn get_file_name(&self, id: u64) -> Option<String> {
+    for (name, &fid) in &self.fids {
+      if fid == id {
+        return Some(name.clone());
+      }
+    }
+    None
+  }
+
+  fn inject_sources(&self, input: &str) -> Result<String, String> {
+    let mut result = input.to_string();
+    let ini_sym = "##LOC{";
+    let end_sym = "}LOC##";
+    while let (Some(ini), Some(end)) = (result.find(ini_sym), result.find(end_sym)) {
+      let got = &result[ini + ini_sym.len()..end];
+      let loc = got.parse::<u64>().map_err(|_| "Failed to parse location")?;
+      let fid = src_fid(loc);
+      let ini = src_ini(loc) as usize;
+      let end = src_end(loc) as usize;
+      if loc == 0 {
+        result = result.replace(&format!("{}{}{}", ini_sym, got, end_sym), "");
+      } else if let Some(file_name) = self.get_file_name(fid) {
+        let source_file = std::fs::read_to_string(&file_name).map_err(|_| "Failed to read source file")?;
+        let context_str = highlight_error(ini, end, &source_file);
+        let context_str = format!("\x1b[4m{}\x1b[0m\n{}", file_name, context_str);
+        result = result.replace(&format!("{}{}{}", ini_sym, got, end_sym), &context_str);
+      } else {
+        return Err("File ID not found".to_string());
+      }
+    }
+    Ok(result)
+  }
+
 }
 
-fn run() -> Result<(), String> {
-  let book = Book::load("Bool")?;
-  //let book = KindParser::new("f : * = ∀(a: *) λf λx (ID (f (f a b c)))").parse_book()?;
-  println!("{}", book.show());
-  println!("{}", book.to_hvm1());
-  return Ok(());
+//fn run() -> Result<(), String> {
+  //let book = Book::load("Nat")?;
+  //println!("{}", book.show());
+  //println!("{}", book.to_hvm1());
+  //return Ok(());
+//}
+
+//fn main() {
+  //if let Err(e) = run() {
+    //eprintln!("{}", e);
+  //}
+//}
+
+
+fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
+  // Gets used def names, sorted alphabetically.
+  let mut used_defs: Vec<_> = book.defs.keys().collect();
+  used_defs.sort();
+  let used_defs = used_defs.iter().map(|name| format!("(Pair \"{}\" Book.{})", name, name)).collect::<Vec<_>>().join(" ");
+  // Generates '.check.hvm1' contents.
+  let kind2_hvm1 = include_str!("./kind2.hvm1");
+  let book_hvm1 = book.to_hvm1();
+  let main_hvm1 = match command {
+    "check" => format!("Main = (Checker.many [{}])\n", used_defs),
+    "run"   => format!("Main = (Normalizer Book.{})\n", arg),
+    _       => panic!("invalid command"),
+  };
+  let hvm1_code = format!("{}\n{}\n{}", kind2_hvm1, book_hvm1, main_hvm1);
+  return hvm1_code;
 }
 
 fn main() {
-  if let Err(e) = run() {
-    eprintln!("{}", e);
+  let args: Vec<String> = env::args().collect();
+
+  if args.len() < 3 {
+    show_help();
+  }
+
+  let cmd = &args[1];
+  let arg = &args[2];
+
+  //println!("loading");
+  match cmd.as_str() {
+    "check" | "run" => {
+      match Book::load(arg) {
+        Ok(book) => {
+          //println!("loaded!");
+          let check_hvm1 = generate_check_hvm1(&book, cmd, arg);
+
+          // Saves it to a file.
+          let mut file = File::create(".check.hvm1").expect("Failed to create '.check.hvm1'.");
+          file.write_all(check_hvm1.as_bytes()).expect("Failed to write '.check.hvm1'.");
+
+          let output = Command::new("hvm1").arg("run").arg("-t").arg("1").arg("-c").arg("-f").arg(".check.hvm1").arg("(Main)").output().expect("Failed to execute command");
+          //let stdout : Result<String,String> = Ok(format!("{}", String::from_utf8_lossy(&output.stdout)));
+          let stdout = book.inject_sources(&format!("{}", String::from_utf8_lossy(&output.stdout)));
+          let stderr = String::from_utf8_lossy(&output.stderr);
+
+          match stdout {
+            //Ok(output) => println!("{}", output.replace("(ERRORS_FOUND)","")),
+            Ok(output) => println!("{}", output),
+            Err(error) => eprintln!("{}", error),
+          }
+
+          if !output.stderr.is_empty() {
+            eprintln!("{}", stderr);
+          }
+        },
+        Err(e) => {
+          eprintln!("{}", e);
+          std::process::exit(1);
+        },
+      }
+    },
+    _ => {
+      show_help();
+    },
   }
 }
+
+fn show_help() {
+  eprintln!("Usage: kind2 [check|run] <name>");
+  std::process::exit(1);
+}