summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs66
-rw-r--r--dhall/src/core/valuef.rs3
-rw-r--r--dhall/src/error/mod.rs1
-rw-r--r--dhall/src/phase/normalize.rs25
-rw-r--r--dhall/src/phase/typecheck.rs21
5 files changed, 53 insertions, 63 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 7f98826..4a78b05 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -27,13 +27,14 @@ pub(crate) enum Form {
}
use Form::{Unevaled, NF, WHNF};
-#[derive(Debug)]
/// Partially normalized value.
/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
/// Invariant: if `form` is `NF`, `value` must be fully normalized
+#[derive(Debug)]
struct ValueInternal {
form: Form,
value: ValueF,
+ /// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
}
@@ -69,11 +70,15 @@ impl ValueInternal {
value: ValueF::Const(Const::Type),
ty: None,
},
- |vint| match &vint.form {
- Unevaled => {
+ |vint| match (&vint.form, &vint.ty) {
+ (Unevaled, None) => ValueInternal {
+ form: NF,
+ value: ValueF::Const(Const::Sort),
+ ty: None,
+ },
+ (Unevaled, Some(ty)) => {
let new_value =
- normalize_whnf(vint.value, vint.ty.as_ref())
- .into_whnf(vint.ty.as_ref());
+ normalize_whnf(vint.value, &ty).into_whnf(&ty);
ValueInternal {
form: WHNF,
value: new_value,
@@ -81,7 +86,7 @@ impl ValueInternal {
}
}
// Already in WHNF
- WHNF | NF => vint,
+ (WHNF, _) | (NF, _) => vint,
},
)
}
@@ -103,10 +108,9 @@ impl ValueInternal {
fn get_type(&self) -> Result<&Value, TypeError> {
match &self.ty {
Some(t) => Ok(t),
- None => Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- )),
+ None => {
+ Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+ }
}
}
}
@@ -115,9 +119,13 @@ impl Value {
pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
ValueInternal { form, value, ty }.into_value()
}
+ // TODO: this is very wrong
pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
Value::new(v, Unevaled, None)
}
+ pub(crate) fn const_sort() -> Value {
+ Value::new(ValueF::Const(Const::Sort), NF, None)
+ }
pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
Value::new(v, Unevaled, Some(t))
}
@@ -225,27 +233,30 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- let ty = self.get_type().ok();
- let vovf = apply_any(self.clone(), v.clone(), ty.as_ref());
- match self.as_internal().get_type() {
- Err(_) => vovf.into_value_untyped(),
- Ok(t) => match &*t.as_whnf() {
- ValueF::Pi(x, _, e) => {
- let t = e.subst_shift(&x.into(), &v);
- vovf.into_value_with_type(t)
- }
- _ => unreachable!("Internal type error"),
- },
+ let t = self.get_type_not_sort();
+ let vovf = apply_any(self.clone(), v.clone(), &t);
+ let t_borrow = t.as_whnf();
+ match &*t_borrow {
+ ValueF::Pi(x, _, e) => {
+ let t = e.subst_shift(&x.into(), &v);
+ vovf.into_value_with_type(t)
+ }
+ _ => unreachable!("Internal type error"),
}
}
pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
Ok(self.as_internal().get_type()?.clone())
}
+ /// When we know the value isn't `Sort`, this gets the type directly
+ pub(crate) fn get_type_not_sort(&self) -> Value {
+ self.get_type()
+ .expect("Internal type error: value is `Sort` but shouldn't be")
+ }
}
impl VoVF {
- pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF {
+ pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
match self {
VoVF::ValueF {
val,
@@ -256,7 +267,7 @@ impl VoVF {
VoVF::Value(v) => {
let v_ty = v.get_type().ok();
debug_assert_eq!(
- ty,
+ Some(ty),
v_ty.as_ref(),
"The type recovered from normalization doesn't match the stored type."
);
@@ -264,12 +275,6 @@ impl VoVF {
}
}
}
- pub(crate) fn into_value_untyped(self) -> Value {
- match self {
- VoVF::Value(v) => v,
- VoVF::ValueF { val, form } => Value::new(val, form, None),
- }
- }
pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
match self {
VoVF::Value(v) => {
@@ -288,7 +293,8 @@ impl VoVF {
pub(crate) fn app(self, x: Value) -> VoVF {
VoVF::Value(match self {
VoVF::Value(v) => v.app(x),
- VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
+ // TODO: this is very wrong
+ VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x),
})
}
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 42606a9..5638078 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -47,9 +47,6 @@ pub(crate) enum ValueF {
}
impl ValueF {
- pub(crate) fn into_value_untyped(self) -> Value {
- Value::from_valuef_untyped(self)
- }
pub(crate) fn into_value_with_type(self, t: Value) -> Value {
Value::from_valuef_and_type(self, t)
}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13a9d7e..2ddaf3d 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -54,7 +54,6 @@ pub(crate) enum TypeMessage {
NotAFunction(Value),
TypeMismatch(Value, Value, Value),
AnnotMismatch(Value, Value),
- Untyped,
InvalidListElement(usize, Value, Value),
InvalidListType(Value),
InvalidOptionalType(Value),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fe99696..9837a8b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -46,7 +46,7 @@ macro_rules! make_closure {
let var: AlphaLabel = Label::from(stringify!($var)).into();
let ty = make_closure!($($ty)*);
let body = make_closure!($($body)*);
- let body_ty = body.get_type().expect("Internal type error");
+ let body_ty = body.get_type_not_sort();
let lam_ty = ValueF::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)
@@ -60,7 +60,7 @@ macro_rules! make_closure {
};
(Some($($rest:tt)*)) => {{
let v = make_closure!($($rest)*);
- let v_type = v.get_type().expect("Internal type error");
+ 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)
}};
@@ -79,7 +79,7 @@ macro_rules! make_closure {
([ $($head:tt)* ] # $($tail:tt)*) => {{
let head = make_closure!($($head)*);
let tail = make_closure!($($tail)*);
- let list_type = tail.get_type().expect("Internal type error");
+ let list_type = tail.get_type_not_sort();
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::ListAppend,
ValueF::NEListLit(vec![head])
@@ -90,11 +90,7 @@ macro_rules! make_closure {
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(
- b: Builtin,
- args: Vec<Value>,
- _ty: Option<&Value>,
-) -> VoVF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
use dhall_syntax::Builtin::*;
use ValueF::*;
@@ -251,9 +247,7 @@ pub(crate) fn apply_builtin(
// Extract the type of the list elements
let t = match &*l_whnf {
EmptyListLit(t) => t.clone(),
- NEListLit(xs) => {
- xs[0].get_type().expect("Internal type error")
- }
+ NEListLit(xs) => xs[0].get_type_not_sort(),
_ => unreachable!(),
};
@@ -429,7 +423,7 @@ pub(crate) fn apply_builtin(
}
}
-pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
let fallback = |f: Value, a: Value| {
ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
};
@@ -524,7 +518,7 @@ fn apply_binop<'a>(
o: BinOp,
x: &'a Value,
y: &'a Value,
- ty: Option<&Value>,
+ ty: &Value,
) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -618,7 +612,6 @@ fn apply_binop<'a>(
Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let ty = ty.expect("Internal type error");
let ty_borrow = ty.as_whnf();
let kts = match &*ty_borrow {
RecordType(kts) => kts,
@@ -647,7 +640,7 @@ fn apply_binop<'a>(
pub(crate) fn normalize_one_layer(
expr: ExprF<Value, Normalized>,
- ty: Option<&Value>,
+ ty: &Value,
) -> VoVF {
use ValueF::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
@@ -808,7 +801,7 @@ pub(crate) fn normalize_one_layer(
}
/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
match v {
ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 270191a..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
- match c {
- Const::Type => Ok(const_to_value(Const::Kind)),
- Const::Kind => Ok(const_to_value(Const::Sort)),
- Const::Sort => {
- Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
- }
- }
-}
-
pub(crate) fn const_to_value(c: Const) -> Value {
let v = ValueF::Const(c);
- match type_of_const(c) {
- Ok(t) => Value::from_valuef_and_type(v, t),
- Err(_) => Value::from_valuef_untyped(v),
+ match c {
+ Const::Type => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ }
+ Const::Kind => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ }
+ Const::Sort => Value::const_sort(),
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:16:37 +0000