From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 17:07:59 +0200 Subject: Enforce type information almost everywhere --- dhall/src/core/value.rs | 66 ++++++++++++++++++++++++-------------------- dhall/src/core/valuef.rs | 3 -- dhall/src/error/mod.rs | 1 - dhall/src/phase/normalize.rs | 25 ++++++----------- dhall/src/phase/typecheck.rs | 21 ++++++-------- 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, } @@ -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 { 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 { 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, - _ty: Option<&Value>, -) -> VoVF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec, _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> { 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, - 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 { - 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(), } } -- cgit v1.2.3