summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs1
-rw-r--r--dhall/src/expr.rs46
-rw-r--r--dhall/src/imports.rs127
-rw-r--r--dhall/src/lib.rs23
-rw-r--r--dhall/src/main.rs20
-rw-r--r--dhall/src/normalize.rs15
-rw-r--r--dhall/src/traits.rs (renamed from dhall/src/dhall_type.rs)22
-rw-r--r--dhall/src/typecheck.rs663
-rw-r--r--dhall/tests/common/mod.rs105
-rw-r--r--dhall/tests/normalization.rs1
-rw-r--r--dhall/tests/parser.rs1
-rw-r--r--dhall/tests/traits.rs (renamed from dhall/tests/dhall_type.rs)14
-rw-r--r--dhall/tests/typecheck.rs13
-rw-r--r--dhall_core/src/core.rs40
-rw-r--r--dhall_core/src/parser.rs2
-rw-r--r--dhall_generator/src/derive.rs (renamed from dhall_generator/src/dhall_type.rs)16
-rw-r--r--dhall_generator/src/lib.rs12
-rw-r--r--dhall_generator/src/quote.rs (renamed from dhall_generator/src/dhall_expr.rs)3
18 files changed, 722 insertions, 402 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 1ba1873..87972cf 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -29,6 +29,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
"False" => BoolLit(false),
"Type" => Const(Const::Type),
"Kind" => Const(Const::Kind),
+ "Sort" => Const(Const::Sort),
s => Var(V(Label::from(s), 0)),
},
},
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
new file mode 100644
index 0000000..7baf628
--- /dev/null
+++ b/dhall/src/expr.rs
@@ -0,0 +1,46 @@
+use crate::imports::ImportRoot;
+use dhall_core::*;
+
+macro_rules! derive_other_traits {
+ ($ty:ident) => {
+ impl std::cmp::PartialEq for $ty {
+ fn eq(&self, other: &Self) -> bool {
+ self.0 == other.0
+ }
+ }
+
+ impl std::fmt::Display for $ty {
+ fn fmt(
+ &self,
+ f: &mut std::fmt::Formatter,
+ ) -> Result<(), std::fmt::Error> {
+ self.0.fmt(f)
+ }
+ }
+ };
+}
+
+#[derive(Debug, Clone, Eq)]
+pub struct Parsed(pub(crate) SubExpr<X, Import>, pub(crate) ImportRoot);
+derive_other_traits!(Parsed);
+
+#[derive(Debug, Clone, Eq)]
+pub struct Resolved(pub(crate) SubExpr<X, X>);
+derive_other_traits!(Resolved);
+
+#[derive(Debug, Clone, Eq)]
+pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
+derive_other_traits!(Typed);
+
+#[derive(Debug, Clone, Eq)]
+pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type);
+derive_other_traits!(Normalized);
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Type(pub(crate) TypeInternal);
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum TypeInternal {
+ Expr(Box<Normalized>),
+ Untyped,
+}
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 96268ca..fdde8c3 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -1,6 +1,8 @@
// use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X};
use dhall_core::{Expr, Import, X};
// use std::path::Path;
+use crate::binary::DecodeError;
+use crate::expr::*;
use dhall_core::*;
use std::fmt;
use std::fs::File;
@@ -8,9 +10,38 @@ use std::io::Read;
use std::path::Path;
use std::path::PathBuf;
-pub fn panic_imports<S: Clone>(expr: &Expr<S, Import>) -> Expr<S, X> {
- let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) };
- expr.map_embed(&no_import)
+#[derive(Debug)]
+pub enum ImportError {
+ ParseError(ParseError),
+ BinaryDecodeError(DecodeError),
+ IOError(std::io::Error),
+ UnexpectedImportError(Import),
+}
+impl From<ParseError> for ImportError {
+ fn from(e: ParseError) -> Self {
+ ImportError::ParseError(e)
+ }
+}
+impl From<DecodeError> for ImportError {
+ fn from(e: DecodeError) -> Self {
+ ImportError::BinaryDecodeError(e)
+ }
+}
+impl From<std::io::Error> for ImportError {
+ fn from(e: std::io::Error) -> Self {
+ ImportError::IOError(e)
+ }
+}
+impl fmt::Display for ImportError {
+ fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+ use self::ImportError::*;
+ match self {
+ ParseError(e) => e.fmt(f),
+ BinaryDecodeError(_) => unimplemented!(),
+ IOError(e) => e.fmt(f),
+ UnexpectedImportError(e) => e.fmt(f),
+ }
+ }
}
/// A root from which to resolve relative imports.
@@ -22,7 +53,7 @@ pub enum ImportRoot {
fn resolve_import(
import: &Import,
root: &ImportRoot,
-) -> Result<Expr<X, X>, DhallError> {
+) -> Result<Expr<X, X>, ImportError> {
use self::ImportRoot::*;
use dhall_core::FilePrefix::*;
use dhall_core::ImportLocation::*;
@@ -42,55 +73,59 @@ fn resolve_import(
}
}
-#[derive(Debug)]
-pub enum DhallError {
- ParseError(ParseError),
- IOError(std::io::Error),
+fn resolve_expr(
+ Parsed(expr, root): Parsed,
+ allow_imports: bool,
+) -> Result<Resolved, ImportError> {
+ let resolve = |import: &Import| -> Result<SubExpr<X, X>, ImportError> {
+ if allow_imports {
+ let expr = resolve_import(import, &root)?;
+ Ok(expr.roll())
+ } else {
+ Err(ImportError::UnexpectedImportError(import.clone()))
+ }
+ };
+ let expr = expr.as_ref().traverse_embed(&resolve)?;
+ Ok(Resolved(expr.squash_embed()))
}
-impl From<ParseError> for DhallError {
- fn from(e: ParseError) -> Self {
- DhallError::ParseError(e)
+
+impl Parsed {
+ pub fn load_from_file(f: &Path) -> Result<Parsed, ImportError> {
+ let mut buffer = String::new();
+ File::open(f)?.read_to_string(&mut buffer)?;
+ let expr = parse_expr(&*buffer)?;
+ let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
+ Ok(Parsed(expr, root))
}
-}
-impl From<std::io::Error> for DhallError {
- fn from(e: std::io::Error) -> Self {
- DhallError::IOError(e)
+
+ pub fn load_from_str(s: &str) -> Result<Parsed, ImportError> {
+ let expr = parse_expr(s)?;
+ let root = ImportRoot::LocalDir(std::env::current_dir()?);
+ Ok(Parsed(expr, root))
}
-}
-impl fmt::Display for DhallError {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use self::DhallError::*;
- match self {
- ParseError(e) => e.fmt(f),
- IOError(e) => e.fmt(f),
- }
+
+ pub fn load_from_binary_file(f: &Path) -> Result<Parsed, ImportError> {
+ let mut buffer = Vec::new();
+ File::open(f)?.read_to_end(&mut buffer)?;
+ let expr = crate::binary::decode(&buffer)?;
+ let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
+ Ok(Parsed(expr, root))
+ }
+
+ pub fn resolve(self) -> Result<Resolved, ImportError> {
+ crate::imports::resolve_expr(self, true)
+ }
+ pub fn skip_resolve(self) -> Result<Resolved, ImportError> {
+ crate::imports::resolve_expr(self, false)
}
}
+// Deprecated
pub fn load_dhall_file(
f: &Path,
resolve_imports: bool,
-) -> Result<Expr<X, X>, DhallError> {
- let mut buffer = String::new();
- File::open(f)?.read_to_string(&mut buffer)?;
- let expr = parse_expr(&*buffer)?;
- let expr = if resolve_imports {
- let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
- let resolve = |import: &Import| -> Expr<X, X> {
- resolve_import(import, &root).unwrap()
- };
- expr.as_ref().map_embed(&resolve).squash_embed()
- } else {
- panic_imports(expr.as_ref())
- };
- Ok(expr)
-}
-
-pub fn load_dhall_file_no_resolve_imports(
- f: &Path,
-) -> Result<ParsedExpr, DhallError> {
- let mut buffer = String::new();
- File::open(f)?.read_to_string(&mut buffer)?;
- let expr = parse_expr(&*buffer)?;
- Ok(expr)
+) -> Result<Expr<X, X>, ImportError> {
+ let expr = Parsed::load_from_file(f)?;
+ let expr = resolve_expr(expr, resolve_imports)?;
+ Ok(expr.0.unroll())
}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 103fd29..f00e5b6 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -7,23 +7,14 @@
clippy::many_single_char_names
)]
+mod binary;
+mod imports;
mod normalize;
-pub use crate::normalize::*;
-pub mod binary;
-mod dhall_type;
-pub mod imports;
+pub mod traits;
pub mod typecheck;
-pub use crate::dhall_type::*;
+pub use crate::imports::{load_dhall_file, ImportError};
+pub use crate::traits::StaticType;
pub use dhall_generator::expr;
pub use dhall_generator::subexpr;
-pub use dhall_generator::Type;
-
-pub use crate::imports::*;
-
-// pub struct DhallExpr(dhall_core::DhallExpr);
-
-// impl DhallExpr {
-// pub fn normalize(self) -> Self {
-// DhallExpr(crate::normalize::normalize(self.0))
-// }
-// }
+pub use dhall_generator::StaticType;
+pub mod expr;
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 77f558c..2881d5a 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -2,9 +2,6 @@ use std::error::Error;
use std::io::{self, Read};
use term_painter::ToStyle;
-use dhall::*;
-use dhall_core::*;
-
const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
const BOLD: term_painter::Attr = term_painter::Attr::Bold;
@@ -57,17 +54,19 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
fn main() {
let mut buffer = String::new();
io::stdin().read_to_string(&mut buffer).unwrap();
- let expr = match parse_expr(&buffer) {
- Ok(e) => e,
+
+ let expr = match dhall::expr::Parsed::load_from_str(&buffer) {
+ Ok(expr) => expr,
Err(e) => {
print_error(&format!("Parse error {}", e), &buffer, 0, 0);
return;
}
};
- let expr: SubExpr<_, _> = rc(imports::panic_imports(expr.as_ref()));
+ let expr = expr.resolve().unwrap();
- let type_expr = match typecheck::type_of(expr.clone()) {
+ let expr = match expr.typecheck() {
+ Ok(expr) => expr,
Err(e) => {
let explain = ::std::env::args().any(|s| s == "--explain");
if !explain {
@@ -84,10 +83,9 @@ fn main() {
// FIXME Print source position
return;
}
- Ok(type_expr) => type_expr,
};
- println!("{}", type_expr);
- println!();
- println!("{}", normalize(expr));
+ let expr = expr.normalize();
+
+ println!("{}", expr);
}
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 24a8601..c07d3cb 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1,8 +1,19 @@
#![allow(non_snake_case)]
+use crate::expr::*;
use dhall_core::*;
use dhall_generator::dhall_expr;
use std::fmt;
+impl Typed {
+ pub fn normalize(self) -> Normalized {
+ Normalized(normalize(self.0), self.1)
+ }
+ /// Pretends this expression is normalized. Use with care.
+ pub fn skip_normalize(self) -> Normalized {
+ Normalized(self.0, self.1)
+ }
+}
+
fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
where
S: fmt::Debug + Clone,
@@ -202,7 +213,7 @@ enum WhatNext<'a, S, A> {
DoneAsIs,
}
-pub fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
+fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
where
S: fmt::Debug + Clone,
A: fmt::Debug + Clone,
@@ -306,7 +317,7 @@ where
/// However, `normalize` will not fail if the expression is ill-typed and will
/// leave ill-typed sub-expressions unevaluated.
///
-pub fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
+fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
where
S: fmt::Debug + Clone,
A: fmt::Debug + Clone,
diff --git a/dhall/src/dhall_type.rs b/dhall/src/traits.rs
index 6b0e06e..64e07d9 100644
--- a/dhall/src/dhall_type.rs
+++ b/dhall/src/traits.rs
@@ -4,37 +4,37 @@ use dhall_generator::*;
#[derive(Debug, Clone)]
pub enum ConversionError {}
-pub trait Type {
+pub trait StaticType {
fn get_type() -> DhallExpr;
// fn as_dhall(&self) -> DhallExpr;
// fn from_dhall(e: DhallExpr) -> Result<Self, DhallConversionError>;
}
-impl Type for bool {
+impl StaticType for bool {
fn get_type() -> DhallExpr {
dhall_expr!(Bool)
}
}
-impl Type for Natural {
+impl StaticType for Natural {
fn get_type() -> DhallExpr {
dhall_expr!(Natural)
}
}
-impl Type for Integer {
+impl StaticType for Integer {
fn get_type() -> DhallExpr {
dhall_expr!(Integer)
}
}
-impl Type for String {
+impl StaticType for String {
fn get_type() -> DhallExpr {
dhall_expr!(Text)
}
}
-impl<A: Type, B: Type> Type for (A, B) {
+impl<A: StaticType, B: StaticType> StaticType for (A, B) {
fn get_type() -> DhallExpr {
let ta = A::get_type();
let tb = B::get_type();
@@ -42,33 +42,33 @@ impl<A: Type, B: Type> Type for (A, B) {
}
}
-impl<T: Type> Type for Option<T> {
+impl<T: StaticType> StaticType for Option<T> {
fn get_type() -> DhallExpr {
let t = T::get_type();
dhall_expr!(Optional t)
}
}
-impl<T: Type> Type for Vec<T> {
+impl<T: StaticType> StaticType for Vec<T> {
fn get_type() -> DhallExpr {
let t = T::get_type();
dhall_expr!(List t)
}
}
-impl<'a, T: Type> Type for &'a T {
+impl<'a, T: StaticType> StaticType for &'a T {
fn get_type() -> DhallExpr {
T::get_type()
}
}
-impl<T> Type for std::marker::PhantomData<T> {
+impl<T> StaticType for std::marker::PhantomData<T> {
fn get_type() -> DhallExpr {
dhall_expr!({})
}
}
-impl<T: Type, E: Type> Type for Result<T, E> {
+impl<T: StaticType, E: StaticType> StaticType for Result<T, E> {
fn get_type() -> DhallExpr {
let tt = T::get_type();
let te = E::get_type();
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e63b032..babfad0 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,8 +1,7 @@
#![allow(non_snake_case)]
-use std::collections::HashSet;
use std::fmt;
-use crate::normalize::normalize;
+use crate::expr::*;
use dhall_core;
use dhall_core::context::Context;
use dhall_core::*;
@@ -10,21 +9,119 @@ use dhall_generator as dhall;
use self::TypeMessage::*;
-fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
- use dhall_core::Const::*;
- use dhall_core::ExprF::*;
- match c {
- Type => Ok(Kind),
- Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
+impl Resolved {
+ pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
+ type_of_(self.0.clone())
+ }
+ /// Pretends this expression has been typechecked. Use with care.
+ pub fn skip_typecheck(self) -> Typed {
+ Typed(self.0, UNTYPE)
+ }
+}
+impl Typed {
+ #[inline(always)]
+ fn as_expr(&self) -> &SubExpr<X, X> {
+ &self.0
+ }
+ #[inline(always)]
+ fn into_expr(self) -> SubExpr<X, X> {
+ self.0
+ }
+ #[inline(always)]
+ pub fn get_type(&self) -> &Type {
+ &self.1
+ }
+ #[inline(always)]
+ fn get_type_move(self) -> Type {
+ self.1
+ }
+}
+impl Normalized {
+ #[inline(always)]
+ fn as_expr(&self) -> &SubExpr<X, X> {
+ &self.0
+ }
+ #[inline(always)]
+ fn into_expr(self) -> SubExpr<X, X> {
+ self.0
+ }
+ #[inline(always)]
+ pub fn get_type(&self) -> &Type {
+ &self.1
+ }
+ #[inline(always)]
+ fn into_type(self) -> Type {
+ crate::expr::Type(TypeInternal::Expr(Box::new(self)))
+ }
+ // Expose the outermost constructor
+ #[inline(always)]
+ fn unroll_ref(&self) -> &Expr<X, X> {
+ self.as_expr().as_ref()
+ }
+ #[inline(always)]
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ // shift the type too ?
+ Normalized(shift(delta, var, &self.0), self.1.clone())
}
}
+impl Type {
+ #[inline(always)]
+ pub fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
+ use TypeInternal::*;
+ match &self.0 {
+ Expr(e) => Ok(e),
+ Untyped => Err(TypeError::new(
+ &Context::new(),
+ rc(ExprF::Const(Const::Sort)),
+ TypeMessage::Untyped,
+ )),
+ }
+ }
+ #[inline(always)]
+ fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
+ use TypeInternal::*;
+ match self.0 {
+ Expr(e) => Ok(*e),
+ Untyped => Err(TypeError::new(
+ &Context::new(),
+ rc(ExprF::Const(Const::Sort)),
+ TypeMessage::Untyped,
+ )),
+ }
+ }
+ // Expose the outermost constructor
+ #[inline(always)]
+ fn unroll_ref(&self) -> Result<&Expr<X, X>, TypeError<X>> {
+ Ok(self.as_normalized()?.unroll_ref())
+ }
+ #[inline(always)]
+ pub fn get_type(&self) -> &Type {
+ use TypeInternal::*;
+ match &self.0 {
+ Expr(e) => e.get_type(),
+ Untyped => &UNTYPE,
+ }
+ }
+ #[inline(always)]
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ use TypeInternal::*;
+ crate::expr::Type(match &self.0 {
+ Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Untyped => Untyped,
+ })
+ }
+}
+
+const UNTYPE: Type = Type(TypeInternal::Untyped);
fn rule(a: Const, b: Const) -> Result<Const, ()> {
use dhall_core::Const::*;
match (a, b) {
- (Type, Kind) => Err(()),
+ (_, Type) => Ok(Type),
(Kind, Kind) => Ok(Kind),
- (Type, Type) | (Kind, Type) => Ok(Type),
+ (Sort, Sort) => Ok(Sort),
+ (Sort, Kind) => Ok(Sort),
+ _ => Err(()),
}
}
@@ -48,11 +145,7 @@ fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
}
// Takes normalized expressions as input
-fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
-where
- S: ::std::fmt::Debug,
- T: ::std::fmt::Debug,
-{
+fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
use dhall_core::ExprF::*;
fn go<S, T>(
ctx: &mut Vec<(Label, Label)>,
@@ -108,8 +201,14 @@ where
(_, _) => false,
}
}
- let mut ctx = vec![];
- go::<S, T>(&mut ctx, eL0, eR0)
+ match (&eL0.0, &eR0.0) {
+ (TypeInternal::Untyped, TypeInternal::Untyped) => false,
+ (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+ let mut ctx = vec![];
+ go(&mut ctx, l.unroll_ref(), r.unroll_ref())
+ }
+ _ => false,
+ }
}
fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
@@ -176,346 +275,386 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
}
}
-fn ensure_equal<'a, S, F1, F2>(
- x: &'a Expr<S, X>,
- y: &'a Expr<S, X>,
- mkerr: F1,
- mkmsg: F2,
-) -> Result<(), TypeError<S>>
-where
- S: std::fmt::Debug,
- F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
- F2: FnOnce() -> TypeMessage<S>,
-{
- if prop_equal(x, y) {
- Ok(())
- } else {
- Err(mkerr(mkmsg()))
- }
+macro_rules! ensure_equal {
+ ($x:expr, $y:expr, $err:expr $(,)*) => {
+ if !prop_equal(&$x, &$y) {
+ return Err($err);
+ }
+ };
}
-/// Type-check an expression and return the expression's type if type-checking
-/// succeeds or an error if type-checking fails
-///
-/// `type_with` normalizes the type since while type-checking. It expects the
-/// context to contain only normalized expressions.
-pub fn type_with<S>(
- ctx: &Context<Label, SubExpr<S, X>>,
- e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
- S: ::std::fmt::Debug + Clone,
-{
+macro_rules! ensure_matches {
+ ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => {
+ match $x.unroll_ref()? {
+ $pat => $branch,
+ _ => return Err($err),
+ }
+ };
+}
+
+macro_rules! ensure_is_type {
+ ($x:expr, $err:expr $(,)*) => {
+ ensure_matches!($x, Const(Type) => {}, $err)
+ };
+}
+
+macro_rules! ensure_is_const {
+ ($x:expr, $err:expr $(,)*) => {
+ ensure_matches!($x, Const(k) => *k, $err)
+ };
+}
+
+/// Type-check an expression and return the expression alongside its type
+/// if type-checking succeeded, or an error if type-checking failed
+pub fn type_with(
+ ctx: &Context<Label, Type>,
+ e: SubExpr<X, X>,
+) -> Result<Typed, TypeError<X>> {
use dhall_core::BinOp::*;
use dhall_core::Builtin::*;
use dhall_core::Const::*;
use dhall_core::ExprF::*;
let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
- let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
- {
- Const(k) => Ok(*k),
- _ => Err(mkerr(msg)),
- };
- let ensure_is_type =
- |x: SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() {
- Const(Type) => Ok(()),
- _ => Err(mkerr(msg)),
- };
+ let mktype =
+ |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
+
+ enum Ret {
+ RetType(crate::expr::Type),
+ RetExpr(Expr<X, X>),
+ }
+ use Ret::*;
let ret = match e.as_ref() {
Lam(x, t, b) => {
- let t2 = normalize(SubExpr::clone(t));
+ let t = mktype(ctx, t.clone())?;
let ctx2 = ctx
- .insert(x.clone(), t2.clone())
- .map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = type_with(&ctx2, b.clone())?;
- let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?;
- Ok(Pi(x.clone(), t2, tB))
+ .insert(x.clone(), t.clone())
+ .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let b = type_with(&ctx2, b.clone())?;
+ Ok(RetType(mktype(
+ ctx,
+ rc(Pi(
+ x.clone(),
+ t.into_normalized()?.into_expr(),
+ b.get_type_move().into_normalized()?.into_expr(),
+ )),
+ )?))
}
Pi(x, tA, tB) => {
- let ttA = type_with(ctx, tA.clone())?;
- let tA = normalize(SubExpr::clone(tA));
- let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
+ let tA = mktype(ctx, tA.clone())?;
+ let kA = ensure_is_const!(
+ &tA.get_type(),
+ mkerr(InvalidInputType(tA.into_normalized()?)),
+ );
let ctx2 = ctx
.insert(x.clone(), tA.clone())
- .map(|e| shift(1, &V(x.clone(), 0), e));
+ .map(|e| e.shift(1, &V(x.clone(), 0)));
let tB = type_with(&ctx2, tB.clone())?;
- let kB = match tB.as_ref() {
- Const(k) => *k,
- _ => {
- return Err(TypeError::new(
- &ctx2,
- e.clone(),
- InvalidOutputType(tB),
- ));
- }
- };
+ let kB = ensure_is_const!(
+ &tB.get_type(),
+ TypeError::new(
+ &ctx2,
+ e.clone(),
+ InvalidOutputType(tB.get_type_move().into_normalized()?),
+ ),
+ );
match rule(kA, kB) {
- Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))),
- Ok(_) => Ok(Const(kB)),
+ Err(()) => Err(mkerr(NoDependentTypes(
+ tA.clone().into_normalized()?,
+ tB.get_type_move().into_normalized()?,
+ ))),
+ Ok(k) => Ok(RetExpr(Const(k))),
}
}
Let(f, mt, r, b) => {
let r = if let Some(t) = mt {
- rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
+ let r = SubExpr::clone(r);
+ let t = SubExpr::clone(t);
+ dhall::subexpr!(r: t)
} else {
SubExpr::clone(r)
};
- let tR = type_with(ctx, r)?;
- let ttR = type_with(ctx, tR.clone())?;
+ let r = type_with(ctx, r)?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
- let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
+ let kR = ensure_is_const!(
+ &r.get_type().get_type(),
+ mkerr(InvalidInputType(r.get_type_move().into_normalized()?)),
+ );
- let ctx2 = ctx.insert(f.clone(), tR.clone());
- let tB = type_with(&ctx2, b.clone())?;
- let ttB = type_with(ctx, tB.clone())?;
+ let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
+ let b = type_with(&ctx2, b.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
- let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
+ let kB = ensure_is_const!(
+ &b.get_type().get_type(),
+ mkerr(InvalidOutputType(b.get_type_move().into_normalized()?)),
+ );
if let Err(()) = rule(kR, kB) {
- return Err(mkerr(NoDependentLet(tR, tB)));
+ return Err(mkerr(NoDependentLet(
+ r.get_type_move().into_normalized()?,
+ b.get_type_move().into_normalized()?,
+ )));
}
- Ok(tB.unroll())
+ Ok(RetType(b.get_type_move()))
}
_ => match e
.as_ref()
- .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
+ .traverse_ref_simple(|e| type_with(ctx, e.clone()))?
{
Lam(_, _, _) => unreachable!(),
Pi(_, _, _) => unreachable!(),
Let(_, _, _, _) => unreachable!(),
- Const(c) => axiom(c).map(Const),
+ Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
+ Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
+ Const(Sort) => Ok(RetType(UNTYPE)),
Var(V(x, n)) => match ctx.lookup(&x, n) {
- Some(e) => Ok(e.unroll()),
+ Some(e) => Ok(RetType(e.clone())),
None => Err(mkerr(UnboundVariable)),
},
- App((f, mut tf), args) => {
+ App(f, args) => {
let mut iter = args.into_iter();
let mut seen_args: Vec<SubExpr<_, _>> = vec![];
- while let Some((a, ta)) = iter.next() {
- seen_args.push(a.clone());
- let (x, tx, tb) = match tf.as_ref() {
+ let mut tf = f.get_type().clone();
+ while let Some(a) = iter.next() {
+ seen_args.push(a.as_expr().clone());
+ let (x, tx, tb) = ensure_matches!(tf,
Pi(x, tx, tb) => (x, tx, tb),
- _ => {
- return Err(mkerr(NotAFunction(
- rc(App(f.clone(), seen_args)),
- tf,
- )));
- }
- };
- ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || {
- TypeMismatch(
- rc(App(f.clone(), seen_args.clone())),
- tx.clone(),
- a.clone(),
- ta.clone(),
- )
- })?;
- tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb));
+ mkerr(NotAFunction(Typed(
+ rc(App(f.into_expr(), seen_args)),
+ tf,
+ )))
+ );
+ let tx = mktype(ctx, tx.clone())?;
+ ensure_equal!(
+ tx,
+ a.get_type(),
+ mkerr(TypeMismatch(
+ Typed(rc(App(f.into_expr(), seen_args)), tf),
+ tx.into_normalized()?,
+ a,
+ ))
+ );
+ tf = mktype(
+ ctx,
+ subst_shift(&V(x.clone(), 0), &a.as_expr(), &tb),
+ )?;
}
- Ok(tf.unroll())
+ Ok(RetType(tf))
}
- Annot((x, tx), (t, _)) => {
- let t = normalize(t.clone());
- ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
- AnnotMismatch(x.clone(), t.clone(), tx.clone())
- })?;
- Ok(t.unroll())
+ Annot(x, t) => {
+ let t = t.normalize().into_type();
+ ensure_equal!(
+ t,
+ x.get_type(),
+ mkerr(AnnotMismatch(x, t.into_normalized()?))
+ );
+ Ok(RetType(x.get_type_move()))
}
- BoolIf((x, tx), (y, ty), (z, tz)) => {
- ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
- InvalidPredicate(x.clone(), tx.clone())
- })?;
- let tty = type_with(ctx, ty.clone())?;
- ensure_is_type(
- tty.clone(),
- IfBranchMustBeTerm(
- true,
- y.clone(),
- ty.clone(),
- tty.clone(),
- ),
- )?;
+ BoolIf(x, y, z) => {
+ ensure_equal!(
+ x.get_type(),
+ mktype(ctx, rc(Builtin(Bool)))?,
+ mkerr(InvalidPredicate(x)),
+ );
+ ensure_is_type!(
+ y.get_type().get_type(),
+ mkerr(IfBranchMustBeTerm(true, y)),
+ );
- let ttz = type_with(ctx, tz.clone())?;
- ensure_is_type(
- ttz.clone(),
- IfBranchMustBeTerm(
- false,
- z.clone(),
- tz.clone(),
- ttz.clone(),
- ),
- )?;
+ ensure_is_type!(
+ z.get_type().get_type(),
+ mkerr(IfBranchMustBeTerm(false, z)),
+ );
- ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || {
- IfBranchMismatch(
- y.clone(),
- z.clone(),
- ty.clone(),
- tz.clone(),
- )
- })?;
- Ok(ty.unroll())
+ ensure_equal!(
+ y.get_type(),
+ z.get_type(),
+ mkerr(IfBranchMismatch(y, z))
+ );
+
+ Ok(RetType(y.get_type_move()))
}
- EmptyListLit((t, tt)) => {
- ensure_is_type(tt, InvalidListType(t.clone()))?;
- let t = normalize(SubExpr::clone(t));
- Ok(dhall::expr!(List t))
+ EmptyListLit(t) => {
+ let t = t.normalize().into_type();
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidListType(t.into_normalized()?)),
+ );
+ let t = t.into_normalized()?.into_expr();
+ Ok(RetExpr(dhall::expr!(List t)))
}
NEListLit(xs) => {
let mut iter = xs.into_iter().enumerate();
- let (_, (_, t)) = iter.next().unwrap();
- let s = type_with(ctx, t.clone())?;
- ensure_is_type(s, InvalidListType(t.clone()))?;
- for (i, (y, ty)) in iter {
- ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
- InvalidListElement(i, t.clone(), y.clone(), ty.clone())
- })?;
+ let (_, x) = iter.next().unwrap();
+ ensure_is_type!(
+ x.get_type().get_type(),
+ mkerr(InvalidListType(
+ x.get_type_move().into_normalized()?
+ )),
+ );
+ for (i, y) in iter {
+ ensure_equal!(
+ x.get_type(),
+ y.get_type(),
+ mkerr(InvalidListElement(
+ i,
+ x.get_type_move().into_normalized()?,
+ y
+ ))
+ );
}
- Ok(dhall::expr!(List t))
+ let t = x.get_type_move().into_normalized()?.into_expr();
+ Ok(RetExpr(dhall::expr!(List t)))
}
- EmptyOptionalLit((t, tt)) => {
- ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
- let t = normalize(t.clone());
- Ok(dhall::expr!(Optional t))
+ EmptyOptionalLit(t) => {
+ let t = t.normalize().into_type();
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidOptionalType(t.into_normalized()?)),
+ );
+ let t = t.into_normalized()?.into_expr();
+ Ok(RetExpr(dhall::expr!(Optional t)))
}
- NEOptionalLit((_, t)) => {
- let s = type_with(ctx, t.clone())?;
- ensure_is_type(s, InvalidOptionalType(t.clone()))?;
- Ok(dhall::expr!(Optional t))
+ NEOptionalLit(x) => {
+ let tx = x.get_type_move();
+ ensure_is_type!(
+ tx.get_type(),
+ mkerr(InvalidOptionalType(tx.into_normalized()?,)),
+ );
+ let t = tx.into_normalized()?.into_expr();
+ Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
- for (k, (t, tt)) in kts {
- ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
+ for (k, t) in kts {
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidFieldType(k, t)),
+ );
}
- Ok(Const(Type))
+ Ok(RetExpr(dhall::expr!(Type)))
}
RecordLit(kvs) => {
let kts = kvs
.into_iter()
- .map(|(k, (v, t))| {
- let s = type_with(ctx, t.clone())?;
- ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
- Ok((k.clone(), t))
+ .map(|(k, v)| {
+ ensure_is_type!(
+ v.get_type().get_type(),
+ mkerr(InvalidField(k, v)),
+ );
+ Ok((
+ k,
+ v.get_type_move().into_normalized()?.into_expr(),
+ ))
})
.collect::<Result<_, _>>()?;
- Ok(RecordType(kts))
+ Ok(RetExpr(RecordType(kts)))
}
- Field((r, tr), x) => match tr.as_ref() {
+ Field(r, x) => ensure_matches!(r.get_type(),
RecordType(kts) => match kts.get(&x) {
- Some(e) => Ok(e.unroll()),
- None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
+ Some(e) => Ok(RetExpr(e.unroll())),
+ None => Err(mkerr(MissingField(x, r))),
},
- _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))),
- },
- Builtin(b) => Ok(type_of_builtin(b)),
- BoolLit(_) => Ok(Builtin(Bool)),
- NaturalLit(_) => Ok(Builtin(Natural)),
- IntegerLit(_) => Ok(Builtin(Integer)),
- DoubleLit(_) => Ok(Builtin(Double)),
+ mkerr(NotARecord(x, r))
+ ),
+ Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
+ BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))),
+ NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))),
+ IntegerLit(_) => Ok(RetExpr(dhall::expr!(Integer))),
+ DoubleLit(_) => Ok(RetExpr(dhall::expr!(Double))),
// TODO: check type of interpolations
- TextLit(_) => Ok(Builtin(Text)),
- BinOp(o, (l, tl), (r, tr)) => {
- let t = Builtin(match o {
- BoolAnd => Bool,
- BoolOr => Bool,
- BoolEQ => Bool,
- BoolNE => Bool,
- NaturalPlus => Natural,
- NaturalTimes => Natural,
- TextAppend => Text,
- _ => panic!("Unimplemented typecheck case: {:?}", e),
- });
-
- ensure_equal(tl.as_ref(), &t, mkerr, || {
- BinOpTypeMismatch(o, l.clone(), tl.clone())
- })?;
-
- ensure_equal(tr.as_ref(), &t, mkerr, || {
- BinOpTypeMismatch(o, r.clone(), tr.clone())
- })?;
-
- Ok(t)
+ TextLit(_) => Ok(RetExpr(dhall::expr!(Text))),
+ BinOp(o, l, r) => {
+ let t = mktype(
+ ctx,
+ match o {
+ BoolAnd => dhall::subexpr!(Bool),
+ BoolOr => dhall::subexpr!(Bool),
+ BoolEQ => dhall::subexpr!(Bool),
+ BoolNE => dhall::subexpr!(Bool),
+ NaturalPlus => dhall::subexpr!(Natural),
+ NaturalTimes => dhall::subexpr!(Natural),
+ TextAppend => dhall::subexpr!(Text),
+ _ => panic!("Unimplemented typecheck case: {:?}", e),
+ },
+ )?;
+
+ ensure_equal!(l.get_type(), t, mkerr(BinOpTypeMismatch(o, l)));
+
+ ensure_equal!(r.get_type(), t, mkerr(BinOpTypeMismatch(o, r)));
+
+ Ok(RetType(t))
}
Embed(p) => match p {},
_ => panic!("Unimplemented typecheck case: {:?}", e),
},
}?;
- Ok(rc(ret))
+ match ret {
+ RetExpr(ret) => Ok(Typed(e, mktype(ctx, rc(ret))?)),
+ RetType(typ) => Ok(Typed(e, typ)),
+ }
}
/// `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<S: ::std::fmt::Debug + Clone>(
- e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>> {
+pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
+ let e = type_of_(e)?;
+ Ok(e.get_type_move().into_normalized()?.into_expr())
+}
+
+pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
let ctx = Context::new();
- type_with(&ctx, e) //.map(|e| e.into_owned())
+ let e = type_with(&ctx, e)?;
+ // Ensure the inferred type isn't UNTYPE
+ e.get_type().as_normalized()?;
+ Ok(e)
}
/// The specific type error
#[derive(Debug)]
pub enum TypeMessage<S> {
UnboundVariable,
- InvalidInputType(SubExpr<S, X>),
- InvalidOutputType(SubExpr<S, X>),
- NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
- TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
- AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+ InvalidInputType(Normalized),
+ InvalidOutputType(Normalized),
+ NotAFunction(Typed),
+ TypeMismatch(Typed, Normalized, Typed),
+ AnnotMismatch(Typed, Normalized),
Untyped,
- InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
- InvalidListType(SubExpr<S, X>),
- InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
- InvalidOptionalLiteral(usize),
- InvalidOptionalType(SubExpr<S, X>),
- InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
- IfBranchMismatch(
- SubExpr<S, X>,
- SubExpr<S, X>,
- SubExpr<S, X>,
- SubExpr<S, X>,
- ),
- IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
- InvalidField(Label, SubExpr<S, X>),
- InvalidFieldType(Label, SubExpr<S, X>),
- InvalidAlternative(Label, SubExpr<S, X>),
- InvalidAlternativeType(Label, SubExpr<S, X>),
+ InvalidListElement(usize, Normalized, Typed),
+ InvalidListType(Normalized),
+ InvalidOptionalType(Normalized),
+ InvalidPredicate(Typed),
+ IfBranchMismatch(Typed, Typed),
+ IfBranchMustBeTerm(bool, Typed),
+ InvalidField(Label, Typed),
+ InvalidFieldType(Label, Typed),
DuplicateAlternative(Label),
- MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
FieldCollision(Label),
- MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
- MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
- UnusedHandler(HashSet<Label>),
- MissingHandler(HashSet<Label>),
- HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
- HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
- HandlerNotAFunction(Label, SubExpr<S, X>),
- NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
- MissingField(Label, SubExpr<S, X>),
- BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
- NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
- NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
+ NotARecord(Label, Typed),
+ MissingField(Label, Typed),
+ BinOpTypeMismatch(BinOp, Typed),
+ NoDependentLet(Normalized, Normalized),
+ NoDependentTypes(Normalized, Normalized),
+ MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
}
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<S> {
- pub context: Context<Label, SubExpr<S, X>>,
+ pub context: Context<Label, Type>,
pub current: SubExpr<S, X>,
pub type_message: TypeMessage<S>,
}
impl<S> TypeError<S> {
pub fn new(
- context: &Context<Label, SubExpr<S, X>>,
+ context: &Context<Label, Type>,
current: SubExpr<S, X>,
type_message: TypeMessage<S>,
) -> Self {
@@ -533,8 +672,8 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
UnboundVariable => "Unbound variable",
InvalidInputType(_) => "Invalid function input",
InvalidOutputType(_) => "Invalid function output",
- NotAFunction(_, _) => "Not a function",
- TypeMismatch(_, _, _, _) => "Wrong type of function argument",
+ NotAFunction(_) => "Not a function",
+ TypeMismatch(_, _, _) => "Wrong type of function argument",
_ => "Unhandled error",
}
}
@@ -546,13 +685,19 @@ impl<S> fmt::Display for TypeMessage<S> {
UnboundVariable => {
f.write_str(include_str!("errors/UnboundVariable.txt"))
}
- TypeMismatch(e0, e1, e2, e3) => {
+ TypeMismatch(e0, e1, e2) => {
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));
+ .replace("$txt0", &format!("{}", e0.as_expr()))
+ .replace("$txt1", &format!("{}", e1.as_expr()))
+ .replace("$txt2", &format!("{}", e2.as_expr()))
+ .replace(
+ "$txt3",
+ &format!(
+ "{}",
+ e2.get_type().as_normalized().unwrap().as_expr()
+ ),
+ );
f.write_str(&s)
}
_ => f.write_str("Unhandled error message"),
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index 397a8ee..5f16d2c 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -44,14 +44,21 @@ pub enum Feature {
TypeInferenceFailure,
}
-pub fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, DhallError> {
- load_dhall_file(&PathBuf::from(file_path), true)
+// Deprecated
+fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, ImportError> {
+ dhall::load_dhall_file(&PathBuf::from(file_path), true)
}
-pub fn read_dhall_file_no_resolve_imports<'i>(
+fn load_from_file_str<'i>(
file_path: &str,
-) -> Result<ParsedExpr, DhallError> {
- load_dhall_file_no_resolve_imports(&PathBuf::from(file_path))
+) -> Result<dhall::expr::Parsed, ImportError> {
+ dhall::expr::Parsed::load_from_file(&PathBuf::from(file_path))
+}
+
+fn load_from_binary_file_str<'i>(
+ file_path: &str,
+) -> Result<dhall::expr::Parsed, ImportError> {
+ dhall::expr::Parsed::load_from_binary_file(&PathBuf::from(file_path))
}
pub fn run_test(base_path: &str, feature: Feature) {
@@ -71,63 +78,99 @@ pub fn run_test(base_path: &str, feature: Feature) {
ParserSuccess => {
let expr_file_path = base_path.clone() + "A.dhall";
let expected_file_path = base_path + "B.dhallb";
- let expr = read_dhall_file_no_resolve_imports(&expr_file_path)
+ let expr = load_from_file_str(&expr_file_path)
.map_err(|e| println!("{}", e))
.unwrap();
- use std::fs::File;
- use std::io::Read;
- let mut file = File::open(expected_file_path).unwrap();
- let mut data = Vec::new();
- file.read_to_end(&mut data).unwrap();
- let expected = dhall::binary::decode(&data).unwrap();
+ let expected = load_from_binary_file_str(&expected_file_path)
+ .map_err(|e| println!("{}", e))
+ .unwrap();
assert_eq_pretty!(expr, expected);
// Round-trip pretty-printer
- let expr = parse_expr(&expr.to_string()).unwrap();
+ let expr =
+ dhall::expr::Parsed::load_from_str(&expr.to_string()).unwrap();
assert_eq!(expr, expected);
}
ParserFailure => {
let file_path = base_path + ".dhall";
- let err =
- read_dhall_file_no_resolve_imports(&file_path).unwrap_err();
+ let err = load_from_file_str(&file_path).unwrap_err();
match err {
- DhallError::ParseError(_) => {}
+ ImportError::ParseError(_) => {}
e => panic!("Expected parse error, got: {:?}", e),
}
}
Normalization => {
let expr_file_path = base_path.clone() + "A.dhall";
let expected_file_path = base_path + "B.dhall";
- let expr = rc(read_dhall_file(&expr_file_path).unwrap());
- let expected = rc(read_dhall_file(&expected_file_path).unwrap());
+ let expr = load_from_file_str(&expr_file_path)
+ .unwrap()
+ .resolve()
+ .unwrap()
+ .skip_typecheck()
+ .normalize();
+ let expected = load_from_file_str(&expected_file_path)
+ .unwrap()
+ .resolve()
+ .unwrap()
+ .skip_typecheck()
+ .normalize();
- assert_eq_display!(normalize(expr), normalize(expected));
+ assert_eq_display!(expr, expected);
}
TypecheckFailure => {
let file_path = base_path + ".dhall";
- let expr = rc(read_dhall_file(&file_path).unwrap());
- typecheck::type_of(expr).unwrap_err();
+ load_from_file_str(&file_path)
+ .unwrap()
+ .skip_resolve()
+ .unwrap()
+ .typecheck()
+ .unwrap_err();
}
TypecheckSuccess => {
- let expr_file_path = base_path.clone() + "A.dhall";
- let expected_file_path = base_path + "B.dhall";
- let expr = rc(read_dhall_file(&expr_file_path).unwrap());
- let expected = rc(read_dhall_file(&expected_file_path).unwrap());
- typecheck::type_of(rc(ExprF::Annot(expr, expected))).unwrap();
+ // Many tests stack overflow in debug mode
+ std::thread::Builder::new()
+ .stack_size(4 * 1024 * 1024)
+ .spawn(|| {
+ let expr_file_path = base_path.clone() + "A.dhall";
+ let expected_file_path = base_path + "B.dhall";
+ let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+ let expected =
+ rc(read_dhall_file(&expected_file_path).unwrap());
+ typecheck::type_of(dhall::subexpr!(expr: expected))
+ .unwrap();
+ })
+ .unwrap()
+ .join()
+ .unwrap();
}
TypeInferenceFailure => {
let file_path = base_path + ".dhall";
- let expr = rc(read_dhall_file(&file_path).unwrap());
- typecheck::type_of(expr).unwrap_err();
+ load_from_file_str(&file_path)
+ .unwrap()
+ .skip_resolve()
+ .unwrap()
+ .typecheck()
+ .unwrap_err();
}
TypeInferenceSuccess => {
let expr_file_path = base_path.clone() + "A.dhall";
let expected_file_path = base_path + "B.dhall";
- let expr = rc(read_dhall_file(&expr_file_path).unwrap());
- let expected = rc(read_dhall_file(&expected_file_path).unwrap());
- assert_eq_display!(typecheck::type_of(expr).unwrap(), expected);
+ let expr = load_from_file_str(&expr_file_path)
+ .unwrap()
+ .skip_resolve()
+ .unwrap()
+ .typecheck()
+ .unwrap();
+ let ty = expr.get_type().as_normalized().unwrap();
+ let expected = load_from_file_str(&expected_file_path)
+ .unwrap()
+ .skip_resolve()
+ .unwrap()
+ .skip_typecheck()
+ .skip_normalize();
+ assert_eq_display!(ty, &expected);
}
}
}
diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs
index 5ecc02f..a36a6ac 100644
--- a/dhall/tests/normalization.rs
+++ b/dhall/tests/normalization.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;
diff --git a/dhall/tests/parser.rs b/dhall/tests/parser.rs
index 0b5e2d6..3969dc9 100644
--- a/dhall/tests/parser.rs
+++ b/dhall/tests/parser.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;
diff --git a/dhall/tests/dhall_type.rs b/dhall/tests/traits.rs
index 941e3a4..ac6b5e6 100644
--- a/dhall/tests/dhall_type.rs
+++ b/dhall/tests/traits.rs
@@ -1,5 +1,5 @@
#![feature(proc_macro_hygiene)]
-use dhall::Type;
+use dhall::StaticType;
use dhall_generator::dhall_expr;
#[test]
@@ -11,18 +11,18 @@ fn test_dhall_type() {
dhall_expr!({ _1: Bool, _2: Optional Text })
);
- #[derive(dhall::Type)]
+ #[derive(dhall::StaticType)]
#[allow(dead_code)]
struct A {
field1: bool,
field2: Option<bool>,
}
assert_eq!(
- <A as dhall::Type>::get_type(),
+ <A as dhall::StaticType>::get_type(),
dhall_expr!({ field1: Bool, field2: Optional Bool })
);
- #[derive(Type)]
+ #[derive(StaticType)]
#[allow(dead_code)]
struct B<'a, T: 'a> {
field1: &'a T,
@@ -30,12 +30,12 @@ fn test_dhall_type() {
}
assert_eq!(<B<'static, bool>>::get_type(), A::get_type());
- #[derive(Type)]
+ #[derive(StaticType)]
#[allow(dead_code)]
struct C<T>(T, Option<String>);
assert_eq!(<C<bool>>::get_type(), <(bool, Option<String>)>::get_type());
- #[derive(Type)]
+ #[derive(StaticType)]
#[allow(dead_code)]
struct D();
assert_eq!(
@@ -43,7 +43,7 @@ fn test_dhall_type() {
dhall_expr!({ _1: {}, _2: Optional Text })
);
- #[derive(Type)]
+ #[derive(StaticType)]
#[allow(dead_code)]
enum E<T> {
A(T),
diff --git a/dhall/tests/typecheck.rs b/dhall/tests/typecheck.rs
index 367765c..8d72313 100644
--- a/dhall/tests/typecheck.rs
+++ b/dhall/tests/typecheck.rs
@@ -1,3 +1,4 @@
+#![feature(proc_macro_hygiene)]
#![feature(custom_inner_attributes)]
#![rustfmt::skip]
mod common;
@@ -7,11 +8,11 @@ macro_rules! tc_success {
make_spec_test!(TypecheckSuccess, $name, $path);
};
}
-macro_rules! tc_failure {
- ($name:ident, $path:expr) => {
- make_spec_test!(TypecheckFailure, $name, $path);
- };
-}
+// macro_rules! tc_failure {
+// ($name:ident, $path:expr) => {
+// make_spec_test!(TypecheckFailure, $name, $path);
+// };
+// }
macro_rules! ti_success {
($name:ident, $path:expr) => {
@@ -176,7 +177,7 @@ tc_success!(spec_typecheck_success_prelude_Text_concat_1, "prelude/Text/concat/1
// tc_failure!(spec_typecheck_failure_combineMixedRecords, "combineMixedRecords");
// tc_failure!(spec_typecheck_failure_duplicateFields, "duplicateFields");
-tc_failure!(spec_typecheck_failure_hurkensParadox, "hurkensParadox");
+// tc_failure!(spec_typecheck_failure_hurkensParadox, "hurkensParadox");
// ti_success!(spec_typeinference_success_simple_alternativesAreTypes, "simple/alternativesAreTypes");
// ti_success!(spec_typeinference_success_simple_kindParameter, "simple/kindParameter");
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index a56c5a3..89506ec 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -68,6 +68,7 @@ impl From<NaiveDouble> for f64 {
pub enum Const {
Type,
Kind,
+ Sort,
}
/// Bound variable
@@ -285,6 +286,28 @@ impl<S, A> Expr<S, A> {
self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone())
}
+ #[inline(always)]
+ pub fn traverse_embed<B, Err, F>(
+ &self,
+ map_embed: &F,
+ ) -> Result<Expr<S, B>, Err>
+ where
+ S: Clone,
+ B: Clone,
+ F: Fn(&A) -> Result<B, Err>,
+ {
+ let recurse = |e: &SubExpr<S, A>| -> Result<SubExpr<S, B>, Err> {
+ Ok(e.as_ref().traverse_embed(map_embed)?.roll())
+ };
+ self.as_ref().traverse(
+ |e| recurse(e),
+ |_, e| recurse(e),
+ |x| Ok(S::clone(x)),
+ map_embed,
+ |x| Ok(Label::clone(x)),
+ )
+ }
+
pub fn map_label<F>(&self, map_label: &F) -> Self
where
A: Clone,
@@ -319,6 +342,23 @@ impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> {
}
}
+impl<S: Clone, A: Clone> Expr<S, SubExpr<S, A>> {
+ pub fn squash_embed(&self) -> SubExpr<S, A> {
+ match self.as_ref() {
+ ExprF::Embed(e) => e.clone(),
+ e => e
+ .map(
+ |e| e.as_ref().squash_embed(),
+ |_, e| e.as_ref().squash_embed(),
+ S::clone,
+ |_| unreachable!(),
+ Label::clone,
+ )
+ .roll(),
+ }
+ }
+}
+
impl<SE, L, N, E> ExprF<SE, L, N, E> {
#[inline(always)]
pub fn as_ref(&self) -> ExprF<&SE, &L, &N, &E>
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 67bcf77..41a2ce7 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -764,6 +764,7 @@ make_parser! {
"False" => BoolLit(false),
"Type" => Const(crate::Const::Type),
"Kind" => Const(crate::Const::Kind),
+ "Sort" => Const(crate::Const::Sort),
_ => Var(V(l, idx)),
}
}
@@ -777,6 +778,7 @@ make_parser! {
"False" => BoolLit(false),
"Type" => Const(crate::Const::Type),
"Kind" => Const(crate::Const::Kind),
+ "Sort" => Const(crate::Const::Sort),
_ => Var(V(l, 0)),
}
}
diff --git a/dhall_generator/src/dhall_type.rs b/dhall_generator/src/derive.rs
index 3b1d1c9..159ff5c 100644
--- a/dhall_generator/src/dhall_type.rs
+++ b/dhall_generator/src/derive.rs
@@ -44,11 +44,11 @@ pub fn derive_for_struct(
.map(|(name, ty)| {
let name = dhall_core::Label::from(name);
constraints.push(ty.clone());
- (name, quote!(<#ty as dhall::Type>::get_type()))
+ (name, quote!(<#ty as dhall::StaticType>::get_type()))
})
.collect();
let record =
- crate::dhall_expr::quote_exprf(dhall_core::ExprF::RecordType(fields));
+ crate::quote::quote_exprf(dhall_core::ExprF::RecordType(fields));
Ok(quote! { dhall_core::rc(#record) })
}
@@ -88,12 +88,12 @@ pub fn derive_for_enum(
};
let ty = ty?;
constraints.push(ty.clone());
- Ok((name, quote!(<#ty as dhall::Type>::get_type())))
+ Ok((name, quote!(<#ty as dhall::StaticType>::get_type())))
})
.collect::<Result<_, Error>>()?;
let union =
- crate::dhall_expr::quote_exprf(dhall_core::ExprF::UnionType(variants));
+ crate::quote::quote_exprf(dhall_core::ExprF::UnionType(variants));
Ok(quote! { dhall_core::rc(#union) })
}
@@ -136,7 +136,7 @@ pub fn derive_type_inner(
let mut local_where_clause = orig_where_clause.clone();
local_where_clause
.predicates
- .push(parse_quote!(#ty: dhall::Type));
+ .push(parse_quote!(#ty: dhall::StaticType));
let phantoms = generics.params.iter().map(|param| match param {
syn::GenericParam::Type(syn::TypeParam { ident, .. }) => {
quote!(#ident)
@@ -156,12 +156,14 @@ pub fn derive_type_inner(
// Ensure that all the fields have a Type impl
let mut where_clause = orig_where_clause.clone();
for ty in constraints.iter() {
- where_clause.predicates.push(parse_quote!(#ty: dhall::Type));
+ where_clause
+ .predicates
+ .push(parse_quote!(#ty: dhall::StaticType));
}
let ident = &input.ident;
let tokens = quote! {
- impl #impl_generics dhall::Type for #ident #ty_generics
+ impl #impl_generics dhall::StaticType for #ident #ty_generics
#where_clause {
fn get_type() -> dhall_core::DhallExpr {
#(#assertions)*
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index f31faa4..b422834 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -1,7 +1,7 @@
extern crate proc_macro;
-mod dhall_expr;
-mod dhall_type;
+mod derive;
+mod quote;
use proc_macro::TokenStream;
@@ -13,15 +13,15 @@ pub fn dhall_expr(input: TokenStream) -> TokenStream {
#[proc_macro]
pub fn expr(input: TokenStream) -> TokenStream {
- dhall_expr::expr(input)
+ quote::expr(input)
}
#[proc_macro]
pub fn subexpr(input: TokenStream) -> TokenStream {
- dhall_expr::subexpr(input)
+ quote::subexpr(input)
}
-#[proc_macro_derive(Type)]
+#[proc_macro_derive(StaticType)]
pub fn derive_type(input: TokenStream) -> TokenStream {
- dhall_type::derive_type(input)
+ derive::derive_type(input)
}
diff --git a/dhall_generator/src/dhall_expr.rs b/dhall_generator/src/quote.rs
index d0c5733..8fce89d 100644
--- a/dhall_generator/src/dhall_expr.rs
+++ b/dhall_generator/src/quote.rs
@@ -63,6 +63,9 @@ where
let a = quote_vec(a);
quote! { dhall_core::ExprF::App(#f, #a) }
}
+ Annot(x, t) => {
+ quote! { dhall_core::ExprF::Annot(#x, #t) }
+ }
Const(c) => {
let c = quote_const(c);
quote! { dhall_core::ExprF::Const(#c) }
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 16:51:23 +0000