diff options
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/core/value.rs | 38 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 7 | ||||
-rw-r--r-- | dhall/src/error/mod.rs | 20 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 15 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 94 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 198 | ||||
-rw-r--r-- | dhall/src/tests.rs | 2 |
7 files changed, 182 insertions, 192 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index ef43e3e..213a2bd 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -193,23 +193,17 @@ impl Value { Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// WARNING: avoid normalizing any thunk while holding on to this ref - /// or you could run into BorrowMut panics - /// TODO: deprecated because of misleading name - pub(crate) fn as_valuef(&self) -> Ref<ValueF> { - self.as_whnf() - } - - /// WARNING: avoid normalizing any thunk while holding on to this ref - /// or you could run into BorrowMut panics + /// 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<ValueF> { self.do_normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_whnf) } - /// TODO: deprecated because of misleading name - pub(crate) fn to_valuef(&self) -> ValueF { - self.as_valuef().clone() + /// TODO: cloning a valuef can often be avoided + pub(crate) fn to_whnf(&self) -> ValueF { + self.as_whnf().clone() } pub(crate) fn normalize_to_expr_maybe_alpha( @@ -275,14 +269,19 @@ impl TypedValue { TypedValue(Value::from_valuef_and_type(v, t)) } - pub(crate) fn to_valuef(&self) -> ValueF { - self.0.to_valuef() + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref<ValueF> { + self.0.as_whnf() + } + pub(crate) fn to_whnf(&self) -> ValueF { + self.0.to_whnf() } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr() + self.as_whnf().normalize_to_expr() } pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr_maybe_alpha(true) + self.as_whnf().normalize_to_expr_maybe_alpha(true) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -294,8 +293,7 @@ impl TypedValue { Typed::from_typedvalue(self) } pub(crate) fn as_const(&self) -> Option<Const> { - // TODO: avoid clone - match &self.to_valuef() { + match &*self.as_whnf() { ValueF::Const(c) => Some(*c), _ => None, } @@ -357,14 +355,14 @@ impl Subst<Typed> for TypedValue { impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - *self.as_valuef() == *other.as_valuef() + *self.as_whnf() == *other.as_whnf() } } impl std::cmp::Eq for Value {} impl std::cmp::PartialEq for TypedValue { fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() + &*self.as_whnf() == &*other.as_whnf() } } impl std::cmp::Eq for TypedValue {} diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 9e6e8c8..0ba1d59 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -12,8 +12,9 @@ use crate::phase::{Normalized, Typed}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. -/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize as needed. +/// If you compare for equality two `ValueF`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(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures @@ -348,7 +349,7 @@ impl Subst<Typed> for ValueF { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - ValueF::Var(v) if v == var => val.to_valuef(), + ValueF::Var(v) if v == var => val.to_whnf(), ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), ValueF::Const(c) => ValueF::Const(*c), ValueF::BoolLit(b) => ValueF::BoolLit(*b), diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 8f6ff51..34a89c0 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -4,7 +4,7 @@ use dhall_syntax::{BinOp, Import, Label, ParseError, V}; use crate::core::context::TypecheckContext; use crate::phase::resolve::ImportStack; -use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; +use crate::phase::{NormalizedSubExpr, Type, Typed}; pub type Result<T> = std::result::Result<T, Error>; @@ -48,24 +48,24 @@ pub struct TypeError { #[derive(Debug)] pub(crate) enum TypeMessage { UnboundVariable(V<Label>), - InvalidInputType(Normalized), - InvalidOutputType(Normalized), + InvalidInputType(Typed), + InvalidOutputType(Typed), NotAFunction(Typed), - TypeMismatch(Typed, Normalized, Typed), - AnnotMismatch(Typed, Normalized), + TypeMismatch(Typed, Typed, Typed), + AnnotMismatch(Typed, Typed), Untyped, FieldCollision(Label), - InvalidListElement(usize, Normalized, Typed), - InvalidListType(Normalized), - InvalidOptionalType(Normalized), + InvalidListElement(usize, Typed, Typed), + InvalidListType(Typed), + InvalidOptionalType(Typed), InvalidPredicate(Typed), IfBranchMismatch(Typed, Typed), IfBranchMustBeTerm(bool, Typed), InvalidFieldType(Label, Type), - NotARecord(Label, Normalized), + NotARecord(Label, Typed), MustCombineRecord(Typed), MissingRecordField(Label, Typed), - MissingUnionField(Label, Normalized), + MissingUnionField(Label, Typed), BinOpTypeMismatch(BinOp, Typed), InvalidTextInterpolation(Typed), Merge1ArgMustBeRecord(Typed), diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index c18f976..a38e9d3 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -1,4 +1,5 @@ use std::borrow::Cow; +use std::cell::Ref; use std::fmt::Display; use std::path::Path; @@ -111,8 +112,13 @@ impl Typed { Typed::from_const(Const::Type) } - pub(crate) fn to_valuef(&self) -> ValueF { - self.0.to_valuef() + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref<ValueF> { + self.0.as_whnf() + } + pub(crate) fn to_whnf(&self) -> ValueF { + self.0.to_whnf() } pub fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() @@ -134,9 +140,6 @@ impl Typed { pub(crate) fn into_typedvalue(self) -> TypedValue { self.0 } - pub(crate) fn to_normalized(&self) -> Normalized { - self.clone().normalize() - } pub(crate) fn as_const(&self) -> Option<Const> { self.0.as_const() } @@ -229,7 +232,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() + self.0 == other.0 } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 6c65e43..785a75f 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -68,23 +68,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { r, EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())), )), - (NaturalIsZero, [n, r..]) => match &*n.as_valuef() { + (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), }, - (NaturalEven, [n, r..]) => match &*n.as_valuef() { + (NaturalEven, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), _ => Err(()), }, - (NaturalOdd, [n, r..]) => match &*n.as_valuef() { + (NaturalOdd, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), _ => Err(()), }, - (NaturalToInteger, [n, r..]) => match &*n.as_valuef() { + (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), _ => Err(()), }, - (NaturalShow, [n, r..]) => match &*n.as_valuef() { + (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), @@ -92,7 +92,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_valuef(), &*b.as_valuef()) { + match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => { Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) } @@ -102,7 +102,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { _ => Err(()), } } - (IntegerShow, [n, r..]) => match &*n.as_valuef() { + (IntegerShow, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -113,18 +113,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (IntegerToDouble, [n, r..]) => match &*n.as_valuef() { + (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), _ => Err(()), }, - (DoubleShow, [n, r..]) => match &*n.as_valuef() { + (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), )), _ => Err(()), }, - (TextShow, [v, r..]) => match &*v.as_valuef() { + (TextShow, [v, r..]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -158,33 +158,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (ListLength, [_, l, r..]) => match &*l.as_valuef() { + (ListLength, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(_) => Ok((r, NaturalLit(0))), NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), _ => Err(()), }, - (ListHead, [_, l, r..]) => match &*l.as_valuef() { + (ListHead, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) } _ => Err(()), }, - (ListLast, [_, l, r..]) => match &*l.as_valuef() { + (ListLast, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()))) } _ => Err(()), }, - (ListReverse, [_, l, r..]) => match &*l.as_valuef() { + (ListReverse, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), NEListLit(xs) => { Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) } _ => Err(()), }, - (ListIndexed, [_, l, r..]) => match &*l.as_valuef() { + (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); kts.insert( @@ -210,11 +210,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (ListBuild, [t, f, r..]) => match &*f.as_valuef() { + (ListBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_valuef())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -237,8 +237,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { )), )), }, - (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() { - EmptyListLit(_) => Ok((r, nil.to_valuef())), + (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { + EmptyListLit(_) => Ok((r, nil.to_whnf())), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { @@ -248,15 +248,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .app_value(v) .into_value(); } - Ok((r, v.to_valuef())) + Ok((r, v.to_whnf())) } _ => Err(()), }, - (OptionalBuild, [t, f, r..]) => match &*f.as_valuef() { + (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_valuef())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -273,18 +273,16 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { )), )), }, - (OptionalFold, [_, v, _, just, nothing, r..]) => { - match &*v.as_valuef() { - EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())), - NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), - _ => Err(()), - } - } - (NaturalBuild, [f, r..]) => match &*f.as_valuef() { + (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { + EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), + _ => Err(()), + }, + (NaturalBuild, [f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_valuef())) + Ok((r, args[0].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -297,8 +295,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .app_valuef(NaturalLit(0)), )), }, - (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() { - NaturalLit(0) => Ok((r, zero.to_valuef())), + (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { + NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { let fold = ValueF::from_builtin(NaturalFold) .app(NaturalLit(n - 1)) @@ -326,11 +324,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); - let f_borrow = f.as_valuef(); + let f_borrow = f.as_whnf(); match &*f_borrow { ValueF::Lam(x, _, e) => { let val = Typed::from_value_untyped(a); - e.subst_shift(&x.into(), &val).to_valuef() + e.subst_shift(&x.into(), &val).to_whnf() } ValueF::AppliedBuiltin(b, args) => { use std::iter::once; @@ -362,7 +360,7 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_valuef(); + let e_borrow = e.as_whnf(); match &*e_borrow { ValueF::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) @@ -520,8 +518,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_valuef(); - let y_borrow = y.as_valuef(); + 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), @@ -678,7 +676,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), ExprF::EmptyListLit(ref t) => { // Check if the type is of the form `List x` - let t_borrow = t.as_valuef(); + let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { Ret::ValueF(EmptyListLit( @@ -718,13 +716,13 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } } ExprF::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_valuef(); + let b_borrow = b.as_whnf(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_valuef(); - let e2_borrow = e2.as_valuef(); + 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), @@ -748,7 +746,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { Ret::ValueF(RecordLit(HashMap::new())) } ExprF::Projection(ref v, ref ls) => { - let v_borrow = v.as_valuef(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => Ret::ValueF(RecordLit( ls.iter() @@ -764,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } } ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_valuef(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Value(r.clone()), @@ -784,8 +782,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } ExprF::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_valuef(); - let variant_borrow = variant.as_valuef(); + 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()), @@ -814,8 +812,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { match ret { Ret::ValueF(v) => v, - Ret::Value(th) => th.to_valuef(), - Ret::ValueRef(th) => th.to_valuef(), + Ret::Value(th) => th.as_whnf().clone(), + Ret::ValueRef(th) => th.as_whnf().clone(), Ret::Expr(expr) => ValueF::PartialExpr(expr), } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4154afe..c303ada 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -22,12 +22,7 @@ fn tck_pi_type( let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - ctx, - InvalidInputType(tx.to_normalized()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { @@ -35,7 +30,7 @@ fn tck_pi_type( _ => { return Err(TypeError::new( &ctx2, - InvalidOutputType(te.get_type()?.to_normalized()), + InvalidOutputType(te.get_type()?.into_owned()), )) } }; @@ -415,18 +410,14 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &tf.to_valuef() { + let (x, tx, tb) = match &*tf.as_whnf() { ValueF::Pi(x, tx, tb) => { (x.clone(), tx.to_type(), tb.to_type()) } _ => return Err(mkerr(NotAFunction(f.clone()))), }; if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch( - f.clone(), - tx.to_normalized(), - a.clone(), - ))); + return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone()))); } Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) @@ -434,13 +425,13 @@ fn type_last_layer( Annot(x, t) => { let t = t.to_type(); if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized()))); + return Err(mkerr(AnnotMismatch(x.clone(), t))); } Ok(RetTypeOnly(x.get_type()?.into_owned())) } Assert(t) => { - match t.to_valuef() { - ValueF::Equivalence(ref x, ref y) if x == y => {} + match &*t.as_whnf() { + ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { return Err(mkerr(AssertMismatch( x.to_typed(), @@ -472,14 +463,11 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - match &t.to_valuef() { + match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidListType(t.to_normalized()), - )) + return Err(TypeError::new(ctx, InvalidListType(t.clone()))) } } Ok(RetTypeOnly(t)) @@ -491,7 +479,7 @@ fn type_last_layer( if x.get_type()? != y.get_type()? { return Err(mkerr(InvalidListElement( i, - x.get_type()?.to_normalized(), + x.get_type()?.into_owned(), y.clone(), ))); } @@ -500,14 +488,14 @@ fn type_last_layer( if t.get_type()?.as_const() != Some(Type) { return Err(TypeError::new( ctx, - InvalidListType(t.to_normalized()), + InvalidListType(t.into_owned()), )); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type), ) @@ -517,16 +505,13 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?.into_owned(); if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidOptionalType(t.to_normalized()), - )); + return Err(TypeError::new(ctx, InvalidOptionalType(t))); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type).into_type(), ) @@ -551,7 +536,7 @@ fn type_last_layer( .into_type(), )), Field(r, x) => { - match &r.get_type()?.to_valuef() { + match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { Ok(RetTypeOnly(tth.to_type())) @@ -561,8 +546,7 @@ fn type_last_layer( }, // TODO: branch here only when r.get_type() is a Const _ => { - let r = r.to_type(); - match &r.to_valuef() { + match &*r.as_whnf() { ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { @@ -581,21 +565,21 @@ fn type_last_layer( None => { Err(mkerr(MissingUnionField( x.clone(), - r.to_normalized(), + r.clone(), ))) }, }, _ => { Err(mkerr(NotARecord( x.clone(), - r.to_normalized() + r.clone() ))) }, } } // _ => Err(mkerr(NotARecord( // x, - // r.to_type()?.to_normalized(), + // r.to_type()?, // ))), } } @@ -633,20 +617,22 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(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| r_t.clone()); + let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union Ok(RetTypeOnly( @@ -662,8 +648,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedValue>, - kts_r: HashMap<Label, TypedValue>, + kts_l: &HashMap<Label, TypedValue>, + kts_r: &HashMap<Label, TypedValue>, ) -> Result<Typed, TypeError> { use crate::phase::normalize::outer_join; @@ -674,7 +660,7 @@ fn type_last_layer( inner_l: &TypedValue, inner_r: &TypedValue| -> Result<Typed, TypeError> { - match (inner_l.to_valuef(), inner_r.to_valuef()) { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { ( ValueF::RecordType(inner_l_kvs), ValueF::RecordType(inner_r_kvs), @@ -690,11 +676,9 @@ fn type_last_layer( let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, + combine, + kts_l, + kts_r, ); Ok(tck_record_type( @@ -717,13 +701,15 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -735,8 +721,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedValue>, - kts_r: HashMap<Label, TypedValue>, + kts_l: &HashMap<Label, TypedValue>, + kts_r: &HashMap<Label, TypedValue>, ) -> Result<Typed, TypeError> { use crate::phase::normalize::intersection_with_key; @@ -747,7 +733,7 @@ fn type_last_layer( kts_l_inner: &TypedValue, kts_r_inner: &TypedValue| -> Result<Typed, TypeError> { - match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { ( ValueF::RecordType(kvs_l_inner), ValueF::RecordType(kvs_r_inner), @@ -760,13 +746,7 @@ fn type_last_layer( } }; - let kts = intersection_with_key( - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, - ); + let kts = intersection_with_key(combine, kts_l, kts_r); Ok(tck_record_type( ctx, @@ -776,8 +756,8 @@ fn type_last_layer( }; // Extract the Const of the LHS - let k_l = match l.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_l = match l.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -786,8 +766,8 @@ fn type_last_layer( }; // Extract the Const of the RHS - let k_r = match r.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_r = match r.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -808,7 +788,8 @@ fn type_last_layer( }; // Extract the LHS record type - let kts_x = match l.to_valuef() { + let borrow_l = l.as_whnf(); + let kts_x = match &*borrow_l { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -818,7 +799,8 @@ fn type_last_layer( }; // Extract the RHS record type - let kts_y = match r.to_valuef() { + let borrow_r = r.as_whnf(); + let kts_y = match &*borrow_r { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -833,7 +815,7 @@ fn type_last_layer( .and(Ok(RetTypeOnly(Typed::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_valuef() { + match &*l.get_type()?.as_whnf() { ValueF::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -895,56 +877,63 @@ fn type_last_layer( Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let handlers = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), }; - let variants = match union.get_type()?.to_valuef() { + let union_type = union.get_type()?; + let union_borrow = union_type.as_whnf(); + let variants = match &*union_borrow { ValueF::UnionType(kts) => kts, _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), }; let mut inferred_type = None; - for (x, handler) in handlers.iter() { - let handler_return_type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &handler_type.to_valuef() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) + for (x, handler) in handlers { + let handler_return_type = + match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => { + let variant_type = variant_type.to_type(); + let handler_type = handler.to_type(); + let (x, tx, tb) = match &*handler_type.as_whnf() { + ValueF::Pi(x, tx, tb) => { + (x.clone(), tx.to_type(), tb.to_type()) + } + _ => { + return Err(mkerr(NotAFunction( + handler_type.clone(), + ))) + } + }; + + if &variant_type != &tx { + return Err(mkerr(TypeMismatch( + handler_type, + tx, + variant_type, + ))); } - _ => return Err(mkerr(NotAFunction(handler_type))), - }; - - if &variant_type != &tx { - return Err(mkerr(TypeMismatch( - handler_type, - tx.to_normalized(), - variant_type, - ))); - } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => { - return Err(mkerr( + // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. + match tb.over_binder(x) { + Some(x) => x, + None => return Err(mkerr( MergeHandlerReturnTypeMustNotBeDependent, - )) + )), } } - } - // Union alternative without type - Some(None) => handler.to_type(), - None => { - return Err(mkerr(MergeHandlerMissingVariant( - x.clone(), - ))) - } - }; + // Union alternative without type + Some(None) => handler.to_type(), + None => { + return Err(mkerr(MergeHandlerMissingVariant( + x.clone(), + ))) + } + }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { @@ -974,8 +963,9 @@ fn type_last_layer( } } Projection(record, labels) => { - let trecord = record.get_type()?; - let kts = match trecord.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let kts = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(ProjectionMustBeRecord)), }; @@ -991,7 +981,7 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::RecordType(new_kts).into_value(), - trecord.get_type()?.into_owned(), + record_type.get_type()?.into_owned(), ) .to_type(), )) diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 70cff46..44e22e4 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -185,7 +185,7 @@ pub fn run_test( } TypeInference => { let expr = expr.typecheck()?; - let ty = expr.get_type()?.to_normalized(); + let ty = expr.get_type()?.into_owned().normalize(); assert_eq_display!(ty, expected); } Normalization => { |