diff options
Diffstat (limited to 'src')
45 files changed, 0 insertions, 4440 deletions
diff --git a/src/context.rs b/src/context.rs deleted file mode 100644 index c2e1913..0000000 --- a/src/context.rs +++ /dev/null @@ -1,51 +0,0 @@ -use std::collections::HashMap; - -/// A `(Context a)` associates `Text` labels with values of type `a` -/// -/// The `Context` is used for type-checking when `(a = Expr X)` -/// -/// * You create a `Context` using `empty` and `insert` -/// * You transform a `Context` using `fmap` -/// * You consume a `Context` using `lookup` and `toList` -/// -/// The difference between a `Context` and a `Map` is that a `Context` lets you -/// have multiple ordered occurrences of the same key and you can query for the -/// `n`th occurrence of a given key. -/// -#[derive(Debug, Clone)] -pub struct Context<'i, T>(HashMap<&'i str, Vec<T>>); - -impl<'i, T> Context<'i, T> { - /// An empty context with no key-value pairs - pub fn new() -> Self { - Context(HashMap::new()) - } - - /// Look up a key by name and index - /// - /// ```c - /// lookup _ _ empty = Nothing - /// lookup k 0 (insert k v c) = Just v - /// lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n - /// lookup k n (insert j v c) = lookup k n c -- k /= j - /// ``` - pub fn lookup<'a>(&'a self, k: &str, n: usize) -> Option<&'a T> { - self.0.get(k).and_then(|v| v.get(v.len() - 1 - n)) - } - - pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> { - Context(self.0.iter().map(|(k, v)| (*k, v.iter().map(&f).collect())).collect()) - } -} - -impl<'i, T: Clone> Context<'i, T> { - /// Add a key-value pair to the `Context` - pub fn insert(&self, k: &'i str, v: T) -> Self { - let mut ctx = (*self).clone(); - { - let m = ctx.0.entry(k).or_insert_with(Vec::new); - m.push(v); - } - ctx - } -} diff --git a/src/core.rs b/src/core.rs deleted file mode 100644 index 473a6a6..0000000 --- a/src/core.rs +++ /dev/null @@ -1,1056 +0,0 @@ -#![allow(non_snake_case)] -use std::collections::BTreeMap; -use std::fmt::{self, Display}; -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, 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)] // (Eq, Show) -pub struct V<'i>(pub &'i str, pub usize); - -/* -instance IsString Var where - fromString str = V (fromString str) 0 - -instance Buildable Var where - build = buildVar -*/ - -/// Syntax tree for expressions -#[derive(Debug, Clone, PartialEq)] // (Functor, Foldable, Traversable, Show) -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 types - BuiltinType(BuiltinType), - /// Built-in function values - BuiltinValue(BuiltinValue), - /// `BoolLit b ~ b` - BoolLit(bool), - /// `BoolAnd x y ~ x && y` - BoolAnd(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `BoolOr x y ~ x || y` - BoolOr(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `BoolEQ x y ~ x == y` - BoolEQ(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `BoolNE x y ~ x != y` - BoolNE(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `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), - /// `NaturalPlus x y ~ x + y` - NaturalPlus(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `NaturalTimes x y ~ x * y` - NaturalTimes(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `IntegerLit n ~ n` - IntegerLit(Integer), - /// `DoubleLit n ~ n` - DoubleLit(Double), - /// `TextLit t ~ t` - TextLit(Builder), - /// `TextAppend x y ~ x ++ y` - TextAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `ListLit t [x, y, z] ~ [x, y, z] : List t` - ListLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>), - /// `OptionalLit t [e] ~ [e] : Optional t` - /// `OptionalLit t [] ~ [] : Optional t` - OptionalLit(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>>), - /// `Combine x y ~ x ∧ y` - Combine(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>), - /// `Merge x y t ~ merge x y : t` - Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, 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), -} - -/// Built-in types -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum BuiltinType { - /// `Bool ~ Bool` - Bool, - /// `Natural ~ Natural` - Natural, - /// `Integer ~ Integer` - Integer, - /// `Double ~ Double` - Double, - /// `Text ~ Text` - Text, - /// `List ~ List` - List, - /// `Optional ~ Optional` - Optional, -} - -/// Built-in function values -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum BuiltinValue { - /// `NaturalFold ~ Natural/fold` - NaturalFold, - /// `NaturalBuild ~ Natural/build` - NaturalBuild, - /// `NaturalIsZero ~ Natural/isZero` - NaturalIsZero, - /// `NaturalEven ~ Natural/even` - NaturalEven, - /// `NaturalOdd ~ Natural/odd` - NaturalOdd, - NaturalShow, - /// `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, - /// `OptionalFold ~ Optional/fold` - OptionalFold, -} - -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<BuiltinType> for Expr<'i, S, A> { - fn from(t: BuiltinType) -> Self { - Expr::BuiltinType(t) - } -} - -impl<'i, S, A> From<BuiltinValue> for Expr<'i, S, A> { - fn from(t: BuiltinValue) -> Self { - Expr::BuiltinValue(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("[", "] : List ", es, f, |e, f| e.fmt(f))?; - t.fmt_e(f) - } - &OptionalLit(ref t, ref es) => { - fmt_list("[", "] : Optional ", es, f, |e, f| e.fmt(f))?; - t.fmt_e(f) - } - &Merge(ref a, ref b, ref c) => { - write!(f, "merge ")?; - a.fmt_e(f)?; - write!(f, " ")?; - b.fmt_e(f)?; - write!(f, " : ")?; - c.fmt_d(f) - } - &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::Expr::*; - match self { - // FIXME precedence - &BoolOr(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" || ")?; b.fmt_c(f) } - &TextAppend(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ++ ")?; b.fmt_c(f) } - &NaturalPlus(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" + ")?; b.fmt_c(f) } - &BoolAnd(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" && ")?; b.fmt_c(f) } - &Combine(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ^ ")?; b.fmt_c(f) } - &NaturalTimes(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" * ")?; b.fmt_c(f) } - &BoolEQ(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" == ")?; b.fmt_c(f) } - &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), - &BuiltinType(t) => t.fmt(f), - &BuiltinValue(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 BuiltinType { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - <Self as fmt::Debug>::fmt(self, f) - } -} - -impl Display for BuiltinValue { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use crate::BuiltinValue::*; - f.write_str(match *self { - ListBuild => "List/build", - ListFold => "List/fold", - ListHead => "List/head", - ListIndexed => "List/indexed", - ListLast => "List/last", - ListLength => "List/length", - ListReverse => "List/reverse", - NaturalBuild => "Natural/build", - NaturalEven => "Natural/even", - NaturalFold => "Natural/fold", - NaturalIsZero => "Natural/isZero", - NaturalOdd => "Natural/odd", - NaturalShow => "Natural/show", - OptionalFold => "Optional/fold", - }) - } -} - -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), - BuiltinType(t) => BuiltinType(t), - BuiltinValue(v) => BuiltinValue(v), - BoolLit(a) => BoolLit(a), - BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b), - BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b), - BoolEQ(ref a, ref b) => shift_op2(BoolEQ, d, v, a, b), - BoolNE(ref a, ref b) => shift_op2(BoolNE, 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), - NaturalPlus(ref a, ref b) => NaturalPlus(bx(shift(d, v, a)), bx(shift(d, v, b))), - NaturalTimes(ref a, ref b) => shift_op2(NaturalTimes, d, v, a, b), - IntegerLit(a) => IntegerLit(a), - DoubleLit(a) => DoubleLit(a), - TextLit(ref a) => TextLit(a.clone()), - TextAppend(ref a, ref b) => shift_op2(TextAppend, d, v, a, b), - ListLit(ref t, ref es) => { - ListLit(bx(shift(d, v, t)), - es.iter().map(|e| shift(d, v, e)).collect()) - } - OptionalLit(ref t, ref es) => { - OptionalLit(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))) - } - Combine(ref a, ref b) => shift_op2(Combine, d, v, a, b), - Merge(ref a, ref b, ref c) => { - Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), 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()), - } -} - -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), - BuiltinType(t) => BuiltinType(t), - BuiltinValue(v) => BuiltinValue(v), - BoolLit(a) => BoolLit(a), - BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b), - BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b), - BoolEQ(ref a, ref b) => subst_op2(BoolEQ, v, e, a, b), - BoolNE(ref a, ref b) => subst_op2(BoolNE, 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), - NaturalPlus(ref a, ref b) => subst_op2(NaturalPlus, v, e, a, b), - NaturalTimes(ref a, ref b) => subst_op2(NaturalTimes, v, e, a, b), - IntegerLit(a) => IntegerLit(a), - DoubleLit(a) => DoubleLit(a), - TextLit(ref a) => TextLit(a.clone()), - TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b), - ListLit(ref a, ref b) => { - let a2 = subst(v, e, a); - let b2 = b.iter().map(|be| subst(v, e, be)).collect(); - ListLit(bx(a2), b2) - } - OptionalLit(ref a, ref b) => { - let a2 = subst(v, e, a); - let b2 = b.iter().map(|be| subst(v, e, be)).collect(); - OptionalLit(bx(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))) - } - Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b), - Merge(ref a, ref b, ref c) => { - Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), 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()), - } -} - -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::BuiltinValue::*; - 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 BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) | - (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) | - - // fold/build fusion for `Natural` - (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) | - (BuiltinValue(NaturalFold), App(box BuiltinValue(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 - */ - (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0), - (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0), - (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), - (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()), - (App(f@box BuiltinValue(ListBuild), box t), k) => { - let labeled = - normalize::<_, T, _>(&app(app(app(k.clone(), app( - BuiltinType(self::BuiltinType::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(bx(t), v) - } else { - app(App(f, bx(t)), k) - } - } - (App(box App(box App(box App(box BuiltinValue(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 { - BuiltinValue(ListLength) => - NaturalLit(ys.len()), - BuiltinValue(ListHead) => - normalize(&OptionalLit(t, ys.into_iter().take(1).collect())), - BuiltinValue(ListLast) => - normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())), - BuiltinValue(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 (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing -> - normalize (maybe nothing just' (toMaybe xs)) - where - just' y = App just y - toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList - */ - (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), - BuiltinType(t) => BuiltinType(t), - BuiltinValue(v) => BuiltinValue(v), - BoolLit(b) => BoolLit(b), - BoolAnd(ref x, ref y) => { - with_binop(BoolAnd, Expr::bool_lit, - |xn, yn| BoolLit(xn && yn), - normalize(x), normalize(y)) - } - BoolOr(ref x, ref y) => { - with_binop(BoolOr, Expr::bool_lit, - |xn, yn| BoolLit(xn || yn), - normalize(x), normalize(y)) - } - BoolEQ(ref x, ref y) => { - with_binop(BoolEQ, Expr::bool_lit, - |xn, yn| BoolLit(xn == yn), - normalize(x), normalize(y)) - } - 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), - NaturalPlus(ref x, ref y) => { - with_binop(NaturalPlus, Expr::natural_lit, - |xn, yn| NaturalLit(xn + yn), - normalize(x), normalize(y)) - } - 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()), - 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 = normalize(t); - let es2 = es.iter().map(normalize).collect(); - ListLit(bx(t2), es2) - } - OptionalLit(ref t, ref es) => { - let t2 = normalize(t); - let es2 = es.iter().map(normalize).collect(); - OptionalLit(bx(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)), - Combine(ref _x0, ref _y0) => unimplemented!(), - 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()), - } -} - -fn with_binop<T, U, Get, Set, Op>(op: Op, get: Get, set: Set, x: T, y: T) -> T - where Get: Fn(&T) -> Option<U>, - Set: FnOnce(U, U) -> T, - Op: FnOnce(Box<T>, Box<T>) -> T, -{ - if let (Some(xv), Some(yv)) = (get(&x), get(&y)) { - set(xv, yv) - } else { - op(bx(x), bx(y)) - } -} diff --git a/src/dhall.pest.visibility b/src/dhall.pest.visibility deleted file mode 100644 index c09fccf..0000000 --- a/src/dhall.pest.visibility +++ /dev/null @@ -1,188 +0,0 @@ -# end_of_line -# tab -# block_comment -# block_comment_chunk -# block_comment_continue -# not_end_of_line -# line_comment -# whitespace_chunk -# whitespace -# nonempty_whitespace -# ALPHA -# DIGIT -# HEXDIG -# simple_label -# quoted_label -# label -# double_quote_chunk -# double_quote_literal -# single_quote_continue -# single_quote_literal -# text_literal -# if_raw -# then_raw -# else_raw -# let_raw -# in_raw -# as_raw -# using_raw -# merge_raw -# missing_raw -# Some_raw -# constructors_raw -# Natural_fold_raw -# Natural_build_raw -# Natural_isZero_raw -# Natural_even_raw -# Natural_odd_raw -# Natural_toInteger_raw -# Natural_show_raw -# Integer_toDouble_raw -# Integer_show_raw -# Double_show_raw -# List_build_raw -# List_fold_raw -# List_length_raw -# List_head_raw -# List_last_raw -# List_indexed_raw -# List_reverse_raw -# Optional_fold_raw -# Optional_build_raw -# Text_show_raw -# Bool_raw -# Optional_raw -# None_raw -# Natural_raw -# Integer_raw -# Double_raw -# Text_raw -# List_raw -# True_raw -# False_raw -# NaN_raw -# Infinity_raw -# Type_raw -# Kind_raw -# Sort_raw -# reserved_raw -# reserved_namespaced_raw -# reserved -# reserved_namespaced -# if_ -# then_ -# else_ -# let_ -# in_ -# as_ -# using -# merge -# constructors -# Some -# Optional -# Text -# List -# equal -# or -# plus -# text_append -# list_append -# and -# times -# double_equal -# not_equal -# dot -# open_brace -# close_brace -# open_bracket -# close_bracket -# open_angle -# close_angle -# bar -# comma -# open_parens -# close_parens -# at -# colon -# import_alt -# combine -# combine_types -# prefer -# lambda -# forall -# arrow -# exponent -# double_literal -# natural_literal_raw -integer_literal -natural_literal -# identifier -# identifier_reserved_prefix -# identifier_reserved_namespaced_prefix -# missing -# path_character -# quoted_path_character -# path_component -# directory -# file -# local_raw -# local -# scheme -# http_raw -# authority -# userinfo -# host -# port -# IP_literal -# IPvFuture -# IPv6address -# h16 -# ls32 -# IPv4address -# dec_octet -# reg_name -# pchar -# query -# fragment -# pct_encoded -# unreserved -# sub_delims -# http -# env -# bash_environment_variable -# posix_environment_variable -# posix_environment_variable_character -# import_type -# hash -# import_hashed -# import -# expression -# annotated_expression -# empty_collection -# non_empty_optional -# operator_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 -# import_expression -# selector_expression -# primitive_expression -# labels -# record_type_or_literal -# non_empty_record_type_or_literal -# non_empty_record_type -# non_empty_record_literal -# union_type_or_literal -# non_empty_union_type_or_literal -# non_empty_list_literal -# complete_expression diff --git a/src/errors/AnnotMismatch.txt b/src/errors/AnnotMismatch.txt deleted file mode 100644 index 4904bf8..0000000 --- a/src/errors/AnnotMismatch.txt +++ /dev/null @@ -1,117 +0,0 @@ -Explanation: Every function declares what type or kind of argument to accept - -For example: - - - ┌───────────────────────────────┐ - │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have type ❰Bool❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ Natural/even : Natural → Bool │ This built-in function only accepts - └───────────────────────────────┘ arguments that have type ❰Natural❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have kind ❰Type❱ - ⇧ - The function's input kind - - - ┌────────────────────┐ - │ List : Type → Type │ This built-in function only accepts arguments that - └────────────────────┘ have kind ❰Type❱ - ⇧ - The function's input kind - - -For example, the following expressions are valid: - - - ┌────────────────────────┐ - │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌─────────────────┐ - │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of - └─────────────────┘ argument that the ❰Natural/even❱ function accepts, - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌───────────┐ - │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument - └───────────┘ that that the ❰List❱ function accepts - - -However, you can $_NOT apply a function to the wrong type or kind of argument - -For example, the following expressions are not valid: - - - ┌───────────────────────┐ - │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function - └───────────────────────┘ expects an argument that has type ❰Bool❱ - - - ┌──────────────────┐ - │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function - └──────────────────┘ expects an argument that has type ❰Natural❱ - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous - └────────────────────────┘ function expects an argument of kind ❰Type❱ - - - ┌────────┐ - │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an - └────────┘ argument that has kind ❰Type❱ - - -You tried to invoke the following function: - -↳ $txt0 - -... which expects an argument of type or kind: - -↳ $txt1 - -... on the following argument: - -↳ $txt2 - -... which has a different type or kind: - -↳ $txt3 - -Some common reasons why you might get this error: - -● You omit a function argument by mistake: - - - ┌────────────────────────────────────────┐ - │ List/head ([1, 2, 3] : List Integer) │ - └────────────────────────────────────────┘ - ⇧ - ❰List/head❱ is missing the first argument, - which should be: ❰Integer❱ - - -● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ - - ┌────────────────┐ - │ Natural/even 2 │ - └────────────────┘ - ⇧ - This should be ❰+2❱ diff --git a/src/errors/CantTextAppend.txt b/src/errors/CantTextAppend.txt deleted file mode 100644 index 26b9ceb..0000000 --- a/src/errors/CantTextAppend.txt +++ /dev/null @@ -1,28 +0,0 @@ -Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱ - -For example, this is a valid use of ❰++❱: - - - ┌────────────────┐ - │ "ABC" ++ "DEF" │ - └────────────────┘ - - -You provided this argument: - -↳ $txt0 - -... which does not have type ❰Text❱ but instead has type: - -↳ $txt1 - -Some common reasons why you might get this error: - -● You might have thought that ❰++❱ was the operator to combine two lists: - - ┌───────────────────────────────────────────────────────────┐ - │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │ Not valid - └───────────────────────────────────────────────────────────┘ - - The Dhall programming language does not provide a built-in operator for - combining two lists diff --git a/src/errors/DuplicateAlternative.txt b/src/errors/DuplicateAlternative.txt deleted file mode 100644 index 077f8aa..0000000 --- a/src/errors/DuplicateAlternative.txt +++ /dev/null @@ -1,18 +0,0 @@ -Explanation: Unions may not have two alternatives that share the same name - -For example, the following expressions are $_NOT valid: - - - ┌─────────────────────────────┐ - │ < foo = True | foo : Text > │ Invalid: ❰foo❱ appears twice - └─────────────────────────────┘ - - - ┌───────────────────────────────────────┐ - │ < foo = 1 | bar : Bool | bar : Text > │ Invalid: ❰bar❱ appears twice - └───────────────────────────────────────┘ - - -You have more than one alternative named: - -↳ $txt0 diff --git a/src/errors/FieldCollision.txt b/src/errors/FieldCollision.txt deleted file mode 100644 index 2b2d260..0000000 --- a/src/errors/FieldCollision.txt +++ /dev/null @@ -1,43 +0,0 @@ -Explanation: You can combine records if they don't share any fields in common, -like this: - - - ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { baz = True } │ - └───────────────────────────────────────────┘ - - - ┌────────────────────────────────────────┐ - │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │ - └────────────────────────────────────────┘ - - -... but you cannot merge two records that share the same field - -For example, the following expression is $_NOT valid: - - - ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ fields - └───────────────────────────────────────────┘ - - -You combined two records that share the following field: - -↳ $txt0 - -... which is not allowed - -Some common reasons why you might get this error: - -● You tried to use ❰∧❱ to update a field's value, like this: - - - ┌────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │ - └────────────────────────────────────────┘ - ⇧ - Invalid attempt to update ❰foo❱'s value to ❰2❱ - - Field updates are intentionally not allowed as the Dhall language discourages - patch-oriented programming diff --git a/src/errors/HandlerInputTypeMismatch.txt b/src/errors/HandlerInputTypeMismatch.txt deleted file mode 100644 index 7d3525b..0000000 --- a/src/errors/HandlerInputTypeMismatch.txt +++ /dev/null @@ -1,49 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... as long as the input type of each handler function matches the type of the -corresponding alternative: - - - ┌───────────────────────────────────────────────────────────┐ - │ union : < Left : Natural | Right : Bool > │ - └───────────────────────────────────────────────────────────┘ - ⇧ ⇧ - These must match These must match - ⇩ ⇩ - ┌───────────────────────────────────────────────────────────┐ - │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │ - └───────────────────────────────────────────────────────────┘ - - -For example, the following expression is $_NOT valid: - - - Invalid: Doesn't match the type of the ❰Right❱ alternative - ⇩ - ┌──────────────────────────────────────────────────────────────────────┐ - │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │ - │ in let union = < Left = +2 | Right : Bool > │ - │ in merge handlers union : Bool │ - └──────────────────────────────────────────────────────────────────────┘ - - -Your handler for the following alternative: - -↳ $txt0 - -... needs to accept an input value of type: - -↳ $txt1 - -... but actually accepts an input value of a different type: - -↳ $txt2 diff --git a/src/errors/HandlerNotAFunction.txt b/src/errors/HandlerNotAFunction.txt deleted file mode 100644 index ff87443..0000000 --- a/src/errors/HandlerNotAFunction.txt +++ /dev/null @@ -1,32 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... as long as each handler is a function - -For example, the following expression is $_NOT valid: - - - ┌─────────────────────────────────────────┐ - │ merge { Foo = True } < Foo = 1 > : Bool │ - └─────────────────────────────────────────┘ - ⇧ - Invalid: Not a function - - -Your handler for this alternative: - -↳ $txt0 - -... has the following type: - -↳ $txt1 - -... which is not the type of a function diff --git a/src/errors/HandlerOutputTypeMismatch.txt b/src/errors/HandlerOutputTypeMismatch.txt deleted file mode 100644 index f359459..0000000 --- a/src/errors/HandlerOutputTypeMismatch.txt +++ /dev/null @@ -1,51 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... as long as the output type of each handler function matches the declared type -of the result: - - - ┌───────────────────────────────────────────────────────────┐ - │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │ - └───────────────────────────────────────────────────────────┘ - ⇧ ⇧ - These output types ... - - ... must match the declared type of the ❰merge❱ - ⇩ - ┌─────────────────────────────┐ - │ merge handlers union : Bool │ - └─────────────────────────────┘ - - -For example, the following expression is $_NOT valid: - - - ┌──────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Text │ - └──────────────────────────────────────────────────────────────────────┘ - ⇧ - Invalid: Doesn't match output of either handler - - -Your handler for the following alternative: - -↳ $txt0 - -... needs to return an output value of type: - -↳ $txt1 - -... but actually returns an output value of a different type: - -↳ $txt2 diff --git a/src/errors/IfBranchMismatch.txt b/src/errors/IfBranchMismatch.txt deleted file mode 100644 index a95b130..0000000 --- a/src/errors/IfBranchMismatch.txt +++ /dev/null @@ -1,63 +0,0 @@ -Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which -is an expression: - - - Expression for ❰then❱ branch - ⇩ - ┌────────────────────────────────┐ - │ if True then "Hello, world!" │ - │ else "Goodbye, world!" │ - └────────────────────────────────┘ - ⇧ - Expression for ❰else❱ branch - - -These two expressions must have the same type. For example, the following ❰if❱ -expressions are all valid: - - - ┌──────────────────────────────────┐ - │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱ - └──────────────────────────────────┘ - - - ┌────────────────────────────┐ - │ λ(b : Bool) → │ - │ if b then Natural/even │ Both branches have type ❰Natural → Bool❱ - │ else Natural/odd │ - └────────────────────────────┘ - - -However, the following expression is $_NOT valid: - - - This branch has type ❰Integer❱ - ⇩ - ┌────────────────────────┐ - │ if True then 0 │ - │ else "ABC" │ - └────────────────────────┘ - ⇧ - This branch has type ❰Text❱ - - -The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is -always ❰True❱ or ❰False❱ - -Your ❰if❱ expression has the following ❰then❱ branch: - -↳ $txt0 - -... which has type: - -↳ $txt2 - -... and the following ❰else❱ branch: - -↳ $txt1 - -... which has a different type: - -↳ $txt3 - -Fix your ❰then❱ and ❰else❱ branches to have matching types diff --git a/src/errors/IfBranchMustBeTerm.txt b/src/errors/IfBranchMustBeTerm.txt deleted file mode 100644 index 4c15881..0000000 --- a/src/errors/IfBranchMustBeTerm.txt +++ /dev/null @@ -1,51 +0,0 @@ -Explanation: Every ❰if❱ expression begins with a predicate which must have type -❰Bool❱ - -For example, these are valid ❰if❱ expressions: - - - ┌──────────────────────────────┐ - │ if True then "Yes" else "No" │ - └──────────────────────────────┘ - ⇧ - Predicate - - - ┌─────────────────────────────────────────┐ - │ λ(x : Bool) → if x then False else True │ - └─────────────────────────────────────────┘ - ⇧ - Predicate - - -... but these are $_NOT valid ❰if❱ expressions: - - - ┌───────────────────────────┐ - │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱ - └───────────────────────────┘ - - - ┌────────────────────────────┐ - │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱ - └────────────────────────────┘ - - -Your ❰if❱ expression begins with the following predicate: - -↳ $txt0 - -... that has type: - -↳ $txt1 - -... but the predicate must instead have type ❰Bool❱ - -Some common reasons why you might get this error: - -● You might be used to other programming languages that accept predicates other - than ❰Bool❱ - - For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat - them as equivalent to ❰False❱. However, the Dhall language does not permit - this diff --git a/src/errors/InvalidAlterantive.txt b/src/errors/InvalidAlterantive.txt deleted file mode 100644 index 391fc3a..0000000 --- a/src/errors/InvalidAlterantive.txt +++ /dev/null @@ -1,48 +0,0 @@ -Explanation: Every union type specifies the type of each alternative, like this: - - - The type of the first alternative is ❰Bool❱ - ⇩ - ┌──────────────────────────────────┐ - │ < Left : Bool, Right : Natural > │ A union type with two alternatives - └──────────────────────────────────┘ - ⇧ - The type of the second alternative is ❰Natural❱ - - -However, these alternatives can only be annotated with types. For example, the -following union types are $_NOT valid: - - - ┌────────────────────────────┐ - │ < Left : Bool, Right : 1 > │ Invalid union type - └────────────────────────────┘ - ⇧ - This is a term and not a type - - - ┌───────────────────────────────┐ - │ < Left : Bool, Right : Type > │ Invalid union type - └───────────────────────────────┘ - ⇧ - This is a kind and not a type - - -You provided a union type with an alternative named: - -↳ $txt0 - -... annotated with the following expression which is not a type: - -↳ $txt1 - -Some common reasons why you might get this error: - -● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one - alternative: - - ┌─────────────────┐ - │ < Example : 1 > │ - └─────────────────┘ - ⇧ - This could be ❰=❱ instead diff --git a/src/errors/InvalidAlterantiveType.txt b/src/errors/InvalidAlterantiveType.txt deleted file mode 100644 index f5dadef..0000000 --- a/src/errors/InvalidAlterantiveType.txt +++ /dev/null @@ -1,49 +0,0 @@ -Explanation: Every union literal begins by selecting one alternative and -specifying the value for that alternative, like this: - - - Select the ❰Left❱ alternative, whose value is ❰True❱ - ⇩ - ┌──────────────────────────────────┐ - │ < Left = True, Right : Natural > │ A union literal with two alternatives - └──────────────────────────────────┘ - - -However, this value must be a term and not a type. For example, the following -values are $_NOT valid: - - - ┌──────────────────────────────────┐ - │ < Left = Text, Right : Natural > │ Invalid union literal - └──────────────────────────────────┘ - ⇧ - This is a type and not a term - - - ┌───────────────────────────────┐ - │ < Left = Type, Right : Type > │ Invalid union type - └───────────────────────────────┘ - ⇧ - This is a kind and not a term - - -You provided a union literal with an alternative named: - -↳ $txt0 - -... whose value is: - -↳ $txt1 - -... which is not a term - -Some common reasons why you might get this error: - -● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one - alternative: - - ┌────────────────────┐ - │ < Example = Text > │ - └────────────────────┘ - ⇧ - This could be ❰:❱ instead diff --git a/src/errors/InvalidField.txt b/src/errors/InvalidField.txt deleted file mode 100644 index bfbf106..0000000 --- a/src/errors/InvalidField.txt +++ /dev/null @@ -1,35 +0,0 @@ -Explanation: Every record literal is a set of fields assigned to values, like -this: - - ┌────────────────────────────────────────┐ - │ { foo = 100, bar = True, baz = "ABC" } │ - └────────────────────────────────────────┘ - -However, fields can only be terms and cannot be types or kinds - -For example, these record literals are $_NOT valid: - - - ┌───────────────────────────┐ - │ { foo = 100, bar = Text } │ - └───────────────────────────┘ - ⇧ - ❰Text❱ is a type and not a term - - - ┌───────────────────────────┐ - │ { foo = 100, bar = Type } │ - └───────────────────────────┘ - ⇧ - ❰Type❱ is a kind and not a term - - -You provided a record literal with a key named: - -↳ $txt0 - -... whose value is: - -↳ $txt1 - -... which is not a term diff --git a/src/errors/InvalidFieldType.txt b/src/errors/InvalidFieldType.txt deleted file mode 100644 index 4f76a64..0000000 --- a/src/errors/InvalidFieldType.txt +++ /dev/null @@ -1,34 +0,0 @@ -Explanation: Every record type documents the type of each field, like this: - - ┌──────────────────────────────────────────────┐ - │ { foo : Integer, bar : Integer, baz : Text } │ - └──────────────────────────────────────────────┘ - -However, fields cannot be annotated with expressions other than types - -For example, these record types are $_NOT valid: - - - ┌────────────────────────────┐ - │ { foo : Integer, bar : 1 } │ - └────────────────────────────┘ - ⇧ - ❰1❱ is an ❰Integer❱ and not a ❰Type❱ - - - ┌───────────────────────────────┐ - │ { foo : Integer, bar : Type } │ - └───────────────────────────────┘ - ⇧ - ❰Type❱ is a ❰Kind❱ and not a ❰Type❱ - - -You provided a record type with a key named: - -↳ $txt0 - -... annotated with the following expression: - -↳ $txt1 - -... which is not a type diff --git a/src/errors/InvalidInputType.txt b/src/errors/InvalidInputType.txt deleted file mode 100644 index eabafa4..0000000 --- a/src/errors/InvalidInputType.txt +++ /dev/null @@ -1,61 +0,0 @@ -Explanation: A function can accept an input "term" that has a given "type", like -this: - - - This is the input term that the function accepts - ⇩ - ┌───────────────────────┐ - │ ∀(x : Natural) → Bool │ This is the type of a function that accepts an - └───────────────────────┘ input term named ❰x❱ that has type ❰Natural❱ - ⇧ - This is the type of the input term - - - ┌────────────────┐ - │ Bool → Integer │ This is the type of a function that accepts an anonymous - └────────────────┘ input term that has type ❰Bool❱ - ⇧ - This is the type of the input term - - -... or a function can accept an input "type" that has a given "kind", like this: - - - This is the input type that the function accepts - ⇩ - ┌────────────────────┐ - │ ∀(a : Type) → Type │ This is the type of a function that accepts an input - └────────────────────┘ type named ❰a❱ that has kind ❰Type❱ - ⇧ - This is the kind of the input type - - - ┌──────────────────────┐ - │ (Type → Type) → Type │ This is the type of a function that accepts an - └──────────────────────┘ anonymous input type that has kind ❰Type → Type❱ - ⇧ - This is the kind of the input type - - -Other function inputs are $_NOT valid, like this: - - - ┌──────────────┐ - │ ∀(x : 1) → x │ ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱ - └──────────────┘ cannot have "type" ❰1❱ or "kind" ❰1❱ - ⇧ - This is not a type or kind - - - ┌──────────┐ - │ True → x │ ❰True❱ is a "term" and not a "type" nor a "kind" so the - └──────────┘ anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱ - ⇧ - This is not a type or kind - - -You annotated a function input with the following expression: - -↳ $txt - -... which is neither a type nor a kind diff --git a/src/errors/InvalidListElement.txt b/src/errors/InvalidListElement.txt deleted file mode 100644 index 59db7b7..0000000 --- a/src/errors/InvalidListElement.txt +++ /dev/null @@ -1,30 +0,0 @@ -Explanation: Every element in the list must have a type matching the type -annotation at the end of the list - -For example, this is a valid ❰List❱: - - - ┌──────────────────────────┐ - │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱ - └──────────────────────────┘ - - -.. but this is $_NOT a valid ❰List❱: - - - ┌──────────────────────────────┐ - │ [1, "ABC", 3] : List Integer │ The second element is not an ❰Integer❱ - └──────────────────────────────┘ - - -Your ❰List❱ elements should have this type: - -↳ $txt0 - -... but the following element at index $txt1: - -↳ $txt2 - -... has this type instead: - -↳ $txt3 diff --git a/src/errors/InvalidListType.txt b/src/errors/InvalidListType.txt deleted file mode 100644 index 676647e..0000000 --- a/src/errors/InvalidListType.txt +++ /dev/null @@ -1,43 +0,0 @@ -Explanation: Every ❰List❱ documents the type of its elements with a type -annotation, like this: - - - ┌──────────────────────────┐ - │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s - └──────────────────────────┘ - ⇧ - The type of the ❰List❱'s elements, which are ❰Integer❱s - - - ┌───────────────────┐ - │ [] : List Integer │ An empty ❰List❱ - └───────────────────┘ - ⇧ - You still specify the type even when the ❰List❱ is empty - - -The element type must be a type and not something else. For example, the -following element types are $_NOT valid: - - - ┌──────────────┐ - │ ... : List 1 │ - └──────────────┘ - ⇧ - This is an ❰Integer❱ and not a ❰Type❱ - - - ┌─────────────────┐ - │ ... : List Type │ - └─────────────────┘ - ⇧ - This is a ❰Kind❱ and not a ❰Type❱ - - -Even if the ❰List❱ is empty you still must specify a valid type - -You declared that the ❰List❱'s elements should have type: - -↳ $txt0 - -... which is not a ❰Type❱ diff --git a/src/errors/InvalidOptionType.txt b/src/errors/InvalidOptionType.txt deleted file mode 100644 index 3bc81de..0000000 --- a/src/errors/InvalidOptionType.txt +++ /dev/null @@ -1,44 +0,0 @@ -Explanation: Every optional element ends with a type annotation for the element -that might be present, like this: - - - ┌────────────────────────┐ - │ [1] : Optional Integer │ An optional element that's present - └────────────────────────┘ - ⇧ - The type of the ❰Optional❱ element, which is an ❰Integer❱ - - - ┌────────────────────────┐ - │ [] : Optional Integer │ An optional element that's absent - └────────────────────────┘ - ⇧ - You still specify the type even when the element is absent - - -The element type must be a type and not something else. For example, the -following element types are $_NOT valid: - - - ┌──────────────────┐ - │ ... : Optional 1 │ - └──────────────────┘ - ⇧ - This is an ❰Integer❱ and not a ❰Type❱ - - - ┌─────────────────────┐ - │ ... : Optional Type │ - └─────────────────────┘ - ⇧ - This is a ❰Kind❱ and not a ❰Type❱ - - -Even if the element is absent you still must specify a valid type - -You declared that the ❰Optional❱ element should have type: - -↳ $txt0 - -... which is not a ❰Type❱ - diff --git a/src/errors/InvalidOptionalElement.txt b/src/errors/InvalidOptionalElement.txt deleted file mode 100644 index 0254220..0000000 --- a/src/errors/InvalidOptionalElement.txt +++ /dev/null @@ -1,29 +0,0 @@ -Explanation: An ❰Optional❱ element must have a type matching the type annotation - -For example, this is a valid ❰Optional❱ value: - - - ┌────────────────────────┐ - │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type - └────────────────────────┘ - - -... but this is $_NOT a valid ❰Optional❱ value: - - - ┌────────────────────────────┐ - │ ["ABC"] : Optional Integer │ ❰"ABC"❱ is not an ❰Integer❱ - └────────────────────────────┘ - - -Your ❰Optional❱ element should have this type: - -↳ $txt0 - -... but the element you provided: - -↳ $txt1 - -... has this type instead: - -↳ $txt2 diff --git a/src/errors/InvalidOptionalLiteral.txt b/src/errors/InvalidOptionalLiteral.txt deleted file mode 100644 index 41c0fdc..0000000 --- a/src/errors/InvalidOptionalLiteral.txt +++ /dev/null @@ -1,53 +0,0 @@ -Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s: - - - ┌───────────────────────┐ - │ [] : Optional Integer │ An ❰Optional❱ value which is absent - └───────────────────────┘ - - - ┌───────────────────────┐ - │ [] : List Integer │ An empty (0-element) ❰List❱ - └───────────────────────┘ - - - ┌────────────────────────┐ - │ [1] : Optional Integer │ An ❰Optional❱ value which is present - └────────────────────────┘ - - - ┌────────────────────────┐ - │ [1] : List Integer │ A singleton (1-element) ❰List❱ - └────────────────────────┘ - - -However, an ❰Optional❱ value can $_NOT have more than one element, whereas a -❰List❱ can have multiple elements: - - - ┌───────────────────────────┐ - │ [1, 2] : Optional Integer │ Invalid: multiple elements $_NOT allowed - └───────────────────────────┘ - - - ┌───────────────────────────┐ - │ [1, 2] : List Integer │ Valid: multiple elements allowed - └───────────────────────────┘ - - -Your ❰Optional❱ value had this many elements: - -↳ $txt0 - -... when an ❰Optional❱ value can only have at most one element - -Some common reasons why you might get this error: - -● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this: - - - ┌────────────────────────────────────────────────────┐ - │ List/length Integer ([1, 2, 3] : Optional Integer) │ - └────────────────────────────────────────────────────┘ - ⇧ - This should be ❰List❱ instead diff --git a/src/errors/InvalidOutputType.txt b/src/errors/InvalidOutputType.txt deleted file mode 100644 index dd2695d..0000000 --- a/src/errors/InvalidOutputType.txt +++ /dev/null @@ -1,68 +0,0 @@ -Explanation: A function can return an output "term" that has a given "type", -like this: - - - ┌────────────────────┐ - │ ∀(x : Text) → Bool │ This is the type of a function that returns an - └────────────────────┘ output term that has type ❰Bool❱ - ⇧ - This is the type of the output term - - - ┌────────────────┐ - │ Bool → Integer │ This is the type of a function that returns an output - └────────────────┘ term that has type ❰Int❱ - ⇧ - This is the type of the output term - - -... or a function can return an output "type" that has a given "kind", like -this: - - ┌────────────────────┐ - │ ∀(a : Type) → Type │ This is the type of a function that returns an - └────────────────────┘ output type that has kind ❰Type❱ - ⇧ - This is the kind of the output type - - - ┌──────────────────────┐ - │ (Type → Type) → Type │ This is the type of a function that returns an - └──────────────────────┘ output type that has kind ❰Type❱ - ⇧ - This is the kind of the output type - - -Other outputs are $_NOT valid, like this: - - - ┌─────────────────┐ - │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the - └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱ - ⇧ - This is not a type or kind - - - ┌─────────────┐ - │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the - └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱ - ⇧ - This is not a type or kind - - -You specified that your function outputs a: - -↳ $txt - -... which is neither a type nor a kind: - -Some common reasons why you might get this error: - -● You use ❰∀❱ instead of ❰λ❱ by mistake, like this: - - - ┌────────────────┐ - │ ∀(x: Bool) → x │ - └────────────────┘ - ⇧ - Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function diff --git a/src/errors/InvalidPredicate.txt b/src/errors/InvalidPredicate.txt deleted file mode 100644 index 4c15881..0000000 --- a/src/errors/InvalidPredicate.txt +++ /dev/null @@ -1,51 +0,0 @@ -Explanation: Every ❰if❱ expression begins with a predicate which must have type -❰Bool❱ - -For example, these are valid ❰if❱ expressions: - - - ┌──────────────────────────────┐ - │ if True then "Yes" else "No" │ - └──────────────────────────────┘ - ⇧ - Predicate - - - ┌─────────────────────────────────────────┐ - │ λ(x : Bool) → if x then False else True │ - └─────────────────────────────────────────┘ - ⇧ - Predicate - - -... but these are $_NOT valid ❰if❱ expressions: - - - ┌───────────────────────────┐ - │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱ - └───────────────────────────┘ - - - ┌────────────────────────────┐ - │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱ - └────────────────────────────┘ - - -Your ❰if❱ expression begins with the following predicate: - -↳ $txt0 - -... that has type: - -↳ $txt1 - -... but the predicate must instead have type ❰Bool❱ - -Some common reasons why you might get this error: - -● You might be used to other programming languages that accept predicates other - than ❰Bool❱ - - For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat - them as equivalent to ❰False❱. However, the Dhall language does not permit - this diff --git a/src/errors/MissingField.txt b/src/errors/MissingField.txt deleted file mode 100644 index de14a33..0000000 --- a/src/errors/MissingField.txt +++ /dev/null @@ -1,30 +0,0 @@ -Explanation: You can only access fields on records, like this: - - - ┌─────────────────────────────────┐ - │ { foo = True, bar = "ABC" }.foo │ This is valid ... - └─────────────────────────────────┘ - - - ┌───────────────────────────────────────────┐ - │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this - └───────────────────────────────────────────┘ - - -... but you can only access fields if they are present - -For example, the following expression is $_NOT valid: - - ┌─────────────────────────────────┐ - │ { foo = True, bar = "ABC" }.qux │ - └─────────────────────────────────┘ - ⇧ - Invalid: the record has no ❰qux❱ field - -You tried to access a field named: - -↳ $txt0 - -... but the field is missing because the record only defines the following fields: - -↳ $txt1 diff --git a/src/errors/MissingHandler.txt b/src/errors/MissingHandler.txt deleted file mode 100644 index 433445e..0000000 --- a/src/errors/MissingHandler.txt +++ /dev/null @@ -1,32 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... but you must provide exactly one handler per alternative in the union. You -cannot omit any handlers - -For example, the following expression is $_NOT valid: - - - Invalid: Missing ❰Right❱ handler - ⇩ - ┌─────────────────────────────────────────────────┐ - │ let handlers = { Left = Natural/even } │ - │ in let union = < Left = +2 | Right : Bool > │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────┘ - - -Note that you need to provide handlers for other alternatives even if those -alternatives are never used - -You need to supply the following handlers: - -↳ $txt0 diff --git a/src/errors/MustCombineARecord.txt b/src/errors/MustCombineARecord.txt deleted file mode 100644 index 141b969..0000000 --- a/src/errors/MustCombineARecord.txt +++ /dev/null @@ -1,46 +0,0 @@ -Explanation: You can combine records using the ❰∧❱ operator, like this: - - - ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { baz = True } │ - └───────────────────────────────────────────┘ - - - ┌─────────────────────────────────────────────┐ - │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │ - └─────────────────────────────────────────────┘ - - -... but you cannot combine values that are not records. - -For example, the following expressions are $_NOT valid: - - - ┌──────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ 1 │ - └──────────────────────────────┘ - ⇧ - Invalid: Not a record - - - ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │ - └───────────────────────────────────────────┘ - ⇧ - Invalid: This is a record type and not a record - - - ┌───────────────────────────────────────────┐ - │ { foo = 1, bar = "ABC" } ∧ < baz = True > │ - └───────────────────────────────────────────┘ - ⇧ - Invalid: This is a union and not a record - - -You tried to combine the following value: - -↳ $txt0 - -... which is not a record, but is actually a: - -↳ $txt1 diff --git a/src/errors/MustMergeARecord.txt b/src/errors/MustMergeARecord.txt deleted file mode 100644 index 79094bd..0000000 --- a/src/errors/MustMergeARecord.txt +++ /dev/null @@ -1,43 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... but the first argument to ❰merge❱ must be a record and not some other type. - -For example, the following expression is $_NOT valid: - - - ┌─────────────────────────────────────────┐ - │ let handler = λ(x : Bool) → x │ - │ in merge handler < Foo = True > : True │ - └─────────────────────────────────────────┘ - ⇧ - Invalid: ❰handler❱ isn't a record - - -You provided the following handler: - -↳ $txt0 - -... which is not a record, but is actually a value of type: - -↳ $txt1 - -Some common reasons why you might get this error: - -● You accidentally provide an empty record type instead of an empty record when - you ❰merge❱ an empty union: - - - ┌──────────────────────────────────────────┐ - │ λ(x : <>) → λ(a : Type) → merge {} x : a │ - └──────────────────────────────────────────┘ - ⇧ - This should be ❰{=}❱ instead diff --git a/src/errors/MustMergeUnion.txt b/src/errors/MustMergeUnion.txt deleted file mode 100644 index 68df70c..0000000 --- a/src/errors/MustMergeUnion.txt +++ /dev/null @@ -1,31 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... but the second argument to ❰merge❱ must be a union and not some other type. - -For example, the following expression is $_NOT valid: - - - ┌──────────────────────────────────────────┐ - │ let handlers = { Foo = λ(x : Bool) → x } │ - │ in merge handlers True : True │ - └──────────────────────────────────────────┘ - ⇧ - Invalid: ❰True❱ isn't a union - - -You tried to ❰merge❱ this expression: - -↳ $txt0 - -... which is not a union, but is actually a value of type: - -↳ $txt1 diff --git a/src/errors/NoDependentLet.txt b/src/errors/NoDependentLet.txt deleted file mode 100644 index fdc65b4..0000000 --- a/src/errors/NoDependentLet.txt +++ /dev/null @@ -1,76 +0,0 @@ -Explanation: The Dhall programming language does not allow ❰let❱ expressions -from terms to types. These ❰let❱ expressions are also known as "dependent ❰let❱ -expressions" because you have a type whose value depends on the value of a term. - -The Dhall language forbids these dependent ❰let❱ expressions in order to -guarantee that ❰let❱ expressions of the form: - - - ┌────────────────────┐ - │ let x : t = r in e │ - └────────────────────┘ - - -... are always equivalent to: - - - ┌──────────────────┐ - │ (λ(x : t) → e) r │ - └──────────────────┘ - - -This means that both expressions should normalize to the same result and if one -of the two fails to type check then the other should fail to type check, too. - -For this reason, the following is $_NOT legal code: - - - ┌───────────────────┐ - │ let x = 2 in Text │ - └───────────────────┘ - - -... because the above ❰let❱ expression is equivalent to: - - - ┌─────────────────────────────┐ - │ let x : Integer = 2 in Text │ - └─────────────────────────────┘ - - -... which in turn must be equivalent to: - - - ┌───────────────────────────┐ - │ (λ(x : Integer) → Text) 2 │ - └───────────────────────────┘ - - -... which in turn fails to type check because this sub-expression: - - - ┌───────────────────────┐ - │ λ(x : Integer) → Text │ - └───────────────────────┘ - - -... has type: - - - ┌───────────────────────┐ - │ ∀(x : Integer) → Text │ - └───────────────────────┘ - - -... which is a forbidden dependent function type (i.e. a function from a term to -a type). Therefore the equivalent ❰let❱ expression is also forbidden. - -Your ❰let❱ expression is invalid because the input has type: - -↳ $txt0 - -... and the output has kind: - -↳ $txt1 - -... which makes this a forbidden dependent ❰let❱ expression diff --git a/src/errors/NoDependentTypes.txt b/src/errors/NoDependentTypes.txt deleted file mode 100644 index 435bdcb..0000000 --- a/src/errors/NoDependentTypes.txt +++ /dev/null @@ -1,31 +0,0 @@ -Explanation: The Dhall programming language does not allow functions from terms -to types. These function types are also known as "dependent function types" -because you have a type whose value "depends" on the value of a term. - -For example, this is $_NOT a legal function type: - - - ┌─────────────┐ - │ Bool → Type │ - └─────────────┘ - - -Similarly, this is $_NOT legal code: - - - ┌────────────────────────────────────────────────────┐ - │ λ(Vector : Natural → Type → Type) → Vector +0 Text │ - └────────────────────────────────────────────────────┘ - ⇧ - Invalid dependent type - - -Your function type is invalid because the input has type: - -↳ $txt0 - -... and the output has kind: - -↳ $txt1 - -... which makes this a forbidden dependent function type diff --git a/src/errors/NotAFunction.txt b/src/errors/NotAFunction.txt deleted file mode 100644 index dd2695d..0000000 --- a/src/errors/NotAFunction.txt +++ /dev/null @@ -1,68 +0,0 @@ -Explanation: A function can return an output "term" that has a given "type", -like this: - - - ┌────────────────────┐ - │ ∀(x : Text) → Bool │ This is the type of a function that returns an - └────────────────────┘ output term that has type ❰Bool❱ - ⇧ - This is the type of the output term - - - ┌────────────────┐ - │ Bool → Integer │ This is the type of a function that returns an output - └────────────────┘ term that has type ❰Int❱ - ⇧ - This is the type of the output term - - -... or a function can return an output "type" that has a given "kind", like -this: - - ┌────────────────────┐ - │ ∀(a : Type) → Type │ This is the type of a function that returns an - └────────────────────┘ output type that has kind ❰Type❱ - ⇧ - This is the kind of the output type - - - ┌──────────────────────┐ - │ (Type → Type) → Type │ This is the type of a function that returns an - └──────────────────────┘ output type that has kind ❰Type❱ - ⇧ - This is the kind of the output type - - -Other outputs are $_NOT valid, like this: - - - ┌─────────────────┐ - │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the - └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱ - ⇧ - This is not a type or kind - - - ┌─────────────┐ - │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the - └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱ - ⇧ - This is not a type or kind - - -You specified that your function outputs a: - -↳ $txt - -... which is neither a type nor a kind: - -Some common reasons why you might get this error: - -● You use ❰∀❱ instead of ❰λ❱ by mistake, like this: - - - ┌────────────────┐ - │ ∀(x: Bool) → x │ - └────────────────┘ - ⇧ - Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function diff --git a/src/errors/NotARecord.txt b/src/errors/NotARecord.txt deleted file mode 100644 index e0eebc8..0000000 --- a/src/errors/NotARecord.txt +++ /dev/null @@ -1,48 +0,0 @@ -Explanation: You can only access fields on records, like this: - - - ┌─────────────────────────────────┐ - │ { foo = True, bar = "ABC" }.foo │ This is valid ... - └─────────────────────────────────┘ - - - ┌───────────────────────────────────────────┐ - │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this - └───────────────────────────────────────────┘ - - -... but you cannot access fields on non-record expressions - -For example, the following expression is $_NOT valid: - - - ┌───────┐ - │ 1.foo │ - └───────┘ - ⇧ - Invalid: Not a record - - -You tried to access a field named: - -↳ $txt0 - -... on the following expression which is not a record: - -↳ $txt1 - -... but is actually an expression of type: - -↳ $txt2 - -Some common reasons why you might get this error: - -● You accidentally try to access a field of a union instead of a record, like - this: - - - ┌─────────────────┐ - │ < foo : a >.foo │ - └─────────────────┘ - ⇧ - This is a union, not a record diff --git a/src/errors/TypeMismatch.txt b/src/errors/TypeMismatch.txt deleted file mode 100644 index 4904bf8..0000000 --- a/src/errors/TypeMismatch.txt +++ /dev/null @@ -1,117 +0,0 @@ -Explanation: Every function declares what type or kind of argument to accept - -For example: - - - ┌───────────────────────────────┐ - │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have type ❰Bool❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ Natural/even : Natural → Bool │ This built-in function only accepts - └───────────────────────────────┘ arguments that have type ❰Natural❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have kind ❰Type❱ - ⇧ - The function's input kind - - - ┌────────────────────┐ - │ List : Type → Type │ This built-in function only accepts arguments that - └────────────────────┘ have kind ❰Type❱ - ⇧ - The function's input kind - - -For example, the following expressions are valid: - - - ┌────────────────────────┐ - │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌─────────────────┐ - │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of - └─────────────────┘ argument that the ❰Natural/even❱ function accepts, - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌───────────┐ - │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument - └───────────┘ that that the ❰List❱ function accepts - - -However, you can $_NOT apply a function to the wrong type or kind of argument - -For example, the following expressions are not valid: - - - ┌───────────────────────┐ - │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function - └───────────────────────┘ expects an argument that has type ❰Bool❱ - - - ┌──────────────────┐ - │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function - └──────────────────┘ expects an argument that has type ❰Natural❱ - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous - └────────────────────────┘ function expects an argument of kind ❰Type❱ - - - ┌────────┐ - │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an - └────────┘ argument that has kind ❰Type❱ - - -You tried to invoke the following function: - -↳ $txt0 - -... which expects an argument of type or kind: - -↳ $txt1 - -... on the following argument: - -↳ $txt2 - -... which has a different type or kind: - -↳ $txt3 - -Some common reasons why you might get this error: - -● You omit a function argument by mistake: - - - ┌────────────────────────────────────────┐ - │ List/head ([1, 2, 3] : List Integer) │ - └────────────────────────────────────────┘ - ⇧ - ❰List/head❱ is missing the first argument, - which should be: ❰Integer❱ - - -● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ - - ┌────────────────┐ - │ Natural/even 2 │ - └────────────────┘ - ⇧ - This should be ❰+2❱ diff --git a/src/errors/UnboundVariable.txt b/src/errors/UnboundVariable.txt deleted file mode 100644 index bd7d483..0000000 --- a/src/errors/UnboundVariable.txt +++ /dev/null @@ -1,97 +0,0 @@ -Explanation: Expressions can only reference previously introduced (i.e. "bound") -variables that are still "in scope" - -For example, the following valid expressions introduce a "bound" variable named -❰x❱: - - - ┌─────────────────┐ - │ λ(x : Bool) → x │ Anonymous functions introduce "bound" variables - └─────────────────┘ - ⇧ - This is the bound variable - - - ┌─────────────────┐ - │ let x = 1 in x │ ❰let❱ expressions introduce "bound" variables - └─────────────────┘ - ⇧ - This is the bound variable - - -However, the following expressions are not valid because they all reference a -variable that has not been introduced yet (i.e. an "unbound" variable): - - - ┌─────────────────┐ - │ λ(x : Bool) → y │ The variable ❰y❱ hasn't been introduced yet - └─────────────────┘ - ⇧ - This is the unbound variable - - - ┌──────────────────────────┐ - │ (let x = True in x) && x │ ❰x❱ is undefined outside the parentheses - └──────────────────────────┘ - ⇧ - This is the unbound variable - - - ┌────────────────┐ - │ let x = x in x │ The definition for ❰x❱ cannot reference itself - └────────────────┘ - ⇧ - This is the unbound variable - - -Some common reasons why you might get this error: - -● You misspell a variable name, like this: - - - ┌────────────────────────────────────────────────────┐ - │ λ(empty : Bool) → if emty then "Empty" else "Full" │ - └────────────────────────────────────────────────────┘ - ⇧ - Typo - - -● You misspell a reserved identifier, like this: - - - ┌──────────────────────────┐ - │ foral (a : Type) → a → a │ - └──────────────────────────┘ - ⇧ - Typo - - -● You tried to define a recursive value, like this: - - - ┌─────────────────────┐ - │ let x = x + +1 in x │ - └─────────────────────┘ - ⇧ - Recursive definitions are not allowed - - -● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱ - - - Unbound variable - ⇩ - ┌─────────────────┐ - │ (x : Bool) → x │ - └─────────────────┘ - ⇧ - A ❰λ❱ here would transform this into a valid anonymous function - - - Unbound variable - ⇩ - ┌────────────────────┐ - │ (x : Bool) → Bool │ - └────────────────────┘ - ⇧ - A ❰∀❱ or ❰forall❱ here would transform this into a valid function type diff --git a/src/errors/Untyped.txt b/src/errors/Untyped.txt deleted file mode 100644 index 4904bf8..0000000 --- a/src/errors/Untyped.txt +++ /dev/null @@ -1,117 +0,0 @@ -Explanation: Every function declares what type or kind of argument to accept - -For example: - - - ┌───────────────────────────────┐ - │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have type ❰Bool❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ Natural/even : Natural → Bool │ This built-in function only accepts - └───────────────────────────────┘ arguments that have type ❰Natural❱ - ⇧ - The function's input type - - - ┌───────────────────────────────┐ - │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts - └───────────────────────────────┘ arguments that have kind ❰Type❱ - ⇧ - The function's input kind - - - ┌────────────────────┐ - │ List : Type → Type │ This built-in function only accepts arguments that - └────────────────────┘ have kind ❰Type❱ - ⇧ - The function's input kind - - -For example, the following expressions are valid: - - - ┌────────────────────────┐ - │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌─────────────────┐ - │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of - └─────────────────┘ argument that the ❰Natural/even❱ function accepts, - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind - └────────────────────────┘ of argument that the anonymous function accepts - - - ┌───────────┐ - │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument - └───────────┘ that that the ❰List❱ function accepts - - -However, you can $_NOT apply a function to the wrong type or kind of argument - -For example, the following expressions are not valid: - - - ┌───────────────────────┐ - │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function - └───────────────────────┘ expects an argument that has type ❰Bool❱ - - - ┌──────────────────┐ - │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function - └──────────────────┘ expects an argument that has type ❰Natural❱ - - - ┌────────────────────────┐ - │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous - └────────────────────────┘ function expects an argument of kind ❰Type❱ - - - ┌────────┐ - │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an - └────────┘ argument that has kind ❰Type❱ - - -You tried to invoke the following function: - -↳ $txt0 - -... which expects an argument of type or kind: - -↳ $txt1 - -... on the following argument: - -↳ $txt2 - -... which has a different type or kind: - -↳ $txt3 - -Some common reasons why you might get this error: - -● You omit a function argument by mistake: - - - ┌────────────────────────────────────────┐ - │ List/head ([1, 2, 3] : List Integer) │ - └────────────────────────────────────────┘ - ⇧ - ❰List/head❱ is missing the first argument, - which should be: ❰Integer❱ - - -● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ - - ┌────────────────┐ - │ Natural/even 2 │ - └────────────────┘ - ⇧ - This should be ❰+2❱ diff --git a/src/errors/UnusedHandler.txt b/src/errors/UnusedHandler.txt deleted file mode 100644 index 2e46a12..0000000 --- a/src/errors/UnusedHandler.txt +++ /dev/null @@ -1,32 +0,0 @@ -Explanation: You can ❰merge❱ the alternatives of a union using a record with one -handler per alternative, like this: - - - ┌─────────────────────────────────────────────────────────────────────┐ - │ let union = < Left = +2 | Right : Bool > │ - │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ - │ in merge handlers union : Bool │ - └─────────────────────────────────────────────────────────────────────┘ - - -... but you must provide exactly one handler per alternative in the union. You -cannot supply extra handlers - -For example, the following expression is $_NOT valid: - - - ┌───────────────────────────────────────┐ - │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing - │ in let handlers = │ - │ { Left = Natural/even │ - │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used - │ } │ - │ in merge handlers union : Bool │ - └───────────────────────────────────────┘ - - -You provided the following handlers: - -↳ $txt0 - -... which had no matching alternatives in the union you tried to ❰merge❱ diff --git a/src/generated_parser.rs b/src/generated_parser.rs deleted file mode 100644 index 452b4cd..0000000 --- a/src/generated_parser.rs +++ /dev/null @@ -1,6 +0,0 @@ -#[allow(unused_imports)] -use pest_derive::*; - -#[derive(Parser)] -#[grammar = "dhall.pest"] -pub struct DhallParser; diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop deleted file mode 100644 index 150961f..0000000 --- a/src/grammar.lalrpop +++ /dev/null @@ -1,162 +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::BuiltinType::*; -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> ":" <Expr> => bx(Annot(<>)), - 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(c, a)), - ExprC, -}; - -ListLike: ExprListFn<'input> = { - List => ListLit, - Optional => OptionalLit, -}; - -BoolOr: ExprOpFn<'input> = { "||" => BoolOr }; -NaturalPlus: ExprOpFn<'input> = { "+" => NaturalPlus }; -TextAppend: ExprOpFn<'input> = { "++" => TextAppend }; -BoolAnd: ExprOpFn<'input> = { "&&" => BoolAnd }; -CombineOp: ExprOpFn<'input> = { Combine => Combine }; -NaturalTimes: ExprOpFn<'input> = { "*" => NaturalTimes }; -BoolEQ: ExprOpFn<'input> = { "==" => BoolEQ }; -BoolNE: ExprOpFn<'input> = { "!=" => BoolNE }; - -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(BuiltinType(List)), - Optional => bx(BuiltinType(Optional)), - Builtin => bx(builtin_expr(<>)), - 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/src/grammar_util.rs b/src/grammar_util.rs deleted file mode 100644 index c546a13..0000000 --- a/src/grammar_util.rs +++ /dev/null @@ -1,14 +0,0 @@ -use crate::core::{Expr, X}; -use crate::lexer::Builtin; - -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(BoxExpr<'i>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>; - -pub fn builtin_expr<'i, S, A>(b: Builtin) -> Expr<'i, S, A> { - match b { - Builtin::Type(t) => Expr::BuiltinType(t), - Builtin::Value(v) => Expr::BuiltinValue(v), - } -} diff --git a/src/lexer.rs b/src/lexer.rs deleted file mode 100644 index 5b4dcaa..0000000 --- a/src/lexer.rs +++ /dev/null @@ -1,378 +0,0 @@ -use nom::*; - -use crate::core::Const; -use crate::core::BuiltinType; -use crate::core::BuiltinType::*; -use crate::core::BuiltinValue; -use crate::core::BuiltinValue::*; - -#[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 Builtin { - Type(BuiltinType), - Value(BuiltinValue), -} - -#[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::IResult::*;; - use nom::ErrorKind; - 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!(Builtin::Value(NaturalFold), ident_tag!("Natural/fold")) | - value!(Builtin::Value(NaturalBuild), ident_tag!("Natural/build")) | - value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) | - value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) | - value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) | - value!(Builtin::Value(NaturalShow), ident_tag!("Natural/show")) | - value!(Builtin::Type(Natural), ident_tag!("Natural")) | - value!(Builtin::Type(Integer), ident_tag!("Integer")) | - value!(Builtin::Type(Double), ident_tag!("Double")) | - value!(Builtin::Type(Text), ident_tag!("Text")) | - value!(Builtin::Value(ListBuild), ident_tag!("List/build")) | - value!(Builtin::Value(ListFold), ident_tag!("List/fold")) | - value!(Builtin::Value(ListLength), ident_tag!("List/length")) | - value!(Builtin::Value(ListHead), ident_tag!("List/head")) | - value!(Builtin::Value(ListLast), ident_tag!("List/last")) | - value!(Builtin::Value(ListIndexed), ident_tag!("List/indexed")) | - value!(Builtin::Value(ListReverse), ident_tag!("List/reverse")) | - value!(Builtin::Value(OptionalFold), ident_tag!("Optional/fold")) | - value!(Builtin::Type(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(self::Builtin::Type(crate::core::BuiltinType::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/src/lib.rs b/src/lib.rs deleted file mode 100644 index e07071d..0000000 --- a/src/lib.rs +++ /dev/null @@ -1,12 +0,0 @@ -#![feature(box_patterns)] - -pub mod context; -mod core; -pub use crate::core::*; -use lalrpop_util::lalrpop_mod; -lalrpop_mod!(pub grammar); // synthesized by LALRPOP -mod grammar_util; -mod generated_parser; -pub mod lexer; -pub mod parser; -pub mod typecheck; diff --git a/src/main.rs b/src/main.rs deleted file mode 100644 index cdab3c0..0000000 --- a/src/main.rs +++ /dev/null @@ -1,101 +0,0 @@ -use std::io::{self, Read}; -use std::error::Error; -use term_painter::ToStyle; - -use dhall::*; - -const ERROR_STYLE: term_painter::Color = term_painter::Color::Red; -const BOLD: term_painter::Attr = term_painter::Attr::Bold; - -fn print_error(message: &str, source: &str, start: usize, end: usize) { - let line_number = bytecount::count(source[..start].as_bytes(), b'\n'); - let line_start = source[..start].rfind('\n').map(|i| i + 1).unwrap_or(0); - let line_end = source[end..].find('\n').unwrap_or(0) + end; - let context_prefix = &source[line_start..start]; - let context_highlighted = &source[start..end]; - let context_suffix = &source[end..line_end]; - - let line_number_str = line_number.to_string(); - let line_number_width = line_number_str.len(); - - BOLD.with(|| { - ERROR_STYLE.with(|| { - print!("error: "); - }); - println!("{}", message); - }); - BOLD.with(|| { - print!(" -->"); - }); - println!(" {}:{}:0", "(stdin)", line_number); - BOLD.with(|| { - println!("{:w$} |", "", w = line_number_width); - print!("{} |", line_number_str); - }); - print!(" {}", context_prefix); - BOLD.with(|| { - ERROR_STYLE.with(|| { - print!("{}", context_highlighted); - }); - }); - println!("{}", context_suffix); - BOLD.with(|| { - print!("{:w$} |", "", w = line_number_width); - ERROR_STYLE.with(|| { - println!(" {:so$}{:^>ew$}", "", "", - so = source[line_start..start].chars().count(), - ew = ::std::cmp::max(1, source[start..end].chars().count())); - }); - }); -} - -fn main() { - let mut buffer = String::new(); - io::stdin().read_to_string(&mut buffer).unwrap(); - let expr = match parser::parse_expr(&buffer) { - Ok(e) => e, - Err(lalrpop_util::ParseError::User { error: lexer::LexicalError::Error(pos, e) }) => { - print_error(&format!("Unexpected token {:?}", e), &buffer, pos, pos); - return; - } - Err(lalrpop_util::ParseError::UnrecognizedToken { token: Some((start, t, end)), expected: e }) => { - print_error(&format!("Unrecognized token {:?}", t), &buffer, start, end); - if !e.is_empty() { - println!("Expected {:?}", e); - } - return; - } - Err(e) => { - print_error(&format!("Parser error {:?}", e), &buffer, 0, 0); - return; - } - }; - - /* - expr' <- load expr - */ - - let type_expr = match typecheck::type_of(&expr) { - Err(e) => { - let explain = ::std::env::args().any(|s| s == "--explain"); - if !explain { - term_painter::Color::BrightBlack.with(|| { - println!("Use \"dhall --explain\" for detailed errors"); - }); - } - ERROR_STYLE.with(|| print!("Error: ")); - println!("{}", e.type_message.description()); - if explain { - println!("{}", e.type_message); - } - println!("{}", e.current); - // FIXME Print source position - return; - } - Ok(type_expr) => type_expr, - }; - - println!("{}", type_expr); - println!(""); - println!("{}", normalize::<_, X, _>(&expr)); -} diff --git a/src/parser.rs b/src/parser.rs deleted file mode 100644 index 057fce2..0000000 --- a/src/parser.rs +++ /dev/null @@ -1,91 +0,0 @@ -use lalrpop_util; - -use crate::grammar; -use crate::grammar_util::BoxExpr; -use crate::lexer::{Lexer, LexicalError, Tok}; -use crate::core::{bx, Expr}; - -pub type ParseError<'i> = lalrpop_util::ParseError<usize, Tok<'i>, LexicalError>; - -pub fn parse_expr(s: &str) -> Result<BoxExpr, ParseError> { - grammar::ExprParser::new().parse(Lexer::new(s)) -} - -use pest::Parser; -use pest::error::Error; -use pest::iterators::Pair; -use crate::generated_parser::{DhallParser, Rule}; - -fn debug_pair(pair: Pair<Rule>) { - fn aux(indent: usize, pair: Pair<Rule>) { - let indent_str = "| ".repeat(indent); - println!(r#"{}{:?}: "{}""#, indent_str, pair.as_rule(), pair.as_str()); - for p in pair.into_inner() { - aux(indent+1, p); - } - } - aux(0, pair) -} - -pub fn parse_expr_pest(s: &str) -> Result<BoxExpr, Error<Rule>> { - let parsed_expr = DhallParser::parse(Rule::complete_expression, s)?.next().unwrap(); - debug_pair(parsed_expr.clone()); - // println!("{}", parsed_expr.clone()); - - fn parse_pair(pair: Pair<Rule>) -> BoxExpr { - match pair.as_rule() { - Rule::natural_literal => bx(Expr::NaturalLit(str::parse(pair.as_str().trim()).unwrap())), - Rule::plus_expression => { - let mut inner = pair.into_inner().map(parse_pair); - let first_expr = inner.next().unwrap(); - inner.fold(first_expr, |acc, e| bx(Expr::NaturalPlus(acc, e))) - } - Rule::times_expression => { - let mut inner = pair.into_inner().map(parse_pair); - let first_expr = inner.next().unwrap(); - inner.fold(first_expr, |acc, e| bx(Expr::NaturalTimes(acc, e))) - } - r => panic!("{:?}", r), - } - } - - Ok(parse_pair(parsed_expr)) -} - - -#[test] -fn test_parse() { - use crate::core::Expr::*; - let expr = "((22 + 3) * 10)"; - println!("{:?}", parse_expr(expr)); - match parse_expr_pest(expr) { - Err(e) => println!("{}", e), - ok => println!("{:?}", ok), - } - assert_eq!(parse_expr_pest(expr).unwrap(), parse_expr(expr).unwrap()); - assert!(false); - - println!("test {:?}", parse_expr("3 + 5 * 10")); - assert!(parse_expr("22").is_ok()); - assert!(parse_expr("(22)").is_ok()); - assert_eq!(parse_expr("3 + 5 * 10").ok(), - Some(Box::new(NaturalPlus(Box::new(NaturalLit(3)), - Box::new(NaturalTimes(Box::new(NaturalLit(5)), - Box::new(NaturalLit(10)))))))); - // The original parser is apparently right-associative - assert_eq!(parse_expr("2 * 3 * 4").ok(), - Some(Box::new(NaturalTimes(Box::new(NaturalLit(2)), - Box::new(NaturalTimes(Box::new(NaturalLit(3)), - Box::new(NaturalLit(4)))))))); - assert!(parse_expr("((((22))))").is_ok()); - assert!(parse_expr("((22)").is_err()); - println!("{:?}", parse_expr("\\(b : Bool) -> b == False")); - assert!(parse_expr("\\(b : Bool) -> b == False").is_ok()); - println!("{:?}", parse_expr("foo.bar")); - assert!(parse_expr("foo.bar").is_ok()); - assert!(parse_expr("[] : List Bool").is_ok()); - - // println!("{:?}", parse_expr("< Left = True | Right : Natural >")); - // println!("{:?}", parse_expr(r#""bl${42}ah""#)); - // assert!(parse_expr("< Left = True | Right : Natural >").is_ok()); -} diff --git a/src/typecheck.rs b/src/typecheck.rs deleted file mode 100644 index 62ff7d2..0000000 --- a/src/typecheck.rs +++ /dev/null @@ -1,616 +0,0 @@ -#![allow(non_snake_case)] -use std::collections::BTreeMap; -use std::collections::HashSet; -use std::fmt; - -use crate::context::Context; -use crate::core; -use crate::core::{Expr, V, X, bx, normalize, shift, subst}; -use crate::core::{pi, app}; -use crate::core::BuiltinType::*; -use crate::core::BuiltinValue::*; -use crate::core::Const::*; -use crate::core::Expr::*; - -use self::TypeMessage::*; - -fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> { - match c { - Type => Ok(Kind), - Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)), - } -} - -fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> { - match (a, b) { - (Type, Kind) => Err(()), - (Kind, Kind) => Ok(Kind), - (Type, Type) | - (Kind, Type) => Ok(Type), - } -} - -fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool { - let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1)); - match (vl, vr, xxs) { - (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR, - (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true, - (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => { - let nL2 = if xL == xL2 { nL - 1 } else { nL }; - let nR2 = if xR == xR2 { nR - 1 } else { nR }; - match_vars(&V(xL, nL2), &V(xR, nR2), xs) - } - } -} - -fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool - where S: Clone + ::std::fmt::Debug, - T: Clone + ::std::fmt::Debug -{ - fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool - where S: Clone + ::std::fmt::Debug, - T: Clone + ::std::fmt::Debug - { - match (el, er) { - (&Const(Type), &Const(Type)) | - (&Const(Kind), &Const(Kind)) => true, - (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx), - (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => { - //ctx <- State.get - let eq1 = go(ctx, tL, tR); - if eq1 { - //State.put ((xL, xR):ctx) - ctx.push((xL, xR)); - let eq2 = go(ctx, bL, bR); - //State.put ctx - let _ = ctx.pop(); - eq2 - } else { - false - } - } - (&App(ref fL, ref aL), &App(ref fR, ref aR)) => - if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false }, - (&BuiltinType(a), &BuiltinType(b)) => a == b, - (&Record(ref ktsL0), &Record(ref ktsR0)) => { - if ktsL0.len() != ktsR0.len() { - return false; - } - /* - let go ((kL, tL):ktsL) ((kR, tR):ktsR) - | kL == kR = do - b <- go tL tR - if b - then go ktsL ktsR - else return False - go [] [] = return True - go _ _ = return False - */ - /* - for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) { - if kL == kR { - if !go(ctx, tL, tR) { - return false; - } - } else { - return false; - } - } - true - */ - !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { - kL != kR || !go(ctx, tL, tR) - }) - } - (&Union(ref ktsL0), &Union(ref ktsR0)) => { - if ktsL0.len() != ktsR0.len() { - return false; - } - /* - let loop ((kL, tL):ktsL) ((kR, tR):ktsR) - | kL == kR = do - b <- go tL tR - if b - then loop ktsL ktsR - else return False - loop [] [] = return True - loop _ _ = return False - loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0) - */ - !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { - kL != kR || !go(ctx, tL, tR) - }) - } - (_, _) => false, - } - } - let mut ctx = vec![]; - go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0)) -} - -fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>, - e: &Expr<'i, S, X>, - t: core::BuiltinType, - ef: EF, - l: &Expr<'i, S, X>, - r: &Expr<'i, S, X>) - -> Result<Expr<'i, S, X>, TypeError<'i, S>> - where S: Clone + ::std::fmt::Debug + 'i, - EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>, -{ - let tl = normalize(&type_with(ctx, l)?); - match tl { - BuiltinType(lt) if lt == t => {} - _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))), - } - - let tr = normalize(&type_with(ctx, r)?); - match tr { - BuiltinType(rt) if rt == t => {} - _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))), - } - - Ok(BuiltinType(t)) -} - -/// Type-check an expression and return the expression'i type if type-checking -/// suceeds or an error if type-checking fails -/// -/// `type_with` does not necessarily normalize the type since full normalization -/// is not necessary for just type-checking. If you actually care about the -/// returned type then you may want to `normalize` it afterwards. -pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, - e: &Expr<'i, S, X>) - -> Result<Expr<'i, S, X>, TypeError<'i, S>> - where S: Clone + ::std::fmt::Debug + 'i -{ - match *e { - Const(c) => axiom(c).map(Const), //.map(Cow::Owned), - Var(V(x, n)) => { - ctx.lookup(x, n) - .cloned() - //.map(Cow::Borrowed) - .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable)) - } - Lam(x, ref tA, ref b) => { - let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); - let tB = type_with(&ctx2, b)?; - let p = Pi(x, tA.clone(), bx(tB)); - let _ = type_with(ctx, &p)?; - //Ok(Cow::Owned(p)) - Ok(p) - } - Pi(x, ref tA, ref tB) => { - let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?); - let kA = match tA2 { - Const(k) => k, - _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))), - }; - - let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); - let tB = normalize(&type_with(&ctx2, tB)?); - let kB = match tB { - Const(k) => k, - _ => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))), - }; - - match rule(kA, kB) { - Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))), - Ok(k) => Ok(Const(k)), - } - } - App(ref f, ref a) => { - let tf = normalize(&type_with(ctx, f)?); - let (x, tA, tB) = match tf { - Pi(x, tA, tB) => (x, tA, tB), - _ => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))), - }; - let tA2 = type_with(ctx, a)?; - if prop_equal(&tA, &tA2) { - let vx0 = V(x, 0); - let a2 = shift::<S, S, X>( 1, vx0, a); - let tB2 = subst(vx0, &a2, &tB); - let tB3 = shift::<S, S, X>(-1, vx0, &tB2); - Ok(tB3) - } else { - let nf_A = normalize(&tA); - let nf_A2 = normalize(&tA2); - Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2))) - } - } - Let(f, ref mt, ref r, ref b) => { - let tR = type_with(ctx, r)?; - let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?); - let kR = match ttR { - Const(k) => k, - // Don't bother to provide a `let`-specific version of this error - // message because this should never happen anyway - _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))), - }; - - let ctx2 = ctx.insert(f, tR.clone()); - let tB = type_with(&ctx2, b)?; - let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?); - let kB = match ttB { - Const(k) => k, - // Don't bother to provide a `let`-specific version of this error - // message because this should never happen anyway - _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))), - }; - - if let Err(()) = rule(kR, kB) { - return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB))); - } - - if let Some(ref t) = *mt { - let nf_t = normalize(t); - let nf_tR = normalize(&tR); - if !prop_equal(&nf_tR, &nf_t) { - return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR))); - } - } - - Ok(tB) - } - Annot(ref x, ref t) => { - // This is mainly just to check that `t` is not `Kind` - let _ = type_with(ctx, t)?; - - let t2 = type_with(ctx, x)?; - if prop_equal(t, &t2) { - Ok((**t).clone()) - } else { - let nf_t = normalize(t); - let nf_t2 = normalize(&t2); - Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2))) - } - } - BuiltinType(t) => Ok(match t { - List | Optional => pi("_", Const(Type), Const(Type)), - Bool | Natural | Integer | Double | Text => Const(Type), - }), - BoolLit(_) => Ok(BuiltinType(Bool)), - BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r), - BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r), - BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r), - BoolNE(ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r), - BoolIf(ref x, ref y, ref z) => { - let tx = normalize(&type_with(ctx, x)?); - match tx { - BuiltinType(Bool) => {} - _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))), - } - let ty = normalize(&type_with(ctx, y)?); - let tty = normalize(&type_with(ctx, &ty)?); - match tty { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))), - } - - let tz = normalize(&type_with(ctx, z)?); - let ttz = normalize(&type_with(ctx, &tz)?); - match ttz { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))), - } - - if !prop_equal(&ty, &tz) { - return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz))); - } - Ok(ty) - } - NaturalLit(_) => Ok(BuiltinType(Natural)), - BuiltinValue(NaturalFold) => - Ok(pi("_", Natural, - pi("natural", Const(Type), - pi("succ", pi("_", "natural", "natural"), - pi("zero", "natural", "natural"))))), - BuiltinValue(NaturalBuild) => - Ok(pi("_", - pi("natural", Const(Type), - pi("succ", pi("_", "natural", "natural"), - pi("zero", "natural", "natural"))), - Natural)), - BuiltinValue(NaturalIsZero) | - BuiltinValue(NaturalEven) | - BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)), - NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r), - NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r), - IntegerLit(_) => Ok(BuiltinType(Integer)), - DoubleLit(_) => Ok(BuiltinType(Double)), - TextLit(_) => Ok(BuiltinType(Text)), - TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r), - ListLit(ref t, ref xs) => { - let s = normalize::<_, S, _>(&type_with(ctx, t)?); - match s { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, InvalidListType((**t).clone()))), - } - for (i, x) in xs.iter().enumerate() { - let t2 = type_with(ctx, x)?; - if !prop_equal(t, &t2) { - let nf_t = normalize(t); - let nf_t2 = normalize(&t2); - return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) ) - } - } - Ok(App(bx(BuiltinType(List)), t.clone())) - } - BuiltinValue(ListBuild) => - Ok(pi("a", Const(Type), - pi("_", - pi("list", Const(Type), - pi("cons", pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list"))), - app(List, "a")))), - BuiltinValue(ListFold) => - Ok(pi("a", Const(Type), - pi("_", app(List, "a"), - pi("list", Const(Type), - pi("cons", pi("_", "a", pi("_", "list", "list")), - pi("nil", "list", "list")))))), - BuiltinValue(ListLength) => - Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))), - BuiltinValue(ListHead) | - BuiltinValue(ListLast) => - Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))), - BuiltinValue(ListIndexed) => { - let mut m = BTreeMap::new(); - m.insert("index", BuiltinType(Natural)); - m.insert("value", Expr::from("a")); - Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m))))) - } - BuiltinValue(ListReverse) => - Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))), - OptionalLit(ref t, ref xs) => { - let s = normalize::<_, S, _>(&type_with(ctx, t)?); - match s { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, InvalidOptionalType((**t).clone()))), - } - let n = xs.len(); - if 2 <= n { - return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n))); - } - for x in xs { - let t2 = type_with(ctx, x)?; - if !prop_equal(t, &t2) { - let nf_t = normalize(t); - let nf_t2 = normalize(&t2); - return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2))); - } - } - Ok(App(bx(BuiltinType(Optional)), t.clone())) - } - BuiltinValue(OptionalFold) => - Ok(pi("a", Const(Type), - pi("_", app(Optional, "a"), - pi("optional", Const(Type), - pi("just", pi("_", "a", "optional"), - pi("nothing", "optional", "optional")))))), - Record(ref kts) => { - for (k, t) in kts { - let s = normalize::<S, S, X>(&type_with(ctx, t)?); - match s { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))), - } - } - Ok(Const(Type)) - } - RecordLit(ref kvs) => { - let kts = kvs.iter().map(|(&k, v)| { - let t = type_with(ctx, v)?; - let s = normalize::<S, S, X>(&type_with(ctx, &t)?); - match s { - Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))), - } - Ok((k, t)) - }).collect::<Result<_, _>>()?; - Ok(Record(kts)) - } -/* -type_with ctx e@(Union kts ) = do - let process (k, t) = do - s <- fmap Dhall.Core.normalize (type_with ctx t) - case s of - Const Type -> return () - _ -> Left (TypeError ctx e (InvalidAlternativeType k t)) - mapM_ process (Data.Map.toList kts) - return (Const Type) -type_with ctx e@(UnionLit k v kts) = do - case Data.Map.lookup k kts of - Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) - Nothing -> return () - t <- type_with ctx v - let union = Union (Data.Map.insert k t kts) - _ <- type_with ctx union - return union -type_with ctx e@(Combine kvsX kvsY) = do - tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX) - ktsX <- case tKvsX of - Record kts -> return kts - _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX)) - - tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY) - ktsY <- case tKvsY of - Record kts -> return kts - _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY)) - - let combineTypes ktsL ktsR = do - let ks = - Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR) - kts <- forM (toList ks) (\k -> do - case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of - (Just (Record ktsL'), Just (Record ktsR')) -> do - t <- combineTypes ktsL' ktsR' - return (k, t) - (Nothing, Just t) -> do - return (k, t) - (Just t, Nothing) -> do - return (k, t) - _ -> do - Left (TypeError ctx e (FieldCollision k)) ) - return (Record (Data.Map.fromList kts)) - - combineTypes ktsX ktsY -type_with ctx e@(Merge kvsX kvsY t) = do - tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX) - ktsX <- case tKvsX of - Record kts -> return kts - _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) - let ksX = Data.Map.keysSet ktsX - - tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY) - ktsY <- case tKvsY of - Union kts -> return kts - _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) - let ksY = Data.Map.keysSet ktsY - - let diffX = Data.Set.difference ksX ksY - let diffY = Data.Set.difference ksY ksX - - if Data.Set.null diffX - then return () - else Left (TypeError ctx e (UnusedHandler diffX)) - - let process (kY, tY) = do - case Data.Map.lookup kY ktsX of - Nothing -> Left (TypeError ctx e (MissingHandler diffY)) - Just tX -> - case tX of - Pi _ tY' t' -> do - if prop_equal tY tY' - then return () - else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) - if prop_equal t t' - then return () - else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t')) - _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) - mapM_ process (Data.Map.toList ktsY) - return t - */ - Field(ref r, x) => { - let t = normalize(&type_with(ctx, r)?); - match t { - Record(ref kts) => - kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))), - _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))), - } - } - /* -type_with ctx (Note s e' ) = case type_with ctx e' of - Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m) - Left (TypeError ctx2 e'' m) -> Left (TypeError ctx2 (Note s e'') m) - Right r -> Right r -*/ - Embed(p) => match p {}, - _ => panic!("Unimplemented typecheck case: {:?}", e), - } -} - -/// `typeOf` is the same as `type_with` with an empty context, meaning that the -/// expression must be closed (i.e. no free variables), otherwise type-checking -/// will fail. -pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result<Expr<'i, S, X>, TypeError<'i, S>> { - let ctx = Context::new(); - type_with(&ctx, e) //.map(|e| e.into_owned()) -} - -/// The specific type error -#[derive(Debug)] -pub enum TypeMessage<'i, S> { - UnboundVariable, - InvalidInputType(Expr<'i, S, X>), - InvalidOutputType(Expr<'i, S, X>), - NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>), - TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - Untyped, - InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - InvalidListType(Expr<'i, S, X>), - InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - InvalidOptionalLiteral(usize), - InvalidOptionalType(Expr<'i, S, X>), - InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>), - IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - InvalidField(String, Expr<'i, S, X>), - InvalidFieldType(String, Expr<'i, S, X>), - InvalidAlternative(String, Expr<'i, S, X>), - InvalidAlternativeType(String, Expr<'i, S, X>), - DuplicateAlternative(String), - MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>), - FieldCollision(String), - MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>), - MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>), - UnusedHandler(HashSet<String>), - MissingHandler(HashSet<String>), - HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), - HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), - HandlerNotAFunction(String, Expr<'i, S, X>), - NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>), - MissingField(String, Expr<'i, S, X>), - CantAnd(Expr<'i, S, X>, Expr<'i, S, X>), - CantOr(Expr<'i, S, X>, Expr<'i, S, X>), - CantEQ(Expr<'i, S, X>, Expr<'i, S, X>), - CantNE(Expr<'i, S, X>, Expr<'i, S, X>), - CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>), - CantAdd(Expr<'i, S, X>, Expr<'i, S, X>), - CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>), - NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>), - NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>), -} - -/// A structured type error that includes context -#[derive(Debug)] -pub struct TypeError<'i, S> { - pub context: Context<'i, Expr<'i, S, X>>, - pub current: Expr<'i, S, X>, - pub type_message: TypeMessage<'i, S>, -} - -impl<'i, S: Clone> TypeError<'i, S> { - pub fn new(context: &Context<'i, Expr<'i, S, X>>, - current: &Expr<'i, S, X>, - type_message: TypeMessage<'i, S>) - -> Self { - TypeError { - context: context.clone(), - current: current.clone(), - type_message: type_message, - } - } -} - -impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> { - fn description(&self) -> &str { - match *self { - UnboundVariable => "Unbound variable", - InvalidInputType(_) => "Invalid function input", - InvalidOutputType(_) => "Invalid function output", - NotAFunction(_, _) => "Not a function", - TypeMismatch(_, _, _, _) => "Wrong type of function argument", - _ => "Unhandled error", - } - } -} - -impl<'i, S> fmt::Display for TypeMessage<'i, S> { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - match *self { - UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")), - TypeMismatch(ref e0, ref e1, ref e2, ref e3) => { - let template = include_str!("errors/TypeMismatch.txt"); - let s = template - .replace("$txt0", &format!("{}", e0)) - .replace("$txt1", &format!("{}", e1)) - .replace("$txt2", &format!("{}", e2)) - .replace("$txt3", &format!("{}", e3)); - f.write_str(&s) - } - _ => f.write_str("Unhandled error message"), - } - } -} |