diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/core/context.rs | 34 | ||||
| -rw-r--r-- | dhall/src/core/value.rs | 68 | ||||
| -rw-r--r-- | dhall/src/core/valuef.rs | 14 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 72 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 33 |
5 files changed, 113 insertions, 108 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 851e4c4..deabe44 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::TypedValue; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::TypeError; @@ -11,7 +11,7 @@ use crate::error::TypeError; #[derive(Debug, Clone)] enum CtxItem { Kept(AlphaVar, TypedValue), - Replaced(Value, TypedValue), + Replaced(TypedValue), } #[derive(Debug, Clone)] @@ -32,10 +32,7 @@ impl TypecheckContext { e: TypedValue, ) -> Result<Self, TypeError> { let mut vec = self.0.as_ref().clone(); - vec.push(( - x.clone(), - CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()), - )); + vec.push((x.clone(), CtxItem::Replaced(e))); Ok(TypecheckContext(Rc::new(vec))) } pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> { @@ -45,13 +42,15 @@ impl TypecheckContext { match var.over_binder(l) { None => { let i = i.under_multiple_binders(&shift_map); - let (th, t) = match i { + return Some(match i { CtxItem::Kept(newvar, t) => { - (ValueF::Var(newvar).into_value(), t) + TypedValue::from_valuef_and_type( + ValueF::Var(newvar), + t, + ) } - CtxItem::Replaced(th, t) => (th, t), - }; - return Some(TypedValue::from_value_and_type(th, t)); + CtxItem::Replaced(v) => v, + }); } Some(newvar) => var = newvar, }; @@ -114,9 +113,7 @@ impl Shift for CtxItem { CtxItem::Kept(v, t) => { CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) } - CtxItem::Replaced(e, t) => { - CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?) - } + CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), }) } } @@ -130,14 +127,9 @@ impl Shift for TypecheckContext { impl Subst<TypedValue> for CtxItem { fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { match self { - CtxItem::Replaced(e, t) => CtxItem::Replaced( - e.subst_shift(var, val), - t.subst_shift(var, val), - ), + CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => { - CtxItem::Replaced(val.to_value(), t.subst_shift(var, val)) - } + None => CtxItem::Replaced(val.clone()), Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), }, } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f4cb6b6..c4e3831 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF}; +use dhall_syntax::Const; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; use crate::phase::typecheck::type_of_const; -use crate::phase::{Normalized, NormalizedSubExpr, Typed}; +use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] enum Form { @@ -28,7 +28,7 @@ enum Form { } use Form::{Unevaled, NF, WHNF}; -#[derive(Debug, Clone)] +#[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 @@ -108,7 +108,7 @@ impl ValueInternal { } impl Value { - pub(crate) fn from_valuef(v: ValueF) -> Value { + pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { ValueInternal { form: Unevaled, value: v, @@ -124,18 +124,8 @@ impl Value { } .into_value() } - pub(crate) fn from_partial_expr(e: ExprF<Value, Normalized>) -> Value { - Value::from_valuef(ValueF::PartialExpr(e)) - } - // TODO: avoid using this function - pub(crate) fn with_type(self, t: TypedValue) -> Value { - let vint = self.as_internal(); - ValueInternal { - form: vint.form, - value: vint.value.clone(), - ty: Some(t), - } - .into_value() + pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { + Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type)) } /// Mutates the contents. If no one else shares this thunk, @@ -214,7 +204,7 @@ impl Value { } pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { - self.app_value(val.into_value()) + self.app_value(val.into_value_untyped()) } pub(crate) fn app_value(&self, th: Value) -> ValueF { @@ -227,41 +217,39 @@ impl Value { } impl TypedValue { - pub(crate) fn from_valuef(v: ValueF) -> TypedValue { - TypedValue::from_value_untyped(Value::from_valuef(v)) - } - - pub(crate) fn normalize_nf(&self) -> ValueF { - self.0.normalize_nf().clone() - } - - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + pub fn from_value(th: Value) -> Self { + TypedValue(th) } - - pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self { - TypedValue(th.with_type(t)) + pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue { + TypedValue::from_value(Value::from_valuef_untyped(v)) } - pub fn from_value_simple_type(th: Value) -> Self { - TypedValue::from_value_and_type(th, TypedValue::const_type()) + pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) } - pub(crate) fn from_value_untyped(th: Value) -> Self { - TypedValue(th) + // TODO: do something with the info that the type is Type. Maybe check + // is a type is present ? + pub(crate) fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value(th) } pub(crate) fn from_const(c: Const) -> Self { match type_of_const(c) { Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)), } } pub fn const_type() -> Self { TypedValue::from_const(Const::Type) } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { - TypedValue(Value::from_valuef_and_type(v, t)) + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.normalize_nf().clone() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index b948eb1..de55d2f 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -48,8 +48,14 @@ pub enum ValueF { } impl ValueF { - pub(crate) fn into_value(self) -> Value { - Value::from_valuef(self) + pub(crate) fn into_value_untyped(self) -> Value { + Value::from_valuef_untyped(self) + } + pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value { + Value::from_valuef_and_type(self, t) + } + pub(crate) fn into_value_simple_type(self) -> Value { + Value::from_valuef_simple_type(self) } /// Convert the value to a fully normalized syntactic expression @@ -258,12 +264,12 @@ impl ValueF { /// Apply to a value pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { - self.app_value(val.into_value()) + self.app_value(val.into_value_untyped()) } /// Apply to a thunk pub fn app_value(self, th: Value) -> ValueF { - Value::from_valuef(self).app_value(th) + Value::from_valuef_untyped(self).app_value(th) } pub fn from_builtin(b: Builtin) -> ValueF { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index dabfe87..27858d8 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -20,7 +20,7 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - ValueF::Var(var).into_value() + ValueF::Var(var).into_value_untyped() }}; // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { @@ -30,30 +30,40 @@ macro_rules! make_closure { make_closure!($($ty)*), ), make_closure!($($rest)*), - ).into_value() + ).into_value_untyped() + }; + (Natural) => { + ValueF::from_builtin(Builtin::Natural) + .into_value_simple_type() }; - (Natural) => { ValueF::from_builtin(Builtin::Natural).into_value() }; (List $($rest:tt)*) => { ValueF::from_builtin(Builtin::List) .app_value(make_closure!($($rest)*)) - .into_value() + .into_value_simple_type() }; - (Some $($rest:tt)*) => { - ValueF::NEOptionalLit(make_closure!($($rest)*)).into_value() + (Some($($rest:tt)*)) => { + ValueF::NEOptionalLit(make_closure!($($rest)*)) + .into_value_untyped() }; (1 + $($rest:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Value::from_valuef(ValueF::NaturalLit(1)), - )).into_value() + Value::from_valuef_and_type( + ValueF::NaturalLit(1), + TypedValue::from_value(make_closure!(Natural)) + ), + )).into_value_with_type( + TypedValue::from_value(make_closure!(Natural)) + ) }; ([ $($head:tt)* ] # $($tail:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![make_closure!($($head)*)]).into_value(), + ValueF::NEListLit(vec![make_closure!($($head)*)]) + .into_value_untyped(), make_closure!($($tail)*), - )).into_value() + )).into_value_untyped() }; } @@ -189,10 +199,17 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedValue::from_valuef(ValueF::from_builtin(Natural)), + TypedValue::from_valuef_untyped(ValueF::from_builtin( + Natural, + )), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypedValue::from_valuef(RecordType(kts))))) + Ok(( + r, + EmptyListLit(TypedValue::from_valuef_untyped(RecordType( + kts, + ))), + )) } NEListLit(xs) => { let xs = xs @@ -201,9 +218,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .map(|(i, e)| { let i = NaturalLit(i); let mut kvs = HashMap::new(); - kvs.insert("index".into(), Value::from_valuef(i)); + kvs.insert( + "index".into(), + Value::from_valuef_untyped(i), + ); kvs.insert("value".into(), e.clone()); - Value::from_valuef(RecordLit(kvs)) + Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); Ok((r, NEListLit(xs))) @@ -246,7 +266,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .clone() .app_value(x.clone()) .app_value(v) - .into_value(); + .into_value_untyped(); } Ok((r, v.to_whnf())) } @@ -267,7 +287,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { f.app_valuef( ValueF::from_builtin(Optional).app_value(t.clone()), ) - .app_value(make_closure!(λ(x: #t) -> Some var(x, 0))) + .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) .app_valuef(EmptyOptionalLit( TypedValue::from_value_simple_type(t.clone()), )), @@ -327,7 +347,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { let f_borrow = f.as_whnf(); match &*f_borrow { ValueF::Lam(x, _, e) => { - let val = TypedValue::from_value_untyped(a); + let val = TypedValue::from_value(a); e.subst_shift(&x.into(), &val).to_whnf() } ValueF::AppliedBuiltin(b, args) => { @@ -602,11 +622,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Value::from_partial_expr(ExprF::BinOp( + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )) + ))) }); Ret::ValueF(RecordLit(kvs)) } @@ -619,7 +639,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypedValue::from_value_untyped(Value::from_partial_expr( + TypedValue::from_valuef_untyped(ValueF::PartialExpr( ExprF::BinOp( RecursiveRecordTypeMerge, v1.to_value(), @@ -655,15 +675,15 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::Annot(x, _) => Ret::Value(x), ExprF::Assert(_) => Ret::Expr(expr), ExprF::Lam(x, t, e) => { - Ret::ValueF(Lam(x.into(), TypedValue::from_value_untyped(t), e)) + Ret::ValueF(Lam(x.into(), TypedValue::from_value(t), e)) } ExprF::Pi(x, t, e) => Ret::ValueF(Pi( x.into(), - TypedValue::from_value_untyped(t), - TypedValue::from_value_untyped(e), + TypedValue::from_value(t), + TypedValue::from_value(e), )), ExprF::Let(x, _, v, b) => { - let v = TypedValue::from_value_untyped(v); + let v = TypedValue::from_value(v); Ret::Value(b.subst_shift(&x.into(), &v)) } ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), @@ -697,12 +717,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } ExprF::RecordType(kts) => Ret::ValueF(RecordType( kts.into_iter() - .map(|(k, t)| (k, TypedValue::from_value_untyped(t))) + .map(|(k, t)| (k, TypedValue::from_value(t))) .collect(), )), ExprF::UnionType(kts) => Ret::ValueF(UnionType( kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedValue::from_value_untyped(t)))) + .map(|(k, t)| (k, t.map(|t| TypedValue::from_value(t)))) .collect(), )), ExprF::TextLit(elts) => { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 07c4ad8..e24f5a3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::TypedValue; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -37,8 +37,8 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(TypedValue::from_value_and_type( - ValueF::Pi(x.into(), tx, te).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::Pi(x.into(), tx, te), TypedValue::from_const(k), )) } @@ -70,8 +70,8 @@ fn tck_record_type( // An empty record type has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::RecordType(new_kts), TypedValue::from_const(k), )) } @@ -115,8 +115,8 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_value_and_type( - ValueF::UnionType(new_kts).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::UnionType(new_kts), TypedValue::from_const(k), )) } @@ -281,6 +281,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { } } +// TODO: this can't fail in practise pub(crate) fn builtin_to_type(b: Builtin) -> Result<TypedValue, TypeError> { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } @@ -351,8 +352,8 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - TypedValue::from_value_and_type( - Value::from_partial_expr(expr), + TypedValue::from_valuef_and_type( + ValueF::PartialExpr(expr), typ, ) } @@ -465,10 +466,9 @@ fn type_last_layer( )); } - Ok(RetTypeOnly(TypedValue::from_value_and_type( + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.to_value()) - .into_value(), + .app_value(t.to_value()), TypedValue::from_const(Type), ))) } @@ -478,10 +478,9 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly(TypedValue::from_value_and_type( + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t.to_value()) - .into_value(), + .app_value(t.to_value()), TypedValue::from_const(Type), ))) } @@ -942,8 +941,8 @@ fn type_last_layer( }; } - Ok(RetTypeOnly(TypedValue::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), ))) } |