From d6240a4b184cac1fbf61ab35f9f3813efb780d31 Mon Sep 17 00:00:00 2001 From: NanoTech Date: Tue, 6 Dec 2016 09:10:15 +0000 Subject: Initial commit --- .gitignore | 2 + Cargo.lock | 274 ++++++++++++++++++++++++++++++++++++++++++++++++++++ Cargo.toml | 12 +++ LICENSE | 48 +++++++++ build.rs | 6 ++ src/core.rs | 222 ++++++++++++++++++++++++++++++++++++++++++ src/grammar.lalrpop | 94 ++++++++++++++++++ src/grammar_util.rs | 8 ++ src/lexer.rs | 240 +++++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 31 ++++++ src/parser.rs | 34 +++++++ 11 files changed, 971 insertions(+) create mode 100644 .gitignore create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 LICENSE create mode 100644 build.rs create mode 100644 src/core.rs create mode 100644 src/grammar.lalrpop create mode 100644 src/grammar_util.rs create mode 100644 src/lexer.rs create mode 100644 src/main.rs create mode 100644 src/parser.rs 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 "] +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 { + /// `Const c ~ c` + Const(Const), + /// `Var (V x 0) ~ x`
+ /// `Var (V x n) ~ x@n` + Var(Var), + /// `Lam x A b ~ λ(x : A) -> b` + Lam(String, Box>, Box>), + /// `Pi "_" A B ~ A -> B` + /// `Pi x A B ~ ∀(x : A) -> B` + Pi(String, Box>, Box>), + /// `App f A ~ f A` + App(Box>, Box>), + /// `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>, Box>), + /// `Annot x t ~ x : t` + Annot(Box>, Box>), + /// `Bool ~ Bool` + Bool, + /// `BoolLit b ~ b` + BoolLit(bool), + /// `BoolAnd x y ~ x && y` + BoolAnd(Box>, Box>), + /// `BoolOr x y ~ x || y` + BoolOr(Box>, Box>), + /// `BoolEQ x y ~ x == y` + BoolEQ(Box>, Box>), + /// `BoolNE x y ~ x != y` + BoolNE(Box>, Box>), + /// `BoolIf x y z ~ if x then y else z` + BoolIf(Box>, Box>, Box>), + /// `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>, Box>), + /// `NaturalTimes x y ~ x * y` + NaturalTimes(Box>, Box>), + /// `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>, Box>), + /// `List ~ List` + List, + /// `ListLit t [x, y, z] ~ [x, y, z] : List t` + ListLit(Box>, Vec>), + /// `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>, Vec>), + /// `OptionalFold ~ Optional/fold` + OptionalFold, + /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` + Record(HashMap>), + /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` + RecordLit(HashMap>), + /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >` + Union(HashMap>), + /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >` + UnionLit(String, Box>, HashMap>), + /// `Combine x y ~ x ∧ y` + Combine(Box>, Box>), + /// `Merge x y t ~ merge x y : t` + Merge(Box>, Box>, Box>), + /// `Field e x ~ e.x` + Field(Box>, String), + /// `Note S x ~ e` + Note(S, Box>), + /// `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(), + Nat => Tok::Natural(), + Bool => Tok::Bool(), + Label => Tok::Identifier(), + Reserved => Tok::Reserved(), + + "(" => 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 + ":" => bx(Annot(<>)), + ExprB, +}; + +ExprB: BoxExpr = { + Lambda "("