Merge branch 'kind2-hvm2' of https://github.com/LunaAmora/kind2 into LunaAmora-kind2-hvm2

2024-07-07 10:06:36 +03:00 · 2024-03-14 18:32:03 -03:00 · 2024-03-14 18:32:03 -03:00 · d98da0863e
commit d98da0863e
parent f8ab510b1e 69bbdfc382
8 changed files with 1101 additions and 49 deletions
--- a/.gitignore
+++ b/.gitignore
@ -3,6 +3,7 @@
 .kind21/
 plans.txt
 .check.hvm1
+.check.hvm2
 demo/
 .fill.tmp
 .check.hs
--- a/src/book/compile.rs
+++ b/src/book/compile.rs
@ -22,6 +22,15 @@ impl Book {
    //code
  }

+  pub fn to_hvm2_checker(&self) -> String {
+    let mut code = String::new();
+    for (name, term) in &self.defs {
+      let expr = term.to_hvm2_checker(im::Vector::new(), &mut 0);
+      code.push_str(&format!("Book.{} = (Ref \"{}\" {})\n", name, name, expr));
+    }
+    code
+  }
+
  pub fn to_hs_checker(&self) -> String {
    let mut code = String::new();
    for (name, term) in &self.defs {
--- a/src/book/mod.rs
+++ b/src/book/mod.rs
@ -40,15 +40,15 @@ impl Book {
  }

  // Creates a book, loading a term, its dependencies, and stdlib
-  pub fn boot(name: &str) -> Result<Self, String> {
+  pub fn boot(base: &str, name: &str) -> Result<Self, String> {
    let mut book = Book::new();
-    book.load(name)?;
-    book.load("String")?;
-    book.load("String.cons")?;
-    book.load("String.nil")?;
-    book.load("Nat")?;
-    book.load("Nat.succ")?;
-    book.load("Nat.zero")?;
+    book.load(base, name)?;
+    book.load(base, "String")?;
+    book.load(base, "String.cons")?;
+    book.load(base, "String.nil")?;
+    book.load(base, "Nat")?;
+    book.load(base, "Nat.succ")?;
+    book.load(base, "Nat.zero")?;
    return Ok(book);
  }

@ -58,10 +58,10 @@ impl Book {
  }

  // Same as load, mutably adding to a 'book'
-  pub fn load(&mut self, name: &str) -> Result<(), String> {
+  pub fn load(&mut self, base: &str, name: &str) -> Result<(), String> {
    if !self.defs.contains_key(name) {
      // Parses a file into a new book
-      let file = format!("./{}.kind2", name);
+      let file = format!("{}/{}.kind2", base, name);
      let text = std::fs::read_to_string(&file).map_err(|_| format!("Could not read file: {}", file))?;
      let fid  = self.get_file_id(&file);
      let defs = KindParser::new(&text).parse_book(name, fid)?;
@ -74,7 +74,7 @@ impl Book {
        let mut dependencies = BTreeSet::new();
        def_term.get_free_vars(im::Vector::new(), &mut dependencies);
        for ref_name in dependencies {
-          if let Err(_) = self.load(&ref_name) {
+          if let Err(_) = self.load(&base, &ref_name) {
            self.handle_unbound(&file, &ref_name)?;
          }
        }
--- a/src/info/mod.rs
+++ b/src/info/mod.rs
@ -76,7 +76,8 @@ impl Info {
      let mut parser = KindParser::new(line);
      match parser.parse_info() {
        Ok(info) => infos.push(info),
-        Err(_)   => println!(">> {}", line),
+        Err(_) if line == "*" => {}
+        Err(_)   => println!("{}", line),
      }
    }
    infos
--- a/src/kind2.hvm2
+++ b/src/kind2.hvm2
@ -0,0 +1,877 @@
+// This is a Haskell implementation of Kind2's type checker. Since Kind2 isn't
+// bootstrapped, we can't use Kind2 itself to type-check it, and developing a
+// complex checker in an untyped language (like HVM) is hard. As such, this
+// Haskell view helps me develop and debug the checker, and it is done in a way
+// that makes it easy to manually compile it to HVM, keeping an HVM view. It can
+// also be useful to let us benchmark all versions (GHC/HVM1/HVM2), giving us a
+// good idea on how these compare in performance.
+
+// Kind2 Types
+// -----------
+
+data Maybe
+  = (Some val)
+  | None
+
+data Bool
+  = False
+  | True
+
+data Oper
+  = ADD | SUB | MUL | DIV
+  | MOD | EQ  | NE  | LT
+  | GT  | LTE | GTE | AND
+  | OR  | XOR | LSH | RSH
+
+data Term
+  = (All nam inp bod) // All String Term (Term -> Term)
+  | (Lam nam bod)     // Lam String (Term -> Term)
+  | (App fun arg)     // App Term Term
+  | (Ann chk val typ) // Ann Bool Term Term
+  | (Slf nam typ bod) // Slf String Term (Term -> Term)
+  | (Ins val)         // Ins Term
+  | (Ref nam val)     // Ref String Term
+  | (Let nam val bod) // Let String Term (Term -> Term)
+  | (Use nam val bod) // Use String Term (Term -> Term)
+  | Set               // Set
+  | U60               // U60
+  | (Num val)         // Num U60
+  | (Op2 opr fst snd) // Op2 Oper Term Term
+  | (Swi nam x z s p) // Swi String Term Term (Term -> Term) (Term -> Term)
+  | (Hol nam ctx)     // Hol String [Term]
+  | (Met uid spn)     // Met U60 [Term]
+  | (Var nam idx)     // Var String U60
+  | (Src src val)     // Src U60 Term
+  | (Txt val)         // Txt String
+  | (Nat val)         // Nat Integer
+
+data Info
+  = (Found name type ctx dep)               // Found String Term [Term] Int
+  | (Solve name term dep)                   // Solve U60 Term U60
+  | (Error src detected expected value dep) // Error U60 Term Term Term Int
+  | (Vague name)                            // Vague String
+  | (Print value dep)                       // Print Term Int
+
+data Check = (Check a t1 t2 b)             // Check U60 Term Term U60
+data State = (State map check info)        // State (Map Term) [Check] [Info] -- state type
+data Res   = (Done state a) | (Fail state) // Done State a | Fail State -- result type
+data Env   = (Env env)                     // Env (State -> Res a) -- environment computation
+
+data Bits = (O bits) | (I bits) | E
+data Map  = (Leaf) | (Node v lft rgt) // Leaf | Node (Maybe a) (Map a) (Map a)
+
+// Prelude
+// -------
+// Note: many of these functions are present in Haskell, but we re-implement
+// them here in order to have identical equivalents on HVM's view.
+
+data Error
+  = Unreachable
+  | InvalidTopLevelDefinition
+
+If True  then else = then
+If False then else = else
+
+if 0 then else = else
+if n then else = then
+
+and True b  = b
+and False _ = False
+
+not True  = False
+not False = True
+
+eq lft rgt = (if (== lft rgt) True False)
+
+// map :: (a -> b) -> [a] -> [b]
+map f []               = []
+map f (List.cons x xs) = (List.cons (f x) (map f xs))
+
+// even :: U60 -> Bool
+even n = (eq (% n 2) 0)
+
+// reverse :: [a] -> [a] 
+reverse l =  (reverseGo l [])
+  reverseGo []               a = a
+  reverseGo (List.cons x xs) a = (reverseGo xs (List.cons x a))
+
+// elem :: (a -> a -> Bool) -> a -> [a] -> Bool
+elem cmp a []               = False
+elem cmp a (List.cons x xs) = (If (cmp a x) True (elem cmp a xs))
+
+// u60Show :: U60 -> String
+u60Show n = (u60ShowGo n "")
+  u60ShowGo n res        = (u60ShowGoMatch (< n 10) n res)
+  u60ShowGoMatch 0 n res = (u60ShowGo (/ n 10) (String.cons (+ '0' (% n 10)) res))
+  u60ShowGoMatch _ n res = (String.cons (+ '0' n) res)
+
+// u60Name :: U60 -> String
+u60Name n = (u60NameGo (+ n 1))
+  u60NameGo 0 = ""
+  u60NameGo n = (String.cons (+ 'a' (% (- n 1) 26)) (u60NameGo (/ (- n 1) 26)))
+
+// listFind :: Eq a => a -> [(a, b)] -> Maybe b
+listFind _    []                          = None
+listFind name (List.cons (nam, val) tail) = (If (stringEqual name nam) (Some val) (listFind name tail))
+
+// listMap :: (a -> b) -> [a] -> [b]
+listMap f []     = []
+listMap f (List.cons x xs) = (List.cons (f x) (listMap f xs))
+
+// listPush :: a -> [a] -> [a]
+listPush x []     = [x]
+listPush x (List.cons y ys) = (List.cons y (listPush x ys))
+
+// newLine :: String
+newLine = "\n"
+
+// quote :: String
+quote = "\""
+
+// stringEqual :: String -> String -> Bool
+stringEqual "" "" = True
+stringEqual "" _  = False
+stringEqual _  "" = False
+stringEqual (String.cons x xs) (String.cons y ys) = (if (== x y) (stringEqual xs ys) False)
+
+// stringConcat :: String -> String -> String
+stringConcat ""                 ys = ys
+stringConcat (String.cons x xs) ys = (String.cons x (stringConcat xs ys))
+
+// stringJoin :: [String] -> String
+stringJoin [] = ""
+stringJoin (List.cons x xs) = (stringConcat x (stringJoin xs))
+
+// stringTail :: String -> String
+stringTail "" = ""
+stringTail (String.cons _ xs) = xs
+
+// pairFst :: (a, b) -> a
+pairFst (fst, _) = fst
+
+// pairSnd :: (a, b) -> b
+pairSnd (_, snd) = snd
+
+// pairGet :: (a, b) -> (a -> b -> c) -> c
+pairGet (fst, snd) fun = (fun fst snd)
+
+// maybeMatch :: Maybe a -> (a -> b) -> b -> b
+maybeMatch (Some value) some _ = (some value)
+maybeMatch None      _    none = none
+
+// maybePure :: a -> Maybe a
+maybePure x = (Some x)
+
+// maybeBind :: Maybe a -> (a -> Maybe b) -> Maybe b
+maybeBind a b = (maybeMatch a b None)
+
+// key :: U60 -> Bits
+key 0 = E
+key 1 = (I E)
+key n = (If (even n)
+  (O (key (/ n 2)))
+  (I (key (/ n 2))))
+
+// mapNew :: Map a
+mapNew = Leaf
+
+// mapHas :: Bits -> Map a -> Bool
+mapHas E        (Node (Some _) _ _) = True
+mapHas (O bits) (Node _ lft _)      = (mapHas bits lft)
+mapHas (I bits) (Node _ _ rgt)      = (mapHas bits rgt)
+mapHas _        _                   = False
+
+// mapGet :: Bits -> Map a -> Maybe a
+mapGet E        (Node val _ _) = val
+mapGet (O bits) (Node _ lft _) = (mapGet bits lft)
+mapGet (I bits) (Node _ _ rgt) = (mapGet bits rgt)
+mapGet _        Leaf           = None
+
+// mapSet :: Bits -> a -> Map a -> Map a
+mapSet E        val Leaf             = (Node (Some val) Leaf Leaf)
+mapSet E        val (Node _ lft rgt) = (Node (Some val) lft rgt)
+mapSet (O bits) val Leaf             = (Node None (mapSet bits val Leaf) Leaf)
+mapSet (O bits) val (Node v lft rgt) = (Node v (mapSet bits val lft) rgt)
+mapSet (I bits) val Leaf             = (Node None Leaf (mapSet bits val Leaf))
+mapSet (I bits) val (Node v lft rgt) = (Node v lft (mapSet bits val rgt))
+
+// Environment
+// -----------
+
+// infoIsSolve :: Info -> Bool
+infoIsSolve (Solve _ _ _) = True
+infoIsSolve _             = False
+
+// Pattern matches on a computation result
+// resMatch :: Res a -> (State -> a -> b) -> (State -> Info -> b) -> b
+// resMatch (Done state value) done _    = (Done state value)
+// resMatch (Fail state)       _    fail = (Fail state)
+
+// Monadic bind function
+// envBind :: Env a -> (a -> Env b) -> Env b
+envBind (Env a) b = (Env (λstate (match (a state) {
+  (Done state_ value): let (Env b_) = (b value); (b_ state_)
+  (Fail state_)      : (Fail state_)
+})))
+
+// envPure :: a -> Env a
+envPure a = (Env λstate (Done state a))
+
+// envFail :: Env a
+envFail = (Env λstate (Fail state))
+
+// envRun :: Env a -> Res a
+envRun (Env chk) = (chk (State mapNew [] []))
+
+// envLog :: Info -> Env U60
+envLog log = (Env λstate let (State fill susp logs) = state; (Done (State fill susp (List.cons log logs)) 1))
+
+// envSnapshot :: Env State
+envSnapshot = (Env λstate (Done state state))
+
+// envRewind :: State -> Env U60
+envRewind state = (Env λ_ (Done state 0))
+
+// envSusp :: Check -> Env *
+envSusp chk = (Env λstate let (State fill susp logs) = state; (Done (State fill (listPush chk susp) logs) *))
+
+// envFill :: U60 -> Term -> Env *
+envFill k v = (Env λstate let (State fill susp logs) = state; (Done (State (mapSet (key k) v fill) susp logs) *))
+
+// envGetFill :: Env (Map Term)
+envGetFill = (Env λstate let (State fill susp logs) = state; (Done (State fill susp logs) fill))
+
+// envTakeSusp :: Env [Check]
+envTakeSusp = (Env λstate let (State fill susp logs) = state; (Done (State fill [] logs) susp))
+
+// instance Functor Env where
+//   fmap f (Env chk) = Env λlogs -> case chk logs of
+//     Done logs' a -> Done logs' (f a)
+//     Fail logs' -> Fail logs'
+
+// instance Applicative Env where
+//   pure = envPure
+//   (Env chkF) <*> (Env chkA) = Env λlogs -> case chkF logs of
+//     Done logs' f -> case chkA logs' of
+//       Done logs'' a -> Done logs'' (f a)
+//       Fail logs'' -> Fail logs''
+//     Fail logs' -> Fail logs'
+
+// instance Monad Env where
+//   (Env a) >>= b = envBind (Env a) b
+
+// Evaluation
+// ----------
+
+// Evaluation levels:
+// - 0: reduces refs never
+// - 1: reduces refs on redexes
+// - 2: reduces refs always
+
+// termReduce :: Map Term -> U60 -> Term -> Term
+termReduce fill lv (App fun arg)     = (termReduceApp fill lv (termReduce fill lv fun) arg)
+termReduce fill lv (Ann chk val typ) = (termReduce fill lv val)
+termReduce fill lv (Ins val)         = (termReduce fill lv val)
+termReduce fill lv (Ref nam val)     = (termReduceRef fill lv nam (termReduce fill lv val))
+termReduce fill lv (Let nam val bod) = (termReduce fill lv (bod val))
+termReduce fill lv (Use nam val bod) = (termReduce fill lv (bod val))
+termReduce fill lv (Op2 opr fst snd) = (termReduceOp2 fill lv opr (termReduce fill lv fst) (termReduce fill lv snd))
+termReduce fill lv (Swi nam x z s p) = (termReduceSwi fill lv nam (termReduce fill lv x) z s p)
+termReduce fill lv (Txt txt)         = (termReduceTxt fill lv txt)
+termReduce fill lv (Nat val)         = (termReduceNat fill lv val)
+termReduce fill lv (Src src val)     = (termReduce fill lv val)
+termReduce fill lv (Met uid spn)     = (termReduceMet fill lv uid spn)
+termReduce fill lv val               = val
+
+// termReduceApp :: Map Term -> U60 -> Term -> Term -> Term
+termReduceApp fill 2  (Ref nam val) arg = (termReduceApp fill 2 val arg)
+termReduceApp fill 1  (Ref nam val) arg = (termReduceApp fill 1 val arg)
+termReduceApp fill lv (Met uid spn) arg = (termReduce fill lv (Met uid (listPush arg spn)))
+termReduceApp fill lv (Lam nam bod) arg = (termReduce fill lv (bod (termReduce fill 0 arg)))
+termReduceApp fill lv fun arg           = (App fun arg)
+
+// termReduceMet :: Map Term -> U60 -> U60 -> [Term] -> Term
+termReduceMet fill lv uid spn = match (mapGet (key uid) fill) {
+  (Some val): (termReduce fill lv (termReduceMetSpine val spn))
+  (None)    : (Met uid spn)
+}
+
+// termReduceMetSpine :: Term -> [Term] -> Term
+termReduceMetSpine val []               = val
+termReduceMetSpine val (List.cons x xs) = (termReduceMetSpine (App val x) xs)
+
+// termReduceOp2 :: Map Term -> U60 -> Oper -> Term -> Term -> Term
+termReduceOp2 fill 1  op  (Ref _ x) (Num snd) = (termReduceOp2 fill 1 op x (Num snd))
+termReduceOp2 fill 2  op  (Ref _ x) (Num snd) = (termReduceOp2 fill 2 op x (Num snd))
+termReduceOp2 fill 1  op  (Num fst) (Ref _ x) = (termReduceOp2 fill 1 op (Num fst) x)
+termReduceOp2 fill 2  op  (Num fst) (Ref _ x) = (termReduceOp2 fill 2 op (Num fst) x)
+termReduceOp2 fill lv ADD (Num fst) (Num snd) = (Num (+ fst snd))
+termReduceOp2 fill lv SUB (Num fst) (Num snd) = (Num (- fst snd))
+termReduceOp2 fill lv MUL (Num fst) (Num snd) = (Num (* fst snd))
+termReduceOp2 fill lv DIV (Num fst) (Num snd) = (Num (/ fst snd))
+termReduceOp2 fill lv MOD (Num fst) (Num snd) = (Num (% fst snd))
+termReduceOp2 fill lv EQ  (Num fst) (Num snd) = (Num (== fst snd))
+termReduceOp2 fill lv NE  (Num fst) (Num snd) = (Num (!= fst snd))
+termReduceOp2 fill lv LT  (Num fst) (Num snd) = (Num (< fst snd))
+termReduceOp2 fill lv GT  (Num fst) (Num snd) = (Num (> fst snd))
+termReduceOp2 fill lv LTE (Num fst) (Num snd) = (Num (<= fst snd))
+termReduceOp2 fill lv GTE (Num fst) (Num snd) = (Num (>= fst snd))
+termReduceOp2 fill lv AND (Num fst) (Num snd) = (Num (& fst snd))
+termReduceOp2 fill lv OR  (Num fst) (Num snd) = (Num (| fst snd))
+termReduceOp2 fill lv XOR (Num fst) (Num snd) = (Num (^ fst snd))
+termReduceOp2 fill lv LSH (Num fst) (Num snd) = (Num (<< fst snd))
+termReduceOp2 fill lv RSH (Num fst) (Num snd) = (Num (>> fst snd))
+termReduceOp2 fill lv opr fst snd             = (Op2 opr fst snd)
+
+// termReduceSwi :: Map Term -> U60 -> String -> Term -> Term -> (Term -> Term) -> (Term -> Term) -> Term
+termReduceSwi fill 2  nam (Ref _ x)           z s p = (termReduceSwi fill 2 nam x z s p)
+termReduceSwi fill 1  nam (Ref _ x)           z s p = (termReduceSwi fill 1 nam x z s p)
+termReduceSwi fill lv nam (Num 0)             z s p = (termReduce fill lv z)
+termReduceSwi fill lv nam (Num n)             z s p = (termReduce fill lv (s (Num (- n 1))))
+termReduceSwi fill lv nam (Op2 ADD (Num 1) k) z s p = (termReduce fill lv (s k))
+termReduceSwi fill lv nam val                 z s p = (Swi nam val z s p)
+
+// termReduceRef :: Map Term -> U60 -> String -> Term -> Term
+termReduceRef fill 2  nam val = (termReduce fill 2 val)
+termReduceRef fill 1  nam val = (Ref nam val)
+termReduceRef fill lv nam val = (Ref nam val)
+
+// termReduceTxt :: Map Term -> U60 -> String -> Term
+termReduceTxt fill lv ""                 = (termReduce fill lv Book.String.nil)
+termReduceTxt fill lv (String.cons x xs) = (termReduce fill lv (App (App Book.String.cons (Num x)) (Txt xs)))
+
+// termReduceNat :: Map Term -> Int -> Integer -> Term
+termReduceNat fill lv 0 = Book.Nat.zero
+termReduceNat fill lv n = (App Book.Nat.succ (termReduceNat fill lv (- n 1)))
+
+// Normalization
+// -------------
+
+// termNormal :: Map Term -> U60 -> Term -> U60 -> Term
+// termNormal fill lv term dep = termNormalGo fill lv (termNormalPrefer fill (termReduce fill 0 term) (termReduce fill lv term)) dep where
+termNormal fill lv term dep = (termNormalGo fill lv (termReduce fill lv term) dep)
+
+  // termNormalPrefer fill soft (Lam _ _)   = soft
+  // termNormalPrefer fill soft (Slf _ _ _) = soft
+  // termNormalPrefer fill soft (All _ _ _) = soft
+  // termNormalPrefer fill soft hard        = hard
+
+  termNormalGo fill lv (All nam inp bod) dep = (All nam (termNormal fill lv inp dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
+  termNormalGo fill lv (Lam nam bod)     dep = (Lam nam (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
+  termNormalGo fill lv (App fun arg)     dep = (App (termNormal fill lv fun dep) (termNormal fill lv arg dep))
+  termNormalGo fill lv (Ann chk val typ) dep = (Ann chk (termNormal fill lv val dep) (termNormal fill lv typ dep))
+  termNormalGo fill lv (Slf nam typ bod) dep = (Slf nam typ (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
+  termNormalGo fill lv (Ins val)         dep = (Ins (termNormal fill lv val dep))
+  termNormalGo fill lv (Ref nam val)     dep = (Ref nam (termNormal fill lv val dep))
+  termNormalGo fill lv (Let nam val bod) dep = (Let nam (termNormal fill lv val dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
+  termNormalGo fill lv (Use nam val bod) dep = (Use nam (termNormal fill lv val dep) (λx (termNormal fill lv (bod (Var nam dep)) (+ dep 1))))
+  termNormalGo fill lv (Hol nam ctx)     dep = (Hol nam ctx)
+  termNormalGo fill lv Set               dep = (Set)
+  termNormalGo fill lv U60               dep = (U60)
+  termNormalGo fill lv (Num val)         dep = (Num val)
+  termNormalGo fill lv (Op2 opr fst snd) dep = (Op2 opr (termNormal fill lv fst dep) (termNormal fill lv snd dep))
+  termNormalGo fill lv (Swi nam x z s p) dep = (Swi nam (termNormal fill lv x dep) (termNormal fill lv z dep) (λk (termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep)) (λk (termNormal fill lv (p (Var nam dep)) dep)))
+  termNormalGo fill lv (Txt val)         dep = (Txt val)
+  termNormalGo fill lv (Nat val)         dep = (Nat val)
+  termNormalGo fill lv (Var nam idx)     dep = (Var nam idx)
+  termNormalGo fill lv (Src src val)     dep = (Src src (termNormal fill lv val dep))
+  termNormalGo fill lv (Met uid spn)     dep = (Met uid spn) // TODO: normalize spine
+
+// Equality
+// --------
+
+// termEqual :: Term -> Term -> U60 -> Env Bool
+termEqual a b dep =
+//   (trace (stringJoin ["equal:\n- ", (termShow a dep), "\n- ", (termShow b dep)])
+  (envBind envGetFill λfill
+  let a_ = (termReduce fill 2 a)
+  let b_ = (termReduce fill 2 b)
+  (termTryIdentical a_ b_ dep (termSimilar a_ b_ dep)))
+
+// termTryIdentical :: Term -> Term -> U60 -> Env Bool -> Env Bool
+termTryIdentical a b dep cont =
+  (envBind envSnapshot λstate
+  (envBind (termIdentical a b dep) λequal
+  (If equal
+    (envPure True)
+    (envBind (envRewind state) λ_ cont))))
+
+// termSimilar :: Term -> Term -> U60 -> Env Bool
+termSimilar (All aNam aInp aBod) (All bNam bInp bBod) dep =
+  (envBind (termEqual aInp bInp dep) λeInp
+  (envBind (termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1)) λeBod
+  (envPure (and eInp eBod))))
+termSimilar (Lam aNam aBod) (Lam bNam bBod) dep =
+  (termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1))
+termSimilar (App aFun aArg) (App bFun bArg) dep =
+  (envBind (termEqual aFun bFun dep) λeFun
+  (envBind (termEqual aArg bArg dep) λeArg
+  (envPure (and eFun eArg))))
+termSimilar (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
+  (termSimilar (termReduce mapNew 0 aTyp) (termReduce mapNew 0 bTyp) dep)
+// termSimilar (Hol aNam aCtx) (Hol bNam bCtx) dep =
+  // (envPure (eq aNam bNam))
+// termSimilar (Met aUid aSpn) (Met bUid bSpn) dep =
+  // (envPure (eq aUid bUid))
+termSimilar (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep =
+  (envBind (termEqual aFst bFst dep) λeFst
+  (envBind (termEqual aSnd bSnd dep) λeSnd
+  (envPure (and eFst eSnd))))
+termSimilar (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep =
+  (envBind (termEqual aX bX dep) λeX
+  (envBind (termEqual aZ bZ dep) λeZ
+  (envBind (termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) λeS
+  (envBind (termEqual (aP (Var aNam dep)) (bP (Var bNam dep)) dep) λeP
+  (envPure (and (and (and eX eZ) eS) eP))))))
+termSimilar a b dep = (envPure False)
+
+// termIdentical :: Term -> Term -> U60 -> Env Bool
+termIdentical a b dep = (termIdenticalGo a b dep)
+
+// termIdenticalGo :: Term -> Term -> U60 -> Env Bool
+termIdenticalGo (All aNam aInp aBod) (All bNam bInp bBod) dep =
+  (envBind (termIdentical aInp bInp dep) (λiInp
+  (envBind (termIdentical (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1)) λiBod
+  (envPure (and iInp iBod)))))
+termIdenticalGo (Lam aNam aBod) (Lam bNam bBod) dep =
+  (termIdentical (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1))
+termIdenticalGo (App aFun aArg) (App bFun bArg) dep =
+  (envBind (termIdentical aFun bFun dep) λiFun
+  (envBind (termIdentical aArg bArg dep) λiArg
+  (envPure (and iFun iArg))))
+termIdenticalGo (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
+  (termIdentical aTyp bTyp dep)
+termIdenticalGo (Ins aVal) b dep =
+  (termIdentical aVal b dep)
+termIdenticalGo a (Ins bVal) dep =
+  (termIdentical a bVal dep)
+termIdenticalGo (Let aNam aVal aBod) b dep =
+  (termIdentical (aBod aVal) b dep)
+termIdenticalGo a (Let bNam bVal bBod) dep =
+  (termIdentical a (bBod bVal) dep)
+termIdenticalGo (Use aNam aVal aBod) b dep =
+  (termIdentical (aBod aVal) b dep)
+termIdenticalGo a (Use bNam bVal bBod) dep =
+  (termIdentical a (bBod bVal) dep)
+termIdenticalGo Set Set dep =
+  (envPure True)
+termIdenticalGo (Ann chk aVal aTyp) b dep =
+  (termIdentical aVal b dep)
+termIdenticalGo a (Ann chk bVal bTyp) dep =
+  (termIdentical a bVal dep)
+// termIdenticalGo (Met aUid aSpn) (Met bUid bSpn) dep =
+  // envPure (eq aUid bUid)
+termIdenticalGo (Met aUid aSpn) b dep =
+  // traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)])
+  (termUnify aUid aSpn b dep)
+termIdenticalGo a (Met bUid bSpn) dep =
+  // traceShow (stringJoin ["unify: ", (u60Show bUid), " x=", (termShow (Met bUid bSpn) dep), " t=", (termShow a dep)])
+  (termUnify bUid bSpn a dep)
+termIdenticalGo (Hol aNam aCtx) b dep =
+  (envPure True)
+termIdenticalGo a (Hol bNam bCtx) dep =
+  (envPure True)
+termIdenticalGo U60 U60 dep =
+  (envPure True)
+termIdenticalGo (Num aVal) (Num bVal) dep =
+  (envPure (eq aVal bVal))
+termIdenticalGo (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep =
+  (envBind (termIdentical aFst bFst dep) λiFst
+  (envBind (termIdentical aSnd bSnd dep) λiSnd
+  (envPure (and iFst iSnd))))
+termIdenticalGo (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep =
+  (envBind (termIdentical aX bX dep) λiX
+  (envBind (termIdentical aZ bZ dep) λiZ
+  (envBind (termIdentical (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) λiS
+  (envBind (termIdentical (aP (Var aNam dep)) (bP (Var bNam dep)) dep) λiP
+  (envPure (and (and (and iX iZ) iS) iP))))))
+termIdenticalGo (Txt aTxt) (Txt bTxt) dep =
+  (envPure (stringEqual aTxt bTxt))
+termIdenticalGo (Nat aVal) (Nat bVal) dep =
+  (envPure (eq aVal bVal))
+termIdenticalGo (Src aSrc aVal) b dep =
+  (termIdentical aVal b dep)
+termIdenticalGo a (Src bSrc bVal) dep =
+  (termIdentical a bVal dep)
+termIdenticalGo (Ref aNam aVal) (Ref bNam bVal) dep =
+  (envPure (stringEqual aNam bNam))
+termIdenticalGo (Var aNam aIdx) (Var bNam bIdx) dep =
+  (envPure (eq aIdx bIdx))
+termIdenticalGo a b dep =
+  (envPure False)
+
+// Unification
+// -----------
+
+// The unification algorithm is a simple pattern unifier, based on smalltt:
+// > https://github.com/AndrasKovacs/elaboration-zoo/blob/master/03-holes/Main.hs
+// The pattern unification problem provides a solution to the following problem:
+//   (?X x y z ...) = K
+// When:
+//   1. The LHS spine, `x y z ...`, consists of distinct variables.
+//   2. Every free var of the RHS, `K`, occurs in the spine.
+//   3. The LHS hole, `?A`, doesn't occur in the RHS, `K`.
+// If these conditions are met, ?X is solved as:
+//   ?X = λx λy λz ... K
+// In this implementation, checking condition `2` is not necessary, because we
+// subst holes directly where they occur (rather than on top-level definitions),
+// so, it is impossible for unbound variables to appear. We also don't check for
+// condition 3, and just allow recursive solutions.
+
+// If possible, solves a `(?X x y z ...) = K` problem, generating a subst.
+// termUnify :: U60 -> [Term] -> Term -> U60 -> Env Bool
+termUnify uid spn b dep =
+  (envBind envGetFill λfill
+  let unsolved = (not (mapHas (key uid) fill))
+  let solvable = (termUnifyValid fill spn [])
+  (If (and unsolved solvable)
+    let solution = (termUnifySolve fill uid spn b)
+    // (trace (stringJoin ["solve: ", (u60Show uid), " ", (termShow solution dep)])
+    (envBind (envFill uid solution) λ_ 
+      (envPure True))
+    (envPure False)))
+
+// Checks if an problem is solveable by pattern unification.
+// termUnifyValid :: Map Term -> [Term] -> [U60] -> Bool
+termUnifyValid fill []                vars = True
+termUnifyValid fill (List.cons x spn) vars = match (termReduce fill 0 x) {
+  (Var nam idx): (not (and (elem eq idx vars) (termUnifyValid fill spn (List.cons idx vars))))
+  otherwise    : False
+}
+  
+// Generates the solution, adding binders and renaming variables.
+// termUnifySolve :: Map Term -> U60 -> [Term] -> Term -> Term
+termUnifySolve fill uid []                b = b
+termUnifySolve fill uid (List.cons x spn) b = match (termReduce fill 0 x) {
+  (Var nam idx): (Lam nam λx (termUnifySubst idx x (termUnifySolve fill uid spn b)))
+  otherwise    : (trace "unreachable" Unreachable)
+}
+
+// Substitutes a Bruijn level variable by a `neo` value in `term`.
+// termUnifySubst :: U60 -> Term -> Term -> Term
+// termUnifySubst lvl neo term = term
+termUnifySubst lvl neo (All nam inp bod) = (All nam (termUnifySubst lvl neo inp) (λx (termUnifySubst lvl neo (bod x))))
+termUnifySubst lvl neo (Lam nam bod)     = (Lam nam (λx (termUnifySubst lvl neo (bod x))))
+termUnifySubst lvl neo (App fun arg)     = (App (termUnifySubst lvl neo fun) (termUnifySubst lvl neo arg))
+termUnifySubst lvl neo (Ann chk val typ) = (Ann chk (termUnifySubst lvl neo val) (termUnifySubst lvl neo typ))
+termUnifySubst lvl neo (Slf nam typ bod) = (Slf nam (termUnifySubst lvl neo typ) (λx (termUnifySubst lvl neo (bod x))))
+termUnifySubst lvl neo (Ins val)         = (Ins (termUnifySubst lvl neo val))
+termUnifySubst lvl neo (Ref nam val)     = (Ref nam (termUnifySubst lvl neo val))
+termUnifySubst lvl neo (Let nam val bod) = (Let nam (termUnifySubst lvl neo val) (λx (termUnifySubst lvl neo (bod x))))
+termUnifySubst lvl neo (Use nam val bod) = (Use nam (termUnifySubst lvl neo val) (λx (termUnifySubst lvl neo (bod x))))
+termUnifySubst lvl neo (Met uid spn)     = (Met uid (map (termUnifySubst lvl neo) spn))
+termUnifySubst lvl neo (Hol nam ctx)     = (Hol nam (map (termUnifySubst lvl neo) ctx))
+termUnifySubst lvl neo Set               = Set
+termUnifySubst lvl neo U60               = U60
+termUnifySubst lvl neo (Num n)           = (Num n)
+termUnifySubst lvl neo (Op2 opr fst snd) = (Op2 opr (termUnifySubst lvl neo fst) (termUnifySubst lvl neo snd))
+termUnifySubst lvl neo (Swi nam x z s p) = (Swi nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (λk (termUnifySubst lvl neo (s k))) (λk (termUnifySubst lvl neo (p k))))
+termUnifySubst lvl neo (Txt txt)         = (Txt txt)
+termUnifySubst lvl neo (Nat val)         = (Nat val)
+termUnifySubst lvl neo (Var nam idx)     = (if (== lvl idx) neo (Var nam idx))
+termUnifySubst lvl neo (Src src val)     = (Src src (termUnifySubst lvl neo val))
+
+// Type-Checking
+// -------------
+
+// termIfAll :: Term -> (String -> Term -> (Term -> Term) -> a) -> a -> a
+termIfAll (All nam inp bod) yep _   = (yep nam inp bod)
+termIfAll _                 _   nop = nop
+
+// termIfSlf :: Term -> (String -> Term -> (Term -> Term) -> a) -> a -> a
+termIfSlf (Slf nam typ bod) yep _   = (yep nam typ bod)
+termIfSlf _                 _   nop = nop
+
+// termInfer :: Term -> U60 -> Env Term
+termInfer term dep =
+  // trace (stringJoin ["infer: ", (termShow term dep)])
+  (termInferGo term dep)
+
+// termInferGo :: Term -> U60 -> Env Term
+termInferGo (All nam inp bod) dep =
+  (envBind (envSusp (Check 0 inp Set dep)) λ_
+  (envBind (envSusp (Check 0 (bod (Ann False (Var nam dep) inp)) Set (+ dep 1))) λ_
+  (envPure Set)))
+termInferGo (App fun arg) dep =
+  (envBind (termInfer fun dep) λftyp
+  (envBind envGetFill λfill
+  match (termReduce fill 2 ftyp) {
+    (All ftyp_nam ftyp_inp ftyp_bod):
+      (envBind (envSusp (Check 0 arg ftyp_inp dep)) λ_
+      (envPure (ftyp_bod arg)))
+    otherwise:
+      (envBind (envLog (Error 0 (Hol "function" []) ftyp (App fun arg) dep)) λ_
+      envFail)
+  }))
+termInferGo (Ann chk val typ) dep =
+  (envBind (If chk
+    (termCheck 0 val typ dep)
+    (envPure *))  λ_
+  (envPure typ))
+termInferGo (Slf nam typ bod) dep =
+  (envBind (envSusp (Check 0 (bod (Ann False (Var nam dep) typ)) Set (+ dep 1))) λ_
+  (envPure Set))
+termInferGo (Ins val) dep =
+  (envBind (termInfer val dep) λvtyp
+  (envBind envGetFill λfill
+  match (termReduce fill 2 vtyp) {
+    (Slf vtyp_nam vtyp_typ vtyp_bod):
+      (envPure (vtyp_bod (Ins val)))
+    otherwise:
+      (envBind (envLog (Error 0 (Hol "self-type" []) vtyp (Ins val) dep)) λ_
+      envFail)
+  }))
+termInferGo (Ref nam val) dep =
+  (termInfer val dep)
+termInferGo Set dep =
+  (envPure Set)
+termInferGo U60 dep =
+  (envPure Set)
+termInferGo (Num num) dep =
+  (envPure U60)
+termInferGo (Txt txt) dep =
+  (envPure Book.String)
+termInferGo (Nat val) dep =
+  (envPure Book.Nat)
+termInferGo (Op2 opr fst snd) dep =
+  (envBind (envSusp (Check 0 fst U60 dep)) λ_
+  (envBind (envSusp (Check 0 snd U60 dep)) λ_
+  (envPure U60)))
+termInferGo (Swi nam x z s p) dep =
+  (envBind (envSusp (Check 0 x U60 dep)) λ_
+  (envBind (envSusp (Check 0 (p (Ann False (Var nam dep) U60)) Set dep)) λ_
+  (envBind (envSusp (Check 0 z (p (Num 0)) dep)) λ_
+  (envBind (envSusp (Check 0 (s (Ann False (Var (stringConcat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (stringConcat nam "-1") dep))) (+ dep 1))) λ_
+  (envPure (p x))))))
+termInferGo (Let nam val bod) dep =
+  (envBind (termInfer val dep) λtyp
+  (termInfer (bod (Ann False (Var nam dep) typ)) dep))
+termInferGo (Use nam val bod) dep =
+  (termInfer (bod val) dep)
+termInferGo (Lam nam bod) dep =
+  (envBind (envLog (Error 0  (Hol "type_annotation" []) (Hol "untyped_lambda" []) (Lam nam bod) dep)) λ_
+  envFail)
+termInferGo (Hol nam ctx) dep =
+  (envBind (envLog (Error 0  (Hol "type_annotation" []) (Hol "untyped_hole" []) (Hol nam ctx) dep)) λ_
+  envFail)
+termInferGo (Met uid spn) dep =
+  (envBind (envLog (Error 0  (Hol "type_annotation" []) (Hol "untyped_meta" []) (Met uid spn) dep)) λ_
+  envFail)
+termInferGo (Var nam idx) dep =
+  (envBind (envLog (Error 0  (Hol "type_annotation" []) (Hol "untyped_variable" []) (Var nam idx) dep)) λ_
+  envFail)
+termInferGo (Src src val) dep =
+  (termInfer val dep)
+
+// termCheck :: U60 -> Term -> Term -> U60 -> Env *
+termCheck src val typ dep =
+  // (trace (stringJoin ["check: ", (termShow val dep), "\n    :: ", (termShow typ dep)])
+  (termCheckGo src val typ dep)
+
+// termCheckGo :: U60 -> Term -> Term -> U60 -> Env *
+termCheckGo src (Lam termNam termBod) typx dep =
+  (envBind envGetFill λfill
+    match (termReduce fill 2 typx) {
+      (All typeNam typeInp typeBod):
+        let ann  = (Ann False (Var termNam dep) typeInp)
+        let term = (termBod ann)
+        let typx = (typeBod ann)
+        (termCheck 0 term typx (+ dep 1))
+      otherwise:
+        (envBind (termInfer (Lam termNam termBod) dep) λ_
+        (envPure *))
+    })
+termCheckGo src (Ins termVal) typx dep =
+  (envBind envGetFill λfill
+  match (termReduce fill 2 typx) {
+    (Slf typeNam typeTyp typeBod):
+      (termCheck 0 termVal (typeBod (Ins termVal)) dep)
+    _:
+      (envBind (termInfer (Ins termVal) dep) λ_
+      (envPure *))
+  })
+termCheckGo src (Let termNam termVal termBod) typx dep =
+  (envBind (termInfer termVal dep) λtermTyp
+  (termCheck 0 (termBod (Ann False (Var termNam dep) termTyp)) typx dep))
+termCheckGo src (Use termNam termVal termBod) typx dep =
+  (termCheck 0 (termBod termVal) typx dep)
+termCheckGo src (Hol termNam termCtx) typx dep =
+  (envBind (envLog (Found termNam typx termCtx dep)) λ_
+  (envPure *))
+termCheckGo src (Met uid spn) typx dep =
+  (envPure *)
+termCheckGo src (Ann chk val typ) typx dep =
+  (envBind (termCheckCompare src val typ typx dep) λ_
+  (If chk
+    (termCheck src val typ dep)
+    (envPure *)))
+// termCheckGo src (Ref termNam (Ann termVal termTyp)) typx dep =
+  // (envBind (termEqual typx termTyp dep) λequal
+  // (termCheckReport src equal termTyp typx termVal dep)
+termCheckGo src (Src termSrc termVal) typx dep =
+  (termCheck termSrc termVal typx dep)
+termCheckGo src term typx dep =
+  (envBind (termInfer term dep) λinfer
+  (termCheckCompare src term typx infer dep))
+
+termCheckCompare src term expected detected dep =
+  (envBind (termEqual expected detected dep) λequal
+  (If equal
+    (envBind envTakeSusp λsusp
+      (envBind (listCheck susp) λ_
+      (envPure *)))
+    (envBind (envLog (Error src expected detected term dep)) λ_
+    envFail)))
+
+// listCheck :: [a] -> Env *
+listCheck []               = (envPure *)
+listCheck (List.cons x xs) = 
+  let (Check src val typ dep) = x; 
+  (envBind (termCheck src val typ dep) λ_ (listCheck xs))
+    
+// termCheckReport :: U60 -> Bool -> Term -> Term -> Term -> U60 -> Env *
+// termCheckReport src False detected expected value dep =
+  // (envLog (Error src detected expected value dep)
+  // envFail)
+// termCheckReport src True detected expected value dep =
+  // (envPure *)
+
+// termCheckDef :: Term -> Env *
+termCheckDef (Ref nam (Ann chk val typ)) = (envBind (termCheck 0 val typ 0) λ_ (envPure *))
+termCheckDef (Ref nam val)               = (envBind (termInfer val 0)       λ_ (envPure *))
+termCheckDef other                       = (trace "invalid top-level definition" InvalidTopLevelDefinition)
+
+// Stringification
+// ---------------
+
+// termShow :: Term -> U60 -> String
+termShow (All nam inp bod) dep =
+  let nam_ = nam
+  let inp_ = (termShow inp dep)
+  let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
+  (stringJoin ["∀(", nam_, ": ", inp_, ") ", bod_])
+termShow (Lam nam bod) dep =
+  let nam_ = nam
+  let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
+  (stringJoin ["λ", nam_, " ", bod_])
+termShow (App fun arg) dep =
+  let fun_ = (termShow fun dep)
+  let arg_ = (termShow arg dep)
+  (stringJoin ["(", fun_, " ", arg_, ")"])
+termShow (Ann chk val typ) dep =
+  let val_ = (termShow val dep)
+  let typ_ = (termShow typ dep)
+  (stringJoin ["{", val_, ": ", typ_, "}"])
+termShow (Slf nam typ bod) dep =
+  (termShow typ dep)
+termShow (Ins val) dep =
+  let val_ = (termShow val dep)
+  (stringJoin ["~", val_])
+termShow (Ref nam val) dep = nam
+termShow (Let nam val bod) dep =
+  let nam_ = nam
+  let val_ = (termShow val dep)
+  let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
+  (stringJoin ["let ", nam_, " = ", val_, "; ", bod_])
+termShow (Use nam val bod) dep =
+  let nam_ = nam
+  let val_ = (termShow val dep)
+  let bod_ = (termShow (bod (Var nam dep)) (+ dep 1))
+  (stringJoin ["use ", nam_, " = ", val_, "; ", bod_])
+termShow Set dep = "*"
+termShow U60 dep = "#U60"
+termShow (Num val) dep =
+  let val_ = (u60Show val)
+  (stringJoin ["#", val_])
+termShow (Op2 opr fst snd) dep =
+  let opr_ = (operShow opr)
+  let fst_ = (termShow fst dep)
+  let snd_ = (termShow snd dep)
+  (stringJoin ["#(", opr_, " ", fst_, " ", snd_, ")"])
+termShow (Swi nam x z s p) dep =
+  let nam_ = nam
+  let x_   = (termShow x dep)
+  let z_   = (termShow z dep)
+  let s_   = (termShow (s (Var (stringConcat nam "-1") dep)) (+ dep 1))
+  let p_   = (termShow (p (Var nam dep)) dep)
+  (stringJoin ["#match ", nam_, " = ", x_, " { #0: ", z_, " #+: ", s_, " }: ", p_])
+termShow (Txt txt) dep = (stringJoin [quote, txt, quote])
+termShow (Nat val) dep = (u60Show val)
+termShow (Hol nam ctx) dep = (stringJoin ["?", nam])
+termShow (Met uid spn) dep = (stringJoin ["(_", (termShowSpn (reverse spn) dep), ")"])
+termShow (Var nam idx) dep = nam
+// termShow (Var nam idx) dep = stringJoin [nam, "^", (u60Show idx)]
+termShow (Src src val) dep = (termShow val dep)
+// termShow (Src src val) dep = stringJoin ["!", (termShow val dep)]
+
+// termShowSpn :: [Term] -> U60 -> String
+termShowSpn []               dep = ""
+termShowSpn (List.cons x xs) dep = (stringJoin [" ", (termShow x dep), (termShowSpn xs dep)])
+
+// operShow :: Oper -> String
+operShow ADD = "+"
+operShow SUB = "-"
+operShow MUL = "*"
+operShow DIV = "/"
+operShow MOD = "%"
+operShow EQ  = "=="
+operShow NE  = "!="
+operShow LT  = "<"
+operShow GT  = ">"
+operShow LTE = "<="
+operShow GTE = ">="
+operShow AND = "&"
+operShow OR  = "|"
+operShow XOR = "^"
+operShow LSH = "<<"
+operShow RSH = ">>"
+
+// contextShow :: Map Term -> [Term] -> U60 -> String
+contextShow fill []               dep = ""
+contextShow fill (List.cons x xs) dep = (stringJoin [" ", (contextShowAnn fill x dep), (contextShow fill xs dep)])
+
+// contextShowAnn :: Map Term -> Term -> U60 -> String
+contextShowAnn fill (Ann chk val typ) dep = (stringJoin ["{", (termShow (termNormal fill 0 val dep) dep), ": ", (termShow (termNormal fill 0 typ dep) dep), "}"])
+contextShowAnn fill term              dep = (termShow (termNormal fill 0 term dep) dep)
+
+// infoShow :: Map Term -> Info -> String
+infoShow fill (Found name typ ctx dep) =
+  let typ_ = (termShow (termNormal fill 1 typ dep) dep)
+  let ctx_ = (stringTail (contextShow fill ctx dep))
+  (stringJoin ["#found{", name, " ", typ_, " [", ctx_, "]}"])
+infoShow fill (Error src expected detected value dep) =
+  let exp = (termShow (termNormal fill 1 expected dep) dep)
+  let det = (termShow (termNormal fill 1 detected dep) dep)
+  let val = (termShow (termNormal fill 0 value dep) dep)
+  (stringJoin ["#error{", exp, " ", det, " ", val, " ", (u60Show src), "}"])
+infoShow fill (Solve name term dep) =
+  let term_ = (termShow (termNormal fill 1 term dep) dep)
+  (stringJoin ["#solve{", name, " ",  term_, "}"])
+infoShow fill (Vague name) =
+  (stringJoin ["#vague{", name, "}"])
+infoShow fill (Print value dep) =
+  let val = (termShow (termNormal fill 0 value dep) dep)
+  (stringJoin ["#print{", val, "}"])
+
+// API
+// ---
+
+// Normalizes a term
+// apiNormal :: Term -> IO *
+apiNormal term = (putStrLn (infoShow mapNew (Print (termNormal mapNew 2 term 0) 0)) *)
+
+// apiCheck :: Term -> IO *
+apiCheck term = match (envRun (termCheckDef term)) {
+  (Done state value): (apiPrintLogs state)
+  (Fail state)      : (apiPrintLogs state)
+}
+
+// apiPrintLogs :: State -> IO *
+apiPrintLogs (State fill susp (List.cons log logs)) =
+  (putStrLn (infoShow fill log)
+  (apiPrintLogs (State fill susp logs)))
+apiPrintLogs (State fill susp []) =
+  *
+
+putStrLn = HVM.print
+trace = HVM.print
--- a/src/main.rs
+++ b/src/main.rs
@ -34,6 +34,18 @@ fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
  return hvm1_code;
 }

+fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
+  let kind_hvm2 = include_str!("./kind2.hvm2");
+  let book_hvm2 = book.to_hvm2_checker();
+  let main_hvm2 = match command {
+    "check" => format!("main = (apiCheck Book.{})\n", arg),
+    "run"   => format!("main = (apiNormal Book.{})\n", arg),
+    _       => panic!("invalid command"),
+  };
+  let hvm2_code = format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2);
+  return hvm2_code;
+}
+
 fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String {
  let kind_hs = include_str!("./kind2.hs");
  let kind_hs = kind_hs.lines().filter(|line| !line.starts_with("xString")).collect::<Vec<_>>().join("\n");
@ -54,57 +66,79 @@ fn generate_hvm2(book: &Book, _command: &str, arg: &str) -> String {
  return code_hvm2;
 }

+pub fn get_infos(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info>, String) {
+  // Auto-formats the definition.
+  // let defn = book.defs.get(file).unwrap();
+  // let form = book.format_def(file, defn).flatten(60);
+
+  // Overwrites the original file with the formatted version.
+  // File::create(&format!("./{}.kind2", file))
+  //   .and_then(|mut file| file.write_all(form.as_bytes()))
+  //   .unwrap_or_else(|_| panic!("Failed to auto-format '{}.kind2'.", file));
+
+  let command = match runtime {
+    "--ghc" => {
+      // Generates the Haskell checker.
+      let check_hs = generate_check_hs(&book, cmd, file);
+      let mut file = File::create(".check.hs").expect("Failed to create '.check.hs'.");
+      file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
+
+      // Calls GHC and get outputs.
+      Command::new("runghc").arg(".check.hs").output().expect("Failed to execute command")
+    }
+    "--hvm1" => {
+      // Generates the HVM1 checker.
+      let check_hvm1 = generate_check_hvm1(&book, cmd, 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'.");
+
+      // Calls HVM1 and get outputs.
+      Command::new("hvm1").arg("run").arg("-t").arg("1").arg("-c").arg("-f").arg(".check.hvm1").arg("(Main)").output().expect("Failed to execute command")
+    }
+    "--hvm2" => {
+      // Generates the hvm2 checker.
+      let check_hs = generate_check_hvm2(&book, cmd, file);
+      let mut file = File::create(".check.hvm2").expect("Failed to create '.check.hs'.");
+      file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
+
+      // Calls HVMl and get outputs.
+      Command::new("hvml").arg("run").arg("-L").arg(".check.hvm2").output().expect("Failed to execute command")
+    }
+    _ => panic!("invalid command"),
+  };
+  
+  let stdout = String::from_utf8_lossy(&command.stdout);
+  let stderr = String::from_utf8_lossy(&command.stderr);
+
+  (Info::parse_infos(&stdout), stderr.to_string())
+}
+
 fn main() {
  let args: Vec<String> = env::args().collect();

-  if args.len() < 3 {
+  if args.len() < 2 {
    show_help();
  }

  let cmd = &args[1];
-  let arg = &args[2];

  //println!("loading");
  match cmd.as_str() {
    "check" | "run" => {
-      match Book::boot(arg) {
+      if args.len() < 3 {
+        show_help();
+      }
+      let arg = &args[2];
+      let opt = &args.get(3).map(|x| x.as_str()).unwrap_or("--ghc");
+      match Book::boot(".", arg) {
        Ok(book) => {
-          // Auto-formats the definition.
-          //let defn = book.defs.get(arg).unwrap();
-          //let form = book.format_def(arg, defn).flatten(60);
+          let (infos, stderr) = get_infos(&book, cmd, arg, opt);

-          // Overwrites the original file with the formatted version.
-          //File::create(&format!("./{}.kind2", arg))
-            //.and_then(|mut file| file.write_all(form.as_bytes()))
-            //.unwrap_or_else(|_| panic!("Failed to auto-format '{}.kind2'.", arg));
-
-          // Generates the HVM1 checker.
-          //let check_hvm1 = generate_check_hvm1(&book, cmd, arg);
-          //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'.");
-
-          // Calls HVM1 and get outputs.
-          // FIXME: re-enable HVM version
-          //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 = String::from_utf8_lossy(&output.stdout);
-          //let stderr = String::from_utf8_lossy(&output.stderr);
-          
-          // Generates the Haskell checker.
-          let check_hs = generate_check_hs(&book, cmd, arg);
-          let mut file = File::create(".check.hs").expect("Failed to create '.check.hs'.");
-          file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
-
-          // Calls GHC and get outputs.
-          let output = Command::new("runghc").arg(".check.hs").output().expect("Failed to execute command");
-          let stdout = String::from_utf8_lossy(&output.stdout);
-          let stderr = String::from_utf8_lossy(&output.stderr);
-
-          // Parses and print stdout infos.
-          let infos = Info::parse_infos(&stdout);
          for info in &infos {
            println!("{}", info.pretty(&book))
          }
-          if infos.len() == 0 {
+
+          if stderr.is_empty() && infos.len() == 0 {
            println!("check!");
          }

@ -117,6 +151,9 @@ fn main() {
        },
      }
    },
+    "compare" => {
+      test_runtime_compatibility();
+    }
    _ => {
      show_help();
    },
@ -131,5 +168,36 @@ fn main() {

 fn show_help() {
  eprintln!("Usage: kind2 [check|run] <name>");
+  eprintln!("       kind2 compare");
  std::process::exit(1);
 }
+
+fn test_runtime_compatibility() {
+  use std::fs;
+
+  let q = env!("CARGO_MANIFEST_DIR").to_owned() + "/book/";
+  let paths = fs::read_dir(&q).unwrap();
+  let mut paths: Vec<_> = paths.into_iter().map(|path| path.unwrap().path()).collect();
+  paths.sort();
+  for path in paths {
+    let base = path.file_stem().unwrap().to_str().unwrap();
+    let Ok(book) = Book::boot(&q, base) else {
+      continue;
+    };
+    print!("{:<30}: ", base);
+    for rt in ["--ghc", "--hvm2"] {
+      let _ = std::io::stdout().flush();
+      let (infos, stderr) = get_infos(&book, "check", base, rt);
+      if stderr.is_empty() {
+        if infos.len() == 0 {
+          print!("\x1b[32;1m+\x1b[0m ");
+        } else {
+          print!("\x1b[31;1m-\x1b[0m ");
+        }
+      } else {
+        print!("\x1b[33;1m*\x1b[0m");
+      }
+    }
+    println!();
+  }
+}
--- a/src/sugar/mod.rs
+++ b/src/sugar/mod.rs
@ -662,7 +662,7 @@ impl ADT {
  
  // Loads an ADT from its λ-encoded file.
  pub fn load(name: &str) -> Result<ADT, String> {
-    let book = Book::boot(name)?;
+    let book = Book::boot(".", name)?;
    if let Some(term) = book.defs.get(name) {
      let mut term = term.clone();
      // Skips Anns, Lams, Srcs
--- a/src/term/compile.rs
+++ b/src/term/compile.rs
@ -48,6 +48,10 @@ impl Oper {
    self.to_ctr()
  }

+  pub fn to_hvm2_checker(&self) -> &'static str {
+    self.to_ctr()
+  }
+
  pub fn to_hs_checker(&self) -> &'static str {
    self.to_ctr()
  }
@ -59,7 +63,99 @@ impl Term {
  pub fn to_hvm1_checker(&self, _env: im::Vector<String>, _met: &mut usize) -> String {
    todo!()
  }
-  
+
+  pub fn to_hvm2_checker(&self, env: im::Vector<String>, met: &mut usize) -> String {
+    fn binder(name: &str) -> String {
+      format!("x{}", name.replace("-", "._."))
+    }
+    match self {
+      Term::All { nam, inp, bod } => {
+        let inp = inp.to_hvm2_checker(env.clone(), met);
+        let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(All \"{}\" {} λ{} {})", nam, inp, binder(nam), bod)
+      }
+      Term::Lam { nam, bod } => {
+        let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod)
+      }
+      Term::App { fun, arg } => {
+        let fun = fun.to_hvm2_checker(env.clone(), met);
+        let arg = arg.to_hvm2_checker(env.clone(), met);
+        format!("(App {} {})", fun, arg)
+      }
+      Term::Ann { chk, val, typ } => {
+        let val = val.to_hvm2_checker(env.clone(), met);
+        let typ = typ.to_hvm2_checker(env.clone(), met);
+        format!("(Ann {} {} {})", if *chk { "True" } else { "False" }, val, typ)
+      }
+      Term::Slf { nam, typ, bod } => {
+        let typ = typ.to_hvm2_checker(env.clone(), met);
+        let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(Slf \"{}\" {} λ{} {})", nam, typ, binder(nam), bod)
+      }
+      Term::Ins { val } => {
+        let val = val.to_hvm2_checker(env.clone(), met);
+        format!("(Ins {})", val)
+      }
+      Term::Set => "(Set)".to_string(),
+      Term::U60 => "(U60)".to_string(),
+      Term::Num { val } => {
+        format!("(Num {})", val)
+      }
+      Term::Op2 { opr, fst, snd } => {
+        let fst = fst.to_hvm2_checker(env.clone(), met);
+        let snd = snd.to_hvm2_checker(env.clone(), met);
+        format!("(Op2 {} {} {})", opr.to_hvm2_checker(), fst, snd)
+      }
+      Term::Swi { nam, x, z, s, p } => {
+        let x = x.to_hvm2_checker(env.clone(), met);
+        let z = z.to_hvm2_checker(env.clone(), met);
+        let s = s.to_hvm2_checker(cons(&env, format!("{}-1", nam)), met);
+        let p = p.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(Swi \"{}\" {} {} λ{} {} λ{} {})", nam, x, z, binder(&format!("{}-1", nam)), s, binder(nam), p)
+      }
+      Term::Let { nam, val, bod } => {
+        let val = val.to_hvm2_checker(env.clone(), met);
+        let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(Let \"{}\" {} λ{} {})", nam, val, binder(nam), bod)
+      }
+      Term::Use { nam, val, bod } => {
+        let val = val.to_hvm2_checker(env.clone(), met);
+        let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met);
+        format!("(Use \"{}\" {} λ{} {})", nam, val, binder(nam), bod)
+      }
+      Term::Hol { nam } => {
+        let env_str = env.iter().map(|n| binder(n)).collect::<Vec<_>>().join(",");
+        format!("(Hol \"{}\" [{}])", nam, env_str)
+      }
+      Term::Met {} => {
+        let uid = *met;
+        *met += 1;
+        format!("(Met {} [])", uid)
+      }
+      Term::Var { nam } => {
+        if env.contains(nam) {
+          format!("{}", binder(nam))
+        } else {
+          format!("(Book.{})", nam)
+        }
+      }
+      Term::Src { src, val } => {
+        let val = val.to_hvm2_checker(env, met);
+        format!("(Src {} {})", src.to_u64(), val)
+      }
+      Term::Nat { nat } => {
+        format!("(Nat {})", nat)
+      }
+      Term::Txt { txt } => {
+        format!("(Txt \"{}\")", txt.replace("\n", "\\n"))
+      }
+      Term::Mch { .. } => {
+        unreachable!()
+      }
+    }
+  }
+
  pub fn to_hs_name(name: &str) -> String {
    format!("x{}", name.replace("-", "_").replace(".","_"))
  }