commit 469eb5976d64aed0c0b0f7efe7902a4fbd5ea1d2
Author: Victor Maia <victor.taelin@gmail.com>
Date:   Tue Jul 12 22:47:17 2022 -0300

    Initial commit

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..ea8c4bf7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/target
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 00000000..26f0514d
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,307 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "aho-corasick"
+version = "0.7.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "atty"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
+dependencies = [
+ "hermit-abi",
+ "libc",
+ "winapi",
+]
+
+[[package]]
+name = "autocfg"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
+
+[[package]]
+name = "bitflags"
+version = "1.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
+
+[[package]]
+name = "clap"
+version = "3.2.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "69c5a7f9997be616e47f0577ee38c91decb33392c5be4866494f34cdf329a9aa"
+dependencies = [
+ "atty",
+ "bitflags",
+ "clap_derive",
+ "clap_lex",
+ "indexmap",
+ "once_cell",
+ "strsim",
+ "termcolor",
+ "textwrap",
+]
+
+[[package]]
+name = "clap_derive"
+version = "3.2.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "759bf187376e1afa7b85b959e6a664a3e7a95203415dba952ad19139e798f902"
+dependencies = [
+ "heck",
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2850f2f5a82cbf437dd5af4d49848fbdfc27c157c3d010345776f952765261c5"
+dependencies = [
+ "os_str_bytes",
+]
+
+[[package]]
+name = "either"
+version = "1.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f107b87b6afc2a64fd13cac55fe06d6c8859f12d4b14cbcdd2c67d0976781be"
+
+[[package]]
+name = "hashbrown"
+version = "0.12.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "607c8a29735385251a339424dd462993c0fed8fa09d378f259377df08c126022"
+
+[[package]]
+name = "heck"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9"
+
+[[package]]
+name = "hermit-abi"
+version = "0.1.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "hvm"
+version = "0.1.31"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "361a02d7ed07086c16927712c1bf610e54c3a43bd5d78deab7708f56c33ee5fb"
+dependencies = [
+ "clap",
+ "itertools",
+ "num_cpus",
+ "regex",
+]
+
+[[package]]
+name = "indexmap"
+version = "1.9.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "10a35a97730320ffe8e2d410b5d3b69279b98d2c14bdb8b70ea89ecf7888d41e"
+dependencies = [
+ "autocfg",
+ "hashbrown",
+]
+
+[[package]]
+name = "itertools"
+version = "0.10.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a9a9d19fa1e79b6215ff29b9d6880b706147f16e9b1dbb1e4e5947b5b02bc5e3"
+dependencies = [
+ "either",
+]
+
+[[package]]
+name = "kind2-rs"
+version = "0.1.0"
+dependencies = [
+ "hvm",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.126"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "349d5a591cd28b49e1d1037471617a32ddcda5731b99419008085f72d5a53836"
+
+[[package]]
+name = "memchr"
+version = "2.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
+
+[[package]]
+name = "num_cpus"
+version = "1.13.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
+dependencies = [
+ "hermit-abi",
+ "libc",
+]
+
+[[package]]
+name = "once_cell"
+version = "1.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "18a6dbe30758c9f83eb00cbea4ac95966305f5a7772f3f42ebfc7fc7eddbd8e1"
+
+[[package]]
+name = "os_str_bytes"
+version = "6.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "21326818e99cfe6ce1e524c2a805c189a99b5ae555a35d19f9a284b427d86afa"
+
+[[package]]
+name = "proc-macro-error"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+dependencies = [
+ "proc-macro-error-attr",
+ "proc-macro2",
+ "quote",
+ "syn",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro-error-attr"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.40"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd96a1e8ed2596c337f8eae5f24924ec83f5ad5ab21ea8e455d3566c69fbcaf7"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.20"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3bcdf212e9776fbcb2d23ab029360416bb1706b1aea2d1a5ba002727cbcab804"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "regex"
+version = "1.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.6.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244"
+
+[[package]]
+name = "strsim"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
+
+[[package]]
+name = "syn"
+version = "1.0.98"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c50aef8a904de4c23c788f104b7dddc7d6f79c647c7c8ce4cc8f73eb0ca773dd"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "termcolor"
+version = "1.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
+name = "textwrap"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b1141d4d61095b28419e22cb0bbf02755f5e54e0526f97f1e3d1d160e60885fb"
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5bd2fe26506023ed7b5e1e315add59d6f584c621d037f9368fea9cfb988f368c"
+
+[[package]]
+name = "version_check"
+version = "0.9.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
+
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-util"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178"
+dependencies = [
+ "winapi",
+]
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 00000000..4f5f2cf4
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,9 @@
+[package]
+name = "kind2-rs"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hvm = "0.1.31"
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 00000000..70eaa273
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,417 @@
+#![allow(dead_code)] 
+#![allow(unused_variables)] 
+
+// imports hashmap
+use std::collections::HashMap;
+
+//  type Bool {
+//    {True}
+//    {False}
+//  }
+//
+//  type List <T: Type> {
+//    {Nil}
+//    {Cons T (List <T>)}
+//  }
+//    
+//  type Equal <T: Type> (a: T) ~ (b: T) {
+//    {Refl} ~ (b = a)
+//  }
+//
+//  Add (a: Nat) (b: Nat) : Nat {
+//    {Zero}   b => b
+//    {Succ a} b => {Succ (Add a b)}
+//  }
+//
+//  Add (a: Nat) (b: Nat) : Nat =
+//    match a {
+//      {Zero}   => b
+//      {Succ a} => {Succ (Add a b)}
+//    }
+//
+//   Map <A: Type> <B: Type> (f: A -> B) (xs: List A) : List B {
+//     A B f {Cons x xs} => {Cons (f x) (map A B f xs)}
+//     A B f {Nil}       => {Nil}
+//   }
+//
+//   Main : (List Nat) =
+//     let x = 50
+//     let y = 60
+//     if (== x y) {
+//       (print "hi")
+//     } else {
+//       (print "bye")
+//     }
+//
+//   alice : Person =
+//     {Person
+//       age: 40
+//       name: "Alice"
+//       items: ["Foo", "Bar", "Tic", "Tac"]
+//     }
+//   
+//   {Cons x xs}
+//   {Cons head: x tail: xs }
+
+use hvm::parser as parser;
+
+#[derive(Clone, Debug)]
+pub enum Term {
+  Typ,
+  Var { name: String },
+  Let { name: String, expr: Box<Term>, body: Box<Term> },
+  App { func: Box<Term>, argm: Box<Term> },
+  Lam { name: String, body: Box<Term> },
+  All { name: String, tipo: Box<Term>, body: Box<Term> },
+  Ctr { name: String, args: Vec<Box<Term>> },
+  Fun { name: String, args: Vec<Box<Term>> },
+}
+
+#[derive(Clone, Debug)]
+pub struct Argument {
+  eras: bool,
+  name: String,
+  tipo: Box<Term>,
+}
+
+#[derive(Clone, Debug)]
+pub struct Rule {
+  pats: Vec<Box<Term>>,
+  body: Box<Term>,
+}
+
+#[derive(Clone, Debug)]
+pub struct Entry {
+  name: String,
+  args: Vec<Box<Argument>>,
+  tipo: Box<Term>,
+  rules: Vec<Box<Rule>>
+}
+
+#[derive(Clone, Debug)]
+pub struct File {
+  entries: HashMap<String, Box<Entry>>
+}
+
+pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  parser::guard(
+    Box::new(|state| {
+      let (state, head) = parser::get_char(state)?;
+      Ok((state, ('a'..='z').contains(&head) || head == '_' || head == '$'))
+    }),
+    Box::new(|state| {
+      let (state, name) = parser::name(state)?;
+      Ok((state, Box::new(Term::Var { name })))
+    }),
+    state,
+  )
+}
+
+pub fn parse_lam(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  parser::guard(
+    parser::text_parser("@"),
+    Box::new(move |state| {
+      let (state, _)    = parser::consume("@", state)?;
+      let (state, name) = parser::name(state)?;
+      let (state, body) = parse_term(state)?;
+      Ok((state, Box::new(Term::Lam { name, body })))
+    }),
+    state,
+  )
+}
+
+pub fn parse_all(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  parser::guard(
+    Box::new(|state| {
+      let (state, all0) = parser::text("(", state)?;
+      let (state, name) = parser::name(state)?;
+      let (state, all1) = parser::text(":", state)?;
+      Ok((state, all0 && all1 && name.len() > 0))
+    }),
+    Box::new(|state| {
+      let (state, _)    = parser::consume("(", state)?;
+      let (state, name) = parser::name(state)?;
+      let (state, _)    = parser::consume(":", state)?;
+      let (state, tipo) = parse_term(state)?;
+      let (state, _)    = parser::consume(")", state)?;
+      let (state, body) = parse_term(state)?;
+      Ok((state, Box::new(Term::All { name, tipo, body })))
+    }),
+    state,
+  )
+}
+
+pub fn parse_app(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  return parser::guard(
+    parser::text_parser("("),
+    Box::new(|state| {
+      parser::list(
+        parser::text_parser("("),
+        parser::text_parser(""),
+        parser::text_parser(")"),
+        Box::new(parse_term),
+        Box::new(|args| {
+          if !args.is_empty() {
+            args.into_iter().reduce(|a, b| Box::new(Term::App { func: a, argm: b })).unwrap()
+          } else {
+            Box::new(Term::Var { name: "?".to_string() })
+          }
+        }),
+        state,
+      )
+    }),
+    state,
+  );
+}
+
+pub fn parse_let(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  return parser::guard(
+    parser::text_parser("let "),
+    Box::new(|state| {
+      let (state, _)    = parser::consume("let ", state)?;
+      let (state, name) = parser::name1(state)?;
+      let (state, _)    = parser::consume("=", state)?;
+      let (state, expr) = parse_term(state)?;
+      let (state, _)    = parser::text(";", state)?;
+      let (state, body) = parse_term(state)?;
+      Ok((state, Box::new(Term::Let { name, expr, body })))
+    }),
+    state,
+  );
+}
+
+pub fn parse_ctr(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  parser::guard(
+    Box::new(|state| {
+      let (state, _)    = parser::text("{", state)?;
+      let (state, head) = parser::get_char(state)?;
+      Ok((state, ('A'..='Z').contains(&head)))
+    }),
+    Box::new(|state| {
+      let (state, open) = parser::text("{", state)?;
+      let (state, name) = parser::name1(state)?;
+      if name == "Type" {
+        Ok((state, Box::new(Term::Typ)))
+      } else {
+        let (state, args) = if open {
+          parser::until(parser::text_parser("}"), Box::new(parse_term), state)?
+        } else {
+          (state, Vec::new())
+        };
+        Ok((state, Box::new(Term::Ctr { name, args })))
+      }
+    }),
+    state,
+  )
+}
+
+pub fn parse_fun(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
+  parser::guard(
+    Box::new(|state| {
+      let (state, _)    = parser::text("(", state)?;
+      let (state, head) = parser::get_char(state)?;
+      Ok((state, ('A'..='Z').contains(&head)))
+    }),
+    Box::new(|state| {
+      let (state, open) = parser::text("(", state)?;
+      let (state, name) = parser::name1(state)?;
+      let (state, args) = if open {
+        parser::until(parser::text_parser(")"), Box::new(parse_term), state)?
+      } else {
+        (state, Vec::new())
+      };
+      Ok((state, Box::new(Term::Fun { name, args })))
+    }),
+    state,
+  )
+}
+
+pub fn parse_term(state: parser::State) -> parser::Answer<Box<Term>> {
+  parser::grammar(
+    "Term",
+    &[
+      Box::new(parse_let), // `let `
+      Box::new(parse_all), // `(name:`
+      Box::new(parse_ctr), // `{Name`
+      Box::new(parse_fun), // `(Name`
+      Box::new(parse_app), // `(`
+      Box::new(parse_lam), // `@`
+      Box::new(parse_var), // 
+      Box::new(|state| Ok((state, None))),
+    ],
+    state,
+  )
+}
+
+pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
+  let (state, name) = parser::name1(state)?;
+  let (state, args) = parser::until(parser::text_parser(":"), Box::new(parse_argument), state)?;
+  let (state, tipo) = parse_term(state)?;
+  let (state, head) = parser::get_char(state)?;
+  if head == '=' {
+    let (state, body) = parse_term(state)?;
+    let rules = vec![Box::new(Rule { pats: vec![], body })];
+    return Ok((state, Box::new(Entry { name, args, tipo, rules })));
+  } else if head == '{' {
+    let (state, rules) = parser::until(parser::text_parser("}"), Box::new(parse_rule), state)?;
+    return Ok((state, Box::new(Entry { name, args, tipo, rules })));
+  } else {
+    parser::expected("'=' or '{'", 1, state)
+  }
+}
+
+pub fn parse_rule(state: parser::State) -> parser::Answer<Box<Rule>> {
+  let (state, pats) = parser::until(parser::text_parser("=>"), Box::new(parse_term), state)?;
+  let (state, body) = parse_term(state)?;
+  return Ok((state, Box::new(Rule { pats, body })));
+}
+
+pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
+  let (state, _)    = parser::consume("(", state)?;
+  let (state, name) = parser::name1(state)?;
+  let (state, _)    = parser::consume(":", state)?;
+  let (state, tipo) = parse_term(state)?;
+  let (state, _)    = parser::consume(")", state)?;
+  return Ok((state, Box::new(Argument { eras: false, name, tipo })));
+}
+
+pub fn parse_file(state: parser::State) -> parser::Answer<Box<File>> {
+  let (state, entry_vec) = parser::until(Box::new(parser::done), Box::new(parse_entry), state)?;
+  let mut entries = HashMap::new();
+  for entry in entry_vec {
+    entries.insert(entry.name.clone(), entry);
+  }
+  return Ok((state, Box::new(File { entries })));
+}
+
+pub fn show_term(term: &Term) -> String {
+  match term {
+    Term::Typ => {
+      format!("Type")
+    }
+    Term::Var { name } => {
+      format!("{}", name)
+    }
+    Term::Let { name, expr, body } => {
+      let expr = show_term(expr);
+      let body = show_term(body);
+      format!("let {} = {}; {}", name, expr, body)
+    }
+    Term::Lam { name, body } => {
+      let body = show_term(body);
+      format!("@{}({})", name, body)
+    }
+    Term::App { func, argm } => {
+      let mut args = vec![argm];
+      let mut expr = func;
+      while let Term::App { func, argm } = &**expr {
+        args.push(argm);
+        expr = func;
+      }
+      args.reverse();
+      format!("({} {})", show_term(expr), args.iter().map(|x| show_term(x)).collect::<Vec<String>>().join(" "))
+    }
+    Term::All { name, tipo, body } => {
+      let body = show_term(body);
+      format!("({}: {}) {}", name, show_term(tipo), body)
+    }
+    Term::Ctr { name, args } => {
+      format!("{{{}{}}}", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
+    }
+    Term::Fun { name, args } => {
+      format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
+    }
+  }
+}
+
+pub fn show_rule(rule: &Rule) -> String {
+  let mut pats = vec![];
+  for pat in &rule.pats {
+    pats.push(show_term(pat));
+  }
+  let body = show_term(&rule.body);
+  format!("{} => {}", pats.join(" "), body)
+}
+
+pub fn show_entry(entry: &Entry) -> String {
+  let name = &entry.name;
+  let mut args = vec![];
+  for arg in &entry.args {
+    args.push(format!(" ({}: {})", arg.name, show_term(&arg.tipo)));
+  }
+  let mut rules = vec![];
+  for rule in &entry.rules {
+    rules.push(format!("\n {}", show_rule(rule)));
+  }
+  format!("{}{} : {} {{{}\n}}", name, args.join(""), show_term(&entry.tipo), rules.join(""))
+}
+
+pub fn show_file(file: &File) -> String {
+  let mut entries = vec![];
+  for entry in file.entries.values() {
+    entries.push(show_entry(entry));
+  }
+  entries.join("\n")
+}
+
+pub fn read_term(code: &str) -> Result<Box<Term>, String> {
+  parser::read(Box::new(parse_term), code)
+}
+
+pub fn read_file(code: &str) -> Result<Box<File>, String> {
+  parser::read(Box::new(parse_file), code)
+}
+
+fn main() -> Result<(), String> {
+
+  //let term = read_term("{Foo @x(x) {Tic} {Tac}}")?;
+  //println!("Parsed: {}", show_term(&*term));
+
+  let file = read_file("
+    Bool : Type {}
+      True  : Bool {}
+      False : Bool {}
+
+    Add (a: Nat) (b: Nat) : Nat {
+      {Zero}   b => b
+      {Succ a} b => {Succ (Add a b)}
+    }
+
+    Not (a: Bool) : Bool {
+      {True}  => {False}
+      {False} => {True}
+    }
+
+    Map (a: Type) (b: Type) (f: (x: a) a) (xs: (List a)) : (List b) {
+      a b f {Cons x xs} => {Cons (f x) (Map a b f xs)}
+      a b f Nil         => {Nil}
+    }
+  ")?;
+
+  println!("parsed:\n\n{}", show_file(&file));
+
+  return Ok(());
+}
+
+
+
+
+
+//Map (a: {Type}) (b: {Type}) (f: (x: a) a) (xs: ({List} a)) : ({List} b) {
+ //a b f {Cons x xs} => {Cons (f x) ({Map} a b f xs)}
+ //a b f {Nil}       => {Nil}
+//}
+
+
+
+
+
+
+
+
+
+
+
+
+
+