summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/core/value.rs38
-rw-r--r--dhall/src/core/valuef.rs7
-rw-r--r--dhall/src/error/mod.rs20
-rw-r--r--dhall/src/phase/mod.rs15
-rw-r--r--dhall/src/phase/normalize.rs94
-rw-r--r--dhall/src/phase/typecheck.rs198
-rw-r--r--dhall/src/tests.rs2
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 => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:34:46 +0000