diff options
Diffstat (limited to '')
33 files changed, 3055 insertions, 3194 deletions
diff --git a/dhall/src/dhall.abnf b/dhall/src/dhall.abnf deleted file mode 120000 index ce13b8e..0000000 --- a/dhall/src/dhall.abnf +++ /dev/null @@ -1 +0,0 @@ -../../dhall-lang/standard/dhall.abnf
\ No newline at end of file diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 6e7be64..4df018d 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,10 +1,9 @@ use std::io::Error as IOError; -use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::value::Value; -use crate::semantics::phase::resolve::ImportStack; -use crate::semantics::phase::NormalizedExpr; -use crate::syntax::{BinOp, Import, Label, ParseError, Span}; +use crate::semantics::resolve::ImportStack; +use crate::semantics::Value; +use crate::syntax::{Import, ParseError}; +use crate::NormalizedExpr; pub type Result<T> = std::result::Result<T, Error>; @@ -37,65 +36,59 @@ pub enum EncodeError { CBORError(serde_cbor::error::Error), } -/// A structured type error that includes context +/// A structured type error #[derive(Debug)] pub struct TypeError { message: TypeMessage, - context: TypecheckContext, } /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage { - UnboundVariable(Span), + // UnboundVariable(Span), InvalidInputType(Value), InvalidOutputType(Value), - NotAFunction(Value), - TypeMismatch(Value, Value, Value), - AnnotMismatch(Value, Value), - InvalidListElement(usize, Value, Value), - InvalidListType(Value), - InvalidOptionalType(Value), - InvalidPredicate(Value), - IfBranchMismatch(Value, Value), - IfBranchMustBeTerm(bool, Value), - InvalidFieldType(Label, Value), - NotARecord(Label, Value), - MustCombineRecord(Value), - MissingRecordField(Label, Value), - MissingUnionField(Label, Value), - BinOpTypeMismatch(BinOp, Value), - InvalidTextInterpolation(Value), - Merge1ArgMustBeRecord(Value), - Merge2ArgMustBeUnionOrOptional(Value), - MergeEmptyNeedsAnnotation, - MergeHandlerMissingVariant(Label), - MergeVariantMissingHandler(Label), - MergeAnnotMismatch, - MergeHandlerTypeMismatch, - MergeHandlerReturnTypeMustNotBeDependent, - ProjectionMustBeRecord, - ProjectionMissingEntry, - ProjectionDuplicateField, + // NotAFunction(Value), + // TypeMismatch(Value, Value, Value), + // AnnotMismatch(Value, Value), + // InvalidListElement(usize, Value, Value), + // InvalidListType(Value), + // InvalidOptionalType(Value), + // InvalidPredicate(Value), + // IfBranchMismatch(Value, Value), + // IfBranchMustBeTerm(bool, Value), + // InvalidFieldType(Label, Value), + // NotARecord(Label, Value), + // MustCombineRecord(Value), + // MissingRecordField(Label, Value), + // MissingUnionField(Label, Value), + // BinOpTypeMismatch(BinOp, Value), + // InvalidTextInterpolation(Value), + // Merge1ArgMustBeRecord(Value), + // Merge2ArgMustBeUnionOrOptional(Value), + // MergeEmptyNeedsAnnotation, + // MergeHandlerMissingVariant(Label), + // MergeVariantMissingHandler(Label), + // MergeAnnotMismatch, + // MergeHandlerTypeMismatch, + // MergeHandlerReturnTypeMustNotBeDependent, + // ProjectionMustBeRecord, + // ProjectionMissingEntry, + // ProjectionDuplicateField, Sort, - RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Value), - UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Value), - EquivalenceTypeMismatch(Value, Value), - AssertMismatch(Value, Value), - AssertMustTakeEquivalence, + // RecordTypeDuplicateField, + // RecordTypeMergeRequiresRecordType(Value), + // UnionTypeDuplicateField, + // EquivalenceArgumentMustBeTerm(bool, Value), + // EquivalenceTypeMismatch(Value, Value), + // AssertMismatch(Value, Value), + // AssertMustTakeEquivalence, + Custom(String), } impl TypeError { - pub(crate) fn new( - context: &TypecheckContext, - message: TypeMessage, - ) -> Self { - TypeError { - context: context.clone(), - message, - } + pub(crate) fn new(message: TypeMessage) -> Self { + TypeError { message } } } @@ -103,28 +96,29 @@ impl std::fmt::Display for TypeError { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; let msg = match &self.message { - UnboundVariable(span) => span.error("Type error: Unbound variable"), + // UnboundVariable(var) => var.error("Type error: Unbound variable"), InvalidInputType(v) => { v.span().error("Type error: Invalid function input") } InvalidOutputType(v) => { v.span().error("Type error: Invalid function output") } - NotAFunction(v) => v.span().error("Type error: Not a function"), - TypeMismatch(x, y, z) => { - x.span() - .error("Type error: Wrong type of function argument") - + "\n" - + &z.span().error(format!( - "This argument has type {:?}", - z.get_type().unwrap() - )) - + "\n" - + &y.span().error(format!( - "But the function expected an argument of type {:?}", - y - )) - } + // NotAFunction(v) => v.span().error("Type error: Not a function"), + // TypeMismatch(x, y, z) => { + // x.span() + // .error("Type error: Wrong type of function argument") + // + "\n" + // + &z.span().error(format!( + // "This argument has type {:?}", + // z.get_type().unwrap() + // )) + // + "\n" + // + &y.span().error(format!( + // "But the function expected an argument of type {:?}", + // y + // )) + // } + Custom(s) => format!("Type error: Unhandled error: {}", s), _ => format!("Type error: Unhandled error: {:?}", self.message), }; write!(f, "{}", msg) diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 62a1b27..dbf1fc0 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -16,3 +16,244 @@ mod tests; pub mod error; pub mod semantics; pub mod syntax; + +use std::fmt::Display; +use std::path::Path; + +use crate::error::{EncodeError, Error, ImportError, 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::syntax::binary; +use crate::syntax::{Builtin, Const, Expr}; + +pub type ParsedExpr = Expr<Normalized>; +pub type DecodedExpr = Expr<Normalized>; +pub type ResolvedExpr = Expr<Normalized>; +pub type NormalizedExpr = Expr<Normalized>; + +#[derive(Debug, Clone)] +pub struct Parsed(ParsedExpr, ImportRoot); + +/// An expression where all imports have been resolved +/// +/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. +#[derive(Debug, Clone)] +pub struct Resolved(ResolvedExpr); + +/// A typed expression +#[derive(Debug, Clone)] +pub struct Typed(TyExpr); + +/// A normalized expression. +/// +/// Invariant: the contained Typed expression must be in normal form, +#[derive(Debug, Clone)] +pub struct Normalized(Value); + +/// Controls conversion from `Value` 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 { + pub fn parse_file(f: &Path) -> Result<Parsed, Error> { + parse::parse_file(f) + } + pub fn parse_str(s: &str) -> Result<Parsed, Error> { + parse::parse_str(s) + } + pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { + parse::parse_binary_file(f) + } + pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { + parse::parse_binary(data) + } + + pub fn resolve(self) -> Result<Resolved, ImportError> { + resolve::resolve(self) + } + pub fn skip_resolve(self) -> Result<Resolved, ImportError> { + resolve::skip_resolve_expr(self) + } + + pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { + binary::encode(&self.0) + } + + /// Converts a value back to the corresponding AST expression. + pub fn to_expr(&self) -> ParsedExpr { + self.0.clone() + } +} + +impl Resolved { + pub fn typecheck(&self) -> Result<Typed, TypeError> { + Ok(Typed(typecheck(&self.0)?)) + } + pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> { + Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) + } + /// Converts a value back to the corresponding AST expression. + pub fn to_expr(&self) -> ResolvedExpr { + self.0.clone() + } +} + +impl Typed { + /// Reduce an expression to its normal form, performing beta reduction + pub fn normalize(&self) -> Normalized { + Normalized(self.0.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, + }) + } + + pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> { + Ok(Normalized(self.0.get_type()?)) + } +} + +impl Normalized { + pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { + binary::encode(&self.to_expr()) + } + + /// Converts a value back to the corresponding AST expression. + pub fn to_expr(&self) -> NormalizedExpr { + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) + } + /// 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, + }) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn into_value(self) -> Value { + self.0 + } + + pub(crate) fn from_const(c: Const) -> Self { + Normalized(Value::from_const(c)) + } + 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 { + 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)) + } + pub fn make_optional_type(t: Normalized) -> Self { + Normalized::from_value( + Value::from_builtin(Builtin::Optional).app(t.to_value()), + ) + } + pub fn make_list_type(t: Normalized) -> Self { + Normalized::from_value( + Value::from_builtin(Builtin::List).app(t.to_value()), + ) + } + 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(), + ) + } + 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(), + ) + } +} + +macro_rules! derive_traits_for_wrapper_struct { + ($ty:ident) => { + impl std::cmp::PartialEq for $ty { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } + } + + impl std::cmp::Eq for $ty {} + + impl std::fmt::Display for $ty { + fn fmt( + &self, + f: &mut std::fmt::Formatter, + ) -> Result<(), std::fmt::Error> { + self.0.fmt(f) + } + } + }; +} + +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) + where + H: std::hash::Hasher, + { + if let Ok(vec) = self.encode() { + vec.hash(state) + } + } +} + +impl Eq for Typed {} +impl PartialEq for Typed { + fn eq(&self, other: &Self) -> bool { + self.normalize() == other.normalize() + } +} +impl Display for Typed { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} + +impl Eq for Normalized {} +impl PartialEq for Normalized { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } +} +impl Display for Normalized { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs new file mode 100644 index 0000000..c20fb77 --- /dev/null +++ b/dhall/src/semantics/builtins.rs @@ -0,0 +1,540 @@ +use crate::semantics::{ + self, typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, 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, +}; +use crate::Normalized; +use std::collections::HashMap; +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 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>, +} + +impl BuiltinClosure<Value> { + 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 { + 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()) + } + /// This doesn't break the invariant because we already checked that the appropriate arguments + /// did not normalize to something that allows evaluation to proceed. + pub fn normalize(&self) { + for x in self.args.iter() { + x.normalize(); + } + } + pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind { + TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold( + ExprKind::Builtin(self.b), + |acc, (v, ty)| { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(acc), + Some(ty.clone()), + Span::Artificial, + ), + v.to_tyexpr(venv), + ) + }, + )) + } +} + +pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> { + Expr::new(x, Span::Artificial) +} + +// Ad-hoc macro to help construct the types of builtins +macro_rules! make_type { + (Type) => { rc(ExprKind::Const(Const::Type)) }; + (Bool) => { rc(ExprKind::Builtin(Builtin::Bool)) }; + (Natural) => { rc(ExprKind::Builtin(Builtin::Natural)) }; + (Integer) => { rc(ExprKind::Builtin(Builtin::Integer)) }; + (Double) => { rc(ExprKind::Builtin(Builtin::Double)) }; + (Text) => { rc(ExprKind::Builtin(Builtin::Text)) }; + ($var:ident) => { + rc(ExprKind::Var(V(stringify!($var).into(), 0))) + }; + (Optional $ty:ident) => { + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::Optional)), + make_type!($ty) + )) + }; + (List $($rest:tt)*) => { + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + make_type!($($rest)*) + )) + }; + ({ $($label:ident : $ty:ident),* }) => {{ + let mut kts = DupTreeMap::new(); + $( + kts.insert( + Label::from(stringify!($label)), + make_type!($ty), + ); + )* + rc(ExprKind::RecordType(kts)) + }}; + ($ty:ident -> $($rest:tt)*) => { + rc(ExprKind::Pi( + "_".into(), + make_type!($ty), + make_type!($($rest)*) + )) + }; + (($($arg:tt)*) -> $($rest:tt)*) => { + rc(ExprKind::Pi( + "_".into(), + make_type!($($arg)*), + make_type!($($rest)*) + )) + }; + (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + rc(ExprKind::Pi( + stringify!($var).into(), + make_type!($($ty)*), + make_type!($($rest)*) + )) + }; +} + +pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> { + use Builtin::*; + match b { + Bool | Natural | Integer | Double | Text => make_type!(Type), + List | Optional => make_type!( + Type -> Type + ), + + NaturalFold => make_type!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural + ), + NaturalBuild => make_type!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural + ), + NaturalIsZero | NaturalEven | NaturalOdd => make_type!( + Natural -> Bool + ), + NaturalToInteger => make_type!(Natural -> Integer), + NaturalShow => make_type!(Natural -> Text), + NaturalSubtract => make_type!(Natural -> Natural -> Natural), + + IntegerToDouble => make_type!(Integer -> Double), + IntegerShow => make_type!(Integer -> Text), + IntegerNegate => make_type!(Integer -> Integer), + IntegerClamp => make_type!(Integer -> Natural), + + DoubleShow => make_type!(Double -> Text), + TextShow => make_type!(Text -> Text), + + ListBuild => make_type!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a + ), + ListFold => make_type!( + forall (a: Type) -> + (List a) -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list + ), + ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), + ListHead | ListLast => { + make_type!(forall (a: Type) -> (List a) -> Optional a) + } + ListIndexed => make_type!( + forall (a: Type) -> + (List a) -> + List { index: Natural, value: a } + ), + ListReverse => make_type!( + forall (a: Type) -> (List a) -> List a + ), + + OptionalBuild => make_type!( + forall (a: Type) -> + (forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional) -> + Optional a + ), + OptionalFold => make_type!( + forall (a: Type) -> + (Optional a) -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + ), + OptionalNone => make_type!( + forall (A: Type) -> Optional A + ), + } +} + +// Ad-hoc macro to help construct closures +macro_rules! make_closure { + (var($var:ident)) => {{ + rc(ExprKind::Var(V( + Label::from(stringify!($var)).into(), + 0 + ))) + }}; + (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ + let var = Label::from(stringify!($var)); + let ty = make_closure!($($ty)*); + let body = make_closure!($($body)*); + rc(ExprKind::Lam(var, ty, body)) + }}; + (Type) => { + rc(ExprKind::Const(Type)) + }; + (Natural) => { + rc(ExprKind::Builtin(Builtin::Natural)) + }; + (List $($ty:tt)*) => {{ + let ty = make_closure!($($ty)*); + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + ty + )) + }}; + (Some($($v:tt)*)) => { + rc(ExprKind::SomeLit( + make_closure!($($v)*) + )) + }; + (1 + $($v:tt)*) => { + rc(ExprKind::BinOp( + BinOp::NaturalPlus, + make_closure!($($v)*), + rc(ExprKind::NaturalLit(1)) + )) + }; + ([ $($head:tt)* ] # $($tail:tt)*) => {{ + let head = make_closure!($($head)*); + let tail = make_closure!($($tail)*); + rc(ExprKind::BinOp( + BinOp::ListAppend, + rc(ExprKind::NEListLit(vec![head])), + tail, + )) + }}; +} + +#[allow(clippy::cognitive_complexity)] +fn apply_builtin( + b: Builtin, + args: Vec<Value>, + ty: &Value, + types: Vec<Value>, + env: NzEnv, +) -> ValueKind { + use Builtin::*; + use ValueKind::*; + + // Small helper enum + enum Ret { + ValueKind(ValueKind), + Value(Value), + DoneAsIs, + } + let make_closure = |e| typecheck(&e).unwrap().eval(&env); + + 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)), + _ => Ret::DoneAsIs, + }, + (NaturalEven, [n]) => match &*n.kind() { + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), + _ => Ret::DoneAsIs, + }, + (NaturalOdd, [n]) => match &*n.kind() { + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), + _ => Ret::DoneAsIs, + }, + (NaturalToInteger, [n]) => match &*n.kind() { + NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), + _ => Ret::DoneAsIs, + }, + (NaturalShow, [n]) => match &*n.kind() { + NaturalLit(n) => Ret::ValueKind(TextLit( + semantics::TextLit::from_text(n.to_string()), + )), + _ => Ret::DoneAsIs, + }, + (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { + (NaturalLit(a), NaturalLit(b)) => { + Ret::ValueKind(NaturalLit(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)), + _ => Ret::DoneAsIs, + }, + (IntegerShow, [n]) => match &*n.kind() { + IntegerLit(n) => { + let s = if *n < 0 { + n.to_string() + } else { + format!("+{}", n) + }; + Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) + } + _ => Ret::DoneAsIs, + }, + (IntegerToDouble, [n]) => match &*n.kind() { + IntegerLit(n) => { + Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) + } + _ => Ret::DoneAsIs, + }, + (IntegerNegate, [n]) => match &*n.kind() { + IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), + _ => Ret::DoneAsIs, + }, + (IntegerClamp, [n]) => match &*n.kind() { + IntegerLit(n) => { + Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) + } + _ => Ret::DoneAsIs, + }, + (DoubleShow, [n]) => match &*n.kind() { + DoubleLit(n) => Ret::ValueKind(TextLit( + semantics::TextLit::from_text(n.to_string()), + )), + _ => Ret::DoneAsIs, + }, + (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(); + let s = txt.to_string(); + Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) + } else { + Ret::DoneAsIs + } + } + _ => Ret::DoneAsIs, + }, + (ListLength, [_, l]) => match &*l.kind() { + EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), + NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), + _ => Ret::DoneAsIs, + }, + (ListHead, [_, l]) => match &*l.kind() { + EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), + NEListLit(xs) => { + Ret::ValueKind(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( + xs.iter().rev().next().unwrap().clone(), + )), + _ => Ret::DoneAsIs, + }, + (ListReverse, [_, l]) => match &*l.kind() { + EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), + NEListLit(xs) => { + Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) + } + _ => Ret::DoneAsIs, + }, + (ListIndexed, [_, l]) => { + let l_whnf = l.kind(); + match &*l_whnf { + 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), + ); + + // Construct the new list, with added indices + let list = match &*l_whnf { + EmptyListLit(_) => EmptyListLit(t), + NEListLit(xs) => NEListLit( + xs.iter() + .enumerate() + .map(|(i, e)| { + let mut kvs = HashMap::new(); + kvs.insert( + "index".into(), + Value::from_kind_and_type( + NaturalLit(i), + Value::from_builtin( + Builtin::Natural, + ), + ), + ); + kvs.insert("value".into(), e.clone()); + Value::from_kind_and_type( + RecordLit(kvs), + t.clone(), + ) + }) + .collect(), + ), + _ => unreachable!(), + }; + Ret::ValueKind(list) + } + _ => Ret::DoneAsIs, + } + } + (ListBuild, [t, f]) => { + let list_t = Value::from_builtin(List).app(t.clone()); + Ret::Value( + f.app(list_t.clone()) + .app( + make_closure(make_closure!( + λ(T : Type) -> + λ(a : var(T)) -> + λ(as : List var(T)) -> + [ var(a) ] # var(as) + )) + .app(t.clone()), + ) + .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), + ) + } + (ListFold, [_, l, _, cons, nil]) => match &*l.kind() { + EmptyListLit(_) => Ret::Value(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::DoneAsIs, + }, + (OptionalBuild, [t, f]) => { + let optional_t = Value::from_builtin(Optional).app(t.clone()); + Ret::Value( + f.app(optional_t.clone()) + .app( + make_closure(make_closure!( + λ(T : Type) -> + λ(a : var(T)) -> + Some(var(a)) + )) + .app(t.clone()), + ) + .app( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + ) + } + (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { + EmptyOptionalLit(_) => Ret::Value(nothing.clone()), + NEOptionalLit(x) => Ret::Value(just.app(x.clone())), + _ => Ret::DoneAsIs, + }, + (NaturalBuild, [f]) => Ret::Value( + f.app(Value::from_builtin(Natural)) + .app(make_closure(make_closure!( + λ(x : Natural) -> + 1 + var(x) + ))) + .app( + NaturalLit(0) + .into_value_with_type(Value::from_builtin(Natural)), + ), + ), + + (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)), + ) + .app(t.clone()) + .app(succ.clone()) + .app(zero.clone()); + Ret::Value(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, + }), + } +} + +impl<Value: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Value> { + 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> {} diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs deleted file mode 100644 index f755f72..0000000 --- a/dhall/src/semantics/core/context.rs +++ /dev/null @@ -1,144 +0,0 @@ -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::TypeError; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::syntax::{Label, V}; - -#[derive(Debug, Clone)] -enum CtxItem { - Kept(AlphaVar, Value), - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>); - -impl TypecheckContext { - pub fn new() -> Self { - TypecheckContext(Rc::new(Vec::new())) - } - pub fn insert_type(&self, x: &Label, t: Value) -> Self { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - TypecheckContext(Rc::new(vec)) - } - pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(e))); - Ok(TypecheckContext(Rc::new(vec))) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Value> { - let mut var = var.clone(); - let mut shift_map: HashMap<Label, _> = HashMap::new(); - for (l, i) in self.0.iter().rev() { - match var.over_binder(l) { - None => { - let i = i.under_multiple_binders(&shift_map); - return Some(match i { - CtxItem::Kept(newvar, t) => { - Value::from_kind_and_type(ValueKind::Var(newvar), t) - } - CtxItem::Replaced(v) => v, - }); - } - Some(newvar) => var = newvar, - }; - if let CtxItem::Kept(_, _) = i { - *shift_map.entry(l.clone()).or_insert(0) += 1; - } - } - // Unbound variable - None - } - /// Given a var that makes sense in the current context, map the given function in such a way - /// that the passed variable always makes sense in the context of the passed item. - /// Once we pass the variable definition, the variable doesn't make sense anymore so we just - /// copy the remaining items. - fn do_with_var<E>( - &self, - var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>, - ) -> Result<Self, E> { - let mut vec = Vec::new(); - vec.reserve(self.0.len()); - let mut var = var.clone(); - let mut iter = self.0.iter().rev(); - for (l, i) in iter.by_ref() { - vec.push((l.clone(), f(&var, i)?)); - if let CtxItem::Kept(_, _) = i { - match var.over_binder(l) { - None => break, - Some(newvar) => var = newvar, - }; - } - } - for (l, i) in iter { - vec.push((l.clone(), (*i).clone())); - } - vec.reverse(); - Ok(TypecheckContext(Rc::new(vec))) - } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - if delta < 0 { - Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) - } else { - Some(TypecheckContext(Rc::new( - self.0 - .iter() - .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) - .collect::<Result<_, _>>()?, - ))) - } - } - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) - .unwrap() - } -} - -impl Shift for CtxItem { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - CtxItem::Kept(v, t) => { - CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) - } - CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), - }) - } -} - -impl Shift for TypecheckContext { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - self.shift(delta, var) - } -} - -impl Subst<Value> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), - CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => CtxItem::Replaced(val.clone()), - Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), - }, - } - } -} - -impl Subst<Value> for TypecheckContext { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.subst_shift(var, val) - } -} - -/// Don't count contexts when comparing stuff. -/// This is dirty but needed. -impl PartialEq for TypecheckContext { - fn eq(&self, _: &Self) -> bool { - true - } -} -impl Eq for TypecheckContext {} diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs deleted file mode 100644 index 90d74ea..0000000 --- a/dhall/src/semantics/core/mod.rs +++ /dev/null @@ -1,3 +0,0 @@ -pub mod context; -pub mod value; -pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs deleted file mode 100644 index 6fa00ac..0000000 --- a/dhall/src/semantics/core/value.rs +++ /dev/null @@ -1,591 +0,0 @@ -use std::cell::{Ref, RefCell, RefMut}; -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; -use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; -use crate::semantics::to_expr; -use crate::syntax::{ - Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, Span, -}; - -use self::Form::{Unevaled, NF, WHNF}; - -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation -/// automatically. Uses a RefCell to share computation. -/// Can optionally store a type from typechecking to preserve type information. -/// If you compare for equality two `Value`s in WHNF, 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<RefCell<ValueInternal>>); - -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -/// Invariant: if `form` is `NF`, `value` must be fully normalized -#[derive(Debug)] -struct ValueInternal { - form: Form, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option<Value>, - span: Span, -} - -#[derive(Debug, Clone, Copy)] -pub(crate) enum Form { - /// No constraints; expression may not be normalized at all. - Unevaled, - /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may - /// not be normalized. This means that the first constructor of the contained ValueKind is the first - /// constructor of the final Normal Form (NF). - WHNF, - /// Normal Form, i.e. completely normalized. - /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the - /// ValueKind is in 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. - NF, -} - -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec<Value>), - - Var(AlphaVar), - 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>>), - UnionConstructor(Label, HashMap<Label, Option<Value>>), - UnionLit(Label, Value, HashMap<Label, Option<Value>>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec<InterpolatedTextContents<Value>>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind<Value, Normalized>), -} - -impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { - ValueInternal { - form, - kind, - ty: Some(ty), - span, - } - .into_value() - } - pub(crate) fn const_sort() -> Value { - ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: Span::Artificial, - } - .into_value() - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(v, Unevaled, t, Span::Artificial) - } - pub(crate) fn from_kind_and_type_and_span( - v: ValueKind, - t: Value, - span: Span, - ) -> Value { - Value::new(v, Unevaled, t, span) - } - pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(v, WHNF, t, Span::Artificial) - } - pub(crate) fn from_const(c: Const) -> Self { - const_to_value(c) - } - pub(crate) fn from_builtin(b: Builtin) -> Self { - builtin_to_value(b) - } - pub(crate) fn with_span(self, span: Span) -> Self { - self.as_internal_mut().span = span; - self - } - - pub(crate) fn as_const(&self) -> Option<Const> { - match &*self.as_whnf() { - ValueKind::Const(c) => Some(*c), - _ => None, - } - } - pub(crate) fn span(&self) -> Span { - self.as_internal().span.clone() - } - - fn as_internal(&self) -> Ref<ValueInternal> { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut<ValueInternal> { - self.0.borrow_mut() - } - /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an - /// unevaled PartialExpr. You probably want to use `as_whnf`. - pub(crate) fn as_kind(&self) -> Ref<ValueKind> { - Ref::map(self.as_internal(), ValueInternal::as_kind) - } - /// 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 as_whnf(&self) -> Ref<ValueKind> { - self.normalize_whnf(); - self.as_kind() - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::value_to_expr(self, opts) - } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { - self.as_whnf().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() - } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_value(self) - } - - /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { - match Rc::get_mut(&mut self.0) { - // Mutate directly if sole owner - Some(refcell) => f(RefCell::get_mut(refcell)), - // Otherwise mutate through the refcell - None => f(&mut self.as_internal_mut()), - } - } - /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - self.mutate_internal(|vint| vint.normalize_nf()) - } - - pub(crate) fn normalize_whnf(&self) { - let borrow = self.as_internal(); - match borrow.form { - Unevaled => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already at least in WHNF - WHNF | NF => {} - } - } - pub(crate) fn normalize_nf(&self) { - self.as_internal_mut().normalize_nf(); - } - - pub(crate) fn app(&self, v: Value) -> Value { - let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueKind::Pi(x, t, e) => { - v.check_type(t); - e.subst_shift(&x.into(), &v) - } - _ => unreachable!("Internal type error"), - }; - Value::from_kind_and_type_whnf( - 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) { - 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.as_internal().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") - } -} - -impl ValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_kind(&self) -> &ValueKind { - &self.kind - } - - fn normalize_whnf(&mut self) { - take_mut::take_or_recover( - self, - // Dummy value in case the other closure panics - || ValueInternal { - form: Unevaled, - kind: ValueKind::Const(Const::Type), - ty: None, - span: Span::Artificial, - }, - |vint| match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - kind: normalize_whnf(vint.kind, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: vint.span, - }, - // Already in WHNF - (WHNF, _) | (NF, _) => vint, - }, - ) - } - fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.kind.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} - } - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } - } -} - -impl ValueKind { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_kind_and_type(self, t) - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::kind_to_expr(self, opts) - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - ValueKind::Var(_) - | ValueKind::Const(_) - | ValueKind::BoolLit(_) - | ValueKind::NaturalLit(_) - | ValueKind::IntegerLit(_) - | ValueKind::DoubleLit(_) => {} - - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); - } - - ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueKind::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } - ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for Value { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Value(self.0.shift(delta, var)?)) - } -} - -impl Shift for ValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(ValueInternal { - form: self.form, - kind: self.kind.shift(delta, var)?, - ty: self.ty.shift(delta, var)?, - span: self.span.clone(), - }) - } -} - -impl Shift for ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.shift(delta, var)?) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.shift(delta, var)?) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.shift(delta, var)?) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.shift(delta, var)?) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.shift(delta, var)?) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.shift(delta, var)?) - } - ValueKind::UnionConstructor(x, kts) => { - ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.shift(delta, var)?) - } - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.shift(delta, var)?, - y.shift(delta, var)?, - ), - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.shift(delta, var)?) - } - }) - } -} - -impl Subst<Value> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_kind() { - // If the var matches, we can just reuse the provided value instead of copying it. - // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { - if let Ok(self_ty) = self.get_type() { - val.check_type(&self_ty.subst_shift(var, val)); - } - val.clone() - } - _ => Value(self.0.subst_shift(var, val)), - } - } -} - -impl Subst<Value> for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - ValueInternal { - // The resulting value may not stay in wnhf after substitution - form: Unevaled, - kind: self.kind.subst_shift(var, val), - ty: self.ty.subst_shift(var, val), - span: self.span.clone(), - } - } -} - -impl Subst<Value> for ValueKind { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.subst_shift(var, val)) - } - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.subst_shift(var, val)) - } - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.subst_shift(var, val)) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.subst_shift(var, val)) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.subst_shift(var, val)) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.subst_shift(var, val)) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.subst_shift(var, val)) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.subst_shift(var, val)) - } - ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( - x.clone(), - kts.subst_shift(var, val), - ), - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), - } - } -} - -// TODO: use Rc comparison to shortcut on identical pointers -impl std::cmp::PartialEq for Value { - fn eq(&self, other: &Self) -> bool { - *self.as_whnf() == *other.as_whnf() - } -} -impl std::cmp::Eq for Value {} - -impl std::fmt::Debug for Value { - fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let vint: &ValueInternal = &self.as_internal(); - if let ValueKind::Const(c) = &vint.kind { - write!(fmt, "{:?}", c) - } else { - let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); - x.field("value", &vint.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/core/var.rs b/dhall/src/semantics/core/var.rs deleted file mode 100644 index 1548713..0000000 --- a/dhall/src/semantics/core/var.rs +++ /dev/null @@ -1,295 +0,0 @@ -use std::collections::HashMap; - -use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; - -/// Stores a pair of variables: a normal one and one -/// that corresponds to the alpha-normalized version of the first one. -/// Equality is up to alpha-equivalence (compares on the second one only). -#[derive(Clone, Eq)] -pub struct AlphaVar { - normal: V<Label>, - alpha: V<()>, -} - -// Exactly like a Label, but equality returns always true. -// This is so that ValueKind equality is exactly alpha-equivalence. -#[derive(Clone, Eq)] -pub struct AlphaLabel(Label); - -pub(crate) trait Shift: Sized { - // Shift an expression to move it around binders without changing the meaning of its free - // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an - // expression from under a binder, if the expression does not refer to that bound variable. - // Returns None if delta was negative and the variable was free in the expression. - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>; - - fn over_binder<T>(&self, x: T) -> Option<Self> - where - T: Into<AlphaVar>, - { - self.shift(-1, &x.into()) - } - - fn under_binder<T>(&self, x: T) -> Self - where - T: Into<AlphaVar>, - { - // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - - fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self - where - Self: Clone, - { - let mut v = self.clone(); - for (x, n) in shift_map { - v = v.shift(*n as isize, &x.into()).unwrap(); - } - v - } -} - -pub(crate) trait Subst<S> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self; -} - -impl AlphaVar { - pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { - if alpha { - V("_".into(), self.alpha.1) - } else { - self.normal.clone() - } - } - pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self { - AlphaVar { - normal, - alpha: V((), alpha), - } - } -} - -impl AlphaLabel { - pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { - if alpha { - "_".into() - } else { - self.to_label() - } - } - pub(crate) fn to_label(&self) -> Label { - self.clone().into() - } -} - -impl Shift for AlphaVar { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(AlphaVar { - normal: self.normal.shift(delta, &var.normal)?, - alpha: self.alpha.shift(delta, &var.alpha)?, - }) - } -} - -/// Equality up to alpha-equivalence -impl std::cmp::PartialEq for AlphaVar { - fn eq(&self, other: &Self) -> bool { - self.alpha == other.alpha - } -} -impl std::cmp::PartialEq for AlphaLabel { - fn eq(&self, _other: &Self) -> bool { - true - } -} - -impl std::fmt::Debug for AlphaVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1) - } -} - -impl std::fmt::Debug for AlphaLabel { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaLabel({})", &self.0) - } -} - -impl From<Label> for AlphaVar { - fn from(x: Label) -> AlphaVar { - AlphaVar { - normal: V(x, 0), - alpha: V((), 0), - } - } -} -impl<'a> From<&'a Label> for AlphaVar { - fn from(x: &'a Label) -> AlphaVar { - x.clone().into() - } -} -impl From<AlphaLabel> for AlphaVar { - fn from(x: AlphaLabel) -> AlphaVar { - let l: Label = x.into(); - l.into() - } -} -impl<'a> From<&'a AlphaLabel> for AlphaVar { - fn from(x: &'a AlphaLabel) -> AlphaVar { - x.clone().into() - } -} - -impl From<Label> for AlphaLabel { - fn from(x: Label) -> AlphaLabel { - AlphaLabel(x) - } -} -impl From<AlphaLabel> for Label { - fn from(x: AlphaLabel) -> Label { - x.0 - } -} -impl Shift for () { - fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { - Some(()) - } -} - -impl<A: Shift, B: Shift> Shift for (A, B) { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for Option<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - None => None, - Some(x) => Some(x.shift(delta, var)?), - }) - } -} - -impl<T: Shift> Shift for Box<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Box::new(self.as_ref().shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for std::rc::Rc<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for std::cell::RefCell<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?)) - } -} - -impl<T: Shift, E: Clone> Shift for ExprKind<T, E> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(self.traverse_ref_with_special_handling_of_binders( - |v| Ok(v.shift(delta, var)?), - |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - )?) - } -} - -impl<T: Shift> Shift for Vec<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some( - self.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::<Result<_, _>>()?, - ) - } -} - -impl<K, T: Shift> Shift for HashMap<K, T> -where - K: Clone + std::hash::Hash + Eq, -{ - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some( - self.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::<Result<_, _>>()?, - ) - } -} - -impl<T: Shift> Shift for InterpolatedTextContents<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?) - } -} - -impl<S> Subst<S> for () { - fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {} -} - -impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - (self.0.subst_shift(var, val), self.1.subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for Option<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.as_ref().map(|x| x.subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for Box<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - Box::new(self.as_ref().subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - std::rc::Rc::new(self.as_ref().subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - std::cell::RefCell::new(self.borrow().subst_shift(var, val)) - } -} - -impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.map_ref_with_special_handling_of_binders( - |v| v.subst_shift(var, val), - |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ) - } -} - -impl<S, T: Subst<S>> Subst<S> for Vec<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.iter().map(|v| v.subst_shift(var, val)).collect() - } -} - -impl<S, T: Subst<S>> Subst<S> for InterpolatedTextContents<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.map_ref(|x| x.subst_shift(var, val)) - } -} - -impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T> -where - K: Clone + std::hash::Hash + Eq, -{ - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect() - } -} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 1eeef86..98fdf5a 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,3 +1,8 @@ -pub mod core; -pub mod phase; -pub mod to_expr; +pub mod builtins; +pub mod nze; +pub mod parse; +pub mod resolve; +pub mod tck; +pub(crate) use self::builtins::*; +pub(crate) use self::nze::*; +pub(crate) use self::tck::*; diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs new file mode 100644 index 0000000..0b22a8b --- /dev/null +++ b/dhall/src/semantics/nze/env.rs @@ -0,0 +1,76 @@ +use crate::semantics::{AlphaVar, Value, ValueKind}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum NzVar { + /// Reverse-debruijn index: counts number of binders from the bottom of the stack. + Bound(usize), + /// Fake fresh variable generated for expression equality checking. + Fresh(usize), +} + +#[derive(Debug, Clone)] +enum NzEnvItem { + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec<NzEnvItem>, +} + +impl NzVar { + pub fn new(idx: usize) -> Self { + NzVar::Bound(idx) + } + pub fn fresh() -> Self { + use std::sync::atomic::{AtomicUsize, Ordering}; + // Global counter to ensure uniqueness of the generated id. + static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0); + let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); + NzVar::Fresh(id) + } + /// Get index of bound variable. + /// Panics on a fresh variable. + pub fn idx(&self) -> usize { + match self { + NzVar::Bound(i) => *i, + NzVar::Fresh(_) => panic!( + "Trying to use a fresh variable outside of equality checking" + ), + } + } +} + +impl NzEnv { + pub fn new() -> Self { + NzEnv { items: Vec::new() } + } + + pub fn insert_type(&self, t: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Kept(t)); + env + } + pub fn insert_value(&self, e: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Replaced(e)); + env + } + pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { + 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(), + } + } + pub fn lookup_ty(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => ty.clone(), + NzEnvItem::Replaced(x) => x.get_type().unwrap(), + } + } +} diff --git a/dhall/src/semantics/nze/lazy.rs b/dhall/src/semantics/nze/lazy.rs new file mode 100644 index 0000000..d361313 --- /dev/null +++ b/dhall/src/semantics/nze/lazy.rs @@ -0,0 +1,64 @@ +use once_cell::unsync::OnceCell; +use std::cell::Cell; +use std::fmt::Debug; +use std::ops::Deref; + +pub trait Eval<Tgt> { + fn eval(self) -> Tgt; +} + +/// A value which is initialized from a `Src` on the first access. +pub struct Lazy<Src, Tgt> { + /// Exactly one of `src` of `tgt` must be set at a given time. + /// Once `src` is unset and `tgt` is set, we never go back. + src: Cell<Option<Src>>, + tgt: OnceCell<Tgt>, +} + +impl<Src, Tgt> Lazy<Src, Tgt> +where + Src: Eval<Tgt>, +{ + /// Creates a new lazy value with the given initializing value. + pub fn new(src: Src) -> Self { + Lazy { + src: Cell::new(Some(src)), + tgt: OnceCell::new(), + } + } + /// Creates a new lazy value with the given already-initialized value. + pub fn new_completed(tgt: Tgt) -> Self { + let lazy = Lazy { + src: Cell::new(None), + tgt: OnceCell::new(), + }; + let _ = lazy.tgt.set(tgt); + lazy + } +} + +impl<Src, Tgt> Deref for Lazy<Src, Tgt> +where + Src: Eval<Tgt>, +{ + type Target = Tgt; + fn deref(&self) -> &Self::Target { + self.tgt.get_or_init(|| { + let src = self.src.take().unwrap(); + src.eval() + }) + } +} + +impl<Src, Tgt> Debug for Lazy<Src, Tgt> +where + Tgt: Debug, +{ + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if let Some(tgt) = self.tgt.get() { + fmt.debug_tuple("Lazy@Init").field(tgt).finish() + } else { + fmt.debug_tuple("Lazy@Uninit").finish() + } + } +} diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs new file mode 100644 index 0000000..2c8d907 --- /dev/null +++ b/dhall/src/semantics/nze/mod.rs @@ -0,0 +1,9 @@ +pub mod env; +pub mod lazy; +pub mod normalize; +pub mod value; +pub mod var; +pub(crate) use env::*; +pub(crate) use normalize::*; +pub(crate) use value::*; +pub(crate) use var::*; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs new file mode 100644 index 0000000..e9d140b --- /dev/null +++ b/dhall/src/semantics/nze/normalize.rs @@ -0,0 +1,421 @@ +use std::collections::HashMap; + +use crate::semantics::NzEnv; +use crate::semantics::{ + Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, + ValueKind, +}; +use crate::syntax::{ + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, +}; +use crate::Normalized; + +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { + match f.kind() { + ValueKind::LamClosure { closure, .. } => { + closure.apply(a).to_whnf_check_type(ty) + } + 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)), + } +} + +pub(crate) fn squash_textlit( + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, +) -> Vec<InterpolatedTextContents<Value>> { + use std::mem::replace; + use InterpolatedTextContents::{Expr, Text}; + + fn inner( + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, + crnt_str: &mut String, + ret: &mut Vec<InterpolatedTextContents<Value>>, + ) { + for contents in elts { + match contents { + Text(s) => crnt_str.push_str(&s), + Expr(e) => match e.kind() { + ValueKind::TextLit(elts2) => { + inner(elts2.iter().cloned(), crnt_str, ret) + } + _ => { + if !crnt_str.is_empty() { + ret.push(Text(replace(crnt_str, String::new()))) + } + ret.push(Expr(e.clone())) + } + }, + } + } + } + + let mut crnt_str = String::new(); + let mut ret = Vec::new(); + inner(elts, &mut crnt_str, &mut ret); + if !crnt_str.is_empty() { + ret.push(Text(replace(&mut crnt_str, String::new()))) + } + ret +} + +pub(crate) fn merge_maps<K, V, F, Err>( + map1: &HashMap<K, V>, + map2: &HashMap<K, V>, + mut f: F, +) -> Result<HashMap<K, V>, Err> +where + F: FnMut(&K, &V, &V) -> Result<V, Err>, + K: std::hash::Hash + Eq + Clone, + V: Clone, +{ + let mut kvs = HashMap::new(); + for (x, v2) in map2 { + let newv = if let Some(v1) = map1.get(x) { + f(x, v1, v2)? + } else { + v2.clone() + }; + kvs.insert(x.clone(), newv); + } + for (x, v1) in map1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v1.clone()); + } + Ok(kvs) +} + +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueKind(ValueKind), + Value(Value), + ValueRef(&'a Value), + Expr(ExprKind<Value, Normalized>), +} + +fn apply_binop<'a>( + o: BinOp, + x: &'a Value, + y: &'a Value, + ty: &Value, +) -> 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, + }; + 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)), + + (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), + (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), + (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { + Ret::ValueKind(NaturalLit(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)) + } + + (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()), + ), + + (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => { + Ret::ValueRef(y) + } + (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => { + Ret::ValueRef(x) + } + (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)), + ), + + (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + Ret::ValueRef(x) + } + (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + Ret::ValueRef(y) + } + (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let mut kvs = kvs2.clone(); + for (x, v) in kvs1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v.clone()); + } + Ret::ValueKind(RecordLit(kvs)) + } + + (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + Ret::ValueRef(x) + } + (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + Ret::ValueRef(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(), + )) + })?; + Ret::ValueKind(RecordLit(kvs)) + } + + (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { + let kts = merge_maps::<_, _, _, !>( + 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(), + )) + }, + )?; + Ret::ValueKind(RecordType(kts)) + } + + (Equivalence, _, _) => { + Ret::ValueKind(ValueKind::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, EmptyOptionalLit, IntegerLit, NEListLit, + NEOptionalLit, NaturalLit, 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::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::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::EmptyListLit(t) => { + let arg = match &*t.kind() { + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, + args, + .. + }) if args.len() == 1 => args[0].clone(), + _ => panic!("internal type error"), + }; + Ret::ValueKind(ValueKind::EmptyListLit(arg)) + } + ExprKind::NEListLit(elts) => { + Ret::ValueKind(NEListLit(elts.into_iter().collect())) + } + ExprKind::RecordLit(kvs) => { + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) + } + ExprKind::RecordType(kvs) => { + Ret::ValueKind(RecordType(kvs.into_iter().collect())) + } + ExprKind::UnionType(kvs) => { + Ret::ValueKind(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()) + } else { + Ret::ValueKind(ValueKind::TextLit(tlit)) + } + } + ExprKind::BoolIf(ref b, ref e1, ref e2) => { + match b.kind() { + BoolLit(true) => Ret::ValueRef(e1), + BoolLit(false) => Ret::ValueRef(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), + _ => Ret::Expr(expr), + } + } + } + } + ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + Some(ret) => ret, + None => Ret::Expr(expr), + }, + + ExprKind::Projection(_, ref ls) if ls.is_empty() => { + Ret::ValueKind(RecordLit(HashMap::new())) + } + ExprKind::Projection(ref v, ref ls) => match v.kind() { + RecordLit(kvs) => Ret::ValueKind(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), + _ => Ret::Expr(expr), + }, + ExprKind::Field(ref v, ref l) => match v.kind() { + RecordLit(kvs) => match kvs.get(l) { + Some(r) => Ret::Value(r.clone()), + None => Ret::Expr(expr), + }, + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), + _ => Ret::Expr(expr), + }, + 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()), + None => Ret::Expr(expr), + }, + UnionLit(l, v, _, _, _) => match kvs.get(l) { + Some(h) => Ret::Value(h.app(v.clone())), + None => Ret::Expr(expr), + }, + EmptyOptionalLit(_) => match kvs.get(&"None".into()) { + Some(h) => Ret::Value(h.clone()), + None => Ret::Expr(expr), + }, + NEOptionalLit(v) => match kvs.get(&"Some".into()) { + Some(h) => Ret::Value(h.app(v.clone())), + None => Ret::Expr(expr), + }, + _ => Ret::Expr(expr), + }, + _ => Ret::Expr(expr), + } + } + ExprKind::ToMap(_, _) => unimplemented!("toMap"), + }; + + 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), + } +} + +/// 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)) => { + let annot = annot.eval(env); + ValueKind::LamClosure { + binder: Binder::new(binder.clone()), + annot: annot.clone(), + closure: Closure::new(annot, env, body.clone()), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = annot.eval(env); + let closure = Closure::new(annot.clone(), env, body.clone()); + ValueKind::PiClosure { + binder: Binder::new(binder.clone()), + annot, + closure, + } + } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.eval(env); + 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) + } + } +} diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs new file mode 100644 index 0000000..ae06942 --- /dev/null +++ b/dhall/src/semantics/nze/value.rs @@ -0,0 +1,656 @@ +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, +}; +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 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_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 new file mode 100644 index 0000000..264b81d --- /dev/null +++ b/dhall/src/semantics/nze/var.rs @@ -0,0 +1,36 @@ +use crate::syntax::Label; + +// Exactly like a Label, but equality returns always true. +// This is so that ValueKind equality is exactly alpha-equivalence. +#[derive(Clone, Eq)] +pub struct Binder { + name: Label, +} + +impl Binder { + pub(crate) fn new(name: Label) -> Self { + Binder { name } + } + pub(crate) fn to_label(&self) -> Label { + self.clone().into() + } +} + +/// Equality up to alpha-equivalence +impl std::cmp::PartialEq for Binder { + fn eq(&self, _other: &Self) -> bool { + true + } +} + +impl std::fmt::Debug for Binder { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "Binder({})", &self.name) + } +} + +impl From<Binder> for Label { + fn from(x: Binder) -> Label { + x.name + } +} diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/parse.rs index 00db422..ee35536 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/parse.rs @@ -3,10 +3,10 @@ use std::io::Read; use std::path::Path; use crate::error::Error; -use crate::semantics::phase::resolve::ImportRoot; -use crate::semantics::phase::Parsed; +use crate::semantics::resolve::ImportRoot; use crate::syntax::binary; use crate::syntax::parse_expr; +use crate::Parsed; pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = String::new(); diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs deleted file mode 100644 index 5332eb3..0000000 --- a/dhall/src/semantics/phase/mod.rs +++ /dev/null @@ -1,259 +0,0 @@ -use std::fmt::Display; -use std::path::Path; - -use crate::error::{EncodeError, Error, ImportError, TypeError}; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::to_expr::ToExprOptions; -use crate::syntax::binary; -use crate::syntax::{Builtin, Const, Expr}; -use resolve::ImportRoot; - -pub(crate) mod normalize; -pub(crate) mod parse; -pub(crate) mod resolve; -pub(crate) mod typecheck; - -pub type ParsedExpr = Expr<Normalized>; -pub type DecodedExpr = Expr<Normalized>; -pub type ResolvedExpr = Expr<Normalized>; -pub type NormalizedExpr = Expr<Normalized>; - -#[derive(Debug, Clone)] -pub struct Parsed(ParsedExpr, ImportRoot); - -/// An expression where all imports have been resolved -/// -/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. -#[derive(Debug, Clone)] -pub struct Resolved(ResolvedExpr); - -/// A typed expression -#[derive(Debug, Clone)] -pub struct Typed(Value); - -/// A normalized expression. -/// -/// Invariant: the contained Typed expression must be in normal form, -#[derive(Debug, Clone)] -pub struct Normalized(Typed); - -impl Parsed { - pub fn parse_file(f: &Path) -> Result<Parsed, Error> { - parse::parse_file(f) - } - pub fn parse_str(s: &str) -> Result<Parsed, Error> { - parse::parse_str(s) - } - pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { - parse::parse_binary_file(f) - } - pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { - parse::parse_binary(data) - } - - pub fn resolve(self) -> Result<Resolved, ImportError> { - resolve::resolve(self) - } - pub fn skip_resolve(self) -> Result<Resolved, ImportError> { - resolve::skip_resolve_expr(self) - } - - pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - binary::encode(&self.0) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ParsedExpr { - self.0.clone() - } -} - -impl Resolved { - pub fn typecheck(self) -> Result<Typed, TypeError> { - Ok(typecheck::typecheck(self.0)?.into_typed()) - } - pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> { - Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())? - .into_typed()) - } - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { - self.0.clone() - } -} - -impl Typed { - /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(mut self) -> Normalized { - self.normalize_mut(); - Normalized(self) - } - - pub(crate) fn from_const(c: Const) -> Self { - Typed(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { - Typed(Value::from_kind_and_type(v, t.into_value())) - } - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) - } - pub(crate) fn const_type() -> Self { - Typed::from_const(Const::Type) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the - /// process. - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result<Typed, TypeError> { - Ok(self.0.get_type()?.into_typed()) - } - - pub fn make_builtin_type(b: Builtin) -> Self { - Typed::from_value(Value::from_builtin(b)) - } - pub fn make_optional_type(t: Typed) -> Self { - Typed::from_value( - Value::from_builtin(Builtin::Optional).app(t.to_value()), - ) - } - pub fn make_list_type(t: Typed) -> Self { - Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value())) - } - pub fn make_record_type( - kts: impl Iterator<Item = (String, Typed)>, - ) -> Self { - Typed::from_kind_and_type( - ValueKind::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), - ), - Typed::const_type(), - ) - } - pub fn make_union_type( - kts: impl Iterator<Item = (String, Option<Typed>)>, - ) -> Self { - Typed::from_kind_and_type( - ValueKind::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) - .collect(), - ), - Typed::const_type(), - ) - } -} - -impl Normalized { - pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - binary::encode(&self.to_expr()) - } - - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.0.normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.normalize_to_expr_alpha() - } - pub(crate) fn into_typed(self) -> Typed { - self.0 - } -} - -impl Shift for Typed { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Typed(self.0.shift(delta, var)?)) - } -} - -impl Shift for Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Normalized(self.0.shift(delta, var)?)) - } -} - -impl Subst<Value> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Typed(self.0.subst_shift(var, val)) - } -} - -macro_rules! derive_traits_for_wrapper_struct { - ($ty:ident) => { - impl std::cmp::PartialEq for $ty { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } - } - - impl std::cmp::Eq for $ty {} - - impl std::fmt::Display for $ty { - fn fmt( - &self, - f: &mut std::fmt::Formatter, - ) -> Result<(), std::fmt::Error> { - self.0.fmt(f) - } - } - }; -} - -derive_traits_for_wrapper_struct!(Parsed); -derive_traits_for_wrapper_struct!(Resolved); -derive_traits_for_wrapper_struct!(Normalized); - -impl std::hash::Hash for Normalized { - fn hash<H>(&self, state: &mut H) - where - H: std::hash::Hasher, - { - if let Ok(vec) = self.encode() { - vec.hash(state) - } - } -} - -impl Eq for Typed {} -impl PartialEq for Typed { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } -} - -impl Display for Typed { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs deleted file mode 100644 index bf0c626..0000000 --- a/dhall/src/semantics/phase/normalize.rs +++ /dev/null @@ -1,791 +0,0 @@ -use std::collections::HashMap; -use std::convert::TryInto; - -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::Normalized; -use crate::syntax; -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, - Label, NaiveDouble, -}; - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (#$var:ident) => { $var.clone() }; - (var($var:ident, $n:expr, $($ty:tt)*)) => {{ - let var = AlphaVar::from_var_and_alpha( - Label::from(stringify!($var)).into(), - $n - ); - ValueKind::Var(var) - .into_value_with_type(make_closure!($($ty)*)) - }}; - // Warning: assumes that $ty, as a dhall value, has type `Type` - (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var: AlphaLabel = Label::from(stringify!($var)).into(); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - let body_ty = body.get_type_not_sort(); - let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty) - .into_value_with_type(Value::from_const(Type)); - ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty) - }}; - (Natural) => { - Value::from_builtin(Builtin::Natural) - }; - (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app(make_closure!($($rest)*)) - }; - (Some($($rest:tt)*)) => {{ - let v = make_closure!($($rest)*); - let v_type = v.get_type_not_sort(); - let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); - ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) - }}; - (1 + $($rest:tt)*) => { - ValueKind::PartialExpr(ExprKind::BinOp( - syntax::BinOp::NaturalPlus, - make_closure!($($rest)*), - Value::from_kind_and_type( - ValueKind::NaturalLit(1), - make_closure!(Natural) - ), - )).into_value_with_type( - make_closure!(Natural) - ) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - let list_type = tail.get_type_not_sort(); - ValueKind::PartialExpr(ExprKind::BinOp( - syntax::BinOp::ListAppend, - ValueKind::NEListLit(vec![head]) - .into_value_with_type(list_type.clone()), - tail, - )).into_value_with_type(list_type) - }}; -} - -#[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec<Value>, - ty: &Value, -) -> ValueKind { - use syntax::Builtin::*; - use ValueKind::*; - - // Small helper enum - enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - // For applications that can return a function, it's important to keep the remaining - // arguments to apply them to the resulting function. - ValueWithRemainingArgs(&'a [Value], Value), - DoneAsIs, - } - - let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), - _ => Ret::DoneAsIs, - }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), - _ => Ret::DoneAsIs, - }, - (NaturalShow, [n]) => { - match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueKind(NaturalLit(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)), - _ => Ret::DoneAsIs, - }, - (IntegerShow, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) - } - _ => Ret::DoneAsIs, - }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) - } - _ => Ret::DoneAsIs, - }, - (IntegerNegate, [n]) => match &*n.as_whnf() { - IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), - _ => Ret::DoneAsIs, - }, - (IntegerClamp, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) - } - _ => Ret::DoneAsIs, - }, - (DoubleShow, [n]) => { - match &*n.as_whnf() { - DoubleLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (TextShow, [v]) => match &*v.as_whnf() { - TextLit(elts) => { - match elts.as_slice() { - // Empty string literal. - [] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::empty().collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - // If there are no interpolations (invariants ensure that when there are no - // interpolations, there is a single Text item) in the literal. - [InterpolatedTextContents::Text(s)] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::once(InterpolatedTextContents::Text( - s.clone(), - )) - .collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, - } - } - _ => Ret::DoneAsIs, - }, - (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), - NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), - _ => Ret::DoneAsIs, - }, - (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) - } - _ => Ret::DoneAsIs, - }, - (ListIndexed, [_, l]) => { - let l_whnf = l.as_whnf(); - match &*l_whnf { - 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), - ); - - // Construct the new list, with added indices - let list = match &*l_whnf { - EmptyListLit(_) => EmptyListLit(t), - NEListLit(xs) => NEListLit( - xs.iter() - .enumerate() - .map(|(i, e)| { - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Value::from_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), - ); - kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::ValueKind(list) - } - _ => Ret::DoneAsIs, - } - } - (ListBuild, [t, f]) => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("a")); - let t2 = t1.under_binder(Label::from("as")); - make_closure!( - λ(a : #t) -> - λ(as : List #t1) -> - [ var(a, 1, #t2) ] # var(as, 0, List #t2) - ) - }) - .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), - ) - } - (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), - NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v); - } - Ret::ValueWithRemainingArgs(r, v) - } - _ => Ret::DoneAsIs, - }, - (OptionalBuild, [t, f]) => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("a")); - make_closure!(λ(a: #t) -> Some(var(a, 0, #t1))) - }) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ) - } - (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf() - { - EmptyOptionalLit(_) => { - Ret::ValueWithRemainingArgs(r, nothing.clone()) - } - NEOptionalLit(x) => { - Ret::ValueWithRemainingArgs(r, just.app(x.clone())) - } - _ => Ret::DoneAsIs, - }, - (NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), - ), - - (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() { - NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), - NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) - .app(t.clone()) - .app(succ.clone()) - .app(zero.clone()); - Ret::ValueWithRemainingArgs(r, succ.app(fold)) - } - _ => Ret::DoneAsIs, - }, - _ => Ret::DoneAsIs, - }; - match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => { - let n_consumed_args = args.len() - unconsumed_args.len(); - for x in args.into_iter().skip(n_consumed_args) { - v = v.app(x); - } - v.to_whnf_check_type(ty) - } - Ret::DoneAsIs => AppliedBuiltin(b, args), - } -} - -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.as_whnf(); - match &*f_borrow { - ValueKind::Lam(x, _, e) => { - e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) - } - ValueKind::AppliedBuiltin(b, args) => { - use std::iter::once; - let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args, ty) - } - ValueKind::UnionConstructor(l, kts) => { - ValueKind::UnionLit(l.clone(), a, kts.clone()) - } - _ => { - drop(f_borrow); - ValueKind::PartialExpr(ExprKind::App(f, a)) - } - } -} - -pub(crate) fn squash_textlit( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, -) -> Vec<InterpolatedTextContents<Value>> { - use std::mem::replace; - use InterpolatedTextContents::{Expr, Text}; - - fn inner( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, - crnt_str: &mut String, - ret: &mut Vec<InterpolatedTextContents<Value>>, - ) { - for contents in elts { - match contents { - Text(s) => crnt_str.push_str(&s), - Expr(e) => { - let e_borrow = e.as_whnf(); - match &*e_borrow { - ValueKind::TextLit(elts2) => { - inner(elts2.iter().cloned(), crnt_str, ret) - } - _ => { - drop(e_borrow); - if !crnt_str.is_empty() { - ret.push(Text(replace(crnt_str, String::new()))) - } - ret.push(Expr(e.clone())) - } - } - } - } - } - } - - let mut crnt_str = String::new(); - let mut ret = Vec::new(); - inner(elts, &mut crnt_str, &mut ret); - if !crnt_str.is_empty() { - ret.push(Text(replace(&mut crnt_str, String::new()))) - } - ret -} - -pub(crate) fn merge_maps<K, V, F, Err>( - map1: &HashMap<K, V>, - map2: &HashMap<K, V>, - mut f: F, -) -> Result<HashMap<K, V>, Err> -where - F: FnMut(&K, &V, &V) -> Result<V, Err>, - K: std::hash::Hash + Eq + Clone, - V: Clone, -{ - let mut kvs = HashMap::new(); - for (x, v2) in map2 { - let newv = if let Some(v1) = map1.get(x) { - f(x, v1, v2)? - } else { - v2.clone() - }; - kvs.insert(x.clone(), newv); - } - for (x, v1) in map1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v1.clone()); - } - Ok(kvs) -} - -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - ValueRef(&'a Value), - Expr(ExprKind<Value, Normalized>), -} - -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> 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, - TextLit, - }; - let x_borrow = x.as_whnf(); - let y_borrow = y.as_whnf(); - Some(match (o, &*x_borrow, &*y_borrow) { - (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)), - - (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(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)) - } - - (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()), - ), - - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueKind(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueKind(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) - } - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - Ret::ValueKind(RecordLit(kvs)) - } - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.as_whnf(); - let kts = match &*ty_borrow { - RecordType(kts) => kts, - _ => unreachable!("Internal type error"), - }; - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )), - kts.get(k).expect("Internal type error").clone(), - )) - })?; - Ret::ValueKind(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { - unreachable!("This case should have been handled in typecheck") - } - - _ => return None, - }) -} - -pub(crate) fn normalize_one_layer( - expr: ExprKind<Value, Normalized>, - ty: &Value, -) -> ValueKind { - use ValueKind::{ - AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, - IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, - 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::Const(_) - | ExprKind::Builtin(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) - | ExprKind::RecordType(_) - | ExprKind::UnionType(_) => { - unreachable!("This case should have been handled in typecheck") - } - 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::EmptyListLit(ref t) => { - // Check if the type is of the form `List x` - let t_borrow = t.as_whnf(); - match &*t_borrow { - AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueKind(EmptyListLit(args[0].clone())) - } - _ => { - drop(t_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::NEListLit(elts) => { - Ret::ValueKind(NEListLit(elts.into_iter().collect())) - } - ExprKind::RecordLit(kvs) => { - Ret::ValueKind(RecordLit(kvs.into_iter().collect())) - } - ExprKind::TextLit(elts) => { - use InterpolatedTextContents::Expr; - let elts: Vec<_> = squash_textlit(elts.into_iter()); - // Simplify bare interpolation - if let [Expr(th)] = elts.as_slice() { - Ret::Value(th.clone()) - } else { - Ret::ValueKind(TextLit(elts)) - } - } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_whnf(); - match &*b_borrow { - BoolLit(true) => Ret::ValueRef(e1), - BoolLit(false) => Ret::ValueRef(e2), - _ => { - let e1_borrow = e1.as_whnf(); - let e2_borrow = e2.as_whnf(); - match (&*e1_borrow, &*e2_borrow) { - // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), - _ if e1 == e2 => Ret::ValueRef(e1), - _ => { - drop(b_borrow); - drop(e1_borrow); - drop(e2_borrow); - Ret::Expr(expr) - } - } - } - } - } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, - - ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueKind(RecordLit(HashMap::new())) - } - ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.as_whnf(); - match &*v_borrow { - RecordLit(kvs) => Ret::ValueKind(RecordLit( - ls.iter() - .filter_map(|l| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::Field(ref v, ref l) => { - let v_borrow = v.as_whnf(); - match &*v_borrow { - RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), - None => { - drop(v_borrow); - Ret::Expr(expr) - } - }, - UnionType(kts) => { - Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) - } - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::ProjectionByExpr(_, _) => { - unimplemented!("selection by expression") - } - ExprKind::Completion(_, _) => unimplemented!("record completion"), - - ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_whnf(); - let variant_borrow = variant.as_whnf(); - match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), EmptyOptionalLit(_)) => { - match kvs.get(&"None".into()) { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - (RecordLit(kvs), NEOptionalLit(v)) => { - match kvs.get(&"Some".into()) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - _ => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::ToMap(_, _) => unimplemented!("toMap"), - }; - - 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), - } -} - -/// Normalize a ValueKind into WHNF -pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { - match v { - ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(squash_textlit(elts.into_iter())) - } - // All other cases are already in WHNF - v => v, - } -} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs deleted file mode 100644 index 3960146..0000000 --- a/dhall/src/semantics/phase/typecheck.rs +++ /dev/null @@ -1,838 +0,0 @@ -use std::borrow::Cow; -use std::cmp::max; -use std::collections::HashMap; - -use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{Shift, Subst}; -use crate::semantics::phase::normalize::merge_maps; -use crate::semantics::phase::Normalized; -use crate::syntax; -use crate::syntax::{ - Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, - UnspannedExpr, -}; - -fn tck_pi_type( - ctx: &TypecheckContext, - x: Label, - tx: Value, - te: Value, -) -> Result<Value, TypeError> { - use TypeMessage::*; - let ctx2 = ctx.insert_type(&x, tx.clone()); - - let ka = match tx.get_type()?.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), - }; - - let kb = match te.get_type()?.as_const() { - Some(k) => k, - _ => { - return Err(TypeError::new( - &ctx2, - InvalidOutputType(te.get_type()?), - )) - } - }; - - let k = function_check(ka, kb); - - Ok(Value::from_kind_and_type( - ValueKind::Pi(x.into(), tx, te), - Value::from_const(k), - )) -} - -fn tck_record_type( - ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>, -) -> Result<Value, TypeError> { - use std::collections::hash_map::Entry; - use TypeMessage::*; - let mut new_kts = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; - for e in kts { - let (x, t) = e?; - // Construct the union of the contained `Const`s - match t.get_type()?.as_const() { - Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), - } - // Check for duplicated entries - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(ctx, RecordTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - Ok(Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - Value::from_const(k), - )) -} - -fn tck_union_type<Iter>( - ctx: &TypecheckContext, - kts: Iter, -) -> Result<Value, TypeError> -where - Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>, -{ - use std::collections::hash_map::Entry; - use TypeMessage::*; - let mut new_kts = HashMap::new(); - // Check that all types are the same const - let mut k = None; - for e in kts { - let (x, t) = e?; - if let Some(t) = &t { - match (k, t.get_type()?.as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x, t.clone()), - )) - } - } - } - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(ctx, UnionTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - // An empty union type has type Type; - // an union type with only unary variants also has type Type - let k = k.unwrap_or(Const::Type); - - Ok(Value::from_kind_and_type( - ValueKind::UnionType(new_kts), - Value::from_const(k), - )) -} - -fn function_check(a: Const, b: Const) -> Const { - if b == Const::Type { - Const::Type - } else { - max(a, b) - } -} - -pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueKind::Const(c); - match c { - Const::Type => { - Value::from_kind_and_type(v, const_to_value(Const::Kind)) - } - Const::Kind => { - Value::from_kind_and_type(v, const_to_value(Const::Sort)) - } - Const::Sort => Value::const_sort(), - } -} - -pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> { - Expr::new(x, Span::Artificial) -} - -// Ad-hoc macro to help construct the types of builtins -macro_rules! make_type { - (Type) => { ExprKind::Const(Const::Type) }; - (Bool) => { ExprKind::Builtin(Builtin::Bool) }; - (Natural) => { ExprKind::Builtin(Builtin::Natural) }; - (Integer) => { ExprKind::Builtin(Builtin::Integer) }; - (Double) => { ExprKind::Builtin(Builtin::Double) }; - (Text) => { ExprKind::Builtin(Builtin::Text) }; - ($var:ident) => { - ExprKind::Var(syntax::V(stringify!($var).into(), 0)) - }; - (Optional $ty:ident) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::Optional)), - rc(make_type!($ty)) - ) - }; - (List $($rest:tt)*) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - rc(make_type!($($rest)*)) - ) - }; - ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = syntax::map::DupTreeMap::new(); - $( - kts.insert( - Label::from(stringify!($label)), - rc(make_type!($ty)), - ); - )* - ExprKind::RecordType(kts) - }}; - ($ty:ident -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($ty)), - rc(make_type!($($rest)*)) - ) - }; - (($($arg:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($($arg)*)), - rc(make_type!($($rest)*)) - ) - }; - (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - stringify!($var).into(), - rc(make_type!($($ty)*)), - rc(make_type!($($rest)*)) - ) - }; -} - -fn type_of_builtin<E>(b: Builtin) -> Expr<E> { - use syntax::Builtin::*; - rc(match b { - Bool | Natural | Integer | Double | Text => make_type!(Type), - List | Optional => make_type!( - Type -> Type - ), - - NaturalFold => make_type!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => make_type!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => make_type!( - Natural -> Bool - ), - NaturalToInteger => make_type!(Natural -> Integer), - NaturalShow => make_type!(Natural -> Text), - NaturalSubtract => make_type!(Natural -> Natural -> Natural), - - IntegerToDouble => make_type!(Integer -> Double), - IntegerShow => make_type!(Integer -> Text), - IntegerNegate => make_type!(Integer -> Integer), - IntegerClamp => make_type!(Integer -> Natural), - - DoubleShow => make_type!(Double -> Text), - TextShow => make_type!(Text -> Text), - - ListBuild => make_type!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => make_type!( - forall (a: Type) -> - (List a) -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), - ListHead | ListLast => { - make_type!(forall (a: Type) -> (List a) -> Optional a) - } - ListIndexed => make_type!( - forall (a: Type) -> - (List a) -> - List { index: Natural, value: a } - ), - ListReverse => make_type!( - forall (a: Type) -> (List a) -> List a - ), - - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => make_type!( - forall (A: Type) -> Optional A - ), - }) -} - -pub(crate) fn builtin_to_value(b: Builtin) -> Value { - let ctx = TypecheckContext::new(); - Value::from_kind_and_type( - ValueKind::from_builtin(b), - type_with(&ctx, type_of_builtin(b)).unwrap(), - ) -} - -/// Type-check an expression and return the expression alongside its type if type-checking -/// succeeded, or an error if type-checking failed. -/// Some normalization is done while typechecking, so the returned expression might be partially -/// normalized as well. -fn type_with( - ctx: &TypecheckContext, - e: Expr<Normalized>, -) -> Result<Value, TypeError> { - use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; - let span = e.span(); - - Ok(match e.as_ref() { - Lam(var, annot, body) => { - let annot = type_with(ctx, annot.clone())?; - annot.normalize_nf(); - let ctx2 = ctx.insert_type(var, annot.clone()); - let body = type_with(&ctx2, body.clone())?; - let body_type = body.get_type()?; - Value::from_kind_and_type( - ValueKind::Lam(var.clone().into(), annot.clone(), body), - tck_pi_type(ctx, var.clone(), annot, body_type)?, - ) - } - Pi(x, ta, tb) => { - let ta = type_with(ctx, ta.clone())?; - let ctx2 = ctx.insert_type(x, ta.clone()); - let tb = type_with(&ctx2, tb.clone())?; - return tck_pi_type(ctx, x.clone(), ta, tb); - } - Let(x, t, v, e) => { - let v = if let Some(t) = t { - t.rewrap(Annot(v.clone(), t.clone())) - } else { - v.clone() - }; - - let v = type_with(ctx, v)?; - return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); - } - Embed(p) => p.clone().into_typed().into_value(), - Var(var) => match ctx.lookup(&var) { - Some(typed) => typed.clone(), - None => { - return Err(TypeError::new( - ctx, - TypeMessage::UnboundVariable(span), - )) - } - }, - e => { - // Typecheck recursively all subexpressions - let expr = e.traverse_ref_with_special_handling_of_binders( - |e| type_with(ctx, e.clone()), - |_, _| unreachable!(), - )?; - type_last_layer(ctx, expr, span)? - } - }) -} - -/// When all sub-expressions have been typed, check the remaining toplevel -/// layer. -fn type_last_layer( - ctx: &TypecheckContext, - e: ExprKind<Value, Normalized>, - span: Span, -) -> Result<Value, TypeError> { - use syntax::BinOp::*; - use syntax::Builtin::*; - use syntax::Const::Type; - use syntax::ExprKind::*; - use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); - - /// Intermediary return type - enum Ret { - /// Returns the contained value as is - RetWhole(Value), - /// Returns the input expression `e` with the contained value as its type - RetTypeOnly(Value), - } - use Ret::*; - - let ret = match &e { - Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => { - unreachable!() - } - App(f, a) => { - let tf = f.get_type()?; - let tf_borrow = tf.as_whnf(); - let (x, tx, tb) = match &*tf_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), - _ => return mkerr(NotAFunction(f.clone())), - }; - if &a.get_type()? != tx { - return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); - } - - let ret = tb.subst_shift(&x.into(), a); - ret.normalize_nf(); - RetTypeOnly(ret) - } - Annot(x, t) => { - if &x.get_type()? != t { - return mkerr(AnnotMismatch(x.clone(), t.clone())); - } - RetWhole(x.clone()) - } - Assert(t) => { - match &*t.as_whnf() { - ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(x, y) => { - return mkerr(AssertMismatch(x.clone(), y.clone())) - } - _ => return mkerr(AssertMustTakeEquivalence), - } - RetTypeOnly(t.clone()) - } - BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { - return mkerr(InvalidPredicate(x.clone())); - } - - if y.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(true, y.clone())); - } - - if z.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(false, z.clone())); - } - - if y.get_type()? != z.get_type()? { - return mkerr(IfBranchMismatch(y.clone(), z.clone())); - } - - RetTypeOnly(y.get_type()?) - } - EmptyListLit(t) => { - match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args) - if args.len() == 1 => {} - _ => return mkerr(InvalidListType(t.clone())), - } - RetTypeOnly(t.clone()) - } - NEListLit(xs) => { - let mut iter = xs.iter().enumerate(); - let (_, x) = iter.next().unwrap(); - for (i, y) in iter { - if x.get_type()? != y.get_type()? { - return mkerr(InvalidListElement( - i, - x.get_type()?, - y.clone(), - )); - } - } - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t)); - } - - RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) - } - SomeLit(x) => { - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidOptionalType(t)); - } - - RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) - } - RecordType(kts) => RetWhole(tck_record_type( - ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - UnionType(kts) => RetWhole(tck_union_type( - ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - RecordLit(kvs) => RetTypeOnly(tck_record_type( - ctx, - kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), - )?), - Field(r, x) => { - match &*r.get_type()?.as_whnf() { - ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => { - RetTypeOnly(tth.clone()) - }, - None => return mkerr(MissingRecordField(x.clone(), - r.clone())), - }, - // TODO: branch here only when r.get_type() is a Const - _ => { - match &*r.as_whnf() { - ValueKind::UnionType(kts) => match kts.get(&x) { - // Constructor has type T -> < x: T, ... > - Some(Some(t)) => { - RetTypeOnly( - tck_pi_type( - ctx, - x.clone(), - t.clone(), - r.under_binder(x), - )? - ) - }, - Some(None) => { - RetTypeOnly(r.clone()) - }, - None => { - return mkerr(MissingUnionField( - x.clone(), - r.clone(), - )) - }, - }, - _ => { - return mkerr(NotARecord( - x.clone(), - r.clone() - )) - }, - } - } - // _ => mkerr(NotARecord( - // x, - // r?, - // )), - } - } - Const(c) => RetWhole(const_to_value(*c)), - Builtin(b) => RetWhole(builtin_to_value(*b)), - BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), - NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), - IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), - DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), - TextLit(interpolated) => { - let text_type = builtin_to_value(Text); - for contents in interpolated.iter() { - use InterpolatedTextContents::Expr; - if let Expr(x) = contents { - if x.get_type()? != text_type { - return mkerr(InvalidTextInterpolation(x.clone())); - } - } - } - RetTypeOnly(text_type) - } - BinOp(RightBiasedRecordMerge, l, r) => { - let l_type = l.get_type()?; - let r_type = r.get_type()?; - - // Extract the LHS record type - let l_type_borrow = l_type.as_whnf(); - let kts_x = match &*l_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(l.clone())), - }; - - // Extract the RHS record type - let r_type_borrow = r_type.as_whnf(); - let kts_y = match &*r_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(r.clone())), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { - Ok(r_t.clone()) - })?; - - // Construct the final record type from the union - RetTypeOnly(tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), - )?) - } - BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( - ctx, - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.get_type()?, - r.get_type()?, - ), - Span::Artificial, - )?), - BinOp(RecursiveRecordTypeMerge, l, r) => { - // Extract the LHS record type - let borrow_l = l.as_whnf(); - let kts_x = match &*borrow_l { - ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } - }; - - // Extract the RHS record type - let borrow_r = r.as_whnf(); - let kts_y = match &*borrow_r { - ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } - }; - - // Ensure that the records combine without a type error - let kts = merge_maps( - kts_x, - kts_y, - // If the Label exists for both records, then we hit the recursive case. - |_, l: &Value, r: &Value| { - type_last_layer( - ctx, - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - Span::Artificial, - ) - }, - )?; - - RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) - } - BinOp(o @ ListAppend, l, r) => { - match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _) => {} - _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), - } - - if l.get_type()? != r.get_type()? { - return mkerr(BinOpTypeMismatch(*o, r.clone())); - } - - RetTypeOnly(l.get_type()?) - } - BinOp(Equivalence, l, r) => { - if l.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); - } - if r.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); - } - - if l.get_type()? != r.get_type()? { - return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); - } - - RetWhole(Value::from_kind_and_type( - ValueKind::Equivalence(l.clone(), r.clone()), - Value::from_const(Type), - )) - } - BinOp(o, l, r) => { - let t = builtin_to_value(match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, - ListAppend => unreachable!(), - RightBiasedRecordMerge => unreachable!(), - RecursiveRecordMerge => unreachable!(), - RecursiveRecordTypeMerge => unreachable!(), - ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"), - Equivalence => unreachable!(), - }); - - if l.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, l.clone())); - } - - if r.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, r.clone())); - } - - RetTypeOnly(t) - } - Merge(record, union, type_annot) => { - let record_type = record.get_type()?; - let record_borrow = record_type.as_whnf(); - let handlers = match &*record_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), - }; - - let union_type = union.get_type()?; - let union_borrow = union_type.as_whnf(); - let variants = match &*union_borrow { - ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(syntax::Builtin::Optional, args) - if args.len() == 1 => - { - let ty = &args[0]; - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => { - return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone())) - } - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type = - match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let handler_type_borrow = handler_type.as_whnf(); - let (x, tx, tb) = match &*handler_type_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), - _ => { - return mkerr(NotAFunction( - handler_type.clone(), - )) - } - }; - - if variant_type != tx { - return mkerr(TypeMismatch( - handler_type.clone(), - tx.clone(), - variant_type.clone(), - )); - } - - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => return mkerr( - MergeHandlerReturnTypeMustNotBeDependent, - ), - } - } - // Union alternative without type - Some(None) => handler_type.clone(), - None => { - return mkerr(MergeHandlerMissingVariant(x.clone())) - } - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return mkerr(MergeHandlerTypeMismatch); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return mkerr(MergeVariantMissingHandler(x.clone())); - } - } - - match (inferred_type, type_annot.as_ref()) { - (Some(t1), Some(t2)) => { - if &t1 != t2 { - return mkerr(MergeAnnotMismatch); - } - RetTypeOnly(t1) - } - (Some(t), None) => RetTypeOnly(t), - (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr(MergeEmptyNeedsAnnotation), - } - } - ToMap(_, _) => unimplemented!("toMap"), - Projection(record, labels) => { - let record_type = record.get_type()?; - let record_type_borrow = record_type.as_whnf(); - let kts = match &*record_type_borrow { - ValueKind::RecordType(kts) => kts, - _ => return mkerr(ProjectionMustBeRecord), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return mkerr(ProjectionMissingEntry), - Some(t) => { - use std::collections::hash_map::Entry; - match new_kts.entry(l.clone()) { - Entry::Occupied(_) => { - return mkerr(ProjectionDuplicateField) - } - Entry::Vacant(e) => e.insert(t.clone()), - } - } - }; - } - - RetTypeOnly(Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - record_type.get_type()?, - )) - } - ProjectionByExpr(_, _) => unimplemented!("selection by expression"), - Completion(_, _) => unimplemented!("record completion"), - }; - - Ok(match ret { - RetTypeOnly(typ) => Value::from_kind_and_type_and_span( - ValueKind::PartialExpr(e), - typ, - span, - ), - RetWhole(v) => v.with_span(span), - }) -} - -/// `type_of` is the same as `type_with` with an empty context, meaning that the -/// expression must be closed (i.e. no free variables), otherwise type-checking -/// will fail. -pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> { - type_with(&TypecheckContext::new(), e) -} - -pub(crate) fn typecheck_with( - expr: Expr<Normalized>, - ty: Expr<Normalized>, -) -> Result<Value, TypeError> { - typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty))) -} diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/resolve.rs index cc4a024..3acf114 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/resolve.rs @@ -2,9 +2,9 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; use crate::error::{Error, ImportError}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; +use crate::{Normalized, NormalizedExpr, Parsed, Resolved}; type Import = syntax::Import<NormalizedExpr>; diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs new file mode 100644 index 0000000..812ca7a --- /dev/null +++ b/dhall/src/semantics/tck/env.rs @@ -0,0 +1,124 @@ +use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value}; +use crate::syntax::{Label, V}; + +/// Environment for indexing variables. +#[derive(Debug, Clone, Copy)] +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, +} + +impl VarEnv { + pub fn new() -> Self { + VarEnv { size: 0 } + } + pub fn size(&self) -> usize { + self.size + } + pub fn insert(&self) -> Self { + VarEnv { + size: self.size + 1, + } + } + pub fn lookup(&self, var: &NzVar) -> AlphaVar { + self.lookup_fallible(var).unwrap() + } + pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> { + let idx = self.size.checked_sub(var.idx() + 1)?; + Some(AlphaVar::new(idx)) + } +} + +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(), + } + } + pub fn as_varenv(&self) -> VarEnv { + self.names.as_varenv() + } + pub fn as_nzenv(&self) -> &NzEnv { + &self.items + } + pub fn as_nameenv(&self) -> &NameEnv { + &self.names + } + + pub fn insert_type(&self, x: &Label, t: Type) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_type(t), + } + } + pub fn insert_value(&self, x: &Label, e: Value) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_value(e), + } + } + pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> { + let var = self.names.unlabel_var(var)?; + let ty = self.items.lookup_ty(&var); + Some((TyExprKind::Var(var), ty)) + } +} diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs new file mode 100644 index 0000000..1df2a48 --- /dev/null +++ b/dhall/src/semantics/tck/mod.rs @@ -0,0 +1,6 @@ +pub mod env; +pub mod tyexpr; +pub mod typecheck; +pub(crate) use env::*; +pub(crate) use tyexpr::*; +pub(crate) use typecheck::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs new file mode 100644 index 0000000..1a048f9 --- /dev/null +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -0,0 +1,137 @@ +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 + } + 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 new file mode 100644 index 0000000..20076cd --- /dev/null +++ b/dhall/src/semantics/tck/typecheck.rs @@ -0,0 +1,611 @@ +use std::borrow::Cow; +use std::cmp::max; +use std::collections::HashMap; + +use crate::error::{TypeError, TypeMessage}; +use crate::semantics::merge_maps; +use crate::semantics::{ + type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr, + TyExprKind, Type, Value, ValueKind, +}; +use crate::syntax::{ + BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span, +}; +use crate::Normalized; + +fn type_of_recordtype<'a>( + tys: impl Iterator<Item = Cow<'a, TyExpr>>, +) -> Result<Type, TypeError> { + // 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 mkerr("InvalidFieldType"), + } + } + Ok(Value::from_const(k)) +} + +fn function_check(a: Const, b: Const) -> Const { + if b == Const::Type { + Const::Type + } else { + max(a, b) + } +} + +fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> { + let ks = match src.as_const() { + Some(k) => k, + _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))), + }; + let kt = match tgt.as_const() { + Some(k) => k, + _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))), + }; + + Ok(Value::from_const(function_check(ks, kt))) +} + +fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> { + Err(TypeError::new(TypeMessage::Custom(x.to_string()))) +} + +/// When all sub-expressions have been typed, check the remaining toplevel +/// layer. +fn type_one_layer( + env: &TyEnv, + kind: &ExprKind<TyExpr, Normalized>, +) -> Result<Type, TypeError> { + Ok(match kind { + ExprKind::Import(..) => unreachable!( + "There should remain no imports in a resolved expression" + ), + ExprKind::Var(..) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) + | ExprKind::Const(Const::Sort) + | ExprKind::Embed(..) => unreachable!(), // Handled in type_with + + ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Value::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), + ExprKind::TextLit(interpolated) => { + let text_type = Value::from_builtin(Builtin::Text); + for contents in interpolated.iter() { + use InterpolatedTextContents::Expr; + if let Expr(x) = contents { + if x.get_type()? != text_type { + return mkerr("InvalidTextInterpolation"); + } + } + } + text_type + } + ExprKind::EmptyListLit(t) => { + let t = t.eval(env.as_nzenv()); + match &*t.kind() { + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, + args, + .. + }) if args.len() == 1 => {} + _ => return mkerr("InvalidListType"), + }; + t + } + ExprKind::NEListLit(xs) => { + let mut iter = xs.iter(); + let x = iter.next().unwrap(); + for y in iter { + if x.get_type()? != y.get_type()? { + return mkerr("InvalidListElement"); + } + } + let t = x.get_type()?; + if t.get_type()?.as_const() != Some(Const::Type) { + return mkerr("InvalidListType"); + } + + Value::from_builtin(Builtin::List).app(t) + } + ExprKind::SomeLit(x) => { + let t = x.get_type()?; + if t.get_type()?.as_const() != Some(Const::Type) { + return mkerr("InvalidOptionalType"); + } + + Value::from_builtin(Builtin::Optional).app(t) + } + ExprKind::RecordLit(kvs) => { + use std::collections::hash_map::Entry; + let mut kts = HashMap::new(); + for (x, v) in kvs { + // Check for duplicated entries + match kts.entry(x.clone()) { + Entry::Occupied(_) => { + return mkerr("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(v.get_type()?), + }; + } + + let ty = type_of_recordtype( + kts.iter() + .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), + )?; + Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + } + ExprKind::RecordType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + for (x, _) in kts { + // Check for duplicated entries + match seen_fields.entry(x.clone()) { + Entry::Occupied(_) => { + return mkerr("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + } + + type_of_recordtype(kts.iter().map(|(_, t)| Cow::Borrowed(t)))? + } + ExprKind::UnionType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + if let Some(t) = t { + match (k, t.get_type()?.as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => return mkerr("InvalidFieldType"), + } + } + match seen_fields.entry(x) { + Entry::Occupied(_) => { + return mkerr("UnionTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + } + + // An empty union type has type Type; + // an union type with only unary variants also has type Type + let k = k.unwrap_or(Const::Type); + + Value::from_const(k) + } + ExprKind::Field(scrut, x) => { + match &*scrut.get_type()?.kind() { + ValueKind::RecordType(kts) => match kts.get(&x) { + Some(tth) => tth.clone(), + None => return mkerr("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) { + // Constructor has type T -> < x: T, ... > + Some(Some(ty)) => { + let pi_ty = type_of_function( + ty.get_type()?, + scrut.get_type()?, + )?; + Value::from_kind_and_type( + ValueKind::PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant( + scrut_nf, + ), + }, + pi_ty, + ) + } + Some(None) => scrut_nf, + None => return mkerr("MissingUnionField"), + }, + _ => return mkerr("NotARecord"), + } + } // _ => mkerr("NotARecord"), + } + } + ExprKind::Annot(x, t) => { + let t = t.eval(env.as_nzenv()); + let x_ty = x.get_type()?; + if x_ty != t { + return mkerr(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 mkerr(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 mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,)); + } + 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 mkerr("AssertMismatch"), + _ => return mkerr("AssertMustTakeEquivalence"), + } + t + } + ExprKind::App(f, arg) => { + match f.get_type()?.kind() { + ValueKind::PiClosure { annot, closure, .. } => { + if arg.get_type()? != *annot { + // return mkerr(format!("function annot mismatch")); + return mkerr(format!( + "function annot mismatch: ({} : {}) : {}", + arg.to_expr_tyenv(env), + arg.get_type()? + .to_tyexpr(env.as_varenv()) + .to_expr_tyenv(env), + annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env), + )); + } + + let arg_nf = arg.eval(env.as_nzenv()); + closure.apply(arg_nf) + } + _ => return mkerr(format!("apply to not Pi")), + } + } + ExprKind::BoolIf(x, y, z) => { + if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { + return mkerr("InvalidPredicate"); + } + if y.get_type()?.get_type()?.as_const() != Some(Const::Type) { + return mkerr("IfBranchMustBeTerm"); + } + if z.get_type()?.get_type()?.as_const() != Some(Const::Type) { + return mkerr("IfBranchMustBeTerm"); + } + if y.get_type()? != z.get_type()? { + return mkerr("IfBranchMismatch"); + } + + y.get_type()? + } + ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => { + let x_type = x.get_type()?; + let y_type = y.get_type()?; + + // Extract the LHS record type + let kts_x = match x_type.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("MustCombineRecord"), + }; + // Extract the RHS record type + let kts_y = match y_type.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("MustCombineRecord"), + }; + + // Union the two records, prefering + // the values found in the RHS. + let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { + Ok(r_t.clone()) + })?; + + // Construct the final record type + let ty = type_of_recordtype( + kts.iter() + .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), + )?; + Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + } + 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()), + ); + let ty = type_one_layer(env, &ekind)?; + TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial) + .eval(env.as_nzenv()) + } + 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 mkerr("RecordTypeMergeRequiresRecordType"), + }; + let kts_y = match y_val.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("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()), + ), + )?; + } + } + + // 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)) + } + ExprKind::BinOp(BinOp::ListAppend, l, r) => { + let l_ty = l.get_type()?; + match &*l_ty.kind() { + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, + .. + }) => {} + _ => return mkerr("BinOpTypeMismatch"), + } + + if l_ty != r.get_type()? { + return mkerr("BinOpTypeMismatch"); + } + + l_ty + } + ExprKind::BinOp(BinOp::Equivalence, l, r) => { + if l.get_type()? != r.get_type()? { + return mkerr("EquivalenceTypeMismatch"); + } + if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { + return mkerr("EquivalenceArgumentsMustBeTerms"); + } + + Value::from_const(Const::Type) + } + ExprKind::BinOp(o, l, r) => { + let t = Value::from_builtin(match o { + BinOp::BoolAnd + | BinOp::BoolOr + | BinOp::BoolEQ + | BinOp::BoolNE => Builtin::Bool, + BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural, + BinOp::TextAppend => Builtin::Text, + BinOp::ListAppend + | BinOp::RightBiasedRecordMerge + | BinOp::RecursiveRecordMerge + | BinOp::RecursiveRecordTypeMerge + | BinOp::Equivalence => unreachable!(), + BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"), + }); + + if l.get_type()? != t { + return mkerr("BinOpTypeMismatch"); + } + + if r.get_type()? != t { + return mkerr("BinOpTypeMismatch"); + } + + t + } + ExprKind::Merge(record, union, type_annot) => { + let record_type = record.get_type()?; + let handlers = match record_type.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("Merge1ArgMustBeRecord"), + }; + + let union_type = union.get_type()?; + let variants = match union_type.kind() { + ValueKind::UnionType(kts) => Cow::Borrowed(kts), + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::Optional, + args, + .. + }) if args.len() == 1 => { + let ty = &args[0]; + let mut kts = HashMap::new(); + kts.insert("None".into(), None); + kts.insert("Some".into(), Some(ty.clone())); + Cow::Owned(kts) + } + _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), + }; + + let mut inferred_type = None; + for (x, handler_type) in handlers { + let handler_return_type = match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => match handler_type.kind() { + ValueKind::PiClosure { closure, annot, .. } => { + if variant_type != annot { + return mkerr("MergeHandlerTypeMismatch"); + } + + closure.remove_binder().or_else(|()| { + mkerr("MergeReturnTypeIsDependent") + })? + } + _ => return mkerr("NotAFunction"), + }, + // Union alternative without type + Some(None) => handler_type.clone(), + None => return mkerr("MergeHandlerMissingVariant"), + }; + match &inferred_type { + None => inferred_type = Some(handler_return_type), + Some(t) => { + if t != &handler_return_type { + return mkerr("MergeHandlerTypeMismatch"); + } + } + } + } + for x in variants.keys() { + if !handlers.contains_key(x) { + return mkerr("MergeVariantMissingHandler"); + } + } + + let type_annot = + type_annot.as_ref().map(|t| t.eval(env.as_nzenv())); + match (inferred_type, type_annot) { + (Some(t1), Some(t2)) => { + if t1 != t2 { + return mkerr("MergeAnnotMismatch"); + } + t1 + } + (Some(t), None) => t, + (None, Some(t)) => t, + (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), + } + } + ExprKind::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::Projection(record, labels) => { + let record_type = record.get_type()?; + let kts = match record_type.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("ProjectionMustBeRecord"), + }; + + let mut new_kts = HashMap::new(); + for l in labels { + match kts.get(l) { + None => return mkerr("ProjectionMissingEntry"), + Some(t) => { + use std::collections::hash_map::Entry; + match new_kts.entry(l.clone()) { + Entry::Occupied(_) => { + return mkerr("ProjectionDuplicateField") + } + Entry::Vacant(e) => e.insert(t.clone()), + } + } + }; + } + + Value::from_kind_and_type( + ValueKind::RecordType(new_kts), + record_type.get_type()?, + ) + } + ExprKind::ProjectionByExpr(_, _) => { + unimplemented!("selection by expression") + } + ExprKind::Completion(_, _) => unimplemented!("record completion"), + }) +} + +/// `type_with` typechecks an expressio in the provided environment. +pub(crate) fn type_with( + env: &TyEnv, + expr: &Expr<Normalized>, +) -> Result<TyExpr, TypeError> { + let (tyekind, ty) = match expr.as_ref() { + ExprKind::Var(var) => match env.lookup(&var) { + Some((k, ty)) => (k, Some(ty)), + None => return mkerr("unbound variable"), + }, + 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.clone()); + let body = type_with(&body_env, body)?; + let body_ty = body.get_type()?; + let ty = TyExpr::new( + TyExprKind::Expr(ExprKind::Pi( + binder.clone(), + annot.clone(), + body_ty.to_tyexpr(body_env.as_varenv()), + )), + Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), + Span::Artificial, + ); + let ty = ty.eval(env.as_nzenv()); + ( + TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), + Some(ty), + ) + } + ExprKind::Pi(binder, annot, body) => { + let annot = type_with(env, annot)?; + let annot_nf = annot.eval(env.as_nzenv()); + let body = + type_with(&env.insert_type(binder, annot_nf.clone()), body)?; + let ty = type_of_function(annot.get_type()?, body.get_type()?)?; + ( + TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), + Some(ty), + ) + } + 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)?; + let val_nf = val.eval(&env.as_nzenv()); + let body = type_with(&env.insert_value(&binder, val_nf), body)?; + let body_ty = body.get_type().ok(); + ( + TyExprKind::Expr(ExprKind::Let( + binder.clone(), + None, + val, + body, + )), + body_ty, + ) + } + 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 = ekind.traverse_ref(|e| type_with(env, e))?; + let ty = type_one_layer(env, &ekind)?; + (TyExprKind::Expr(ekind), Some(ty)) + } + }; + + Ok(TyExpr::new(tyekind, ty, expr.span())) +} + +/// 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> { + type_with(&TyEnv::new(), e) +} + +/// 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))) +} diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs deleted file mode 100644 index b21fb29..0000000 --- a/dhall/src/semantics/to_expr.rs +++ /dev/null @@ -1,105 +0,0 @@ -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::NormalizedExpr; -use crate::syntax; -use crate::syntax::{Builtin, ExprKind}; - -#[derive(Copy, Clone)] -/// Controls conversion from `Value` to `Expr` -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - -/// Converts a value back to the corresponding AST expression. -pub(crate) fn value_to_expr( - val: &Value, - opts: ToExprOptions, -) -> NormalizedExpr { - if opts.normalize { - val.normalize_whnf(); - } - val.as_kind().to_expr(opts) -} - -/// Converts a value back to the corresponding AST expression. -pub(crate) fn kind_to_expr( - kind: &ValueKind, - opts: ToExprOptions, -) -> NormalizedExpr { - match kind { - ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprKind::Builtin(*b)), |acc, v| { - rc(ExprKind::App(acc, v)) - }), - ValueKind::Pi(x, t, e) => rc(ExprKind::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprKind::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::OptionalNone)), - n.to_expr(opts), - )), - ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => { - rc(ExprKind::EmptyListLit(rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - n.to_expr(opts), - )))) - } - ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprKind::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprKind::UnionType( - kts.iter() - .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) - .collect(), - )), - ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( - ValueKind::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprKind::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } -} diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 68cb524..28a0aee 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -24,7 +24,7 @@ pub enum Const { /// The `Int` field is a DeBruijn index. /// See dhall-lang/standard/semantics.md for details #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub struct V<Label>(pub Label, pub usize); +pub struct V(pub Label, pub usize); // Definition order must match precedence order for // pretty-printing to work correctly @@ -112,7 +112,7 @@ pub enum ExprKind<SubExpr, Embed> { Const(Const), /// `x` /// `x@n` - Var(V<Label>), + Var(V), /// `λ(x : A) -> b` Lam(Label, SubExpr, SubExpr), /// `A -> B` @@ -174,29 +174,38 @@ pub enum ExprKind<SubExpr, Embed> { } impl<SE, E> ExprKind<SE, E> { + 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) + } + pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>( &'a self, - visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, - visit_under_binder: impl FnOnce(&'a Label, &'a SE) -> Result<SE2, Err>, + 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, { - visitor::TraverseRefWithBindersVisitor { - visit_subexpr, - visit_under_binder, - } - .visit(self) + self.traverse_ref_maybe_binder(|l, x| match l { + None => visit_subexpr(x), + Some(l) => visit_under_binder(l, x), + }) } - fn traverse_ref<'a, SE2, Err>( + pub(crate) fn traverse_ref<'a, SE2, Err>( &'a self, - visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, + mut visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, ) -> Result<ExprKind<SE2, E>, Err> where E: Clone, { - visitor::TraverseRefVisitor { visit_subexpr }.visit(self) + self.traverse_ref_maybe_binder(|_, e| visit_subexpr(e)) } fn traverse_mut<'a, Err>( @@ -206,6 +215,16 @@ impl<SE, E> ExprKind<SE, E> { 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, + { + trivial_result(self.traverse_ref_maybe_binder(|l, x| Ok(map(l, x)))) + } + pub fn map_ref_with_special_handling_of_binders<'a, SE2>( &'a self, mut map_subexpr: impl FnMut(&'a SE) -> SE2, @@ -214,10 +233,10 @@ impl<SE, E> ExprKind<SE, E> { where E: Clone, { - trivial_result(self.traverse_ref_with_special_handling_of_binders( - |x| Ok(map_subexpr(x)), - |l, x| Ok(map_under_binder(l, x)), - )) + self.map_ref_maybe_binder(|l, x| match l { + None => map_subexpr(x), + Some(l) => map_under_binder(l, x), + }) } pub fn map_ref<'a, SE2>( @@ -227,7 +246,7 @@ impl<SE, E> ExprKind<SE, E> { where E: Clone, { - trivial_result(self.traverse_ref(|x| Ok(map_subexpr(x)))) + 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)) { @@ -295,22 +314,6 @@ impl<E> Expr<E> { } } -impl<Label: PartialEq + Clone> V<Label> { - pub fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> { - let V(x, n) = var; - let V(y, m) = self; - Some(if x == y && n <= m { - V(y.clone(), add_ui(*m, delta)?) - } else { - V(y.clone(), *m) - }) - } - - pub fn over_binder(&self, x: &Label) -> Option<Self> { - self.shift(-1, &V(x.clone(), 0)) - } -} - pub fn trivial_result<T>(x: Result<T, !>) -> T { match x { Ok(x) => x, @@ -318,16 +321,6 @@ pub fn trivial_result<T>(x: Result<T, !>) -> T { } } -/// Add an isize to an usize -/// Returns `None` on over/underflow -fn add_ui(u: usize, i: isize) -> Option<usize> { - Some(if i < 0 { - u.checked_sub(i.checked_neg()? as usize)? - } else { - u.checked_add(i as usize)? - }) -} - impl PartialEq for NaiveDouble { fn eq(&self, other: &Self) -> bool { self.0.to_bits() == other.0.to_bits() @@ -357,9 +350,8 @@ impl From<NaiveDouble> for f64 { } } -/// This is only for the specific `Label` type, not generic -impl From<Label> for V<Label> { - fn from(x: Label) -> V<Label> { +impl From<Label> for V { + fn from(x: Label) -> V { V(x, 0) } } diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs index 424048b..6a1ce7d 100644 --- a/dhall/src/syntax/ast/visitor.rs +++ b/dhall/src/syntax/ast/visitor.rs @@ -1,6 +1,7 @@ -use crate::syntax::*; 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 @@ -295,51 +296,26 @@ where Ok(()) } -pub struct TraverseRefWithBindersVisitor<F1, F2> { - pub visit_subexpr: F1, - pub visit_under_binder: F2, -} +pub struct TraverseRefMaybeBinderVisitor<F>(pub F); -impl<'a, SE, E, SE2, Err, F1, F2> ExprKindVisitor<'a, SE, SE2, E, E> - for TraverseRefWithBindersVisitor<F1, F2> +impl<'a, SE, E, SE2, Err, F> ExprKindVisitor<'a, SE, SE2, E, E> + for TraverseRefMaybeBinderVisitor<F> where SE: 'a, E: 'a + Clone, - F1: FnMut(&'a SE) -> Result<SE2, Err>, - F2: FnOnce(&'a Label, &'a SE) -> Result<SE2, Err>, + 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.visit_subexpr)(subexpr) + (self.0)(None, subexpr) } fn visit_subexpr_under_binder( - self, + mut self, label: &'a Label, subexpr: &'a SE, ) -> Result<SE2, Self::Error> { - (self.visit_under_binder)(label, subexpr) - } - fn visit_embed(self, embed: &'a E) -> Result<E, Self::Error> { - Ok(embed.clone()) - } -} - -pub struct TraverseRefVisitor<F1> { - pub visit_subexpr: F1, -} - -impl<'a, SE, E, SE2, Err, F1> ExprKindVisitor<'a, SE, SE2, E, E> - for TraverseRefVisitor<F1> -where - SE: 'a, - E: 'a + Clone, - F1: FnMut(&'a SE) -> Result<SE2, Err>, -{ - type Error = Err; - - fn visit_subexpr(&mut self, subexpr: &'a SE) -> Result<SE2, Self::Error> { - (self.visit_subexpr)(subexpr) + (self.0)(Some(label), subexpr) } fn visit_embed(self, embed: &'a E) -> Result<E, Self::Error> { Ok(embed.clone()) diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs index c18deb5..52b699c 100644 --- a/dhall/src/syntax/binary/decode.rs +++ b/dhall/src/syntax/binary/decode.rs @@ -3,13 +3,13 @@ use serde_cbor::value::value as cbor; use std::iter::FromIterator; use crate::error::DecodeError; -use crate::semantics::phase::DecodedExpr; use crate::syntax; use crate::syntax::{ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr, URL, V, }; +use crate::DecodedExpr; pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> { match serde_cbor::de::from_slice(data) { diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf new file mode 120000 index 0000000..4a95034 --- /dev/null +++ b/dhall/src/syntax/text/dhall.abnf @@ -0,0 +1 @@ +../../../../dhall-lang/standard/dhall.abnf
\ No newline at end of file diff --git a/dhall/src/dhall.pest.visibility b/dhall/src/syntax/text/dhall.pest.visibility index 03a000b..03a000b 100644 --- a/dhall/src/dhall.pest.visibility +++ b/dhall/src/syntax/text/dhall.pest.visibility diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index ef1471f..2ec63e2 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -5,7 +5,6 @@ use std::rc::Rc; use pest_consume::{match_nodes, Parser}; -use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::map::{DupTreeMap, DupTreeSet}; use crate::syntax::ExprKind::*; @@ -14,6 +13,7 @@ use crate::syntax::{ 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 @@ -422,7 +422,7 @@ impl DhallParser { )) } - fn variable(input: ParseInput) -> ParseResult<V<Label>> { + fn variable(input: ParseInput) -> ParseResult<V> { Ok(match_nodes!(input.into_children(); [label(l), natural_literal(idx)] => V(l, idx), [label(l)] => V(l, 0), diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs index 96f4c2a..06dd70f 100644 --- a/dhall/src/syntax/text/printer.rs +++ b/dhall/src/syntax/text/printer.rs @@ -496,7 +496,7 @@ impl Display for Scheme { } } -impl<Label: Display> Display for V<Label> { +impl Display for V { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let V(x, n) = self; x.fmt(f)?; diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f1648cf..8216243 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -48,7 +48,7 @@ use std::io::{Read, Write}; use std::path::PathBuf; use crate::error::{Error, Result}; -use crate::semantics::phase::Parsed; +use crate::Parsed; #[allow(dead_code)] #[derive(Clone)] @@ -165,20 +165,17 @@ pub fn run_test(test: Test<'_>) -> Result<()> { assert_eq_display!(ty, expected); } TypeInferenceFailure(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); if let Ok(e) = &res { // If e did typecheck, check that get_type fails - res = e.get_type(); + e.get_type().unwrap_err(); } - res.unwrap_err(); } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just // `rm -r dhall/tests/type-errors` and run the tests again. TypeError(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); let file_path = PathBuf::from(file_path); let error_file_path = file_path .strip_prefix("../dhall-lang/tests/type-inference/failure/") @@ -186,11 +183,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> { let error_file_path = PathBuf::from("tests/type-errors/").join(error_file_path); let error_file_path = error_file_path.with_extension("txt"); - if let Ok(e) = &res { - // If e did typecheck, check that get_type fails - res = e.get_type(); - } - let err: Error = res.unwrap_err().into(); + let err: Error = match res { + Ok(e) => { + // If e did typecheck, check that get_type fails + e.get_type().unwrap_err().into() + } + Err(e) => e.into(), + }; if error_file_path.is_file() { let expected_msg = std::fs::read_to_string(error_file_path)?; |