diff --git a/Cargo.lock b/Cargo.lock
index 9a7b15865..e3af9f8c0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -11,6 +11,54 @@ dependencies = [
  "highlight_error",
 ]
 
+[[package]]
+name = "anstream"
+version = "0.6.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb"
+dependencies = [
+ "anstyle",
+ "anstyle-parse",
+ "anstyle-query",
+ "anstyle-wincon",
+ "colorchoice",
+ "utf8parse",
+]
+
+[[package]]
+name = "anstyle"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc"
+
+[[package]]
+name = "anstyle-parse"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c"
+dependencies = [
+ "utf8parse",
+]
+
+[[package]]
+name = "anstyle-query"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648"
+dependencies = [
+ "windows-sys",
+]
+
+[[package]]
+name = "anstyle-wincon"
+version = "3.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7"
+dependencies = [
+ "anstyle",
+ "windows-sys",
+]
+
 [[package]]
 name = "bitmaps"
 version = "2.1.0"
@@ -20,6 +68,39 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "clap"
+version = "4.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b230ab84b0ffdf890d5a10abdbc8b83ae1c4918275daea1ab8801f71536b2651"
+dependencies = [
+ "clap_builder",
+]
+
+[[package]]
+name = "clap_builder"
+version = "4.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4"
+dependencies = [
+ "anstream",
+ "anstyle",
+ "clap_lex",
+ "strsim",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce"
+
+[[package]]
+name = "colorchoice"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
+
 [[package]]
 name = "highlight_error"
 version = "0.1.1"
@@ -45,6 +126,7 @@ name = "kind2"
 version = "0.1.0"
 dependencies = [
  "TSPL",
+ "clap",
  "highlight_error",
  "im",
 ]
@@ -74,14 +156,92 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "strsim"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"
+
 [[package]]
 name = "typenum"
 version = "1.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
 
+[[package]]
+name = "utf8parse"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
+
 [[package]]
 name = "version_check"
 version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
+
+[[package]]
+name = "windows-sys"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b"
+dependencies = [
+ "windows_aarch64_gnullvm",
+ "windows_aarch64_msvc",
+ "windows_i686_gnu",
+ "windows_i686_msvc",
+ "windows_x86_64_gnu",
+ "windows_x86_64_gnullvm",
+ "windows_x86_64_msvc",
+]
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
diff --git a/Cargo.toml b/Cargo.toml
index 428aa7cf1..a1342c79f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -11,3 +11,4 @@ path = "src/main.rs"
 TSPL = "0.0.8"
 highlight_error = "0.1.1"
 im = "15.1.0"
+clap = "4.5.2"
diff --git a/src/book/compile.rs b/src/book/compile.rs
index 70c8ca163..b7447e951 100644
--- a/src/book/compile.rs
+++ b/src/book/compile.rs
@@ -1,8 +1,5 @@
 use crate::{*};
 
-use std::collections::BTreeMap;
-use std::collections::BTreeSet;
-
 impl Book {
 
   pub fn to_hvm1_checker(&self) -> String {
diff --git a/src/book/parse.rs b/src/book/parse.rs
index e2a144954..d9bfb2084 100644
--- a/src/book/parse.rs
+++ b/src/book/parse.rs
@@ -1,8 +1,5 @@
 use crate::{*};
 
-use std::collections::BTreeMap;
-use std::collections::BTreeSet;
-
 impl<'i> KindParser<'i> {
 
   // Parses a top-level use-declaration
diff --git a/src/main.rs b/src/main.rs
index 549e436cc..b3effcc5f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,5 +1,8 @@
-#![allow(dead_code)]
-#![allow(unused_imports)]
+use clap::{Arg, ArgAction, Command};
+use std::fs;
+use std::io::Write;
+use std::path::PathBuf;
+use std::process::Command as SysCommand;
 
 mod book;
 mod info;
@@ -7,33 +10,17 @@ mod show;
 mod sugar;
 mod term;
 
-use book::{*};
-use info::{*};
-use show::{*};
-use sugar::{*};
-use term::{*};
+use book::*;
+use info::*;
+use show::*;
+use sugar::*;
+use term::*;
 
-use TSPL::Parser;
 use highlight_error::highlight_error;
-use std::env;
-use std::fs::File;
-use std::io::Write;
-use std::process::Command;
+use TSPL::Parser;
 
 TSPL::new_parser!(KindParser);
 
-fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
-  let kind_hvm1 = include_str!("./kind2.hvm1");
-  let book_hvm1 = book.to_hvm1_checker();
-  let main_hvm1 = match command {
-    "check" => format!("Main = (API.check Book.{})\n", arg),
-    "run"   => format!("Main = (API.normal Book.{})\n", arg),
-    _       => panic!("invalid command"),
-  };
-  let hvm1_code = format!("{}\n{}\n{}", kind_hvm1, book_hvm1, main_hvm1);
-  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();
@@ -42,162 +29,191 @@ fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
     "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;
+  format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2)
 }
 
 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");
+  let kind_hs = include_str!("./kind2.hs")
+    .lines()
+    .filter(|line| !line.starts_with("xString"))
+    .collect::<Vec<_>>()
+    .join("\n");
   let book_hs = book.to_hs_checker();
   let main_hs = match command {
     "check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
     "run"   => format!("main = (apiNormal {})\n", Term::to_hs_name(arg)),
     _       => panic!("invalid command"),
   };
-  let hs_code = format!("{}\n{}\n{}", kind_hs, book_hs, main_hs);
-  return hs_code;
+  format!("{}\n{}\n{}", kind_hs, book_hs, main_hs)
 }
 
-fn generate_hvm2(book: &Book, _command: &str, arg: &str) -> String {
+fn generate_hvm2(book: &Book, arg: &str) -> String {
   let book_hvm2 = book.to_hvm2();
   let main_hvm2 = format!("main = {}\n", arg);
-  let code_hvm2 = format!("{}\n{}", book_hvm2, main_hvm2);
-  return code_hvm2;
+  format!("{}\n{}", book_hvm2, main_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));
-
+fn run_kore(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info>, String) {
   let command = match runtime {
-    "--ghc" => {
-      // Generates the Haskell checker.
+    "hs" => {
       let check_hs = generate_check_hs(&book, cmd, file);
-      let mut file = File::create(".check.hs").expect("Failed to create '.check.hs'.");
+      let mut file = fs::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")
+      SysCommand::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" => {
+      let check_hvm2 = generate_check_hvm2(&book, cmd, file);
+      let mut file = fs::File::create(".check.hvm2").expect("Failed to create '.check.hvm2'.");
+      file.write_all(check_hvm2.as_bytes()).expect("Failed to write '.check.hvm2'.");
+      SysCommand::new("hvml").arg("run").arg("-L").arg(".check.hvm2").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"),
+    _ => panic!("invalid runtime"),
   };
-  
+
   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();
+fn check(name: &str, runtime: &str) {
+  let book = load_book(name);
+  let (infos, stderr) = run_kore(&book, "check", name, runtime);
 
-  if args.len() < 2 {
-    show_help();
+  for info in &infos {
+    println!("{}", info.pretty(&book));
   }
 
-  let cmd = &args[1];
-
-  //println!("loading");
-  match cmd.as_str() {
-    "check" | "run" => {
-      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) => {
-          let (infos, stderr) = get_infos(&book, cmd, arg, opt);
-
-          for info in &infos {
-            println!("{}", info.pretty(&book))
-          }
-
-          if stderr.is_empty() && infos.len() == 0 {
-            println!("check!");
-          }
-
-          // Prints stdout errors and stats.
-          eprintln!("{}", stderr);
-        },
-        Err(e) => {
-          eprintln!("{}", e);
-          std::process::exit(1);
-        },
-      }
-    },
-    "compare" => {
-      test_runtime_compatibility();
-    }
-    _ => {
-      show_help();
-    },
+  if stderr.is_empty() && infos.is_empty() {
+    println!("check!");
   }
+
+  eprintln!("{stderr}");
 }
 
-//fn main() {
-  //env::set_current_dir("./book").expect("Failed to change directory to ./book");
-  //let adt = term::sugar::adt::ADT::load("Vector");
-  //println!("{:?}", adt);
-//}
+fn normal(name: &str, _level: u32, runtime: &str) {
+  let book = load_book(name);
+  let (infos, stderr) = run_kore(&book, "run", name, runtime);
 
-fn show_help() {
-  eprintln!("Usage: kind2 [check|run] <name>");
-  eprintln!("       kind2 compare");
-  std::process::exit(1);
+  for info in &infos {
+    println!("{}", info.pretty(&book));
+  }
+
+  eprintln!("{stderr}");
 }
 
-fn test_runtime_compatibility() {
-  use std::fs;
+fn format_def(name: &str) {
+  let book = load_book(name);
+  let defn = book.defs.get(name).expect("definition exists");
+  let form = book.format_def(name, defn).flatten(Some(40));
 
-  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();
+  let path = PathBuf::from(format!("./{name}.kind2"));
+  fs::write(&path, form).expect(&format!("failed to write to '{:?}'", path));
+}
+
+fn compile(name: &str) {
+  let book = load_book(name);
+  let code = generate_hvm2(&book, name);
+  println!("{code}");
+}
+
+fn compare_runtimes() {
+  let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
+  let mut paths: Vec<_> = fs::read_dir(&book_dir)
+    .expect("failed to read book directory")
+    .map(|r| r.expect("failed to read entry").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 {
+    let name = path.file_stem().unwrap().to_str().unwrap();
+
+    let Some(book) = Book::boot(book_dir.to_str().unwrap(), name).ok() else {
       continue;
     };
-    print!("{:<30}: ", base);
-    for rt in ["--ghc", "--hvm2"] {
-      let _ = std::io::stdout().flush();
-      let (infos, stderr) = get_infos(&book, "check", base, rt);
+
+    print!("{name:<30}: ");
+
+    for rt in ["hs", "hvm2"] {
+      std::io::stdout().flush().expect("failed to flush stdout");
+      let (infos, stderr) = run_kore(&book, "check", name, rt);
       if stderr.is_empty() {
-        if infos.len() == 0 {
+        if infos.is_empty() {
           print!("\x1b[32;1m+\x1b[0m ");
         } else {
           print!("\x1b[31;1m-\x1b[0m ");
         }
       } else {
-        print!("\x1b[33;1m*\x1b[0m");
+        print!("\x1b[33;1m*\x1b[0m ");
       }
     }
+
     println!();
   }
 }
+
+fn load_book(name: &str) -> Book {
+  let cwd = std::env::current_dir().expect("failed to get current directory");
+  Book::boot(cwd.to_str().unwrap(), name).unwrap_or_else(|e| {
+    eprintln!("{e}");
+    std::process::exit(1);
+  })
+}
+
+fn main() {
+  let matches = Command::new("kind2")
+    .about("The Kind2 Programming Language")
+    .subcommand_required(true)
+    .arg_required_else_help(true)
+    .subcommand(Command::new("check")
+      .about("Type-checks a term")
+      .arg(Arg::new("name").required(true))
+      .arg(Arg::new("runtime")
+        .long("use")
+        .value_parser(["hs", "hvm2"])
+        .default_value("hs")))
+    .subcommand(Command::new("normal")  
+      .about("Normalizes a term")
+      .arg(Arg::new("name").required(true))
+      .arg(Arg::new("level")
+        .long("level")
+        .short('l')
+        .action(ArgAction::Set)
+        .value_parser(clap::value_parser!(u32)))
+      .arg(Arg::new("runtime")
+        .long("use")
+        .value_parser(["hs", "hvm2"])
+        .default_value("hs")))
+    .subcommand(Command::new("format")
+      .about("Pretty-formats a definition")
+      .arg(Arg::new("name").required(true)))
+    .subcommand(Command::new("compile")
+      .about("Compiles to HVM2")  
+      .arg(Arg::new("name").required(true)))
+    .subcommand(Command::new("compare").about("Runs internal comparison tests"))
+    .get_matches();
+
+  match matches.subcommand() {
+    Some(("check", sub_matches)) => {
+      let name = sub_matches.get_one::<String>("name").expect("required");
+      let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
+      check(name, runtime);
+    }
+    Some(("normal", sub_matches)) => {
+      let name = sub_matches.get_one::<String>("name").expect("required");
+      let level = sub_matches.get_one::<u32>("level").copied().unwrap_or(0);
+      let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
+      normal(name, level, runtime);
+    }
+    Some(("format", sub_matches)) => {
+      let name = sub_matches.get_one::<String>("name").expect("required");
+      format_def(name);
+    }
+    Some(("compile", sub_matches)) => {
+      let name = sub_matches.get_one::<String>("name").expect("required");
+      compile(name);
+    }
+    Some(("compare", _)) => compare_runtimes(),
+    _ => unreachable!(),
+  }
+}
diff --git a/src/show/mod.rs b/src/show/mod.rs
index 45ddf7e3b..19b062d55 100644
--- a/src/show/mod.rs
+++ b/src/show/mod.rs
@@ -1,5 +1,3 @@
-use crate::Term;
-
 // Example:
 //   ["(" "foo" "arg0" "arg1" "arg2" ")"]
 // Call:
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 2a95f2b71..2d00fca0b 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -81,7 +81,7 @@ impl Src {
   }
 }
 
-fn name(numb: usize) -> String {
+fn _name(numb: usize) -> String {
   let mut name = String::new();
   let mut numb = numb as i64;
   loop {