summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/mod.rs14
-rw-r--r--dhall/src/semantics/phase/normalize.rs216
-rw-r--r--dhall/src/semantics/phase/typecheck.rs72
3 files changed, 151 insertions, 151 deletions
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 752c257..f27088c 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -2,7 +2,7 @@ use std::fmt::Display;
use std::path::Path;
use crate::semantics::core::value::{ToExprOptions, Value};
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value_kind::ValueKind;
use crate::semantics::core::var::{AlphaVar, Shift, Subst};
use crate::semantics::error::{EncodeError, Error, ImportError, TypeError};
use crate::syntax::binary;
@@ -91,8 +91,8 @@ impl Typed {
pub(crate) fn from_const(c: Const) -> Self {
Typed(Value::from_const(c))
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
- Typed(Value::from_valuef_and_type(v, t.into_value()))
+ 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)
@@ -148,8 +148,8 @@ impl Typed {
pub fn make_record_type(
kts: impl Iterator<Item = (String, Typed)>,
) -> Self {
- Typed::from_valuef_and_type(
- ValueF::RecordType(
+ Typed::from_kind_and_type(
+ ValueKind::RecordType(
kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
),
Typed::const_type(),
@@ -158,8 +158,8 @@ impl Typed {
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Typed>)>,
) -> Self {
- Typed::from_valuef_and_type(
- ValueF::UnionType(
+ Typed::from_kind_and_type(
+ ValueKind::UnionType(
kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
.collect(),
),
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 81c3ce1..157d1f3 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value_kind::ValueKind;
use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::semantics::phase::Normalized;
use crate::syntax;
@@ -19,7 +19,7 @@ macro_rules! make_closure {
Label::from(stringify!($var)).into(),
$n
);
- ValueF::Var(var)
+ ValueKind::Var(var)
.into_value_with_type(make_closure!($($ty)*))
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
@@ -28,9 +28,9 @@ macro_rules! make_closure {
let ty = make_closure!($($ty)*);
let body = make_closure!($($body)*);
let body_ty = body.get_type_not_sort();
- let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+ let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty)
.into_value_with_type(Value::from_const(Type));
- ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+ ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty)
}};
(Natural) => {
Value::from_builtin(Builtin::Natural)
@@ -43,14 +43,14 @@ macro_rules! make_closure {
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);
- ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+ ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type)
}};
(1 + $($rest:tt)*) => {
- ValueF::PartialExpr(ExprF::BinOp(
+ ValueKind::PartialExpr(ExprF::BinOp(
syntax::BinOp::NaturalPlus,
make_closure!($($rest)*),
- Value::from_valuef_and_type(
- ValueF::NaturalLit(1),
+ Value::from_kind_and_type(
+ ValueKind::NaturalLit(1),
make_closure!(Natural)
),
)).into_value_with_type(
@@ -61,9 +61,9 @@ macro_rules! make_closure {
let head = make_closure!($($head)*);
let tail = make_closure!($($tail)*);
let list_type = tail.get_type_not_sort();
- ValueF::PartialExpr(ExprF::BinOp(
+ ValueKind::PartialExpr(ExprF::BinOp(
syntax::BinOp::ListAppend,
- ValueF::NEListLit(vec![head])
+ ValueKind::NEListLit(vec![head])
.into_value_with_type(list_type.clone()),
tail,
)).into_value_with_type(list_type)
@@ -75,13 +75,13 @@ pub(crate) fn apply_builtin(
b: Builtin,
args: Vec<Value>,
ty: &Value,
-) -> ValueF {
+) -> ValueKind {
use syntax::Builtin::*;
- use ValueF::*;
+ use ValueKind::*;
// Small helper enum
enum Ret<'a> {
- ValueF(ValueF),
+ 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.
@@ -90,38 +90,38 @@ pub(crate) fn apply_builtin(
}
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
(NaturalIsZero, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
_ => Ret::DoneAsIs,
},
(NaturalEven, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
_ => Ret::DoneAsIs,
},
(NaturalOdd, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
_ => Ret::DoneAsIs,
},
(NaturalToInteger, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
_ => Ret::DoneAsIs,
},
- (NaturalShow, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => {
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
- n.to_string(),
- )]))
+ (NaturalShow, [n]) => {
+ match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueKind(TextLit(vec![
+ InterpolatedTextContents::Text(n.to_string()),
+ ])),
+ _ => Ret::DoneAsIs,
}
- _ => Ret::DoneAsIs,
- },
+ }
(NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
(NaturalLit(a), NaturalLit(b)) => {
- Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
+ Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
}
(NaturalLit(0), _) => Ret::Value(b.clone()),
- (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
- _ if a == b => Ret::ValueF(NaturalLit(0)),
+ (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+ _ if a == b => Ret::ValueKind(NaturalLit(0)),
_ => Ret::DoneAsIs,
},
(IntegerShow, [n]) => match &*n.as_whnf() {
@@ -131,24 +131,24 @@ pub(crate) fn apply_builtin(
} else {
format!("+{}", n)
};
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
+ Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)]))
}
_ => Ret::DoneAsIs,
},
(IntegerToDouble, [n]) => match &*n.as_whnf() {
IntegerLit(n) => {
- Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+ Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
}
_ => Ret::DoneAsIs,
},
- (DoubleShow, [n]) => match &*n.as_whnf() {
- DoubleLit(n) => {
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
- n.to_string(),
- )]))
+ (DoubleShow, [n]) => {
+ match &*n.as_whnf() {
+ DoubleLit(n) => Ret::ValueKind(TextLit(vec![
+ InterpolatedTextContents::Text(n.to_string()),
+ ])),
+ _ => Ret::DoneAsIs,
}
- _ => Ret::DoneAsIs,
- },
+ }
(TextShow, [v]) => match &*v.as_whnf() {
TextLit(elts) => {
match elts.as_slice() {
@@ -158,7 +158,7 @@ pub(crate) fn apply_builtin(
let txt: InterpolatedText<Normalized> =
std::iter::empty().collect();
let s = txt.to_string();
- Ret::ValueF(TextLit(vec![
+ Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(s),
]))
}
@@ -172,7 +172,7 @@ pub(crate) fn apply_builtin(
))
.collect();
let s = txt.to_string();
- Ret::ValueF(TextLit(vec![
+ Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(s),
]))
}
@@ -182,28 +182,28 @@ pub(crate) fn apply_builtin(
_ => Ret::DoneAsIs,
},
(ListLength, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
- NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
_ => Ret::DoneAsIs,
},
(ListHead, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
+ Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
_ => Ret::DoneAsIs,
},
(ListLast, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
- NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+ 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::ValueF(EmptyListLit(n.clone())),
+ EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+ Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
}
_ => Ret::DoneAsIs,
},
@@ -222,7 +222,7 @@ pub(crate) fn apply_builtin(
let mut kts = HashMap::new();
kts.insert("index".into(), Value::from_builtin(Natural));
kts.insert("value".into(), t.clone());
- let t = Value::from_valuef_and_type(
+ let t = Value::from_kind_and_type(
RecordType(kts),
Value::from_const(Type),
);
@@ -237,7 +237,7 @@ pub(crate) fn apply_builtin(
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_valuef_and_type(
+ Value::from_kind_and_type(
NaturalLit(i),
Value::from_builtin(
Builtin::Natural,
@@ -245,7 +245,7 @@ pub(crate) fn apply_builtin(
),
);
kvs.insert("value".into(), e.clone());
- Value::from_valuef_and_type(
+ Value::from_kind_and_type(
RecordLit(kvs),
t.clone(),
)
@@ -254,14 +254,14 @@ pub(crate) fn apply_builtin(
),
_ => unreachable!(),
};
- Ret::ValueF(list)
+ Ret::ValueKind(list)
}
_ => Ret::DoneAsIs,
}
}
(ListBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(ListFold, args) => {
+ ValueKind::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
Ret::Value(args[1].clone())
} else {
@@ -303,7 +303,7 @@ pub(crate) fn apply_builtin(
},
(OptionalBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(OptionalFold, args) => {
+ ValueKind::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
Ret::Value(args[1].clone())
} else {
@@ -338,7 +338,7 @@ pub(crate) fn apply_builtin(
},
(NaturalBuild, [f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(NaturalFold, args) => {
+ ValueKind::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
Ret::Value(args[0].clone())
} else {
@@ -375,7 +375,7 @@ pub(crate) fn apply_builtin(
_ => Ret::DoneAsIs,
};
match ret {
- Ret::ValueF(v) => v,
+ 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();
@@ -388,23 +388,23 @@ pub(crate) fn apply_builtin(
}
}
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => {
+ ValueKind::Lam(x, _, e) => {
e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
}
- ValueF::AppliedBuiltin(b, args) => {
+ ValueKind::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args, ty)
}
- ValueF::UnionConstructor(l, kts) => {
- ValueF::UnionLit(l.clone(), a, kts.clone())
+ ValueKind::UnionConstructor(l, kts) => {
+ ValueKind::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
- ValueF::PartialExpr(ExprF::App(f, a))
+ ValueKind::PartialExpr(ExprF::App(f, a))
}
}
}
@@ -426,7 +426,7 @@ pub(crate) fn squash_textlit(
Expr(e) => {
let e_borrow = e.as_whnf();
match &*e_borrow {
- ValueF::TextLit(elts2) => {
+ ValueKind::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
}
_ => {
@@ -479,7 +479,7 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueF(ValueF),
+ ValueKind(ValueKind),
Value(Value),
ValueRef(&'a Value),
Expr(ExprF<Value, Normalized>),
@@ -496,7 +496,7 @@ fn apply_binop<'a>(
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use ValueF::{
+ use ValueKind::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
TextLit,
};
@@ -505,58 +505,58 @@ fn apply_binop<'a>(
Some(match (o, &*x_borrow, &*y_borrow) {
(BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
(BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
+ (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::ValueF(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
+ (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::ValueF(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
+ (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::ValueF(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
+ (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::ValueF(NaturalLit(x + y))
+ Ret::ValueKind(NaturalLit(x + y))
}
- (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ (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::ValueF(NaturalLit(x * y))
+ Ret::ValueKind(NaturalLit(x * y))
}
(ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
(ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
- xs.iter().chain(ys.iter()).cloned().collect(),
- )),
+ (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::ValueF(TextLit(
+ (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::ValueF(TextLit(squash_textlit(
+ 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::ValueF(TextLit(squash_textlit(
+ Ret::ValueKind(TextLit(squash_textlit(
once(x).chain(y.iter().cloned()),
)))
}
@@ -573,7 +573,7 @@ fn apply_binop<'a>(
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- Ret::ValueF(RecordLit(kvs))
+ Ret::ValueKind(RecordLit(kvs))
}
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
@@ -589,8 +589,8 @@ fn apply_binop<'a>(
_ => unreachable!("Internal type error"),
};
let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
- Ok(Value::from_valuef_and_type(
- ValueF::PartialExpr(ExprF::BinOp(
+ Ok(Value::from_kind_and_type(
+ ValueKind::PartialExpr(ExprF::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
@@ -598,7 +598,7 @@ fn apply_binop<'a>(
kts.get(k).expect("Internal type error").clone(),
))
})?;
- Ret::ValueF(RecordLit(kvs))
+ Ret::ValueKind(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
@@ -612,8 +612,8 @@ fn apply_binop<'a>(
pub(crate) fn normalize_one_layer(
expr: ExprF<Value, Normalized>,
ty: &Value,
-) -> ValueF {
- use ValueF::{
+) -> ValueKind {
+ use ValueKind::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
UnionConstructor, UnionLit, UnionType,
@@ -639,17 +639,17 @@ pub(crate) fn normalize_one_layer(
}
ExprF::Assert(_) => Ret::Expr(expr),
ExprF::App(v, a) => Ret::Value(v.app(a)),
- ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
- ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
- ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
- ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
- ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
+ ExprF::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
+ ExprF::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
+ ExprF::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
+ ExprF::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+ ExprF::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
ExprF::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::ValueF(EmptyListLit(args[0].clone()))
+ Ret::ValueKind(EmptyListLit(args[0].clone()))
}
_ => {
drop(t_borrow);
@@ -658,10 +658,10 @@ pub(crate) fn normalize_one_layer(
}
}
ExprF::NEListLit(elts) => {
- Ret::ValueF(NEListLit(elts.into_iter().collect()))
+ Ret::ValueKind(NEListLit(elts.into_iter().collect()))
}
ExprF::RecordLit(kvs) => {
- Ret::ValueF(RecordLit(kvs.into_iter().collect()))
+ Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
}
ExprF::TextLit(elts) => {
use InterpolatedTextContents::Expr;
@@ -670,7 +670,7 @@ pub(crate) fn normalize_one_layer(
if let [Expr(th)] = elts.as_slice() {
Ret::Value(th.clone())
} else {
- Ret::ValueF(TextLit(elts))
+ Ret::ValueKind(TextLit(elts))
}
}
ExprF::BoolIf(ref b, ref e1, ref e2) => {
@@ -701,12 +701,12 @@ pub(crate) fn normalize_one_layer(
},
ExprF::Projection(_, ref ls) if ls.is_empty() => {
- Ret::ValueF(RecordLit(HashMap::new()))
+ Ret::ValueKind(RecordLit(HashMap::new()))
}
ExprF::Projection(ref v, ref ls) => {
let v_borrow = v.as_whnf();
match &*v_borrow {
- RecordLit(kvs) => Ret::ValueF(RecordLit(
+ RecordLit(kvs) => Ret::ValueKind(RecordLit(
ls.iter()
.filter_map(|l| {
kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -730,7 +730,7 @@ pub(crate) fn normalize_one_layer(
}
},
UnionType(kts) => {
- Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
+ Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
}
_ => {
drop(v_borrow);
@@ -773,20 +773,20 @@ pub(crate) fn normalize_one_layer(
};
match ret {
- Ret::ValueF(v) => v,
+ 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) => ValueF::PartialExpr(expr),
+ Ret::Expr(expr) => ValueKind::PartialExpr(expr),
}
}
-/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
+/// Normalize a ValueKind into WHNF
+pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
match v {
- ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
- ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
- ValueF::TextLit(elts) => {
- ValueF::TextLit(squash_textlit(elts.into_iter()))
+ 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
index 59380a3..96a0b4b 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
use crate::semantics::core::context::TypecheckContext;
use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value_kind::ValueKind;
use crate::semantics::core::var::{Shift, Subst};
use crate::semantics::error::{TypeError, TypeMessage};
use crate::semantics::phase::normalize::merge_maps;
@@ -39,8 +39,8 @@ fn tck_pi_type(
let k = function_check(ka, kb);
- Ok(Value::from_valuef_and_type(
- ValueF::Pi(x.into(), tx, te),
+ Ok(Value::from_kind_and_type(
+ ValueKind::Pi(x.into(), tx, te),
Value::from_const(k),
))
}
@@ -71,8 +71,8 @@ fn tck_record_type(
};
}
- Ok(Value::from_valuef_and_type(
- ValueF::RecordType(new_kts),
+ Ok(Value::from_kind_and_type(
+ ValueKind::RecordType(new_kts),
Value::from_const(k),
))
}
@@ -116,8 +116,8 @@ where
// an union type with only unary variants also has type Type
let k = k.unwrap_or(Const::Type);
- Ok(Value::from_valuef_and_type(
- ValueF::UnionType(new_kts),
+ Ok(Value::from_kind_and_type(
+ ValueKind::UnionType(new_kts),
Value::from_const(k),
))
}
@@ -131,13 +131,13 @@ fn function_check(a: Const, b: Const) -> Const {
}
pub(crate) fn const_to_value(c: Const) -> Value {
- let v = ValueF::Const(c);
+ let v = ValueKind::Const(c);
match c {
Const::Type => {
- Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ Value::from_kind_and_type(v, const_to_value(Const::Kind))
}
Const::Kind => {
- Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ Value::from_kind_and_type(v, const_to_value(Const::Sort))
}
Const::Sort => Value::const_sort(),
}
@@ -290,8 +290,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
- Value::from_valuef_and_type(
- ValueF::from_builtin(b),
+ Value::from_kind_and_type(
+ ValueKind::from_builtin(b),
type_with(&ctx, type_of_builtin(b)).unwrap(),
)
}
@@ -313,8 +313,8 @@ fn type_with(
let ctx2 = ctx.insert_type(var, annot.clone());
let body = type_with(&ctx2, body.clone())?;
let body_type = body.get_type()?;
- Value::from_valuef_and_type(
- ValueF::Lam(var.clone().into(), annot.clone(), body),
+ Value::from_kind_and_type(
+ ValueKind::Lam(var.clone().into(), annot.clone(), body),
tck_pi_type(ctx, var.clone(), annot, body_type)?,
)
}
@@ -389,7 +389,7 @@ fn type_last_layer(
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
let (x, tx, tb) = match &*tf_borrow {
- ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ ValueKind::Pi(x, tx, tb) => (x, tx, tb),
_ => return mkerr(NotAFunction(f.clone())),
};
if &a.get_type()? != tx {
@@ -406,8 +406,8 @@ fn type_last_layer(
}
Assert(t) => {
match &*t.as_whnf() {
- ValueF::Equivalence(x, y) if x == y => {}
- ValueF::Equivalence(x, y) => {
+ ValueKind::Equivalence(x, y) if x == y => {}
+ ValueKind::Equivalence(x, y) => {
return mkerr(AssertMismatch(x.clone(), y.clone()))
}
_ => return mkerr(AssertMustTakeEquivalence),
@@ -415,7 +415,7 @@ fn type_last_layer(
RetTypeOnly(t.clone())
}
BoolIf(x, y, z) => {
- if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) {
+ if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
return mkerr(InvalidPredicate(x.clone()));
}
@@ -435,7 +435,7 @@ fn type_last_layer(
}
EmptyListLit(t) => {
match &*t.as_whnf() {
- ValueF::AppliedBuiltin(syntax::Builtin::List, args)
+ ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
if args.len() == 1 => {}
_ => return mkerr(InvalidListType(t.clone())),
}
@@ -482,7 +482,7 @@ fn type_last_layer(
)?),
Field(r, x) => {
match &*r.get_type()?.as_whnf() {
- ValueF::RecordType(kts) => match kts.get(&x) {
+ ValueKind::RecordType(kts) => match kts.get(&x) {
Some(tth) => {
RetTypeOnly(tth.clone())
},
@@ -492,7 +492,7 @@ fn type_last_layer(
// TODO: branch here only when r.get_type() is a Const
_ => {
match &*r.as_whnf() {
- ValueF::UnionType(kts) => match kts.get(&x) {
+ ValueKind::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
RetTypeOnly(
@@ -553,14 +553,14 @@ fn type_last_layer(
// Extract the LHS record type
let l_type_borrow = l_type.as_whnf();
let kts_x = match &*l_type_borrow {
- ValueF::RecordType(kts) => kts,
+ 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 {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(MustCombineRecord(r.clone())),
};
@@ -589,7 +589,7 @@ fn type_last_layer(
// Extract the LHS record type
let borrow_l = l.as_whnf();
let kts_x = match &*borrow_l {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => {
return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
}
@@ -598,7 +598,7 @@ fn type_last_layer(
// Extract the RHS record type
let borrow_r = r.as_whnf();
let kts_y = match &*borrow_r {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => {
return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
}
@@ -626,7 +626,7 @@ fn type_last_layer(
}
BinOp(o @ ListAppend, l, r) => {
match &*l.get_type()?.as_whnf() {
- ValueF::AppliedBuiltin(List, _) => {}
+ ValueKind::AppliedBuiltin(List, _) => {}
_ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
}
@@ -648,8 +648,8 @@ fn type_last_layer(
return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- RetWhole(Value::from_valuef_and_type(
- ValueF::Equivalence(l.clone(), r.clone()),
+ RetWhole(Value::from_kind_and_type(
+ ValueKind::Equivalence(l.clone(), r.clone()),
Value::from_const(Type),
))
}
@@ -684,14 +684,14 @@ fn type_last_layer(
let record_type = record.get_type()?;
let record_borrow = record_type.as_whnf();
let handlers = match &*record_borrow {
- ValueF::RecordType(kts) => kts,
+ 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 {
- ValueF::UnionType(kts) => kts,
+ ValueKind::UnionType(kts) => kts,
_ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
};
@@ -703,7 +703,7 @@ fn type_last_layer(
Some(Some(variant_type)) => {
let handler_type_borrow = handler_type.as_whnf();
let (x, tx, tb) = match &*handler_type_borrow {
- ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ ValueKind::Pi(x, tx, tb) => (x, tx, tb),
_ => {
return mkerr(NotAFunction(
handler_type.clone(),
@@ -765,7 +765,7 @@ fn type_last_layer(
let record_type = record.get_type()?;
let record_type_borrow = record_type.as_whnf();
let kts = match &*record_type_borrow {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(ProjectionMustBeRecord),
};
@@ -777,8 +777,8 @@ fn type_last_layer(
};
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::RecordType(new_kts),
+ RetTypeOnly(Value::from_kind_and_type(
+ ValueKind::RecordType(new_kts),
record_type.get_type()?,
))
}
@@ -786,8 +786,8 @@ fn type_last_layer(
};
Ok(match ret {
- RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
- ValueF::PartialExpr(e),
+ RetTypeOnly(typ) => Value::from_kind_and_type_and_span(
+ ValueKind::PartialExpr(e),
typ,
span,
),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 17:33:27 +0000