summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/core.rs1205
-rw-r--r--dhall/src/grammar.lalrpop164
-rw-r--r--dhall/src/grammar_util.rs7
-rw-r--r--dhall/src/lexer.rs394
-rw-r--r--dhall/src/lib.rs7
-rw-r--r--dhall/src/main.rs1
-rw-r--r--dhall/src/parser.rs827
-rw-r--r--dhall/src/typecheck.rs14
8 files changed, 8 insertions, 2611 deletions
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
deleted file mode 100644
index 340cb04..0000000
--- a/dhall/src/core.rs
+++ /dev/null
@@ -1,1205 +0,0 @@
-#![allow(non_snake_case)]
-use std::collections::BTreeMap;
-use std::fmt::{self, Display};
-use std::path::PathBuf;
-
-/// 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, Copy, Clone, PartialEq, Eq)] // (Show, Bounded, Enum)
-pub enum Const {
- Type,
- Kind,
-}
-
-/// Path to an external resource
-#[derive(Debug, Clone, 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, Copy, Clone, PartialEq, Eq)]
-pub struct V<'i>(pub &'i str, pub usize);
-
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BinOp {
- /// x && y`
- BoolAnd,
- /// x || y`
- BoolOr,
- /// x == y`
- BoolEQ,
- /// x != y`
- BoolNE,
- /// x + y`
- NaturalPlus,
- /// x * y`
- NaturalTimes,
- /// x ++ y`
- TextAppend,
- /// x ∧ y`
- Combine,
- /// x //\\ y
- CombineTypes,
- /// x ? y
- ImportAlt,
- /// x // y
- Prefer,
- /// x # y
- ListAppend,
-}
-
-/// Syntax tree for expressions
-#[derive(Debug, Clone, PartialEq)]
-pub enum Expr<'i, S, A> {
- /// `Const c ~ c`
- Const(Const),
- /// `Var (V x 0) ~ x`<br>
- /// `Var (V x n) ~ x@n`
- Var(V<'i>),
- /// `Lam x A b ~ λ(x : A) -> b`
- Lam(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Pi "_" A B ~ A -> B`
- /// `Pi x A B ~ ∀(x : A) -> B`
- Pi(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `App f A ~ f A`
- App(Box<Expr<'i, S, A>>, Box<Expr<'i, 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(
- &'i str,
- Option<Box<Expr<'i, S, A>>>,
- Box<Expr<'i, S, A>>,
- Box<Expr<'i, S, A>>,
- ),
- /// `Annot x t ~ x : t`
- Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// Built-in values
- Builtin(Builtin),
- // Binary operations
- BinOp(BinOp, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `BoolLit b ~ b`
- BoolLit(bool),
- /// `BoolIf x y z ~ if x then y else z`
- BoolIf(
- Box<Expr<'i, S, A>>,
- Box<Expr<'i, S, A>>,
- Box<Expr<'i, S, A>>,
- ),
- /// `NaturalLit n ~ +n`
- NaturalLit(Natural),
- /// `IntegerLit n ~ n`
- IntegerLit(Integer),
- /// `DoubleLit n ~ n`
- DoubleLit(Double),
- /// `TextLit t ~ t`
- TextLit(Builder),
- /// `ListLit t [x, y, z] ~ [x, y, z] : List t`
- ListLit(Option<Box<Expr<'i, S, A>>>, Vec<Expr<'i, S, A>>),
- /// `OptionalLit t [e] ~ [e] : Optional t`
- /// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(Option<Box<Expr<'i, S, A>>>, Vec<Expr<'i, S, A>>),
- /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
- Record(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
- RecordLit(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >`
- Union(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >`
- UnionLit(
- &'i str,
- Box<Expr<'i, S, A>>,
- BTreeMap<&'i str, Expr<'i, S, A>>,
- ),
- /// `Merge x y t ~ merge x y : t`
- Merge(
- Box<Expr<'i, S, A>>,
- Box<Expr<'i, S, A>>,
- Option<Box<Expr<'i, S, A>>>,
- ),
- /// `Field e x ~ e.x`
- Field(Box<Expr<'i, S, A>>, &'i str),
- /// `Note S x ~ e`
- Note(S, Box<Expr<'i, S, A>>),
- /// `Embed path ~ path`
- Embed(A),
-
- FailedParse(String, Vec<Expr<'i, S, A>>),
-}
-
-/// Built-ins
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum Builtin {
- Bool,
- Natural,
- Integer,
- Double,
- Text,
- List,
- Optional,
- NaturalBuild,
- NaturalFold,
- NaturalIsZero,
- NaturalEven,
- NaturalOdd,
- NaturalToInteger,
- NaturalShow,
- IntegerToDouble,
- IntegerShow,
- DoubleShow,
- ListBuild,
- ListFold,
- ListLength,
- ListHead,
- ListLast,
- ListIndexed,
- ListReverse,
- OptionalFold,
- OptionalBuild,
- TextShow,
-}
-
-impl<'i> From<&'i str> for V<'i> {
- fn from(s: &'i str) -> Self {
- V(s, 0)
- }
-}
-
-impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
- fn from(s: &'i str) -> Self {
- Expr::Var(s.into())
- }
-}
-
-impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
- fn from(t: Builtin) -> Self {
- Expr::Builtin(t)
- }
-}
-
-impl<'i, S, A> Expr<'i, S, A> {
- fn bool_lit(&self) -> Option<bool> {
- match *self {
- Expr::BoolLit(v) => Some(v),
- _ => None,
- }
- }
-
- fn natural_lit(&self) -> Option<usize> {
- match *self {
- Expr::NaturalLit(v) => Some(v),
- _ => None,
- }
- }
-
- fn text_lit(&self) -> Option<String> {
- match *self {
- Expr::TextLit(ref t) => Some(t.clone()), // FIXME?
- _ => None,
- }
- }
-}
-
-// There is a one-to-one correspondence between the formatters in this section
-// and the grammar in grammar.lalrpop. Each formatter is named after the
-// corresponding grammar rule and the relationship between formatters exactly matches
-// the relationship between grammar rules. This leads to the nice emergent property
-// of automatically getting all the parentheses and precedences right.
-//
-// This approach has one major disadvantage: you can get an infinite loop if
-// you add a new constructor to the syntax tree without adding a matching
-// case the corresponding builder.
-
-impl<'i, S, A: Display> Display for Expr<'i, S, A> {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- // buildExprA
- use crate::Expr::*;
- match self {
- &Annot(ref a, ref b) => {
- a.fmt_b(f)?;
- write!(f, " : ")?;
- b.fmt(f)
- }
- &Note(_, ref b) => b.fmt(f),
- a => a.fmt_b(f),
- }
- }
-}
-
-impl<'i, S, A: Display> Expr<'i, S, A> {
- fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Lam(a, ref b, ref c) => {
- write!(f, "λ({} : ", a)?;
- b.fmt(f)?;
- write!(f, ") → ")?;
- c.fmt_b(f)
- }
- &BoolIf(ref a, ref b, ref c) => {
- write!(f, "if ")?;
- a.fmt(f)?;
- write!(f, " then ")?;
- b.fmt_b(f)?;
- write!(f, " else ")?;
- c.fmt_c(f)
- }
- &Pi("_", ref b, ref c) => {
- b.fmt_c(f)?;
- write!(f, " → ")?;
- c.fmt_b(f)
- }
- &Pi(a, ref b, ref c) => {
- write!(f, "∀({} : ", a)?;
- b.fmt(f)?;
- write!(f, ") → ")?;
- c.fmt_b(f)
- }
- &Let(a, None, ref c, ref d) => {
- write!(f, "let {} = ", a)?;
- c.fmt(f)?;
- write!(f, ") → ")?;
- d.fmt_b(f)
- }
- &Let(a, Some(ref b), ref c, ref d) => {
- write!(f, "let {} : ", a)?;
- b.fmt(f)?;
- write!(f, " = ")?;
- c.fmt(f)?;
- write!(f, ") → ")?;
- d.fmt_b(f)
- }
- &ListLit(ref t, ref es) => {
- fmt_list("[", "]", es, f, |e, f| e.fmt(f))?;
- match t {
- Some(t) => {
- write!(f, " : List ")?;
- t.fmt_e(f)?
- }
- None => {}
- }
- Ok(())
- }
- &OptionalLit(ref t, ref es) => {
- fmt_list("[", "]", es, f, |e, f| e.fmt(f))?;
- match t {
- Some(t) => {
- write!(f, " : Optional ")?;
- t.fmt_e(f)?
- }
- None => {}
- }
- Ok(())
- }
- &Merge(ref a, ref b, ref c) => {
- write!(f, "merge ")?;
- a.fmt_e(f)?;
- write!(f, " ")?;
- b.fmt_e(f)?;
- match c {
- Some(c) => {
- write!(f, " : ")?;
- c.fmt_d(f)?
- }
- None => {}
- }
- Ok(())
- }
- &Note(_, ref b) => b.fmt_b(f),
- a => a.fmt_c(f),
- }
- }
-
- fn fmt_c(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::BinOp::*;
- use crate::Expr::*;
- match self {
- // FIXME precedence
- &BinOp(BoolOr, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" || ")?;
- b.fmt_c(f)
- }
- &BinOp(TextAppend, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" ++ ")?;
- b.fmt_c(f)
- }
- &BinOp(NaturalPlus, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" + ")?;
- b.fmt_c(f)
- }
- &BinOp(BoolAnd, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" && ")?;
- b.fmt_c(f)
- }
- &BinOp(Combine, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" ^ ")?;
- b.fmt_c(f)
- }
- &BinOp(NaturalTimes, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" * ")?;
- b.fmt_c(f)
- }
- &BinOp(BoolEQ, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" == ")?;
- b.fmt_c(f)
- }
- &BinOp(BoolNE, ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" != ")?;
- b.fmt_c(f)
- }
- &Note(_, ref b) => b.fmt_c(f),
- a => a.fmt_d(f),
- }
- }
-
- fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &App(ref a, ref b) => {
- a.fmt_d(f)?;
- f.write_str(" ")?;
- b.fmt_e(f)
- }
- &Note(_, ref b) => b.fmt_d(f),
- a => a.fmt_e(f),
- }
- }
-
- fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Field(ref a, b) => {
- a.fmt_e(f)?;
- write!(f, ".{}", b)
- }
- &Note(_, ref b) => b.fmt_e(f),
- a => a.fmt_f(f),
- }
- }
-
- fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Var(a) => a.fmt(f),
- &Const(k) => k.fmt(f),
- &Builtin(v) => v.fmt(f),
- &BoolLit(true) => f.write_str("True"),
- &BoolLit(false) => f.write_str("False"),
- &IntegerLit(a) => a.fmt(f),
- &NaturalLit(a) => {
- f.write_str("+")?;
- a.fmt(f)
- }
- &DoubleLit(a) => a.fmt(f),
- &TextLit(ref a) => <String as fmt::Debug>::fmt(a, f), // FIXME Format with Haskell escapes
- &Record(ref a) if a.is_empty() => f.write_str("{}"),
- &Record(ref a) => fmt_list("{ ", " }", a, f, |(k, t), f| {
- write!(f, "{} : {}", k, t)
- }),
- &RecordLit(ref a) if a.is_empty() => f.write_str("{=}"),
- &RecordLit(ref a) => fmt_list("{ ", " }", a, f, |(k, v), f| {
- write!(f, "{} = {}", k, v)
- }),
- &Union(ref _a) => f.write_str("Union"),
- &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"),
- &Embed(ref a) => a.fmt(f),
- &Note(_, ref b) => b.fmt_f(f),
- a => write!(f, "({})", a),
- }
- }
-}
-
-fn fmt_list<T, I, F>(
- open: &str,
- close: &str,
- it: I,
- f: &mut fmt::Formatter,
- func: F,
-) -> Result<(), fmt::Error>
-where
- I: IntoIterator<Item = T>,
- F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>,
-{
- f.write_str(open)?;
- for (i, x) in it.into_iter().enumerate() {
- if i > 0 {
- f.write_str(", ")?;
- }
- func(x, f)?;
- }
- f.write_str(close)
-}
-
-impl Display for Const {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- <Self as fmt::Debug>::fmt(self, f)
- }
-}
-
-impl Display for Builtin {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Builtin::*;
- f.write_str(match *self {
- Bool => "Bool",
- Natural => "Natural",
- Integer => "Integer",
- Double => "Double",
- Text => "Text",
- List => "List",
- Optional => "Optional",
- NaturalBuild => "Natural/build",
- NaturalFold => "Natural/fold",
- NaturalIsZero => "Natural/isZero",
- NaturalEven => "Natural/even",
- NaturalOdd => "Natural/odd",
- NaturalToInteger => "Natural/toInteger",
- NaturalShow => "Natural/show",
- IntegerToDouble => "Integer/toDouble",
- IntegerShow => "Integer/show",
- DoubleShow => "Double/show",
- ListBuild => "List/build",
- ListFold => "List/fold",
- ListLength => "List/length",
- ListHead => "List/head",
- ListLast => "List/last",
- ListIndexed => "List/indexed",
- ListReverse => "List/reverse",
- OptionalFold => "Optional/fold",
- OptionalBuild => "Optional/build",
- TextShow => "Text/show",
- })
- }
-}
-
-impl Builtin {
- pub fn parse(s: &str) -> Option<Self> {
- use self::Builtin::*;
- match s {
- "Bool" => Some(Bool),
- "Natural" => Some(Natural),
- "Integer" => Some(Integer),
- "Double" => Some(Double),
- "Text" => Some(Text),
- "List" => Some(List),
- "Optional" => Some(Optional),
- "Natural/build" => Some(NaturalBuild),
- "Natural/fold" => Some(NaturalFold),
- "Natural/isZero" => Some(NaturalIsZero),
- "Natural/even" => Some(NaturalEven),
- "Natural/odd" => Some(NaturalOdd),
- "Natural/toInteger" => Some(NaturalToInteger),
- "Natural/show" => Some(NaturalShow),
- "Integer/toDouble" => Some(IntegerToDouble),
- "Integer/show" => Some(IntegerShow),
- "Double/show" => Some(DoubleShow),
- "List/build" => Some(ListBuild),
- "List/fold" => Some(ListFold),
- "List/length" => Some(ListLength),
- "List/head" => Some(ListHead),
- "List/last" => Some(ListLast),
- "List/indexed" => Some(ListIndexed),
- "List/reverse" => Some(ListReverse),
- "Optional/fold" => Some(OptionalFold),
- "Optional/build" => Some(OptionalBuild),
- "Text/show" => Some(TextShow),
- _ => None,
- }
- }
-}
-
-impl<'i> Display for V<'i> {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- let V(x, n) = *self;
- f.write_str(x)?;
- if n != 0 {
- write!(f, "@{}", n)?;
- }
- Ok(())
- }
-}
-
-pub fn pi<'i, S, A, Name, Et, Ev>(
- var: Name,
- ty: Et,
- value: Ev,
-) -> Expr<'i, S, A>
-where
- Name: Into<&'i str>,
- Et: Into<Expr<'i, S, A>>,
- Ev: Into<Expr<'i, S, A>>,
-{
- Expr::Pi(var.into(), bx(ty.into()), bx(value.into()))
-}
-
-pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A>
-where
- Ef: Into<Expr<'i, S, A>>,
- Ex: Into<Expr<'i, S, A>>,
-{
- Expr::App(bx(f.into()), bx(x.into()))
-}
-
-pub type Builder = String;
-pub type Double = f64;
-pub type Int = isize;
-pub type Integer = isize;
-pub type Natural = usize;
-
-/// A void type
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum X {}
-
-impl Display for X {
- fn fmt(&self, _: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- match *self {}
- }
-}
-
-pub fn bx<T>(x: T) -> Box<T> {
- Box::new(x)
-}
-
-fn add_ui(u: usize, i: isize) -> usize {
- if i < 0 {
- u.checked_sub(i.checked_neg().unwrap() as usize).unwrap()
- } else {
- u.checked_add(i as usize).unwrap()
- }
-}
-
-fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
-where
- I: IntoIterator<Item = (&'a K, &'a V)>,
- K: Eq + Ord + Copy + 'a,
- V: 'a,
- F: Fn(&V) -> U,
-{
- it.into_iter().map(|(&k, v)| (k, f(v))).collect()
-}
-
-fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V
-where
- F: FnOnce(U, U) -> V,
- G: Fn(T) -> U,
-{
- f(g(a), g(b))
-}
-
-/// `shift` is used by both normalization and type-checking to avoid variable
-/// capture by shifting variable indices
-///
-/// For example, suppose that you were to normalize the following expression:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
-/// ```
-///
-/// If you were to substitute `y` with `x` without shifting any variable
-/// indices, then you would get the following incorrect result:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form
-/// ```
-///
-/// In order to substitute `x` in place of `y` we need to `shift` `x` by `1` in
-/// order to avoid being misinterpreted as the `x` bound by the innermost
-/// lambda. If we perform that `shift` then we get the correct result:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → λ(x : a) → x@1
-/// ```
-///
-/// As a more worked example, suppose that you were to normalize the following
-/// expression:
-///
-/// ```c
-/// λ(a : Type)
-/// → λ(f : a → a → a)
-/// → λ(x : a)
-/// → λ(x : a)
-/// → (λ(x : a) → f x x@1) x@1
-/// ```
-///
-/// The correct normalized result would be:
-///
-/// ```c
-/// λ(a : Type)
-/// → λ(f : a → a → a)
-/// → λ(x : a)
-/// → λ(x : a)
-/// → f x@1 x
-/// ```
-///
-/// The above example illustrates how we need to both increase and decrease
-/// variable indices as part of substitution:
-///
-/// * We need to increase the index of the outer `x\@1` to `x\@2` before we
-/// substitute it into the body of the innermost lambda expression in order
-/// to avoid variable capture. This substitution changes the body of the
-/// lambda expression to `(f x\@2 x\@1)`
-///
-/// * We then remove the innermost lambda and therefore decrease the indices of
-/// both `x`s in `(f x\@2 x\@1)` to `(f x\@1 x)` in order to reflect that one
-/// less `x` variable is now bound within that scope
-///
-/// Formally, `(shift d (V x n) e)` modifies the expression `e` by adding `d` to
-/// the indices of all variables named `x` whose indices are greater than
-/// `(n + m)`, where `m` is the number of bound variables of the same name
-/// within that scope
-///
-/// In practice, `d` is always `1` or `-1` because we either:
-///
-/// * increment variables by `1` to avoid variable capture during substitution
-/// * decrement variables by `1` when deleting lambdas after substitution
-///
-/// `n` starts off at `0` when substitution begins and increments every time we
-/// descend into a lambda or let expression that binds a variable of the same
-/// name in order to avoid shifting the bound variables by mistake.
-///
-pub fn shift<'i, S, T, A: Clone>(
- d: isize,
- v: V,
- e: &Expr<'i, S, A>,
-) -> Expr<'i, T, A> {
- use crate::Expr::*;
- let V(x, n) = v;
- match *e {
- Const(a) => Const(a),
- Var(V(x2, n2)) => {
- let n3 = if x == x2 && n <= n2 {
- add_ui(n2, d)
- } else {
- n2
- };
- Var(V(x2, n3))
- }
- Lam(x2, ref tA, ref b) => {
- let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x, n), tA);
- let b2 = shift(d, V(x, n2), b);
- Lam(x2, bx(tA2), bx(b2))
- }
- Pi(x2, ref tA, ref tB) => {
- let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x, n), tA);
- let tB2 = shift(d, V(x, n2), tB);
- pi(x2, tA2, tB2)
- }
- App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)),
- Let(f, ref mt, ref r, ref e) => {
- let n2 = if x == f { n + 1 } else { n };
- let e2 = shift(d, V(x, n2), e);
- let mt2 = mt.as_ref().map(|t| bx(shift(d, V(x, n), t)));
- let r2 = shift(d, V(x, n), r);
- Let(f, mt2, bx(r2), bx(e2))
- }
- Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b),
- Builtin(v) => Builtin(v),
- BoolLit(a) => BoolLit(a),
- BinOp(o, ref a, ref b) => shift_op2(|x, y| BinOp(o, x, y), d, v, a, b),
- BoolIf(ref a, ref b, ref c) => {
- BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
- }
- NaturalLit(a) => NaturalLit(a),
- IntegerLit(a) => IntegerLit(a),
- DoubleLit(a) => DoubleLit(a),
- TextLit(ref a) => TextLit(a.clone()),
- ListLit(ref t, ref es) => ListLit(
- t.as_ref().map(|t| bx(shift(d, v, t))),
- es.iter().map(|e| shift(d, v, e)).collect(),
- ),
- OptionalLit(ref t, ref es) => OptionalLit(
- t.as_ref().map(|t| bx(shift(d, v, t))),
- es.iter().map(|e| shift(d, v, e)).collect(),
- ),
- Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))),
- RecordLit(ref a) => {
- RecordLit(map_record_value(a, |val| shift(d, v, val)))
- }
- Union(ref a) => Union(map_record_value(a, |val| shift(d, v, val))),
- UnionLit(k, ref uv, ref a) => UnionLit(
- k,
- bx(shift(d, v, uv)),
- map_record_value(a, |val| shift(d, v, val)),
- ),
- Merge(ref a, ref b, ref c) => Merge(
- bx(shift(d, v, a)),
- bx(shift(d, v, b)),
- c.as_ref().map(|c| bx(shift(d, v, c))),
- ),
- Field(ref a, b) => Field(bx(shift(d, v, a)), b),
- Note(_, ref b) => shift(d, v, b),
- // The Dhall compiler enforces that all embedded values are closed expressions
- // and `shift` does nothing to a closed expression
- Embed(ref p) => Embed(p.clone()),
- _ => panic!(),
- }
-}
-
-fn shift_op2<'i, S, T, A, F>(
- f: F,
- d: isize,
- v: V,
- a: &Expr<'i, S, A>,
- b: &Expr<'i, S, A>,
-) -> Expr<'i, T, A>
-where
- F: FnOnce(Box<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> Expr<'i, T, A>,
- A: Clone,
-{
- map_op2(f, |x| bx(shift(d, v, x)), a, b)
-}
-
-/// Substitute all occurrences of a variable with an expression
-///
-/// ```c
-/// subst x C B ~ B[x := C]
-/// ```
-///
-pub fn subst<'i, S, T, A>(
- v: V<'i>,
- e: &Expr<'i, S, A>,
- b: &Expr<'i, T, A>,
-) -> Expr<'i, S, A>
-where
- S: Clone,
- A: Clone,
-{
- use crate::Expr::*;
- let V(x, n) = v;
- match *b {
- Const(a) => Const(a),
- Lam(y, ref tA, ref b) => {
- let n2 = if x == y { n + 1 } else { n };
- let b2 = subst(V(x, n2), &shift(1, V(y, 0), e), b);
- let tA2 = subst(V(x, n), e, tA);
- Lam(y, bx(tA2), bx(b2))
- }
- Pi(y, ref tA, ref tB) => {
- let n2 = if x == y { n + 1 } else { n };
- let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB);
- let tA2 = subst(V(x, n), e, tA);
- pi(y, tA2, tB2)
- }
- App(ref f, ref a) => {
- let f2 = subst(v, e, f);
- let a2 = subst(v, e, a);
- app(f2, a2)
- }
- Var(v2) => {
- if v == v2 {
- e.clone()
- } else {
- Var(v2)
- }
- }
- Let(f, ref mt, ref r, ref b) => {
- let n2 = if x == f { n + 1 } else { n };
- let b2 = subst(V(x, n2), &shift(1, V(f, 0), e), b);
- let mt2 = mt.as_ref().map(|t| bx(subst(V(x, n), e, t)));
- let r2 = subst(V(x, n), e, r);
- Let(f, mt2, bx(r2), bx(b2))
- }
- Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b),
- Builtin(v) => Builtin(v),
- BoolLit(a) => BoolLit(a),
- BinOp(o, ref a, ref b) => subst_op2(|x, y| BinOp(o, x, y), v, e, a, b),
- BoolIf(ref a, ref b, ref c) => {
- BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
- }
- NaturalLit(a) => NaturalLit(a),
- IntegerLit(a) => IntegerLit(a),
- DoubleLit(a) => DoubleLit(a),
- TextLit(ref a) => TextLit(a.clone()),
- ListLit(ref a, ref b) => {
- let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
- let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- ListLit(a2, b2)
- }
- OptionalLit(ref a, ref b) => {
- let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
- let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- OptionalLit(a2, b2)
- }
- Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))),
- RecordLit(ref kvs) => {
- RecordLit(map_record_value(kvs, |val| subst(v, e, val)))
- }
- Union(ref kts) => Union(map_record_value(kts, |t| subst(v, e, t))),
- UnionLit(k, ref uv, ref kvs) => UnionLit(
- k,
- bx(subst(v, e, uv)),
- map_record_value(kvs, |val| subst(v, e, val)),
- ),
- Merge(ref a, ref b, ref c) => Merge(
- bx(subst(v, e, a)),
- bx(subst(v, e, b)),
- c.as_ref().map(|c| bx(subst(v, e, c))),
- ),
- Field(ref a, b) => Field(bx(subst(v, e, a)), b),
- Note(_, ref b) => subst(v, e, b),
- Embed(ref p) => Embed(p.clone()),
- _ => panic!(),
- }
-}
-
-fn subst_op2<'i, S, T, A, F>(
- f: F,
- v: V<'i>,
- e: &Expr<'i, S, A>,
- a: &Expr<'i, T, A>,
- b: &Expr<'i, T, A>,
-) -> Expr<'i, S, A>
-where
- F: FnOnce(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> Expr<'i, S, A>,
- S: Clone,
- A: Clone,
-{
- map_op2(f, |x| bx(subst(v, e, x)), a, b)
-}
-
-/// Reduce an expression to its normal form, performing beta reduction
-///
-/// `normalize` does not type-check the expression. You may want to type-check
-/// expressions before normalizing them since normalization can convert an
-/// ill-typed expression into a well-typed expression.
-///
-/// However, `normalize` will not fail if the expression is ill-typed and will
-/// leave ill-typed sub-expressions unevaluated.
-///
-pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
-where
- S: Clone + fmt::Debug,
- T: Clone + fmt::Debug,
- A: Clone + fmt::Debug,
-{
- use crate::BinOp::*;
- use crate::Builtin::*;
- use crate::Expr::*;
- match *e {
- Const(k) => Const(k),
- Var(v) => Var(v),
- Lam(x, ref tA, ref b) => {
- let tA2 = normalize(tA);
- let b2 = normalize(b);
- Lam(x, bx(tA2), bx(b2))
- }
- Pi(x, ref tA, ref tB) => {
- let tA2 = normalize(tA);
- let tB2 = normalize(tB);
- pi(x, tA2, tB2)
- }
- App(ref f, ref a) => match normalize::<S, T, A>(f) {
- Lam(x, _A, b) => {
- // Beta reduce
- let vx0 = V(x, 0);
- let a2 = shift::<S, S, A>(1, vx0, a);
- let b2 = subst::<S, T, A>(vx0, &a2, &b);
- let b3 = shift::<S, T, A>(-1, vx0, &b2);
- normalize(&b3)
- }
- f2 => match (f2, normalize::<S, T, A>(a)) {
- // fold/build fusion for `List`
- (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
- (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
-
- // fold/build fusion for `Natural`
- (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) |
- (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2),
-
- /*
- App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
- normalize (go n0)
- where
- go !0 = zero
- go !n = App succ' (go (n - 1))
- App NaturalBuild k
- | check -> NaturalLit n
- | otherwise -> App f' a'
- where
- labeled =
- normalize (App (App (App k Natural) "Succ") "Zero")
-
- n = go 0 labeled
- where
- go !m (App (Var "Succ") e') = go (m + 1) e'
- go !m (Var "Zero") = m
- go !_ _ = internalError text
- check = go labeled
- where
- go (App (Var "Succ") e') = go e'
- go (Var "Zero") = True
- go _ = False
- */
- (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
- (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
- (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
- (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
- (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
- (App(f@box Builtin(ListBuild), box t), k) => {
- let labeled =
- normalize::<_, T, _>(&app(app(app(k.clone(), app(
- Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil"));
-
- fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
- where S: Clone, A: Clone
- {
- match e {
- App(box App(box Var(V("Cons", _)), box x), box e2) => {
- v.push(x);
- list_to_vector(v, e2)
- }
- Var(V("Nil", _)) => {}
- _ => panic!("internalError list_to_vector"),
- }
- }
- fn check<S, A>(e: &Expr<S, A>) -> bool {
- match *e {
- App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2),
- Var(V("Nil", _)) => true,
- _ => false,
- }
- }
-
- if check(&labeled) {
- let mut v = vec![];
- list_to_vector(&mut v, labeled);
- ListLit(Some(bx(t)), v)
- } else {
- app(App(f, bx(t)), k)
- }
- }
- (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
- let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
- App(bx(App(cons.clone(), bx(y))), bx(ys))
- );
- normalize(&e2)
- }
- (App(f, x_), ListLit(t, ys)) => match *f {
- Builtin(ListLength) =>
- NaturalLit(ys.len()),
- Builtin(ListHead) =>
- normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
- Builtin(ListLast) =>
- normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
- Builtin(ListReverse) => {
- let mut xs = ys;
- xs.reverse();
- normalize(&ListLit(t, xs))
- }
- _ => app(App(f, x_), ListLit(t, ys)),
- },
- /*
- App (App ListIndexed _) (ListLit t xs) ->
- normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
- where
- t' = Record (Data.Map.fromList kts)
- where
- kts = [ ("index", Natural)
- , ("value", t)
- ]
- adapt (n, x) = RecordLit (Data.Map.fromList kvs)
- where
- kvs = [ ("index", NaturalLit (fromIntegral n))
- , ("value", x)
- ]
- */
- (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
- let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _|
- App(just.clone(), bx(y))
- );
- normalize(&e2)
- }
- (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => {
- normalize(&b)
- }
- (App(box Builtin(OptionalBuild), a0), g) => {
- let e2: Expr<_, _> = app(app(app(g,
- App(bx(Builtin(Optional)), a0.clone())),
- Lam("x", a0.clone(),
- bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))),
- OptionalLit(Some(a0), vec![]));
- normalize(&e2)
- }
- (f2, a2) => app(f2, a2),
- },
- },
- Let(f, _, ref r, ref b) => {
- let r2 = shift::<_, S, _>(1, V(f, 0), r);
- let b2 = subst(V(f, 0), &r2, b);
- let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
- normalize(&b3)
- }
- Annot(ref x, _) => normalize(x),
- Builtin(v) => Builtin(v),
- BoolLit(b) => BoolLit(b),
- BinOp(BoolAnd, ref x, ref y) => with_binop(
- BoolAnd,
- Expr::bool_lit,
- |xn, yn| BoolLit(xn && yn),
- normalize(x),
- normalize(y),
- ),
- BinOp(BoolOr, ref x, ref y) => with_binop(
- BoolOr,
- Expr::bool_lit,
- |xn, yn| BoolLit(xn || yn),
- normalize(x),
- normalize(y),
- ),
- BinOp(BoolEQ, ref x, ref y) => with_binop(
- BoolEQ,
- Expr::bool_lit,
- |xn, yn| BoolLit(xn == yn),
- normalize(x),
- normalize(y),
- ),
- BinOp(BoolNE, ref x, ref y) => with_binop(
- BoolNE,
- Expr::bool_lit,
- |xn, yn| BoolLit(xn != yn),
- normalize(x),
- normalize(y),
- ),
- BoolIf(ref b, ref t, ref f) => match normalize(b) {
- BoolLit(true) => normalize(t),
- BoolLit(false) => normalize(f),
- b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))),
- },
- NaturalLit(n) => NaturalLit(n),
- BinOp(NaturalPlus, ref x, ref y) => with_binop(
- NaturalPlus,
- Expr::natural_lit,
- |xn, yn| NaturalLit(xn + yn),
- normalize(x),
- normalize(y),
- ),
- BinOp(NaturalTimes, ref x, ref y) => with_binop(
- NaturalTimes,
- Expr::natural_lit,
- |xn, yn| NaturalLit(xn * yn),
- normalize(x),
- normalize(y),
- ),
- IntegerLit(n) => IntegerLit(n),
- DoubleLit(n) => DoubleLit(n),
- TextLit(ref t) => TextLit(t.clone()),
- BinOp(TextAppend, ref x, ref y) => with_binop(
- TextAppend,
- Expr::text_lit,
- |xt, yt| TextLit(xt + &yt),
- normalize(x),
- normalize(y),
- ),
- ListLit(ref t, ref es) => {
- let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
- let es2 = es.iter().map(normalize).collect();
- ListLit(t2, es2)
- }
- OptionalLit(ref t, ref es) => {
- let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
- let es2 = es.iter().map(normalize).collect();
- OptionalLit(t2, es2)
- }
- Record(ref kts) => Record(map_record_value(kts, normalize)),
- RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
- Union(ref kts) => Union(map_record_value(kts, normalize)),
- UnionLit(k, ref v, ref kvs) => {
- UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize))
- }
- Merge(ref _x, ref _y, ref _t) => unimplemented!(),
- Field(ref r, x) => match normalize(r) {
- RecordLit(kvs) => match kvs.get(x) {
- Some(r2) => normalize(r2),
- None => {
- Field(bx(RecordLit(map_record_value(&kvs, normalize))), x)
- }
- },
- r2 => Field(bx(r2), x),
- },
- Note(_, ref e) => normalize(e),
- Embed(ref a) => Embed(a.clone()),
- _ => unimplemented!(),
- }
-}
-
-fn with_binop<'a, S, A, U, Get, Set>(
- op: BinOp,
- get: Get,
- set: Set,
- x: Expr<'a, S, A>,
- y: Expr<'a, S, A>,
-) -> Expr<'a, S, A>
-where
- Get: Fn(&Expr<'a, S, A>) -> Option<U>,
- Set: FnOnce(U, U) -> Expr<'a, S, A>,
-{
- if let (Some(xv), Some(yv)) = (get(&x), get(&y)) {
- set(xv, yv)
- } else {
- Expr::BinOp(op, bx(x), bx(y))
- }
-}
diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop
deleted file mode 100644
index 1ffe2ff..0000000
--- a/dhall/src/grammar.lalrpop
+++ /dev/null
@@ -1,164 +0,0 @@
-use std::collections::BTreeMap;
-use std::iter;
-use std::iter::FromIterator;
-
-use crate::core;
-use crate::core::bx;
-use crate::core::Expr::*;
-use crate::core::Builtin;
-use crate::core::Builtin::*;
-use crate::core::BinOp::*;
-use crate::grammar_util::*;
-use crate::lexer::*;
-
-grammar<'input>;
-
-extern {
- type Location = usize;
- type Error = LexicalError;
-
- enum Tok<'input> {
- Pi => Tok::Pi,
- Lambda => Tok::Lambda,
- Combine => Tok::Combine,
- "->" => Tok::Arrow,
-
- Int => Tok::Integer(<isize>),
- Nat => Tok::Natural(<usize>),
- Text => Tok::Text(<String>),
- Bool => Tok::Bool(<bool>),
- Label => Tok::Identifier(<&'input str>),
- Const => Tok::Const(<core::Const>),
- Let => Tok::Keyword(Keyword::Let),
- In => Tok::Keyword(Keyword::In),
- If => Tok::Keyword(Keyword::If),
- Then => Tok::Keyword(Keyword::Then),
- Else => Tok::Keyword(Keyword::Else),
- List => Tok::ListLike(ListLike::List),
- Optional => Tok::ListLike(ListLike::Optional),
- Builtin => Tok::Builtin(<Builtin>),
-
- "{" => Tok::BraceL,
- "}" => Tok::BraceR,
- "[" => Tok::BracketL,
- "]" => Tok::BracketR,
- "(" => Tok::ParenL,
- ")" => Tok::ParenR,
- "&&" => Tok::BoolAnd,
- "||" => Tok::BoolOr,
- "==" => Tok::CompareEQ,
- "!=" => Tok::CompareNE,
- "++" => Tok::Append,
- "*" => Tok::Times,
- "+" => Tok::Plus,
- "," => Tok::Comma,
- "." => Tok::Dot,
- ":" => Tok::Ascription,
- "=" => Tok::Equals,
- }
-}
-
-pub Expr: BoxExpr<'input> = { // exprA
- ExprB,
-};
-
-ExprB: BoxExpr<'input> = {
- Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
- Pi "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Pi(<>)),
- If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
- <ExprC> "->" <ExprB> => bx(Pi("_", <>)),
- Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
- "[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(Some(c), a)),
- <ExprC> ":" <Expr> => bx(Annot(<>)),
- ExprC,
-};
-
-ListLike: ExprListFn<'input> = {
- List => ListLit,
- Optional => OptionalLit,
-};
-
-BoolOr: ExprOpFn<'input> = { "||" => (|x,y| BinOp(BoolOr, x, y)) };
-NaturalPlus: ExprOpFn<'input> = { "+" => (|x,y| BinOp(NaturalPlus, x, y)) };
-TextAppend: ExprOpFn<'input> = { "++" => (|x,y| BinOp(TextAppend, x, y)) };
-BoolAnd: ExprOpFn<'input> = { "&&" => (|x,y| BinOp(BoolAnd, x, y)) };
-CombineOp: ExprOpFn<'input> = { Combine => (|x,y| BinOp(Combine, x, y)) };
-NaturalTimes: ExprOpFn<'input> = { "*" => (|x,y| BinOp(NaturalTimes, x, y)) };
-BoolEQ: ExprOpFn<'input> = { "==" => (|x,y| BinOp(BoolEQ, x, y)) };
-BoolNE: ExprOpFn<'input> = { "!=" => (|x,y| BinOp(BoolNE, x, y)) };
-
-Tier<NextTier, Op>: BoxExpr<'input> = {
- <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,
-};
-
-ExprC = 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<'input> = {
- <v:(ExprE)+> => {
- let mut it = v.into_iter();
- let f = it.next().unwrap();
- it.fold(f, |f, x| bx(App(f, x)))
- }
-};
-
-ExprE: BoxExpr<'input> = {
- <a:ExprF> <fields:("." <Label>)*> => {
- fields.into_iter().fold(a, |x, f| bx(Field(x, f)))
- },
-};
-
-ExprF: BoxExpr<'input> = {
- Nat => bx(NaturalLit(<>)),
- Int => bx(IntegerLit(<>)),
- Text => bx(TextLit(<>)),
- Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
- Const => bx(Const(<>)),
- List => bx(Builtin(List)),
- Optional => bx(Builtin(Optional)),
- Builtin => bx(Builtin(<>)),
- Bool => bx(BoolLit(<>)),
- Record,
- RecordLit,
- "(" <Expr> ")",
-};
-
-SepBy<S, T>: iter::Chain<::std::vec::IntoIter<T>, ::std::option::IntoIter<T>> = {
- <v:(<T> S)*> <last:T?> => v.into_iter().chain(last.into_iter()),
-};
-
-SepBy1<S, T>: iter::Chain<::std::vec::IntoIter<T>, iter::Once<T>> = {
- <v:(<T> S)*> <last:T> => v.into_iter().chain(iter::once(last)),
-};
-
-Elems: Vec<ParsedExpr<'input>> = {
- <v:SepBy<",", Expr>> => {
- v.into_iter()
- .map(|b| *b)
- .collect::<Vec<_>>()
- }
-};
-
-RecordLit: BoxExpr<'input> = {
- "{" "=" "}" => bx(RecordLit(BTreeMap::new())),
- "{" <FieldValues> "}" => bx(RecordLit(BTreeMap::from_iter(<>))),
-};
-
-Record: BoxExpr<'input> = {
- "{" <FieldTypes> "}" => bx(Record(BTreeMap::from_iter(<>))),
-};
-
-FieldValues = SepBy1<",", Field<"=">>;
-FieldTypes = SepBy<",", Field<":">>;
-
-Field<Sep>: (&'input str, ParsedExpr<'input>) = {
- <a:Label> Sep <b:Expr> => (a, *b),
-};
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
deleted file mode 100644
index ce73444..0000000
--- a/dhall/src/grammar_util.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-use crate::core::{Expr, X};
-
-pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
-pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
-pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
-pub type ExprListFn<'i> =
- fn(Option<BoxExpr<'i>>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
deleted file mode 100644
index 5fc0f05..0000000
--- a/dhall/src/lexer.rs
+++ /dev/null
@@ -1,394 +0,0 @@
-use nom::*;
-
-use crate::core::Builtin;
-use crate::core::Builtin::*;
-use crate::core::Const;
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Keyword {
- Let,
- In,
- If,
- Then,
- Else,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ListLike {
- List,
- Optional,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Tok<'i> {
- Identifier(&'i str),
- Keyword(Keyword),
- Builtin(Builtin),
- ListLike(ListLike),
- Const(Const),
- Bool(bool),
- Integer(isize),
- Natural(usize),
- Text(String),
-
- // Symbols
- BraceL,
- BraceR,
- BracketL,
- BracketR,
- ParenL,
- ParenR,
- Arrow,
- Lambda,
- Pi,
- Combine,
- BoolAnd,
- BoolOr,
- CompareEQ,
- CompareNE,
- Append,
- Times,
- Plus,
- Comma,
- Dot,
- Ascription,
- Equals,
-}
-
-#[derive(Debug)]
-pub enum LexicalError {
- Error(usize, nom::simple_errors::Err<u32>),
- Incomplete(nom::Needed),
-}
-
-pub type Spanned<Tok, Loc, Error> = Result<(Loc, Tok, Loc), Error>;
-
-#[allow(dead_code)]
-fn is_identifier_first_char(c: char) -> bool {
- c.is_alphabetic() || c == '_'
-}
-
-fn is_identifier_rest_char(c: char) -> bool {
- is_identifier_first_char(c) || c.is_digit(10) || c == '/'
-}
-
-macro_rules! digits {
- ($i:expr, $t:tt, $radix:expr) => {{
- let r: nom::IResult<&str, $t> = map_res!(
- $i,
- take_while1_s!(call!(|c: char| c.is_digit($radix))),
- |s| $t::from_str_radix(s, $radix)
- );
- r
- }};
-}
-
-named!(natural<&str, usize>, digits!(usize, 10));
-named!(integral<&str, isize>, digits!(isize, 10));
-named!(integer<&str, isize>, alt!(
- preceded!(tag!("-"), map!(integral, |i: isize| -i)) |
- preceded!(tag!("+"), integral)
-));
-named!(boolean<&str, bool>, alt!(
- value!(true, tag!("True")) |
- value!(false, tag!("False"))
-));
-
-named!(identifier<&str, &str>, recognize!(preceded!(
- take_while1_s!(is_identifier_first_char),
- take_while_s!(is_identifier_rest_char))
-));
-
-/// Parse an identifier, ensuring a whole identifier is parsed and not just a prefix.
-macro_rules! ident_tag {
- ($i:expr, $tag:expr) => {
- match identifier($i) {
- nom::IResult::Done(i, s) => {
- if s == $tag {
- nom::IResult::Done(i, s)
- } else {
- nom::IResult::Error(error_position!(
- nom::ErrorKind::Tag,
- $i
- ))
- }
- }
- r => r,
- }
- };
-}
-
-fn string_escape_single(c: char) -> Option<&'static str> {
- match c {
- 'n' => Some("\n"),
- 'r' => Some("\r"),
- 't' => Some("\t"),
- '"' => Some("\""),
- '\'' => Some("'"),
- '\\' => Some("\\"),
- '0' => Some("\0"),
- 'a' => Some("\x07"),
- 'b' => Some("\x08"),
- 'f' => Some("\x0c"),
- 'v' => Some("\x0b"),
- '&' => Some(""),
- _ => None,
- }
-}
-
-named!(string_escape_numeric<&str, char>, map_opt!(alt!(
- preceded!(tag!("x"), digits!(u32, 16)) |
- preceded!(tag!("o"), digits!(u32, 8)) |
- digits!(u32, 10)
-), ::std::char::from_u32));
-
-fn string_lit_inner(input: &str) -> nom::IResult<&str, String> {
- use nom::ErrorKind;
- use nom::IResult::*; ;
- let mut s = String::new();
- let mut cs = input.char_indices().peekable();
- while let Some((i, c)) = cs.next() {
- match c {
- '"' => return nom::IResult::Done(&input[i..], s),
- '\\' => match cs.next() {
- Some((_, s)) if s.is_whitespace() => {
- while cs.peek().map(|&(_, s)| s.is_whitespace())
- == Some(true)
- {
- let _ = cs.next();
- }
- if cs.next().map(|p| p.1) != Some('\\') {
- return Error(error_position!(
- ErrorKind::Custom(4 /* FIXME */),
- input
- ));
- }
- }
- Some((j, ec)) => {
- if let Some(esc) = string_escape_single(ec) {
- s.push_str(esc);
- // FIXME Named ASCII escapes and control character escapes
- } else {
- match string_escape_numeric(&input[j..]) {
- Done(rest, esc) => {
- let &(k, _) = cs.peek().unwrap();
- // digits are always single byte ASCII characters
- let consumed = input[k..].len() - rest.len();
- for _ in 0..consumed {
- let _ = cs.next();
- }
- s.push(esc);
- }
- Incomplete(s) => return Incomplete(s),
- Error(e) => return Error(e),
- }
- }
- }
- _ => {
- return Error(error_position!(
- ErrorKind::Custom(5 /* FIXME */),
- input
- ));
- }
- },
- _ => s.push(c),
- }
- }
- Error(error_position!(ErrorKind::Custom(3 /* FIXME */), input))
-}
-
-named!(string_lit<&str, String>, delimited!(tag!("\""), string_lit_inner, tag!("\"")));
-
-named!(keyword<&str, Keyword>, alt!(
- value!(Keyword::Let, ident_tag!("let")) |
- value!(Keyword::In, ident_tag!("in")) |
- value!(Keyword::If, ident_tag!("if")) |
- value!(Keyword::Then, ident_tag!("then")) |
- value!(Keyword::Else, ident_tag!("else"))
-));
-
-named!(type_const<&str, Const>, alt!(
- value!(Const::Type, ident_tag!("Type")) |
- value!(Const::Kind, ident_tag!("Kind"))
-));
-
-named!(list_like<&str, ListLike>, alt!(
- value!(ListLike::List, ident_tag!("List")) |
- value!(ListLike::Optional, ident_tag!("Optional"))
-));
-
-named!(builtin<&str, Builtin>, alt!(
- value!(NaturalFold, ident_tag!("Natural/fold")) |
- value!(NaturalBuild, ident_tag!("Natural/build")) |
- value!(NaturalIsZero, ident_tag!("Natural/isZero")) |
- value!(NaturalEven, ident_tag!("Natural/even")) |
- value!(NaturalOdd, ident_tag!("Natural/odd")) |
- value!(NaturalShow, ident_tag!("Natural/show")) |
- value!(Natural, ident_tag!("Natural")) |
- value!(Integer, ident_tag!("Integer")) |
- value!(Double, ident_tag!("Double")) |
- value!(Text, ident_tag!("Text")) |
- value!(ListBuild, ident_tag!("List/build")) |
- value!(ListFold, ident_tag!("List/fold")) |
- value!(ListLength, ident_tag!("List/length")) |
- value!(ListHead, ident_tag!("List/head")) |
- value!(ListLast, ident_tag!("List/last")) |
- value!(ListIndexed, ident_tag!("List/indexed")) |
- value!(ListReverse, ident_tag!("List/reverse")) |
- value!(OptionalFold, ident_tag!("Optional/fold")) |
- value!(Bool, ident_tag!("Bool"))
-));
-
-named!(token<&str, Tok>, alt!(
- value!(Tok::Pi, ident_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!(type_const, Tok::Const) |
- map!(boolean, Tok::Bool) |
- map!(keyword, Tok::Keyword) |
- map!(builtin, Tok::Builtin) |
- map!(list_like, Tok::ListLike) |
- map!(natural, Tok::Natural) |
- map!(integer, Tok::Integer) |
- map!(identifier, Tok::Identifier) |
- map!(string_lit, Tok::Text) |
-
- value!(Tok::BraceL, tag!("{")) |
- value!(Tok::BraceR, tag!("}")) |
- value!(Tok::BracketL, tag!("[")) |
- value!(Tok::BracketR, tag!("]")) |
- 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::Comma, tag!(",")) |
- value!(Tok::Dot, tag!(".")) |
- value!(Tok::Ascription, tag!(":")) |
- value!(Tok::Equals, tag!("="))
-));
-
-fn find_end(input: &str, ending: &str) -> Option<usize> {
- input.find(ending).map(|i| i + ending.len())
-}
-
-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) -> bool {
- let input = self.current_input();
- let trimmed = input.trim_start();
- let whitespace_len = input.len() - trimmed.len();
- let skipped = whitespace_len > 0;
- if skipped {
- // println!("skipped {} whitespace bytes in {}..{}", whitespace_len, self.offset, self.offset + whitespace_len);
- self.offset += whitespace_len;
- }
- skipped
- }
-
- fn skip_comments(&mut self) -> bool {
- let input = self.current_input();
- if !input.is_char_boundary(0) || !input.is_char_boundary(2) {
- return false;
- }
- let skip = match &input[0..2] {
- "{-" => find_end(input, "-}"),
- "--" => find_end(input, "\n"), // Also skips past \r\n (CRLF)
- _ => None,
- }
- .unwrap_or(0);
- // println!("skipped {} bytes of comment", skip);
- self.offset += skip;
- skip != 0
- }
-
- fn skip_comments_and_whitespace(&mut self) {
- while self.skip_whitespace() || self.skip_comments() {}
- }
-}
-
-impl<'input> Iterator for Lexer<'input> {
- type Item = Spanned<Tok<'input>, usize, LexicalError>;
-
- fn next(&mut self) -> Option<Self::Item> {
- use nom::IResult::*;
- self.skip_comments_and_whitespace();
- let input = self.current_input();
- if input.is_empty() {
- return None;
- }
- 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) => {
- let offset = self.offset;
- self.offset = self.input.len();
- Some(Err(LexicalError::Error(offset, 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"),
- Ascription,
- Builtin(crate::core::Builtin::Bool),
- ParenR,
- Arrow,
- Identifier("b"),
- CompareEQ,
- Bool(false),
- ];
- let lexer = Lexer::new(s);
- let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
- assert_eq!(&tokens, &expected);
-
- assert_eq!(string_lit(r#""a\&b""#).to_result(), Ok("ab".to_owned()));
- assert_eq!(
- string_lit(r#""a\ \b""#).to_result(),
- Ok("ab".to_owned())
- );
- assert!(string_lit(r#""a\ b""#).is_err());
- assert_eq!(string_lit(r#""a\nb""#).to_result(), Ok("a\nb".to_owned()));
- assert_eq!(
- string_lit(r#""\o141\x62\99""#).to_result(),
- Ok("abc".to_owned())
- );
-}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 7cc96e1..902df53 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -2,11 +2,4 @@
#![feature(trace_macros)]
pub mod context;
-mod core;
-pub use crate::core::*;
-use lalrpop_util::lalrpop_mod;
-lalrpop_mod!(pub grammar);
-mod grammar_util;
-pub mod lexer;
-pub mod parser;
pub mod typecheck;
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 78a2905..3e8aca4 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -3,6 +3,7 @@ use std::io::{self, Read};
use term_painter::ToStyle;
use dhall::*;
+use dhall_core::*;
const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
const BOLD: term_painter::Attr = term_painter::Attr::Bold;
diff --git a/dhall/src/parser.rs b/dhall/src/parser.rs
deleted file mode 100644
index 6b20c01..0000000
--- a/dhall/src/parser.rs
+++ /dev/null
@@ -1,827 +0,0 @@
-use std::collections::BTreeMap;
-// use itertools::*;
-use lalrpop_util;
-use pest::iterators::Pair;
-use pest::Parser;
-
-use dhall_parser::{DhallParser, Rule};
-
-use crate::core;
-use crate::core::{bx, BinOp, Builtin, Const, Expr, V};
-use crate::grammar;
-use crate::grammar_util::{BoxExpr, ParsedExpr};
-use crate::lexer::{Lexer, LexicalError, Tok};
-
-pub fn parse_expr_lalrpop(
- s: &str,
-) -> Result<BoxExpr, lalrpop_util::ParseError<usize, Tok, LexicalError>> {
- grammar::ExprParser::new().parse(Lexer::new(s))
- // Ok(bx(Expr::BoolLit(false)))
-}
-
-pub type ParseError = pest::error::Error<Rule>;
-
-pub type ParseResult<T> = Result<T, ParseError>;
-
-pub fn custom_parse_error(pair: &Pair<Rule>, msg: String) -> ParseError {
- let msg =
- format!("{} while matching on:\n{}", msg, debug_pair(pair.clone()));
- let e = pest::error::ErrorVariant::CustomError { message: msg };
- pest::error::Error::new_from_span(e, pair.as_span())
-}
-
-fn debug_pair(pair: Pair<Rule>) -> String {
- use std::fmt::Write;
- let mut s = String::new();
- fn aux(s: &mut String, indent: usize, prefix: String, pair: Pair<Rule>) {
- let indent_str = "| ".repeat(indent);
- let rule = pair.as_rule();
- let contents = pair.as_str().clone();
- let mut inner = pair.into_inner();
- let mut first = true;
- while let Some(p) = inner.next() {
- if first {
- first = false;
- let last = inner.peek().is_none();
- if last && p.as_str() == contents {
- let prefix = format!("{}{:?} > ", prefix, rule);
- aux(s, indent, prefix, p);
- continue;
- } else {
- writeln!(
- s,
- r#"{}{}{:?}: "{}""#,
- indent_str, prefix, rule, contents
- )
- .unwrap();
- }
- }
- aux(s, indent + 1, "".into(), p);
- }
- if first {
- writeln!(
- s,
- r#"{}{}{:?}: "{}""#,
- indent_str, prefix, rule, contents
- )
- .unwrap();
- }
- }
- aux(&mut s, 0, "".into(), pair);
- s
-}
-
-/* Macro to pattern-match iterators.
- * Returns `Result<_, IterMatchError<_>>`.
- *
- * Example:
- * ```
- * let vec = vec![1, 2, 3];
- *
- * match_iter!(vec.into_iter(); (x, y?, z) => {
- * // x: T
- * // y: Option<T>
- * // z: T
- * })
- *
- * // or
- * match_iter!(vec.into_iter(); (x, y, z*) => {
- * // x, y: T
- * // z: impl Iterator<T>
- * })
- * ```
- *
-*/
-#[derive(Debug)]
-enum IterMatchError<T> {
- NotEnoughItems,
- TooManyItems,
- NoMatchFound,
- Other(T), // Allow other macros to inject their own errors
-}
-macro_rules! match_iter {
- // Everything else pattern
- (@match 0, $iter:expr, $x:ident* $($rest:tt)*) => {
- match_iter!(@match 2, $iter $($rest)*);
- #[allow(unused_mut)]
- let mut $x = $iter;
- };
- // Alias to use in macros
- (@match 0, $iter:expr, $x:ident?? $($rest:tt)*) => {
- match_iter!(@match 2, $iter $($rest)*);
- #[allow(unused_mut)]
- let mut $x = $iter;
- };
- // Optional pattern
- (@match 0, $iter:expr, $x:ident? $($rest:tt)*) => {
- match_iter!(@match 1, $iter $($rest)*);
- #[allow(unused_mut)]
- let mut $x = $iter.next();
- match $iter.next() {
- Some(_) => break Err(IterMatchError::TooManyItems),
- None => {},
- };
- };
- // Normal pattern
- (@match 0, $iter:expr, $x:ident $($rest:tt)*) => {
- #[allow(unused_mut)]
- let mut $x = match $iter.next() {
- Some(x) => x,
- None => break Err(IterMatchError::NotEnoughItems),
- };
- match_iter!(@match 0, $iter $($rest)*);
- };
- // Normal pattern after a variable length one: declare reversed and take from the end
- (@match $w:expr, $iter:expr, $x:ident $($rest:tt)*) => {
- match_iter!(@match $w, $iter $($rest)*);
- #[allow(unused_mut)]
- let mut $x = match $iter.next_back() {
- Some(x) => x,
- None => break Err(IterMatchError::NotEnoughItems),
- };
- };
-
- // Check no elements remain
- (@match 0, $iter:expr $(,)*) => {
- match $iter.next() {
- Some(_) => break Err(IterMatchError::TooManyItems),
- None => {},
- };
- };
- (@match $_:expr, $iter:expr) => {};
-
- (@panic; $($args:tt)*) => {
- {
- let ret: Result<_, IterMatchError<()>> = match_iter!($($args)*);
- ret.unwrap()
- }
- };
- ($iter:expr; ($($args:tt)*) => $body:expr) => {
- {
- #[allow(unused_mut)]
- let mut iter = $iter;
- // Not a real loop; used for error handling
- let ret: Result<_, IterMatchError<_>> = loop {
- match_iter!(@match 0, iter, $($args)*);
- break Ok($body);
- };
- ret
- }
- };
-}
-
-/* Extends match_iter with typed matches. Takes a callback that determines
- * when a capture matches.
- * Returns `Result<_, IterMatchError<_>>`; errors returned by the callback will
- * get propagated using IterMatchError::Other.
- *
- * Example:
- * ```
- * macro_rules! callback {
- * (@type_callback, positive, $x:expr) => {
- * if $x >= 0 { Ok($x) } else { Err(()) }
- * };
- * (@type_callback, negative, $x:expr) => {
- * if $x <= 0 { Ok($x) } else { Err(()) }
- * };
- * (@type_callback, any, $x:expr) => {
- * Ok($x)
- * };
- * }
- *
- * let vec = vec![-1, 2, 3];
- *
- * match_iter_typed!(callback; vec.into_iter();
- * (x: positive, y?: negative, z: any) => { ... },
- * )
- * ```
- *
-*/
-macro_rules! match_iter_typed {
- // Collect untyped arguments to pass to match_iter!
- (@collect, ($($vars:tt)*), ($($args:tt)*), ($($acc:tt)*), ($x:ident : $ty:ident, $($rest:tt)*)) => {
- match_iter_typed!(@collect, ($($vars)*), ($($args)*), ($($acc)*, $x), ($($rest)*))
- };
- (@collect, ($($vars:tt)*), ($($args:tt)*), ($($acc:tt)*), ($x:ident? : $ty:ident, $($rest:tt)*)) => {
- match_iter_typed!(@collect, ($($vars)*), ($($args)*), ($($acc)*, $x?), ($($rest)*))
- };
- (@collect, ($($vars:tt)*), ($($args:tt)*), ($($acc:tt)*), ($x:ident* : $ty:ident, $($rest:tt)*)) => {
- match_iter_typed!(@collect, ($($vars)*), ($($args)*), ($($acc)*, $x??), ($($rest)*))
- };
- // Catch extra comma if exists
- (@collect, ($($vars:tt)*), ($($args:tt)*), (,$($acc:tt)*), ($(,)*)) => {
- match_iter_typed!(@collect, ($($vars)*), ($($args)*), ($($acc)*), ())
- };
- (@collect, ($iter:expr, $body:expr, $callback:ident, $error:ident), ($($args:tt)*), ($($acc:tt)*), ($(,)*)) => {
- match_iter!($iter; ($($acc)*) => {
- match_iter_typed!(@callback, $callback, $iter, $($args)*);
- $body
- })
- };
-
- // Pass the matches through the callback
- (@callback, $callback:ident, $iter:expr, $x:ident : $ty:ident $($rest:tt)*) => {
- let $x = $callback!(@type_callback, $ty, $x);
- #[allow(unused_mut)]
- let mut $x = match $x {
- Ok(x) => x,
- Err(e) => break Err(IterMatchError::Other(e)),
- };
- match_iter_typed!(@callback, $callback, $iter $($rest)*);
- };
- (@callback, $callback: ident, $iter:expr, $x:ident? : $ty:ident $($rest:tt)*) => {
- let $x = $x.map(|x| $callback!(@type_callback, $ty, x));
- #[allow(unused_mut)]
- let mut $x = match $x {
- Some(Ok(x)) => Some(x),
- Some(Err(e)) => break Err(IterMatchError::Other(e)),
- None => None,
- };
- match_iter_typed!(@callback, $callback, $iter $($rest)*);
- };
- (@callback, $callback: ident, $iter:expr, $x:ident* : $ty:ident $($rest:tt)*) => {
- let $x = $x.map(|x| $callback!(@type_callback, $ty, x)).collect();
- let $x: Vec<_> = match $x {
- Ok(x) => x,
- Err(e) => break Err(IterMatchError::Other(e)),
- };
- #[allow(unused_mut)]
- let mut $x = $x.into_iter();
- match_iter_typed!(@callback, $callback, $iter $($rest)*);
- };
- (@callback, $callback:ident, $iter:expr $(,)*) => {};
-
- ($callback:ident; $iter:expr; ($($args:tt)*) => $body:expr) => {
- {
- #[allow(unused_mut)]
- let mut iter = $iter;
- match_iter_typed!(@collect,
- (iter, $body, $callback, last_error),
- ($($args)*), (), ($($args)*,)
- )
- }
- };
-}
-
-/* Extends match_iter and match_iter_typed with branching.
- * Returns `Result<_, IterMatchError<_>>`; errors returned by the callback will
- * get propagated using IterMatchError::Other.
- * Allows multiple branches. The passed iterator must be Clone.
- * Will check the branches in order, testing each branch using the callback macro provided.
- *
- * Example:
- * ```
- * macro_rules! callback {
- * (@type_callback, positive, $x:expr) => {
- * if $x >= 0 { Ok($x) } else { Err(()) }
- * };
- * (@type_callback, negative, $x:expr) => {
- * if $x <= 0 { Ok($x) } else { Err(()) }
- * };
- * (@type_callback, any, $x:expr) => {
- * Ok($x)
- * };
- * (@branch_callback, typed, $($args:tt)*) => {
- * match_iter_typed!(callback; $($args)*)
- * };
- * (@branch_callback, untyped, $($args:tt)*) => {
- * match_iter!($($args)*)
- * };
- * }
- *
- * let vec = vec![-1, 2, 3];
- *
- * match_iter_branching!(branch_callback; vec.into_iter();
- * typed!(x: positive, y?: negative, z: any) => { ... },
- * untyped!(x, y, z) => { ... },
- * )
- * ```
- *
-*/
-macro_rules! match_iter_branching {
- (@noclone, $callback:ident; $arg:expr; $( $submac:ident!($($args:tt)*) => $body:expr ),* $(,)*) => {
- {
- #[allow(unused_assignments)]
- let mut last_error = IterMatchError::NoMatchFound;
- // Not a real loop; used for error handling
- // Would use loop labels but they create warnings
- #[allow(unreachable_code)]
- loop {
- $(
- let matched: Result<_, IterMatchError<_>> =
- $callback!(@branch_callback, $submac, $arg; ($($args)*) => $body);
- #[allow(unused_assignments)]
- match matched {
- Ok(v) => break Ok(v),
- Err(e) => last_error = e,
- };
- )*
- break Err(last_error);
- }
- }
- };
- ($callback:ident; $iter:expr; $($args:tt)*) => {
- {
- #[allow(unused_mut)]
- let mut iter = $iter;
- match_iter_branching!(@noclone, $callback; iter.clone(); $($args)*)
- }
- };
-}
-
-macro_rules! match_pair {
- (@type_callback, $ty:ident, $x:expr) => {
- $ty($x)
- };
- (@branch_callback, children, $pair:expr; $($args:tt)*) => {
- {
- #[allow(unused_mut)]
- let mut pairs = $pair.clone().into_inner();
- match_iter_typed!(match_pair; pairs; $($args)*)
- }
- };
- (@branch_callback, self, $pair:expr; ($x:ident : $ty:ident) => $body:expr) => {
- {
- let $x = match_pair!(@type_callback, $ty, $pair.clone());
- match $x {
- Ok($x) => Ok($body),
- Err(e) => Err(IterMatchError::Other(e)),
- }
- }
- };
- (@branch_callback, raw_pair, $pair:expr; ($x:ident) => $body:expr) => {
- {
- let $x = $pair.clone();
- Ok($body)
- }
- };
- (@branch_callback, captured_str, $pair:expr; ($x:ident) => $body:expr) => {
- {
- let $x = $pair.as_str();
- Ok($body)
- }
- };
-
- ($pair:expr; $($args:tt)*) => {
- {
- let pair = $pair;
- let result = match_iter_branching!(@noclone, match_pair; pair; $($args)*);
- result.map_err(|e| match e {
- IterMatchError::Other(e) => e,
- _ => custom_parse_error(&pair, "No match found".to_owned()),
- })
- }
- };
-}
-
-macro_rules! make_pest_parse_function {
- ($name:ident<$o:ty>; $submac:ident!( $($args:tt)* )) => (
- #[allow(unused_variables)]
- #[allow(non_snake_case)]
- fn $name<'a>(pair: Pair<'a, Rule>) -> ParseResult<$o> {
- $submac!(pair; $($args)*)
- }
- );
-}
-
-macro_rules! named {
- ($name:ident<$o:ty>; $($args:tt)*) => (
- make_pest_parse_function!($name<$o>; match_pair!( $($args)* ));
- );
-}
-
-macro_rules! rule {
- ($name:ident<$o:ty>; $($args:tt)*) => (
- make_pest_parse_function!($name<$o>; match_rule!(
- Rule::$name => match_pair!( $($args)* ),
- ));
- );
-}
-
-macro_rules! rule_group {
- ($name:ident<$o:ty>; $($ty:ident),*) => (
- make_pest_parse_function!($name<$o>; match_rule!(
- $(
- Rule::$ty => match_pair!(raw_pair!(p) => $ty(p)?),
- )*
- ));
- );
-}
-
-macro_rules! match_rule {
- ($pair:expr; $($pat:pat => $submac:ident!( $($args:tt)* ),)*) => {
- {
- #[allow(unreachable_patterns)]
- match $pair.as_rule() {
- $(
- $pat => $submac!($pair; $($args)*),
- )*
- r => Err(custom_parse_error(&$pair, format!("Unexpected {:?}", r))),
- }
- }
- };
-}
-
-rule!(EOI<()>; children!() => ());
-
-named!(str<&'a str>; captured_str!(s) => s.trim());
-
-named!(raw_str<&'a str>; captured_str!(s) => s);
-
-rule!(escaped_quote_pair<&'a str>;
- children!() => "''"
-);
-rule!(escaped_interpolation<&'a str>;
- children!() => "${"
-);
-
-rule!(single_quote_continue<Vec<&'a str>>;
- // TODO: handle interpolation
- // children!(c: expression, rest: single_quote_continue) => {
- // rest.push(c); rest
- // },
- children!(c: escaped_quote_pair, rest: single_quote_continue) => {
- rest.push(c); rest
- },
- children!(c: escaped_interpolation, rest: single_quote_continue) => {
- rest.push(c); rest
- },
- // capture interpolation as string
- children!(c: raw_str, rest: single_quote_continue) => {
- rest.push(c); rest
- },
- children!() => {
- vec![]
- },
-);
-
-rule!(let_binding<(&'a str, Option<BoxExpr<'a>>, BoxExpr<'a>)>;
- children!(name: str, annot?: expression, expr: expression) => (name, annot, expr)
-);
-
-named!(record_entry<(&'a str, BoxExpr<'a>)>;
- children!(name: str, expr: expression) => (name, expr)
-);
-
-named!(partial_record_entries<(BoxExpr<'a>, BTreeMap<&'a str, ParsedExpr<'a>>)>;
- children!(expr: expression, entries*: record_entry) => {
- let mut map: BTreeMap<&str, ParsedExpr> = BTreeMap::new();
- for (n, e) in entries {
- map.insert(n, *e);
- }
- (expr, map)
- }
-);
-
-rule!(non_empty_record_literal<(BoxExpr<'a>, BTreeMap<&'a str, ParsedExpr<'a>>)>;
- self!(x: partial_record_entries) => x
-);
-
-rule!(non_empty_record_type<(BoxExpr<'a>, BTreeMap<&'a str, ParsedExpr<'a>>)>;
- self!(x: partial_record_entries) => x
-);
-
-rule!(union_type_entry<(&'a str, BoxExpr<'a>)>;
- children!(name: str, expr: expression) => (name, expr)
-);
-
-rule!(union_type_entries<BTreeMap<&'a str, ParsedExpr<'a>>>;
- children!(entries*: union_type_entry) => {
- let mut map: BTreeMap<&str, ParsedExpr> = BTreeMap::new();
- for (n, e) in entries {
- map.insert(n, *e);
- }
- map
- }
-);
-
-rule!(non_empty_union_type_or_literal
- <(Option<(&'a str, BoxExpr<'a>)>, BTreeMap<&'a str, ParsedExpr<'a>>)>;
- children!(label: str, e: expression, entries: union_type_entries) => {
- (Some((label, e)), entries)
- },
- children!(l: str, e: expression, rest: non_empty_union_type_or_literal) => {
- let (x, mut entries) = rest;
- entries.insert(l, *e);
- (x, entries)
- },
- children!(l: str, e: expression) => {
- let mut entries = BTreeMap::new();
- entries.insert(l, *e);
- (None, entries)
- },
-);
-
-rule!(empty_union_type<()>; children!() => ());
-
-rule_group!(expression<BoxExpr<'a>>;
- identifier_raw,
- lambda_expression,
- ifthenelse_expression,
- let_expression,
- forall_expression,
- arrow_expression,
- merge_expression,
- empty_collection,
- non_empty_optional,
-
- annotated_expression,
- import_alt_expression,
- or_expression,
- plus_expression,
- text_append_expression,
- list_append_expression,
- and_expression,
- combine_expression,
- prefer_expression,
- combine_types_expression,
- times_expression,
- equal_expression,
- not_equal_expression,
- application_expression,
-
- selector_expression_raw,
- literal_expression_raw,
- empty_record_type,
- empty_record_literal,
- non_empty_record_type_or_literal,
- union_type_or_literal,
- non_empty_list_literal_raw,
- final_expression
-);
-
-// TODO: parse escapes and interpolation
-rule!(double_quote_literal<String>;
- children!(strs*: raw_str) => {
- strs.collect()
- }
-);
-rule!(single_quote_literal<String>;
- children!(eol: raw_str, contents: single_quote_continue) => {
- contents.push(eol);
- contents.into_iter().rev().collect()
- }
-);
-
-rule!(double_literal_raw<core::Double>;
- raw_pair!(pair) => {
- pair.as_str().trim()
- .parse()
- .map_err(|e: std::num::ParseFloatError| custom_parse_error(&pair, format!("{}", e)))?
- }
-);
-
-rule!(minus_infinity_literal<()>; children!() => ());
-rule!(plus_infinity_literal<()>; children!() => ());
-rule!(NaN_raw<()>; children!() => ());
-
-rule!(natural_literal_raw<core::Natural>;
- raw_pair!(pair) => {
- pair.as_str().trim()
- .parse()
- .map_err(|e: std::num::ParseIntError| custom_parse_error(&pair, format!("{}", e)))?
- }
-);
-
-rule!(integer_literal_raw<core::Integer>;
- raw_pair!(pair) => {
- pair.as_str().trim()
- .parse()
- .map_err(|e: std::num::ParseIntError| custom_parse_error(&pair, format!("{}", e)))?
- }
-);
-
-rule!(identifier_raw<BoxExpr<'a>>;
- children!(name: str, idx?: natural_literal_raw) => {
- match Builtin::parse(name) {
- Some(b) => bx(Expr::Builtin(b)),
- None => match name {
- "True" => bx(Expr::BoolLit(true)),
- "False" => bx(Expr::BoolLit(false)),
- "Type" => bx(Expr::Const(Const::Type)),
- "Kind" => bx(Expr::Const(Const::Kind)),
- name => bx(Expr::Var(V(name, idx.unwrap_or(0)))),
- }
- }
- }
-);
-
-rule!(lambda_expression<BoxExpr<'a>>;
- children!(label: str, typ: expression, body: expression) => {
- bx(Expr::Lam(label, typ, body))
- }
-);
-
-rule!(ifthenelse_expression<BoxExpr<'a>>;
- children!(cond: expression, left: expression, right: expression) => {
- bx(Expr::BoolIf(cond, left, right))
- }
-);
-
-rule!(let_expression<BoxExpr<'a>>;
- children!(bindings*: let_binding, final_expr: expression) => {
- bindings.fold(final_expr, |acc, x| bx(Expr::Let(x.0, x.1, x.2, acc)))
- }
-);
-
-rule!(forall_expression<BoxExpr<'a>>;
- children!(label: str, typ: expression, body: expression) => {
- bx(Expr::Pi(label, typ, body))
- }
-);
-
-rule!(arrow_expression<BoxExpr<'a>>;
- children!(typ: expression, body: expression) => {
- bx(Expr::Pi("_", typ, body))
- }
-);
-
-rule!(merge_expression<BoxExpr<'a>>;
- children!(x: expression, y: expression, z?: expression) => {
- bx(Expr::Merge(x, y, z))
- }
-);
-
-rule!(empty_collection<BoxExpr<'a>>;
- children!(x: str, y: expression) => {
- match x {
- "Optional" => bx(Expr::OptionalLit(Some(y), vec![])),
- "List" => bx(Expr::ListLit(Some(y), vec![])),
- _ => unreachable!(),
- }
- }
-);
-
-rule!(non_empty_optional<BoxExpr<'a>>;
- children!(x: expression, _y: str, z: expression) => {
- bx(Expr::OptionalLit(Some(z), vec![*x]))
- }
-);
-
-macro_rules! binop {
- ($rule:ident, $op:ident) => {
- rule!($rule<BoxExpr<'a>>;
- children!(first: expression, rest*: expression) => {
- rest.fold(first, |acc, e| bx(Expr::BinOp(BinOp::$op, acc, e)))
- }
- );
- };
-}
-
-rule!(annotated_expression<BoxExpr<'a>>;
- children!(e: expression, annot: expression) => {
- bx(Expr::Annot(e, annot))
- },
- children!(e: expression) => e,
-);
-
-binop!(import_alt_expression, ImportAlt);
-binop!(or_expression, BoolOr);
-binop!(plus_expression, NaturalPlus);
-binop!(text_append_expression, TextAppend);
-binop!(list_append_expression, ListAppend);
-binop!(and_expression, BoolAnd);
-binop!(combine_expression, Combine);
-binop!(prefer_expression, Prefer);
-binop!(combine_types_expression, CombineTypes);
-binop!(times_expression, NaturalTimes);
-binop!(equal_expression, BoolEQ);
-binop!(not_equal_expression, BoolNE);
-
-rule!(application_expression<BoxExpr<'a>>;
- children!(first: expression, rest*: expression) => {
- rest.fold(first, |acc, e| bx(Expr::App(acc, e)))
- }
-);
-
-rule!(selector_expression_raw<BoxExpr<'a>>;
- children!(first: expression, rest*: str) => {
- rest.fold(first, |acc, e| bx(Expr::Field(acc, e)))
- }
-);
-
-rule!(literal_expression_raw<BoxExpr<'a>>;
- children!(n: double_literal_raw) => bx(Expr::DoubleLit(n)),
- children!(n: minus_infinity_literal) => bx(Expr::DoubleLit(std::f64::NEG_INFINITY)),
- children!(n: plus_infinity_literal) => bx(Expr::DoubleLit(std::f64::INFINITY)),
- children!(n: NaN_raw) => bx(Expr::DoubleLit(std::f64::NAN)),
- children!(n: natural_literal_raw) => bx(Expr::NaturalLit(n)),
- children!(n: integer_literal_raw) => bx(Expr::IntegerLit(n)),
- children!(s: double_quote_literal) => bx(Expr::TextLit(s)),
- children!(s: single_quote_literal) => bx(Expr::TextLit(s)),
- children!(e: expression) => e,
-);
-
-rule!(empty_record_type<BoxExpr<'a>>;
- children!() => bx(Expr::Record(BTreeMap::new()))
-);
-rule!(empty_record_literal<BoxExpr<'a>>;
- children!() => bx(Expr::RecordLit(BTreeMap::new()))
-);
-rule!(non_empty_record_type_or_literal<BoxExpr<'a>>;
- children!(first_label: str, rest: non_empty_record_type) => {
- let (first_expr, mut map) = rest;
- map.insert(first_label, *first_expr);
- bx(Expr::Record(map))
- },
- children!(first_label: str, rest: non_empty_record_literal) => {
- let (first_expr, mut map) = rest;
- map.insert(first_label, *first_expr);
- bx(Expr::RecordLit(map))
- },
-);
-
-rule!(union_type_or_literal<BoxExpr<'a>>;
- children!(_e: empty_union_type) => {
- bx(Expr::Union(BTreeMap::new()))
- },
- children!(x: non_empty_union_type_or_literal) => {
- match x {
- (Some((l, e)), entries) => bx(Expr::UnionLit(l, e, entries)),
- (None, entries) => bx(Expr::Union(entries)),
- }
- },
-);
-
-rule!(non_empty_list_literal_raw<BoxExpr<'a>>;
- children!(items*: expression) => {
- bx(Expr::ListLit(None, items.map(|x| *x).collect()))
- }
-);
-
-rule!(final_expression<BoxExpr<'a>>;
- children!(e: expression, _eoi: EOI) => e
-);
-
-pub fn parse_expr_pest(s: &str) -> ParseResult<BoxExpr> {
- let pairs = DhallParser::parse(Rule::final_expression, s)?;
- // Match the only item in the pairs iterator
- match_iter!(@panic; pairs; (p) => expression(p))
- // Ok(bx(Expr::BoolLit(false)))
-}
-
-#[test]
-fn test_parse() {
- use crate::core::BinOp::*;
- use crate::core::Expr::*;
- // let expr = r#"{ x = "foo", y = 4 }.x"#;
- // let expr = r#"(1 + 2) * 3"#;
- let expr = r#"if True then 1 + 3 * 5 else 2"#;
- println!("{:?}", parse_expr_lalrpop(expr));
- use std::thread;
- // I don't understand why it stack overflows even on tiny expressions...
- thread::Builder::new()
- .stack_size(3 * 1024 * 1024)
- .spawn(move || match parse_expr_pest(expr) {
- Err(e) => {
- println!("{:?}", e);
- println!("{}", e);
- }
- ok => println!("{:?}", ok),
- })
- .unwrap()
- .join()
- .unwrap();
- // assert_eq!(parse_expr_pest(expr).unwrap(), parse_expr_lalrpop(expr).unwrap());
- // assert!(false);
-
- println!("test {:?}", parse_expr_lalrpop("3 + 5 * 10"));
- assert!(parse_expr_lalrpop("22").is_ok());
- assert!(parse_expr_lalrpop("(22)").is_ok());
- assert_eq!(
- parse_expr_lalrpop("3 + 5 * 10").ok(),
- Some(Box::new(BinOp(
- NaturalPlus,
- Box::new(NaturalLit(3)),
- Box::new(BinOp(
- NaturalTimes,
- Box::new(NaturalLit(5)),
- Box::new(NaturalLit(10))
- ))
- )))
- );
- // The original parser is apparently right-associative
- assert_eq!(
- parse_expr_lalrpop("2 * 3 * 4").ok(),
- Some(Box::new(BinOp(
- NaturalTimes,
- Box::new(NaturalLit(2)),
- Box::new(BinOp(
- NaturalTimes,
- Box::new(NaturalLit(3)),
- Box::new(NaturalLit(4))
- ))
- )))
- );
- assert!(parse_expr_lalrpop("((((22))))").is_ok());
- assert!(parse_expr_lalrpop("((22)").is_err());
- println!("{:?}", parse_expr_lalrpop("\\(b : Bool) -> b == False"));
- assert!(parse_expr_lalrpop("\\(b : Bool) -> b == False").is_ok());
- println!("{:?}", parse_expr_lalrpop("foo.bar"));
- assert!(parse_expr_lalrpop("foo.bar").is_ok());
- assert!(parse_expr_lalrpop("[] : List Bool").is_ok());
-
- // println!("{:?}", parse_expr_lalrpop("< Left = True | Right : Natural >"));
- // println!("{:?}", parse_expr_lalrpop(r#""bl${42}ah""#));
- // assert!(parse_expr_lalrpop("< Left = True | Right : Natural >").is_ok());
-}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 976293d..61a83e7 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -4,12 +4,12 @@ use std::collections::HashSet;
use std::fmt;
use crate::context::Context;
-use crate::core;
-use crate::core::Builtin::*;
-use crate::core::Const::*;
-use crate::core::Expr::*;
-use crate::core::{app, pi};
-use crate::core::{bx, normalize, shift, subst, Expr, V, X};
+use dhall_core::core;
+use dhall_core::core::Builtin::*;
+use dhall_core::core::Const::*;
+use dhall_core::core::Expr::*;
+use dhall_core::core::{app, pi};
+use dhall_core::core::{bx, normalize, shift, subst, Expr, V, X};
use self::TypeMessage::*;
@@ -184,7 +184,7 @@ pub fn type_with<'i, S>(
where
S: Clone + ::std::fmt::Debug + 'i,
{
- use crate::BinOp::*;
+ use dhall_core::BinOp::*;
match *e {
Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
Var(V(x, n)) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 15:51:50 +0000