diff options
Diffstat (limited to 'dhall')
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 | |