summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril Feneanar2020-02-19 17:25:57 +0000
committerGitHub2020-02-19 17:25:57 +0000
commitffbde252a850c7d96e1000e1be52792c41733a28 (patch)
treee668b7f764fb4981a802bc619e0b2ff62fa9ce16 /dhall
parente4b3a879907b6dcc75d25847ae21a23d0201aae1 (diff)
parent7cbfc1a0d32766a383d1f48902502adaa2234d2f (diff)
Merge pull request #131 from Nadrieril/hir
Decouple main expression types
Diffstat (limited to '')
-rw-r--r--dhall/build.rs3
-rw-r--r--dhall/src/error/mod.rs57
-rw-r--r--dhall/src/lib.rs128
-rw-r--r--dhall/src/semantics/builtins.rs267
-rw-r--r--dhall/src/semantics/mod.rs1
-rw-r--r--dhall/src/semantics/nze/env.rs54
-rw-r--r--dhall/src/semantics/nze/mod.rs4
-rw-r--r--dhall/src/semantics/nze/nir.rs510
-rw-r--r--dhall/src/semantics/nze/normalize.rs413
-rw-r--r--dhall/src/semantics/nze/value.rs666
-rw-r--r--dhall/src/semantics/nze/var.rs2
-rw-r--r--dhall/src/semantics/resolve.rs181
-rw-r--r--dhall/src/semantics/resolve/env.rs104
-rw-r--r--dhall/src/semantics/resolve/hir.rs135
-rw-r--r--dhall/src/semantics/resolve/mod.rs6
-rw-r--r--dhall/src/semantics/resolve/resolve.rs231
-rw-r--r--dhall/src/semantics/tck/env.rs87
-rw-r--r--dhall/src/semantics/tck/mod.rs4
-rw-r--r--dhall/src/semantics/tck/tir.rs175
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs137
-rw-r--r--dhall/src/semantics/tck/typecheck.rs670
-rw-r--r--dhall/src/syntax/ast/expr.rs140
-rw-r--r--dhall/src/syntax/ast/import.rs24
-rw-r--r--dhall/src/syntax/ast/visitor.rs397
-rw-r--r--dhall/src/syntax/binary/decode.rs20
-rw-r--r--dhall/src/syntax/binary/encode.rs53
-rw-r--r--dhall/src/syntax/text/parser.rs21
-rw-r--r--dhall/src/syntax/text/printer.rs47
-rw-r--r--dhall/src/tests.rs24
-rw-r--r--dhall/tests/import/failure/cycle.txt2
-rw-r--r--dhall/tests/import/failure/importBoundary.txt8
-rw-r--r--dhall/tests/type-inference/failure/SortInLet.txt7
-rw-r--r--dhall/tests/type-inference/failure/hurkensParadox.txt8
-rw-r--r--dhall/tests/type-inference/failure/recordOfKind.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/Sort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt4
55 files changed, 2227 insertions, 2474 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index 8deb637..7c62083 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -299,9 +299,6 @@ fn generate_tests() -> std::io::Result<()> {
|| path == "unit/RecursiveRecordMergeWithinFieldSelection0"
|| path == "unit/RecursiveRecordMergeWithinFieldSelection2"
|| path == "unit/RecursiveRecordMergeWithinFieldSelection3"
- // TODO: record completion
- || path == "simple/completion"
- || path == "unit/Completion"
}),
input_type: FileType::Text,
output_type: Some(FileType::Text),
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13b61fa..8829d47 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -2,7 +2,6 @@ use std::io::Error as IOError;
use crate::semantics::resolve::ImportStack;
use crate::syntax::{Import, ParseError};
-use crate::NormalizedExpr;
mod builder;
pub(crate) use builder::*;
@@ -10,8 +9,13 @@ pub(crate) use builder::*;
pub type Result<T> = std::result::Result<T, Error>;
#[derive(Debug)]
+pub struct Error {
+ kind: ErrorKind,
+}
+
+#[derive(Debug)]
#[non_exhaustive]
-pub enum Error {
+pub(crate) enum ErrorKind {
IO(IOError),
Parse(ParseError),
Decode(DecodeError),
@@ -21,10 +25,9 @@ pub enum Error {
}
#[derive(Debug)]
-pub enum ImportError {
- Recursive(Import<NormalizedExpr>, Box<Error>),
- UnexpectedImport(Import<NormalizedExpr>),
- ImportCycle(ImportStack, Import<NormalizedExpr>),
+pub(crate) enum ImportError {
+ UnexpectedImport(Import<()>),
+ ImportCycle(ImportStack, Import<()>),
}
#[derive(Debug)]
@@ -47,10 +50,18 @@ pub struct TypeError {
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage {
- Sort,
Custom(String),
}
+impl Error {
+ pub(crate) fn new(kind: ErrorKind) -> Self {
+ Error { kind }
+ }
+ pub(crate) fn kind(&self) -> &ErrorKind {
+ &self.kind
+ }
+}
+
impl TypeError {
pub(crate) fn new(message: TypeMessage) -> Self {
TypeError { message }
@@ -61,7 +72,6 @@ impl std::fmt::Display for TypeError {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
use TypeMessage::*;
let msg = match &self.message {
- Sort => format!("Type error: Unhandled error: {:?}", self.message),
Custom(s) => format!("Type error: {}", s),
};
write!(f, "{}", msg)
@@ -72,45 +82,50 @@ impl std::error::Error for TypeError {}
impl std::fmt::Display for Error {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
- match self {
- Error::IO(err) => write!(f, "{}", err),
- Error::Parse(err) => write!(f, "{}", err),
- Error::Decode(err) => write!(f, "{:?}", err),
- Error::Encode(err) => write!(f, "{:?}", err),
- Error::Resolve(err) => write!(f, "{:?}", err),
- Error::Typecheck(err) => write!(f, "{}", err),
+ match &self.kind {
+ ErrorKind::IO(err) => write!(f, "{}", err),
+ ErrorKind::Parse(err) => write!(f, "{}", err),
+ ErrorKind::Decode(err) => write!(f, "{:?}", err),
+ ErrorKind::Encode(err) => write!(f, "{:?}", err),
+ ErrorKind::Resolve(err) => write!(f, "{:?}", err),
+ ErrorKind::Typecheck(err) => write!(f, "{}", err),
}
}
}
impl std::error::Error for Error {}
+impl From<ErrorKind> for Error {
+ fn from(kind: ErrorKind) -> Error {
+ Error::new(kind)
+ }
+}
impl From<IOError> for Error {
fn from(err: IOError) -> Error {
- Error::IO(err)
+ ErrorKind::IO(err).into()
}
}
impl From<ParseError> for Error {
fn from(err: ParseError) -> Error {
- Error::Parse(err)
+ ErrorKind::Parse(err).into()
}
}
impl From<DecodeError> for Error {
fn from(err: DecodeError) -> Error {
- Error::Decode(err)
+ ErrorKind::Decode(err).into()
}
}
impl From<EncodeError> for Error {
fn from(err: EncodeError) -> Error {
- Error::Encode(err)
+ ErrorKind::Encode(err).into()
}
}
impl From<ImportError> for Error {
fn from(err: ImportError) -> Error {
- Error::Resolve(err)
+ ErrorKind::Resolve(err).into()
}
}
impl From<TypeError> for Error {
fn from(err: TypeError) -> Error {
- Error::Typecheck(err)
+ ErrorKind::Typecheck(err).into()
}
}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index d8eeb4a..9922144 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -18,18 +18,20 @@ pub mod syntax;
use std::fmt::Display;
use std::path::Path;
-use crate::error::{EncodeError, Error, ImportError, TypeError};
+use crate::error::{EncodeError, Error, TypeError};
use crate::semantics::parse;
use crate::semantics::resolve;
use crate::semantics::resolve::ImportRoot;
-use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind};
+use crate::semantics::{
+ typecheck, typecheck_with, Hir, Nir, NirKind, Tir, Type,
+};
use crate::syntax::binary;
-use crate::syntax::{Builtin, Const, Expr};
+use crate::syntax::{Builtin, Expr};
-pub type ParsedExpr = Expr<Normalized>;
-pub type DecodedExpr = Expr<Normalized>;
-pub type ResolvedExpr = Expr<Normalized>;
-pub type NormalizedExpr = Expr<Normalized>;
+pub type ParsedExpr = Expr;
+pub type DecodedExpr = Expr;
+pub type ResolvedExpr = Expr;
+pub type NormalizedExpr = Expr;
#[derive(Debug, Clone)]
pub struct Parsed(ParsedExpr, ImportRoot);
@@ -38,25 +40,26 @@ pub struct Parsed(ParsedExpr, ImportRoot);
///
/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
#[derive(Debug, Clone)]
-pub struct Resolved(ResolvedExpr);
+pub struct Resolved(Hir);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(TyExpr);
+pub struct Typed {
+ hir: Hir,
+ ty: Type,
+}
/// A normalized expression.
///
-/// Invariant: the contained Typed expression must be in normal form,
+/// Invariant: the contained expression must be in normal form,
#[derive(Debug, Clone)]
-pub struct Normalized(Value);
+pub struct Normalized(Nir);
-/// Controls conversion from `Value` to `Expr`
+/// Controls conversion from `Nir` to `Expr`
#[derive(Copy, Clone)]
pub(crate) struct ToExprOptions {
/// Whether to convert all variables to `_`
pub(crate) alpha: bool,
- /// Whether to normalize before converting
- pub(crate) normalize: bool,
}
impl Parsed {
@@ -73,11 +76,11 @@ impl Parsed {
parse::parse_binary(data)
}
- pub fn resolve(self) -> Result<Resolved, ImportError> {
+ pub fn resolve(self) -> Result<Resolved, Error> {
resolve::resolve(self)
}
- pub fn skip_resolve(self) -> Result<Resolved, ImportError> {
- resolve::skip_resolve_expr(self)
+ pub fn skip_resolve(self) -> Result<Resolved, Error> {
+ Ok(Resolved(resolve::skip_resolve(&self.0)?))
}
pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
@@ -92,33 +95,39 @@ impl Parsed {
impl Resolved {
pub fn typecheck(&self) -> Result<Typed, TypeError> {
- Ok(Typed(typecheck(&self.0)?))
+ Ok(Typed::from_tir(typecheck(&self.0)?))
}
pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> {
- Ok(Typed(typecheck_with(&self.0, ty.to_expr())?))
+ Ok(Typed::from_tir(typecheck_with(&self.0, ty.to_hir())?))
}
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> ResolvedExpr {
- self.0.clone()
+ self.0.to_expr_noopts()
}
}
impl Typed {
+ fn from_tir(tir: Tir<'_>) -> Self {
+ Typed {
+ hir: tir.as_hir().clone(),
+ ty: tir.ty().clone(),
+ }
+ }
/// Reduce an expression to its normal form, performing beta reduction
pub fn normalize(&self) -> Normalized {
- Normalized(self.0.rec_eval_closed_expr())
+ Normalized(self.hir.rec_eval_closed_expr())
}
/// Converts a value back to the corresponding AST expression.
fn to_expr(&self) -> ResolvedExpr {
- self.0.to_expr(ToExprOptions {
- alpha: false,
- normalize: false,
- })
+ self.hir.to_expr(ToExprOptions { alpha: false })
}
+ pub(crate) fn ty(&self) -> &Type {
+ &self.ty
+ }
pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
- Ok(Normalized(self.0.get_type()?))
+ Ok(Normalized(self.ty.clone().into_nir()))
}
}
@@ -129,71 +138,55 @@ impl Normalized {
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> NormalizedExpr {
- self.0.to_expr(ToExprOptions {
- alpha: false,
- normalize: false,
- })
+ self.0.to_expr(ToExprOptions { alpha: false })
+ }
+ /// Converts a value back to the corresponding Hir expression.
+ pub(crate) fn to_hir(&self) -> Hir {
+ self.0.to_hir_noenv()
}
/// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
- self.0.to_expr(ToExprOptions {
- alpha: true,
- normalize: false,
- })
+ self.0.to_expr(ToExprOptions { alpha: true })
}
- pub(crate) fn to_value(&self) -> Value {
+ pub(crate) fn to_nir(&self) -> Nir {
self.0.clone()
}
- pub(crate) fn into_value(self) -> Value {
+ pub(crate) fn into_nir(self) -> Nir {
self.0
}
- pub(crate) fn from_const(c: Const) -> Self {
- Normalized(Value::from_const(c))
+ pub(crate) fn from_kind(v: NirKind) -> Self {
+ Normalized(Nir::from_kind(v))
}
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self {
- Normalized(Value::from_kind_and_type(v, t.into_value()))
- }
- pub(crate) fn from_value(th: Value) -> Self {
+ pub(crate) fn from_nir(th: Nir) -> Self {
Normalized(th)
}
- pub(crate) fn const_type() -> Self {
- Normalized::from_const(Const::Type)
- }
pub fn make_builtin_type(b: Builtin) -> Self {
- Normalized::from_value(Value::from_builtin(b))
+ Normalized::from_nir(Nir::from_builtin(b))
}
pub fn make_optional_type(t: Normalized) -> Self {
- Normalized::from_value(
- Value::from_builtin(Builtin::Optional).app(t.to_value()),
+ Normalized::from_nir(
+ Nir::from_builtin(Builtin::Optional).app(t.to_nir()),
)
}
pub fn make_list_type(t: Normalized) -> Self {
- Normalized::from_value(
- Value::from_builtin(Builtin::List).app(t.to_value()),
- )
+ Normalized::from_nir(Nir::from_builtin(Builtin::List).app(t.to_nir()))
}
pub fn make_record_type(
kts: impl Iterator<Item = (String, Normalized)>,
) -> Self {
- Normalized::from_kind_and_type(
- ValueKind::RecordType(
- kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
- ),
- Normalized::const_type(),
- )
+ Normalized::from_kind(NirKind::RecordType(
+ kts.map(|(k, t)| (k.into(), t.into_nir())).collect(),
+ ))
}
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Normalized>)>,
) -> Self {
- Normalized::from_kind_and_type(
- ValueKind::UnionType(
- kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
- .collect(),
- ),
- Normalized::const_type(),
- )
+ Normalized::from_kind(NirKind::UnionType(
+ kts.map(|(k, t)| (k.into(), t.map(|t| t.into_nir())))
+ .collect(),
+ ))
}
}
@@ -219,7 +212,6 @@ macro_rules! derive_traits_for_wrapper_struct {
}
derive_traits_for_wrapper_struct!(Parsed);
-derive_traits_for_wrapper_struct!(Resolved);
impl std::hash::Hash for Normalized {
fn hash<H>(&self, state: &mut H)
@@ -243,6 +235,12 @@ impl From<Normalized> for NormalizedExpr {
}
}
+impl Display for Resolved {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+ self.to_expr().fmt(f)
+ }
+}
+
impl Eq for Typed {}
impl PartialEq for Typed {
fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 907d449..61de0c7 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,11 +1,12 @@
use crate::semantics::{
- typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+ skip_resolve, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
};
use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
- InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V,
+ InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr,
+ V,
};
use crate::Normalized;
use std::collections::HashMap;
@@ -14,32 +15,26 @@ use std::convert::TryInto;
/// A partially applied builtin.
/// Invariant: the evaluation of the given args must not be able to progress further
#[derive(Debug, Clone)]
-pub(crate) struct BuiltinClosure<Value> {
+pub(crate) struct BuiltinClosure<Nir> {
pub env: NzEnv,
pub b: Builtin,
/// Arguments applied to the closure so far.
- pub args: Vec<Value>,
- /// Keeps the types of the partial applications around to be able to convert back to TyExpr.
- /// If the args so far are `x_1`, ..., `x_n`, this contains the types of `b`, `b x1`, ...,
- /// `b x_1 x_2 ... x_(n-1)`.
- pub types: Vec<Value>,
+ pub args: Vec<Nir>,
}
-impl BuiltinClosure<Value> {
+impl BuiltinClosure<Nir> {
pub fn new(b: Builtin, env: NzEnv) -> Self {
BuiltinClosure {
env,
b,
args: Vec::new(),
- types: Vec::new(),
}
}
- pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind {
+ pub fn apply(&self, a: Nir) -> NirKind {
use std::iter::once;
let args = self.args.iter().cloned().chain(once(a.clone())).collect();
- let types = self.types.iter().cloned().chain(once(f_ty)).collect();
- apply_builtin(self.b, args, ret_ty, types, self.env.clone())
+ apply_builtin(self.b, args, self.env.clone())
}
/// This doesn't break the invariant because we already checked that the appropriate arguments
/// did not normalize to something that allows evaluation to proceed.
@@ -48,24 +43,20 @@ impl BuiltinClosure<Value> {
x.normalize();
}
}
- pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind {
- TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold(
+ pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+ HirKind::Expr(self.args.iter().fold(
ExprKind::Builtin(self.b),
- |acc, (v, ty)| {
+ |acc, v| {
ExprKind::App(
- TyExpr::new(
- TyExprKind::Expr(acc),
- Some(ty.clone()),
- Span::Artificial,
- ),
- v.to_tyexpr(venv),
+ Hir::new(HirKind::Expr(acc), Span::Artificial),
+ v.to_hir(venv),
)
},
))
}
}
-pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+pub(crate) fn rc(x: UnspannedExpr) -> Expr {
Expr::new(x, Span::Artificial)
}
@@ -125,9 +116,9 @@ macro_rules! make_type {
};
}
-pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+pub(crate) fn type_of_builtin(b: Builtin) -> Hir {
use Builtin::*;
- match b {
+ let expr = match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
List | Optional => make_type!(
Type -> Type
@@ -210,7 +201,8 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
OptionalNone => make_type!(
forall (A: Type) -> Optional A
),
- }
+ };
+ skip_resolve(&expr).unwrap()
}
// Ad-hoc macro to help construct closures
@@ -249,7 +241,7 @@ macro_rules! make_closure {
rc(ExprKind::BinOp(
BinOp::NaturalPlus,
make_closure!($($v)*),
- rc(ExprKind::NaturalLit(1))
+ rc(ExprKind::Lit(LitKind::Natural(1)))
))
};
([ $($head:tt)* ] # $($tail:tt)*) => {{
@@ -264,148 +256,140 @@ macro_rules! make_closure {
}
#[allow(clippy::cognitive_complexity)]
-fn apply_builtin(
- b: Builtin,
- args: Vec<Value>,
- ty: &Value,
- types: Vec<Value>,
- env: NzEnv,
-) -> ValueKind {
- use Builtin::*;
- use ValueKind::*;
+fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
+ use LitKind::{Bool, Double, Integer, Natural};
+ use NirKind::*;
// Small helper enum
enum Ret {
- ValueKind(ValueKind),
- Value(Value),
+ NirKind(NirKind),
+ Nir(Nir),
DoneAsIs,
}
- let make_closure = |e| typecheck(&e).unwrap().eval(&env);
+ let make_closure = |e| {
+ typecheck(&skip_resolve(&e).unwrap())
+ .unwrap()
+ .eval(env.clone())
+ };
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
- (NaturalIsZero, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
+ (Builtin::OptionalNone, [t]) => {
+ Ret::NirKind(EmptyOptionalLit(t.clone()))
+ }
+ (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))),
_ => Ret::DoneAsIs,
},
- (NaturalEven, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
+ (Builtin::NaturalEven, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))),
_ => Ret::DoneAsIs,
},
- (NaturalOdd, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
+ (Builtin::NaturalOdd, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))),
_ => Ret::DoneAsIs,
},
- (NaturalToInteger, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
+ (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))),
_ => Ret::DoneAsIs,
},
- (NaturalShow, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::Value(Value::from_text(n)),
+ (Builtin::NaturalShow, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)),
_ => Ret::DoneAsIs,
},
- (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
- (NaturalLit(a), NaturalLit(b)) => {
- Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
+ (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
+ (Lit(Natural(a)), Lit(Natural(b))) => {
+ Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 })))
}
- (NaturalLit(0), _) => Ret::Value(b.clone()),
- (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
- _ if a == b => Ret::ValueKind(NaturalLit(0)),
+ (Lit(Natural(0)), _) => Ret::Nir(b.clone()),
+ (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+ _ if a == b => Ret::NirKind(Lit(Natural(0))),
_ => Ret::DoneAsIs,
},
- (IntegerShow, [n]) => match &*n.kind() {
- IntegerLit(n) => {
+ (Builtin::IntegerShow, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
let s = if *n < 0 {
n.to_string()
} else {
format!("+{}", n)
};
- Ret::Value(Value::from_text(s))
+ Ret::Nir(Nir::from_text(s))
}
_ => Ret::DoneAsIs,
},
- (IntegerToDouble, [n]) => match &*n.kind() {
- IntegerLit(n) => {
- Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
+ (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
+ Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64))))
}
_ => Ret::DoneAsIs,
},
- (IntegerNegate, [n]) => match &*n.kind() {
- IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+ (Builtin::IntegerNegate, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))),
_ => Ret::DoneAsIs,
},
- (IntegerClamp, [n]) => match &*n.kind() {
- IntegerLit(n) => {
- Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+ (Builtin::IntegerClamp, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
+ Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0))))
}
_ => Ret::DoneAsIs,
},
- (DoubleShow, [n]) => match &*n.kind() {
- DoubleLit(n) => Ret::Value(Value::from_text(n)),
+ (Builtin::DoubleShow, [n]) => match &*n.kind() {
+ Lit(Double(n)) => Ret::Nir(Nir::from_text(n)),
_ => Ret::DoneAsIs,
},
- (TextShow, [v]) => match &*v.kind() {
+ (Builtin::TextShow, [v]) => match &*v.kind() {
TextLit(tlit) => {
if let Some(s) = tlit.as_text() {
// Printing InterpolatedText takes care of all the escaping
let txt: InterpolatedText<Normalized> =
std::iter::once(InterpolatedTextContents::Text(s))
.collect();
- Ret::Value(Value::from_text(txt))
+ Ret::Nir(Nir::from_text(txt))
} else {
Ret::DoneAsIs
}
}
_ => Ret::DoneAsIs,
},
- (ListLength, [_, l]) => match &*l.kind() {
- EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
- NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
+ (Builtin::ListLength, [_, l]) => match &*l.kind() {
+ EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))),
+ NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))),
_ => Ret::DoneAsIs,
},
- (ListHead, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+ (Builtin::ListHead, [_, l]) => match &*l.kind() {
+ EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
+ Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
_ => Ret::DoneAsIs,
},
- (ListLast, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
- NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
+ (Builtin::ListLast, [_, l]) => match &*l.kind() {
+ EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => Ret::NirKind(NEOptionalLit(
xs.iter().rev().next().unwrap().clone(),
)),
_ => Ret::DoneAsIs,
},
- (ListReverse, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
+ (Builtin::ListReverse, [_, l]) => match &*l.kind() {
+ EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
+ Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect()))
}
_ => Ret::DoneAsIs,
},
- (ListIndexed, [_, l]) => {
- let l_whnf = l.kind();
- match &*l_whnf {
+ (Builtin::ListIndexed, [t, l]) => {
+ match l.kind() {
EmptyListLit(_) | NEListLit(_) => {
- // Extract the type of the list elements
- let t = match &*l_whnf {
- EmptyListLit(t) => t.clone(),
- NEListLit(xs) => xs[0].get_type_not_sort(),
- _ => unreachable!(),
- };
-
// Construct the returned record type: { index: Natural, value: t }
let mut kts = HashMap::new();
- kts.insert("index".into(), Value::from_builtin(Natural));
- kts.insert("value".into(), t.clone());
- let t = Value::from_kind_and_type(
- RecordType(kts),
- Value::from_const(Type),
+ kts.insert(
+ "index".into(),
+ Nir::from_builtin(Builtin::Natural),
);
+ kts.insert("value".into(), t.clone());
+ let t = Nir::from_kind(RecordType(kts));
// Construct the new list, with added indices
- let list = match &*l_whnf {
+ let list = match l.kind() {
EmptyListLit(_) => EmptyListLit(t),
NEListLit(xs) => NEListLit(
xs.iter()
@@ -414,31 +398,23 @@ fn apply_builtin(
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_kind_and_type(
- NaturalLit(i),
- Value::from_builtin(
- Builtin::Natural,
- ),
- ),
+ Nir::from_kind(Lit(Natural(i))),
);
kvs.insert("value".into(), e.clone());
- Value::from_kind_and_type(
- RecordLit(kvs),
- t.clone(),
- )
+ Nir::from_kind(RecordLit(kvs))
})
.collect(),
),
_ => unreachable!(),
};
- Ret::ValueKind(list)
+ Ret::NirKind(list)
}
_ => Ret::DoneAsIs,
}
}
- (ListBuild, [t, f]) => {
- let list_t = Value::from_builtin(List).app(t.clone());
- Ret::Value(
+ (Builtin::ListBuild, [t, f]) => {
+ let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
+ Ret::Nir(
f.app(list_t.clone())
.app(
make_closure(make_closure!(
@@ -449,23 +425,24 @@ fn apply_builtin(
))
.app(t.clone()),
)
- .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+ .app(EmptyListLit(t.clone()).into_nir()),
)
}
- (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
- EmptyListLit(_) => Ret::Value(nil.clone()),
+ (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
+ EmptyListLit(_) => Ret::Nir(nil.clone()),
NEListLit(xs) => {
let mut v = nil.clone();
for x in xs.iter().cloned().rev() {
v = cons.app(x).app(v);
}
- Ret::Value(v)
+ Ret::Nir(v)
}
_ => Ret::DoneAsIs,
},
- (OptionalBuild, [t, f]) => {
- let optional_t = Value::from_builtin(Optional).app(t.clone());
- Ret::Value(
+ (Builtin::OptionalBuild, [t, f]) => {
+ let optional_t =
+ Nir::from_builtin(Builtin::Optional).app(t.clone());
+ Ret::Nir(
f.app(optional_t.clone())
.app(
make_closure(make_closure!(
@@ -475,61 +452,47 @@ fn apply_builtin(
))
.app(t.clone()),
)
- .app(
- EmptyOptionalLit(t.clone())
- .into_value_with_type(optional_t),
- ),
+ .app(EmptyOptionalLit(t.clone()).into_nir()),
)
}
- (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
- EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
- NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
+ (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
+ EmptyOptionalLit(_) => Ret::Nir(nothing.clone()),
+ NEOptionalLit(x) => Ret::Nir(just.app(x.clone())),
_ => Ret::DoneAsIs,
},
- (NaturalBuild, [f]) => Ret::Value(
- f.app(Value::from_builtin(Natural))
+ (Builtin::NaturalBuild, [f]) => Ret::Nir(
+ f.app(Nir::from_builtin(Builtin::Natural))
.app(make_closure(make_closure!(
λ(x : Natural) ->
1 + var(x)
)))
- .app(
- NaturalLit(0)
- .into_value_with_type(Value::from_builtin(Natural)),
- ),
+ .app(Lit(Natural(0)).into_nir()),
),
- (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
- NaturalLit(0) => Ret::Value(zero.clone()),
- NaturalLit(n) => {
- let fold = Value::from_builtin(NaturalFold)
- .app(
- NaturalLit(n - 1)
- .into_value_with_type(Value::from_builtin(Natural)),
- )
+ (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
+ Lit(Natural(0)) => Ret::Nir(zero.clone()),
+ Lit(Natural(n)) => {
+ let fold = Nir::from_builtin(Builtin::NaturalFold)
+ .app(Lit(Natural(n - 1)).into_nir())
.app(t.clone())
.app(succ.clone())
.app(zero.clone());
- Ret::Value(succ.app(fold))
+ Ret::Nir(succ.app(fold))
}
_ => Ret::DoneAsIs,
},
_ => Ret::DoneAsIs,
};
match ret {
- Ret::ValueKind(v) => v,
- Ret::Value(v) => v.to_whnf_check_type(ty),
- Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure {
- b,
- args,
- types,
- env,
- }),
+ Ret::NirKind(v) => v,
+ Ret::Nir(v) => v.kind().clone(),
+ Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
}
}
-impl<Value: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Value> {
+impl<Nir: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Nir> {
fn eq(&self, other: &Self) -> bool {
self.b == other.b && self.args == other.args
}
}
-impl<Value: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Value> {}
+impl<Nir: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Nir> {}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 98fdf5a..87033c9 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -5,4 +5,5 @@ pub mod resolve;
pub mod tck;
pub(crate) use self::builtins::*;
pub(crate) use self::nze::*;
+pub(crate) use self::resolve::*;
pub(crate) use self::tck::*;
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..55050ed 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Nir, NirKind};
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum NzVar {
@@ -9,18 +9,20 @@ pub(crate) enum NzVar {
}
#[derive(Debug, Clone)]
-enum NzEnvItem {
+enum EnvItem<Type> {
// Variable is bound with given type
- Kept(Value),
+ Kept(Type),
// Variable has been replaced by corresponding value
- Replaced(Value),
+ Replaced(Nir, Type),
}
#[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
- items: Vec<NzEnvItem>,
+pub(crate) struct ValEnv<Type> {
+ items: Vec<EnvItem<Type>>,
}
+pub(crate) type NzEnv = ValEnv<()>;
+
impl NzVar {
pub fn new(idx: usize) -> Self {
NzVar::Bound(idx)
@@ -44,33 +46,49 @@ impl NzVar {
}
}
-impl NzEnv {
+impl<Type: Clone> ValEnv<Type> {
pub fn new() -> Self {
- NzEnv { items: Vec::new() }
+ ValEnv { items: Vec::new() }
+ }
+ pub fn discard_types(&self) -> ValEnv<()> {
+ let items = self
+ .items
+ .iter()
+ .map(|i| match i {
+ EnvItem::Kept(_) => EnvItem::Kept(()),
+ EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
+ })
+ .collect();
+ ValEnv { items }
}
- pub fn insert_type(&self, t: Value) -> Self {
+ pub fn insert_type(&self, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Kept(t));
+ env.items.push(EnvItem::Kept(ty));
env
}
- pub fn insert_value(&self, e: Value) -> Self {
+ pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Replaced(e));
+ env.items.push(EnvItem::Replaced(e, ty));
env
}
- pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+ pub fn lookup_val(&self, var: &AlphaVar) -> NirKind {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
- NzEnvItem::Replaced(x) => x.kind().clone(),
+ EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
+ EnvItem::Replaced(x, _) => x.kind().clone(),
}
}
- pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+ pub fn lookup_ty(&self, var: &AlphaVar) -> Type {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) => ty.clone(),
- NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+ EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
}
}
}
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+ fn from(x: &'a NzEnv) -> Self {
+ x.clone()
+ }
+}
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 2c8d907..2648339 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,9 +1,9 @@
pub mod env;
pub mod lazy;
+pub mod nir;
pub mod normalize;
-pub mod value;
pub mod var;
pub(crate) use env::*;
+pub(crate) use nir::*;
pub(crate) use normalize::*;
-pub(crate) use value::*;
pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
new file mode 100644
index 0000000..4ed66b7
--- /dev/null
+++ b/dhall/src/semantics/nze/nir.rs
@@ -0,0 +1,510 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::semantics::nze::lazy;
+use crate::semantics::{
+ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+ BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+};
+use crate::syntax::{
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+ Span,
+};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+/// Stands for "Normalized intermediate representation"
+#[derive(Clone)]
+pub(crate) struct Nir(Rc<NirInternal>);
+
+#[derive(Debug)]
+struct NirInternal {
+ kind: lazy::Lazy<Thunk, NirKind>,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+pub(crate) enum Thunk {
+ /// A completely unnormalized expression.
+ Thunk { env: NzEnv, body: Hir },
+ /// A partially normalized expression that may need to go through `normalize_one_layer`.
+ PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+ /// Normal closure
+ Closure { env: NzEnv, body: Hir },
+ /// Closure that ignores the argument passed
+ ConstantClosure { body: Nir },
+}
+
+/// A text literal with interpolations.
+// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
+// text values must be merged.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
+
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Nirs in a NirKind are in WHNF, and recursively so, then the NirKind is in
+/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
+/// if we have the first constructor of the NF at all levels, we actually have the NF.
+/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Nir`s to get to the NF.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum NirKind {
+ /// Closures
+ LamClosure {
+ binder: Binder,
+ annot: Nir,
+ closure: Closure,
+ },
+ PiClosure {
+ binder: Binder,
+ annot: Nir,
+ closure: Closure,
+ },
+ AppliedBuiltin(BuiltinClosure<Nir>),
+
+ Var(NzVar),
+ Const(Const),
+ Lit(LitKind),
+ EmptyOptionalLit(Nir),
+ NEOptionalLit(Nir),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ EmptyListLit(Nir),
+ NEListLit(Vec<Nir>),
+ RecordType(HashMap<Label, Nir>),
+ RecordLit(HashMap<Label, Nir>),
+ UnionType(HashMap<Label, Option<Nir>>),
+ UnionConstructor(Label, HashMap<Label, Option<Nir>>),
+ UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
+ TextLit(TextLit),
+ Equivalence(Nir, Nir),
+ /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
+ PartialExpr(ExprKind<Nir>),
+}
+
+impl Nir {
+ /// Construct a Nir from a completely unnormalized expression.
+ pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+ NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
+ }
+ /// Construct a Nir from a partially normalized expression that's not in WHNF.
+ pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
+ // TODO: env
+ let env = NzEnv::new();
+ NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
+ }
+ /// Make a Nir from a NirKind
+ pub(crate) fn from_kind(v: NirKind) -> Nir {
+ NirInternal::from_whnf(v).into_nir()
+ }
+ pub(crate) fn from_const(c: Const) -> Self {
+ let v = NirKind::Const(c);
+ NirInternal::from_whnf(v).into_nir()
+ }
+ pub(crate) fn from_builtin(b: Builtin) -> Self {
+ Self::from_builtin_env(b, &NzEnv::new())
+ }
+ pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+ Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
+ }
+ pub(crate) fn from_text(txt: impl ToString) -> Self {
+ Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
+ }
+
+ pub(crate) fn as_const(&self) -> Option<Const> {
+ match &*self.kind() {
+ NirKind::Const(c) => Some(*c),
+ _ => None,
+ }
+ }
+
+ /// This is what you want if you want to pattern-match on the value.
+ pub(crate) fn kind(&self) -> &NirKind {
+ self.0.kind()
+ }
+
+ pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+ Type::new(self.clone(), u.into())
+ }
+ /// Converts a value back to the corresponding AST expression.
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ self.to_hir_noenv().to_expr(opts)
+ }
+ pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+ }
+
+ pub(crate) fn normalize(&self) {
+ self.0.normalize()
+ }
+
+ pub(crate) fn app(&self, v: Nir) -> Nir {
+ Nir::from_kind(apply_any(self.clone(), v))
+ }
+
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
+ ExprKind::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+ })
+ .collect(),
+ )
+ };
+
+ let hir = match &*self.kind() {
+ NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+ NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+ self_kind => HirKind::Expr(match self_kind {
+ NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
+ unreachable!()
+ }
+ NirKind::LamClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Lam(
+ binder.to_label(),
+ annot.to_hir(venv),
+ closure.to_hir(venv),
+ ),
+ NirKind::PiClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Pi(
+ binder.to_label(),
+ annot.to_hir(venv),
+ closure.to_hir(venv),
+ ),
+ NirKind::Const(c) => ExprKind::Const(*c),
+ NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+ NirKind::EmptyOptionalLit(n) => ExprKind::App(
+ Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
+ n.to_hir(venv),
+ ),
+ NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+ NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+ HirKind::Expr(ExprKind::App(
+ Nir::from_builtin(Builtin::List).to_hir(venv),
+ n.to_hir(venv),
+ )),
+ Span::Artificial,
+ )),
+ NirKind::NEListLit(elts) => ExprKind::NEListLit(
+ elts.iter().map(|v| v.to_hir(venv)).collect(),
+ ),
+ NirKind::TextLit(elts) => ExprKind::TextLit(
+ elts.iter()
+ .map(|t| t.map_ref(|v| v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::RecordLit(kvs) => ExprKind::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::RecordType(kts) => ExprKind::RecordType(
+ kts.iter()
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::UnionType(kts) => map_uniontype(kts),
+ NirKind::UnionConstructor(l, kts) => ExprKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ),
+ NirKind::UnionLit(l, v, kts) => ExprKind::App(
+ Hir::new(
+ HirKind::Expr(ExprKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ )),
+ Span::Artificial,
+ ),
+ v.to_hir(venv),
+ ),
+ NirKind::Equivalence(x, y) => ExprKind::BinOp(
+ BinOp::Equivalence,
+ x.to_hir(venv),
+ y.to_hir(venv),
+ ),
+ NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+ }),
+ };
+
+ Hir::new(hir, Span::Artificial)
+ }
+ pub fn to_hir_noenv(&self) -> Hir {
+ self.to_hir(VarEnv::new())
+ }
+}
+
+impl NirInternal {
+ fn from_whnf(k: NirKind) -> Self {
+ NirInternal {
+ kind: lazy::Lazy::new_completed(k),
+ }
+ }
+ fn from_thunk(th: Thunk) -> Self {
+ NirInternal {
+ kind: lazy::Lazy::new(th),
+ }
+ }
+ fn into_nir(self) -> Nir {
+ Nir(Rc::new(self))
+ }
+
+ fn kind(&self) -> &NirKind {
+ &self.kind
+ }
+ fn normalize(&self) {
+ self.kind().normalize();
+ }
+}
+
+impl NirKind {
+ pub(crate) fn into_nir(self) -> Nir {
+ Nir::from_kind(self)
+ }
+
+ pub(crate) fn normalize(&self) {
+ match self {
+ NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+
+ NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
+ tth.normalize();
+ }
+
+ NirKind::NEOptionalLit(th) => {
+ th.normalize();
+ }
+ NirKind::LamClosure { annot, closure, .. }
+ | NirKind::PiClosure { annot, closure, .. } => {
+ annot.normalize();
+ closure.normalize();
+ }
+ NirKind::AppliedBuiltin(closure) => closure.normalize(),
+ NirKind::NEListLit(elts) => {
+ for x in elts.iter() {
+ x.normalize();
+ }
+ }
+ NirKind::RecordLit(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ NirKind::RecordType(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ NirKind::UnionLit(_, v, kts) => {
+ v.normalize();
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ NirKind::TextLit(tlit) => tlit.normalize(),
+ NirKind::Equivalence(x, y) => {
+ x.normalize();
+ y.normalize();
+ }
+ NirKind::PartialExpr(e) => {
+ e.map_ref(Nir::normalize);
+ }
+ }
+ }
+
+ pub(crate) fn from_builtin(b: Builtin) -> NirKind {
+ NirKind::from_builtin_env(b, NzEnv::new())
+ }
+ pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+ NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ }
+}
+
+impl Thunk {
+ fn new(env: NzEnv, body: Hir) -> Self {
+ Thunk::Thunk { env, body }
+ }
+ fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
+ Thunk::PartialExpr { env, expr }
+ }
+ fn eval(self) -> NirKind {
+ match self {
+ Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+ Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+ }
+ }
+}
+
+impl Closure {
+ pub fn new(env: &NzEnv, body: Hir) -> Self {
+ Closure::Closure {
+ env: env.clone(),
+ body,
+ }
+ }
+ /// New closure that ignores its argument
+ pub fn new_constant(body: Nir) -> Self {
+ Closure::ConstantClosure { body }
+ }
+
+ pub fn apply(&self, val: Nir) -> Nir {
+ match self {
+ Closure::Closure { env, body, .. } => {
+ body.eval(env.insert_value(val, ()))
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+ fn apply_var(&self, var: NzVar) -> Nir {
+ match self {
+ Closure::Closure { .. } => {
+ self.apply(Nir::from_kind(NirKind::Var(var)))
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+
+ // TODO: somehow normalize the body. Might require to pass an env.
+ pub fn normalize(&self) {}
+
+ /// Convert this closure to a Hir expression
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ self.apply_var(NzVar::new(venv.size()))
+ .to_hir(venv.insert())
+ }
+ /// If the closure variable is free in the closure, return Err. Otherwise, return the value
+ /// with that free variable remove.
+ pub fn remove_binder(&self) -> Result<Nir, ()> {
+ match self {
+ Closure::Closure { .. } => {
+ let v = NzVar::fresh();
+ // TODO: handle case where variable is used in closure
+ // TODO: return information about where the variable is used
+ Ok(self.apply_var(v))
+ }
+ Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+ }
+ }
+}
+
+impl TextLit {
+ pub fn new(
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+ ) -> Self {
+ TextLit(squash_textlit(elts))
+ }
+ pub fn interpolate(v: Nir) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Expr(v)])
+ }
+ pub fn from_text(s: String) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ }
+
+ pub fn concat(&self, other: &TextLit) -> TextLit {
+ TextLit::new(self.iter().chain(other.iter()).cloned())
+ }
+ pub fn is_empty(&self) -> bool {
+ self.0.is_empty()
+ }
+ /// If the literal consists of only one interpolation and not text, return the interpolated
+ /// value.
+ pub fn as_single_expr(&self) -> Option<&Nir> {
+ use InterpolatedTextContents::Expr;
+ if let [Expr(v)] = self.0.as_slice() {
+ Some(v)
+ } else {
+ None
+ }
+ }
+ /// If there are no interpolations, return the corresponding text value.
+ pub fn as_text(&self) -> Option<String> {
+ use InterpolatedTextContents::Text;
+ if self.is_empty() {
+ Some(String::new())
+ } else if let [Text(s)] = self.0.as_slice() {
+ Some(s.clone())
+ } else {
+ None
+ }
+ }
+ pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
+ self.0.iter()
+ }
+ /// Normalize the contained values. This does not break the invariant because we have already
+ /// ensured that no contained values normalize to a TextLit.
+ pub fn normalize(&self) {
+ for x in self.0.iter() {
+ x.map_ref(Nir::normalize);
+ }
+ }
+}
+
+impl lazy::Eval<NirKind> for Thunk {
+ fn eval(self) -> NirKind {
+ self.eval()
+ }
+}
+
+/// Compare two values for equality modulo alpha/beta-equivalence.
+impl std::cmp::PartialEq for Nir {
+ fn eq(&self, other: &Self) -> bool {
+ Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+ }
+}
+impl std::cmp::Eq for Nir {}
+
+impl std::cmp::PartialEq for Thunk {
+ fn eq(&self, _other: &Self) -> bool {
+ unreachable!(
+ "Trying to compare thunks but we should only compare WHNFs"
+ )
+ }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+ fn eq(&self, other: &Self) -> bool {
+ let v = NzVar::fresh();
+ self.apply_var(v) == other.apply_var(v)
+ }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Nir {
+ fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ let vint: &NirInternal = &self.0;
+ let kind = vint.kind();
+ if let NirKind::Const(c) = kind {
+ return write!(fmt, "{:?}", c);
+ }
+ let mut x = fmt.debug_struct(&format!("Nir@WHNF"));
+ x.field("kind", kind);
+ x.finish()
+ }
+}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index a00b7ff..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,49 +3,39 @@ use std::collections::HashMap;
use crate::semantics::NzEnv;
use crate::semantics::{
- Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
- ValueKind,
+ Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
+ BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
};
-use crate::Normalized;
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
match f.kind() {
- ValueKind::LamClosure { closure, .. } => {
- closure.apply(a).to_whnf_check_type(ty)
+ NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
+ NirKind::AppliedBuiltin(closure) => closure.apply(a),
+ NirKind::UnionConstructor(l, kts) => {
+ NirKind::UnionLit(l.clone(), a, kts.clone())
}
- ValueKind::AppliedBuiltin(closure) => {
- closure.apply(a, f.get_type().unwrap(), ty)
- }
- ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
- l.clone(),
- a,
- kts.clone(),
- uniont.clone(),
- f.get_type().unwrap(),
- ),
- _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
+ _ => NirKind::PartialExpr(ExprKind::App(f, a)),
}
}
pub(crate) fn squash_textlit(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-) -> Vec<InterpolatedTextContents<Value>> {
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+) -> Vec<InterpolatedTextContents<Nir>> {
use std::mem::replace;
use InterpolatedTextContents::{Expr, Text};
fn inner(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
crnt_str: &mut String,
- ret: &mut Vec<InterpolatedTextContents<Value>>,
+ ret: &mut Vec<InterpolatedTextContents<Nir>>,
) {
for contents in elts {
match contents {
Text(s) => crnt_str.push_str(&s),
Expr(e) => match e.kind() {
- ValueKind::TextLit(elts2) => {
+ NirKind::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
}
_ => {
@@ -96,86 +86,77 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueKind(ValueKind),
- Value(Value),
- ValueRef(&'a Value),
- Expr(ExprKind<Value, Normalized>),
+ NirKind(NirKind),
+ Nir(Nir),
+ NirRef(&'a Nir),
+ Expr(ExprKind<Nir>),
}
-fn apply_binop<'a>(
- o: BinOp,
- x: &'a Value,
- y: &'a Value,
- ty: &Value,
-) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use ValueKind::{
- BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
- };
+ use LitKind::{Bool, Natural};
+ use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+
Some(match (o, x.kind(), y.kind()) {
- (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
- (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
- (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
- (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
- (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
- (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
- (BoolOr, _, _) if x == y => Ret::ValueRef(x),
- (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
- (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
- (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
- (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
- (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+ (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y),
+ (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x),
+ (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))),
+ (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))),
+ (BoolAnd, _, _) if x == y => Ret::NirRef(x),
+ (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))),
+ (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))),
+ (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y),
+ (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x),
+ (BoolOr, _, _) if x == y => Ret::NirRef(x),
+ (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y),
+ (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x),
+ (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))),
+ (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))),
+ (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y),
+ (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x),
+ (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))),
+ (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))),
- (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
- (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
- (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueKind(NaturalLit(x + y))
+ (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
+ (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
+ (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
+ Ret::NirKind(Lit(Natural(x + y)))
}
- (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
- (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
- (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
- (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueKind(NaturalLit(x * y))
+ (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))),
+ (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+ (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y),
+ (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x),
+ (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
+ Ret::NirKind(Lit(Natural(x * y)))
}
- (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
- (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
- NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
- ),
+ (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
+ xs.iter().chain(ys.iter()).cloned().collect(),
+ )),
- (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
- Ret::ValueRef(y)
- }
- (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
- Ret::ValueRef(x)
+ (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
+ (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
+ (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
+ Ret::NirKind(NirKind::TextLit(x.concat(y)))
}
- (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
- Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
- }
- (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
- ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
- ),
- (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
- ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
- ),
+ (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
+ x.concat(&TextLit::interpolate(y.clone())),
+ )),
+ (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
+ TextLit::interpolate(x.clone()).concat(y),
+ )),
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
+ Ret::NirRef(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
+ Ret::NirRef(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -183,32 +164,25 @@ fn apply_binop<'a>(
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- Ret::ValueKind(RecordLit(kvs))
+ Ret::NirKind(RecordLit(kvs))
}
- (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
+ (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
+ Ret::NirRef(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
+ Ret::NirRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let kts = match ty.kind() {
- RecordType(kts) => kts,
- _ => unreachable!("Internal type error"),
- };
- let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
- Ok(Value::from_partial_expr(
- ExprKind::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- ),
- kts.get(k).expect("Internal type error").clone(),
- ))
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+ Ok(Nir::from_partial_expr(ExprKind::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ )))
})?;
- Ret::ValueKind(RecordLit(kvs))
+ Ret::NirKind(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
@@ -216,118 +190,107 @@ fn apply_binop<'a>(
kts_x,
kts_y,
// If the Label exists for both records, then we hit the recursive case.
- |_, l: &Value, r: &Value| {
- Ok(Value::from_partial_expr(
- ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.clone(),
- r.clone(),
- ),
- ty.clone(),
- ))
+ |_, l: &Nir, r: &Nir| {
+ Ok(Nir::from_partial_expr(ExprKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ )))
},
)?;
- Ret::ValueKind(RecordType(kts))
+ Ret::NirKind(RecordType(kts))
}
(Equivalence, _, _) => {
- Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+ Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
}
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(
- expr: ExprKind<Value, Normalized>,
- ty: &Value,
- env: &NzEnv,
-) -> ValueKind {
- use ValueKind::{
- BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
- NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
- RecordType, UnionConstructor, UnionLit, UnionType,
+pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+ use LitKind::Bool;
+ use NirKind::{
+ EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+ PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+ UnionType,
};
let ret = match expr {
- ExprKind::Import(_) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
- // Those cases have already been completely handled in the typechecking phase (using
- // `RetWhole`), so they won't appear here.
- ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
- | ExprKind::Embed(_)
- | ExprKind::Var(_) => {
- unreachable!("This case should have been handled in typecheck")
+ ExprKind::Import(..) | ExprKind::Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
}
- ExprKind::Annot(x, _) => Ret::Value(x),
- ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
- ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+ ExprKind::Var(..)
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..) => unreachable!(
+ "This case should have been handled in normalize_hir_whnf"
+ ),
+
+ ExprKind::Annot(x, _) => Ret::Nir(x),
+ ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
+ ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
ExprKind::Assert(_) => Ret::Expr(expr),
- ExprKind::App(v, a) => Ret::Value(v.app(a)),
- ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
- ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
- ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
- ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
- ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+ ExprKind::App(v, a) => Ret::Nir(v.app(a)),
+ ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())),
+ ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
}) if args.len() == 1 => args[0].clone(),
_ => panic!("internal type error"),
};
- Ret::ValueKind(ValueKind::EmptyListLit(arg))
+ Ret::NirKind(NirKind::EmptyListLit(arg))
}
ExprKind::NEListLit(elts) => {
- Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+ Ret::NirKind(NEListLit(elts.into_iter().collect()))
}
ExprKind::RecordLit(kvs) => {
- Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+ Ret::NirKind(RecordLit(kvs.into_iter().collect()))
}
ExprKind::RecordType(kvs) => {
- Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+ Ret::NirKind(RecordType(kvs.into_iter().collect()))
}
ExprKind::UnionType(kvs) => {
- Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+ Ret::NirKind(UnionType(kvs.into_iter().collect()))
}
ExprKind::TextLit(elts) => {
let tlit = TextLit::new(elts.into_iter());
// Simplify bare interpolation
if let Some(v) = tlit.as_single_expr() {
- Ret::Value(v.clone())
+ Ret::Nir(v.clone())
} else {
- Ret::ValueKind(ValueKind::TextLit(tlit))
+ Ret::NirKind(NirKind::TextLit(tlit))
}
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
match b.kind() {
- BoolLit(true) => Ret::ValueRef(e1),
- BoolLit(false) => Ret::ValueRef(e2),
+ Lit(Bool(true)) => Ret::NirRef(e1),
+ Lit(Bool(false)) => Ret::NirRef(e2),
_ => {
match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
- (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
- _ if e1 == e2 => Ret::ValueRef(e1),
+ (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+ _ if e1 == e2 => Ret::NirRef(e1),
_ => Ret::Expr(expr),
}
}
}
}
- ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
ExprKind::Projection(_, ref ls) if ls.is_empty() => {
- Ret::ValueKind(RecordLit(HashMap::new()))
+ Ret::NirKind(RecordLit(HashMap::new()))
}
ExprKind::Projection(ref v, ref ls) => match v.kind() {
- RecordLit(kvs) => Ret::ValueKind(RecordLit(
+ RecordLit(kvs) => Ret::NirKind(RecordLit(
ls.iter()
.filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
.collect(),
@@ -335,7 +298,6 @@ pub(crate) fn normalize_one_layer(
PartialExpr(ExprKind::Projection(v2, _)) => {
return normalize_one_layer(
ExprKind::Projection(v2.clone(), ls.clone()),
- ty,
env,
)
}
@@ -343,63 +305,42 @@ pub(crate) fn normalize_one_layer(
},
ExprKind::Field(ref v, ref l) => match v.kind() {
RecordLit(kvs) => match kvs.get(l) {
- Some(r) => Ret::Value(r.clone()),
+ Some(r) => Ret::Nir(r.clone()),
None => Ret::Expr(expr),
},
- UnionType(kts) => Ret::ValueKind(UnionConstructor(
- l.clone(),
- kts.clone(),
- v.get_type().unwrap(),
- )),
+ UnionType(kts) => {
+ Ret::NirKind(UnionConstructor(l.clone(), kts.clone()))
+ }
PartialExpr(ExprKind::BinOp(
BinOp::RightBiasedRecordMerge,
x,
y,
)) => match (x.kind(), y.kind()) {
(_, RecordLit(kvs)) => match kvs.get(l) {
- Some(r) => Ret::Value(r.clone()),
+ Some(r) => Ret::Nir(r.clone()),
None => {
return normalize_one_layer(
ExprKind::Field(x.clone(), l.clone()),
- ty,
env,
)
}
},
(RecordLit(kvs), _) => match kvs.get(l) {
Some(r) => Ret::Expr(ExprKind::Field(
- Value::from_kind_and_type(
- PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- Value::from_kind_and_type(
- RecordLit({
- let mut kvs = HashMap::new();
- kvs.insert(l.clone(), r.clone());
- kvs
- }),
- Value::from_kind_and_type(
- RecordType({
- let mut kvs = HashMap::new();
- kvs.insert(
- l.clone(),
- r.get_type_not_sort(),
- );
- kvs
- }),
- r.get_type_not_sort()
- .get_type_not_sort(),
- ),
- ),
- y.clone(),
- )),
- v.get_type_not_sort(),
- ),
+ Nir::from_kind(PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ Nir::from_kind(RecordLit({
+ let mut kvs = HashMap::new();
+ kvs.insert(l.clone(), r.clone());
+ kvs
+ })),
+ y.clone(),
+ ))),
l.clone(),
)),
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -416,7 +357,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -426,7 +366,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(x.clone(), l.clone()),
- ty,
env,
)
}
@@ -438,25 +377,24 @@ pub(crate) fn normalize_one_layer(
ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
match handlers.kind() {
RecordLit(kvs) => match variant.kind() {
- UnionConstructor(l, _, _) => match kvs.get(l) {
- Some(h) => Ret::Value(h.clone()),
+ UnionConstructor(l, _) => match kvs.get(l) {
+ Some(h) => Ret::Nir(h.clone()),
None => Ret::Expr(expr),
},
- UnionLit(l, v, _, _, _) => match kvs.get(l) {
- Some(h) => Ret::Value(h.app(v.clone())),
+ UnionLit(l, v, _) => match kvs.get(l) {
+ Some(h) => Ret::Nir(h.app(v.clone())),
None => Ret::Expr(expr),
},
EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
- Some(h) => Ret::Value(h.clone()),
+ Some(h) => Ret::Nir(h.clone()),
None => Ret::Expr(expr),
},
NEOptionalLit(v) => match kvs.get(&"Some".into()) {
- Some(h) => Ret::Value(h.app(v.clone())),
+ Some(h) => Ret::Nir(h.app(v.clone())),
None => Ret::Expr(expr),
},
_ => Ret::Expr(expr),
@@ -467,37 +405,24 @@ pub(crate) fn normalize_one_layer(
ExprKind::ToMap(ref v, ref annot) => match v.kind() {
RecordLit(kvs) if kvs.is_empty() => {
match annot.as_ref().map(|v| v.kind()) {
- Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+ Some(NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
})) if args.len() == 1 => {
- Ret::ValueKind(EmptyListLit(args[0].clone()))
+ Ret::NirKind(EmptyListLit(args[0].clone()))
}
_ => Ret::Expr(expr),
}
}
- RecordLit(kvs) => Ret::ValueKind(NEListLit(
+ RecordLit(kvs) => Ret::NirKind(NEListLit(
kvs.iter()
.sorted_by_key(|(k, _)| k.clone())
.map(|(k, v)| {
let mut rec = HashMap::new();
- let mut rec_ty = HashMap::new();
- rec.insert("mapKey".into(), Value::from_text(k));
+ rec.insert("mapKey".into(), Nir::from_text(k));
rec.insert("mapValue".into(), v.clone());
- rec_ty.insert(
- "mapKey".into(),
- Value::from_builtin(Builtin::Text),
- );
- rec_ty.insert("mapValue".into(), v.get_type_not_sort());
-
- Value::from_kind_and_type(
- ValueKind::RecordLit(rec),
- Value::from_kind_and_type(
- ValueKind::RecordType(rec_ty),
- Value::from_const(Const::Type),
- ),
- )
+ Nir::from_kind(NirKind::RecordLit(rec))
})
.collect(),
)),
@@ -506,45 +431,41 @@ pub(crate) fn normalize_one_layer(
};
match ret {
- Ret::ValueKind(v) => v,
- Ret::Value(v) => v.to_whnf_check_type(ty),
- Ret::ValueRef(v) => v.to_whnf_check_type(ty),
- Ret::Expr(expr) => ValueKind::PartialExpr(expr),
+ Ret::NirKind(v) => v,
+ Ret::Nir(v) => v.kind().clone(),
+ Ret::NirRef(v) => v.kind().clone(),
+ Ret::Expr(expr) => NirKind::PartialExpr(expr),
}
}
-/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
- match tye.kind() {
- TyExprKind::Var(var) => env.lookup_val(var),
- TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+ match hir.kind() {
+ HirKind::Var(var) => env.lookup_val(var),
+ HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
- ValueKind::LamClosure {
+ NirKind::LamClosure {
binder: Binder::new(binder.clone()),
- annot: annot.clone(),
- closure: Closure::new(annot, env, body.clone()),
+ annot: annot,
+ closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
let annot = annot.eval(env);
- let closure = Closure::new(annot.clone(), env, body.clone());
- ValueKind::PiClosure {
+ NirKind::PiClosure {
binder: Binder::new(binder.clone()),
annot,
- closure,
+ closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
let val = val.eval(env);
- body.eval(&env.insert_value(val)).kind().clone()
+ body.eval(env.insert_value(val, ())).kind().clone()
}
- TyExprKind::Expr(e) => {
- let ty = match tye.get_type() {
- Ok(ty) => ty,
- Err(_) => return ValueKind::Const(Const::Sort),
- };
- let e = e.map_ref(|tye| tye.eval(env));
- normalize_one_layer(e, &ty, env)
+ HirKind::Expr(e) => {
+ let e = e.map_ref(|hir| hir.eval(env));
+ normalize_one_layer(e, env)
}
}
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
deleted file mode 100644
index 607aa0d..0000000
--- a/dhall/src/semantics/nze/value.rs
+++ /dev/null
@@ -1,666 +0,0 @@
-use std::collections::HashMap;
-use std::rc::Rc;
-
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
-use crate::semantics::{
- apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
- TyEnv,
-};
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
-use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural, Span,
-};
-use crate::{Normalized, NormalizedExpr, ToExprOptions};
-
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
-/// automatically. Uses a Rc<RefCell> to share computation.
-/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
-/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
-/// normalize as needed.
-#[derive(Clone)]
-pub(crate) struct Value(Rc<ValueInternal>);
-
-#[derive(Debug)]
-struct ValueInternal {
- kind: lazy::Lazy<Thunk, ValueKind>,
- /// This is None if and only if `form` is `Sort` (which doesn't have a type)
- ty: Option<Value>,
- span: Span,
-}
-
-/// An unevaluated subexpression
-#[derive(Debug, Clone)]
-pub(crate) enum Thunk {
- /// A completely unnormalized expression.
- Thunk { env: NzEnv, body: TyExpr },
- /// A partially normalized expression that may need to go through `normalize_one_layer`.
- PartialExpr {
- env: NzEnv,
- expr: ExprKind<Value, Normalized>,
- ty: Value,
- },
-}
-
-/// An unevaluated subexpression that takes an argument.
-#[derive(Debug, Clone)]
-pub(crate) enum Closure {
- /// Normal closure
- Closure {
- arg_ty: Value,
- env: NzEnv,
- body: TyExpr,
- },
- /// Closure that ignores the argument passed
- ConstantClosure { body: Value },
-}
-
-/// A text literal with interpolations.
-// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
-// text values must be merged.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
-
-/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
-/// normalized up to the first constructor, but subexpressions may not be fully normalized.
-/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
-/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
-/// if we have the first constructor of the NF at all levels, we actually have the NF.
-/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
-/// we only need to recursively normalize its sub-`Value`s to get to the NF.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
- /// Closures
- LamClosure {
- binder: Binder,
- annot: Value,
- closure: Closure,
- },
- PiClosure {
- binder: Binder,
- annot: Value,
- closure: Closure,
- },
- AppliedBuiltin(BuiltinClosure<Value>),
-
- Var(NzVar),
- Const(Const),
- BoolLit(bool),
- NaturalLit(Natural),
- IntegerLit(Integer),
- DoubleLit(NaiveDouble),
- EmptyOptionalLit(Value),
- NEOptionalLit(Value),
- // EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(Value),
- NEListLit(Vec<Value>),
- RecordType(HashMap<Label, Value>),
- RecordLit(HashMap<Label, Value>),
- UnionType(HashMap<Label, Option<Value>>),
- // Also keep the type of the uniontype around
- UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
- // Also keep the type of the uniontype and the constructor around
- UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
- TextLit(TextLit),
- Equivalence(Value, Value),
- /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
- PartialExpr(ExprKind<Value, Normalized>),
-}
-
-impl Value {
- pub(crate) fn const_sort() -> Value {
- ValueInternal::from_whnf(
- ValueKind::Const(Const::Sort),
- None,
- Span::Artificial,
- )
- .into_value()
- }
- /// Construct a Value from a completely unnormalized expression.
- pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
- ValueInternal::from_thunk(
- Thunk::new(env, tye.clone()),
- tye.get_type().ok(),
- tye.span().clone(),
- )
- .into_value()
- }
- /// Construct a Value from a partially normalized expression that's not in WHNF.
- pub(crate) fn from_partial_expr(
- e: ExprKind<Value, Normalized>,
- ty: Value,
- ) -> Value {
- // TODO: env
- let env = NzEnv::new();
- ValueInternal::from_thunk(
- Thunk::from_partial_expr(env, e, ty.clone()),
- Some(ty),
- Span::Artificial,
- )
- .into_value()
- }
- /// Make a Value from a ValueKind
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
- ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
- }
- pub(crate) fn from_const(c: Const) -> Self {
- let v = ValueKind::Const(c);
- match c {
- Const::Type => {
- Value::from_kind_and_type(v, Value::from_const(Const::Kind))
- }
- Const::Kind => {
- Value::from_kind_and_type(v, Value::from_const(Const::Sort))
- }
- Const::Sort => Value::const_sort(),
- }
- }
- pub(crate) fn from_builtin(b: Builtin) -> Self {
- Self::from_builtin_env(b, &NzEnv::new())
- }
- pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
- Value::from_kind_and_type(
- ValueKind::from_builtin_env(b, env.clone()),
- typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
- )
- }
- pub(crate) fn from_text(txt: impl ToString) -> Self {
- Value::from_kind_and_type(
- ValueKind::TextLit(TextLit::from_text(txt.to_string())),
- Value::from_builtin(Builtin::Text),
- )
- }
-
- pub(crate) fn as_const(&self) -> Option<Const> {
- match &*self.kind() {
- ValueKind::Const(c) => Some(*c),
- _ => None,
- }
- }
- // pub(crate) fn span(&self) -> Span {
- // self.0.span.clone()
- // }
-
- /// This is what you want if you want to pattern-match on the value.
- /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
- /// panics.
- pub(crate) fn kind(&self) -> &ValueKind {
- self.0.kind()
- }
-
- /// Converts a value back to the corresponding AST expression.
- pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- if opts.normalize {
- self.normalize();
- }
-
- self.to_tyexpr_noenv().to_expr(opts)
- }
- pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
- }
- pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
- self.kind().clone()
- }
- /// Before discarding type information, check that it matches the expected return type.
- pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
- self.check_type(ty);
- self.to_whnf_ignore_type()
- }
-
- /// Normalizes contents to normal form; faster than `normalize` if
- /// no one else shares this.
- pub(crate) fn normalize_mut(&mut self) {
- match Rc::get_mut(&mut self.0) {
- // Mutate directly if sole owner
- Some(vint) => vint.normalize_mut(),
- // Otherwise mutate through the refcell
- None => self.normalize(),
- }
- }
- pub(crate) fn normalize(&self) {
- self.0.normalize()
- }
-
- pub(crate) fn app(&self, v: Value) -> Value {
- let body_t = match &*self.get_type_not_sort().kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- v.check_type(annot);
- closure.apply(v.clone())
- }
- _ => unreachable!("Internal type error"),
- };
- Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
- }
-
- /// In debug mode, panic if the provided type doesn't match the value's type.
- /// Otherwise does nothing.
- pub(crate) fn check_type(&self, _ty: &Value) {
- // TODO: reenable
- // debug_assert_eq!(
- // Some(ty),
- // self.get_type().ok().as_ref(),
- // "Internal type error"
- // );
- }
- pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
- Ok(self.0.get_type()?.clone())
- }
- /// When we know the value isn't `Sort`, this gets the type directly
- pub(crate) fn get_type_not_sort(&self) -> Value {
- self.get_type()
- .expect("Internal type error: value is `Sort` but shouldn't be")
- }
-
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
- let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
- ExprKind::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
- })
- .collect(),
- )
- };
-
- let tye = match &*self.kind() {
- ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
- ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
- self_kind => TyExprKind::Expr(match self_kind {
- ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
- unreachable!()
- }
- ValueKind::LamClosure {
- binder,
- annot,
- closure,
- } => ExprKind::Lam(
- binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(venv),
- ),
- ValueKind::PiClosure {
- binder,
- annot,
- closure,
- } => ExprKind::Pi(
- binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(venv),
- ),
- ValueKind::Const(c) => ExprKind::Const(*c),
- ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
- ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
- ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
- ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
- ValueKind::EmptyOptionalLit(n) => ExprKind::App(
- Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
- n.to_tyexpr(venv),
- ),
- ValueKind::NEOptionalLit(n) => {
- ExprKind::SomeLit(n.to_tyexpr(venv))
- }
- ValueKind::EmptyListLit(n) => {
- ExprKind::EmptyListLit(TyExpr::new(
- TyExprKind::Expr(ExprKind::App(
- Value::from_builtin(Builtin::List).to_tyexpr(venv),
- n.to_tyexpr(venv),
- )),
- Some(Value::from_const(Const::Type)),
- Span::Artificial,
- ))
- }
- ValueKind::NEListLit(elts) => ExprKind::NEListLit(
- elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
- ),
- ValueKind::TextLit(elts) => ExprKind::TextLit(
- elts.iter()
- .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::RecordType(kts) => ExprKind::RecordType(
- kts.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::UnionType(kts) => map_uniontype(kts),
- ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(t.clone()),
- Span::Artificial,
- ),
- l.clone(),
- ),
- ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
- TyExpr::new(
- TyExprKind::Expr(ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(uniont.clone()),
- Span::Artificial,
- ),
- l.clone(),
- )),
- Some(ctort.clone()),
- Span::Artificial,
- ),
- v.to_tyexpr(venv),
- ),
- ValueKind::Equivalence(x, y) => ExprKind::BinOp(
- BinOp::Equivalence,
- x.to_tyexpr(venv),
- y.to_tyexpr(venv),
- ),
- ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
- }),
- };
-
- TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
- }
- pub fn to_tyexpr_noenv(&self) -> TyExpr {
- self.to_tyexpr(VarEnv::new())
- }
-}
-
-impl ValueInternal {
- fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
- ValueInternal {
- kind: lazy::Lazy::new_completed(k),
- ty,
- span,
- }
- }
- fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
- ValueInternal {
- kind: lazy::Lazy::new(th),
- ty,
- span,
- }
- }
- fn into_value(self) -> Value {
- Value(Rc::new(self))
- }
-
- fn kind(&self) -> &ValueKind {
- &self.kind
- }
- fn normalize(&self) {
- self.kind().normalize();
- }
- // TODO: deprecated
- fn normalize_mut(&mut self) {
- self.normalize();
- }
-
- fn get_type(&self) -> Result<&Value, TypeError> {
- match &self.ty {
- Some(t) => Ok(t),
- None => Err(TypeError::new(TypeMessage::Sort)),
- }
- }
-}
-
-impl ValueKind {
- pub(crate) fn into_value_with_type(self, t: Value) -> Value {
- Value::from_kind_and_type(self, t)
- }
-
- pub(crate) fn normalize(&self) {
- match self {
- ValueKind::Var(..)
- | ValueKind::Const(_)
- | ValueKind::BoolLit(_)
- | ValueKind::NaturalLit(_)
- | ValueKind::IntegerLit(_)
- | ValueKind::DoubleLit(_) => {}
-
- ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
- tth.normalize();
- }
-
- ValueKind::NEOptionalLit(th) => {
- th.normalize();
- }
- ValueKind::LamClosure { annot, closure, .. }
- | ValueKind::PiClosure { annot, closure, .. } => {
- annot.normalize();
- closure.normalize();
- }
- ValueKind::AppliedBuiltin(closure) => closure.normalize(),
- ValueKind::NEListLit(elts) => {
- for x in elts.iter() {
- x.normalize();
- }
- }
- ValueKind::RecordLit(kvs) => {
- for x in kvs.values() {
- x.normalize();
- }
- }
- ValueKind::RecordType(kvs) => {
- for x in kvs.values() {
- x.normalize();
- }
- }
- ValueKind::UnionType(kts)
- | ValueKind::UnionConstructor(_, kts, _) => {
- for x in kts.values().flat_map(|opt| opt) {
- x.normalize();
- }
- }
- ValueKind::UnionLit(_, v, kts, _, _) => {
- v.normalize();
- for x in kts.values().flat_map(|opt| opt) {
- x.normalize();
- }
- }
- ValueKind::TextLit(tlit) => tlit.normalize(),
- ValueKind::Equivalence(x, y) => {
- x.normalize();
- y.normalize();
- }
- ValueKind::PartialExpr(e) => {
- e.map_ref(Value::normalize);
- }
- }
- }
-
- pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
- ValueKind::from_builtin_env(b, NzEnv::new())
- }
- pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
- ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
- }
-}
-
-impl Thunk {
- pub fn new(env: &NzEnv, body: TyExpr) -> Self {
- Thunk::Thunk {
- env: env.clone(),
- body,
- }
- }
- pub fn from_partial_expr(
- env: NzEnv,
- expr: ExprKind<Value, Normalized>,
- ty: Value,
- ) -> Self {
- Thunk::PartialExpr { env, expr, ty }
- }
- pub fn eval(self) -> ValueKind {
- match self {
- Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
- Thunk::PartialExpr { env, expr, ty } => {
- normalize_one_layer(expr, &ty, &env)
- }
- }
- }
-}
-
-impl Closure {
- pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
- Closure::Closure {
- arg_ty,
- env: env.clone(),
- body,
- }
- }
- /// New closure that ignores its argument
- pub fn new_constant(body: Value) -> Self {
- Closure::ConstantClosure { body }
- }
-
- pub fn apply(&self, val: Value) -> Value {
- match self {
- Closure::Closure { env, body, .. } => {
- body.eval(&env.insert_value(val))
- }
- Closure::ConstantClosure { body, .. } => body.clone(),
- }
- }
- fn apply_var(&self, var: NzVar) -> Value {
- match self {
- Closure::Closure { arg_ty, .. } => {
- let val = Value::from_kind_and_type(
- ValueKind::Var(var),
- arg_ty.clone(),
- );
- self.apply(val)
- }
- Closure::ConstantClosure { body, .. } => body.clone(),
- }
- }
-
- // TODO: somehow normalize the body. Might require to pass an env.
- pub fn normalize(&self) {}
- /// Convert this closure to a TyExpr
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
- self.apply_var(NzVar::new(venv.size()))
- .to_tyexpr(venv.insert())
- }
- /// If the closure variable is free in the closure, return Err. Otherwise, return the value
- /// with that free variable remove.
- pub fn remove_binder(&self) -> Result<Value, ()> {
- match self {
- Closure::Closure { .. } => {
- let v = NzVar::fresh();
- // TODO: handle case where variable is used in closure
- // TODO: return information about where the variable is used
- Ok(self.apply_var(v))
- }
- Closure::ConstantClosure { body, .. } => Ok(body.clone()),
- }
- }
-}
-
-impl TextLit {
- pub fn new(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
- ) -> Self {
- TextLit(squash_textlit(elts))
- }
- pub fn interpolate(v: Value) -> TextLit {
- TextLit(vec![InterpolatedTextContents::Expr(v)])
- }
- pub fn from_text(s: String) -> TextLit {
- TextLit(vec![InterpolatedTextContents::Text(s)])
- }
-
- pub fn concat(&self, other: &TextLit) -> TextLit {
- TextLit::new(self.iter().chain(other.iter()).cloned())
- }
- pub fn is_empty(&self) -> bool {
- self.0.is_empty()
- }
- /// If the literal consists of only one interpolation and not text, return the interpolated
- /// value.
- pub fn as_single_expr(&self) -> Option<&Value> {
- use InterpolatedTextContents::Expr;
- if let [Expr(v)] = self.0.as_slice() {
- Some(v)
- } else {
- None
- }
- }
- /// If there are no interpolations, return the corresponding text value.
- pub fn as_text(&self) -> Option<String> {
- use InterpolatedTextContents::Text;
- if self.is_empty() {
- Some(String::new())
- } else if let [Text(s)] = self.0.as_slice() {
- Some(s.clone())
- } else {
- None
- }
- }
- pub fn iter(
- &self,
- ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
- self.0.iter()
- }
- /// Normalize the contained values. This does not break the invariant because we have already
- /// ensured that no contained values normalize to a TextLit.
- pub fn normalize(&self) {
- for x in self.0.iter() {
- x.map_ref(Value::normalize);
- }
- }
-}
-
-impl lazy::Eval<ValueKind> for Thunk {
- fn eval(self) -> ValueKind {
- self.eval()
- }
-}
-
-/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
- fn eq(&self, other: &Self) -> bool {
- Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
- }
-}
-impl std::cmp::Eq for Value {}
-
-impl std::cmp::PartialEq for Thunk {
- fn eq(&self, _other: &Self) -> bool {
- unreachable!(
- "Trying to compare thunks but we should only compare WHNFs"
- )
- }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for Closure {
- fn eq(&self, other: &Self) -> bool {
- let v = NzVar::fresh();
- self.apply_var(v) == other.apply_var(v)
- }
-}
-impl std::cmp::Eq for Closure {}
-
-impl std::fmt::Debug for Value {
- fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let vint: &ValueInternal = &self.0;
- let kind = vint.kind();
- if let ValueKind::Const(c) = kind {
- return write!(fmt, "{:?}", c);
- }
- let mut x = fmt.debug_struct(&format!("Value@WHNF"));
- x.field("kind", kind);
- if let Some(ty) = vint.ty.as_ref() {
- x.field("type", &ty);
- } else {
- x.field("type", &None::<()>);
- }
- x.finish()
- }
-}
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
index 264b81d..413c759 100644
--- a/dhall/src/semantics/nze/var.rs
+++ b/dhall/src/semantics/nze/var.rs
@@ -1,7 +1,7 @@
use crate::syntax::Label;
// Exactly like a Label, but equality returns always true.
-// This is so that ValueKind equality is exactly alpha-equivalence.
+// This is so that NirKind equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct Binder {
name: Label,
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
deleted file mode 100644
index 3acf114..0000000
--- a/dhall/src/semantics/resolve.rs
+++ /dev/null
@@ -1,181 +0,0 @@
-use std::collections::HashMap;
-use std::path::{Path, PathBuf};
-
-use crate::error::{Error, ImportError};
-use crate::syntax;
-use crate::syntax::{FilePath, ImportLocation, URL};
-use crate::{Normalized, NormalizedExpr, Parsed, Resolved};
-
-type Import = syntax::Import<NormalizedExpr>;
-
-/// A root from which to resolve relative imports.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ImportRoot {
- LocalDir(PathBuf),
-}
-
-type ImportCache = HashMap<Import, Normalized>;
-
-pub(crate) type ImportStack = Vec<Import>;
-
-fn resolve_import(
- import: &Import,
- root: &ImportRoot,
- import_cache: &mut ImportCache,
- import_stack: &ImportStack,
-) -> Result<Normalized, ImportError> {
- use self::ImportRoot::*;
- use syntax::FilePrefix::*;
- use syntax::ImportLocation::*;
- let cwd = match root {
- LocalDir(cwd) => cwd,
- };
- match &import.location {
- Local(prefix, path) => {
- let path_buf: PathBuf = path.file_path.iter().collect();
- let path_buf = match prefix {
- // TODO: fail gracefully
- Parent => cwd.parent().unwrap().join(path_buf),
- Here => cwd.join(path_buf),
- _ => unimplemented!("{:?}", import),
- };
- Ok(load_import(&path_buf, import_cache, import_stack).map_err(
- |e| ImportError::Recursive(import.clone(), Box::new(e)),
- )?)
- }
- _ => unimplemented!("{:?}", import),
- }
-}
-
-fn load_import(
- f: &Path,
- import_cache: &mut ImportCache,
- import_stack: &ImportStack,
-) -> Result<Normalized, Error> {
- Ok(
- do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
- .typecheck()?
- .normalize(),
- )
-}
-
-fn do_resolve_expr(
- parsed: Parsed,
- import_cache: &mut ImportCache,
- import_stack: &ImportStack,
-) -> Result<Resolved, ImportError> {
- let Parsed(mut expr, root) = parsed;
- let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
- if import_stack.contains(&import) {
- return Err(ImportError::ImportCycle(import_stack.clone(), import));
- }
- match import_cache.get(&import) {
- Some(expr) => Ok(expr.clone()),
- None => {
- // Copy the import stack and push the current import
- let mut import_stack = import_stack.clone();
- import_stack.push(import.clone());
-
- // Resolve the import recursively
- let expr = resolve_import(
- &import,
- &root,
- import_cache,
- &import_stack,
- )?;
-
- // Add the import to the cache
- import_cache.insert(import, expr.clone());
- Ok(expr)
- }
- }
- };
- expr.traverse_resolve_mut(&mut resolve)?;
- Ok(Resolved(expr))
-}
-
-pub(crate) fn resolve(e: Parsed) -> Result<Resolved, ImportError> {
- do_resolve_expr(e, &mut HashMap::new(), &Vec::new())
-}
-
-pub(crate) fn skip_resolve_expr(
- parsed: Parsed,
-) -> Result<Resolved, ImportError> {
- let mut expr = parsed.0;
- let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
- Err(ImportError::UnexpectedImport(import))
- };
- expr.traverse_resolve_mut(&mut resolve)?;
- Ok(Resolved(expr))
-}
-
-pub trait Canonicalize {
- fn canonicalize(&self) -> Self;
-}
-
-impl Canonicalize for FilePath {
- fn canonicalize(&self) -> FilePath {
- let mut file_path = Vec::new();
- let mut file_path_components = self.file_path.clone().into_iter();
-
- loop {
- let component = file_path_components.next();
- match component.as_ref() {
- // ───────────────────
- // canonicalize(ε) = ε
- None => break,
-
- // canonicalize(directory₀) = directory₁
- // ───────────────────────────────────────
- // canonicalize(directory₀/.) = directory₁
- Some(c) if c == "." => continue,
-
- Some(c) if c == ".." => match file_path_components.next() {
- // canonicalize(directory₀) = ε
- // ────────────────────────────
- // canonicalize(directory₀/..) = /..
- None => file_path.push("..".to_string()),
-
- // canonicalize(directory₀) = directory₁/..
- // ──────────────────────────────────────────────
- // canonicalize(directory₀/..) = directory₁/../..
- Some(ref c) if c == ".." => {
- file_path.push("..".to_string());
- file_path.push("..".to_string());
- }
-
- // canonicalize(directory₀) = directory₁/component
- // ─────────────────────────────────────────────── ; If "component" is not
- // canonicalize(directory₀/..) = directory₁ ; ".."
- Some(_) => continue,
- },
-
- // canonicalize(directory₀) = directory₁
- // ───────────────────────────────────────────────────────── ; If no other
- // canonicalize(directory₀/component) = directory₁/component ; rule matches
- Some(c) => file_path.push(c.clone()),
- }
- }
-
- FilePath { file_path }
- }
-}
-
-impl<SE: Copy> Canonicalize for ImportLocation<SE> {
- fn canonicalize(&self) -> ImportLocation<SE> {
- match self {
- ImportLocation::Local(prefix, file) => {
- ImportLocation::Local(*prefix, file.canonicalize())
- }
- ImportLocation::Remote(url) => ImportLocation::Remote(URL {
- scheme: url.scheme,
- authority: url.authority.clone(),
- path: url.path.canonicalize(),
- query: url.query.clone(),
- headers: url.headers.clone(),
- }),
- ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
- ImportLocation::Missing => ImportLocation::Missing,
- }
- }
-}
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
new file mode 100644
index 0000000..43676cc
--- /dev/null
+++ b/dhall/src/semantics/resolve/env.rs
@@ -0,0 +1,104 @@
+use std::collections::HashMap;
+
+use crate::error::{Error, ImportError};
+use crate::semantics::{AlphaVar, Import, TypedHir, VarEnv};
+use crate::syntax::{Label, V};
+
+/// Environment for resolving names.
+#[derive(Debug, Clone)]
+pub(crate) struct NameEnv {
+ names: Vec<Label>,
+}
+
+pub(crate) type ImportCache = HashMap<Import, TypedHir>;
+pub(crate) type ImportStack = Vec<Import>;
+
+/// Environment for resolving imports
+#[derive(Debug, Clone)]
+pub(crate) struct ImportEnv {
+ cache: ImportCache,
+ stack: ImportStack,
+}
+
+impl NameEnv {
+ pub fn new() -> Self {
+ NameEnv { names: Vec::new() }
+ }
+ pub fn as_varenv(&self) -> VarEnv {
+ VarEnv::from_size(self.names.len())
+ }
+
+ pub fn insert(&self, x: &Label) -> Self {
+ let mut env = self.clone();
+ env.insert_mut(x);
+ env
+ }
+ pub fn insert_mut(&mut self, x: &Label) {
+ self.names.push(x.clone())
+ }
+ pub fn remove_mut(&mut self) {
+ self.names.pop();
+ }
+
+ pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
+ let V(name, idx) = var;
+ let (idx, _) = self
+ .names
+ .iter()
+ .rev()
+ .enumerate()
+ .filter(|(_, n)| *n == name)
+ .nth(*idx)?;
+ Some(AlphaVar::new(idx))
+ }
+ pub fn label_var(&self, var: &AlphaVar) -> V {
+ let name = &self.names[self.names.len() - 1 - var.idx()];
+ let idx = self
+ .names
+ .iter()
+ .rev()
+ .take(var.idx())
+ .filter(|n| *n == name)
+ .count();
+ V(name.clone(), idx)
+ }
+}
+
+impl ImportEnv {
+ pub fn new() -> Self {
+ ImportEnv {
+ cache: HashMap::new(),
+ stack: Vec::new(),
+ }
+ }
+
+ pub fn handle_import(
+ &mut self,
+ import: Import,
+ mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<TypedHir, Error>,
+ ) -> Result<TypedHir, Error> {
+ if self.stack.contains(&import) {
+ return Err(
+ ImportError::ImportCycle(self.stack.clone(), import).into()
+ );
+ }
+ Ok(match self.cache.get(&import) {
+ Some(expr) => expr.clone(),
+ None => {
+ // Push the current import on the stack
+ self.stack.push(import.clone());
+
+ // Resolve the import recursively
+ let expr = do_resolve(self, &import)?;
+
+ // Remove import from the stack.
+ self.stack.pop();
+
+ // Add the import to the cache
+ self.cache.insert(import, expr.clone());
+
+ expr
+ }
+ })
+ }
+}
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
new file mode 100644
index 0000000..2f3464a
--- /dev/null
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -0,0 +1,135 @@
+use crate::error::TypeError;
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
+use crate::syntax::{Expr, ExprKind, Span, V};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct AlphaVar {
+ idx: usize,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum HirKind {
+ /// A resolved variable (i.e. a DeBruijn index)
+ Var(AlphaVar),
+ /// Result of resolving an import.
+ Import(Hir, Type),
+ // Forbidden ExprKind variants: Var, Import, Completion
+ Expr(ExprKind<Hir>),
+}
+
+// An expression with resolved variables and imports.
+#[derive(Debug, Clone)]
+pub(crate) struct Hir {
+ kind: Box<HirKind>,
+ span: Span,
+}
+
+impl AlphaVar {
+ pub(crate) fn new(idx: usize) -> Self {
+ AlphaVar { idx }
+ }
+ pub(crate) fn idx(&self) -> usize {
+ self.idx
+ }
+}
+
+impl Hir {
+ pub fn new(kind: HirKind, span: Span) -> Self {
+ Hir {
+ kind: Box::new(kind),
+ span,
+ }
+ }
+
+ pub fn kind(&self) -> &HirKind {
+ &*self.kind
+ }
+ pub fn span(&self) -> Span {
+ self.span.clone()
+ }
+
+ /// Converts a closed Hir expr back to the corresponding AST expression.
+ pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ hir_to_expr(self, opts, &mut NameEnv::new())
+ }
+ /// Converts a closed Hir expr back to the corresponding AST expression.
+ pub fn to_expr_noopts(&self) -> NormalizedExpr {
+ let opts = ToExprOptions { alpha: false };
+ self.to_expr(opts)
+ }
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ let opts = ToExprOptions { alpha: false };
+ let mut env = env.as_nameenv().clone();
+ hir_to_expr(self, opts, &mut env)
+ }
+
+ /// Typecheck the Hir.
+ pub fn typecheck<'hir>(
+ &'hir self,
+ env: &TyEnv,
+ ) -> Result<Tir<'hir>, TypeError> {
+ type_with(env, self, None)
+ }
+
+ /// Eval the Hir. It will actually get evaluated only as needed on demand.
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+ Nir::new_thunk(env.into(), self.clone())
+ }
+ /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
+ /// needed on demand.
+ pub fn eval_closed_expr(&self) -> Nir {
+ self.eval(NzEnv::new())
+ }
+ /// Eval a closed Hir fully and recursively;
+ pub fn rec_eval_closed_expr(&self) -> Nir {
+ let val = self.eval_closed_expr();
+ val.normalize();
+ val
+ }
+}
+
+fn hir_to_expr(
+ hir: &Hir,
+ opts: ToExprOptions,
+ env: &mut NameEnv,
+) -> NormalizedExpr {
+ let kind = match hir.kind() {
+ HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
+ HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
+ HirKind::Import(hir, _) => {
+ return hir_to_expr(hir, opts, &mut NameEnv::new())
+ }
+ HirKind::Expr(e) => {
+ let e = e.map_ref_maybe_binder(|l, hir| {
+ if let Some(l) = l {
+ env.insert_mut(l);
+ }
+ let e = hir_to_expr(hir, opts, env);
+ if let Some(_) = l {
+ env.remove_mut();
+ }
+ e
+ });
+
+ match e {
+ ExprKind::Lam(_, t, e) if opts.alpha => {
+ ExprKind::Lam("_".into(), t, e)
+ }
+ ExprKind::Pi(_, t, e) if opts.alpha => {
+ ExprKind::Pi("_".into(), t, e)
+ }
+ e => e,
+ }
+ }
+ };
+ Expr::new(kind, hir.span())
+}
+
+impl std::cmp::PartialEq for Hir {
+ fn eq(&self, other: &Self) -> bool {
+ self.kind == other.kind
+ }
+}
+impl std::cmp::Eq for Hir {}
diff --git a/dhall/src/semantics/resolve/mod.rs b/dhall/src/semantics/resolve/mod.rs
new file mode 100644
index 0000000..517907b
--- /dev/null
+++ b/dhall/src/semantics/resolve/mod.rs
@@ -0,0 +1,6 @@
+pub mod env;
+pub mod hir;
+pub mod resolve;
+pub(crate) use env::*;
+pub(crate) use hir::*;
+pub(crate) use resolve::*;
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
new file mode 100644
index 0000000..82800ec
--- /dev/null
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -0,0 +1,231 @@
+use std::borrow::Cow;
+use std::path::{Path, PathBuf};
+
+use crate::error::ErrorBuilder;
+use crate::error::{Error, ImportError};
+use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
+use crate::syntax;
+use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
+use crate::{Parsed, ParsedExpr, Resolved};
+
+// TODO: evaluate import headers
+pub(crate) type Import = syntax::Import<()>;
+
+/// Owned Hir with a type. Different from Tir because the Hir is owned.
+pub(crate) type TypedHir = (Hir, Type);
+
+/// A root from which to resolve relative imports.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ImportRoot {
+ LocalDir(PathBuf),
+}
+
+fn resolve_one_import(
+ env: &mut ImportEnv,
+ import: &Import,
+ root: &ImportRoot,
+) -> Result<TypedHir, Error> {
+ use self::ImportRoot::*;
+ use syntax::FilePrefix::*;
+ use syntax::ImportLocation::*;
+ let cwd = match root {
+ LocalDir(cwd) => cwd,
+ };
+ match &import.location {
+ Local(prefix, path) => {
+ let path_buf: PathBuf = path.file_path.iter().collect();
+ let path_buf = match prefix {
+ // TODO: fail gracefully
+ Parent => cwd.parent().unwrap().join(path_buf),
+ Here => cwd.join(path_buf),
+ _ => unimplemented!("{:?}", import),
+ };
+ Ok(load_import(env, &path_buf)?)
+ }
+ _ => unimplemented!("{:?}", import),
+ }
+}
+
+fn load_import(env: &mut ImportEnv, f: &Path) -> Result<TypedHir, Error> {
+ let parsed = Parsed::parse_file(f)?;
+ let typed = resolve_with_env(env, parsed)?.typecheck()?;
+ Ok((typed.normalize().to_hir(), typed.ty().clone()))
+}
+
+/// Desugar the first level of the expression.
+fn desugar(expr: &Expr) -> Cow<'_, Expr> {
+ match expr.kind() {
+ ExprKind::Completion(ty, compl) => {
+ let ty_field_default = Expr::new(
+ ExprKind::Field(ty.clone(), "default".into()),
+ expr.span(),
+ );
+ let merged = Expr::new(
+ ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ ty_field_default,
+ compl.clone(),
+ ),
+ expr.span(),
+ );
+ let ty_field_type = Expr::new(
+ ExprKind::Field(ty.clone(), "Type".into()),
+ expr.span(),
+ );
+ Cow::Owned(Expr::new(
+ ExprKind::Annot(merged, ty_field_type),
+ expr.span(),
+ ))
+ }
+ _ => Cow::Borrowed(expr),
+ }
+}
+
+/// Traverse the expression, handling import alternatives and passing
+/// found imports to the provided function. Also resolving names.
+fn traverse_resolve_expr(
+ name_env: &mut NameEnv,
+ expr: &Expr,
+ f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
+) -> Result<Hir, Error> {
+ let expr = desugar(expr);
+ Ok(match expr.kind() {
+ ExprKind::Var(var) => match name_env.unlabel_var(&var) {
+ Some(v) => Hir::new(HirKind::Var(v), expr.span()),
+ None => mkerr(
+ ErrorBuilder::new(format!("unbound variable `{}`", var))
+ .span_err(expr.span(), "not found in this scope")
+ .format(),
+ )?,
+ },
+ ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
+ match traverse_resolve_expr(name_env, l, f) {
+ Ok(l) => l,
+ Err(_) => {
+ match traverse_resolve_expr(name_env, r, f) {
+ Ok(r) => r,
+ // TODO: keep track of the other error too
+ Err(e) => return Err(e),
+ }
+ }
+ }
+ }
+ kind => {
+ let kind = kind.traverse_ref_maybe_binder(|l, e| {
+ if let Some(l) = l {
+ name_env.insert_mut(l);
+ }
+ let hir = traverse_resolve_expr(name_env, e, f)?;
+ if let Some(_) = l {
+ name_env.remove_mut();
+ }
+ Ok::<_, Error>(hir)
+ })?;
+ let kind = match kind {
+ ExprKind::Import(import) => {
+ // TODO: evaluate import headers
+ let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
+ let imported = f(import)?;
+ HirKind::Import(imported.0, imported.1)
+ }
+ kind => HirKind::Expr(kind),
+ };
+ Hir::new(kind, expr.span())
+ }
+ })
+}
+
+fn resolve_with_env(
+ env: &mut ImportEnv,
+ parsed: Parsed,
+) -> Result<Resolved, Error> {
+ let Parsed(expr, root) = parsed;
+ let resolved =
+ traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| {
+ env.handle_import(import, |env, import| {
+ resolve_one_import(env, import, &root)
+ })
+ })?;
+ Ok(Resolved(resolved))
+}
+
+pub(crate) fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
+ resolve_with_env(&mut ImportEnv::new(), parsed)
+}
+
+pub(crate) fn skip_resolve(expr: &ParsedExpr) -> Result<Hir, Error> {
+ traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| {
+ Err(ImportError::UnexpectedImport(import).into())
+ })
+}
+
+pub trait Canonicalize {
+ fn canonicalize(&self) -> Self;
+}
+
+impl Canonicalize for FilePath {
+ fn canonicalize(&self) -> FilePath {
+ let mut file_path = Vec::new();
+ let mut file_path_components = self.file_path.clone().into_iter();
+
+ loop {
+ let component = file_path_components.next();
+ match component.as_ref() {
+ // ───────────────────
+ // canonicalize(ε) = ε
+ None => break,
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────
+ // canonicalize(directory₀/.) = directory₁
+ Some(c) if c == "." => continue,
+
+ Some(c) if c == ".." => match file_path_components.next() {
+ // canonicalize(directory₀) = ε
+ // ────────────────────────────
+ // canonicalize(directory₀/..) = /..
+ None => file_path.push("..".to_string()),
+
+ // canonicalize(directory₀) = directory₁/..
+ // ──────────────────────────────────────────────
+ // canonicalize(directory₀/..) = directory₁/../..
+ Some(ref c) if c == ".." => {
+ file_path.push("..".to_string());
+ file_path.push("..".to_string());
+ }
+
+ // canonicalize(directory₀) = directory₁/component
+ // ─────────────────────────────────────────────── ; If "component" is not
+ // canonicalize(directory₀/..) = directory₁ ; ".."
+ Some(_) => continue,
+ },
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────────────────────── ; If no other
+ // canonicalize(directory₀/component) = directory₁/component ; rule matches
+ Some(c) => file_path.push(c.clone()),
+ }
+ }
+
+ FilePath { file_path }
+ }
+}
+
+impl<SE: Copy> Canonicalize for ImportLocation<SE> {
+ fn canonicalize(&self) -> ImportLocation<SE> {
+ match self {
+ ImportLocation::Local(prefix, file) => {
+ ImportLocation::Local(*prefix, file.canonicalize())
+ }
+ ImportLocation::Remote(url) => ImportLocation::Remote(URL {
+ scheme: url.scheme,
+ authority: url.authority.clone(),
+ path: url.path.canonicalize(),
+ query: url.query.clone(),
+ headers: url.headers.clone(),
+ }),
+ ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
+ ImportLocation::Missing => ImportLocation::Missing,
+ }
+ }
+}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fc711c..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,5 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
-use crate::syntax::{Label, V};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
+use crate::syntax::Label;
/// Environment for indexing variables.
#[derive(Debug, Clone, Copy)]
@@ -7,23 +7,20 @@ pub(crate) struct VarEnv {
size: usize,
}
-/// Environment for resolving names.
-#[derive(Debug, Clone)]
-pub(crate) struct NameEnv {
- names: Vec<Label>,
-}
-
/// Environment for typing expressions.
#[derive(Debug, Clone)]
pub(crate) struct TyEnv {
names: NameEnv,
- items: NzEnv,
+ items: ValEnv<Type>,
}
impl VarEnv {
pub fn new() -> Self {
VarEnv { size: 0 }
}
+ pub fn from_size(size: usize) -> Self {
+ VarEnv { size }
+ }
pub fn size(&self) -> usize {
self.size
}
@@ -41,84 +38,42 @@ impl VarEnv {
}
}
-impl NameEnv {
- pub fn new() -> Self {
- NameEnv { names: Vec::new() }
- }
- pub fn as_varenv(&self) -> VarEnv {
- VarEnv {
- size: self.names.len(),
- }
- }
-
- pub fn insert(&self, x: &Label) -> Self {
- let mut env = self.clone();
- env.insert_mut(x);
- env
- }
- pub fn insert_mut(&mut self, x: &Label) {
- self.names.push(x.clone())
- }
- pub fn remove_mut(&mut self) {
- self.names.pop();
- }
-
- pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
- let V(name, idx) = var;
- let (idx, _) = self
- .names
- .iter()
- .rev()
- .enumerate()
- .filter(|(_, n)| *n == name)
- .nth(*idx)?;
- Some(AlphaVar::new(idx))
- }
- pub fn label_var(&self, var: &AlphaVar) -> V {
- let name = &self.names[self.names.len() - 1 - var.idx()];
- let idx = self
- .names
- .iter()
- .rev()
- .take(var.idx())
- .filter(|n| *n == name)
- .count();
- V(name.clone(), idx)
- }
-}
-
impl TyEnv {
pub fn new() -> Self {
TyEnv {
names: NameEnv::new(),
- items: NzEnv::new(),
+ items: ValEnv::new(),
}
}
pub fn as_varenv(&self) -> VarEnv {
self.names.as_varenv()
}
- pub fn as_nzenv(&self) -> &NzEnv {
- &self.items
+ pub fn to_nzenv(&self) -> NzEnv {
+ self.items.discard_types()
}
pub fn as_nameenv(&self) -> &NameEnv {
&self.names
}
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+ pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
TyEnv {
names: self.names.insert(x),
- items: self.items.insert_type(t),
+ items: self.items.insert_type(ty),
}
}
- pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+ pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
TyEnv {
names: self.names.insert(x),
- items: self.items.insert_value(e),
+ items: self.items.insert_value(e, ty),
}
}
- pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
- let var = self.names.unlabel_var(var)?;
- let ty = self.items.lookup_ty(&var);
- Some((var, ty))
+ pub fn lookup(&self, var: &AlphaVar) -> Type {
+ self.items.lookup_ty(&var)
+ }
+}
+
+impl<'a> From<&'a TyEnv> for NzEnv {
+ fn from(x: &'a TyEnv) -> Self {
+ x.to_nzenv()
}
}
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 1df2a48..93c8f48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
pub mod env;
-pub mod tyexpr;
+pub mod tir;
pub mod typecheck;
pub(crate) use env::*;
-pub(crate) use tyexpr::*;
+pub(crate) use tir::*;
pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
new file mode 100644
index 0000000..aeb7bf9
--- /dev/null
+++ b/dhall/src/semantics/tck/tir.rs
@@ -0,0 +1,175 @@
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
+use crate::NormalizedExpr;
+
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+ val: Nir,
+ univ: Universe,
+}
+
+/// A hir expression plus its inferred type.
+/// Stands for "Typed intermediate representation"
+#[derive(Debug, Clone)]
+pub(crate) struct Tir<'hir> {
+ hir: &'hir Hir,
+ ty: Type,
+}
+
+impl Universe {
+ pub fn from_const(c: Const) -> Self {
+ Universe(match c {
+ Const::Type => 0,
+ Const::Kind => 1,
+ Const::Sort => 2,
+ })
+ }
+ pub fn as_const(self) -> Option<Const> {
+ match self.0 {
+ 0 => Some(Const::Type),
+ 1 => Some(Const::Kind),
+ 2 => Some(Const::Sort),
+ _ => None,
+ }
+ }
+ pub fn next(self) -> Self {
+ Universe(self.0 + 1)
+ }
+}
+
+impl Type {
+ pub fn new(val: Nir, univ: Universe) -> Self {
+ Type { val, univ }
+ }
+ /// Creates a new Type and infers its universe by re-typechecking its value.
+ /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
+ /// PiClosure.
+ pub fn new_infer_universe(
+ env: &TyEnv,
+ val: Nir,
+ ) -> Result<Self, TypeError> {
+ let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
+ let u = match c {
+ Some(c) => c.to_universe(),
+ None => unreachable!(
+ "internal type error: this is not a type: {:?}",
+ val
+ ),
+ };
+ Ok(Type::new(val, u))
+ }
+ pub fn from_const(c: Const) -> Self {
+ Self::new(Nir::from_const(c), c.to_universe().next())
+ }
+ pub fn from_builtin(b: Builtin) -> Self {
+ use Builtin::*;
+ match b {
+ Bool | Natural | Integer | Double | Text => {}
+ _ => unreachable!("this builtin is not a type: {}", b),
+ }
+
+ Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+ }
+
+ /// Get the type of this type
+ pub fn ty(&self) -> Universe {
+ self.univ
+ }
+
+ pub fn to_nir(&self) -> Nir {
+ self.val.clone()
+ }
+ pub fn as_nir(&self) -> &Nir {
+ &self.val
+ }
+ pub fn into_nir(self) -> Nir {
+ self.val
+ }
+ pub fn as_const(&self) -> Option<Const> {
+ self.val.as_const()
+ }
+ pub fn kind(&self) -> &NirKind {
+ self.val.kind()
+ }
+
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ self.val.to_hir(venv)
+ }
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+ }
+}
+
+impl<'hir> Tir<'hir> {
+ pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+ Tir { hir, ty }
+ }
+
+ pub fn span(&self) -> Span {
+ self.as_hir().span()
+ }
+ pub fn ty(&self) -> &Type {
+ &self.ty
+ }
+
+ pub fn to_hir(&self) -> Hir {
+ self.as_hir().clone()
+ }
+ pub fn as_hir(&self) -> &Hir {
+ &self.hir
+ }
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ self.as_hir().to_expr_tyenv(env)
+ }
+
+ /// Eval the Tir. It will actually get evaluated only as needed on demand.
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+ self.as_hir().eval(env.into())
+ }
+ pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+ if self.ty().as_const().is_none() {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Expected a type, found: `{}`",
+ self.to_expr_tyenv(env),
+ ))
+ .span_err(
+ self.span(),
+ format!(
+ "this has type: `{}`",
+ self.ty().to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "An expression in type position must have type `Type`, \
+ `Kind` or `Sort`",
+ ))
+ .format(),
+ );
+ }
+ Ok(())
+ }
+ /// Evaluate to a Type.
+ pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+ self.ensure_is_type(env)?;
+ Ok(Type::new(
+ self.eval(env),
+ self.ty()
+ .as_const()
+ .expect("case handled in ensure_is_type")
+ .to_universe(),
+ ))
+ }
+}
+
+impl From<Const> for Universe {
+ fn from(x: Const) -> Universe {
+ Universe::from_const(x)
+ }
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
deleted file mode 100644
index 1886646..0000000
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ /dev/null
@@ -1,137 +0,0 @@
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
-use crate::syntax::{ExprKind, Span, V};
-use crate::Normalized;
-use crate::{NormalizedExpr, ToExprOptions};
-
-pub(crate) type Type = Value;
-
-/// Stores an alpha-normalized variable.
-#[derive(Debug, Clone, Copy)]
-pub struct AlphaVar {
- idx: usize,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
- Var(AlphaVar),
- // Forbidden ExprKind variants: Var, Import, Embed
- Expr(ExprKind<TyExpr, Normalized>),
-}
-
-// An expression with inferred types at every node and resolved variables.
-#[derive(Clone)]
-pub(crate) struct TyExpr {
- kind: Box<TyExprKind>,
- ty: Option<Type>,
- span: Span,
-}
-
-impl AlphaVar {
- pub(crate) fn new(idx: usize) -> Self {
- AlphaVar { idx }
- }
- pub(crate) fn idx(&self) -> usize {
- self.idx
- }
-}
-
-impl TyExpr {
- pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
- TyExpr {
- kind: Box::new(kind),
- ty,
- span,
- }
- }
-
- pub fn kind(&self) -> &TyExprKind {
- &*self.kind
- }
- pub fn span(&self) -> Span {
- self.span.clone()
- }
- pub fn get_type(&self) -> Result<Type, TypeError> {
- match &self.ty {
- Some(t) => Ok(t.clone()),
- None => Err(TypeError::new(TypeMessage::Sort)),
- }
- }
-
- /// Converts a value back to the corresponding AST expression.
- pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- tyexpr_to_expr(self, opts, &mut NameEnv::new())
- }
- pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- let opts = ToExprOptions {
- normalize: true,
- alpha: false,
- };
- let mut env = env.as_nameenv().clone();
- tyexpr_to_expr(self, opts, &mut env)
- }
-
- /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
- pub fn eval(&self, env: &NzEnv) -> Value {
- Value::new_thunk(env, self.clone())
- }
- /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
- /// needed on demand.
- pub fn eval_closed_expr(&self) -> Value {
- self.eval(&NzEnv::new())
- }
- /// Eval a closed TyExpr fully and recursively;
- pub fn rec_eval_closed_expr(&self) -> Value {
- let mut val = self.eval_closed_expr();
- val.normalize_mut();
- val
- }
-}
-
-fn tyexpr_to_expr<'a>(
- tyexpr: &'a TyExpr,
- opts: ToExprOptions,
- env: &mut NameEnv,
-) -> NormalizedExpr {
- rc(match tyexpr.kind() {
- TyExprKind::Var(v) if opts.alpha => {
- ExprKind::Var(V("_".into(), v.idx()))
- }
- TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
- TyExprKind::Expr(e) => {
- let e = e.map_ref_maybe_binder(|l, tye| {
- if let Some(l) = l {
- env.insert_mut(l);
- }
- let e = tyexpr_to_expr(tye, opts, env);
- if let Some(_) = l {
- env.remove_mut();
- }
- e
- });
-
- match e {
- ExprKind::Lam(_, t, e) if opts.alpha => {
- ExprKind::Lam("_".into(), t, e)
- }
- ExprKind::Pi(_, t, e) if opts.alpha => {
- ExprKind::Pi("_".into(), t, e)
- }
- e => e,
- }
- }
- })
-}
-
-impl std::fmt::Debug for TyExpr {
- fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let mut x = fmt.debug_struct("TyExpr");
- x.field("kind", self.kind());
- if let Some(ty) = self.ty.as_ref() {
- x.field("type", &ty);
- } else {
- x.field("type", &None::<()>);
- }
- x.finish()
- }
-}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd9a8fa..972326b 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,34 +5,44 @@ use std::collections::HashMap;
use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::semantics::merge_maps;
use crate::semantics::{
- type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
- TyExprKind, Type, Value, ValueKind,
+ type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
+ NirKind, Tir, TyEnv, Type,
};
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
};
-use crate::Normalized;
-fn type_of_recordtype<'a>(
- span: Span,
- tys: impl Iterator<Item = Cow<'a, TyExpr>>,
-) -> Result<Type, TypeError> {
- let span_err = |msg: &str| {
- mkerr(
- ErrorBuilder::new(msg.to_string())
- .span_err(span.clone(), msg.to_string())
- .format(),
- )
+fn check_rectymerge(
+ span: &Span,
+ env: &TyEnv,
+ x: Nir,
+ y: Nir,
+) -> Result<(), TypeError> {
+ let kts_x = match x.kind() {
+ NirKind::RecordType(kts) => kts,
+ _ => {
+ return mk_span_err(
+ span.clone(),
+ "RecordTypeMergeRequiresRecordType",
+ )
+ }
};
- // An empty record type has type Type
- let mut k = Const::Type;
- for t in tys {
- match t.get_type()?.as_const() {
- Some(c) => k = max(k, c),
- None => return span_err("InvalidFieldType"),
+ let kts_y = match y.kind() {
+ NirKind::RecordType(kts) => kts,
+ _ => {
+ return mk_span_err(
+ span.clone(),
+ "RecordTypeMergeRequiresRecordType",
+ )
+ }
+ };
+ for (k, tx) in kts_x {
+ if let Some(ty) = kts_y.get(k) {
+ // TODO: store Type in RecordType ?
+ check_rectymerge(span, env, tx.clone(), ty.clone())?;
}
}
- Ok(Value::from_const(k))
+ Ok(())
}
fn function_check(a: Const, b: Const) -> Const {
@@ -43,90 +53,62 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
- Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
+ Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
+}
+
+pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
+ mkerr(
+ ErrorBuilder::new(msg.to_string())
+ .span_err(span, msg.to_string())
+ .format(),
+ )
}
/// When all sub-expressions have been typed, check the remaining toplevel
/// layer.
fn type_one_layer(
env: &TyEnv,
- ekind: ExprKind<TyExpr, Normalized>,
+ ekind: ExprKind<Tir<'_>>,
span: Span,
-) -> Result<TyExpr, TypeError> {
- let span_err = |msg: &str| {
- mkerr(
- ErrorBuilder::new(msg.to_string())
- .span_err(span.clone(), msg.to_string())
- .format(),
- )
- };
+) -> Result<Type, TypeError> {
+ let span_err = |msg: &str| mk_span_err(span.clone(), msg);
let ty = match &ekind {
- ExprKind::Import(..) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
+ ExprKind::Import(..) | ExprKind::Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
+ }
ExprKind::Var(..)
| ExprKind::Const(Const::Sort)
- | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
-
- ExprKind::Lam(binder, annot, body) => {
- let body_ty = body.get_type()?;
- let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
- let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
- type_one_layer(env, pi_ekind, Span::Artificial)?
- .eval(env.as_nzenv())
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..)
+ | ExprKind::Annot(..) => {
+ unreachable!("This case should have been handled in type_with")
}
- ExprKind::Pi(_, annot, body) => {
- let ks = match annot.get_type()?.as_const() {
- Some(k) => k,
- _ => {
- return mkerr(
- ErrorBuilder::new(format!(
- "Invalid input type: `{}`",
- annot.get_type()?.to_expr_tyenv(env),
- ))
- .span_err(
- annot.span(),
- format!(
- "this has type: `{}`",
- annot.get_type()?.to_expr_tyenv(env)
- ),
- )
- .help(format!(
- "The input type of a function must have type \
- `Type`, `Kind` or `Sort`",
- ))
- .format(),
- );
- }
- };
- let kt = match body.get_type()?.as_const() {
- Some(k) => k,
- _ => return span_err("Invalid output type"),
- };
- Value::from_const(function_check(ks, kt))
- }
- ExprKind::Let(_, _, _, body) => body.get_type()?,
-
- ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
- ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
+ ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
+ ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
ExprKind::Builtin(b) => {
- let t_expr = type_of_builtin(*b);
- let t_tyexpr = type_with(env, &t_expr)?;
- t_tyexpr.eval(env.as_nzenv())
- }
- ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
- ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
- ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
- ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
+ let t_hir = type_of_builtin(*b);
+ typecheck(&t_hir)?.eval_to_type(env)?
+ }
+ ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
+ ExprKind::Lit(LitKind::Natural(_)) => {
+ Type::from_builtin(Builtin::Natural)
+ }
+ ExprKind::Lit(LitKind::Integer(_)) => {
+ Type::from_builtin(Builtin::Integer)
+ }
+ ExprKind::Lit(LitKind::Double(_)) => {
+ Type::from_builtin(Builtin::Double)
+ }
ExprKind::TextLit(interpolated) => {
- let text_type = Value::from_builtin(Builtin::Text);
+ let text_type = Type::from_builtin(Builtin::Text);
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
- if x.get_type()? != text_type {
+ if *x.ty() != text_type {
return span_err("InvalidTextInterpolation");
}
}
@@ -134,9 +116,9 @@ fn type_one_layer(
text_type
}
ExprKind::EmptyListLit(t) => {
- let t = t.eval(env.as_nzenv());
- match &*t.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ let t = t.eval_to_type(env)?;
+ match t.kind() {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
@@ -149,49 +131,57 @@ fn type_one_layer(
let mut iter = xs.iter();
let x = iter.next().unwrap();
for y in iter {
- if x.get_type()? != y.get_type()? {
+ if x.ty() != y.ty() {
return span_err("InvalidListElement");
}
}
- let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
+ if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidListType");
}
- Value::from_builtin(Builtin::List).app(t)
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
}
ExprKind::SomeLit(x) => {
- let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
+ if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
- Value::from_builtin(Builtin::Optional).app(t)
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::Optional)
+ .app(t)
+ .to_type(Const::Type)
}
ExprKind::RecordLit(kvs) => {
use std::collections::hash_map::Entry;
let mut kts = HashMap::new();
+ // An empty record type has type Type
+ let mut k = Const::Type;
for (x, v) in kvs {
// Check for duplicated entries
match kts.entry(x.clone()) {
Entry::Occupied(_) => {
return span_err("RecordTypeDuplicateField")
}
- Entry::Vacant(e) => e.insert(v.get_type()?),
+ Entry::Vacant(e) => e.insert(v.ty().to_nir()),
};
+
+ // Check that the fields have a valid kind
+ match v.ty().ty().as_const() {
+ Some(c) => k = max(k, c),
+ None => return span_err("InvalidFieldType"),
+ }
}
- let ty = type_of_recordtype(
- span.clone(),
- kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
- )?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
let mut seen_fields = HashMap::new();
- for (x, _) in kts {
+ // An empty record type has type Type
+ let mut k = Const::Type;
+
+ for (x, t) in kts {
// Check for duplicated entries
match seen_fields.entry(x.clone()) {
Entry::Occupied(_) => {
@@ -199,12 +189,15 @@ fn type_one_layer(
}
Entry::Vacant(e) => e.insert(()),
};
+
+ // Check the type is a Const and compute final type
+ match t.ty().as_const() {
+ Some(c) => k = max(k, c),
+ None => return span_err("InvalidFieldType"),
+ }
}
- type_of_recordtype(
- span.clone(),
- kts.iter().map(|(_, t)| Cow::Borrowed(t)),
- )?
+ Type::from_const(k)
}
ExprKind::UnionType(kts) => {
use std::collections::hash_map::Entry;
@@ -213,7 +206,7 @@ fn type_one_layer(
let mut k = None;
for (x, t) in kts {
if let Some(t) = t {
- match (k, t.get_type()?.as_const()) {
+ match (k, t.ty().as_const()) {
(None, Some(k2)) => k = Some(k2),
(Some(k1), Some(k2)) if k1 == k2 => {}
_ => return span_err("InvalidFieldType"),
@@ -231,80 +224,52 @@ fn type_one_layer(
// an union type with only unary variants also has type Type
let k = k.unwrap_or(Const::Type);
- Value::from_const(k)
+ Type::from_const(k)
}
ExprKind::Field(scrut, x) => {
- match &*scrut.get_type()?.kind() {
- ValueKind::RecordType(kts) => match kts.get(&x) {
- Some(tth) => tth.clone(),
+ match scrut.ty().kind() {
+ NirKind::RecordType(kts) => match kts.get(&x) {
+ Some(val) => Type::new_infer_universe(env, val.clone())?,
None => return span_err("MissingRecordField"),
},
- // TODO: branch here only when scrut.get_type() is a Const
- _ => {
- let scrut_nf = scrut.eval(env.as_nzenv());
- match scrut_nf.kind() {
- ValueKind::UnionType(kts) => match kts.get(x) {
+ NirKind::Const(_) => {
+ let scrut = scrut.eval_to_type(env)?;
+ match scrut.kind() {
+ NirKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- // Can't fail because uniontypes must have type Const(_).
- let kt = scrut.get_type()?.as_const().unwrap();
- // The type of the field must be Const smaller than `kt`, thus the
- // function type has type `kt`.
- let pi_ty = Value::from_const(kt);
-
- Value::from_kind_and_type(
- ValueKind::PiClosure {
- binder: Binder::new(x.clone()),
- annot: ty.clone(),
- closure: Closure::new_constant(
- scrut_nf,
- ),
- },
- pi_ty,
- )
+ Nir::from_kind(NirKind::PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: ty.clone(),
+ closure: Closure::new_constant(
+ scrut.to_nir(),
+ ),
+ })
+ .to_type(scrut.ty())
}
- Some(None) => scrut_nf,
+ Some(None) => scrut,
None => return span_err("MissingUnionField"),
},
_ => return span_err("NotARecord"),
}
- } // _ => span_err("NotARecord"),
- }
- }
- ExprKind::Annot(x, t) => {
- let t = t.eval(env.as_nzenv());
- let x_ty = x.get_type()?;
- if x_ty != t {
- return span_err(&format!(
- "annot mismatch: ({} : {}) : {}",
- x.to_expr_tyenv(env),
- x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
- ));
- // return span_err(format!(
- // "annot mismatch: {} != {}",
- // x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- // t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
- // ));
- // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
+ }
+ _ => return span_err("NotARecord"),
}
- x_ty
}
ExprKind::Assert(t) => {
- let t = t.eval(env.as_nzenv());
- match &*t.kind() {
- ValueKind::Equivalence(x, y) if x == y => {}
- ValueKind::Equivalence(..) => {
- return span_err("AssertMismatch")
- }
+ let t = t.eval_to_type(env)?;
+ match t.kind() {
+ NirKind::Equivalence(x, y) if x == y => {}
+ NirKind::Equivalence(..) => return span_err("AssertMismatch"),
_ => return span_err("AssertMustTakeEquivalence"),
}
t
}
ExprKind::App(f, arg) => {
- match f.get_type()?.kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- if arg.get_type()? != *annot {
+ match f.ty().kind() {
+ // TODO: store Type in closure
+ NirKind::PiClosure { annot, closure, .. } => {
+ if arg.ty().as_nir() != annot {
return mkerr(
ErrorBuilder::new(format!(
"wrong type of function argument"
@@ -320,25 +285,25 @@ fn type_one_layer(
arg.span(),
format!(
"but this has type: {}",
- arg.get_type()?.to_expr_tyenv(env),
+ arg.ty().to_expr_tyenv(env),
),
)
.note(format!(
"expected type `{}`\n found type `{}`",
annot.to_expr_tyenv(env),
- arg.get_type()?.to_expr_tyenv(env),
+ arg.ty().to_expr_tyenv(env),
))
.format(),
);
}
- let arg_nf = arg.eval(env.as_nzenv());
- closure.apply(arg_nf)
+ let arg_nf = arg.eval(env);
+ Type::new_infer_universe(env, closure.apply(arg_nf))?
}
_ => return mkerr(
ErrorBuilder::new(format!(
"expected function, found `{}`",
- f.get_type()?.to_expr_tyenv(env)
+ f.ty().to_expr_tyenv(env)
))
.span_err(
f.span(),
@@ -349,33 +314,30 @@ fn type_one_layer(
}
}
ExprKind::BoolIf(x, y, z) => {
- if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
+ if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
- if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return span_err("IfBranchMustBeTerm");
- }
- if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ if y.ty().ty().as_const() != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
- if y.get_type()? != z.get_type()? {
+ if y.ty() != z.ty() {
return span_err("IfBranchMismatch");
}
- y.get_type()?
+ y.ty().clone()
}
ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
- let x_type = x.get_type()?;
- let y_type = y.get_type()?;
+ let x_type = x.ty();
+ let y_type = y.ty();
// Extract the LHS record type
let kts_x = match x_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("MustCombineRecord"),
};
// Extract the RHS record type
let kts_y = match y_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("MustCombineRecord"),
};
@@ -385,80 +347,59 @@ fn type_one_layer(
Ok(r_t.clone())
})?;
- // Construct the final record type
- let ty = type_of_recordtype(
- span.clone(),
- kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
- )?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ let u = max(x.ty().ty(), y.ty().ty());
+ Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
- let ekind = ExprKind::BinOp(
- BinOp::RecursiveRecordTypeMerge,
- x.get_type()?.to_tyexpr(env.as_varenv()),
- y.get_type()?.to_tyexpr(env.as_varenv()),
+ check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
+
+ let hir = Hir::new(
+ HirKind::Expr(ExprKind::BinOp(
+ BinOp::RecursiveRecordTypeMerge,
+ x.ty().to_hir(env.as_varenv()),
+ y.ty().to_hir(env.as_varenv()),
+ )),
+ span.clone(),
);
- type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
+ let x_u = x.ty().ty();
+ let y_u = y.ty().ty();
+ Type::new(hir.eval(env), max(x_u, y_u))
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
- let x_val = x.eval(env.as_nzenv());
- let y_val = y.eval(env.as_nzenv());
- let kts_x = match x_val.kind() {
- ValueKind::RecordType(kts) => kts,
- _ => return span_err("RecordTypeMergeRequiresRecordType"),
- };
- let kts_y = match y_val.kind() {
- ValueKind::RecordType(kts) => kts,
- _ => return span_err("RecordTypeMergeRequiresRecordType"),
- };
- for (k, tx) in kts_x {
- if let Some(ty) = kts_y.get(k) {
- type_one_layer(
- env,
- ExprKind::BinOp(
- BinOp::RecursiveRecordTypeMerge,
- tx.to_tyexpr(env.as_varenv()),
- ty.to_tyexpr(env.as_varenv()),
- ),
- Span::Artificial,
- )?;
- }
- }
+ check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
// A RecordType's type is always a const
- let xk = x.get_type()?.as_const().unwrap();
- let yk = y.get_type()?.as_const().unwrap();
- Value::from_const(max(xk, yk))
+ let xk = x.ty().as_const().unwrap();
+ let yk = y.ty().as_const().unwrap();
+ Type::from_const(max(xk, yk))
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
- let l_ty = l.get_type()?;
- match &*l_ty.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ match l.ty().kind() {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
..
}) => {}
_ => return span_err("BinOpTypeMismatch"),
}
- if l_ty != r.get_type()? {
+ if l.ty() != r.ty() {
return span_err("BinOpTypeMismatch");
}
- l_ty
+ l.ty().clone()
}
ExprKind::BinOp(BinOp::Equivalence, l, r) => {
- if l.get_type()? != r.get_type()? {
+ if l.ty() != r.ty() {
return span_err("EquivalenceTypeMismatch");
}
- if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ if l.ty().ty().as_const() != Some(Const::Type) {
return span_err("EquivalenceArgumentsMustBeTerms");
}
- Value::from_const(Const::Type)
+ Type::from_const(Const::Type)
}
ExprKind::BinOp(o, l, r) => {
- let t = Value::from_builtin(match o {
+ let t = Type::from_builtin(match o {
BinOp::BoolAnd
| BinOp::BoolOr
| BinOp::BoolEQ
@@ -473,27 +414,27 @@ fn type_one_layer(
BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
});
- if l.get_type()? != t {
+ if *l.ty() != t {
return span_err("BinOpTypeMismatch");
}
- if r.get_type()? != t {
+ if *r.ty() != t {
return span_err("BinOpTypeMismatch");
}
t
}
ExprKind::Merge(record, union, type_annot) => {
- let record_type = record.get_type()?;
+ let record_type = record.ty();
let handlers = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("Merge1ArgMustBeRecord"),
};
- let union_type = union.get_type()?;
+ let union_type = union.ty();
let variants = match union_type.kind() {
- ValueKind::UnionType(kts) => Cow::Borrowed(kts),
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::UnionType(kts) => Cow::Borrowed(kts),
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::Optional,
args,
..
@@ -509,10 +450,10 @@ fn type_one_layer(
let mut inferred_type = None;
for (x, handler_type) in handlers {
- let handler_return_type = match variants.get(x) {
+ let handler_return_type: Type = match variants.get(x) {
// Union alternative with type
Some(Some(variant_type)) => match handler_type.kind() {
- ValueKind::PiClosure { closure, annot, .. } => {
+ NirKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
return mkerr(
ErrorBuilder::new(format!(
@@ -543,8 +484,11 @@ fn type_one_layer(
);
}
+ // TODO: this actually doesn't check anything yet
match closure.remove_binder() {
- Ok(v) => v,
+ Ok(v) => {
+ Type::new_infer_universe(env, v.clone())?
+ }
Err(()) => {
return span_err(
"MergeReturnTypeIsDependent",
@@ -588,7 +532,9 @@ fn type_one_layer(
}
},
// Union alternative without type
- Some(None) => handler_type.clone(),
+ Some(None) => {
+ Type::new_infer_universe(env, handler_type.clone())?
+ }
None => return span_err("MergeHandlerMissingVariant"),
};
match &inferred_type {
@@ -606,8 +552,10 @@ fn type_one_layer(
}
}
- let type_annot =
- type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
+ let type_annot = type_annot
+ .as_ref()
+ .map(|t| t.eval_to_type(env))
+ .transpose()?;
match (inferred_type, type_annot) {
(Some(t1), Some(t2)) => {
if t1 != t2 {
@@ -621,9 +569,12 @@ fn type_one_layer(
}
}
ExprKind::ToMap(record, annot) => {
- let record_t = record.get_type()?;
+ if record.ty().ty().as_const() != Some(Const::Type) {
+ return span_err("`toMap` only accepts records of type `Type`");
+ }
+ let record_t = record.ty();
let kts = match record_t.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => {
return span_err("The argument to `toMap` must be a record")
}
@@ -638,12 +589,12 @@ fn type_one_layer(
annotation",
);
};
- let annot_val = annot.eval(env.as_nzenv());
+ let annot_val = annot.eval_to_type(env)?;
let err_msg = "The type of `toMap x` must be of the form \
`List { mapKey : Text, mapValue : T }`";
let arg = match annot_val.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
@@ -651,14 +602,14 @@ fn type_one_layer(
_ => return span_err(err_msg),
};
let kts = match arg.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err(err_msg),
};
if kts.len() != 2 {
return span_err(err_msg);
}
match kts.get(&"mapKey".into()) {
- Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+ Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
_ => return span_err(err_msg),
}
match kts.get(&"mapValue".into()) {
@@ -668,11 +619,6 @@ fn type_one_layer(
annot_val
} else {
let entry_type = kts.iter().next().unwrap().1.clone();
- if entry_type.get_type()?.as_const() != Some(Const::Type) {
- return span_err(
- "`toMap` only accepts records of type `Type`",
- );
- }
for (_, t) in kts.iter() {
if *t != entry_type {
return span_err(
@@ -682,16 +628,13 @@ fn type_one_layer(
}
let mut kts = HashMap::new();
- kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+ kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
kts.insert("mapValue".into(), entry_type);
- let output_type = Value::from_builtin(Builtin::List).app(
- Value::from_kind_and_type(
- ValueKind::RecordType(kts),
- Value::from_const(Const::Type),
- ),
- );
+ let output_type: Type = Nir::from_builtin(Builtin::List)
+ .app(Nir::from_kind(NirKind::RecordType(kts)))
+ .to_type(Const::Type);
if let Some(annot) = annot {
- let annot_val = annot.eval(env.as_nzenv());
+ let annot_val = annot.eval_to_type(env)?;
if output_type != annot_val {
return span_err("Annotation mismatch");
}
@@ -700,9 +643,9 @@ fn type_one_layer(
}
}
ExprKind::Projection(record, labels) => {
- let record_type = record.get_type()?;
+ let record_type = record.ty();
let kts = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
@@ -722,21 +665,21 @@ fn type_one_layer(
};
}
- Value::from_kind_and_type(
- ValueKind::RecordType(new_kts),
- record_type.get_type()?,
- )
+ Type::new_infer_universe(
+ env,
+ Nir::from_kind(NirKind::RecordType(new_kts)),
+ )?
}
ExprKind::ProjectionByExpr(record, selection) => {
- let record_type = record.get_type()?;
+ let record_type = record.ty();
let rec_kts = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
- let selection_val = selection.eval(env.as_nzenv());
+ let selection_val = selection.eval_to_type(env)?;
let sel_kts = match selection_val.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionByExprTakesRecordType"),
};
@@ -753,110 +696,119 @@ fn type_one_layer(
selection_val
}
- ExprKind::Completion(ty, compl) => {
- let ty_field_default = type_one_layer(
- env,
- ExprKind::Field(ty.clone(), "default".into()),
- span.clone(),
- )?;
- let ty_field_type = type_one_layer(
- env,
- ExprKind::Field(ty.clone(), "Type".into()),
- span.clone(),
- )?;
- let merge = type_one_layer(
- env,
- ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- ty_field_default,
- compl.clone(),
- ),
- span.clone(),
- )?;
- return type_one_layer(
- env,
- ExprKind::Annot(merge, ty_field_type),
- span.clone(),
- );
- }
};
- Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
+ Ok(ty)
}
-/// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(
+/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
+/// to compare with.
+pub(crate) fn type_with<'hir>(
env: &TyEnv,
- expr: &Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
- let (tyekind, ty) = match expr.as_ref() {
- ExprKind::Var(var) => match env.lookup(&var) {
- Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
- None => {
- return mkerr(
- ErrorBuilder::new(format!("unbound variable `{}`", var))
- .span_err(expr.span(), "not found in this scope")
- .format(),
- )
- }
- },
- ExprKind::Const(Const::Sort) => {
- (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
- }
- ExprKind::Embed(p) => {
- return Ok(p.clone().into_value().to_tyexpr_noenv())
- }
- ekind => {
- let ekind = match ekind {
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body_env = env.insert_type(binder, annot_nf);
- let body = type_with(&body_env, body)?;
- ExprKind::Lam(binder.clone(), annot, body)
- }
- ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body_env = env.insert_type(binder, annot_nf);
- let body = type_with(&body_env, body)?;
- ExprKind::Pi(binder.clone(), annot, body)
- }
- ExprKind::Let(binder, annot, val, body) => {
- let val = if let Some(t) = annot {
- t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
- } else {
- val.clone()
- };
- let val = type_with(env, &val)?;
- val.get_type()?; // Ensure val is not Sort
- let val_nf = val.eval(&env.as_nzenv());
- let body_env = env.insert_value(&binder, val_nf);
- let body = type_with(&body_env, body)?;
- ExprKind::Let(binder.clone(), None, val, body)
+ hir: &'hir Hir,
+ annot: Option<Type>,
+) -> Result<Tir<'hir>, TypeError> {
+ let tir = match hir.kind() {
+ HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
+ HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
+ HirKind::Expr(ExprKind::Var(_)) => {
+ unreachable!("Hir should contain no unresolved variables")
+ }
+ HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+ return mk_span_err(hir.span(), "Sort does not have a type")
+ }
+ HirKind::Expr(ExprKind::Annot(x, t)) => {
+ let t = match t.kind() {
+ HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+ Type::from_const(Const::Sort)
}
- _ => ekind.traverse_ref(|e| type_with(env, e))?,
+ _ => type_with(env, t, None)?.eval_to_type(env)?,
};
- return type_one_layer(env, ekind, expr.span());
+ type_with(env, x, Some(t))?
+ }
+
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+ let annot = type_with(env, annot, None)?;
+ let annot_nf = annot.eval_to_type(env)?;
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body, None)?;
+
+ let u_annot = annot.ty().as_const().unwrap();
+ let u_body = match body.ty().ty().as_const() {
+ Some(k) => k,
+ _ => return mk_span_err(hir.span(), "Invalid output type"),
+ };
+ let u = function_check(u_annot, u_body).to_universe();
+ let ty_hir = Hir::new(
+ HirKind::Expr(ExprKind::Pi(
+ binder.clone(),
+ annot.to_hir(),
+ body.ty().to_hir(body_env.as_varenv()),
+ )),
+ hir.span(),
+ );
+ let ty = Type::new(ty_hir.eval(env), u);
+
+ Tir::from_hir(hir, ty)
+ }
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ let annot = type_with(env, annot, None)?;
+ let annot_val = annot.eval_to_type(env)?;
+ let body_env = env.insert_type(binder, annot_val);
+ let body = type_with(&body_env, body, None)?;
+ body.ensure_is_type(env)?;
+
+ let ks = annot.ty().as_const().unwrap();
+ let kt = body.ty().as_const().unwrap();
+ let ty = Type::from_const(function_check(ks, kt));
+ Tir::from_hir(hir, ty)
+ }
+ HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
+ let val_annot = annot
+ .as_ref()
+ .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?))
+ .transpose()?;
+ let val = type_with(env, &val, val_annot)?;
+ let val_nf = val.eval(env);
+ let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
+ let body = type_with(&body_env, body, None)?;
+ let ty = body.ty().clone();
+ Tir::from_hir(hir, ty)
+ }
+ HirKind::Expr(ekind) => {
+ let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
+ let ty = type_one_layer(env, ekind, hir.span())?;
+ Tir::from_hir(hir, ty)
}
};
- Ok(TyExpr::new(tyekind, ty, expr.span()))
+ if let Some(annot) = annot {
+ if *tir.ty() != annot {
+ return mk_span_err(
+ hir.span(),
+ &format!(
+ "annot mismatch: {} != {}",
+ tir.ty().to_expr_tyenv(env),
+ annot.to_expr_tyenv(env)
+ ),
+ );
+ }
+ }
+
+ Ok(tir)
}
/// Typecheck an expression and return the expression annotated with types if type-checking
/// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
- let res = type_with(&TyEnv::new(), e)?;
- // Ensure that the inferred type exists (i.e. this is not Sort)
- res.get_type()?;
- Ok(res)
+pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
+ type_with(&TyEnv::new(), hir, None)
}
/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(
- expr: &Expr<Normalized>,
- ty: Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
- typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+pub(crate) fn typecheck_with<'hir>(
+ hir: &'hir Hir,
+ ty: Hir,
+) -> Result<Tir<'hir>, TypeError> {
+ let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
+ type_with(&TyEnv::new(), hir, Some(ty))
}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index b493fdb..a479b53 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,6 @@
+use crate::semantics::Universe;
use crate::syntax::map::{DupTreeMap, DupTreeSet};
-use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
+use crate::syntax::visitor;
use crate::syntax::*;
pub type Integer = isize;
@@ -18,6 +19,12 @@ pub enum Const {
Sort,
}
+impl Const {
+ pub(crate) fn to_universe(self) -> Universe {
+ Universe::from_const(self)
+ }
+}
+
/// Bound variable
///
/// The `Label` field is the variable's name (i.e. \"`x`\").
@@ -96,20 +103,34 @@ pub enum Builtin {
// Each node carries an annotation.
#[derive(Debug, Clone)]
-pub struct Expr<Embed> {
- kind: Box<ExprKind<Expr<Embed>, Embed>>,
+pub struct Expr {
+ kind: Box<ExprKind<Expr>>,
span: Span,
}
-pub type UnspannedExpr<Embed> = ExprKind<Expr<Embed>, Embed>;
+pub type UnspannedExpr = ExprKind<Expr>;
+
+/// Simple literals
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum LitKind {
+ /// `True`
+ Bool(bool),
+ /// `1`
+ Natural(Natural),
+ /// `+2`
+ Integer(Integer),
+ /// `3.24`
+ Double(Double),
+}
/// Syntax tree for expressions
// Having the recursion out of the enum definition enables writing
// much more generic code and improves pattern-matching behind
// smart pointers.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum ExprKind<SubExpr, Embed> {
+pub enum ExprKind<SubExpr> {
Const(Const),
+ Lit(LitKind),
/// `x`
/// `x@n`
Var(V),
@@ -131,16 +152,8 @@ pub enum ExprKind<SubExpr, Embed> {
Builtin(Builtin),
// Binary operations
BinOp(BinOp, SubExpr, SubExpr),
- /// `True`
- BoolLit(bool),
/// `if x then y else z`
BoolIf(SubExpr, SubExpr, SubExpr),
- /// `1`
- NaturalLit(Natural),
- /// `+2`
- IntegerLit(Integer),
- /// `3.24`
- DoubleLit(Double),
/// `"Some ${interpolated} text"`
TextLit(InterpolatedText<SubExpr>),
/// `[] : t`
@@ -169,29 +182,21 @@ pub enum ExprKind<SubExpr, Embed> {
Completion(SubExpr, SubExpr),
/// `./some/path`
Import(Import<SubExpr>),
- /// Embeds the result of resolving an import
- Embed(Embed),
}
-impl<SE, E> ExprKind<SE, E> {
+impl<SE> ExprKind<SE> {
pub fn traverse_ref_maybe_binder<'a, SE2, Err>(
&'a self,
visit: impl FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
- ) -> Result<ExprKind<SE2, E>, Err>
- where
- E: Clone,
- {
- visitor::TraverseRefMaybeBinderVisitor(visit).visit(self)
+ ) -> Result<ExprKind<SE2>, Err> {
+ visitor::visit_ref(self, visit)
}
pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>(
&'a self,
mut visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
mut visit_under_binder: impl FnMut(&'a Label, &'a SE) -> Result<SE2, Err>,
- ) -> Result<ExprKind<SE2, E>, Err>
- where
- E: Clone,
- {
+ ) -> Result<ExprKind<SE2>, Err> {
self.traverse_ref_maybe_binder(|l, x| match l {
None => visit_subexpr(x),
Some(l) => visit_under_binder(l, x),
@@ -201,27 +206,14 @@ impl<SE, E> ExprKind<SE, E> {
pub(crate) fn traverse_ref<'a, SE2, Err>(
&'a self,
mut visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
- ) -> Result<ExprKind<SE2, E>, Err>
- where
- E: Clone,
- {
+ ) -> Result<ExprKind<SE2>, Err> {
self.traverse_ref_maybe_binder(|_, e| visit_subexpr(e))
}
- fn traverse_mut<'a, Err>(
- &'a mut self,
- visit_subexpr: impl FnMut(&'a mut SE) -> Result<(), Err>,
- ) -> Result<(), Err> {
- visitor::TraverseMutVisitor { visit_subexpr }.visit(self)
- }
-
pub fn map_ref_maybe_binder<'a, SE2>(
&'a self,
mut map: impl FnMut(Option<&'a Label>, &'a SE) -> SE2,
- ) -> ExprKind<SE2, E>
- where
- E: Clone,
- {
+ ) -> ExprKind<SE2> {
trivial_result(self.traverse_ref_maybe_binder(|l, x| Ok(map(l, x))))
}
@@ -229,10 +221,7 @@ impl<SE, E> ExprKind<SE, E> {
&'a self,
mut map_subexpr: impl FnMut(&'a SE) -> SE2,
mut map_under_binder: impl FnMut(&'a Label, &'a SE) -> SE2,
- ) -> ExprKind<SE2, E>
- where
- E: Clone,
- {
+ ) -> ExprKind<SE2> {
self.map_ref_maybe_binder(|l, x| match l {
None => map_subexpr(x),
Some(l) => map_under_binder(l, x),
@@ -242,34 +231,30 @@ impl<SE, E> ExprKind<SE, E> {
pub fn map_ref<'a, SE2>(
&'a self,
mut map_subexpr: impl FnMut(&'a SE) -> SE2,
- ) -> ExprKind<SE2, E>
- where
- E: Clone,
- {
+ ) -> ExprKind<SE2> {
self.map_ref_maybe_binder(|_, e| map_subexpr(e))
}
-
- pub fn map_mut<'a>(&'a mut self, mut map_subexpr: impl FnMut(&'a mut SE)) {
- trivial_result(self.traverse_mut(|x| Ok(map_subexpr(x))))
- }
}
-impl<E> Expr<E> {
- pub fn as_ref(&self) -> &UnspannedExpr<E> {
+impl Expr {
+ pub fn as_ref(&self) -> &UnspannedExpr {
+ &self.kind
+ }
+ pub fn kind(&self) -> &UnspannedExpr {
&self.kind
}
pub fn span(&self) -> Span {
self.span.clone()
}
- pub fn new(kind: UnspannedExpr<E>, span: Span) -> Self {
+ pub fn new(kind: UnspannedExpr, span: Span) -> Self {
Expr {
kind: Box::new(kind),
span,
}
}
- pub fn rewrap<E2>(&self, kind: UnspannedExpr<E2>) -> Expr<E2> {
+ pub fn rewrap(&self, kind: UnspannedExpr) -> Expr {
Expr {
kind: Box::new(kind),
span: self.span.clone(),
@@ -281,43 +266,6 @@ impl<E> Expr<E> {
span,
}
}
-
- pub fn traverse_resolve_mut<Err, F1>(
- &mut self,
- f: &mut F1,
- ) -> Result<(), Err>
- where
- E: Clone,
- F1: FnMut(Import<Expr<E>>) -> Result<E, Err>,
- {
- match self.kind.as_mut() {
- ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
- let garbage_expr = ExprKind::BoolLit(false);
- let new_self = if l.traverse_resolve_mut(f).is_ok() {
- l
- } else {
- r.traverse_resolve_mut(f)?;
- r
- };
- *self.kind =
- std::mem::replace(new_self.kind.as_mut(), garbage_expr);
- }
- _ => {
- self.kind.traverse_mut(|e| e.traverse_resolve_mut(f))?;
- if let ExprKind::Import(import) = self.kind.as_mut() {
- let garbage_import = Import {
- mode: ImportMode::Code,
- location: ImportLocation::Missing,
- hash: None,
- };
- // Move out of &mut import
- let import = std::mem::replace(import, garbage_import);
- *self.kind = ExprKind::Embed(f(import)?);
- }
- }
- }
- Ok(())
- }
}
pub fn trivial_result<T>(x: Result<T, !>) -> T {
@@ -362,15 +310,15 @@ impl From<Label> for V {
}
}
-impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> {
+impl std::cmp::PartialEq for Expr {
fn eq(&self, other: &Self) -> bool {
self.kind == other.kind
}
}
-impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {}
+impl std::cmp::Eq for Expr {}
-impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> {
+impl std::hash::Hash for Expr {
fn hash<H>(&self, state: &mut H)
where
H: std::hash::Hasher,
diff --git a/dhall/src/syntax/ast/import.rs b/dhall/src/syntax/ast/import.rs
index da3e99b..7bde6e0 100644
--- a/dhall/src/syntax/ast/import.rs
+++ b/dhall/src/syntax/ast/import.rs
@@ -75,15 +75,6 @@ impl<SE> URL<SE> {
headers,
})
}
- pub fn traverse_mut<'a, Err>(
- &'a mut self,
- f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
- ) -> Result<(), Err> {
- if let Some(header) = &mut self.headers {
- f(header)?;
- }
- Ok(())
- }
}
impl<SE> ImportLocation<SE> {
@@ -99,15 +90,6 @@ impl<SE> ImportLocation<SE> {
Missing => Missing,
})
}
- pub fn traverse_mut<'a, Err>(
- &'a mut self,
- f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
- ) -> Result<(), Err> {
- if let ImportLocation::Remote(url) = self {
- url.traverse_mut(f)?;
- }
- Ok(())
- }
}
impl<SE> Import<SE> {
@@ -121,10 +103,4 @@ impl<SE> Import<SE> {
hash: self.hash.clone(),
})
}
- pub fn traverse_mut<'a, Err>(
- &'a mut self,
- f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
- ) -> Result<(), Err> {
- self.location.traverse_mut(f)
- }
}
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index 6a1ce7d..c361bc1 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -2,343 +2,112 @@ use std::iter::FromIterator;
use crate::syntax::*;
-/// A visitor trait that can be used to traverse `ExprKind`s. We need this pattern so that Rust lets
-/// us have as much mutability as we can.
-/// For example, `traverse_ref_with_special_handling_of_binders` cannot be made using only
-/// `traverse_ref`, because `traverse_ref` takes a `FnMut` so we would need to pass multiple
-/// mutable reverences to this argument to `traverse_ref`. But Rust's ownership system is all about
-/// preventing exactly this ! So we have to be more clever. The visitor pattern allows us to have
-/// only one mutable thing the whole time: the visitor itself. The visitor can then carry around
-/// multiple closures or just one, and Rust is ok with either. See for example TraverseRefVisitor.
-pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized {
- type Error;
-
- fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error>;
- fn visit_embed(self, embed: &'a E1) -> Result<E2, Self::Error>;
-
- fn visit_subexpr_under_binder(
- mut self,
- _label: &'a Label,
- subexpr: &'a SE1,
- ) -> Result<SE2, Self::Error> {
- self.visit_subexpr(subexpr)
- }
-
- fn visit(
- self,
- input: &'a ExprKind<SE1, E1>,
- ) -> Result<ExprKind<SE2, E2>, Self::Error> {
- visit_ref(self, input)
- }
+fn vec<'a, T, U, Err>(
+ x: &'a [T],
+ f: impl FnMut(&'a T) -> Result<U, Err>,
+) -> Result<Vec<U>, Err> {
+ x.iter().map(f).collect()
}
-/// Like `ExprKindVisitor`, but by mutable reference
-pub trait ExprKindMutVisitor<'a, SE, E>: Sized {
- type Error;
-
- fn visit_subexpr(&mut self, subexpr: &'a mut SE)
- -> Result<(), Self::Error>;
- fn visit_embed(self, _embed: &'a mut E) -> Result<(), Self::Error> {
- Ok(())
- }
-
- fn visit_subexpr_under_binder(
- mut self,
- _label: &'a mut Label,
- subexpr: &'a mut SE,
- ) -> Result<(), Self::Error> {
- self.visit_subexpr(subexpr)
- }
+fn opt<'a, T, U, Err>(
+ x: &'a Option<T>,
+ f: impl FnOnce(&'a T) -> Result<U, Err>,
+) -> Result<Option<U>, Err> {
+ Ok(match x {
+ Some(x) => Some(f(x)?),
+ None => None,
+ })
+}
- fn visit(self, input: &'a mut ExprKind<SE, E>) -> Result<(), Self::Error> {
- visit_mut(self, input)
- }
+fn dupmap<'a, SE1, SE2, T, Err>(
+ x: impl IntoIterator<Item = (&'a Label, &'a SE1)>,
+ mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>,
+) -> Result<T, Err>
+where
+ SE1: 'a,
+ T: FromIterator<(Label, SE2)>,
+{
+ x.into_iter().map(|(k, x)| Ok((k.clone(), f(x)?))).collect()
}
-fn visit_ref<'a, V, SE1, SE2, E1, E2>(
- mut v: V,
- input: &'a ExprKind<SE1, E1>,
-) -> Result<ExprKind<SE2, E2>, V::Error>
+fn optdupmap<'a, SE1, SE2, T, Err>(
+ x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
+ mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>,
+) -> Result<T, Err>
where
- V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
+ SE1: 'a,
+ T: FromIterator<(Label, Option<SE2>)>,
{
- fn vec<'a, T, U, Err, F: FnMut(&'a T) -> Result<U, Err>>(
- x: &'a [T],
- f: F,
- ) -> Result<Vec<U>, Err> {
- x.iter().map(f).collect()
- }
- fn opt<'a, T, U, Err, F: FnOnce(&'a T) -> Result<U, Err>>(
- x: &'a Option<T>,
- f: F,
- ) -> Result<Option<U>, Err> {
- Ok(match x {
- Some(x) => Some(f(x)?),
- None => None,
+ x.into_iter()
+ .map(|(k, x)| {
+ Ok((
+ k.clone(),
+ match x {
+ Some(x) => Some(f(x)?),
+ None => None,
+ },
+ ))
})
- }
- fn dupmap<'a, V, SE1, SE2, E1, E2, T>(
- x: impl IntoIterator<Item = (&'a Label, &'a SE1)>,
- mut v: V,
- ) -> Result<T, V::Error>
- where
- SE1: 'a,
- T: FromIterator<(Label, SE2)>,
- V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
- {
- x.into_iter()
- .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
- .collect()
- }
- fn optdupmap<'a, V, SE1, SE2, E1, E2, T>(
- x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
- mut v: V,
- ) -> Result<T, V::Error>
- where
- SE1: 'a,
- T: FromIterator<(Label, Option<SE2>)>,
- V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
- {
- x.into_iter()
- .map(|(k, x)| {
- Ok((
- k.clone(),
- match x {
- Some(x) => Some(v.visit_subexpr(x)?),
- None => None,
- },
- ))
- })
- .collect()
+ .collect()
+}
+
+pub(crate) fn visit_ref<'a, F, SE1, SE2, Err>(
+ input: &'a ExprKind<SE1>,
+ mut f: F,
+) -> Result<ExprKind<SE2>, Err>
+where
+ F: FnMut(Option<&'a Label>, &'a SE1) -> Result<SE2, Err>,
+{
+ // Can't use closures because of borrowing rules
+ macro_rules! expr {
+ ($e:expr) => {
+ f(None, $e)
+ };
+ ($l:expr, $e:expr) => {
+ f(Some($l), $e)
+ };
}
use crate::syntax::ExprKind::*;
Ok(match input {
Var(v) => Var(v.clone()),
Lam(l, t, e) => {
- let t = v.visit_subexpr(t)?;
- let e = v.visit_subexpr_under_binder(l, e)?;
+ let t = expr!(t)?;
+ let e = expr!(l, e)?;
Lam(l.clone(), t, e)
}
Pi(l, t, e) => {
- let t = v.visit_subexpr(t)?;
- let e = v.visit_subexpr_under_binder(l, e)?;
+ let t = expr!(t)?;
+ let e = expr!(l, e)?;
Pi(l.clone(), t, e)
}
Let(l, t, a, e) => {
- let t = opt(t, &mut |e| v.visit_subexpr(e))?;
- let a = v.visit_subexpr(a)?;
- let e = v.visit_subexpr_under_binder(l, e)?;
+ let t = opt(t, &mut |e| expr!(e))?;
+ let a = expr!(a)?;
+ let e = expr!(l, e)?;
Let(l.clone(), t, a, e)
}
- App(f, a) => App(v.visit_subexpr(f)?, v.visit_subexpr(a)?),
- Annot(x, t) => Annot(v.visit_subexpr(x)?, v.visit_subexpr(t)?),
+ App(f, a) => App(expr!(f)?, expr!(a)?),
+ Annot(x, t) => Annot(expr!(x)?, expr!(t)?),
Const(k) => Const(*k),
Builtin(v) => Builtin(*v),
- BoolLit(b) => BoolLit(*b),
- NaturalLit(n) => NaturalLit(*n),
- IntegerLit(n) => IntegerLit(*n),
- DoubleLit(n) => DoubleLit(*n),
- TextLit(t) => TextLit(t.traverse_ref(|e| v.visit_subexpr(e))?),
- BinOp(o, x, y) => BinOp(*o, v.visit_subexpr(x)?, v.visit_subexpr(y)?),
- BoolIf(b, t, f) => BoolIf(
- v.visit_subexpr(b)?,
- v.visit_subexpr(t)?,
- v.visit_subexpr(f)?,
- ),
- EmptyListLit(t) => EmptyListLit(v.visit_subexpr(t)?),
- NEListLit(es) => NEListLit(vec(es, |e| v.visit_subexpr(e))?),
- SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
- RecordType(kts) => RecordType(dupmap(kts, v)?),
- RecordLit(kvs) => RecordLit(dupmap(kvs, v)?),
- UnionType(kts) => UnionType(optdupmap(kts, v)?),
- Merge(x, y, t) => Merge(
- v.visit_subexpr(x)?,
- v.visit_subexpr(y)?,
- opt(t, |e| v.visit_subexpr(e))?,
- ),
- ToMap(x, t) => {
- ToMap(v.visit_subexpr(x)?, opt(t, |e| v.visit_subexpr(e))?)
- }
- Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
- Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
- ProjectionByExpr(e, x) => {
- ProjectionByExpr(v.visit_subexpr(e)?, v.visit_subexpr(x)?)
- }
- Completion(e, x) => {
- Completion(v.visit_subexpr(e)?, v.visit_subexpr(x)?)
- }
- Assert(e) => Assert(v.visit_subexpr(e)?),
- Import(i) => Import(i.traverse_ref(|e| v.visit_subexpr(e))?),
- Embed(a) => Embed(v.visit_embed(a)?),
+ Lit(l) => Lit(l.clone()),
+ TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?),
+ BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?),
+ BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?),
+ EmptyListLit(t) => EmptyListLit(expr!(t)?),
+ NEListLit(es) => NEListLit(vec(es, |e| expr!(e))?),
+ SomeLit(e) => SomeLit(expr!(e)?),
+ RecordType(kts) => RecordType(dupmap(kts, |e| expr!(e))?),
+ RecordLit(kvs) => RecordLit(dupmap(kvs, |e| expr!(e))?),
+ UnionType(kts) => UnionType(optdupmap(kts, |e| expr!(e))?),
+ Merge(x, y, t) => Merge(expr!(x)?, expr!(y)?, opt(t, |e| expr!(e))?),
+ ToMap(x, t) => ToMap(expr!(x)?, opt(t, |e| expr!(e))?),
+ Field(e, l) => Field(expr!(e)?, l.clone()),
+ Projection(e, ls) => Projection(expr!(e)?, ls.clone()),
+ ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e)?, expr!(x)?),
+ Completion(e, x) => Completion(expr!(e)?, expr!(x)?),
+ Assert(e) => Assert(expr!(e)?),
+ Import(i) => Import(i.traverse_ref(|e| expr!(e))?),
})
}
-
-fn visit_mut<'a, V, SE, E>(
- mut v: V,
- input: &'a mut ExprKind<SE, E>,
-) -> Result<(), V::Error>
-where
- V: ExprKindMutVisitor<'a, SE, E>,
-{
- fn vec<'a, V, SE, E>(v: &mut V, x: &'a mut Vec<SE>) -> Result<(), V::Error>
- where
- V: ExprKindMutVisitor<'a, SE, E>,
- {
- for x in x {
- v.visit_subexpr(x)?;
- }
- Ok(())
- }
- fn opt<'a, V, SE, E>(
- v: &mut V,
- x: &'a mut Option<SE>,
- ) -> Result<(), V::Error>
- where
- V: ExprKindMutVisitor<'a, SE, E>,
- {
- if let Some(x) = x {
- v.visit_subexpr(x)?;
- }
- Ok(())
- }
- fn dupmap<'a, V, SE, E>(
- mut v: V,
- x: impl IntoIterator<Item = (&'a Label, &'a mut SE)>,
- ) -> Result<(), V::Error>
- where
- SE: 'a,
- V: ExprKindMutVisitor<'a, SE, E>,
- {
- for (_, x) in x {
- v.visit_subexpr(x)?;
- }
- Ok(())
- }
- fn optdupmap<'a, V, SE, E>(
- mut v: V,
- x: impl IntoIterator<Item = (&'a Label, &'a mut Option<SE>)>,
- ) -> Result<(), V::Error>
- where
- SE: 'a,
- V: ExprKindMutVisitor<'a, SE, E>,
- {
- for (_, x) in x {
- opt(&mut v, x)?;
- }
- Ok(())
- }
-
- use crate::syntax::ExprKind::*;
- match input {
- Var(_) | Const(_) | Builtin(_) | BoolLit(_) | NaturalLit(_)
- | IntegerLit(_) | DoubleLit(_) => {}
- Lam(l, t, e) => {
- v.visit_subexpr(t)?;
- v.visit_subexpr_under_binder(l, e)?;
- }
- Pi(l, t, e) => {
- v.visit_subexpr(t)?;
- v.visit_subexpr_under_binder(l, e)?;
- }
- Let(l, t, a, e) => {
- opt(&mut v, t)?;
- v.visit_subexpr(a)?;
- v.visit_subexpr_under_binder(l, e)?;
- }
- App(f, a) => {
- v.visit_subexpr(f)?;
- v.visit_subexpr(a)?;
- }
- Annot(x, t) => {
- v.visit_subexpr(x)?;
- v.visit_subexpr(t)?;
- }
- TextLit(t) => t.traverse_mut(|e| v.visit_subexpr(e))?,
- BinOp(_, x, y) => {
- v.visit_subexpr(x)?;
- v.visit_subexpr(y)?;
- }
- BoolIf(b, t, f) => {
- v.visit_subexpr(b)?;
- v.visit_subexpr(t)?;
- v.visit_subexpr(f)?;
- }
- EmptyListLit(t) => v.visit_subexpr(t)?,
- NEListLit(es) => vec(&mut v, es)?,
- SomeLit(e) => v.visit_subexpr(e)?,
- RecordType(kts) => dupmap(v, kts)?,
- RecordLit(kvs) => dupmap(v, kvs)?,
- UnionType(kts) => optdupmap(v, kts)?,
- Merge(x, y, t) => {
- v.visit_subexpr(x)?;
- v.visit_subexpr(y)?;
- opt(&mut v, t)?;
- }
- ToMap(x, t) => {
- v.visit_subexpr(x)?;
- opt(&mut v, t)?;
- }
- Field(e, _) => v.visit_subexpr(e)?,
- Projection(e, _) => v.visit_subexpr(e)?,
- ProjectionByExpr(e, x) => {
- v.visit_subexpr(e)?;
- v.visit_subexpr(x)?;
- }
- Completion(x, y) => {
- v.visit_subexpr(x)?;
- v.visit_subexpr(y)?;
- }
- Assert(e) => v.visit_subexpr(e)?,
- Import(i) => i.traverse_mut(|e| v.visit_subexpr(e))?,
- Embed(a) => v.visit_embed(a)?,
- }
- Ok(())
-}
-
-pub struct TraverseRefMaybeBinderVisitor<F>(pub F);
-
-impl<'a, SE, E, SE2, Err, F> ExprKindVisitor<'a, SE, SE2, E, E>
- for TraverseRefMaybeBinderVisitor<F>
-where
- SE: 'a,
- E: 'a + Clone,
- F: FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
-{
- type Error = Err;
-
- fn visit_subexpr(&mut self, subexpr: &'a SE) -> Result<SE2, Self::Error> {
- (self.0)(None, subexpr)
- }
- fn visit_subexpr_under_binder(
- mut self,
- label: &'a Label,
- subexpr: &'a SE,
- ) -> Result<SE2, Self::Error> {
- (self.0)(Some(label), subexpr)
- }
- fn visit_embed(self, embed: &'a E) -> Result<E, Self::Error> {
- Ok(embed.clone())
- }
-}
-
-pub struct TraverseMutVisitor<F1> {
- pub visit_subexpr: F1,
-}
-
-impl<'a, SE, E, Err, F1> ExprKindMutVisitor<'a, SE, E>
- for TraverseMutVisitor<F1>
-where
- SE: 'a,
- E: 'a,
- F1: FnMut(&'a mut SE) -> Result<(), Err>,
-{
- type Error = Err;
-
- fn visit_subexpr(
- &mut self,
- subexpr: &'a mut SE,
- ) -> Result<(), Self::Error> {
- (self.visit_subexpr)(subexpr)
- }
-}
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 52b699c..2e50d61 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -6,8 +6,8 @@ use crate::error::DecodeError;
use crate::syntax;
use crate::syntax::{
Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
- Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr,
- URL, V,
+ Integer, InterpolatedText, Label, LitKind, Natural, Scheme, Span,
+ UnspannedExpr, URL, V,
};
use crate::DecodedExpr;
@@ -19,7 +19,7 @@ pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
}
// Should probably rename this
-fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+fn rc(x: UnspannedExpr) -> Expr {
Expr::new(x, Span::Decoded)
}
@@ -31,8 +31,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
String(s) => match Builtin::parse(s) {
Some(b) => ExprKind::Builtin(b),
None => match s.as_str() {
- "True" => BoolLit(true),
- "False" => BoolLit(false),
+ "True" => Lit(LitKind::Bool(true)),
+ "False" => Lit(LitKind::Bool(false)),
"Type" => Const(Const::Type),
"Kind" => Const(Const::Kind),
"Sort" => Const(Const::Sort),
@@ -40,8 +40,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
},
},
U64(n) => Var(V(Label::from("_"), *n as usize)),
- F64(x) => DoubleLit((*x).into()),
- Bool(b) => BoolLit(*b),
+ F64(x) => Lit(LitKind::Double((*x).into())),
+ Bool(b) => Lit(LitKind::Bool(*b)),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
if l.as_str() == "_" {
@@ -216,9 +216,9 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
let z = cbor_value_to_dhall(&z)?;
BoolIf(x, y, z)
}
- [U64(15), U64(x)] => NaturalLit(*x as Natural),
- [U64(16), U64(x)] => IntegerLit(*x as Integer),
- [U64(16), I64(x)] => IntegerLit(*x as Integer),
+ [U64(15), U64(x)] => Lit(LitKind::Natural(*x as Natural)),
+ [U64(16), U64(x)] => Lit(LitKind::Integer(*x as Integer)),
+ [U64(16), I64(x)] => Lit(LitKind::Integer(*x as Integer)),
[U64(18), String(first), rest @ ..] => {
TextLit(InterpolatedText::from((
first.clone(),
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 5e79f2d..291ac4a 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -9,17 +9,16 @@ use crate::syntax::{
Label, Scheme, V,
};
-/// Warning: will fail if `expr` contains an `Embed` node.
-pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
+pub(crate) fn encode(expr: &Expr) -> Result<Vec<u8>, EncodeError> {
serde_cbor::ser::to_vec(&Serialize::Expr(expr))
.map_err(|e| EncodeError::CBORError(e))
}
-enum Serialize<'a, E> {
- Expr(&'a Expr<E>),
+enum Serialize<'a> {
+ Expr(&'a Expr),
CBOR(cbor::Value),
- RecordMap(&'a DupTreeMap<Label, Expr<E>>),
- UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>),
+ RecordMap(&'a DupTreeMap<Label, Expr>),
+ UnionMap(&'a DupTreeMap<Label, Option<Expr>>),
}
macro_rules! count {
@@ -39,7 +38,7 @@ macro_rules! ser_seq {
}};
}
-fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error>
+fn serialize_subexpr<S>(ser: S, e: &Expr) -> Result<S::Ok, S::Error>
where
S: serde::ser::Serializer,
{
@@ -47,13 +46,14 @@ where
use std::iter::once;
use syntax::Builtin;
use syntax::ExprKind::*;
+ use syntax::LitKind::*;
use self::Serialize::{RecordMap, UnionMap};
- fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
+ fn expr(x: &Expr) -> self::Serialize<'_> {
self::Serialize::Expr(x)
}
let cbor =
- |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) };
+ |v: cbor::Value| -> self::Serialize<'_> { self::Serialize::CBOR(v) };
let tag = |x: u64| cbor(U64(x));
let null = || cbor(cbor::Value::Null);
let label = |l: &Label| cbor(cbor::Value::String(l.into()));
@@ -61,10 +61,10 @@ where
match e.as_ref() {
Const(c) => ser.serialize_str(&c.to_string()),
Builtin(b) => ser.serialize_str(&b.to_string()),
- BoolLit(b) => ser.serialize_bool(*b),
- NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)),
- IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)),
- DoubleLit(n) => {
+ Lit(Bool(b)) => ser.serialize_bool(*b),
+ Lit(Natural(n)) => ser_seq!(ser; tag(15), U64(*n as u64)),
+ Lit(Integer(n)) => ser_seq!(ser; tag(16), I64(*n as i64)),
+ Lit(Double(n)) => {
let n: f64 = (*n).into();
ser.serialize_f64(n)
}
@@ -166,16 +166,10 @@ where
}
Completion(x, y) => ser_seq!(ser; tag(3), tag(13), expr(x), expr(y)),
Import(import) => serialize_import(ser, import),
- Embed(_) => unimplemented!(
- "An expression with resolved imports cannot be binary-encoded"
- ),
}
}
-fn serialize_import<S, E>(
- ser: S,
- import: &Import<Expr<E>>,
-) -> Result<S::Ok, S::Error>
+fn serialize_import<S>(ser: S, import: &Import<Expr>) -> Result<S::Ok, S::Error>
where
S: serde::ser::Serializer,
{
@@ -256,7 +250,7 @@ where
ser_seq.end()
}
-impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
+impl<'a> serde::ser::Serialize for Serialize<'a> {
fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
where
S: serde::ser::Serializer,
@@ -282,10 +276,8 @@ impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
}
}
-fn collect_nested_applications<'a, E>(
- e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<&'a Expr<E>>) {
- fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> {
+fn collect_nested_applications<'a>(e: &'a Expr) -> (&'a Expr, Vec<&'a Expr>) {
+ fn go<'a>(e: &'a Expr, vec: &mut Vec<&'a Expr>) -> &'a Expr {
match e.as_ref() {
ExprKind::App(f, a) => {
vec.push(a);
@@ -299,15 +291,10 @@ fn collect_nested_applications<'a, E>(
(e, vec)
}
-type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>);
+type LetBinding<'a> = (&'a Label, &'a Option<Expr>, &'a Expr);
-fn collect_nested_lets<'a, E>(
- e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) {
- fn go<'a, E>(
- e: &'a Expr<E>,
- vec: &mut Vec<LetBinding<'a, E>>,
- ) -> &'a Expr<E> {
+fn collect_nested_lets<'a>(e: &'a Expr) -> (&'a Expr, Vec<LetBinding<'a>>) {
+ fn go<'a>(e: &'a Expr, vec: &mut Vec<LetBinding<'a>>) -> &'a Expr {
match e.as_ref() {
ExprKind::Let(l, t, v, e) => {
vec.push((l, t, v));
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 8d571c0..f3ebd2b 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -5,23 +5,20 @@ use std::rc::Rc;
use pest_consume::{match_nodes, Parser};
-use crate::syntax;
use crate::syntax::map::{DupTreeMap, DupTreeSet};
use crate::syntax::ExprKind::*;
+use crate::syntax::LitKind::*;
use crate::syntax::{
- Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer,
- InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural,
- Scheme, Span, URL, V,
+ Double, Expr, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
+ Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble,
+ Natural, Scheme, Span, UnspannedExpr, URL, V,
};
-use crate::Normalized;
// This file consumes the parse tree generated by pest and turns it into
// our own AST. All those custom macros should eventually moved into
// their own crate because they are quite general and useful. For now they
// are here and hopefully you can figure out how they work.
-type Expr = syntax::Expr<Normalized>;
-type UnspannedExpr = syntax::UnspannedExpr<Normalized>;
type ParsedText = InterpolatedText<Expr>;
type ParsedTextContents = InterpolatedTextContents<Expr>;
type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc<str>>;
@@ -348,8 +345,8 @@ impl DhallParser {
let e = match crate::syntax::Builtin::parse(s) {
Some(b) => Builtin(b),
None => match s {
- "True" => BoolLit(true),
- "False" => BoolLit(false),
+ "True" => Lit(Bool(true)),
+ "False" => Lit(Bool(false)),
"Type" => Const(crate::syntax::Const::Type),
"Kind" => Const(crate::syntax::Const::Kind),
"Sort" => Const(crate::syntax::Const::Sort),
@@ -837,9 +834,9 @@ impl DhallParser {
#[alias(expression, shortcut = true)]
fn primitive_expression(input: ParseInput) -> ParseResult<Expr> {
Ok(match_nodes!(input.children();
- [double_literal(n)] => spanned(input, DoubleLit(n)),
- [natural_literal(n)] => spanned(input, NaturalLit(n)),
- [integer_literal(n)] => spanned(input, IntegerLit(n)),
+ [double_literal(n)] => spanned(input, Lit(Double(n))),
+ [natural_literal(n)] => spanned(input, Lit(Natural(n))),
+ [integer_literal(n)] => spanned(input, Lit(Integer(n))),
[double_quote_literal(s)] => spanned(input, TextLit(s)),
[single_quote_literal(s)] => spanned(input, TextLit(s)),
[record_type_or_literal(e)] => spanned(input, e),
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 06dd70f..8891d41 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -19,17 +19,17 @@ enum PrintPhase {
// Wraps an Expr with a phase, so that phase selection can be done separate from the actual
// printing.
#[derive(Clone)]
-struct PhasedExpr<'a, E>(&'a Expr<E>, PrintPhase);
+struct PhasedExpr<'a>(&'a Expr, PrintPhase);
-impl<'a, E: Display + Clone> PhasedExpr<'a, E> {
- fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, E> {
+impl<'a> PhasedExpr<'a> {
+ fn phase(self, phase: PrintPhase) -> PhasedExpr<'a> {
PhasedExpr(self.0, phase)
}
}
-impl<E: Display + Clone> UnspannedExpr<E> {
+impl UnspannedExpr {
// Annotate subexpressions with the appropriate phase, defaulting to Base
- fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a, E>, E> {
+ fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a>> {
use crate::syntax::ExprKind::*;
use PrintPhase::*;
let with_base = self.map_ref(|e| PhasedExpr(e, Base));
@@ -134,7 +134,7 @@ where
}
/// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
+impl<SE: Display + Clone> Display for ExprKind<SE> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
use crate::syntax::ExprKind::*;
match self {
@@ -196,15 +196,7 @@ impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
Var(a) => a.fmt(f)?,
Const(k) => k.fmt(f)?,
Builtin(v) => v.fmt(f)?,
- BoolLit(true) => f.write_str("True")?,
- BoolLit(false) => f.write_str("False")?,
- NaturalLit(a) => a.fmt(f)?,
- IntegerLit(a) if *a >= 0 => {
- f.write_str("+")?;
- a.fmt(f)?;
- }
- IntegerLit(a) => a.fmt(f)?,
- DoubleLit(a) => a.fmt(f)?,
+ Lit(a) => a.fmt(f)?,
TextLit(a) => a.fmt(f)?,
RecordType(a) if a.is_empty() => f.write_str("{}")?,
RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| {
@@ -232,19 +224,36 @@ impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
write!(f, "{}::{}", a, b)?;
}
Import(a) => a.fmt(f)?,
- Embed(a) => a.fmt(f)?,
}
Ok(())
}
}
-impl<E: Display + Clone> Display for Expr<E> {
+impl Display for Expr {
+ fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+ self.kind().fmt_phase(f, PrintPhase::Base)
+ }
+}
+
+impl Display for LitKind {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- self.as_ref().fmt_phase(f, PrintPhase::Base)
+ use LitKind::*;
+ match self {
+ Bool(true) => f.write_str("True")?,
+ Bool(false) => f.write_str("False")?,
+ Natural(a) => a.fmt(f)?,
+ Integer(a) if *a >= 0 => {
+ f.write_str("+")?;
+ a.fmt(f)?;
+ }
+ Integer(a) => a.fmt(f)?,
+ Double(a) => a.fmt(f)?,
+ }
+ Ok(())
}
}
-impl<'a, E: Display + Clone> Display for PhasedExpr<'a, E> {
+impl<'a> Display for PhasedExpr<'a> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
self.0.as_ref().fmt_phase(f, self.1)
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 6a67ddc..482f9ae 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -48,9 +48,9 @@ use std::fs::{create_dir_all, read_to_string, File};
use std::io::{Read, Write};
use std::path::PathBuf;
-use crate::error::{Error, Result};
+use crate::error::{Error, ErrorKind, Result};
use crate::syntax::binary;
-use crate::{Normalized, NormalizedExpr, Parsed, Resolved};
+use crate::{Normalized, NormalizedExpr, Parsed, Resolved, Typed};
#[allow(dead_code)]
enum Test {
@@ -96,9 +96,13 @@ impl TestFile {
pub fn resolve(&self) -> Result<Resolved> {
Ok(self.parse()?.resolve()?)
}
+ /// Parse, resolve and tck the target file
+ pub fn typecheck(&self) -> Result<Typed> {
+ Ok(self.resolve()?.typecheck()?)
+ }
/// Parse, resolve, tck and normalize the target file
pub fn normalize(&self) -> Result<Normalized> {
- Ok(self.resolve()?.typecheck()?.normalize())
+ Ok(self.typecheck()?.normalize())
}
/// If UPDATE_TEST_FILES=1, we overwrite the output files with our own output.
@@ -204,7 +208,7 @@ impl TestFile {
from_slice::<Value>(&expr_data).unwrap(),
from_slice::<Value>(&expected_data).unwrap()
);
- // If difference was not visible in the cbor::Value, compare normally.
+ // If difference was not visible in the cbor::Nir, compare normally.
assert_eq!(expr_data, expected_data);
}
}
@@ -246,11 +250,11 @@ fn run_test(test: Test) -> Result<()> {
expected.compare_debug(expr)?;
}
ParserFailure(expr, expected) => {
- use std::io::ErrorKind;
+ use std::io;
let err = expr.parse().unwrap_err();
- match &err {
- Error::Parse(_) => {}
- Error::IO(e) if e.kind() == ErrorKind::InvalidData => {}
+ match err.kind() {
+ ErrorKind::Parse(_) => {}
+ ErrorKind::IO(e) if e.kind() == io::ErrorKind::InvalidData => {}
e => panic!("Expected parse error, got: {:?}", e),
}
expected.compare_ui(err)?;
@@ -282,11 +286,11 @@ fn run_test(test: Test) -> Result<()> {
expected.compare_ui(err)?;
}
TypeInferenceSuccess(expr, expected) => {
- let ty = expr.resolve()?.typecheck()?.get_type()?;
+ let ty = expr.typecheck()?.get_type()?;
expected.compare(ty)?;
}
TypeInferenceFailure(expr, expected) => {
- let err = expr.resolve()?.typecheck().unwrap_err();
+ let err = expr.typecheck().unwrap_err();
expected.compare_ui(err)?;
}
Normalization(expr, expected) => {
diff --git a/dhall/tests/import/failure/cycle.txt b/dhall/tests/import/failure/cycle.txt
index 0a20503..4e9488e 100644
--- a/dhall/tests/import/failure/cycle.txt
+++ b/dhall/tests/import/failure/cycle.txt
@@ -1 +1 @@
-Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Resolve(Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }, Resolve(ImportCycle([Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }], Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None })))))
+ImportCycle([Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }], Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None })
diff --git a/dhall/tests/import/failure/importBoundary.txt b/dhall/tests/import/failure/importBoundary.txt
index 8f78e48..6f0615d 100644
--- a/dhall/tests/import/failure/importBoundary.txt
+++ b/dhall/tests/import/failure/importBoundary.txt
@@ -1 +1,7 @@
-Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "importBoundary.dhall"] }), hash: None }, Typecheck(TypeError { message: Custom("error: unbound variable `x`\n --> <current file>:1:0\n |\n...\n3 | x\n | ^ not found in this scope\n |") }))
+Type error: error: unbound variable `x`
+ --> <current file>:1:0
+ |
+...
+3 | x
+ | ^ not found in this scope
+ |
diff --git a/dhall/tests/type-inference/failure/SortInLet.txt b/dhall/tests/type-inference/failure/SortInLet.txt
index 5b88ff7..19bd26d 100644
--- a/dhall/tests/type-inference/failure/SortInLet.txt
+++ b/dhall/tests/type-inference/failure/SortInLet.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:8
+ |
+1 | let x = Sort in 0
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt
index 6b99615..5aacb80 100644
--- a/dhall/tests/type-inference/failure/hurkensParadox.txt
+++ b/dhall/tests/type-inference/failure/hurkensParadox.txt
@@ -1,15 +1,15 @@
Type error: error: wrong type of function argument
- --> <current file>:6:23
+ --> <current file>:6:15
|
1 | let bottom : Type = ∀(any : Type) → any
2 |
3 | in let not : Type → Type = λ(p : Type) → p → bottom
4 |
...
+ 9 | in let tau
10 | : pow (pow U) → U
-11 | = λ(t : pow (pow U))
- | ^^^ this expects an argument of type: Kind
- | ^ but this has type: Sort
+ | ^^^ this expects an argument of type: Kind
+ | ^ but this has type: Sort
|
= note: expected type `Kind`
found type `Sort`
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
index 5b88ff7..653fe0b 100644
--- a/dhall/tests/type-inference/failure/recordOfKind.txt
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { a = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
index 2a754fc..a39a0fb 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+Type error: error: annot mismatch: { x : Natural } != { y : Natural }
--> <current file>:1:0
|
1 | { x = 1 } : { y : Natural }
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+ | ^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural }
|
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
index e67edb8..9ecc2a4 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+Type error: error: annot mismatch: { x : Natural } != { x : Text }
--> <current file>:1:0
|
1 | { x = 1 } : { x : Text }
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+ | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
index d0a9a01..7a4a12c 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{=}
- | ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
index d4639e9..9235ed4 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{=}
- | ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
index 0839742..6a6cd1e 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{ nam = "John Doe" }
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
index 7edef95..b4fe726 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{ name = True }
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
index e84eb15..ca5bbcd 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `1`
--> <current file>:1:6
|
1 | λ(_ : 1) → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
index 4aa0f4f..168ebb9 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `2`
--> <current file>:1:0
|
1 | 2 → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
index 5b88ff7..6f26607 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+ |
+1 | Kind → Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
index 5b88ff7..169014b 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+ |
+1 | Type → Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
index 5ba4b35..51279f2 100644
--- a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (True : Bool) : Natural
- --> <current file>:1:8
+Type error: error: annot mismatch: Bool != Natural
+ --> <current file>:1:18
|
1 | let x : Natural = True in True
- | ^^^^^^^ annot mismatch: (True : Bool) : Natural
+ | ^^^^ annot mismatch: Bool != Natural
|
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
index 5332fcb..0cc4bba 100644
--- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ([1] : List Natural) : Optional Natural
+Type error: error: annot mismatch: List Natural != Optional Natural
--> <current file>:1:0
|
1 | [ 1 ] : Optional Natural
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ([1] : List Natural) : Optional Natural
+ | ^^^^^ annot mismatch: List Natural != Optional Natural
|
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index 5b88ff7..146018f 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { x = Type, y = Kind }
+ | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
index f74e839..02cf64f 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | True ∧ {=}
+ | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
index f74e839..202a3e5 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | { x = True } ∧ { x = False }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
index f74e839..a0b4676 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | {=} ∧ True
+ | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
index f74e839..769712b 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | { x : Bool } ⩓ { x : Natural }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index 5b88ff7..521ae05 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:15
+ |
+1 | { x = Bool } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index 5b88ff7..3abf62c 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:14
+ |
+1 | { x = {=} } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt
index 5b88ff7..e402127 100644
--- a/dhall/tests/type-inference/failure/unit/Sort.txt
+++ b/dhall/tests/type-inference/failure/unit/Sort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:0
+ |
+1 | Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
index 7360e68..dffadb1 100644
--- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (1 : Natural) : Bool
+Type error: error: annot mismatch: Natural != Bool
--> <current file>:1:0
|
1 | 1 : Bool
- | ^^^^^^^^ annot mismatch: (1 : Natural) : Bool
+ | ^ annot mismatch: Natural != Bool
|