Initial commit

11 files changed, 971 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..3ad9015
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+src/grammar.rs
+target
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..50a3b6b
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,274 @@
+[root]
+name = "dhall"
+version = "0.1.0"
+dependencies = [
+ "lalrpop 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-util 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "nom 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "aho-corasick"
+version = "0.5.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "memchr 0.1.11 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "atty"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "kernel32-sys 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libc 0.2.18 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi 0.2.8 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "bit-set"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "bit-vec 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "bit-vec"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "bitflags"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "diff"
+version = "0.1.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "docopt"
+version = "0.6.86"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "lazy_static 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex 0.1.80 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rustc-serialize 0.3.21 (registry+https://github.com/rust-lang/crates.io-index)",
+ "strsim 0.5.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "fixedbitset"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "itertools"
+version = "0.3.25"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "kernel32-sys"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "winapi 0.2.8 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi-build 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "lalrpop"
+version = "0.12.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "atty 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bit-set 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bitflags 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "diff 0.1.9 (registry+https://github.com/rust-lang/crates.io-index)",
+ "docopt 0.6.86 (registry+https://github.com/rust-lang/crates.io-index)",
+ "itertools 0.3.25 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-intern 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-snap 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-util 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "petgraph 0.1.18 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex 0.1.80 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex-syntax 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rustc-serialize 0.3.21 (registry+https://github.com/rust-lang/crates.io-index)",
+ "term 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "lalrpop-intern"
+version = "0.12.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "lalrpop-snap"
+version = "0.12.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "atty 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bit-set 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bitflags 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "diff 0.1.9 (registry+https://github.com/rust-lang/crates.io-index)",
+ "docopt 0.6.86 (registry+https://github.com/rust-lang/crates.io-index)",
+ "itertools 0.3.25 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-intern 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "lalrpop-util 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "petgraph 0.1.18 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex 0.1.80 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex-syntax 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "rustc-serialize 0.3.21 (registry+https://github.com/rust-lang/crates.io-index)",
+ "term 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "lalrpop-util"
+version = "0.12.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "lazy_static"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "libc"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "memchr"
+version = "0.1.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "libc 0.2.18 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "nom"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "petgraph"
+version = "0.1.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "fixedbitset 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "regex"
+version = "0.1.80"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "aho-corasick 0.5.3 (registry+https://github.com/rust-lang/crates.io-index)",
+ "memchr 0.1.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "regex-syntax 0.3.9 (registry+https://github.com/rust-lang/crates.io-index)",
+ "thread_local 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "utf8-ranges 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "regex-syntax"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "rustc-serialize"
+version = "0.3.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "strsim"
+version = "0.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "term"
+version = "0.4.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "kernel32-sys 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "winapi 0.2.8 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "thread-id"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "kernel32-sys 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libc 0.2.18 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "thread_local"
+version = "0.2.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "thread-id 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "unicode-xid"
+version = "0.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "utf8-ranges"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "winapi"
+version = "0.2.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "winapi-build"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[metadata]
+"checksum aho-corasick 0.5.3 (registry+https://github.com/rust-lang/crates.io-index)" = "ca972c2ea5f742bfce5687b9aef75506a764f61d37f8f649047846a9686ddb66"
+"checksum atty 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "d0fd4c0631f06448cc45a6bbb3b710ebb7ff8ccb96a0800c994afe23a70d5df2"
+"checksum bit-set 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "84527c7b0452f22545cc010e72d366a435561d2b28b978035550b3778c4d428d"
+"checksum bit-vec 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)" = "5b97c2c8e8bbb4251754f559df8af22fb264853c7d009084a576cdf12565089d"
+"checksum bitflags 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "8dead7461c1127cf637931a1e50934eb6eee8bff2f74433ac7909e9afcee04a3"
+"checksum diff 0.1.9 (registry+https://github.com/rust-lang/crates.io-index)" = "e48977eec6d3b7707462c2dc2e1363ad91b5dd822cf942537ccdc2085dc87587"
+"checksum docopt 0.6.86 (registry+https://github.com/rust-lang/crates.io-index)" = "4a7ef30445607f6fc8720f0a0a2c7442284b629cf0d049286860fae23e71c4d9"
+"checksum fixedbitset 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "88c3c33fc4c00db33f5174eb98aea809c4c007db0b71351d810a7e094ea3b64d"
+"checksum itertools 0.3.25 (registry+https://github.com/rust-lang/crates.io-index)" = "16b73f1c685cfd8ff8d75698ed87e6188cd09944b30c0863d45c2c3699d1da0c"
+"checksum kernel32-sys 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "7507624b29483431c0ba2d82aece8ca6cdba9382bff4ddd0f7490560c056098d"
+"checksum lalrpop 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)" = "95af72b26d2056ca73387cb71d29e727c336d2b8a766ee09b210bed44d6f857b"
+"checksum lalrpop-intern 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)" = "4e76b1f6eead09c4edde090dc69e3757775ab36cbf907fb0857181160b9ca5a1"
+"checksum lalrpop-snap 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)" = "a096006ebe9cef49295a142af7cb3cf2f782bf594213c786e0cc070b0d237073"
+"checksum lalrpop-util 0.12.4 (registry+https://github.com/rust-lang/crates.io-index)" = "5ab0e358c557ea426b05719c82ac649cae0f0f7f2855145111fe59eab207b285"
+"checksum lazy_static 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6abe0ee2e758cd6bc8a2cd56726359007748fbf4128da998b65d0b70f881e19b"
+"checksum libc 0.2.18 (registry+https://github.com/rust-lang/crates.io-index)" = "a51822fc847e7a8101514d1d44e354ba2ffa7d4c194dcab48870740e327cac70"
+"checksum memchr 0.1.11 (registry+https://github.com/rust-lang/crates.io-index)" = "d8b629fb514376c675b98c1421e80b151d3817ac42d7c667717d282761418d20"
+"checksum nom 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)" = "628d6ee18ab0ca1c1feb3331caa6ad2e53f6053b2505662b90d194889bbcd571"
+"checksum petgraph 0.1.18 (registry+https://github.com/rust-lang/crates.io-index)" = "bfd1de18b0a5f1777162e5b61aaf498032467d5409ab4ca6dbd03049f5708de1"
+"checksum regex 0.1.80 (registry+https://github.com/rust-lang/crates.io-index)" = "4fd4ace6a8cf7860714a2c2280d6c1f7e6a413486c13298bbc86fd3da019402f"
+"checksum regex-syntax 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)" = "a21935ce5a4dfa48e3ded1aefbbe353fb9ab258b0d3fa0bd168bef00797b3dc7"
+"checksum regex-syntax 0.3.9 (registry+https://github.com/rust-lang/crates.io-index)" = "f9ec002c35e86791825ed294b50008eea9ddfc8def4420124fbc6b08db834957"
+"checksum rustc-serialize 0.3.21 (registry+https://github.com/rust-lang/crates.io-index)" = "bff9fc1c79f2dec76b253273d07682e94a978bd8f132ded071188122b2af9818"
+"checksum strsim 0.5.2 (registry+https://github.com/rust-lang/crates.io-index)" = "67f84c44fbb2f91db7fef94554e6b2ac05909c9c0b0bc23bb98d3a1aebfe7f7c"
+"checksum term 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)" = "3deff8a2b3b6607d6d7cc32ac25c0b33709453ca9cceac006caac51e963cf94a"
+"checksum thread-id 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)" = "a9539db560102d1cef46b8b78ce737ff0bb64e7e18d35b2a5688f7d097d0ff03"
+"checksum thread_local 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)" = "8576dbbfcaef9641452d5cf0df9b0e7eeab7694956dd33bb61515fb8f18cfdd5"
+"checksum unicode-xid 0.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "f69506a2561962651710609304bbb961fa3da598c812f877975a82e48ee144f9"
+"checksum utf8-ranges 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "a1ca13c08c41c9c3e04224ed9ff80461d97e121589ff27c753a16cb10830ae0f"
+"checksum winapi 0.2.8 (registry+https://github.com/rust-lang/crates.io-index)" = "167dc9d6949a9b857f3451275e911c3f44255842c1f7a76f33c55103a909087a"
+"checksum winapi-build 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "2d315eee3b34aca4797b2da6b13ed88266e6d612562a0c46390af8299fc699bc"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..625cda1
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "dhall"
+version = "0.1.0"
+authors = ["NanoTech <nanotech@nanotechcorp.net>"]
+build = "build.rs"
+
+[build-dependencies]
+lalrpop = "0.12.4"
+
+[dependencies]
+lalrpop-util = "0.12.4"
+nom = "2.0.0"
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..e7a3af6
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,48 @@
+Copyright 2017 NanoTech
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+    1. Redistributions of source code must retain the above copyright notice,
+       this list of conditions and the following disclaimer.
+
+    2. Redistributions in binary form must reproduce the above copyright notice,
+       this list of conditions and the following disclaimer in the documentation
+       and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+
+Copyright (c) 2017 Gabriel Gonzalez
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright notice,
+      this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright notice,
+      this list of conditions and the following disclaimer in the documentation
+      and/or other materials provided with the distribution.
+    * Neither the name of Gabriel Gonzalez nor the names of other contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/build.rs b/build.rs
new file mode 100644
index 0000000..ce7e591
--- /dev/null
+++ b/build.rs
@@ -0,0 +1,6 @@
+extern crate lalrpop;
+
+fn main() {
+    lalrpop::process_root().unwrap();
+    println!("cargo:rerun-if-changed=src/grammar.lalrpop");
+}
diff --git a/src/core.rs b/src/core.rs
new file mode 100644
index 0000000..8e59141
--- /dev/null
+++ b/src/core.rs
@@ -0,0 +1,222 @@
+use std::collections::HashMap;
+use std::path::PathBuf;
+
+/*
+module Dhall.Core (
+    -- * Syntax
+      Const(..)
+    , Path(..)
+    , Var(..)
+    , Expr(..)
+
+    -- * Normalization
+    , normalize
+    , subst
+    , shift
+
+    -- * Pretty-printing
+    , pretty
+
+    -- * Miscellaneous
+    , internalError
+    ) where
+*/
+
+/// Constants for a pure type system
+///
+/// The only axiom is:
+///
+/// ```c
+/// ⊦ Type : Kind
+/// ```
+///
+/// ... and the valid rule pairs are:
+///
+/// ```c
+/// ⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)
+/// ⊦ Kind ↝ Type : Type  -- Functions from types to terms (polymorphic functions)
+/// ⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type constructors)
+/// ```
+///
+/// These are the same rule pairs as System Fω
+///
+/// Note that Dhall does not support functions from terms to types and therefore
+/// Dhall is not a dependently typed language
+///
+#[derive(Debug, PartialEq, Eq)] // (Show, Bounded, Enum)
+pub enum Const {
+    Type,
+    Kind,
+}
+
+
+/// Path to an external resource
+#[derive(Debug, PartialEq, Eq)] // (Eq, Ord, Show)
+pub enum Path {
+    File(PathBuf),
+    URL(String),
+}
+
+/// Label for a bound variable
+///
+/// The `String` field is the variable's name (i.e. \"`x`\").
+///
+/// The `Int` field disambiguates variables with the same name if there are
+/// multiple bound variables of the same name in scope.  Zero refers to the
+/// nearest bound variable and the index increases by one for each bound
+/// variable of the same name going outward.  The following diagram may help:
+///
+/// ```c
+///                                 +---refers to--+
+///                                 |              |
+///                                 v              |
+/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0
+///
+///   +------------------refers to-----------------+
+///   |                                            |
+///   v                                            |
+/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1
+/// ```
+///
+/// This `Int` behaves like a De Bruijn index in the special case where all
+/// variables have the same name.
+///
+/// You can optionally omit the index if it is `0`:
+///
+/// ```c
+///                           +refers to+
+///                           |         |
+///                           v         |
+/// \(x : *) -> \(y : *) -> \(x : *) -> x
+/// ```
+///
+/// Zero indices are omitted when pretty-printing `Var`s and non-zero indices
+/// appear as a numeric suffix.
+///
+#[derive(Debug, PartialEq, Eq)] // (Eq, Show)
+pub struct Var(pub String, pub Int);
+
+/*
+instance IsString Var where
+    fromString str = V (fromString str) 0
+
+instance Buildable Var where
+    build = buildVar
+*/
+
+/// Syntax tree for expressions
+#[derive(Debug, PartialEq)] // (Functor, Foldable, Traversable, Show)
+pub enum Expr<S, A> {
+    ///  `Const c                                  ~  c`
+    Const(Const),
+    ///  `Var (V x 0)                              ~  x`<br>
+    ///  `Var (V x n)                              ~  x@n`
+    Var(Var),
+    ///  `Lam x     A b                            ~  λ(x : A) -> b`
+    Lam(String, Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Pi "_" A B                               ~        A  -> B`
+    ///  `Pi x   A B                               ~  ∀(x : A) -> B`
+    Pi(String, Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `App f A                                  ~  f A`
+    App(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Let x Nothing  r e  ~  let x     = r in e`
+    ///  `Let x (Just t) r e  ~  let x : t = r in e`
+    Let(String, Option<Box<Expr<S, A>>>, Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Annot x t                                ~  x : t`
+    Annot(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Bool                                     ~  Bool`
+    Bool,
+    ///  `BoolLit b                                ~  b`
+    BoolLit(bool),
+    ///  `BoolAnd x y                              ~  x && y`
+    BoolAnd(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `BoolOr  x y                              ~  x || y`
+    BoolOr(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `BoolEQ  x y                              ~  x == y`
+    BoolEQ(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `BoolNE  x y                              ~  x != y`
+    BoolNE(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `BoolIf x y z                             ~  if x then y else z`
+    BoolIf(Box<Expr<S, A>>, Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Natural                                  ~  Natural`
+    Natural,
+    ///  `NaturalLit n                             ~  +n`
+    NaturalLit(Natural),
+    ///  `NaturalFold                              ~  Natural/fold`
+    NaturalFold,
+    ///  `NaturalBuild                             ~  Natural/build`
+    NaturalBuild,
+    ///  `NaturalIsZero                            ~  Natural/isZero`
+    NaturalIsZero,
+    ///  `NaturalEven                              ~  Natural/even`
+    NaturalEven,
+    ///  `NaturalOdd                               ~  Natural/odd`
+    NaturalOdd,
+    ///  `NaturalPlus x y                          ~  x + y`
+    NaturalPlus(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `NaturalTimes x y                         ~  x * y`
+    NaturalTimes(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Integer                                  ~  Integer`
+    Integer,
+    ///  `IntegerLit n                             ~  n`
+    IntegerLit(Integer),
+    ///  `Double                                   ~  Double`
+    Double,
+    ///  `DoubleLit n                              ~  n`
+    DoubleLit(Double),
+    ///  `Text                                     ~  Text`
+    Text,
+    ///  `TextLit t                                ~  t`
+    TextLit(Builder),
+    ///  `TextAppend x y                           ~  x ++ y`
+    TextAppend(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `List                                     ~  List`
+    List,
+    ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
+    ListLit(Box<Expr<S, A>>, Vec<Expr<S, A>>),
+    ///  `ListBuild                                ~  List/build`
+    ListBuild,
+    ///  `ListFold                                 ~  List/fold`
+    ListFold,
+    ///  `ListLength                               ~  List/length`
+    ListLength,
+    ///  `ListHead                                 ~  List/head`
+    ListHead,
+    ///  `ListLast                                 ~  List/last`
+    ListLast,
+    ///  `ListIndexed                              ~  List/indexed`
+    ListIndexed,
+    ///  `ListReverse                              ~  List/reverse`
+    ListReverse,
+    ///  `Optional                                 ~  Optional`
+    Optional,
+    ///  `OptionalLit t [e]                        ~  [e] : Optional t`
+    ///  `OptionalLit t []                         ~  []  : Optional t`
+    OptionalLit(Box<Expr<S, A>>, Vec<Expr<S, A>>),
+    ///  `OptionalFold                             ~  Optional/fold`
+    OptionalFold,
+    ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
+    Record(HashMap<String, Expr<S, A>>),
+    ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
+    RecordLit(HashMap<String, Expr<S, A>>),
+    ///  `Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >`
+    Union(HashMap<String, Expr<S, A>>),
+    ///  `UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 >`
+    UnionLit(String, Box<Expr<S, A>>, HashMap<String, Expr<S, A>>),
+    ///  `Combine x y                              ~  x ∧ y`
+    Combine(Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Merge x y t                              ~  merge x y : t`
+    Merge(Box<Expr<S, A>>, Box<Expr<S, A>>, Box<Expr<S, A>>),
+    ///  `Field e x                                ~  e.x`
+    Field(Box<Expr<S, A>>, String),
+    ///  `Note S x                                 ~  e`
+    Note(S, Box<Expr<S, A>>),
+    ///  `Embed path                               ~  path`
+    Embed(A),
+}
+
+pub type Builder = String;
+pub type Double = f64;
+pub type Int = isize;
+pub type Integer = isize;
+pub type Natural = usize;
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
new file mode 100644
index 0000000..e940da9
--- /dev/null
+++ b/src/grammar.lalrpop
@@ -0,0 +1,94 @@
+use core;
+use core::Expr::*;
+use grammar_util::*;
+use lexer::{Keyword, LexicalError, Tok};
+
+grammar;
+
+extern {
+    type Location = usize;
+    type Error = LexicalError;
+
+    enum Tok {
+        Pi => Tok::Pi,
+        Lambda => Tok::Lambda,
+        Combine => Tok::Combine,
+        "->" => Tok::Arrow,
+
+        Int => Tok::Integer(<isize>),
+        Nat => Tok::Natural(<usize>),
+        Bool => Tok::Bool(<bool>),
+        Label => Tok::Identifier(<String>),
+        Reserved => Tok::Reserved(<Keyword>),
+
+        "(" => Tok::ParenL,
+        ")" => Tok::ParenR,
+        "&&" => Tok::BoolAnd,
+        "||" => Tok::BoolOr,
+        "==" => Tok::CompareEQ,
+        "!=" => Tok::CompareNE,
+        "++" => Tok::Append,
+        "*" => Tok::Times,
+        "+" => Tok::Plus,
+        "." => Tok::Dot,
+        ":" => Tok::Ascription,
+        "=" => Tok::Equals,
+    }
+}
+
+pub Expr: BoxExpr = { // exprA
+    <ExprB> ":" <Expr> => bx(Annot(<>)),
+    ExprB,
+};
+
+ExprB: BoxExpr = {
+    Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
+    ExprC0,
+};
+
+BoolOr: ExprOpFn = { "||" => BoolOr };
+NaturalPlus: ExprOpFn = { "+" => NaturalPlus };
+TextAppend: ExprOpFn = { "++" => TextAppend };
+BoolAnd: ExprOpFn = { "&&" => BoolAnd };
+CombineOp: ExprOpFn = { Combine => Combine };
+NaturalTimes: ExprOpFn = { "*" => NaturalTimes };
+BoolEQ: ExprOpFn = { "==" => BoolEQ };
+BoolNE: ExprOpFn = { "!=" => BoolNE };
+
+Tier<NextTier, Op>: BoxExpr = {
+    <a:NextTier> <f:Op> <b:Tier<NextTier, Op>> => bx(f(a, b)),
+    // <b:Tier<NextTier, Op>> <f:Op> <a:NextTier> => bx(f(a, b)),
+    NextTier,
+};
+
+ExprC0 = Tier<ExprC1, BoolOr>;
+ExprC1 = Tier<ExprC2, NaturalPlus>;
+ExprC2 = Tier<ExprC3, TextAppend>;
+ExprC3 = Tier<ExprC4, BoolAnd>;
+ExprC4 = Tier<ExprC5, CombineOp>;
+ExprC5 = Tier<ExprC6, NaturalTimes>;
+ExprC6 = Tier<ExprC7, BoolEQ>;
+ExprC7 = Tier<ExprD, BoolNE>;
+
+ExprD: BoxExpr = {
+    <v:(ExprE)+> => {
+        let mut it = v.into_iter();
+        let f = it.next().unwrap();
+        it.fold(f, |f, x| bx(App(f, x)))
+    }
+};
+
+ExprE: BoxExpr = {
+    <a:ExprF> <fields:("." <Label>)*> => {
+        fields.into_iter().fold(a, |x, f| bx(Field(x, f)))
+    },
+};
+
+ExprF: BoxExpr = {
+    Nat => bx(NaturalLit(<>)),
+    Int => bx(IntegerLit(<>)),
+    Label => bx(Var(core::Var(<>, 0))), // FIXME support var@n syntax
+    Reserved => bx(Bool), // FIXME
+    Bool => bx(BoolLit(<>)),
+    "(" <Expr> ")",
+};
diff --git a/src/grammar_util.rs b/src/grammar_util.rs
new file mode 100644
index 0000000..cbd1e59
--- /dev/null
+++ b/src/grammar_util.rs
@@ -0,0 +1,8 @@
+use core::Expr;
+
+pub type BoxExpr = Box<Expr<(), ()>>;
+pub type ExprOpFn = fn(BoxExpr, BoxExpr) -> Expr<(), ()>;
+
+pub fn bx<T>(x: T) -> Box<T> {
+    Box::new(x)
+}
diff --git a/src/lexer.rs b/src/lexer.rs
new file mode 100644
index 0000000..f141f81
--- /dev/null
+++ b/src/lexer.rs
@@ -0,0 +1,240 @@
+use nom;
+
+use std::str::FromStr;
+
+#[derive(Debug, PartialEq, Eq)]
+pub enum Keyword {
+    Natural,
+    NaturalFold,
+    NaturalBuild,
+    NaturalIsZero,
+    NaturalEven,
+    NaturalOdd,
+    Integer,
+    Double,
+    Text,
+    List,
+    ListBuild,
+    ListFold,
+    ListLength,
+    ListHead,
+    ListLast,
+    ListIndexed,
+    ListReverse,
+    Optional,
+    OptionalFold,
+    Bool,
+}
+
+#[derive(Debug, PartialEq, Eq)]
+pub enum Tok {
+    Identifier(String),
+    Reserved(Keyword),
+    Bool(bool),
+    Integer(isize),
+    Natural(usize),
+
+    // Symbols
+    ParenL,
+    ParenR,
+    Arrow,
+    Lambda,
+    Pi,
+    Combine,
+    BoolAnd,
+    BoolOr,
+    CompareEQ,
+    CompareNE,
+    Append,
+    Times,
+    Plus,
+    Dot,
+    Ascription,
+    Equals,
+}
+
+#[derive(Debug)]
+pub enum LexicalError {
+    Error(nom::simple_errors::Err<u32>),
+    Incomplete(nom::Needed),
+}
+
+pub type Spanned<Tok, Loc, Error> = Result<(Loc, Tok, Loc), Error>;
+
+/*
+macro_rules! one_of_chars {
+    ($c:expr, [$($cs:pat),*]) => {
+        match $c {
+            $($cs => true),*,
+            _ => false,
+        }
+    }
+}
+
+fn is_symbol(c: char) -> bool {
+    one_of_chars!(c, [
+        '!',
+        '&',
+        '(',
+        ')',
+        '*',
+        '+',
+        '-',
+        '/',
+        ':',
+        '=',
+        '>',
+        '\\',
+        '|',
+        '∧',
+        'λ'
+    ])
+}
+named!(symbol<&str, &str>, take_while1_s!(is_symbol));
+*/
+
+fn is_decimal(c: char) -> bool {
+    c.is_digit(10)
+}
+
+named!(identifier<&str, &str>, take_while1_s!(char::is_alphabetic)); // FIXME [A-Za-z_][A-Za-z0-9_/]*
+named!(natural<&str, &str>, preceded!(tag!("+"), take_while1_s!(is_decimal)));
+named!(integral<&str, isize>, map_res!(take_while1_s!(is_decimal), |s| isize::from_str(s)));
+named!(integer<&str, isize>, alt!(
+    preceded!(tag!("-"), map!(integral, |i: isize| -i)) |
+    integral
+));
+named!(boolean<&str, bool>, alt!(
+    value!(true, tag!("True")) |
+    value!(false, tag!("False"))
+));
+
+named!(keyword<&str, Keyword>, alt!(
+    value!(Keyword::Natural, tag!("Natural")) |
+    value!(Keyword::NaturalFold, tag!("Natural/fold")) |
+    value!(Keyword::NaturalBuild, tag!("Natural/build")) |
+    value!(Keyword::NaturalIsZero, tag!("Natural/isZero")) |
+    value!(Keyword::NaturalEven, tag!("Natural/even")) |
+    value!(Keyword::NaturalOdd, tag!("Natural/odd")) |
+    value!(Keyword::Integer, tag!("Integer")) |
+    value!(Keyword::Double, tag!("Double")) |
+    value!(Keyword::Text, tag!("Text")) |
+    value!(Keyword::List, tag!("List")) |
+    value!(Keyword::ListBuild, tag!("List/build")) |
+    value!(Keyword::ListFold, tag!("List/fold")) |
+    value!(Keyword::ListLength, tag!("List/length")) |
+    value!(Keyword::ListHead, tag!("List/head")) |
+    value!(Keyword::ListLast, tag!("List/last")) |
+    value!(Keyword::ListIndexed, tag!("List/indexed")) |
+    value!(Keyword::ListReverse, tag!("List/reverse")) |
+    value!(Keyword::Optional, tag!("Optional")) |
+    value!(Keyword::OptionalFold, tag!("Optional/fold")) |
+    value!(Keyword::Bool, tag!("Bool"))
+));
+
+named!(token<&str, Tok>, alt!(
+    value!(Tok::Pi, tag!("forall")) |
+    value!(Tok::Pi, tag!("∀")) |
+    value!(Tok::Lambda, tag!("\\")) |
+    value!(Tok::Lambda, tag!("λ")) |
+    value!(Tok::Combine, tag!("/\\")) |
+    value!(Tok::Combine, tag!("∧")) |
+    value!(Tok::Arrow, tag!("->")) |
+    value!(Tok::Arrow, tag!("→")) |
+
+    map!(boolean, Tok::Bool) |
+    map!(keyword, Tok::Reserved) |
+    map_opt!(natural, |s| usize::from_str(s).ok().map(|n| Tok::Natural(n))) |
+    map!(integer, Tok::Integer) |
+    map!(identifier, |s: &str| Tok::Identifier(s.to_owned())) |
+
+    value!(Tok::ParenL, tag!("(")) |
+    value!(Tok::ParenR, tag!(")")) |
+    value!(Tok::BoolAnd, tag!("&&")) |
+    value!(Tok::BoolOr, tag!("||")) |
+    value!(Tok::CompareEQ, tag!("==")) |
+    value!(Tok::CompareNE, tag!("!=")) |
+    value!(Tok::Append, tag!("++")) |
+    value!(Tok::Times, tag!("*")) |
+    value!(Tok::Plus, tag!("+")) |
+    value!(Tok::Dot, tag!(".")) |
+    value!(Tok::Ascription, tag!(":")) |
+    value!(Tok::Equals, tag!("="))
+));
+
+pub struct Lexer<'input> {
+    input: &'input str,
+    offset: usize,
+}
+
+impl<'input> Lexer<'input> {
+    pub fn new(input: &'input str) -> Self {
+        Lexer {
+            input: input,
+            offset: 0,
+        }
+    }
+
+    fn current_input(&mut self) -> &'input str {
+        &self.input[self.offset..]
+    }
+
+    fn skip_whitespace(&mut self) {
+        let input = self.current_input();
+        let trimmed = input.trim_left();
+        let whitespace_len = input.len() - trimmed.len();
+        if whitespace_len > 0 {
+            //println!("skipped {} whitespace bytes", whitespace_len);
+            self.offset += whitespace_len;
+        }
+    }
+}
+
+impl<'input> Iterator for Lexer<'input> {
+    type Item = Spanned<Tok, usize, LexicalError>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        if self.offset >= self.input.len() {
+            return None;
+        }
+
+        use nom::IResult::*;
+        self.skip_whitespace();
+        let input = self.current_input();
+        match token(input) {
+            Done(rest, t) => {
+                let parsed_len = input.len() - rest.len();
+                //println!("parsed {} bytes => {:?}", parsed_len, t);
+                let start = self.offset;
+                self.offset += parsed_len;
+                Some(Ok((start, t, self.offset)))
+            }
+            Error(e) => {
+                self.offset = self.input.len();
+                Some(Err(LexicalError::Error(e)))
+            }
+            Incomplete(needed) => {
+                Some(Err(LexicalError::Incomplete(needed)))
+            }
+        }
+    }
+}
+
+#[test]
+fn test_lex() {
+    use self::Tok::*;
+    let s = "λ(b : Bool) → b == False";
+    let expected = [Lambda,
+                    ParenL,
+                    Identifier("b".to_owned()),
+                    Ascription,
+                    Reserved(Keyword::Bool),
+                    ParenR,
+                    Arrow,
+                    Identifier("b".to_owned()),
+                    CompareEQ,
+                    Bool(false)];
+    let lexer = Lexer::new(s);
+    let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
+    assert_eq!(&tokens, &expected);
+}
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..aebbad9
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,31 @@
+extern crate lalrpop_util;
+#[macro_use]
+extern crate nom;
+
+mod core;
+pub use core::*;
+pub mod grammar;
+mod grammar_util;
+pub mod lexer;
+pub mod parser;
+
+fn main() {
+    println!("Hello, world!");
+
+    /*
+    inText <- Data.Text.Lazy.IO.getContents
+
+    expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of
+        Left  err  -> Control.Exception.throwIO err
+        Right expr -> return expr
+
+    expr' <- load expr
+
+    typeExpr <- case Dhall.TypeCheck.typeOf expr' of
+        Left  err      -> Control.Exception.throwIO err
+        Right typeExpr -> return typeExpr
+    Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr))
+    Data.Text.Lazy.IO.hPutStrLn stderr mempty
+    Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) )
+    */
+}
diff --git a/src/parser.rs b/src/parser.rs
new file mode 100644
index 0000000..1561230
--- /dev/null
+++ b/src/parser.rs
@@ -0,0 +1,34 @@
+use lalrpop_util;
+
+use grammar;
+use grammar_util::BoxExpr;
+use lexer::{Lexer, LexicalError, Tok};
+
+pub type ParseError = lalrpop_util::ParseError<usize, Tok, LexicalError>;
+
+fn parse_expr(s: &str) -> Result<BoxExpr, ParseError>  {
+    grammar::parse_Expr(Lexer::new(s))
+}
+
+#[test]
+fn test_parse() {
+    use core::Expr::*;
+    println!("test {:?}", parse_expr("+3 + +5 * +10"));
+    assert!(parse_expr("22").is_ok());
+    assert!(parse_expr("(22)").is_ok());
+    assert_eq!(parse_expr("+3 + +5 * +10").ok(),
+               Some(Box::new(NaturalPlus(Box::new(NaturalLit(3)),
+                                Box::new(NaturalTimes(Box::new(NaturalLit(5)),
+                                                      Box::new(NaturalLit(10))))))));
+    // The original parser is apparently right-associative
+    assert_eq!(parse_expr("+2 * +3 * +4").ok(),
+               Some(Box::new(NaturalTimes(Box::new(NaturalLit(2)),
+                                 Box::new(NaturalTimes(Box::new(NaturalLit(3)),
+                                                       Box::new(NaturalLit(4))))))));
+    assert!(parse_expr("((((22))))").is_ok());
+    assert!(parse_expr("((22)").is_err());
+    println!("{:?}", parse_expr("\\(b : Bool) -> b == False"));
+    assert!(parse_expr("\\(b : Bool) -> b == False").is_ok());
+    println!("{:?}", parse_expr("foo.bar"));
+    assert!(parse_expr("foo.bar").is_ok());
+}