From e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 1 Mar 2019 17:28:19 +0100 Subject: Split abnf_to_pest and dhall into their own crates --- dhall/src/context.rs | 51 ++ dhall/src/core.rs | 1056 ++++++++++++++++++++++++ dhall/src/dhall.pest.visibility | 188 +++++ dhall/src/errors/AnnotMismatch.txt | 117 +++ dhall/src/errors/CantTextAppend.txt | 28 + dhall/src/errors/DuplicateAlternative.txt | 18 + dhall/src/errors/FieldCollision.txt | 43 + dhall/src/errors/HandlerInputTypeMismatch.txt | 49 ++ dhall/src/errors/HandlerNotAFunction.txt | 32 + dhall/src/errors/HandlerOutputTypeMismatch.txt | 51 ++ dhall/src/errors/IfBranchMismatch.txt | 63 ++ dhall/src/errors/IfBranchMustBeTerm.txt | 51 ++ dhall/src/errors/InvalidAlterantive.txt | 48 ++ dhall/src/errors/InvalidAlterantiveType.txt | 49 ++ dhall/src/errors/InvalidField.txt | 35 + dhall/src/errors/InvalidFieldType.txt | 34 + dhall/src/errors/InvalidInputType.txt | 61 ++ dhall/src/errors/InvalidListElement.txt | 30 + dhall/src/errors/InvalidListType.txt | 43 + dhall/src/errors/InvalidOptionType.txt | 44 + dhall/src/errors/InvalidOptionalElement.txt | 29 + dhall/src/errors/InvalidOptionalLiteral.txt | 53 ++ dhall/src/errors/InvalidOutputType.txt | 68 ++ dhall/src/errors/InvalidPredicate.txt | 51 ++ dhall/src/errors/MissingField.txt | 30 + dhall/src/errors/MissingHandler.txt | 32 + dhall/src/errors/MustCombineARecord.txt | 46 ++ dhall/src/errors/MustMergeARecord.txt | 43 + dhall/src/errors/MustMergeUnion.txt | 31 + dhall/src/errors/NoDependentLet.txt | 76 ++ dhall/src/errors/NoDependentTypes.txt | 31 + dhall/src/errors/NotAFunction.txt | 68 ++ dhall/src/errors/NotARecord.txt | 48 ++ dhall/src/errors/TypeMismatch.txt | 117 +++ dhall/src/errors/UnboundVariable.txt | 97 +++ dhall/src/errors/Untyped.txt | 117 +++ dhall/src/errors/UnusedHandler.txt | 32 + dhall/src/generated_parser.rs | 6 + dhall/src/grammar.lalrpop | 162 ++++ dhall/src/grammar_util.rs | 14 + dhall/src/lexer.rs | 378 +++++++++ dhall/src/lib.rs | 12 + dhall/src/main.rs | 101 +++ dhall/src/parser.rs | 91 ++ dhall/src/typecheck.rs | 616 ++++++++++++++ 45 files changed, 4440 insertions(+) create mode 100644 dhall/src/context.rs create mode 100644 dhall/src/core.rs create mode 100644 dhall/src/dhall.pest.visibility create mode 100644 dhall/src/errors/AnnotMismatch.txt create mode 100644 dhall/src/errors/CantTextAppend.txt create mode 100644 dhall/src/errors/DuplicateAlternative.txt create mode 100644 dhall/src/errors/FieldCollision.txt create mode 100644 dhall/src/errors/HandlerInputTypeMismatch.txt create mode 100644 dhall/src/errors/HandlerNotAFunction.txt create mode 100644 dhall/src/errors/HandlerOutputTypeMismatch.txt create mode 100644 dhall/src/errors/IfBranchMismatch.txt create mode 100644 dhall/src/errors/IfBranchMustBeTerm.txt create mode 100644 dhall/src/errors/InvalidAlterantive.txt create mode 100644 dhall/src/errors/InvalidAlterantiveType.txt create mode 100644 dhall/src/errors/InvalidField.txt create mode 100644 dhall/src/errors/InvalidFieldType.txt create mode 100644 dhall/src/errors/InvalidInputType.txt create mode 100644 dhall/src/errors/InvalidListElement.txt create mode 100644 dhall/src/errors/InvalidListType.txt create mode 100644 dhall/src/errors/InvalidOptionType.txt create mode 100644 dhall/src/errors/InvalidOptionalElement.txt create mode 100644 dhall/src/errors/InvalidOptionalLiteral.txt create mode 100644 dhall/src/errors/InvalidOutputType.txt create mode 100644 dhall/src/errors/InvalidPredicate.txt create mode 100644 dhall/src/errors/MissingField.txt create mode 100644 dhall/src/errors/MissingHandler.txt create mode 100644 dhall/src/errors/MustCombineARecord.txt create mode 100644 dhall/src/errors/MustMergeARecord.txt create mode 100644 dhall/src/errors/MustMergeUnion.txt create mode 100644 dhall/src/errors/NoDependentLet.txt create mode 100644 dhall/src/errors/NoDependentTypes.txt create mode 100644 dhall/src/errors/NotAFunction.txt create mode 100644 dhall/src/errors/NotARecord.txt create mode 100644 dhall/src/errors/TypeMismatch.txt create mode 100644 dhall/src/errors/UnboundVariable.txt create mode 100644 dhall/src/errors/Untyped.txt create mode 100644 dhall/src/errors/UnusedHandler.txt create mode 100644 dhall/src/generated_parser.rs create mode 100644 dhall/src/grammar.lalrpop create mode 100644 dhall/src/grammar_util.rs create mode 100644 dhall/src/lexer.rs create mode 100644 dhall/src/lib.rs create mode 100644 dhall/src/main.rs create mode 100644 dhall/src/parser.rs create mode 100644 dhall/src/typecheck.rs (limited to 'dhall/src') diff --git a/dhall/src/context.rs b/dhall/src/context.rs new file mode 100644 index 0000000..c2e1913 --- /dev/null +++ b/dhall/src/context.rs @@ -0,0 +1,51 @@ +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>); + +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>(&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/dhall/src/core.rs b/dhall/src/core.rs new file mode 100644 index 0000000..473a6a6 --- /dev/null +++ b/dhall/src/core.rs @@ -0,0 +1,1056 @@ +#![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`
+ /// `Var (V x n) ~ x@n` + Var(V<'i>), + /// `Lam x A b ~ λ(x : A) -> b` + Lam(&'i str, Box>, Box>), + /// `Pi "_" A B ~ A -> B` + /// `Pi x A B ~ ∀(x : A) -> B` + Pi(&'i str, Box>, Box>), + /// `App f A ~ f A` + App(Box>, Box>), + /// `Let x Nothing r e ~ let x = r in e` + /// `Let x (Just t) r e ~ let x : t = r in e` + Let(&'i str, Option>>, Box>, Box>), + /// `Annot x t ~ x : t` + Annot(Box>, Box>), + /// Built-in types + BuiltinType(BuiltinType), + /// Built-in function values + BuiltinValue(BuiltinValue), + /// `BoolLit b ~ b` + BoolLit(bool), + /// `BoolAnd x y ~ x && y` + BoolAnd(Box>, Box>), + /// `BoolOr x y ~ x || y` + BoolOr(Box>, Box>), + /// `BoolEQ x y ~ x == y` + BoolEQ(Box>, Box>), + /// `BoolNE x y ~ x != y` + BoolNE(Box>, Box>), + /// `BoolIf x y z ~ if x then y else z` + BoolIf(Box>, Box>, Box>), + /// `NaturalLit n ~ +n` + NaturalLit(Natural), + /// `NaturalPlus x y ~ x + y` + NaturalPlus(Box>, Box>), + /// `NaturalTimes x y ~ x * y` + NaturalTimes(Box>, Box>), + /// `IntegerLit n ~ n` + IntegerLit(Integer), + /// `DoubleLit n ~ n` + DoubleLit(Double), + /// `TextLit t ~ t` + TextLit(Builder), + /// `TextAppend x y ~ x ++ y` + TextAppend(Box>, Box>), + /// `ListLit t [x, y, z] ~ [x, y, z] : List t` + ListLit(Box>, Vec>), + /// `OptionalLit t [e] ~ [e] : Optional t` + /// `OptionalLit t [] ~ [] : Optional t` + OptionalLit(Box>, Vec>), + /// `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>, BTreeMap<&'i str, Expr<'i, S, A>>), + /// `Combine x y ~ x ∧ y` + Combine(Box>, Box>), + /// `Merge x y t ~ merge x y : t` + Merge(Box>, Box>, Box>), + /// `Field e x ~ e.x` + Field(Box>, &'i str), + /// `Note S x ~ e` + Note(S, Box>), + /// `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 for Expr<'i, S, A> { + fn from(t: BuiltinType) -> Self { + Expr::BuiltinType(t) + } +} + +impl<'i, S, A> From 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 { + match *self { + Expr::BoolLit(v) => Some(v), + _ => None, + } + } + + fn natural_lit(&self) -> Option { + match *self { + Expr::NaturalLit(v) => Some(v), + _ => None, + } + } + + fn text_lit(&self) -> Option { + 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) => ::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(open: &str, + close: &str, + it: I, + f: &mut fmt::Formatter, + func: F) + -> Result<(), fmt::Error> + where I: IntoIterator, + 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> { + ::fmt(self, f) + } +} + +impl Display for BuiltinType { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + ::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>, + Ev: Into> +{ + 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>, + Ex: Into> +{ + 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(x: T) -> Box { + 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 + where I: IntoIterator, + K: Eq + Ord + Copy + 'a, + V: 'a, + F: Fn(&V) -> U +{ + it.into_iter().map(|(&k, v)| (k, f(v))).collect() +} + +fn map_op2(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>, Box>) -> 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>, Box>) -> 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::(f) { + Lam(x, _A, b) => { // Beta reduce + let vx0 = V(x, 0); + let a2 = shift::( 1, vx0, a); + let b2 = subst::(vx0, &a2, &b); + let b3 = shift::(-1, vx0, &b2); + normalize(&b3) + } + f2 => match (f2, normalize::(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>, 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(e: &Expr) -> 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(op: Op, get: Get, set: Set, x: T, y: T) -> T + where Get: Fn(&T) -> Option, + Set: FnOnce(U, U) -> T, + Op: FnOnce(Box, Box) -> T, +{ + if let (Some(xv), Some(yv)) = (get(&x), get(&y)) { + set(xv, yv) + } else { + op(bx(x), bx(y)) + } +} diff --git a/dhall/src/dhall.pest.visibility b/dhall/src/dhall.pest.visibility new file mode 100644 index 0000000..c09fccf --- /dev/null +++ b/dhall/src/dhall.pest.visibility @@ -0,0 +1,188 @@ +# 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/dhall/src/errors/AnnotMismatch.txt b/dhall/src/errors/AnnotMismatch.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/src/errors/AnnotMismatch.txt @@ -0,0 +1,117 @@ +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/dhall/src/errors/CantTextAppend.txt b/dhall/src/errors/CantTextAppend.txt new file mode 100644 index 0000000..26b9ceb --- /dev/null +++ b/dhall/src/errors/CantTextAppend.txt @@ -0,0 +1,28 @@ +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/dhall/src/errors/DuplicateAlternative.txt b/dhall/src/errors/DuplicateAlternative.txt new file mode 100644 index 0000000..077f8aa --- /dev/null +++ b/dhall/src/errors/DuplicateAlternative.txt @@ -0,0 +1,18 @@ +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/dhall/src/errors/FieldCollision.txt b/dhall/src/errors/FieldCollision.txt new file mode 100644 index 0000000..2b2d260 --- /dev/null +++ b/dhall/src/errors/FieldCollision.txt @@ -0,0 +1,43 @@ +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/dhall/src/errors/HandlerInputTypeMismatch.txt b/dhall/src/errors/HandlerInputTypeMismatch.txt new file mode 100644 index 0000000..7d3525b --- /dev/null +++ b/dhall/src/errors/HandlerInputTypeMismatch.txt @@ -0,0 +1,49 @@ +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/dhall/src/errors/HandlerNotAFunction.txt b/dhall/src/errors/HandlerNotAFunction.txt new file mode 100644 index 0000000..ff87443 --- /dev/null +++ b/dhall/src/errors/HandlerNotAFunction.txt @@ -0,0 +1,32 @@ +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/dhall/src/errors/HandlerOutputTypeMismatch.txt b/dhall/src/errors/HandlerOutputTypeMismatch.txt new file mode 100644 index 0000000..f359459 --- /dev/null +++ b/dhall/src/errors/HandlerOutputTypeMismatch.txt @@ -0,0 +1,51 @@ +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/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt new file mode 100644 index 0000000..a95b130 --- /dev/null +++ b/dhall/src/errors/IfBranchMismatch.txt @@ -0,0 +1,63 @@ +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/dhall/src/errors/IfBranchMustBeTerm.txt b/dhall/src/errors/IfBranchMustBeTerm.txt new file mode 100644 index 0000000..4c15881 --- /dev/null +++ b/dhall/src/errors/IfBranchMustBeTerm.txt @@ -0,0 +1,51 @@ +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/dhall/src/errors/InvalidAlterantive.txt b/dhall/src/errors/InvalidAlterantive.txt new file mode 100644 index 0000000..391fc3a --- /dev/null +++ b/dhall/src/errors/InvalidAlterantive.txt @@ -0,0 +1,48 @@ +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/dhall/src/errors/InvalidAlterantiveType.txt b/dhall/src/errors/InvalidAlterantiveType.txt new file mode 100644 index 0000000..f5dadef --- /dev/null +++ b/dhall/src/errors/InvalidAlterantiveType.txt @@ -0,0 +1,49 @@ +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/dhall/src/errors/InvalidField.txt b/dhall/src/errors/InvalidField.txt new file mode 100644 index 0000000..bfbf106 --- /dev/null +++ b/dhall/src/errors/InvalidField.txt @@ -0,0 +1,35 @@ +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/dhall/src/errors/InvalidFieldType.txt b/dhall/src/errors/InvalidFieldType.txt new file mode 100644 index 0000000..4f76a64 --- /dev/null +++ b/dhall/src/errors/InvalidFieldType.txt @@ -0,0 +1,34 @@ +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/dhall/src/errors/InvalidInputType.txt b/dhall/src/errors/InvalidInputType.txt new file mode 100644 index 0000000..eabafa4 --- /dev/null +++ b/dhall/src/errors/InvalidInputType.txt @@ -0,0 +1,61 @@ +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/dhall/src/errors/InvalidListElement.txt b/dhall/src/errors/InvalidListElement.txt new file mode 100644 index 0000000..59db7b7 --- /dev/null +++ b/dhall/src/errors/InvalidListElement.txt @@ -0,0 +1,30 @@ +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/dhall/src/errors/InvalidListType.txt b/dhall/src/errors/InvalidListType.txt new file mode 100644 index 0000000..676647e --- /dev/null +++ b/dhall/src/errors/InvalidListType.txt @@ -0,0 +1,43 @@ +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/dhall/src/errors/InvalidOptionType.txt b/dhall/src/errors/InvalidOptionType.txt new file mode 100644 index 0000000..3bc81de --- /dev/null +++ b/dhall/src/errors/InvalidOptionType.txt @@ -0,0 +1,44 @@ +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/dhall/src/errors/InvalidOptionalElement.txt b/dhall/src/errors/InvalidOptionalElement.txt new file mode 100644 index 0000000..0254220 --- /dev/null +++ b/dhall/src/errors/InvalidOptionalElement.txt @@ -0,0 +1,29 @@ +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/dhall/src/errors/InvalidOptionalLiteral.txt b/dhall/src/errors/InvalidOptionalLiteral.txt new file mode 100644 index 0000000..41c0fdc --- /dev/null +++ b/dhall/src/errors/InvalidOptionalLiteral.txt @@ -0,0 +1,53 @@ +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/dhall/src/errors/InvalidOutputType.txt b/dhall/src/errors/InvalidOutputType.txt new file mode 100644 index 0000000..dd2695d --- /dev/null +++ b/dhall/src/errors/InvalidOutputType.txt @@ -0,0 +1,68 @@ +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/dhall/src/errors/InvalidPredicate.txt b/dhall/src/errors/InvalidPredicate.txt new file mode 100644 index 0000000..4c15881 --- /dev/null +++ b/dhall/src/errors/InvalidPredicate.txt @@ -0,0 +1,51 @@ +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/dhall/src/errors/MissingField.txt b/dhall/src/errors/MissingField.txt new file mode 100644 index 0000000..de14a33 --- /dev/null +++ b/dhall/src/errors/MissingField.txt @@ -0,0 +1,30 @@ +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/dhall/src/errors/MissingHandler.txt b/dhall/src/errors/MissingHandler.txt new file mode 100644 index 0000000..433445e --- /dev/null +++ b/dhall/src/errors/MissingHandler.txt @@ -0,0 +1,32 @@ +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/dhall/src/errors/MustCombineARecord.txt b/dhall/src/errors/MustCombineARecord.txt new file mode 100644 index 0000000..141b969 --- /dev/null +++ b/dhall/src/errors/MustCombineARecord.txt @@ -0,0 +1,46 @@ +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/dhall/src/errors/MustMergeARecord.txt b/dhall/src/errors/MustMergeARecord.txt new file mode 100644 index 0000000..79094bd --- /dev/null +++ b/dhall/src/errors/MustMergeARecord.txt @@ -0,0 +1,43 @@ +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/dhall/src/errors/MustMergeUnion.txt b/dhall/src/errors/MustMergeUnion.txt new file mode 100644 index 0000000..68df70c --- /dev/null +++ b/dhall/src/errors/MustMergeUnion.txt @@ -0,0 +1,31 @@ +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/dhall/src/errors/NoDependentLet.txt b/dhall/src/errors/NoDependentLet.txt new file mode 100644 index 0000000..fdc65b4 --- /dev/null +++ b/dhall/src/errors/NoDependentLet.txt @@ -0,0 +1,76 @@ +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/dhall/src/errors/NoDependentTypes.txt b/dhall/src/errors/NoDependentTypes.txt new file mode 100644 index 0000000..435bdcb --- /dev/null +++ b/dhall/src/errors/NoDependentTypes.txt @@ -0,0 +1,31 @@ +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/dhall/src/errors/NotAFunction.txt b/dhall/src/errors/NotAFunction.txt new file mode 100644 index 0000000..dd2695d --- /dev/null +++ b/dhall/src/errors/NotAFunction.txt @@ -0,0 +1,68 @@ +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/dhall/src/errors/NotARecord.txt b/dhall/src/errors/NotARecord.txt new file mode 100644 index 0000000..e0eebc8 --- /dev/null +++ b/dhall/src/errors/NotARecord.txt @@ -0,0 +1,48 @@ +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/dhall/src/errors/TypeMismatch.txt b/dhall/src/errors/TypeMismatch.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/src/errors/TypeMismatch.txt @@ -0,0 +1,117 @@ +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/dhall/src/errors/UnboundVariable.txt b/dhall/src/errors/UnboundVariable.txt new file mode 100644 index 0000000..bd7d483 --- /dev/null +++ b/dhall/src/errors/UnboundVariable.txt @@ -0,0 +1,97 @@ +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/dhall/src/errors/Untyped.txt b/dhall/src/errors/Untyped.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/src/errors/Untyped.txt @@ -0,0 +1,117 @@ +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/dhall/src/errors/UnusedHandler.txt b/dhall/src/errors/UnusedHandler.txt new file mode 100644 index 0000000..2e46a12 --- /dev/null +++ b/dhall/src/errors/UnusedHandler.txt @@ -0,0 +1,32 @@ +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/dhall/src/generated_parser.rs b/dhall/src/generated_parser.rs new file mode 100644 index 0000000..452b4cd --- /dev/null +++ b/dhall/src/generated_parser.rs @@ -0,0 +1,6 @@ +#[allow(unused_imports)] +use pest_derive::*; + +#[derive(Parser)] +#[grammar = "dhall.pest"] +pub struct DhallParser; diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop new file mode 100644 index 0000000..150961f --- /dev/null +++ b/dhall/src/grammar.lalrpop @@ -0,0 +1,162 @@ +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(), + Nat => Tok::Natural(), + Text => Tok::Text(), + Bool => Tok::Bool(), + Label => Tok::Identifier(<&'input str>), + Const => Tok::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(), + + "{" => 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 + ":" => bx(Annot(<>)), + ExprB, +}; + +ExprB: BoxExpr<'input> = { + Lambda "("