summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/context.rs51
-rw-r--r--src/core.rs1056
-rw-r--r--src/dhall.pest.visibility188
-rw-r--r--src/errors/AnnotMismatch.txt117
-rw-r--r--src/errors/CantTextAppend.txt28
-rw-r--r--src/errors/DuplicateAlternative.txt18
-rw-r--r--src/errors/FieldCollision.txt43
-rw-r--r--src/errors/HandlerInputTypeMismatch.txt49
-rw-r--r--src/errors/HandlerNotAFunction.txt32
-rw-r--r--src/errors/HandlerOutputTypeMismatch.txt51
-rw-r--r--src/errors/IfBranchMismatch.txt63
-rw-r--r--src/errors/IfBranchMustBeTerm.txt51
-rw-r--r--src/errors/InvalidAlterantive.txt48
-rw-r--r--src/errors/InvalidAlterantiveType.txt49
-rw-r--r--src/errors/InvalidField.txt35
-rw-r--r--src/errors/InvalidFieldType.txt34
-rw-r--r--src/errors/InvalidInputType.txt61
-rw-r--r--src/errors/InvalidListElement.txt30
-rw-r--r--src/errors/InvalidListType.txt43
-rw-r--r--src/errors/InvalidOptionType.txt44
-rw-r--r--src/errors/InvalidOptionalElement.txt29
-rw-r--r--src/errors/InvalidOptionalLiteral.txt53
-rw-r--r--src/errors/InvalidOutputType.txt68
-rw-r--r--src/errors/InvalidPredicate.txt51
-rw-r--r--src/errors/MissingField.txt30
-rw-r--r--src/errors/MissingHandler.txt32
-rw-r--r--src/errors/MustCombineARecord.txt46
-rw-r--r--src/errors/MustMergeARecord.txt43
-rw-r--r--src/errors/MustMergeUnion.txt31
-rw-r--r--src/errors/NoDependentLet.txt76
-rw-r--r--src/errors/NoDependentTypes.txt31
-rw-r--r--src/errors/NotAFunction.txt68
-rw-r--r--src/errors/NotARecord.txt48
-rw-r--r--src/errors/TypeMismatch.txt117
-rw-r--r--src/errors/UnboundVariable.txt97
-rw-r--r--src/errors/Untyped.txt117
-rw-r--r--src/errors/UnusedHandler.txt32
-rw-r--r--src/generated_parser.rs6
-rw-r--r--src/grammar.lalrpop162
-rw-r--r--src/grammar_util.rs14
-rw-r--r--src/lexer.rs378
-rw-r--r--src/lib.rs12
-rw-r--r--src/main.rs101
-rw-r--r--src/parser.rs91
-rw-r--r--src/typecheck.rs616
45 files changed, 0 insertions, 4440 deletions
diff --git a/src/context.rs b/src/context.rs
deleted file mode 100644
index c2e1913..0000000
--- a/src/context.rs
+++ /dev/null
@@ -1,51 +0,0 @@
-use std::collections::HashMap;
-
-/// A `(Context a)` associates `Text` labels with values of type `a`
-///
-/// The `Context` is used for type-checking when `(a = Expr X)`
-///
-/// * You create a `Context` using `empty` and `insert`
-/// * You transform a `Context` using `fmap`
-/// * You consume a `Context` using `lookup` and `toList`
-///
-/// The difference between a `Context` and a `Map` is that a `Context` lets you
-/// have multiple ordered occurrences of the same key and you can query for the
-/// `n`th occurrence of a given key.
-///
-#[derive(Debug, Clone)]
-pub struct Context<'i, T>(HashMap<&'i str, Vec<T>>);
-
-impl<'i, T> Context<'i, T> {
- /// An empty context with no key-value pairs
- pub fn new() -> Self {
- Context(HashMap::new())
- }
-
- /// Look up a key by name and index
- ///
- /// ```c
- /// lookup _ _ empty = Nothing
- /// lookup k 0 (insert k v c) = Just v
- /// lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n
- /// lookup k n (insert j v c) = lookup k n c -- k /= j
- /// ```
- pub fn lookup<'a>(&'a self, k: &str, n: usize) -> Option<&'a T> {
- self.0.get(k).and_then(|v| v.get(v.len() - 1 - n))
- }
-
- pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> {
- Context(self.0.iter().map(|(k, v)| (*k, v.iter().map(&f).collect())).collect())
- }
-}
-
-impl<'i, T: Clone> Context<'i, T> {
- /// Add a key-value pair to the `Context`
- pub fn insert(&self, k: &'i str, v: T) -> Self {
- let mut ctx = (*self).clone();
- {
- let m = ctx.0.entry(k).or_insert_with(Vec::new);
- m.push(v);
- }
- ctx
- }
-}
diff --git a/src/core.rs b/src/core.rs
deleted file mode 100644
index 473a6a6..0000000
--- a/src/core.rs
+++ /dev/null
@@ -1,1056 +0,0 @@
-#![allow(non_snake_case)]
-use std::collections::BTreeMap;
-use std::fmt::{self, Display};
-use std::path::PathBuf;
-
-/*
-module Dhall.Core (
- -- * Syntax
- Const(..)
- , Path(..)
- , Var(..)
- , Expr(..)
-
- -- * Normalization
- , normalize
- , subst
- , shift
-
- -- * Pretty-printing
- , pretty
-
- -- * Miscellaneous
- , internalError
- ) where
-*/
-
-/// Constants for a pure type system
-///
-/// The only axiom is:
-///
-/// ```c
-/// ⊦ Type : Kind
-/// ```
-///
-/// ... and the valid rule pairs are:
-///
-/// ```c
-/// ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)
-/// ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions)
-/// ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors)
-/// ```
-///
-/// These are the same rule pairs as System Fω
-///
-/// Note that Dhall does not support functions from terms to types and therefore
-/// Dhall is not a dependently typed language
-///
-#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Show, Bounded, Enum)
-pub enum Const {
- Type,
- Kind,
-}
-
-
-/// Path to an external resource
-#[derive(Debug, Clone, PartialEq, Eq)] // (Eq, Ord, Show)
-pub enum Path {
- File(PathBuf),
- URL(String),
-}
-
-/// Label for a bound variable
-///
-/// The `String` field is the variable's name (i.e. \"`x`\").
-///
-/// The `Int` field disambiguates variables with the same name if there are
-/// multiple bound variables of the same name in scope. Zero refers to the
-/// nearest bound variable and the index increases by one for each bound
-/// variable of the same name going outward. The following diagram may help:
-///
-/// ```c
-/// +---refers to--+
-/// | |
-/// v |
-/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0
-///
-/// +------------------refers to-----------------+
-/// | |
-/// v |
-/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1
-/// ```
-///
-/// This `Int` behaves like a De Bruijn index in the special case where all
-/// variables have the same name.
-///
-/// You can optionally omit the index if it is `0`:
-///
-/// ```c
-/// +refers to+
-/// | |
-/// v |
-/// \(x : *) -> \(y : *) -> \(x : *) -> x
-/// ```
-///
-/// Zero indices are omitted when pretty-printing `Var`s and non-zero indices
-/// appear as a numeric suffix.
-///
-#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Eq, Show)
-pub struct V<'i>(pub &'i str, pub usize);
-
-/*
-instance IsString Var where
- fromString str = V (fromString str) 0
-
-instance Buildable Var where
- build = buildVar
-*/
-
-/// Syntax tree for expressions
-#[derive(Debug, Clone, PartialEq)] // (Functor, Foldable, Traversable, Show)
-pub enum Expr<'i, S, A> {
- /// `Const c ~ c`
- Const(Const),
- /// `Var (V x 0) ~ x`<br>
- /// `Var (V x n) ~ x@n`
- Var(V<'i>),
- /// `Lam x A b ~ λ(x : A) -> b`
- Lam(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Pi "_" A B ~ A -> B`
- /// `Pi x A B ~ ∀(x : A) -> B`
- Pi(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `App f A ~ f A`
- App(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Let x Nothing r e ~ let x = r in e`
- /// `Let x (Just t) r e ~ let x : t = r in e`
- Let(&'i str, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Annot x t ~ x : t`
- Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// Built-in types
- BuiltinType(BuiltinType),
- /// Built-in function values
- BuiltinValue(BuiltinValue),
- /// `BoolLit b ~ b`
- BoolLit(bool),
- /// `BoolAnd x y ~ x && y`
- BoolAnd(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `BoolOr x y ~ x || y`
- BoolOr(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `BoolEQ x y ~ x == y`
- BoolEQ(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `BoolNE x y ~ x != y`
- BoolNE(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `BoolIf x y z ~ if x then y else z`
- BoolIf(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `NaturalLit n ~ +n`
- NaturalLit(Natural),
- /// `NaturalPlus x y ~ x + y`
- NaturalPlus(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `NaturalTimes x y ~ x * y`
- NaturalTimes(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `IntegerLit n ~ n`
- IntegerLit(Integer),
- /// `DoubleLit n ~ n`
- DoubleLit(Double),
- /// `TextLit t ~ t`
- TextLit(Builder),
- /// `TextAppend x y ~ x ++ y`
- TextAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `ListLit t [x, y, z] ~ [x, y, z] : List t`
- ListLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
- /// `OptionalLit t [e] ~ [e] : Optional t`
- /// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
- /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
- Record(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
- RecordLit(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >`
- Union(BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >`
- UnionLit(&'i str, Box<Expr<'i, S, A>>, BTreeMap<&'i str, Expr<'i, S, A>>),
- /// `Combine x y ~ x ∧ y`
- Combine(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Merge x y t ~ merge x y : t`
- Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
- /// `Field e x ~ e.x`
- Field(Box<Expr<'i, S, A>>, &'i str),
- /// `Note S x ~ e`
- Note(S, Box<Expr<'i, S, A>>),
- /// `Embed path ~ path`
- Embed(A),
-}
-
-/// Built-in types
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinType {
- /// `Bool ~ Bool`
- Bool,
- /// `Natural ~ Natural`
- Natural,
- /// `Integer ~ Integer`
- Integer,
- /// `Double ~ Double`
- Double,
- /// `Text ~ Text`
- Text,
- /// `List ~ List`
- List,
- /// `Optional ~ Optional`
- Optional,
-}
-
-/// Built-in function values
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinValue {
- /// `NaturalFold ~ Natural/fold`
- NaturalFold,
- /// `NaturalBuild ~ Natural/build`
- NaturalBuild,
- /// `NaturalIsZero ~ Natural/isZero`
- NaturalIsZero,
- /// `NaturalEven ~ Natural/even`
- NaturalEven,
- /// `NaturalOdd ~ Natural/odd`
- NaturalOdd,
- NaturalShow,
- /// `ListBuild ~ List/build`
- ListBuild,
- /// `ListFold ~ List/fold`
- ListFold,
- /// `ListLength ~ List/length`
- ListLength,
- /// `ListHead ~ List/head`
- ListHead,
- /// `ListLast ~ List/last`
- ListLast,
- /// `ListIndexed ~ List/indexed`
- ListIndexed,
- /// `ListReverse ~ List/reverse`
- ListReverse,
- /// `OptionalFold ~ Optional/fold`
- OptionalFold,
-}
-
-impl<'i> From<&'i str> for V<'i> {
- fn from(s: &'i str) -> Self {
- V(s, 0)
- }
-}
-
-impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
- fn from(s: &'i str) -> Self {
- Expr::Var(s.into())
- }
-}
-
-impl<'i, S, A> From<BuiltinType> for Expr<'i, S, A> {
- fn from(t: BuiltinType) -> Self {
- Expr::BuiltinType(t)
- }
-}
-
-impl<'i, S, A> From<BuiltinValue> for Expr<'i, S, A> {
- fn from(t: BuiltinValue) -> Self {
- Expr::BuiltinValue(t)
- }
-}
-
-impl<'i, S, A> Expr<'i, S, A> {
- fn bool_lit(&self) -> Option<bool> {
- match *self {
- Expr::BoolLit(v) => Some(v),
- _ => None,
- }
- }
-
- fn natural_lit(&self) -> Option<usize> {
- match *self {
- Expr::NaturalLit(v) => Some(v),
- _ => None,
- }
- }
-
- fn text_lit(&self) -> Option<String> {
- match *self {
- Expr::TextLit(ref t) => Some(t.clone()), // FIXME?
- _ => None,
- }
- }
-}
-
-// There is a one-to-one correspondence between the formatters in this section
-// and the grammar in grammar.lalrpop. Each formatter is named after the
-// corresponding grammar rule and the relationship between formatters exactly matches
-// the relationship between grammar rules. This leads to the nice emergent property
-// of automatically getting all the parentheses and precedences right.
-//
-// This approach has one major disadvantage: you can get an infinite loop if
-// you add a new constructor to the syntax tree without adding a matching
-// case the corresponding builder.
-
-impl<'i, S, A: Display> Display for Expr<'i, S, A> {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { // buildExprA
- use crate::Expr::*;
- match self {
- &Annot(ref a, ref b) => { a.fmt_b(f)?; write!(f, " : ")?; b.fmt(f) }
- &Note(_, ref b) => b.fmt(f),
- a => a.fmt_b(f),
- }
- }
-}
-
-impl<'i, S, A: Display> Expr<'i, S, A> {
- fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Lam(a, ref b, ref c) => {
- write!(f, "λ({} : ", a)?;
- b.fmt(f)?;
- write!(f, ") → ")?;
- c.fmt_b(f)
- }
- &BoolIf(ref a, ref b, ref c) => {
- write!(f, "if ")?;
- a.fmt(f)?;
- write!(f, " then ")?;
- b.fmt_b(f)?;
- write!(f, " else ")?;
- c.fmt_c(f)
- }
- &Pi("_", ref b, ref c) => {
- b.fmt_c(f)?;
- write!(f, " → ")?;
- c.fmt_b(f)
- }
- &Pi(a, ref b, ref c) => {
- write!(f, "∀({} : ", a)?;
- b.fmt(f)?;
- write!(f, ") → ")?;
- c.fmt_b(f)
- }
- &Let(a, None, ref c, ref d) => {
- write!(f, "let {} = ", a)?;
- c.fmt(f)?;
- write!(f, ") → ")?;
- d.fmt_b(f)
- }
- &Let(a, Some(ref b), ref c, ref d) => {
- write!(f, "let {} : ", a)?;
- b.fmt(f)?;
- write!(f, " = ")?;
- c.fmt(f)?;
- write!(f, ") → ")?;
- d.fmt_b(f)
- }
- &ListLit(ref t, ref es) => {
- fmt_list("[", "] : List ", es, f, |e, f| e.fmt(f))?;
- t.fmt_e(f)
- }
- &OptionalLit(ref t, ref es) => {
- fmt_list("[", "] : Optional ", es, f, |e, f| e.fmt(f))?;
- t.fmt_e(f)
- }
- &Merge(ref a, ref b, ref c) => {
- write!(f, "merge ")?;
- a.fmt_e(f)?;
- write!(f, " ")?;
- b.fmt_e(f)?;
- write!(f, " : ")?;
- c.fmt_d(f)
- }
- &Note(_, ref b) => b.fmt_b(f),
- a => a.fmt_c(f),
- }
- }
-
- fn fmt_c(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- // FIXME precedence
- &BoolOr(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" || ")?; b.fmt_c(f) }
- &TextAppend(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ++ ")?; b.fmt_c(f) }
- &NaturalPlus(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" + ")?; b.fmt_c(f) }
- &BoolAnd(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" && ")?; b.fmt_c(f) }
- &Combine(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ^ ")?; b.fmt_c(f) }
- &NaturalTimes(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" * ")?; b.fmt_c(f) }
- &BoolEQ(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" == ")?; b.fmt_c(f) }
- &BoolNE(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" != ")?; b.fmt_c(f) }
- &Note(_, ref b) => b.fmt_c(f),
- a => a.fmt_d(f),
- }
- }
-
- fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &App(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ")?; b.fmt_e(f) }
- &Note(_, ref b) => b.fmt_d(f),
- a => a.fmt_e(f)
- }
- }
-
- fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Field(ref a, b) => { a.fmt_e(f)?; write!(f, ".{}", b) }
- &Note(_, ref b) => b.fmt_e(f),
- a => a.fmt_f(f)
- }
- }
-
- fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::Expr::*;
- match self {
- &Var(a) => a.fmt(f),
- &Const(k) => k.fmt(f),
- &BuiltinType(t) => t.fmt(f),
- &BuiltinValue(v) => v.fmt(f),
- &BoolLit(true) => f.write_str("True"),
- &BoolLit(false) => f.write_str("False"),
- &IntegerLit(a) => a.fmt(f),
- &NaturalLit(a) => {
- f.write_str("+")?;
- a.fmt(f)
- }
- &DoubleLit(a) => a.fmt(f),
- &TextLit(ref a) => <String as fmt::Debug>::fmt(a, f), // FIXME Format with Haskell escapes
- &Record(ref a) if a.is_empty() => f.write_str("{}"),
- &Record(ref a) => {
- fmt_list("{ ", " }", a, f, |(k, t), f| write!(f, "{} : {}", k, t))
- }
- &RecordLit(ref a) if a.is_empty() => f.write_str("{=}"),
- &RecordLit(ref a) => {
- fmt_list("{ ", " }", a, f, |(k, v), f| write!(f, "{} = {}", k, v))
- }
- &Union(ref _a) => f.write_str("Union"),
- &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"),
- &Embed(ref a) => a.fmt(f),
- &Note(_, ref b) => b.fmt_f(f),
- a => write!(f, "({})", a),
- }
- }
-}
-
-fn fmt_list<T, I, F>(open: &str,
- close: &str,
- it: I,
- f: &mut fmt::Formatter,
- func: F)
- -> Result<(), fmt::Error>
- where I: IntoIterator<Item = T>,
- F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>
-{
- f.write_str(open)?;
- for (i, x) in it.into_iter().enumerate() {
- if i > 0 {
- f.write_str(", ")?;
- }
- func(x, f)?;
- }
- f.write_str(close)
-}
-
-impl Display for Const {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- <Self as fmt::Debug>::fmt(self, f)
- }
-}
-
-impl Display for BuiltinType {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- <Self as fmt::Debug>::fmt(self, f)
- }
-}
-
-impl Display for BuiltinValue {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::BuiltinValue::*;
- f.write_str(match *self {
- ListBuild => "List/build",
- ListFold => "List/fold",
- ListHead => "List/head",
- ListIndexed => "List/indexed",
- ListLast => "List/last",
- ListLength => "List/length",
- ListReverse => "List/reverse",
- NaturalBuild => "Natural/build",
- NaturalEven => "Natural/even",
- NaturalFold => "Natural/fold",
- NaturalIsZero => "Natural/isZero",
- NaturalOdd => "Natural/odd",
- NaturalShow => "Natural/show",
- OptionalFold => "Optional/fold",
- })
- }
-}
-
-impl<'i> Display for V<'i> {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- let V(x, n) = *self;
- f.write_str(x)?;
- if n != 0 {
- write!(f, "@{}", n)?;
- }
- Ok(())
- }
-}
-
-pub fn pi<'i, S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<'i, S, A>
- where Name: Into<&'i str>,
- Et: Into<Expr<'i, S, A>>,
- Ev: Into<Expr<'i, S, A>>
-{
- Expr::Pi(var.into(), bx(ty.into()), bx(value.into()))
-}
-
-pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A>
- where Ef: Into<Expr<'i, S, A>>,
- Ex: Into<Expr<'i, S, A>>
-{
- Expr::App(bx(f.into()), bx(x.into()))
-}
-
-pub type Builder = String;
-pub type Double = f64;
-pub type Int = isize;
-pub type Integer = isize;
-pub type Natural = usize;
-
-/// A void type
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum X {}
-
-impl Display for X {
- fn fmt(&self, _: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- match *self {}
- }
-}
-
-pub fn bx<T>(x: T) -> Box<T> {
- Box::new(x)
-}
-
-fn add_ui(u: usize, i: isize) -> usize {
- if i < 0 {
- u.checked_sub(i.checked_neg().unwrap() as usize).unwrap()
- } else {
- u.checked_add(i as usize).unwrap()
- }
-}
-
-fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
- where I: IntoIterator<Item = (&'a K, &'a V)>,
- K: Eq + Ord + Copy + 'a,
- V: 'a,
- F: Fn(&V) -> U
-{
- it.into_iter().map(|(&k, v)| (k, f(v))).collect()
-}
-
-fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V
- where F: FnOnce(U, U) -> V,
- G: Fn(T) -> U,
-{
- f(g(a), g(b))
-}
-
-/// `shift` is used by both normalization and type-checking to avoid variable
-/// capture by shifting variable indices
-///
-/// For example, suppose that you were to normalize the following expression:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
-/// ```
-///
-/// If you were to substitute `y` with `x` without shifting any variable
-/// indices, then you would get the following incorrect result:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form
-/// ```
-///
-/// In order to substitute `x` in place of `y` we need to `shift` `x` by `1` in
-/// order to avoid being misinterpreted as the `x` bound by the innermost
-/// lambda. If we perform that `shift` then we get the correct result:
-///
-/// ```c
-/// λ(a : Type) → λ(x : a) → λ(x : a) → x@1
-/// ```
-///
-/// As a more worked example, suppose that you were to normalize the following
-/// expression:
-///
-/// ```c
-/// λ(a : Type)
-/// → λ(f : a → a → a)
-/// → λ(x : a)
-/// → λ(x : a)
-/// → (λ(x : a) → f x x@1) x@1
-/// ```
-///
-/// The correct normalized result would be:
-///
-/// ```c
-/// λ(a : Type)
-/// → λ(f : a → a → a)
-/// → λ(x : a)
-/// → λ(x : a)
-/// → f x@1 x
-/// ```
-///
-/// The above example illustrates how we need to both increase and decrease
-/// variable indices as part of substitution:
-///
-/// * We need to increase the index of the outer `x\@1` to `x\@2` before we
-/// substitute it into the body of the innermost lambda expression in order
-/// to avoid variable capture. This substitution changes the body of the
-/// lambda expression to `(f x\@2 x\@1)`
-///
-/// * We then remove the innermost lambda and therefore decrease the indices of
-/// both `x`s in `(f x\@2 x\@1)` to `(f x\@1 x)` in order to reflect that one
-/// less `x` variable is now bound within that scope
-///
-/// Formally, `(shift d (V x n) e)` modifies the expression `e` by adding `d` to
-/// the indices of all variables named `x` whose indices are greater than
-/// `(n + m)`, where `m` is the number of bound variables of the same name
-/// within that scope
-///
-/// In practice, `d` is always `1` or `-1` because we either:
-///
-/// * increment variables by `1` to avoid variable capture during substitution
-/// * decrement variables by `1` when deleting lambdas after substitution
-///
-/// `n` starts off at `0` when substitution begins and increments every time we
-/// descend into a lambda or let expression that binds a variable of the same
-/// name in order to avoid shifting the bound variables by mistake.
-///
-pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i, T, A> {
- use crate::Expr::*;
- let V(x, n) = v;
- match *e {
- Const(a) => Const(a),
- Var(V(x2, n2)) => {
- let n3 = if x == x2 && n <= n2 { add_ui(n2, d) } else { n2 };
- Var(V(x2, n3))
- }
- Lam(x2, ref tA, ref b) => {
- let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x, n ), tA);
- let b2 = shift(d, V(x, n2), b);
- Lam(x2, bx(tA2), bx(b2))
- }
- Pi(x2, ref tA, ref tB) => {
- let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x, n ), tA);
- let tB2 = shift(d, V(x, n2), tB);
- pi(x2, tA2, tB2)
- }
- App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)),
- Let(f, ref mt, ref r, ref e) => {
- let n2 = if x == f { n + 1 } else { n };
- let e2 = shift(d, V(x, n2), e);
- let mt2 = mt.as_ref().map(|t| bx(shift(d, V(x, n), t)));
- let r2 = shift(d, V(x, n), r);
- Let(f, mt2, bx(r2), bx(e2))
- }
- Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
- BoolLit(a) => BoolLit(a),
- BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b),
- BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b),
- BoolEQ(ref a, ref b) => shift_op2(BoolEQ, d, v, a, b),
- BoolNE(ref a, ref b) => shift_op2(BoolNE, d, v, a, b),
- BoolIf(ref a, ref b, ref c) => {
- BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
- }
- NaturalLit(a) => NaturalLit(a),
- NaturalPlus(ref a, ref b) => NaturalPlus(bx(shift(d, v, a)), bx(shift(d, v, b))),
- NaturalTimes(ref a, ref b) => shift_op2(NaturalTimes, d, v, a, b),
- IntegerLit(a) => IntegerLit(a),
- DoubleLit(a) => DoubleLit(a),
- TextLit(ref a) => TextLit(a.clone()),
- TextAppend(ref a, ref b) => shift_op2(TextAppend, d, v, a, b),
- ListLit(ref t, ref es) => {
- ListLit(bx(shift(d, v, t)),
- es.iter().map(|e| shift(d, v, e)).collect())
- }
- OptionalLit(ref t, ref es) => {
- OptionalLit(bx(shift(d, v, t)),
- es.iter().map(|e| shift(d, v, e)).collect())
- }
- Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))),
- RecordLit(ref a) => RecordLit(map_record_value(a, |val| shift(d, v, val))),
- Union(ref a) => Union(map_record_value(a, |val| shift(d, v, val))),
- UnionLit(k, ref uv, ref a) => {
- UnionLit(k,
- bx(shift(d, v, uv)),
- map_record_value(a, |val| shift(d, v, val)))
- }
- Combine(ref a, ref b) => shift_op2(Combine, d, v, a, b),
- Merge(ref a, ref b, ref c) => {
- Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
- }
- Field(ref a, b) => Field(bx(shift(d, v, a)), b),
- Note(_, ref b) => shift(d, v, b),
- // The Dhall compiler enforces that all embedded values are closed expressions
- // and `shift` does nothing to a closed expression
- Embed(ref p) => Embed(p.clone()),
- }
-}
-
-fn shift_op2<'i, S, T, A, F>(f: F,
- d: isize,
- v: V,
- a: &Expr<'i, S, A>,
- b: &Expr<'i, S, A>)
- -> Expr<'i, T, A>
- where F: FnOnce(Box<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> Expr<'i, T, A>,
- A: Clone
-{
- map_op2(f, |x| bx(shift(d, v, x)), a, b)
-}
-
-/// Substitute all occurrences of a variable with an expression
-///
-/// ```c
-/// subst x C B ~ B[x := C]
-/// ```
-///
-pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> Expr<'i, S, A>
- where S: Clone,
- A: Clone
-{
- use crate::Expr::*;
- let V(x, n) = v;
- match *b {
- Const(a) => Const(a),
- Lam(y, ref tA, ref b) => {
- let n2 = if x == y { n + 1 } else { n };
- let b2 = subst(V(x, n2), &shift(1, V(y, 0), e), b);
- let tA2 = subst(V(x, n), e, tA);
- Lam(y, bx(tA2), bx(b2))
- }
- Pi(y, ref tA, ref tB) => {
- let n2 = if x == y { n + 1 } else { n };
- let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB);
- let tA2 = subst(V(x, n), e, tA);
- pi(y, tA2, tB2)
- }
- App(ref f, ref a) => {
- let f2 = subst(v, e, f);
- let a2 = subst(v, e, a);
- app(f2, a2)
- }
- Var(v2) => if v == v2 { e.clone() } else { Var(v2) },
- Let(f, ref mt, ref r, ref b) => {
- let n2 = if x == f { n + 1 } else { n };
- let b2 = subst(V(x, n2), &shift(1, V(f, 0), e), b);
- let mt2 = mt.as_ref().map(|t| bx(subst(V(x, n), e, t)));
- let r2 = subst(V(x, n), e, r);
- Let(f, mt2, bx(r2), bx(b2))
- }
- Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
- BoolLit(a) => BoolLit(a),
- BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b),
- BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b),
- BoolEQ(ref a, ref b) => subst_op2(BoolEQ, v, e, a, b),
- BoolNE(ref a, ref b) => subst_op2(BoolNE, v, e, a, b),
- BoolIf(ref a, ref b, ref c) => {
- BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
- }
- NaturalLit(a) => NaturalLit(a),
- NaturalPlus(ref a, ref b) => subst_op2(NaturalPlus, v, e, a, b),
- NaturalTimes(ref a, ref b) => subst_op2(NaturalTimes, v, e, a, b),
- IntegerLit(a) => IntegerLit(a),
- DoubleLit(a) => DoubleLit(a),
- TextLit(ref a) => TextLit(a.clone()),
- TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b),
- ListLit(ref a, ref b) => {
- let a2 = subst(v, e, a);
- let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- ListLit(bx(a2), b2)
- }
- OptionalLit(ref a, ref b) => {
- let a2 = subst(v, e, a);
- let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- OptionalLit(bx(a2), b2)
- }
- Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))),
- RecordLit(ref kvs) => RecordLit(map_record_value(kvs, |val| subst(v, e, val))),
- Union(ref kts) => Union(map_record_value(kts, |t| subst(v, e, t))),
- UnionLit(k, ref uv, ref kvs) => {
- UnionLit(k,
- bx(subst(v, e, uv)),
- map_record_value(kvs, |val| subst(v, e, val)))
- }
- Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b),
- Merge(ref a, ref b, ref c) => {
- Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
- }
- Field(ref a, b) => Field(bx(subst(v, e, a)), b),
- Note(_, ref b) => subst(v, e, b),
- Embed(ref p) => Embed(p.clone()),
- }
-}
-
-fn subst_op2<'i, S, T, A, F>(f: F,
- v: V<'i>,
- e: &Expr<'i, S, A>,
- a: &Expr<'i, T, A>,
- b: &Expr<'i, T, A>)
- -> Expr<'i, S, A>
- where F: FnOnce(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> Expr<'i, S, A>,
- S: Clone,
- A: Clone
-{
- map_op2(f, |x| bx(subst(v, e, x)), a, b)
-}
-
-/// Reduce an expression to its normal form, performing beta reduction
-///
-/// `normalize` does not type-check the expression. You may want to type-check
-/// expressions before normalizing them since normalization can convert an
-/// ill-typed expression into a well-typed expression.
-///
-/// However, `normalize` will not fail if the expression is ill-typed and will
-/// leave ill-typed sub-expressions unevaluated.
-///
-pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
- where S: Clone + fmt::Debug,
- T: Clone + fmt::Debug,
- A: Clone + fmt::Debug,
-{
- use crate::BuiltinValue::*;
- use crate::Expr::*;
- match *e {
- Const(k) => Const(k),
- Var(v) => Var(v),
- Lam(x, ref tA, ref b) => {
- let tA2 = normalize(tA);
- let b2 = normalize(b);
- Lam(x, bx(tA2), bx(b2))
- }
- Pi(x, ref tA, ref tB) => {
- let tA2 = normalize(tA);
- let tB2 = normalize(tB);
- pi(x, tA2, tB2)
- }
- App(ref f, ref a) => match normalize::<S, T, A>(f) {
- Lam(x, _A, b) => { // Beta reduce
- let vx0 = V(x, 0);
- let a2 = shift::<S, S, A>( 1, vx0, a);
- let b2 = subst::<S, T, A>(vx0, &a2, &b);
- let b3 = shift::<S, T, A>(-1, vx0, &b2);
- normalize(&b3)
- }
- f2 => match (f2, normalize::<S, T, A>(a)) {
- // fold/build fusion for `List`
- (App(box BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) |
- (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) |
-
- // fold/build fusion for `Natural`
- (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) |
- (BuiltinValue(NaturalFold), App(box BuiltinValue(NaturalBuild), box e2)) => normalize(&e2),
-
- /*
- App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
- normalize (go n0)
- where
- go !0 = zero
- go !n = App succ' (go (n - 1))
- App NaturalBuild k
- | check -> NaturalLit n
- | otherwise -> App f' a'
- where
- labeled =
- normalize (App (App (App k Natural) "Succ") "Zero")
-
- n = go 0 labeled
- where
- go !m (App (Var "Succ") e') = go (m + 1) e'
- go !m (Var "Zero") = m
- go !_ _ = internalError text
- check = go labeled
- where
- go (App (Var "Succ") e') = go e'
- go (Var "Zero") = True
- go _ = False
- */
- (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
- (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
- (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
- (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
- (App(f@box BuiltinValue(ListBuild), box t), k) => {
- let labeled =
- normalize::<_, T, _>(&app(app(app(k.clone(), app(
- BuiltinType(self::BuiltinType::List), t.clone())), "Cons"), "Nil"));
-
- fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
- where S: Clone, A: Clone
- {
- match e {
- App(box App(box Var(V("Cons", _)), box x), box e2) => {
- v.push(x);
- list_to_vector(v, e2)
- }
- Var(V("Nil", _)) => {}
- _ => panic!("internalError list_to_vector"),
- }
- }
- fn check<S, A>(e: &Expr<S, A>) -> bool {
- match *e {
- App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2),
- Var(V("Nil", _)) => true,
- _ => false,
- }
- }
-
- if check(&labeled) {
- let mut v = vec![];
- list_to_vector(&mut v, labeled);
- ListLit(bx(t), v)
- } else {
- app(App(f, bx(t)), k)
- }
- }
- (App(box App(box App(box App(box BuiltinValue(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
- let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
- App(bx(App(cons.clone(), bx(y))), bx(ys))
- );
- normalize(&e2)
- }
- (App(f, x_), ListLit(t, ys)) => match *f {
- BuiltinValue(ListLength) =>
- NaturalLit(ys.len()),
- BuiltinValue(ListHead) =>
- normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
- BuiltinValue(ListLast) =>
- normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
- BuiltinValue(ListReverse) => {
- let mut xs = ys;
- xs.reverse();
- normalize(&ListLit(t, xs))
- }
- _ => app(App(f, x_), ListLit(t, ys)),
- },
- /*
- App (App ListIndexed _) (ListLit t xs) ->
- normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
- where
- t' = Record (Data.Map.fromList kts)
- where
- kts = [ ("index", Natural)
- , ("value", t)
- ]
- adapt (n, x) = RecordLit (Data.Map.fromList kvs)
- where
- kvs = [ ("index", NaturalLit (fromIntegral n))
- , ("value", x)
- ]
- App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
- normalize (maybe nothing just' (toMaybe xs))
- where
- just' y = App just y
- toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList
- */
- (f2, a2) => app(f2, a2),
- }
- },
- Let(f, _, ref r, ref b) => {
- let r2 = shift::<_, S, _>( 1, V(f, 0), r);
- let b2 = subst(V(f, 0), &r2, b);
- let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
- normalize(&b3)
- }
- Annot(ref x, _) => normalize(x),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
- BoolLit(b) => BoolLit(b),
- BoolAnd(ref x, ref y) => {
- with_binop(BoolAnd, Expr::bool_lit,
- |xn, yn| BoolLit(xn && yn),
- normalize(x), normalize(y))
- }
- BoolOr(ref x, ref y) => {
- with_binop(BoolOr, Expr::bool_lit,
- |xn, yn| BoolLit(xn || yn),
- normalize(x), normalize(y))
- }
- BoolEQ(ref x, ref y) => {
- with_binop(BoolEQ, Expr::bool_lit,
- |xn, yn| BoolLit(xn == yn),
- normalize(x), normalize(y))
- }
- BoolNE(ref x, ref y) => {
- with_binop(BoolNE, Expr::bool_lit,
- |xn, yn| BoolLit(xn != yn),
- normalize(x), normalize(y))
- }
- BoolIf(ref b, ref t, ref f) => match normalize(b) {
- BoolLit(true) => normalize(t),
- BoolLit(false) => normalize(f),
- b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))),
- },
- NaturalLit(n) => NaturalLit(n),
- NaturalPlus(ref x, ref y) => {
- with_binop(NaturalPlus, Expr::natural_lit,
- |xn, yn| NaturalLit(xn + yn),
- normalize(x), normalize(y))
- }
- NaturalTimes(ref x, ref y) => {
- with_binop(NaturalTimes, Expr::natural_lit,
- |xn, yn| NaturalLit(xn * yn),
- normalize(x), normalize(y))
- }
- IntegerLit(n) => IntegerLit(n),
- DoubleLit(n) => DoubleLit(n),
- TextLit(ref t) => TextLit(t.clone()),
- TextAppend(ref x, ref y) => {
- with_binop(TextAppend, Expr::text_lit,
- |xt, yt| TextLit(xt + &yt),
- normalize(x), normalize(y))
- }
- ListLit(ref t, ref es) => {
- let t2 = normalize(t);
- let es2 = es.iter().map(normalize).collect();
- ListLit(bx(t2), es2)
- }
- OptionalLit(ref t, ref es) => {
- let t2 = normalize(t);
- let es2 = es.iter().map(normalize).collect();
- OptionalLit(bx(t2), es2)
- }
- Record(ref kts) => Record(map_record_value(kts, normalize)),
- RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
- Union(ref kts) => Union(map_record_value(kts, normalize)),
- UnionLit(k, ref v, ref kvs) => UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize)),
- Combine(ref _x0, ref _y0) => unimplemented!(),
- Merge(ref _x, ref _y, ref _t) => unimplemented!(),
- Field(ref r, x) => match normalize(r) {
- RecordLit(kvs) => match kvs.get(x) {
- Some(r2) => normalize(r2),
- None => Field(bx(RecordLit(map_record_value(&kvs, normalize))), x),
- },
- r2 => Field(bx(r2), x),
- },
- Note(_, ref e) => normalize(e),
- Embed(ref a) => Embed(a.clone()),
- }
-}
-
-fn with_binop<T, U, Get, Set, Op>(op: Op, get: Get, set: Set, x: T, y: T) -> T
- where Get: Fn(&T) -> Option<U>,
- Set: FnOnce(U, U) -> T,
- Op: FnOnce(Box<T>, Box<T>) -> T,
-{
- if let (Some(xv), Some(yv)) = (get(&x), get(&y)) {
- set(xv, yv)
- } else {
- op(bx(x), bx(y))
- }
-}
diff --git a/src/dhall.pest.visibility b/src/dhall.pest.visibility
deleted file mode 100644
index c09fccf..0000000
--- a/src/dhall.pest.visibility
+++ /dev/null
@@ -1,188 +0,0 @@
-# end_of_line
-# tab
-# block_comment
-# block_comment_chunk
-# block_comment_continue
-# not_end_of_line
-# line_comment
-# whitespace_chunk
-# whitespace
-# nonempty_whitespace
-# ALPHA
-# DIGIT
-# HEXDIG
-# simple_label
-# quoted_label
-# label
-# double_quote_chunk
-# double_quote_literal
-# single_quote_continue
-# single_quote_literal
-# text_literal
-# if_raw
-# then_raw
-# else_raw
-# let_raw
-# in_raw
-# as_raw
-# using_raw
-# merge_raw
-# missing_raw
-# Some_raw
-# constructors_raw
-# Natural_fold_raw
-# Natural_build_raw
-# Natural_isZero_raw
-# Natural_even_raw
-# Natural_odd_raw
-# Natural_toInteger_raw
-# Natural_show_raw
-# Integer_toDouble_raw
-# Integer_show_raw
-# Double_show_raw
-# List_build_raw
-# List_fold_raw
-# List_length_raw
-# List_head_raw
-# List_last_raw
-# List_indexed_raw
-# List_reverse_raw
-# Optional_fold_raw
-# Optional_build_raw
-# Text_show_raw
-# Bool_raw
-# Optional_raw
-# None_raw
-# Natural_raw
-# Integer_raw
-# Double_raw
-# Text_raw
-# List_raw
-# True_raw
-# False_raw
-# NaN_raw
-# Infinity_raw
-# Type_raw
-# Kind_raw
-# Sort_raw
-# reserved_raw
-# reserved_namespaced_raw
-# reserved
-# reserved_namespaced
-# if_
-# then_
-# else_
-# let_
-# in_
-# as_
-# using
-# merge
-# constructors
-# Some
-# Optional
-# Text
-# List
-# equal
-# or
-# plus
-# text_append
-# list_append
-# and
-# times
-# double_equal
-# not_equal
-# dot
-# open_brace
-# close_brace
-# open_bracket
-# close_bracket
-# open_angle
-# close_angle
-# bar
-# comma
-# open_parens
-# close_parens
-# at
-# colon
-# import_alt
-# combine
-# combine_types
-# prefer
-# lambda
-# forall
-# arrow
-# exponent
-# double_literal
-# natural_literal_raw
-integer_literal
-natural_literal
-# identifier
-# identifier_reserved_prefix
-# identifier_reserved_namespaced_prefix
-# missing
-# path_character
-# quoted_path_character
-# path_component
-# directory
-# file
-# local_raw
-# local
-# scheme
-# http_raw
-# authority
-# userinfo
-# host
-# port
-# IP_literal
-# IPvFuture
-# IPv6address
-# h16
-# ls32
-# IPv4address
-# dec_octet
-# reg_name
-# pchar
-# query
-# fragment
-# pct_encoded
-# unreserved
-# sub_delims
-# http
-# env
-# bash_environment_variable
-# posix_environment_variable
-# posix_environment_variable_character
-# import_type
-# hash
-# import_hashed
-# import
-# expression
-# annotated_expression
-# empty_collection
-# non_empty_optional
-# operator_expression
-# import_alt_expression
-# or_expression
-plus_expression
-# text_append_expression
-# list_append_expression
-# and_expression
-# combine_expression
-# prefer_expression
-# combine_types_expression
-times_expression
-# equal_expression
-# not_equal_expression
-# application_expression
-# import_expression
-# selector_expression
-# primitive_expression
-# labels
-# record_type_or_literal
-# non_empty_record_type_or_literal
-# non_empty_record_type
-# non_empty_record_literal
-# union_type_or_literal
-# non_empty_union_type_or_literal
-# non_empty_list_literal
-# complete_expression
diff --git a/src/errors/AnnotMismatch.txt b/src/errors/AnnotMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/src/errors/AnnotMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
- ┌───────────────────────────────┐
- │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have type ❰Bool❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ Natural/even : Natural → Bool │ This built-in function only accepts
- └───────────────────────────────┘ arguments that have type ❰Natural❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have kind ❰Type❱
- ⇧
- The function's input kind
-
-
- ┌────────────────────┐
- │ List : Type → Type │ This built-in function only accepts arguments that
- └────────────────────┘ have kind ❰Type❱
- ⇧
- The function's input kind
-
-
-For example, the following expressions are valid:
-
-
- ┌────────────────────────┐
- │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌─────────────────┐
- │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
- └─────────────────┘ argument that the ❰Natural/even❱ function accepts,
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌───────────┐
- │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
- └───────────┘ that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
- ┌───────────────────────┐
- │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function
- └───────────────────────┘ expects an argument that has type ❰Bool❱
-
-
- ┌──────────────────┐
- │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
- └──────────────────┘ expects an argument that has type ❰Natural❱
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
- └────────────────────────┘ function expects an argument of kind ❰Type❱
-
-
- ┌────────┐
- │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
- └────────┘ argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
- ┌────────────────────────────────────────┐
- │ List/head ([1, 2, 3] : List Integer) │
- └────────────────────────────────────────┘
- ⇧
- ❰List/head❱ is missing the first argument,
- which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
- ┌────────────────┐
- │ Natural/even 2 │
- └────────────────┘
- ⇧
- This should be ❰+2❱
diff --git a/src/errors/CantTextAppend.txt b/src/errors/CantTextAppend.txt
deleted file mode 100644
index 26b9ceb..0000000
--- a/src/errors/CantTextAppend.txt
+++ /dev/null
@@ -1,28 +0,0 @@
-Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱
-
-For example, this is a valid use of ❰++❱:
-
-
- ┌────────────────┐
- │ "ABC" ++ "DEF" │
- └────────────────┘
-
-
-You provided this argument:
-
-↳ $txt0
-
-... which does not have type ❰Text❱ but instead has type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You might have thought that ❰++❱ was the operator to combine two lists:
-
- ┌───────────────────────────────────────────────────────────┐
- │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │ Not valid
- └───────────────────────────────────────────────────────────┘
-
- The Dhall programming language does not provide a built-in operator for
- combining two lists
diff --git a/src/errors/DuplicateAlternative.txt b/src/errors/DuplicateAlternative.txt
deleted file mode 100644
index 077f8aa..0000000
--- a/src/errors/DuplicateAlternative.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-Explanation: Unions may not have two alternatives that share the same name
-
-For example, the following expressions are $_NOT valid:
-
-
- ┌─────────────────────────────┐
- │ < foo = True | foo : Text > │ Invalid: ❰foo❱ appears twice
- └─────────────────────────────┘
-
-
- ┌───────────────────────────────────────┐
- │ < foo = 1 | bar : Bool | bar : Text > │ Invalid: ❰bar❱ appears twice
- └───────────────────────────────────────┘
-
-
-You have more than one alternative named:
-
-↳ $txt0
diff --git a/src/errors/FieldCollision.txt b/src/errors/FieldCollision.txt
deleted file mode 100644
index 2b2d260..0000000
--- a/src/errors/FieldCollision.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: You can combine records if they don't share any fields in common,
-like this:
-
-
- ┌───────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
- └───────────────────────────────────────────┘
-
-
- ┌────────────────────────────────────────┐
- │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │
- └────────────────────────────────────────┘
-
-
-... but you cannot merge two records that share the same field
-
-For example, the following expression is $_NOT valid:
-
-
- ┌───────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ fields
- └───────────────────────────────────────────┘
-
-
-You combined two records that share the following field:
-
-↳ $txt0
-
-... which is not allowed
-
-Some common reasons why you might get this error:
-
-● You tried to use ❰∧❱ to update a field's value, like this:
-
-
- ┌────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │
- └────────────────────────────────────────┘
- ⇧
- Invalid attempt to update ❰foo❱'s value to ❰2❱
-
- Field updates are intentionally not allowed as the Dhall language discourages
- patch-oriented programming
diff --git a/src/errors/HandlerInputTypeMismatch.txt b/src/errors/HandlerInputTypeMismatch.txt
deleted file mode 100644
index 7d3525b..0000000
--- a/src/errors/HandlerInputTypeMismatch.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as the input type of each handler function matches the type of the
-corresponding alternative:
-
-
- ┌───────────────────────────────────────────────────────────┐
- │ union : < Left : Natural | Right : Bool > │
- └───────────────────────────────────────────────────────────┘
- ⇧ ⇧
- These must match These must match
- ⇩ ⇩
- ┌───────────────────────────────────────────────────────────┐
- │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
- └───────────────────────────────────────────────────────────┘
-
-
-For example, the following expression is $_NOT valid:
-
-
- Invalid: Doesn't match the type of the ❰Right❱ alternative
- ⇩
- ┌──────────────────────────────────────────────────────────────────────┐
- │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │
- │ in let union = < Left = +2 | Right : Bool > │
- │ in merge handlers union : Bool │
- └──────────────────────────────────────────────────────────────────────┘
-
-
-Your handler for the following alternative:
-
-↳ $txt0
-
-... needs to accept an input value of type:
-
-↳ $txt1
-
-... but actually accepts an input value of a different type:
-
-↳ $txt2
diff --git a/src/errors/HandlerNotAFunction.txt b/src/errors/HandlerNotAFunction.txt
deleted file mode 100644
index ff87443..0000000
--- a/src/errors/HandlerNotAFunction.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as each handler is a function
-
-For example, the following expression is $_NOT valid:
-
-
- ┌─────────────────────────────────────────┐
- │ merge { Foo = True } < Foo = 1 > : Bool │
- └─────────────────────────────────────────┘
- ⇧
- Invalid: Not a function
-
-
-Your handler for this alternative:
-
-↳ $txt0
-
-... has the following type:
-
-↳ $txt1
-
-... which is not the type of a function
diff --git a/src/errors/HandlerOutputTypeMismatch.txt b/src/errors/HandlerOutputTypeMismatch.txt
deleted file mode 100644
index f359459..0000000
--- a/src/errors/HandlerOutputTypeMismatch.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as the output type of each handler function matches the declared type
-of the result:
-
-
- ┌───────────────────────────────────────────────────────────┐
- │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
- └───────────────────────────────────────────────────────────┘
- ⇧ ⇧
- These output types ...
-
- ... must match the declared type of the ❰merge❱
- ⇩
- ┌─────────────────────────────┐
- │ merge handlers union : Bool │
- └─────────────────────────────┘
-
-
-For example, the following expression is $_NOT valid:
-
-
- ┌──────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Text │
- └──────────────────────────────────────────────────────────────────────┘
- ⇧
- Invalid: Doesn't match output of either handler
-
-
-Your handler for the following alternative:
-
-↳ $txt0
-
-... needs to return an output value of type:
-
-↳ $txt1
-
-... but actually returns an output value of a different type:
-
-↳ $txt2
diff --git a/src/errors/IfBranchMismatch.txt b/src/errors/IfBranchMismatch.txt
deleted file mode 100644
index a95b130..0000000
--- a/src/errors/IfBranchMismatch.txt
+++ /dev/null
@@ -1,63 +0,0 @@
-Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which
-is an expression:
-
-
- Expression for ❰then❱ branch
- ⇩
- ┌────────────────────────────────┐
- │ if True then "Hello, world!" │
- │ else "Goodbye, world!" │
- └────────────────────────────────┘
- ⇧
- Expression for ❰else❱ branch
-
-
-These two expressions must have the same type. For example, the following ❰if❱
-expressions are all valid:
-
-
- ┌──────────────────────────────────┐
- │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱
- └──────────────────────────────────┘
-
-
- ┌────────────────────────────┐
- │ λ(b : Bool) → │
- │ if b then Natural/even │ Both branches have type ❰Natural → Bool❱
- │ else Natural/odd │
- └────────────────────────────┘
-
-
-However, the following expression is $_NOT valid:
-
-
- This branch has type ❰Integer❱
- ⇩
- ┌────────────────────────┐
- │ if True then 0 │
- │ else "ABC" │
- └────────────────────────┘
- ⇧
- This branch has type ❰Text❱
-
-
-The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is
-always ❰True❱ or ❰False❱
-
-Your ❰if❱ expression has the following ❰then❱ branch:
-
-↳ $txt0
-
-... which has type:
-
-↳ $txt2
-
-... and the following ❰else❱ branch:
-
-↳ $txt1
-
-... which has a different type:
-
-↳ $txt3
-
-Fix your ❰then❱ and ❰else❱ branches to have matching types
diff --git a/src/errors/IfBranchMustBeTerm.txt b/src/errors/IfBranchMustBeTerm.txt
deleted file mode 100644
index 4c15881..0000000
--- a/src/errors/IfBranchMustBeTerm.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: Every ❰if❱ expression begins with a predicate which must have type
-❰Bool❱
-
-For example, these are valid ❰if❱ expressions:
-
-
- ┌──────────────────────────────┐
- │ if True then "Yes" else "No" │
- └──────────────────────────────┘
- ⇧
- Predicate
-
-
- ┌─────────────────────────────────────────┐
- │ λ(x : Bool) → if x then False else True │
- └─────────────────────────────────────────┘
- ⇧
- Predicate
-
-
-... but these are $_NOT valid ❰if❱ expressions:
-
-
- ┌───────────────────────────┐
- │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱
- └───────────────────────────┘
-
-
- ┌────────────────────────────┐
- │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱
- └────────────────────────────┘
-
-
-Your ❰if❱ expression begins with the following predicate:
-
-↳ $txt0
-
-... that has type:
-
-↳ $txt1
-
-... but the predicate must instead have type ❰Bool❱
-
-Some common reasons why you might get this error:
-
-● You might be used to other programming languages that accept predicates other
- than ❰Bool❱
-
- For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
- them as equivalent to ❰False❱. However, the Dhall language does not permit
- this
diff --git a/src/errors/InvalidAlterantive.txt b/src/errors/InvalidAlterantive.txt
deleted file mode 100644
index 391fc3a..0000000
--- a/src/errors/InvalidAlterantive.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-Explanation: Every union type specifies the type of each alternative, like this:
-
-
- The type of the first alternative is ❰Bool❱
- ⇩
- ┌──────────────────────────────────┐
- │ < Left : Bool, Right : Natural > │ A union type with two alternatives
- └──────────────────────────────────┘
- ⇧
- The type of the second alternative is ❰Natural❱
-
-
-However, these alternatives can only be annotated with types. For example, the
-following union types are $_NOT valid:
-
-
- ┌────────────────────────────┐
- │ < Left : Bool, Right : 1 > │ Invalid union type
- └────────────────────────────┘
- ⇧
- This is a term and not a type
-
-
- ┌───────────────────────────────┐
- │ < Left : Bool, Right : Type > │ Invalid union type
- └───────────────────────────────┘
- ⇧
- This is a kind and not a type
-
-
-You provided a union type with an alternative named:
-
-↳ $txt0
-
-... annotated with the following expression which is not a type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one
- alternative:
-
- ┌─────────────────┐
- │ < Example : 1 > │
- └─────────────────┘
- ⇧
- This could be ❰=❱ instead
diff --git a/src/errors/InvalidAlterantiveType.txt b/src/errors/InvalidAlterantiveType.txt
deleted file mode 100644
index f5dadef..0000000
--- a/src/errors/InvalidAlterantiveType.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-Explanation: Every union literal begins by selecting one alternative and
-specifying the value for that alternative, like this:
-
-
- Select the ❰Left❱ alternative, whose value is ❰True❱
- ⇩
- ┌──────────────────────────────────┐
- │ < Left = True, Right : Natural > │ A union literal with two alternatives
- └──────────────────────────────────┘
-
-
-However, this value must be a term and not a type. For example, the following
-values are $_NOT valid:
-
-
- ┌──────────────────────────────────┐
- │ < Left = Text, Right : Natural > │ Invalid union literal
- └──────────────────────────────────┘
- ⇧
- This is a type and not a term
-
-
- ┌───────────────────────────────┐
- │ < Left = Type, Right : Type > │ Invalid union type
- └───────────────────────────────┘
- ⇧
- This is a kind and not a term
-
-
-You provided a union literal with an alternative named:
-
-↳ $txt0
-
-... whose value is:
-
-↳ $txt1
-
-... which is not a term
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one
- alternative:
-
- ┌────────────────────┐
- │ < Example = Text > │
- └────────────────────┘
- ⇧
- This could be ❰:❱ instead
diff --git a/src/errors/InvalidField.txt b/src/errors/InvalidField.txt
deleted file mode 100644
index bfbf106..0000000
--- a/src/errors/InvalidField.txt
+++ /dev/null
@@ -1,35 +0,0 @@
-Explanation: Every record literal is a set of fields assigned to values, like
-this:
-
- ┌────────────────────────────────────────┐
- │ { foo = 100, bar = True, baz = "ABC" } │
- └────────────────────────────────────────┘
-
-However, fields can only be terms and cannot be types or kinds
-
-For example, these record literals are $_NOT valid:
-
-
- ┌───────────────────────────┐
- │ { foo = 100, bar = Text } │
- └───────────────────────────┘
- ⇧
- ❰Text❱ is a type and not a term
-
-
- ┌───────────────────────────┐
- │ { foo = 100, bar = Type } │
- └───────────────────────────┘
- ⇧
- ❰Type❱ is a kind and not a term
-
-
-You provided a record literal with a key named:
-
-↳ $txt0
-
-... whose value is:
-
-↳ $txt1
-
-... which is not a term
diff --git a/src/errors/InvalidFieldType.txt b/src/errors/InvalidFieldType.txt
deleted file mode 100644
index 4f76a64..0000000
--- a/src/errors/InvalidFieldType.txt
+++ /dev/null
@@ -1,34 +0,0 @@
-Explanation: Every record type documents the type of each field, like this:
-
- ┌──────────────────────────────────────────────┐
- │ { foo : Integer, bar : Integer, baz : Text } │
- └──────────────────────────────────────────────┘
-
-However, fields cannot be annotated with expressions other than types
-
-For example, these record types are $_NOT valid:
-
-
- ┌────────────────────────────┐
- │ { foo : Integer, bar : 1 } │
- └────────────────────────────┘
- ⇧
- ❰1❱ is an ❰Integer❱ and not a ❰Type❱
-
-
- ┌───────────────────────────────┐
- │ { foo : Integer, bar : Type } │
- └───────────────────────────────┘
- ⇧
- ❰Type❱ is a ❰Kind❱ and not a ❰Type❱
-
-
-You provided a record type with a key named:
-
-↳ $txt0
-
-... annotated with the following expression:
-
-↳ $txt1
-
-... which is not a type
diff --git a/src/errors/InvalidInputType.txt b/src/errors/InvalidInputType.txt
deleted file mode 100644
index eabafa4..0000000
--- a/src/errors/InvalidInputType.txt
+++ /dev/null
@@ -1,61 +0,0 @@
-Explanation: A function can accept an input "term" that has a given "type", like
-this:
-
-
- This is the input term that the function accepts
- ⇩
- ┌───────────────────────┐
- │ ∀(x : Natural) → Bool │ This is the type of a function that accepts an
- └───────────────────────┘ input term named ❰x❱ that has type ❰Natural❱
- ⇧
- This is the type of the input term
-
-
- ┌────────────────┐
- │ Bool → Integer │ This is the type of a function that accepts an anonymous
- └────────────────┘ input term that has type ❰Bool❱
- ⇧
- This is the type of the input term
-
-
-... or a function can accept an input "type" that has a given "kind", like this:
-
-
- This is the input type that the function accepts
- ⇩
- ┌────────────────────┐
- │ ∀(a : Type) → Type │ This is the type of a function that accepts an input
- └────────────────────┘ type named ❰a❱ that has kind ❰Type❱
- ⇧
- This is the kind of the input type
-
-
- ┌──────────────────────┐
- │ (Type → Type) → Type │ This is the type of a function that accepts an
- └──────────────────────┘ anonymous input type that has kind ❰Type → Type❱
- ⇧
- This is the kind of the input type
-
-
-Other function inputs are $_NOT valid, like this:
-
-
- ┌──────────────┐
- │ ∀(x : 1) → x │ ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱
- └──────────────┘ cannot have "type" ❰1❱ or "kind" ❰1❱
- ⇧
- This is not a type or kind
-
-
- ┌──────────┐
- │ True → x │ ❰True❱ is a "term" and not a "type" nor a "kind" so the
- └──────────┘ anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱
- ⇧
- This is not a type or kind
-
-
-You annotated a function input with the following expression:
-
-↳ $txt
-
-... which is neither a type nor a kind
diff --git a/src/errors/InvalidListElement.txt b/src/errors/InvalidListElement.txt
deleted file mode 100644
index 59db7b7..0000000
--- a/src/errors/InvalidListElement.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Explanation: Every element in the list must have a type matching the type
-annotation at the end of the list
-
-For example, this is a valid ❰List❱:
-
-
- ┌──────────────────────────┐
- │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱
- └──────────────────────────┘
-
-
-.. but this is $_NOT a valid ❰List❱:
-
-
- ┌──────────────────────────────┐
- │ [1, "ABC", 3] : List Integer │ The second element is not an ❰Integer❱
- └──────────────────────────────┘
-
-
-Your ❰List❱ elements should have this type:
-
-↳ $txt0
-
-... but the following element at index $txt1:
-
-↳ $txt2
-
-... has this type instead:
-
-↳ $txt3
diff --git a/src/errors/InvalidListType.txt b/src/errors/InvalidListType.txt
deleted file mode 100644
index 676647e..0000000
--- a/src/errors/InvalidListType.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: Every ❰List❱ documents the type of its elements with a type
-annotation, like this:
-
-
- ┌──────────────────────────┐
- │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s
- └──────────────────────────┘
- ⇧
- The type of the ❰List❱'s elements, which are ❰Integer❱s
-
-
- ┌───────────────────┐
- │ [] : List Integer │ An empty ❰List❱
- └───────────────────┘
- ⇧
- You still specify the type even when the ❰List❱ is empty
-
-
-The element type must be a type and not something else. For example, the
-following element types are $_NOT valid:
-
-
- ┌──────────────┐
- │ ... : List 1 │
- └──────────────┘
- ⇧
- This is an ❰Integer❱ and not a ❰Type❱
-
-
- ┌─────────────────┐
- │ ... : List Type │
- └─────────────────┘
- ⇧
- This is a ❰Kind❱ and not a ❰Type❱
-
-
-Even if the ❰List❱ is empty you still must specify a valid type
-
-You declared that the ❰List❱'s elements should have type:
-
-↳ $txt0
-
-... which is not a ❰Type❱
diff --git a/src/errors/InvalidOptionType.txt b/src/errors/InvalidOptionType.txt
deleted file mode 100644
index 3bc81de..0000000
--- a/src/errors/InvalidOptionType.txt
+++ /dev/null
@@ -1,44 +0,0 @@
-Explanation: Every optional element ends with a type annotation for the element
-that might be present, like this:
-
-
- ┌────────────────────────┐
- │ [1] : Optional Integer │ An optional element that's present
- └────────────────────────┘
- ⇧
- The type of the ❰Optional❱ element, which is an ❰Integer❱
-
-
- ┌────────────────────────┐
- │ [] : Optional Integer │ An optional element that's absent
- └────────────────────────┘
- ⇧
- You still specify the type even when the element is absent
-
-
-The element type must be a type and not something else. For example, the
-following element types are $_NOT valid:
-
-
- ┌──────────────────┐
- │ ... : Optional 1 │
- └──────────────────┘
- ⇧
- This is an ❰Integer❱ and not a ❰Type❱
-
-
- ┌─────────────────────┐
- │ ... : Optional Type │
- └─────────────────────┘
- ⇧
- This is a ❰Kind❱ and not a ❰Type❱
-
-
-Even if the element is absent you still must specify a valid type
-
-You declared that the ❰Optional❱ element should have type:
-
-↳ $txt0
-
-... which is not a ❰Type❱
-
diff --git a/src/errors/InvalidOptionalElement.txt b/src/errors/InvalidOptionalElement.txt
deleted file mode 100644
index 0254220..0000000
--- a/src/errors/InvalidOptionalElement.txt
+++ /dev/null
@@ -1,29 +0,0 @@
-Explanation: An ❰Optional❱ element must have a type matching the type annotation
-
-For example, this is a valid ❰Optional❱ value:
-
-
- ┌────────────────────────┐
- │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type
- └────────────────────────┘
-
-
-... but this is $_NOT a valid ❰Optional❱ value:
-
-
- ┌────────────────────────────┐
- │ ["ABC"] : Optional Integer │ ❰"ABC"❱ is not an ❰Integer❱
- └────────────────────────────┘
-
-
-Your ❰Optional❱ element should have this type:
-
-↳ $txt0
-
-... but the element you provided:
-
-↳ $txt1
-
-... has this type instead:
-
-↳ $txt2
diff --git a/src/errors/InvalidOptionalLiteral.txt b/src/errors/InvalidOptionalLiteral.txt
deleted file mode 100644
index 41c0fdc..0000000
--- a/src/errors/InvalidOptionalLiteral.txt
+++ /dev/null
@@ -1,53 +0,0 @@
-Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s:
-
-
- ┌───────────────────────┐
- │ [] : Optional Integer │ An ❰Optional❱ value which is absent
- └───────────────────────┘
-
-
- ┌───────────────────────┐
- │ [] : List Integer │ An empty (0-element) ❰List❱
- └───────────────────────┘
-
-
- ┌────────────────────────┐
- │ [1] : Optional Integer │ An ❰Optional❱ value which is present
- └────────────────────────┘
-
-
- ┌────────────────────────┐
- │ [1] : List Integer │ A singleton (1-element) ❰List❱
- └────────────────────────┘
-
-
-However, an ❰Optional❱ value can $_NOT have more than one element, whereas a
-❰List❱ can have multiple elements:
-
-
- ┌───────────────────────────┐
- │ [1, 2] : Optional Integer │ Invalid: multiple elements $_NOT allowed
- └───────────────────────────┘
-
-
- ┌───────────────────────────┐
- │ [1, 2] : List Integer │ Valid: multiple elements allowed
- └───────────────────────────┘
-
-
-Your ❰Optional❱ value had this many elements:
-
-↳ $txt0
-
-... when an ❰Optional❱ value can only have at most one element
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this:
-
-
- ┌────────────────────────────────────────────────────┐
- │ List/length Integer ([1, 2, 3] : Optional Integer) │
- └────────────────────────────────────────────────────┘
- ⇧
- This should be ❰List❱ instead
diff --git a/src/errors/InvalidOutputType.txt b/src/errors/InvalidOutputType.txt
deleted file mode 100644
index dd2695d..0000000
--- a/src/errors/InvalidOutputType.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-Explanation: A function can return an output "term" that has a given "type",
-like this:
-
-
- ┌────────────────────┐
- │ ∀(x : Text) → Bool │ This is the type of a function that returns an
- └────────────────────┘ output term that has type ❰Bool❱
- ⇧
- This is the type of the output term
-
-
- ┌────────────────┐
- │ Bool → Integer │ This is the type of a function that returns an output
- └────────────────┘ term that has type ❰Int❱
- ⇧
- This is the type of the output term
-
-
-... or a function can return an output "type" that has a given "kind", like
-this:
-
- ┌────────────────────┐
- │ ∀(a : Type) → Type │ This is the type of a function that returns an
- └────────────────────┘ output type that has kind ❰Type❱
- ⇧
- This is the kind of the output type
-
-
- ┌──────────────────────┐
- │ (Type → Type) → Type │ This is the type of a function that returns an
- └──────────────────────┘ output type that has kind ❰Type❱
- ⇧
- This is the kind of the output type
-
-
-Other outputs are $_NOT valid, like this:
-
-
- ┌─────────────────┐
- │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the
- └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱
- ⇧
- This is not a type or kind
-
-
- ┌─────────────┐
- │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the
- └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱
- ⇧
- This is not a type or kind
-
-
-You specified that your function outputs a:
-
-↳ $txt
-
-... which is neither a type nor a kind:
-
-Some common reasons why you might get this error:
-
-● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
-
-
- ┌────────────────┐
- │ ∀(x: Bool) → x │
- └────────────────┘
- ⇧
- Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/src/errors/InvalidPredicate.txt b/src/errors/InvalidPredicate.txt
deleted file mode 100644
index 4c15881..0000000
--- a/src/errors/InvalidPredicate.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: Every ❰if❱ expression begins with a predicate which must have type
-❰Bool❱
-
-For example, these are valid ❰if❱ expressions:
-
-
- ┌──────────────────────────────┐
- │ if True then "Yes" else "No" │
- └──────────────────────────────┘
- ⇧
- Predicate
-
-
- ┌─────────────────────────────────────────┐
- │ λ(x : Bool) → if x then False else True │
- └─────────────────────────────────────────┘
- ⇧
- Predicate
-
-
-... but these are $_NOT valid ❰if❱ expressions:
-
-
- ┌───────────────────────────┐
- │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱
- └───────────────────────────┘
-
-
- ┌────────────────────────────┐
- │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱
- └────────────────────────────┘
-
-
-Your ❰if❱ expression begins with the following predicate:
-
-↳ $txt0
-
-... that has type:
-
-↳ $txt1
-
-... but the predicate must instead have type ❰Bool❱
-
-Some common reasons why you might get this error:
-
-● You might be used to other programming languages that accept predicates other
- than ❰Bool❱
-
- For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
- them as equivalent to ❰False❱. However, the Dhall language does not permit
- this
diff --git a/src/errors/MissingField.txt b/src/errors/MissingField.txt
deleted file mode 100644
index de14a33..0000000
--- a/src/errors/MissingField.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Explanation: You can only access fields on records, like this:
-
-
- ┌─────────────────────────────────┐
- │ { foo = True, bar = "ABC" }.foo │ This is valid ...
- └─────────────────────────────────┘
-
-
- ┌───────────────────────────────────────────┐
- │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this
- └───────────────────────────────────────────┘
-
-
-... but you can only access fields if they are present
-
-For example, the following expression is $_NOT valid:
-
- ┌─────────────────────────────────┐
- │ { foo = True, bar = "ABC" }.qux │
- └─────────────────────────────────┘
- ⇧
- Invalid: the record has no ❰qux❱ field
-
-You tried to access a field named:
-
-↳ $txt0
-
-... but the field is missing because the record only defines the following fields:
-
-↳ $txt1
diff --git a/src/errors/MissingHandler.txt b/src/errors/MissingHandler.txt
deleted file mode 100644
index 433445e..0000000
--- a/src/errors/MissingHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... but you must provide exactly one handler per alternative in the union. You
-cannot omit any handlers
-
-For example, the following expression is $_NOT valid:
-
-
- Invalid: Missing ❰Right❱ handler
- ⇩
- ┌─────────────────────────────────────────────────┐
- │ let handlers = { Left = Natural/even } │
- │ in let union = < Left = +2 | Right : Bool > │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────┘
-
-
-Note that you need to provide handlers for other alternatives even if those
-alternatives are never used
-
-You need to supply the following handlers:
-
-↳ $txt0
diff --git a/src/errors/MustCombineARecord.txt b/src/errors/MustCombineARecord.txt
deleted file mode 100644
index 141b969..0000000
--- a/src/errors/MustCombineARecord.txt
+++ /dev/null
@@ -1,46 +0,0 @@
-Explanation: You can combine records using the ❰∧❱ operator, like this:
-
-
- ┌───────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
- └───────────────────────────────────────────┘
-
-
- ┌─────────────────────────────────────────────┐
- │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │
- └─────────────────────────────────────────────┘
-
-
-... but you cannot combine values that are not records.
-
-For example, the following expressions are $_NOT valid:
-
-
- ┌──────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ 1 │
- └──────────────────────────────┘
- ⇧
- Invalid: Not a record
-
-
- ┌───────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │
- └───────────────────────────────────────────┘
- ⇧
- Invalid: This is a record type and not a record
-
-
- ┌───────────────────────────────────────────┐
- │ { foo = 1, bar = "ABC" } ∧ < baz = True > │
- └───────────────────────────────────────────┘
- ⇧
- Invalid: This is a union and not a record
-
-
-You tried to combine the following value:
-
-↳ $txt0
-
-... which is not a record, but is actually a:
-
-↳ $txt1
diff --git a/src/errors/MustMergeARecord.txt b/src/errors/MustMergeARecord.txt
deleted file mode 100644
index 79094bd..0000000
--- a/src/errors/MustMergeARecord.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... but the first argument to ❰merge❱ must be a record and not some other type.
-
-For example, the following expression is $_NOT valid:
-
-
- ┌─────────────────────────────────────────┐
- │ let handler = λ(x : Bool) → x │
- │ in merge handler < Foo = True > : True │
- └─────────────────────────────────────────┘
- ⇧
- Invalid: ❰handler❱ isn't a record
-
-
-You provided the following handler:
-
-↳ $txt0
-
-... which is not a record, but is actually a value of type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You accidentally provide an empty record type instead of an empty record when
- you ❰merge❱ an empty union:
-
-
- ┌──────────────────────────────────────────┐
- │ λ(x : <>) → λ(a : Type) → merge {} x : a │
- └──────────────────────────────────────────┘
- ⇧
- This should be ❰{=}❱ instead
diff --git a/src/errors/MustMergeUnion.txt b/src/errors/MustMergeUnion.txt
deleted file mode 100644
index 68df70c..0000000
--- a/src/errors/MustMergeUnion.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... but the second argument to ❰merge❱ must be a union and not some other type.
-
-For example, the following expression is $_NOT valid:
-
-
- ┌──────────────────────────────────────────┐
- │ let handlers = { Foo = λ(x : Bool) → x } │
- │ in merge handlers True : True │
- └──────────────────────────────────────────┘
- ⇧
- Invalid: ❰True❱ isn't a union
-
-
-You tried to ❰merge❱ this expression:
-
-↳ $txt0
-
-... which is not a union, but is actually a value of type:
-
-↳ $txt1
diff --git a/src/errors/NoDependentLet.txt b/src/errors/NoDependentLet.txt
deleted file mode 100644
index fdc65b4..0000000
--- a/src/errors/NoDependentLet.txt
+++ /dev/null
@@ -1,76 +0,0 @@
-Explanation: The Dhall programming language does not allow ❰let❱ expressions
-from terms to types. These ❰let❱ expressions are also known as "dependent ❰let❱
-expressions" because you have a type whose value depends on the value of a term.
-
-The Dhall language forbids these dependent ❰let❱ expressions in order to
-guarantee that ❰let❱ expressions of the form:
-
-
- ┌────────────────────┐
- │ let x : t = r in e │
- └────────────────────┘
-
-
-... are always equivalent to:
-
-
- ┌──────────────────┐
- │ (λ(x : t) → e) r │
- └──────────────────┘
-
-
-This means that both expressions should normalize to the same result and if one
-of the two fails to type check then the other should fail to type check, too.
-
-For this reason, the following is $_NOT legal code:
-
-
- ┌───────────────────┐
- │ let x = 2 in Text │
- └───────────────────┘
-
-
-... because the above ❰let❱ expression is equivalent to:
-
-
- ┌─────────────────────────────┐
- │ let x : Integer = 2 in Text │
- └─────────────────────────────┘
-
-
-... which in turn must be equivalent to:
-
-
- ┌───────────────────────────┐
- │ (λ(x : Integer) → Text) 2 │
- └───────────────────────────┘
-
-
-... which in turn fails to type check because this sub-expression:
-
-
- ┌───────────────────────┐
- │ λ(x : Integer) → Text │
- └───────────────────────┘
-
-
-... has type:
-
-
- ┌───────────────────────┐
- │ ∀(x : Integer) → Text │
- └───────────────────────┘
-
-
-... which is a forbidden dependent function type (i.e. a function from a term to
-a type). Therefore the equivalent ❰let❱ expression is also forbidden.
-
-Your ❰let❱ expression is invalid because the input has type:
-
-↳ $txt0
-
-... and the output has kind:
-
-↳ $txt1
-
-... which makes this a forbidden dependent ❰let❱ expression
diff --git a/src/errors/NoDependentTypes.txt b/src/errors/NoDependentTypes.txt
deleted file mode 100644
index 435bdcb..0000000
--- a/src/errors/NoDependentTypes.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-Explanation: The Dhall programming language does not allow functions from terms
-to types. These function types are also known as "dependent function types"
-because you have a type whose value "depends" on the value of a term.
-
-For example, this is $_NOT a legal function type:
-
-
- ┌─────────────┐
- │ Bool → Type │
- └─────────────┘
-
-
-Similarly, this is $_NOT legal code:
-
-
- ┌────────────────────────────────────────────────────┐
- │ λ(Vector : Natural → Type → Type) → Vector +0 Text │
- └────────────────────────────────────────────────────┘
- ⇧
- Invalid dependent type
-
-
-Your function type is invalid because the input has type:
-
-↳ $txt0
-
-... and the output has kind:
-
-↳ $txt1
-
-... which makes this a forbidden dependent function type
diff --git a/src/errors/NotAFunction.txt b/src/errors/NotAFunction.txt
deleted file mode 100644
index dd2695d..0000000
--- a/src/errors/NotAFunction.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-Explanation: A function can return an output "term" that has a given "type",
-like this:
-
-
- ┌────────────────────┐
- │ ∀(x : Text) → Bool │ This is the type of a function that returns an
- └────────────────────┘ output term that has type ❰Bool❱
- ⇧
- This is the type of the output term
-
-
- ┌────────────────┐
- │ Bool → Integer │ This is the type of a function that returns an output
- └────────────────┘ term that has type ❰Int❱
- ⇧
- This is the type of the output term
-
-
-... or a function can return an output "type" that has a given "kind", like
-this:
-
- ┌────────────────────┐
- │ ∀(a : Type) → Type │ This is the type of a function that returns an
- └────────────────────┘ output type that has kind ❰Type❱
- ⇧
- This is the kind of the output type
-
-
- ┌──────────────────────┐
- │ (Type → Type) → Type │ This is the type of a function that returns an
- └──────────────────────┘ output type that has kind ❰Type❱
- ⇧
- This is the kind of the output type
-
-
-Other outputs are $_NOT valid, like this:
-
-
- ┌─────────────────┐
- │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the
- └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱
- ⇧
- This is not a type or kind
-
-
- ┌─────────────┐
- │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the
- └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱
- ⇧
- This is not a type or kind
-
-
-You specified that your function outputs a:
-
-↳ $txt
-
-... which is neither a type nor a kind:
-
-Some common reasons why you might get this error:
-
-● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
-
-
- ┌────────────────┐
- │ ∀(x: Bool) → x │
- └────────────────┘
- ⇧
- Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/src/errors/NotARecord.txt b/src/errors/NotARecord.txt
deleted file mode 100644
index e0eebc8..0000000
--- a/src/errors/NotARecord.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-Explanation: You can only access fields on records, like this:
-
-
- ┌─────────────────────────────────┐
- │ { foo = True, bar = "ABC" }.foo │ This is valid ...
- └─────────────────────────────────┘
-
-
- ┌───────────────────────────────────────────┐
- │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this
- └───────────────────────────────────────────┘
-
-
-... but you cannot access fields on non-record expressions
-
-For example, the following expression is $_NOT valid:
-
-
- ┌───────┐
- │ 1.foo │
- └───────┘
- ⇧
- Invalid: Not a record
-
-
-You tried to access a field named:
-
-↳ $txt0
-
-... on the following expression which is not a record:
-
-↳ $txt1
-
-... but is actually an expression of type:
-
-↳ $txt2
-
-Some common reasons why you might get this error:
-
-● You accidentally try to access a field of a union instead of a record, like
- this:
-
-
- ┌─────────────────┐
- │ < foo : a >.foo │
- └─────────────────┘
- ⇧
- This is a union, not a record
diff --git a/src/errors/TypeMismatch.txt b/src/errors/TypeMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/src/errors/TypeMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
- ┌───────────────────────────────┐
- │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have type ❰Bool❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ Natural/even : Natural → Bool │ This built-in function only accepts
- └───────────────────────────────┘ arguments that have type ❰Natural❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have kind ❰Type❱
- ⇧
- The function's input kind
-
-
- ┌────────────────────┐
- │ List : Type → Type │ This built-in function only accepts arguments that
- └────────────────────┘ have kind ❰Type❱
- ⇧
- The function's input kind
-
-
-For example, the following expressions are valid:
-
-
- ┌────────────────────────┐
- │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌─────────────────┐
- │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
- └─────────────────┘ argument that the ❰Natural/even❱ function accepts,
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌───────────┐
- │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
- └───────────┘ that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
- ┌───────────────────────┐
- │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function
- └───────────────────────┘ expects an argument that has type ❰Bool❱
-
-
- ┌──────────────────┐
- │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
- └──────────────────┘ expects an argument that has type ❰Natural❱
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
- └────────────────────────┘ function expects an argument of kind ❰Type❱
-
-
- ┌────────┐
- │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
- └────────┘ argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
- ┌────────────────────────────────────────┐
- │ List/head ([1, 2, 3] : List Integer) │
- └────────────────────────────────────────┘
- ⇧
- ❰List/head❱ is missing the first argument,
- which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
- ┌────────────────┐
- │ Natural/even 2 │
- └────────────────┘
- ⇧
- This should be ❰+2❱
diff --git a/src/errors/UnboundVariable.txt b/src/errors/UnboundVariable.txt
deleted file mode 100644
index bd7d483..0000000
--- a/src/errors/UnboundVariable.txt
+++ /dev/null
@@ -1,97 +0,0 @@
-Explanation: Expressions can only reference previously introduced (i.e. "bound")
-variables that are still "in scope"
-
-For example, the following valid expressions introduce a "bound" variable named
-❰x❱:
-
-
- ┌─────────────────┐
- │ λ(x : Bool) → x │ Anonymous functions introduce "bound" variables
- └─────────────────┘
- ⇧
- This is the bound variable
-
-
- ┌─────────────────┐
- │ let x = 1 in x │ ❰let❱ expressions introduce "bound" variables
- └─────────────────┘
- ⇧
- This is the bound variable
-
-
-However, the following expressions are not valid because they all reference a
-variable that has not been introduced yet (i.e. an "unbound" variable):
-
-
- ┌─────────────────┐
- │ λ(x : Bool) → y │ The variable ❰y❱ hasn't been introduced yet
- └─────────────────┘
- ⇧
- This is the unbound variable
-
-
- ┌──────────────────────────┐
- │ (let x = True in x) && x │ ❰x❱ is undefined outside the parentheses
- └──────────────────────────┘
- ⇧
- This is the unbound variable
-
-
- ┌────────────────┐
- │ let x = x in x │ The definition for ❰x❱ cannot reference itself
- └────────────────┘
- ⇧
- This is the unbound variable
-
-
-Some common reasons why you might get this error:
-
-● You misspell a variable name, like this:
-
-
- ┌────────────────────────────────────────────────────┐
- │ λ(empty : Bool) → if emty then "Empty" else "Full" │
- └────────────────────────────────────────────────────┘
- ⇧
- Typo
-
-
-● You misspell a reserved identifier, like this:
-
-
- ┌──────────────────────────┐
- │ foral (a : Type) → a → a │
- └──────────────────────────┘
- ⇧
- Typo
-
-
-● You tried to define a recursive value, like this:
-
-
- ┌─────────────────────┐
- │ let x = x + +1 in x │
- └─────────────────────┘
- ⇧
- Recursive definitions are not allowed
-
-
-● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱
-
-
- Unbound variable
- ⇩
- ┌─────────────────┐
- │ (x : Bool) → x │
- └─────────────────┘
- ⇧
- A ❰λ❱ here would transform this into a valid anonymous function
-
-
- Unbound variable
- ⇩
- ┌────────────────────┐
- │ (x : Bool) → Bool │
- └────────────────────┘
- ⇧
- A ❰∀❱ or ❰forall❱ here would transform this into a valid function type
diff --git a/src/errors/Untyped.txt b/src/errors/Untyped.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/src/errors/Untyped.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
- ┌───────────────────────────────┐
- │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have type ❰Bool❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ Natural/even : Natural → Bool │ This built-in function only accepts
- └───────────────────────────────┘ arguments that have type ❰Natural❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have kind ❰Type❱
- ⇧
- The function's input kind
-
-
- ┌────────────────────┐
- │ List : Type → Type │ This built-in function only accepts arguments that
- └────────────────────┘ have kind ❰Type❱
- ⇧
- The function's input kind
-
-
-For example, the following expressions are valid:
-
-
- ┌────────────────────────┐
- │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌─────────────────┐
- │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
- └─────────────────┘ argument that the ❰Natural/even❱ function accepts,
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌───────────┐
- │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
- └───────────┘ that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
- ┌───────────────────────┐
- │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function
- └───────────────────────┘ expects an argument that has type ❰Bool❱
-
-
- ┌──────────────────┐
- │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
- └──────────────────┘ expects an argument that has type ❰Natural❱
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
- └────────────────────────┘ function expects an argument of kind ❰Type❱
-
-
- ┌────────┐
- │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
- └────────┘ argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
- ┌────────────────────────────────────────┐
- │ List/head ([1, 2, 3] : List Integer) │
- └────────────────────────────────────────┘
- ⇧
- ❰List/head❱ is missing the first argument,
- which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
- ┌────────────────┐
- │ Natural/even 2 │
- └────────────────┘
- ⇧
- This should be ❰+2❱
diff --git a/src/errors/UnusedHandler.txt b/src/errors/UnusedHandler.txt
deleted file mode 100644
index 2e46a12..0000000
--- a/src/errors/UnusedHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
- ┌─────────────────────────────────────────────────────────────────────┐
- │ let union = < Left = +2 | Right : Bool > │
- │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
- │ in merge handlers union : Bool │
- └─────────────────────────────────────────────────────────────────────┘
-
-
-... but you must provide exactly one handler per alternative in the union. You
-cannot supply extra handlers
-
-For example, the following expression is $_NOT valid:
-
-
- ┌───────────────────────────────────────┐
- │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing
- │ in let handlers = │
- │ { Left = Natural/even │
- │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used
- │ } │
- │ in merge handlers union : Bool │
- └───────────────────────────────────────┘
-
-
-You provided the following handlers:
-
-↳ $txt0
-
-... which had no matching alternatives in the union you tried to ❰merge❱
diff --git a/src/generated_parser.rs b/src/generated_parser.rs
deleted file mode 100644
index 452b4cd..0000000
--- a/src/generated_parser.rs
+++ /dev/null
@@ -1,6 +0,0 @@
-#[allow(unused_imports)]
-use pest_derive::*;
-
-#[derive(Parser)]
-#[grammar = "dhall.pest"]
-pub struct DhallParser;
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
deleted file mode 100644
index 150961f..0000000
--- a/src/grammar.lalrpop
+++ /dev/null
@@ -1,162 +0,0 @@
-use std::collections::BTreeMap;
-use std::iter;
-use std::iter::FromIterator;
-
-use crate::core;
-use crate::core::bx;
-use crate::core::Expr::*;
-use crate::core::BuiltinType::*;
-use crate::grammar_util::*;
-use crate::lexer::*;
-
-grammar<'input>;
-
-extern {
- type Location = usize;
- type Error = LexicalError;
-
- enum Tok<'input> {
- Pi => Tok::Pi,
- Lambda => Tok::Lambda,
- Combine => Tok::Combine,
- "->" => Tok::Arrow,
-
- Int => Tok::Integer(<isize>),
- Nat => Tok::Natural(<usize>),
- Text => Tok::Text(<String>),
- Bool => Tok::Bool(<bool>),
- Label => Tok::Identifier(<&'input str>),
- Const => Tok::Const(<core::Const>),
- Let => Tok::Keyword(Keyword::Let),
- In => Tok::Keyword(Keyword::In),
- If => Tok::Keyword(Keyword::If),
- Then => Tok::Keyword(Keyword::Then),
- Else => Tok::Keyword(Keyword::Else),
- List => Tok::ListLike(ListLike::List),
- Optional => Tok::ListLike(ListLike::Optional),
- Builtin => Tok::Builtin(<Builtin>),
-
- "{" => Tok::BraceL,
- "}" => Tok::BraceR,
- "[" => Tok::BracketL,
- "]" => Tok::BracketR,
- "(" => Tok::ParenL,
- ")" => Tok::ParenR,
- "&&" => Tok::BoolAnd,
- "||" => Tok::BoolOr,
- "==" => Tok::CompareEQ,
- "!=" => Tok::CompareNE,
- "++" => Tok::Append,
- "*" => Tok::Times,
- "+" => Tok::Plus,
- "," => Tok::Comma,
- "." => Tok::Dot,
- ":" => Tok::Ascription,
- "=" => Tok::Equals,
- }
-}
-
-pub Expr: BoxExpr<'input> = { // exprA
- <ExprB> ":" <Expr> => bx(Annot(<>)),
- ExprB,
-};
-
-ExprB: BoxExpr<'input> = {
- Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
- Pi "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Pi(<>)),
- If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
- <ExprC> "->" <ExprB> => bx(Pi("_", <>)),
- Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
- "[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(c, a)),
- ExprC,
-};
-
-ListLike: ExprListFn<'input> = {
- List => ListLit,
- Optional => OptionalLit,
-};
-
-BoolOr: ExprOpFn<'input> = { "||" => BoolOr };
-NaturalPlus: ExprOpFn<'input> = { "+" => NaturalPlus };
-TextAppend: ExprOpFn<'input> = { "++" => TextAppend };
-BoolAnd: ExprOpFn<'input> = { "&&" => BoolAnd };
-CombineOp: ExprOpFn<'input> = { Combine => Combine };
-NaturalTimes: ExprOpFn<'input> = { "*" => NaturalTimes };
-BoolEQ: ExprOpFn<'input> = { "==" => BoolEQ };
-BoolNE: ExprOpFn<'input> = { "!=" => BoolNE };
-
-Tier<NextTier, Op>: BoxExpr<'input> = {
- <a:NextTier> <f:Op> <b:Tier<NextTier, Op>> => bx(f(a, b)),
- // <b:Tier<NextTier, Op>> <f:Op> <a:NextTier> => bx(f(a, b)),
- NextTier,
-};
-
-ExprC = Tier<ExprC1, BoolOr>;
-ExprC1 = Tier<ExprC2, NaturalPlus>;
-ExprC2 = Tier<ExprC3, TextAppend>;
-ExprC3 = Tier<ExprC4, BoolAnd>;
-ExprC4 = Tier<ExprC5, CombineOp>;
-ExprC5 = Tier<ExprC6, NaturalTimes>;
-ExprC6 = Tier<ExprC7, BoolEQ>;
-ExprC7 = Tier<ExprD, BoolNE>;
-
-ExprD: BoxExpr<'input> = {
- <v:(ExprE)+> => {
- let mut it = v.into_iter();
- let f = it.next().unwrap();
- it.fold(f, |f, x| bx(App(f, x)))
- }
-};
-
-ExprE: BoxExpr<'input> = {
- <a:ExprF> <fields:("." <Label>)*> => {
- fields.into_iter().fold(a, |x, f| bx(Field(x, f)))
- },
-};
-
-ExprF: BoxExpr<'input> = {
- Nat => bx(NaturalLit(<>)),
- Int => bx(IntegerLit(<>)),
- Text => bx(TextLit(<>)),
- Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
- Const => bx(Const(<>)),
- List => bx(BuiltinType(List)),
- Optional => bx(BuiltinType(Optional)),
- Builtin => bx(builtin_expr(<>)),
- Bool => bx(BoolLit(<>)),
- Record,
- RecordLit,
- "(" <Expr> ")",
-};
-
-SepBy<S, T>: iter::Chain<::std::vec::IntoIter<T>, ::std::option::IntoIter<T>> = {
- <v:(<T> S)*> <last:T?> => v.into_iter().chain(last.into_iter()),
-};
-
-SepBy1<S, T>: iter::Chain<::std::vec::IntoIter<T>, iter::Once<T>> = {
- <v:(<T> S)*> <last:T> => v.into_iter().chain(iter::once(last)),
-};
-
-Elems: Vec<ParsedExpr<'input>> = {
- <v:SepBy<",", Expr>> => {
- v.into_iter()
- .map(|b| *b)
- .collect::<Vec<_>>()
- }
-};
-
-RecordLit: BoxExpr<'input> = {
- "{" "=" "}" => bx(RecordLit(BTreeMap::new())),
- "{" <FieldValues> "}" => bx(RecordLit(BTreeMap::from_iter(<>))),
-};
-
-Record: BoxExpr<'input> = {
- "{" <FieldTypes> "}" => bx(Record(BTreeMap::from_iter(<>))),
-};
-
-FieldValues = SepBy1<",", Field<"=">>;
-FieldTypes = SepBy<",", Field<":">>;
-
-Field<Sep>: (&'input str, ParsedExpr<'input>) = {
- <a:Label> Sep <b:Expr> => (a, *b),
-};
diff --git a/src/grammar_util.rs b/src/grammar_util.rs
deleted file mode 100644
index c546a13..0000000
--- a/src/grammar_util.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-use crate::core::{Expr, X};
-use crate::lexer::Builtin;
-
-pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
-pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
-pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
-pub type ExprListFn<'i> = fn(BoxExpr<'i>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
-
-pub fn builtin_expr<'i, S, A>(b: Builtin) -> Expr<'i, S, A> {
- match b {
- Builtin::Type(t) => Expr::BuiltinType(t),
- Builtin::Value(v) => Expr::BuiltinValue(v),
- }
-}
diff --git a/src/lexer.rs b/src/lexer.rs
deleted file mode 100644
index 5b4dcaa..0000000
--- a/src/lexer.rs
+++ /dev/null
@@ -1,378 +0,0 @@
-use nom::*;
-
-use crate::core::Const;
-use crate::core::BuiltinType;
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue;
-use crate::core::BuiltinValue::*;
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Keyword {
- Let,
- In,
- If,
- Then,
- Else,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ListLike {
- List,
- Optional,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Builtin {
- Type(BuiltinType),
- Value(BuiltinValue),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Tok<'i> {
- Identifier(&'i str),
- Keyword(Keyword),
- Builtin(Builtin),
- ListLike(ListLike),
- Const(Const),
- Bool(bool),
- Integer(isize),
- Natural(usize),
- Text(String),
-
- // Symbols
- BraceL,
- BraceR,
- BracketL,
- BracketR,
- ParenL,
- ParenR,
- Arrow,
- Lambda,
- Pi,
- Combine,
- BoolAnd,
- BoolOr,
- CompareEQ,
- CompareNE,
- Append,
- Times,
- Plus,
- Comma,
- Dot,
- Ascription,
- Equals,
-}
-
-#[derive(Debug)]
-pub enum LexicalError {
- Error(usize, nom::simple_errors::Err<u32>),
- Incomplete(nom::Needed),
-}
-
-pub type Spanned<Tok, Loc, Error> = Result<(Loc, Tok, Loc), Error>;
-
-#[allow(dead_code)]
-fn is_identifier_first_char(c: char) -> bool {
- c.is_alphabetic() || c == '_'
-}
-
-fn is_identifier_rest_char(c: char) -> bool {
- is_identifier_first_char(c) || c.is_digit(10) || c == '/'
-}
-
-macro_rules! digits {
- ($i:expr, $t:tt, $radix:expr) => {{
- let r: nom::IResult<&str, $t> =
- map_res!($i, take_while1_s!(call!(|c: char| c.is_digit($radix))),
- |s| $t::from_str_radix(s, $radix));
- r
- }}
-}
-
-named!(natural<&str, usize>, digits!(usize, 10));
-named!(integral<&str, isize>, digits!(isize, 10));
-named!(integer<&str, isize>, alt!(
- preceded!(tag!("-"), map!(integral, |i: isize| -i)) |
- preceded!(tag!("+"), integral)
-));
-named!(boolean<&str, bool>, alt!(
- value!(true, tag!("True")) |
- value!(false, tag!("False"))
-));
-
-named!(identifier<&str, &str>, recognize!(preceded!(
- take_while1_s!(is_identifier_first_char),
- take_while_s!(is_identifier_rest_char))
-));
-
-/// Parse an identifier, ensuring a whole identifier is parsed and not just a prefix.
-macro_rules! ident_tag {
- ($i:expr, $tag:expr) => {
- match identifier($i) {
- nom::IResult::Done(i, s) => {
- if s == $tag {
- nom::IResult::Done(i, s)
- } else {
- nom::IResult::Error(error_position!(nom::ErrorKind::Tag, $i))
- }
- }
- r => r,
- }
- }
-}
-
-fn string_escape_single(c: char) -> Option<&'static str> {
- match c {
- 'n' => Some("\n"),
- 'r' => Some("\r"),
- 't' => Some("\t"),
- '"' => Some("\""),
- '\'' => Some("'"),
- '\\' => Some("\\"),
- '0' => Some("\0"),
- 'a' => Some("\x07"),
- 'b' => Some("\x08"),
- 'f' => Some("\x0c"),
- 'v' => Some("\x0b"),
- '&' => Some(""),
- _ => None,
- }
-}
-
-named!(string_escape_numeric<&str, char>, map_opt!(alt!(
- preceded!(tag!("x"), digits!(u32, 16)) |
- preceded!(tag!("o"), digits!(u32, 8)) |
- digits!(u32, 10)
-), ::std::char::from_u32));
-
-fn string_lit_inner(input: &str) -> nom::IResult<&str, String> {
- use nom::IResult::*;;
- use nom::ErrorKind;
- let mut s = String::new();
- let mut cs = input.char_indices().peekable();
- while let Some((i, c)) = cs.next() {
- match c {
- '"' => return nom::IResult::Done(&input[i..], s),
- '\\' => match cs.next() {
- Some((_, s)) if s.is_whitespace() => {
- while cs.peek().map(|&(_, s)| s.is_whitespace()) == Some(true) {
- let _ = cs.next();
- }
- if cs.next().map(|p| p.1) != Some('\\') {
- return Error(error_position!(ErrorKind::Custom(4 /* FIXME */), input));
- }
- }
- Some((j, ec)) => {
- if let Some(esc) = string_escape_single(ec) {
- s.push_str(esc);
- // FIXME Named ASCII escapes and control character escapes
- } else {
- match string_escape_numeric(&input[j..]) {
- Done(rest, esc) => {
- let &(k, _) = cs.peek().unwrap();
- // digits are always single byte ASCII characters
- let consumed = input[k..].len() - rest.len();
- for _ in 0..consumed { let _ = cs.next(); }
- s.push(esc);
- }
- Incomplete(s) => return Incomplete(s),
- Error(e) => return Error(e),
- }
- }
- },
- _ => return Error(error_position!(ErrorKind::Custom(5 /* FIXME */), input)),
- },
- _ => s.push(c),
- }
- }
- Error(error_position!(ErrorKind::Custom(3 /* FIXME */), input))
-}
-
-named!(string_lit<&str, String>, delimited!(tag!("\""), string_lit_inner, tag!("\"")));
-
-named!(keyword<&str, Keyword>, alt!(
- value!(Keyword::Let, ident_tag!("let")) |
- value!(Keyword::In, ident_tag!("in")) |
- value!(Keyword::If, ident_tag!("if")) |
- value!(Keyword::Then, ident_tag!("then")) |
- value!(Keyword::Else, ident_tag!("else"))
-));
-
-named!(type_const<&str, Const>, alt!(
- value!(Const::Type, ident_tag!("Type")) |
- value!(Const::Kind, ident_tag!("Kind"))
-));
-
-named!(list_like<&str, ListLike>, alt!(
- value!(ListLike::List, ident_tag!("List")) |
- value!(ListLike::Optional, ident_tag!("Optional"))
-));
-
-named!(builtin<&str, Builtin>, alt!(
- value!(Builtin::Value(NaturalFold), ident_tag!("Natural/fold")) |
- value!(Builtin::Value(NaturalBuild), ident_tag!("Natural/build")) |
- value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) |
- value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) |
- value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) |
- value!(Builtin::Value(NaturalShow), ident_tag!("Natural/show")) |
- value!(Builtin::Type(Natural), ident_tag!("Natural")) |
- value!(Builtin::Type(Integer), ident_tag!("Integer")) |
- value!(Builtin::Type(Double), ident_tag!("Double")) |
- value!(Builtin::Type(Text), ident_tag!("Text")) |
- value!(Builtin::Value(ListBuild), ident_tag!("List/build")) |
- value!(Builtin::Value(ListFold), ident_tag!("List/fold")) |
- value!(Builtin::Value(ListLength), ident_tag!("List/length")) |
- value!(Builtin::Value(ListHead), ident_tag!("List/head")) |
- value!(Builtin::Value(ListLast), ident_tag!("List/last")) |
- value!(Builtin::Value(ListIndexed), ident_tag!("List/indexed")) |
- value!(Builtin::Value(ListReverse), ident_tag!("List/reverse")) |
- value!(Builtin::Value(OptionalFold), ident_tag!("Optional/fold")) |
- value!(Builtin::Type(Bool), ident_tag!("Bool"))
-));
-
-named!(token<&str, Tok>, alt!(
- value!(Tok::Pi, ident_tag!("forall")) |
- value!(Tok::Pi, tag!("∀")) |
- value!(Tok::Lambda, tag!("\\")) |
- value!(Tok::Lambda, tag!("λ")) |
- value!(Tok::Combine, tag!("/\\")) |
- value!(Tok::Combine, tag!("∧")) |
- value!(Tok::Arrow, tag!("->")) |
- value!(Tok::Arrow, tag!("→")) |
-
- map!(type_const, Tok::Const) |
- map!(boolean, Tok::Bool) |
- map!(keyword, Tok::Keyword) |
- map!(builtin, Tok::Builtin) |
- map!(list_like, Tok::ListLike) |
- map!(natural, Tok::Natural) |
- map!(integer, Tok::Integer) |
- map!(identifier, Tok::Identifier) |
- map!(string_lit, Tok::Text) |
-
- value!(Tok::BraceL, tag!("{")) |
- value!(Tok::BraceR, tag!("}")) |
- value!(Tok::BracketL, tag!("[")) |
- value!(Tok::BracketR, tag!("]")) |
- value!(Tok::ParenL, tag!("(")) |
- value!(Tok::ParenR, tag!(")")) |
- value!(Tok::BoolAnd, tag!("&&")) |
- value!(Tok::BoolOr, tag!("||")) |
- value!(Tok::CompareEQ, tag!("==")) |
- value!(Tok::CompareNE, tag!("!=")) |
- value!(Tok::Append, tag!("++")) |
- value!(Tok::Times, tag!("*")) |
- value!(Tok::Plus, tag!("+")) |
- value!(Tok::Comma, tag!(",")) |
- value!(Tok::Dot, tag!(".")) |
- value!(Tok::Ascription, tag!(":")) |
- value!(Tok::Equals, tag!("="))
-));
-
-fn find_end(input: &str, ending: &str) -> Option<usize> {
- input.find(ending).map(|i| i + ending.len())
-}
-
-pub struct Lexer<'input> {
- input: &'input str,
- offset: usize,
-}
-
-impl<'input> Lexer<'input> {
- pub fn new(input: &'input str) -> Self {
- Lexer {
- input: input,
- offset: 0,
- }
- }
-
- fn current_input(&mut self) -> &'input str {
- &self.input[self.offset..]
- }
-
- fn skip_whitespace(&mut self) -> bool {
- let input = self.current_input();
- let trimmed = input.trim_start();
- let whitespace_len = input.len() - trimmed.len();
- let skipped = whitespace_len > 0;
- if skipped {
- // println!("skipped {} whitespace bytes in {}..{}", whitespace_len, self.offset, self.offset + whitespace_len);
- self.offset += whitespace_len;
- }
- skipped
- }
-
- fn skip_comments(&mut self) -> bool {
- let input = self.current_input();
- if !input.is_char_boundary(0) || !input.is_char_boundary(2) {
- return false;
- }
- let skip = match &input[0..2] {
- "{-" => find_end(input, "-}"),
- "--" => find_end(input, "\n"), // Also skips past \r\n (CRLF)
- _ => None,
- }.unwrap_or(0);
- // println!("skipped {} bytes of comment", skip);
- self.offset += skip;
- skip != 0
- }
-
- fn skip_comments_and_whitespace(&mut self) {
- while self.skip_whitespace() || self.skip_comments() {}
- }
-}
-
-impl<'input> Iterator for Lexer<'input> {
- type Item = Spanned<Tok<'input>, usize, LexicalError>;
-
- fn next(&mut self) -> Option<Self::Item> {
- use nom::IResult::*;
- self.skip_comments_and_whitespace();
- let input = self.current_input();
- if input.is_empty() {
- return None;
- }
- match token(input) {
- Done(rest, t) => {
- let parsed_len = input.len() - rest.len();
- //println!("parsed {} bytes => {:?}", parsed_len, t);
- let start = self.offset;
- self.offset += parsed_len;
- Some(Ok((start, t, self.offset)))
- }
- Error(e) => {
- let offset = self.offset;
- self.offset = self.input.len();
- Some(Err(LexicalError::Error(offset, e)))
- }
- Incomplete(needed) => {
- Some(Err(LexicalError::Incomplete(needed)))
- }
- }
- }
-}
-
-#[test]
-fn test_lex() {
- use self::Tok::*;
- let s = "λ(b : Bool) → b == False";
- let expected = [Lambda,
- ParenL,
- Identifier("b"),
- Ascription,
- Builtin(self::Builtin::Type(crate::core::BuiltinType::Bool)),
- ParenR,
- Arrow,
- Identifier("b"),
- CompareEQ,
- Bool(false)];
- let lexer = Lexer::new(s);
- let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
- assert_eq!(&tokens, &expected);
-
- assert_eq!(string_lit(r#""a\&b""#).to_result(), Ok("ab".to_owned()));
- assert_eq!(string_lit(r#""a\ \b""#).to_result(), Ok("ab".to_owned()));
- assert!(string_lit(r#""a\ b""#).is_err());
- assert_eq!(string_lit(r#""a\nb""#).to_result(), Ok("a\nb".to_owned()));
- assert_eq!(string_lit(r#""\o141\x62\99""#).to_result(), Ok("abc".to_owned()));
-}
diff --git a/src/lib.rs b/src/lib.rs
deleted file mode 100644
index e07071d..0000000
--- a/src/lib.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-#![feature(box_patterns)]
-
-pub mod context;
-mod core;
-pub use crate::core::*;
-use lalrpop_util::lalrpop_mod;
-lalrpop_mod!(pub grammar); // synthesized by LALRPOP
-mod grammar_util;
-mod generated_parser;
-pub mod lexer;
-pub mod parser;
-pub mod typecheck;
diff --git a/src/main.rs b/src/main.rs
deleted file mode 100644
index cdab3c0..0000000
--- a/src/main.rs
+++ /dev/null
@@ -1,101 +0,0 @@
-use std::io::{self, Read};
-use std::error::Error;
-use term_painter::ToStyle;
-
-use dhall::*;
-
-const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
-const BOLD: term_painter::Attr = term_painter::Attr::Bold;
-
-fn print_error(message: &str, source: &str, start: usize, end: usize) {
- let line_number = bytecount::count(source[..start].as_bytes(), b'\n');
- let line_start = source[..start].rfind('\n').map(|i| i + 1).unwrap_or(0);
- let line_end = source[end..].find('\n').unwrap_or(0) + end;
- let context_prefix = &source[line_start..start];
- let context_highlighted = &source[start..end];
- let context_suffix = &source[end..line_end];
-
- let line_number_str = line_number.to_string();
- let line_number_width = line_number_str.len();
-
- BOLD.with(|| {
- ERROR_STYLE.with(|| {
- print!("error: ");
- });
- println!("{}", message);
- });
- BOLD.with(|| {
- print!(" -->");
- });
- println!(" {}:{}:0", "(stdin)", line_number);
- BOLD.with(|| {
- println!("{:w$} |", "", w = line_number_width);
- print!("{} |", line_number_str);
- });
- print!(" {}", context_prefix);
- BOLD.with(|| {
- ERROR_STYLE.with(|| {
- print!("{}", context_highlighted);
- });
- });
- println!("{}", context_suffix);
- BOLD.with(|| {
- print!("{:w$} |", "", w = line_number_width);
- ERROR_STYLE.with(|| {
- println!(" {:so$}{:^>ew$}", "", "",
- so = source[line_start..start].chars().count(),
- ew = ::std::cmp::max(1, source[start..end].chars().count()));
- });
- });
-}
-
-fn main() {
- let mut buffer = String::new();
- io::stdin().read_to_string(&mut buffer).unwrap();
- let expr = match parser::parse_expr(&buffer) {
- Ok(e) => e,
- Err(lalrpop_util::ParseError::User { error: lexer::LexicalError::Error(pos, e) }) => {
- print_error(&format!("Unexpected token {:?}", e), &buffer, pos, pos);
- return;
- }
- Err(lalrpop_util::ParseError::UnrecognizedToken { token: Some((start, t, end)), expected: e }) => {
- print_error(&format!("Unrecognized token {:?}", t), &buffer, start, end);
- if !e.is_empty() {
- println!("Expected {:?}", e);
- }
- return;
- }
- Err(e) => {
- print_error(&format!("Parser error {:?}", e), &buffer, 0, 0);
- return;
- }
- };
-
- /*
- expr' <- load expr
- */
-
- let type_expr = match typecheck::type_of(&expr) {
- Err(e) => {
- let explain = ::std::env::args().any(|s| s == "--explain");
- if !explain {
- term_painter::Color::BrightBlack.with(|| {
- println!("Use \"dhall --explain\" for detailed errors");
- });
- }
- ERROR_STYLE.with(|| print!("Error: "));
- println!("{}", e.type_message.description());
- if explain {
- println!("{}", e.type_message);
- }
- println!("{}", e.current);
- // FIXME Print source position
- return;
- }
- Ok(type_expr) => type_expr,
- };
-
- println!("{}", type_expr);
- println!("");
- println!("{}", normalize::<_, X, _>(&expr));
-}
diff --git a/src/parser.rs b/src/parser.rs
deleted file mode 100644
index 057fce2..0000000
--- a/src/parser.rs
+++ /dev/null
@@ -1,91 +0,0 @@
-use lalrpop_util;
-
-use crate::grammar;
-use crate::grammar_util::BoxExpr;
-use crate::lexer::{Lexer, LexicalError, Tok};
-use crate::core::{bx, Expr};
-
-pub type ParseError<'i> = lalrpop_util::ParseError<usize, Tok<'i>, LexicalError>;
-
-pub fn parse_expr(s: &str) -> Result<BoxExpr, ParseError> {
- grammar::ExprParser::new().parse(Lexer::new(s))
-}
-
-use pest::Parser;
-use pest::error::Error;
-use pest::iterators::Pair;
-use crate::generated_parser::{DhallParser, Rule};
-
-fn debug_pair(pair: Pair<Rule>) {
- fn aux(indent: usize, pair: Pair<Rule>) {
- let indent_str = "| ".repeat(indent);
- println!(r#"{}{:?}: "{}""#, indent_str, pair.as_rule(), pair.as_str());
- for p in pair.into_inner() {
- aux(indent+1, p);
- }
- }
- aux(0, pair)
-}
-
-pub fn parse_expr_pest(s: &str) -> Result<BoxExpr, Error<Rule>> {
- let parsed_expr = DhallParser::parse(Rule::complete_expression, s)?.next().unwrap();
- debug_pair(parsed_expr.clone());
- // println!("{}", parsed_expr.clone());
-
- fn parse_pair(pair: Pair<Rule>) -> BoxExpr {
- match pair.as_rule() {
- Rule::natural_literal => bx(Expr::NaturalLit(str::parse(pair.as_str().trim()).unwrap())),
- Rule::plus_expression => {
- let mut inner = pair.into_inner().map(parse_pair);
- let first_expr = inner.next().unwrap();
- inner.fold(first_expr, |acc, e| bx(Expr::NaturalPlus(acc, e)))
- }
- Rule::times_expression => {
- let mut inner = pair.into_inner().map(parse_pair);
- let first_expr = inner.next().unwrap();
- inner.fold(first_expr, |acc, e| bx(Expr::NaturalTimes(acc, e)))
- }
- r => panic!("{:?}", r),
- }
- }
-
- Ok(parse_pair(parsed_expr))
-}
-
-
-#[test]
-fn test_parse() {
- use crate::core::Expr::*;
- let expr = "((22 + 3) * 10)";
- println!("{:?}", parse_expr(expr));
- match parse_expr_pest(expr) {
- Err(e) => println!("{}", e),
- ok => println!("{:?}", ok),
- }
- assert_eq!(parse_expr_pest(expr).unwrap(), parse_expr(expr).unwrap());
- assert!(false);
-
- println!("test {:?}", parse_expr("3 + 5 * 10"));
- assert!(parse_expr("22").is_ok());
- assert!(parse_expr("(22)").is_ok());
- assert_eq!(parse_expr("3 + 5 * 10").ok(),
- Some(Box::new(NaturalPlus(Box::new(NaturalLit(3)),
- Box::new(NaturalTimes(Box::new(NaturalLit(5)),
- Box::new(NaturalLit(10))))))));
- // The original parser is apparently right-associative
- assert_eq!(parse_expr("2 * 3 * 4").ok(),
- Some(Box::new(NaturalTimes(Box::new(NaturalLit(2)),
- Box::new(NaturalTimes(Box::new(NaturalLit(3)),
- Box::new(NaturalLit(4))))))));
- assert!(parse_expr("((((22))))").is_ok());
- assert!(parse_expr("((22)").is_err());
- println!("{:?}", parse_expr("\\(b : Bool) -> b == False"));
- assert!(parse_expr("\\(b : Bool) -> b == False").is_ok());
- println!("{:?}", parse_expr("foo.bar"));
- assert!(parse_expr("foo.bar").is_ok());
- assert!(parse_expr("[] : List Bool").is_ok());
-
- // println!("{:?}", parse_expr("< Left = True | Right : Natural >"));
- // println!("{:?}", parse_expr(r#""bl${42}ah""#));
- // assert!(parse_expr("< Left = True | Right : Natural >").is_ok());
-}
diff --git a/src/typecheck.rs b/src/typecheck.rs
deleted file mode 100644
index 62ff7d2..0000000
--- a/src/typecheck.rs
+++ /dev/null
@@ -1,616 +0,0 @@
-#![allow(non_snake_case)]
-use std::collections::BTreeMap;
-use std::collections::HashSet;
-use std::fmt;
-
-use crate::context::Context;
-use crate::core;
-use crate::core::{Expr, V, X, bx, normalize, shift, subst};
-use crate::core::{pi, app};
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue::*;
-use crate::core::Const::*;
-use crate::core::Expr::*;
-
-use self::TypeMessage::*;
-
-fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> {
- match c {
- Type => Ok(Kind),
- Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
- }
-}
-
-fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
- match (a, b) {
- (Type, Kind) => Err(()),
- (Kind, Kind) => Ok(Kind),
- (Type, Type) |
- (Kind, Type) => Ok(Type),
- }
-}
-
-fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
- let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1));
- match (vl, vr, xxs) {
- (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR,
- (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true,
- (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => {
- let nL2 = if xL == xL2 { nL - 1 } else { nL };
- let nR2 = if xR == xR2 { nR - 1 } else { nR };
- match_vars(&V(xL, nL2), &V(xR, nR2), xs)
- }
- }
-}
-
-fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
- where S: Clone + ::std::fmt::Debug,
- T: Clone + ::std::fmt::Debug
-{
- fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool
- where S: Clone + ::std::fmt::Debug,
- T: Clone + ::std::fmt::Debug
- {
- match (el, er) {
- (&Const(Type), &Const(Type)) |
- (&Const(Kind), &Const(Kind)) => true,
- (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx),
- (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => {
- //ctx <- State.get
- let eq1 = go(ctx, tL, tR);
- if eq1 {
- //State.put ((xL, xR):ctx)
- ctx.push((xL, xR));
- let eq2 = go(ctx, bL, bR);
- //State.put ctx
- let _ = ctx.pop();
- eq2
- } else {
- false
- }
- }
- (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
- if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
- (&BuiltinType(a), &BuiltinType(b)) => a == b,
- (&Record(ref ktsL0), &Record(ref ktsR0)) => {
- if ktsL0.len() != ktsR0.len() {
- return false;
- }
- /*
- let go ((kL, tL):ktsL) ((kR, tR):ktsR)
- | kL == kR = do
- b <- go tL tR
- if b
- then go ktsL ktsR
- else return False
- go [] [] = return True
- go _ _ = return False
- */
- /*
- for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) {
- if kL == kR {
- if !go(ctx, tL, tR) {
- return false;
- }
- } else {
- return false;
- }
- }
- true
- */
- !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
- kL != kR || !go(ctx, tL, tR)
- })
- }
- (&Union(ref ktsL0), &Union(ref ktsR0)) => {
- if ktsL0.len() != ktsR0.len() {
- return false;
- }
- /*
- let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
- | kL == kR = do
- b <- go tL tR
- if b
- then loop ktsL ktsR
- else return False
- loop [] [] = return True
- loop _ _ = return False
- loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
- */
- !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
- kL != kR || !go(ctx, tL, tR)
- })
- }
- (_, _) => false,
- }
- }
- let mut ctx = vec![];
- go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
-}
-
-fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
- e: &Expr<'i, S, X>,
- t: core::BuiltinType,
- ef: EF,
- l: &Expr<'i, S, X>,
- r: &Expr<'i, S, X>)
- -> Result<Expr<'i, S, X>, TypeError<'i, S>>
- where S: Clone + ::std::fmt::Debug + 'i,
- EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
-{
- let tl = normalize(&type_with(ctx, l)?);
- match tl {
- BuiltinType(lt) if lt == t => {}
- _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))),
- }
-
- let tr = normalize(&type_with(ctx, r)?);
- match tr {
- BuiltinType(rt) if rt == t => {}
- _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))),
- }
-
- Ok(BuiltinType(t))
-}
-
-/// Type-check an expression and return the expression'i type if type-checking
-/// suceeds or an error if type-checking fails
-///
-/// `type_with` does not necessarily normalize the type since full normalization
-/// is not necessary for just type-checking. If you actually care about the
-/// returned type then you may want to `normalize` it afterwards.
-pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
- e: &Expr<'i, S, X>)
- -> Result<Expr<'i, S, X>, TypeError<'i, S>>
- where S: Clone + ::std::fmt::Debug + 'i
-{
- match *e {
- Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
- Var(V(x, n)) => {
- ctx.lookup(x, n)
- .cloned()
- //.map(Cow::Borrowed)
- .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable))
- }
- Lam(x, ref tA, ref b) => {
- let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
- let tB = type_with(&ctx2, b)?;
- let p = Pi(x, tA.clone(), bx(tB));
- let _ = type_with(ctx, &p)?;
- //Ok(Cow::Owned(p))
- Ok(p)
- }
- Pi(x, ref tA, ref tB) => {
- let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
- let kA = match tA2 {
- Const(k) => k,
- _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))),
- };
-
- let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
- let tB = normalize(&type_with(&ctx2, tB)?);
- let kB = match tB {
- Const(k) => k,
- _ => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))),
- };
-
- match rule(kA, kB) {
- Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))),
- Ok(k) => Ok(Const(k)),
- }
- }
- App(ref f, ref a) => {
- let tf = normalize(&type_with(ctx, f)?);
- let (x, tA, tB) = match tf {
- Pi(x, tA, tB) => (x, tA, tB),
- _ => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))),
- };
- let tA2 = type_with(ctx, a)?;
- if prop_equal(&tA, &tA2) {
- let vx0 = V(x, 0);
- let a2 = shift::<S, S, X>( 1, vx0, a);
- let tB2 = subst(vx0, &a2, &tB);
- let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
- Ok(tB3)
- } else {
- let nf_A = normalize(&tA);
- let nf_A2 = normalize(&tA2);
- Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2)))
- }
- }
- Let(f, ref mt, ref r, ref b) => {
- let tR = type_with(ctx, r)?;
- let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
- let kR = match ttR {
- Const(k) => k,
- // Don't bother to provide a `let`-specific version of this error
- // message because this should never happen anyway
- _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
- };
-
- let ctx2 = ctx.insert(f, tR.clone());
- let tB = type_with(&ctx2, b)?;
- let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
- let kB = match ttB {
- Const(k) => k,
- // Don't bother to provide a `let`-specific version of this error
- // message because this should never happen anyway
- _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
- };
-
- if let Err(()) = rule(kR, kB) {
- return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB)));
- }
-
- if let Some(ref t) = *mt {
- let nf_t = normalize(t);
- let nf_tR = normalize(&tR);
- if !prop_equal(&nf_tR, &nf_t) {
- return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR)));
- }
- }
-
- Ok(tB)
- }
- Annot(ref x, ref t) => {
- // This is mainly just to check that `t` is not `Kind`
- let _ = type_with(ctx, t)?;
-
- let t2 = type_with(ctx, x)?;
- if prop_equal(t, &t2) {
- Ok((**t).clone())
- } else {
- let nf_t = normalize(t);
- let nf_t2 = normalize(&t2);
- Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
- }
- }
- BuiltinType(t) => Ok(match t {
- List | Optional => pi("_", Const(Type), Const(Type)),
- Bool | Natural | Integer | Double | Text => Const(Type),
- }),
- BoolLit(_) => Ok(BuiltinType(Bool)),
- BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
- BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
- BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
- BoolNE(ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r),
- BoolIf(ref x, ref y, ref z) => {
- let tx = normalize(&type_with(ctx, x)?);
- match tx {
- BuiltinType(Bool) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
- }
- let ty = normalize(&type_with(ctx, y)?);
- let tty = normalize(&type_with(ctx, &ty)?);
- match tty {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))),
- }
-
- let tz = normalize(&type_with(ctx, z)?);
- let ttz = normalize(&type_with(ctx, &tz)?);
- match ttz {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))),
- }
-
- if !prop_equal(&ty, &tz) {
- return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz)));
- }
- Ok(ty)
- }
- NaturalLit(_) => Ok(BuiltinType(Natural)),
- BuiltinValue(NaturalFold) =>
- Ok(pi("_", Natural,
- pi("natural", Const(Type),
- pi("succ", pi("_", "natural", "natural"),
- pi("zero", "natural", "natural"))))),
- BuiltinValue(NaturalBuild) =>
- Ok(pi("_",
- pi("natural", Const(Type),
- pi("succ", pi("_", "natural", "natural"),
- pi("zero", "natural", "natural"))),
- Natural)),
- BuiltinValue(NaturalIsZero) |
- BuiltinValue(NaturalEven) |
- BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
- NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
- NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
- IntegerLit(_) => Ok(BuiltinType(Integer)),
- DoubleLit(_) => Ok(BuiltinType(Double)),
- TextLit(_) => Ok(BuiltinType(Text)),
- TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
- ListLit(ref t, ref xs) => {
- let s = normalize::<_, S, _>(&type_with(ctx, t)?);
- match s {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidListType((**t).clone()))),
- }
- for (i, x) in xs.iter().enumerate() {
- let t2 = type_with(ctx, x)?;
- if !prop_equal(t, &t2) {
- let nf_t = normalize(t);
- let nf_t2 = normalize(&t2);
- return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
- }
- }
- Ok(App(bx(BuiltinType(List)), t.clone()))
- }
- BuiltinValue(ListBuild) =>
- Ok(pi("a", Const(Type),
- pi("_",
- pi("list", Const(Type),
- pi("cons", pi("_", "a", pi("_", "list", "list")),
- pi("nil", "list", "list"))),
- app(List, "a")))),
- BuiltinValue(ListFold) =>
- Ok(pi("a", Const(Type),
- pi("_", app(List, "a"),
- pi("list", Const(Type),
- pi("cons", pi("_", "a", pi("_", "list", "list")),
- pi("nil", "list", "list")))))),
- BuiltinValue(ListLength) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
- BuiltinValue(ListHead) |
- BuiltinValue(ListLast) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
- BuiltinValue(ListIndexed) => {
- let mut m = BTreeMap::new();
- m.insert("index", BuiltinType(Natural));
- m.insert("value", Expr::from("a"));
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
- }
- BuiltinValue(ListReverse) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
- OptionalLit(ref t, ref xs) => {
- let s = normalize::<_, S, _>(&type_with(ctx, t)?);
- match s {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidOptionalType((**t).clone()))),
- }
- let n = xs.len();
- if 2 <= n {
- return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n)));
- }
- for x in xs {
- let t2 = type_with(ctx, x)?;
- if !prop_equal(t, &t2) {
- let nf_t = normalize(t);
- let nf_t2 = normalize(&t2);
- return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
- }
- }
- Ok(App(bx(BuiltinType(Optional)), t.clone()))
- }
- BuiltinValue(OptionalFold) =>
- Ok(pi("a", Const(Type),
- pi("_", app(Optional, "a"),
- pi("optional", Const(Type),
- pi("just", pi("_", "a", "optional"),
- pi("nothing", "optional", "optional")))))),
- Record(ref kts) => {
- for (k, t) in kts {
- let s = normalize::<S, S, X>(&type_with(ctx, t)?);
- match s {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))),
- }
- }
- Ok(Const(Type))
- }
- RecordLit(ref kvs) => {
- let kts = kvs.iter().map(|(&k, v)| {
- let t = type_with(ctx, v)?;
- let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
- match s {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))),
- }
- Ok((k, t))
- }).collect::<Result<_, _>>()?;
- Ok(Record(kts))
- }
-/*
-type_with ctx e@(Union kts ) = do
- let process (k, t) = do
- s <- fmap Dhall.Core.normalize (type_with ctx t)
- case s of
- Const Type -> return ()
- _ -> Left (TypeError ctx e (InvalidAlternativeType k t))
- mapM_ process (Data.Map.toList kts)
- return (Const Type)
-type_with ctx e@(UnionLit k v kts) = do
- case Data.Map.lookup k kts of
- Just _ -> Left (TypeError ctx e (DuplicateAlternative k))
- Nothing -> return ()
- t <- type_with ctx v
- let union = Union (Data.Map.insert k t kts)
- _ <- type_with ctx union
- return union
-type_with ctx e@(Combine kvsX kvsY) = do
- tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
- ktsX <- case tKvsX of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))
-
- tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
- ktsY <- case tKvsY of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))
-
- let combineTypes ktsL ktsR = do
- let ks =
- Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)
- kts <- forM (toList ks) (\k -> do
- case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of
- (Just (Record ktsL'), Just (Record ktsR')) -> do
- t <- combineTypes ktsL' ktsR'
- return (k, t)
- (Nothing, Just t) -> do
- return (k, t)
- (Just t, Nothing) -> do
- return (k, t)
- _ -> do
- Left (TypeError ctx e (FieldCollision k)) )
- return (Record (Data.Map.fromList kts))
-
- combineTypes ktsX ktsY
-type_with ctx e@(Merge kvsX kvsY t) = do
- tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
- ktsX <- case tKvsX of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))
- let ksX = Data.Map.keysSet ktsX
-
- tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
- ktsY <- case tKvsY of
- Union kts -> return kts
- _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))
- let ksY = Data.Map.keysSet ktsY
-
- let diffX = Data.Set.difference ksX ksY
- let diffY = Data.Set.difference ksY ksX
-
- if Data.Set.null diffX
- then return ()
- else Left (TypeError ctx e (UnusedHandler diffX))
-
- let process (kY, tY) = do
- case Data.Map.lookup kY ktsX of
- Nothing -> Left (TypeError ctx e (MissingHandler diffY))
- Just tX ->
- case tX of
- Pi _ tY' t' -> do
- if prop_equal tY tY'
- then return ()
- else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
- if prop_equal t t'
- then return ()
- else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))
- _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
- mapM_ process (Data.Map.toList ktsY)
- return t
- */
- Field(ref r, x) => {
- let t = normalize(&type_with(ctx, r)?);
- match t {
- Record(ref kts) =>
- kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))),
- _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))),
- }
- }
- /*
-type_with ctx (Note s e' ) = case type_with ctx e' of
- Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m)
- Left (TypeError ctx2 e'' m) -> Left (TypeError ctx2 (Note s e'') m)
- Right r -> Right r
-*/
- Embed(p) => match p {},
- _ => panic!("Unimplemented typecheck case: {:?}", e),
- }
-}
-
-/// `typeOf` is the same as `type_with` with an empty context, meaning that the
-/// expression must be closed (i.e. no free variables), otherwise type-checking
-/// will fail.
-pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result<Expr<'i, S, X>, TypeError<'i, S>> {
- let ctx = Context::new();
- type_with(&ctx, e) //.map(|e| e.into_owned())
-}
-
-/// The specific type error
-#[derive(Debug)]
-pub enum TypeMessage<'i, S> {
- UnboundVariable,
- InvalidInputType(Expr<'i, S, X>),
- InvalidOutputType(Expr<'i, S, X>),
- NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
- TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- Untyped,
- InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- InvalidListType(Expr<'i, S, X>),
- InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- InvalidOptionalLiteral(usize),
- InvalidOptionalType(Expr<'i, S, X>),
- InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
- IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- InvalidField(String, Expr<'i, S, X>),
- InvalidFieldType(String, Expr<'i, S, X>),
- InvalidAlternative(String, Expr<'i, S, X>),
- InvalidAlternativeType(String, Expr<'i, S, X>),
- DuplicateAlternative(String),
- MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
- FieldCollision(String),
- MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
- MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
- UnusedHandler(HashSet<String>),
- MissingHandler(HashSet<String>),
- HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
- HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
- HandlerNotAFunction(String, Expr<'i, S, X>),
- NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>),
- MissingField(String, Expr<'i, S, X>),
- CantAnd(Expr<'i, S, X>, Expr<'i, S, X>),
- CantOr(Expr<'i, S, X>, Expr<'i, S, X>),
- CantEQ(Expr<'i, S, X>, Expr<'i, S, X>),
- CantNE(Expr<'i, S, X>, Expr<'i, S, X>),
- CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>),
- CantAdd(Expr<'i, S, X>, Expr<'i, S, X>),
- CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>),
- NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>),
- NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>),
-}
-
-/// A structured type error that includes context
-#[derive(Debug)]
-pub struct TypeError<'i, S> {
- pub context: Context<'i, Expr<'i, S, X>>,
- pub current: Expr<'i, S, X>,
- pub type_message: TypeMessage<'i, S>,
-}
-
-impl<'i, S: Clone> TypeError<'i, S> {
- pub fn new(context: &Context<'i, Expr<'i, S, X>>,
- current: &Expr<'i, S, X>,
- type_message: TypeMessage<'i, S>)
- -> Self {
- TypeError {
- context: context.clone(),
- current: current.clone(),
- type_message: type_message,
- }
- }
-}
-
-impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
- fn description(&self) -> &str {
- match *self {
- UnboundVariable => "Unbound variable",
- InvalidInputType(_) => "Invalid function input",
- InvalidOutputType(_) => "Invalid function output",
- NotAFunction(_, _) => "Not a function",
- TypeMismatch(_, _, _, _) => "Wrong type of function argument",
- _ => "Unhandled error",
- }
- }
-}
-
-impl<'i, S> fmt::Display for TypeMessage<'i, S> {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- match *self {
- UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")),
- TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
- let template = include_str!("errors/TypeMismatch.txt");
- let s = template
- .replace("$txt0", &format!("{}", e0))
- .replace("$txt1", &format!("{}", e1))
- .replace("$txt2", &format!("{}", e2))
- .replace("$txt3", &format!("{}", e3));
- f.write_str(&s)
- }
- _ => f.write_str("Unhandled error message"),
- }
- }
-}