summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs40
-rw-r--r--dhall/src/semantics/core/value.rs10
-rw-r--r--dhall/src/semantics/phase/normalize.rs26
-rw-r--r--dhall/src/semantics/tck/typecheck.rs32
4 files changed, 53 insertions, 55 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index a23591e..a536261 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -290,31 +290,31 @@ fn apply_builtin(
let ret = match (b, args.as_slice()) {
(OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
- (NaturalIsZero, [n]) => match &*n.as_whnf() {
+ (NaturalIsZero, [n]) => match &*n.kind() {
NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
_ => Ret::DoneAsIs,
},
- (NaturalEven, [n]) => match &*n.as_whnf() {
+ (NaturalEven, [n]) => match &*n.kind() {
NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
_ => Ret::DoneAsIs,
},
- (NaturalOdd, [n]) => match &*n.as_whnf() {
+ (NaturalOdd, [n]) => match &*n.kind() {
NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
_ => Ret::DoneAsIs,
},
- (NaturalToInteger, [n]) => match &*n.as_whnf() {
+ (NaturalToInteger, [n]) => match &*n.kind() {
NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
_ => Ret::DoneAsIs,
},
(NaturalShow, [n]) => {
- match &*n.as_whnf() {
+ match &*n.kind() {
NaturalLit(n) => Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(n.to_string()),
])),
_ => Ret::DoneAsIs,
}
}
- (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+ (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
(NaturalLit(a), NaturalLit(b)) => {
Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
}
@@ -323,7 +323,7 @@ fn apply_builtin(
_ if a == b => Ret::ValueKind(NaturalLit(0)),
_ => Ret::DoneAsIs,
},
- (IntegerShow, [n]) => match &*n.as_whnf() {
+ (IntegerShow, [n]) => match &*n.kind() {
IntegerLit(n) => {
let s = if *n < 0 {
n.to_string()
@@ -334,31 +334,31 @@ fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
- (IntegerToDouble, [n]) => match &*n.as_whnf() {
+ (IntegerToDouble, [n]) => match &*n.kind() {
IntegerLit(n) => {
Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
}
_ => Ret::DoneAsIs,
},
- (IntegerNegate, [n]) => match &*n.as_whnf() {
+ (IntegerNegate, [n]) => match &*n.kind() {
IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
_ => Ret::DoneAsIs,
},
- (IntegerClamp, [n]) => match &*n.as_whnf() {
+ (IntegerClamp, [n]) => match &*n.kind() {
IntegerLit(n) => {
Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
}
_ => Ret::DoneAsIs,
},
(DoubleShow, [n]) => {
- match &*n.as_whnf() {
+ match &*n.kind() {
DoubleLit(n) => Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(n.to_string()),
])),
_ => Ret::DoneAsIs,
}
}
- (TextShow, [v]) => match &*v.as_whnf() {
+ (TextShow, [v]) => match &*v.kind() {
TextLit(elts) => {
match elts.as_slice() {
// Empty string literal.
@@ -390,26 +390,26 @@ fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
- (ListLength, [_, l]) => match &*l.as_whnf() {
+ (ListLength, [_, l]) => match &*l.kind() {
EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
_ => Ret::DoneAsIs,
},
- (ListHead, [_, l]) => match &*l.as_whnf() {
+ (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.as_whnf() {
+ (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.as_whnf() {
+ (ListReverse, [_, l]) => match &*l.kind() {
EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
@@ -417,7 +417,7 @@ fn apply_builtin(
_ => Ret::DoneAsIs,
},
(ListIndexed, [_, l]) => {
- let l_whnf = l.as_whnf();
+ let l_whnf = l.kind();
match &*l_whnf {
EmptyListLit(_) | NEListLit(_) => {
// Extract the type of the list elements
@@ -484,7 +484,7 @@ fn apply_builtin(
.app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
)
}
- (ListFold, [_, l, _, cons, nil]) => match &*l.as_whnf() {
+ (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
EmptyListLit(_) => Ret::Value(nil.clone()),
NEListLit(xs) => {
let mut v = nil.clone();
@@ -513,7 +513,7 @@ fn apply_builtin(
),
)
}
- (OptionalFold, [_, v, _, just, nothing]) => match &*v.as_whnf() {
+ (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
_ => Ret::DoneAsIs,
@@ -530,7 +530,7 @@ fn apply_builtin(
),
),
- (NaturalFold, [n, t, succ, zero]) => match &*n.as_whnf() {
+ (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
NaturalLit(0) => Ret::Value(zero.clone()),
NaturalLit(n) => {
let fold = Value::from_builtin(NaturalFold)
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index e69d220..02c8013 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -157,7 +157,7 @@ impl Value {
}
pub(crate) fn as_const(&self) -> Option<Const> {
- match &*self.as_whnf() {
+ match &*self.kind() {
ValueKind::Const(c) => Some(*c),
_ => None,
}
@@ -180,7 +180,7 @@ impl Value {
/// 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<Value>> {
+ pub(crate) fn kind(&self) -> Ref<ValueKind<Value>> {
self.normalize_whnf();
self.as_kind()
}
@@ -194,7 +194,7 @@ impl Value {
self.to_tyexpr_noenv().to_expr(opts)
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
- self.as_whnf().clone()
+ 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<Value> {
@@ -233,7 +233,7 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- let body_t = match &*self.get_type_not_sort().as_whnf() {
+ let body_t = match &*self.get_type_not_sort().kind() {
ValueKind::PiClosure { annot, closure, .. } => {
v.check_type(annot);
closure.apply(v.clone())
@@ -617,7 +617,7 @@ impl Closure {
// 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()
+ *self.kind() == *other.kind()
}
}
impl std::cmp::Eq for Value {}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index d7720c7..f36ec4a 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -10,7 +10,7 @@ use crate::syntax::{
};
pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
- let f_borrow = f.as_whnf();
+ let f_borrow = f.kind();
match &*f_borrow {
ValueKind::LamClosure { closure, .. } => {
closure.apply(a).to_whnf_check_type(ty)
@@ -47,7 +47,7 @@ pub(crate) fn squash_textlit(
match contents {
Text(s) => crnt_str.push_str(&s),
Expr(e) => {
- let e_borrow = e.as_whnf();
+ let e_borrow = e.kind();
match &*e_borrow {
ValueKind::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
@@ -123,8 +123,8 @@ fn apply_binop<'a>(
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
TextLit,
};
- let x_borrow = x.as_whnf();
- let y_borrow = y.as_whnf();
+ let x_borrow = x.kind();
+ let y_borrow = y.kind();
Some(match (o, &*x_borrow, &*y_borrow) {
(BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
(BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
@@ -206,7 +206,7 @@ fn apply_binop<'a>(
Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let ty_borrow = ty.as_whnf();
+ let ty_borrow = ty.kind();
let kts = match &*ty_borrow {
RecordType(kts) => kts,
_ => unreachable!("Internal type error"),
@@ -286,7 +286,7 @@ pub(crate) fn normalize_one_layer(
ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
- let arg = match &*t.as_whnf() {
+ let arg = match &*t.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
@@ -319,13 +319,13 @@ pub(crate) fn normalize_one_layer(
}
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
- let b_borrow = b.as_whnf();
+ let b_borrow = b.kind();
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();
+ let e1_borrow = e1.kind();
+ let e2_borrow = e2.kind();
match (&*e1_borrow, &*e2_borrow) {
// Simplify `if b then True else False`
(BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
@@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer(
Ret::ValueKind(RecordLit(HashMap::new()))
}
ExprKind::Projection(ref v, ref ls) => {
- let v_borrow = v.as_whnf();
+ let v_borrow = v.kind();
match &*v_borrow {
RecordLit(kvs) => Ret::ValueKind(RecordLit(
ls.iter()
@@ -365,7 +365,7 @@ pub(crate) fn normalize_one_layer(
}
}
ExprKind::Field(ref v, ref l) => {
- let v_borrow = v.as_whnf();
+ let v_borrow = v.kind();
match &*v_borrow {
RecordLit(kvs) => match kvs.get(l) {
Some(r) => Ret::Value(r.clone()),
@@ -391,8 +391,8 @@ pub(crate) fn normalize_one_layer(
ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
- let handlers_borrow = handlers.as_whnf();
- let variant_borrow = variant.as_whnf();
+ let handlers_borrow = handlers.kind();
+ let variant_borrow = variant.kind();
match (&*handlers_borrow, &*variant_borrow) {
(RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l)
{
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e1a9c11..0c5e779 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -94,7 +94,7 @@ fn type_one_layer(
}
ExprKind::EmptyListLit(t) => {
let t = t.normalize_nf(env.as_nzenv());
- match &*t.as_whnf() {
+ match &*t.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
@@ -189,7 +189,7 @@ fn type_one_layer(
Value::from_const(k)
}
ExprKind::Field(scrut, x) => {
- match &*scrut.get_type()?.as_whnf() {
+ match &*scrut.get_type()?.kind() {
ValueKind::RecordType(kts) => match kts.get(&x) {
Some(tth) => tth.clone(),
None => return mkerr("MissingRecordField"),
@@ -197,7 +197,7 @@ fn type_one_layer(
// TODO: branch here only when scrut.get_type() is a Const
_ => {
let scrut_nf = scrut.normalize_nf(env.as_nzenv());
- let scrut_nf_borrow = scrut_nf.as_whnf();
+ let scrut_nf_borrow = scrut_nf.kind();
match &*scrut_nf_borrow {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
@@ -244,7 +244,7 @@ fn type_one_layer(
}
ExprKind::Assert(t) => {
let t = t.normalize_whnf(env.as_nzenv());
- match &*t.as_whnf() {
+ match &*t.kind() {
ValueKind::Equivalence(x, y) if x == y => {}
ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
_ => return mkerr("AssertMustTakeEquivalence"),
@@ -253,7 +253,7 @@ fn type_one_layer(
}
ExprKind::App(f, arg) => {
let tf = f.get_type()?;
- let tf_borrow = tf.as_whnf();
+ let tf_borrow = tf.kind();
match &*tf_borrow {
ValueKind::PiClosure { annot, closure, .. } => {
if arg.get_type()? != *annot {
@@ -275,9 +275,7 @@ fn type_one_layer(
}
}
ExprKind::BoolIf(x, y, z) => {
- if *x.get_type()?.as_whnf()
- != ValueKind::from_builtin(Builtin::Bool)
- {
+ if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
return mkerr("InvalidPredicate");
}
if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
@@ -297,14 +295,14 @@ fn type_one_layer(
let y_type = y.get_type()?;
// Extract the LHS record type
- let x_type_borrow = x_type.as_whnf();
+ let x_type_borrow = x_type.kind();
let kts_x = match &*x_type_borrow {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("MustCombineRecord"),
};
// Extract the RHS record type
- let y_type_borrow = y_type.as_whnf();
+ let y_type_borrow = y_type.kind();
let kts_y = match &*y_type_borrow {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("MustCombineRecord"),
@@ -336,8 +334,8 @@ fn type_one_layer(
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
let x_val = x.normalize_whnf(env.as_nzenv());
let y_val = y.normalize_whnf(env.as_nzenv());
- let x_val_borrow = x_val.as_whnf();
- let y_val_borrow = y_val.as_whnf();
+ let x_val_borrow = x_val.kind();
+ let y_val_borrow = y_val.kind();
let kts_x = match &*x_val_borrow {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("RecordTypeMergeRequiresRecordType"),
@@ -366,7 +364,7 @@ fn type_one_layer(
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
let l_ty = l.get_type()?;
- match &*l_ty.as_whnf() {
+ match &*l_ty.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
..
@@ -418,14 +416,14 @@ fn type_one_layer(
}
ExprKind::Merge(record, union, type_annot) => {
let record_type = record.get_type()?;
- let record_borrow = record_type.as_whnf();
+ let record_borrow = record_type.kind();
let handlers = match &*record_borrow {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("Merge1ArgMustBeRecord"),
};
let union_type = union.get_type()?;
- let union_borrow = union_type.as_whnf();
+ let union_borrow = union_type.kind();
let variants = match &*union_borrow {
ValueKind::UnionType(kts) => Cow::Borrowed(kts),
ValueKind::AppliedBuiltin(BuiltinClosure {
@@ -447,7 +445,7 @@ fn type_one_layer(
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 handler_type_borrow = handler_type.kind();
match &*handler_type_borrow {
ValueKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
@@ -498,7 +496,7 @@ fn type_one_layer(
ExprKind::ToMap(_, _) => unimplemented!("toMap"),
ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
- let record_type_borrow = record_type.as_whnf();
+ let record_type_borrow = record_type.kind();
let kts = match &*record_type_borrow {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("ProjectionMustBeRecord"),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 02:24:00 +0000