diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/context.rs | 31 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 192 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 26 | ||||
-rw-r--r-- | dhall/src/error/mod.rs | 54 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 16 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 90 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 177 | ||||
-rw-r--r-- | serde_dhall/src/lib.rs | 31 |
8 files changed, 245 insertions, 372 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index deabe44..2bf39c5 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,15 +3,15 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::value::TypedValue; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::TypeError; #[derive(Debug, Clone)] enum CtxItem { - Kept(AlphaVar, TypedValue), - Replaced(TypedValue), + Kept(AlphaVar, Value), + Replaced(Value), } #[derive(Debug, Clone)] @@ -21,21 +21,17 @@ impl TypecheckContext { pub fn new() -> Self { TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_type(&self, x: &Label, t: TypedValue) -> Self { + pub fn insert_type(&self, x: &Label, t: Value) -> Self { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); TypecheckContext(Rc::new(vec)) } - pub fn insert_value( - &self, - x: &Label, - e: TypedValue, - ) -> Result<Self, TypeError> { + pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Replaced(e))); Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> { + pub fn lookup(&self, var: &V<Label>) -> Option<Value> { let mut var = var.clone(); let mut shift_map: HashMap<Label, _> = HashMap::new(); for (l, i) in self.0.iter().rev() { @@ -44,10 +40,7 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); return Some(match i { CtxItem::Kept(newvar, t) => { - TypedValue::from_valuef_and_type( - ValueF::Var(newvar), - t, - ) + Value::from_valuef_and_type(ValueF::Var(newvar), t) } CtxItem::Replaced(v) => v, }); @@ -101,7 +94,7 @@ impl TypecheckContext { ))) } } - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) .unwrap() } @@ -124,8 +117,8 @@ impl Shift for TypecheckContext { } } -impl Subst<TypedValue> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for CtxItem { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), CtxItem::Kept(v, t) => match v.shift(-1, var) { @@ -136,8 +129,8 @@ impl Subst<TypedValue> for CtxItem { } } -impl Subst<TypedValue> for TypecheckContext { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for TypecheckContext { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { self.subst_shift(var, val) } } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index c4e3831..8573d11 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -35,7 +35,7 @@ use Form::{Unevaled, NF, WHNF}; struct ValueInternal { form: Form, value: ValueF, - ty: Option<TypedValue>, + ty: Option<Value>, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -45,11 +45,6 @@ struct ValueInternal { #[derive(Clone)] pub struct Value(Rc<RefCell<ValueInternal>>); -/// A value that needs to carry a type for typechecking to work. -/// TODO: actually enforce this. -#[derive(Debug, Clone)] -pub struct TypedValue(Value); - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -96,7 +91,7 @@ impl ValueInternal { } } - fn get_type(&self) -> Result<&TypedValue, TypeError> { + fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), None => Err(TypeError::new( @@ -116,7 +111,7 @@ impl Value { } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value { + pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { ValueInternal { form: Unevaled, value: v, @@ -125,7 +120,57 @@ impl Value { .into_value() } pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { - Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type)) + Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => Value::from_valuef_untyped(ValueF::Const(c)), + } + } + pub fn const_type() -> Self { + Value::from_const(Const::Type) + } + + pub(crate) fn as_const(&self) -> Option<Const> { + match &*self.as_whnf() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + fn as_internal(&self) -> Ref<ValueInternal> { + self.0.borrow() + } + fn as_internal_mut(&self) -> RefMut<ValueInternal> { + self.0.borrow_mut() + } + /// 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<ValueF> { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) + } + + // TODO: rename `normalize_to_expr` + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr() + } + // TODO: rename `normalize_to_expr_maybe_alpha` + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr_maybe_alpha(true) + } + // TODO: deprecated + pub(crate) fn to_value(&self) -> Value { + self.clone() + } + /// TODO: cloning a valuef can often be avoided + pub(crate) fn to_whnf(&self) -> ValueF { + self.as_whnf().clone() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_value(self) } /// Mutates the contents. If no one else shares this thunk, @@ -138,20 +183,12 @@ impl Value { None => f(&mut self.as_internal_mut()), } } - /// Normalizes contents to normal form; faster than `normalize_nf` if /// no one else shares this thunk. pub(crate) fn normalize_mut(&mut self) { self.mutate_internal(|vint| vint.normalize_nf()) } - fn as_internal(&self) -> Ref<ValueInternal> { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut<ValueInternal> { - self.0.borrow_mut() - } - fn do_normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { @@ -163,7 +200,6 @@ impl Value { WHNF | NF => {} } } - fn do_normalize_nf(&self) { let borrow = self.as_internal(); match borrow.form { @@ -176,26 +212,14 @@ impl Value { } } - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + // TODO: rename to `as_nf` pub(crate) fn normalize_nf(&self) -> Ref<ValueF> { self.do_normalize_nf(); Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// 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<ValueF> { - self.do_normalize_whnf(); - Ref::map(self.as_internal(), ValueInternal::as_whnf) - } - - /// TODO: cloning a valuef can often be avoided - pub(crate) fn to_whnf(&self) -> ValueF { - self.as_whnf().clone() - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, @@ -211,83 +235,11 @@ impl Value { apply_any(self.clone(), th) } - pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> { Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } } -impl TypedValue { - pub fn from_value(th: Value) -> Self { - TypedValue(th) - } - pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue { - TypedValue::from_value(Value::from_valuef_untyped(v)) - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { - TypedValue(Value::from_valuef_and_type(v, t)) - } - // 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_untyped(ValueF::Const(c)), - } - } - pub fn const_type() -> Self { - TypedValue::from_const(Const::Type) - } - - 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 - /// panics. - pub(crate) fn as_whnf(&self) -> Ref<ValueF> { - self.0.as_whnf() - } - pub(crate) fn to_whnf(&self) -> ValueF { - self.0.to_whnf() - } - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.as_whnf().normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.as_whnf().normalize_to_expr_maybe_alpha(true) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_typedvalue(self) - } - pub(crate) fn as_const(&self) -> Option<Const> { - match &*self.as_whnf() { - ValueF::Const(c) => Some(*c), - _ => None, - } - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> { - self.0.get_type() - } -} - impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(Value(self.0.shift(delta, var)?)) @@ -304,20 +256,14 @@ impl Shift for ValueInternal { } } -impl Shift for TypedValue { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(TypedValue(self.0.shift(delta, var)?)) - } -} - -impl Subst<TypedValue> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { Value(self.0.subst_shift(var, val)) } } -impl Subst<TypedValue> for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for ValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, @@ -327,12 +273,7 @@ impl Subst<TypedValue> for ValueInternal { } } -impl Subst<TypedValue> for TypedValue { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { - TypedValue(self.0.subst_shift(var, val)) - } -} - +// 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() @@ -340,13 +281,6 @@ impl std::cmp::PartialEq for Value { } impl std::cmp::Eq for Value {} -impl std::cmp::PartialEq for TypedValue { - fn eq(&self, other: &Self) -> bool { - &*self.as_whnf() == &*other.as_whnf() - } -} -impl std::cmp::Eq for TypedValue {} - impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index de55d2f..0d2655e 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, }; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::OutputSubExpr; use crate::phase::Normalized; @@ -18,8 +18,8 @@ use crate::phase::Normalized; #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures - Lam(AlphaLabel, TypedValue, Value), - Pi(AlphaLabel, TypedValue, TypedValue), + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec<Value>), @@ -29,20 +29,20 @@ pub enum ValueF { NaturalLit(Natural), IntegerLit(Integer), DoubleLit(NaiveDouble), - EmptyOptionalLit(TypedValue), + EmptyOptionalLit(Value), NEOptionalLit(Value), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedValue), + EmptyListLit(Value), NEListLit(Vec<Value>), RecordLit(HashMap<Label, Value>), - RecordType(HashMap<Label, TypedValue>), - UnionType(HashMap<Label, Option<TypedValue>>), - UnionConstructor(Label, HashMap<Label, Option<TypedValue>>), - UnionLit(Label, Value, HashMap<Label, Option<TypedValue>>), + RecordType(HashMap<Label, Value>), + UnionType(HashMap<Label, Option<Value>>), + UnionConstructor(Label, HashMap<Label, Option<Value>>), + UnionLit(Label, Value, HashMap<Label, Option<Value>>), // Invariant: this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec<InterpolatedTextContents<Value>>), - Equivalence(TypedValue, TypedValue), + Equivalence(Value, Value), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF<Value, Normalized>), } @@ -51,7 +51,7 @@ impl ValueF { pub(crate) fn into_value_untyped(self) -> Value { Value::from_valuef_untyped(self) } - pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } pub(crate) fn into_value_simple_type(self) -> Value { @@ -333,8 +333,8 @@ impl Shift for ValueF { } } -impl Subst<TypedValue> for ValueF { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueF::AppliedBuiltin(b, args) => { ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 0f2f5fc..b34c3a2 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,7 +3,7 @@ use std::io::Error as IOError; use dhall_syntax::{BinOp, Import, Label, ParseError, V}; use crate::core::context::TypecheckContext; -use crate::core::value::TypedValue; +use crate::core::value::Value; use crate::phase::resolve::ImportStack; use crate::phase::NormalizedSubExpr; @@ -49,28 +49,28 @@ pub struct TypeError { #[derive(Debug)] pub(crate) enum TypeMessage { UnboundVariable(V<Label>), - InvalidInputType(TypedValue), - InvalidOutputType(TypedValue), - NotAFunction(TypedValue), - TypeMismatch(TypedValue, TypedValue, TypedValue), - AnnotMismatch(TypedValue, TypedValue), + InvalidInputType(Value), + InvalidOutputType(Value), + NotAFunction(Value), + TypeMismatch(Value, Value, Value), + AnnotMismatch(Value, Value), Untyped, FieldCollision(Label), - InvalidListElement(usize, TypedValue, TypedValue), - InvalidListType(TypedValue), - InvalidOptionalType(TypedValue), - InvalidPredicate(TypedValue), - IfBranchMismatch(TypedValue, TypedValue), - IfBranchMustBeTerm(bool, TypedValue), - InvalidFieldType(Label, TypedValue), - NotARecord(Label, TypedValue), - MustCombineRecord(TypedValue), - MissingRecordField(Label, TypedValue), - MissingUnionField(Label, TypedValue), - BinOpTypeMismatch(BinOp, TypedValue), - InvalidTextInterpolation(TypedValue), - Merge1ArgMustBeRecord(TypedValue), - Merge2ArgMustBeUnion(TypedValue), + InvalidListElement(usize, Value, Value), + InvalidListType(Value), + InvalidOptionalType(Value), + InvalidPredicate(Value), + IfBranchMismatch(Value, Value), + IfBranchMustBeTerm(bool, Value), + InvalidFieldType(Label, Value), + NotARecord(Label, Value), + MustCombineRecord(Value), + MissingRecordField(Label, Value), + MissingUnionField(Label, Value), + BinOpTypeMismatch(BinOp, Value), + InvalidTextInterpolation(Value), + Merge1ArgMustBeRecord(Value), + Merge2ArgMustBeUnion(Value), MergeEmptyNeedsAnnotation, MergeHandlerMissingVariant(Label), MergeVariantMissingHandler(Label), @@ -80,14 +80,14 @@ pub(crate) enum TypeMessage { ProjectionMustBeRecord, ProjectionMissingEntry, Sort, - RecordMismatch(TypedValue, TypedValue), + RecordMismatch(Value, Value), RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(TypedValue), - RecordTypeMismatch(TypedValue, TypedValue, TypedValue, TypedValue), + RecordTypeMergeRequiresRecordType(Value), + RecordTypeMismatch(Value, Value, Value, Value), UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, TypedValue), - EquivalenceTypeMismatch(TypedValue, TypedValue), - AssertMismatch(TypedValue, TypedValue), + EquivalenceArgumentMustBeTerm(bool, Value), + EquivalenceTypeMismatch(Value, Value), + AssertMismatch(Value, Value), AssertMustTakeEquivalence, } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index e58e689..91d64c3 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -4,7 +4,7 @@ use std::path::Path; use dhall_syntax::{Const, SubExpr}; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; @@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TypedValue); +pub struct Typed(Value); /// A normalized expression. /// @@ -91,12 +91,12 @@ impl Typed { } pub(crate) fn from_const(c: Const) -> Self { - Typed(TypedValue::from_const(c)) + Typed(Value::from_const(c)) } pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(TypedValue::from_valuef_and_type(v, t.into_typedvalue())) + Typed(Value::from_valuef_and_type(v, t.into_value())) } - pub(crate) fn from_typedvalue(th: TypedValue) -> Self { + pub(crate) fn from_value(th: Value) -> Self { Typed(th) } pub fn const_type() -> Self { @@ -112,7 +112,7 @@ impl Typed { pub fn to_value(&self) -> Value { self.0.to_value() } - pub(crate) fn into_typedvalue(self) -> TypedValue { + pub(crate) fn into_value(self) -> Value { self.0 } @@ -155,8 +155,8 @@ impl Shift for Normalized { } } -impl Subst<TypedValue> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst<Value> for Typed { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { Typed(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 27858d8..821c5fd 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -26,9 +26,7 @@ macro_rules! make_closure { (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { ValueF::Lam( Label::from(stringify!($var)).into(), - TypedValue::from_value_simple_type( - make_closure!($($ty)*), - ), + make_closure!($($ty)*), make_closure!($($rest)*), ).into_value_untyped() }; @@ -51,10 +49,10 @@ macro_rules! make_closure { make_closure!($($rest)*), Value::from_valuef_and_type( ValueF::NaturalLit(1), - TypedValue::from_value(make_closure!(Natural)) + make_closure!(Natural) ), )).into_value_with_type( - TypedValue::from_value(make_closure!(Natural)) + make_closure!(Natural) ) }; ([ $($head:tt)* ] # $($tail:tt)*) => { @@ -74,10 +72,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced. let ret = match (b, args.as_slice()) { - (OptionalNone, [t, r..]) => Ok(( - r, - EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())), - )), + (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))), (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), @@ -199,16 +194,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedValue::from_valuef_untyped(ValueF::from_builtin( - Natural, - )), + Value::from_valuef_untyped(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); Ok(( r, - EmptyListLit(TypedValue::from_valuef_untyped(RecordType( - kts, - ))), + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), )) } NEListLit(xs) => { @@ -252,9 +243,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { [ var(x, 1) ] # var(xs, 0) ) }) - .app_valuef(EmptyListLit( - TypedValue::from_value_simple_type(t.clone()), - )), + .app_valuef(EmptyListLit(t.clone())), )), }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { @@ -288,9 +277,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { ValueF::from_builtin(Optional).app_value(t.clone()), ) .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) - .app_valuef(EmptyOptionalLit( - TypedValue::from_value_simple_type(t.clone()), - )), + .app_valuef(EmptyOptionalLit(t.clone())), )), }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { @@ -346,10 +333,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(a); - e.subst_shift(&x.into(), &val).to_whnf() - } + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); @@ -639,21 +623,18 @@ 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_valuef_untyped(ValueF::PartialExpr( - ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.to_value(), - v2.to_value(), - ), - )) + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( + RecursiveRecordTypeMerge, + v1.to_value(), + v2.to_value(), + ))) }); Ret::ValueF(RecordType(kvs)) } - (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence( - TypedValue::from_value_simple_type(x.clone()), - TypedValue::from_value_simple_type(y.clone()), - )), + (Equivalence, _, _) => { + Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone())) + } _ => return None, }) @@ -674,18 +655,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::Var(_) => unreachable!(), ExprF::Annot(x, _) => Ret::Value(x), ExprF::Assert(_) => Ret::Expr(expr), - ExprF::Lam(x, 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(t), - TypedValue::from_value(e), - )), - ExprF::Let(x, _, v, b) => { - let v = TypedValue::from_value(v); - Ret::Value(b.subst_shift(&x.into(), &v)) - } + ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)), + ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)), + ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)), ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), @@ -699,9 +671,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueF(EmptyListLit( - TypedValue::from_value_simple_type(args[0].clone()), - )) + Ret::ValueF(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -715,16 +685,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::RecordLit(kvs) => { Ret::ValueF(RecordLit(kvs.into_iter().collect())) } - ExprF::RecordType(kts) => Ret::ValueF(RecordType( - kts.into_iter() - .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(t)))) - .collect(), - )), + ExprF::RecordType(kts) => { + Ret::ValueF(RecordType(kts.into_iter().collect())) + } + ExprF::UnionType(kts) => { + Ret::ValueF(UnionType(kts.into_iter().collect())) + } ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index e24f5a3..e65881e 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; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -14,9 +14,9 @@ use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: TypedValue, - te: TypedValue, -) -> Result<TypedValue, TypeError> { + tx: Value, + te: Value, +) -> Result<Value, TypeError> { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); @@ -37,16 +37,16 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::Pi(x.into(), tx, te), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, TypedValue), TypeError>>, -) -> Result<TypedValue, TypeError> { + kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>, +) -> Result<Value, TypeError> { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -70,18 +70,18 @@ fn tck_record_type( // An empty record type has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::RecordType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_union_type<Iter>( ctx: &TypecheckContext, kts: Iter, -) -> Result<TypedValue, TypeError> +) -> Result<Value, TypeError> where - Iter: IntoIterator<Item = Result<(Label, Option<TypedValue>), TypeError>>, + Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>, { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; @@ -115,9 +115,9 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::UnionType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } @@ -130,10 +130,10 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn type_of_const(c: Const) -> Result<TypedValue, TypeError> { +pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> { match c { - Const::Type => Ok(TypedValue::from_const(Const::Kind)), - Const::Kind => Ok(TypedValue::from_const(Const::Sort)), + Const::Type => Ok(Value::from_const(Const::Kind)), + Const::Kind => Ok(Value::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -282,16 +282,16 @@ 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> { +pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetWhole(TypedValue), - /// Use the contained TypedValue as the type of the input expression - RetTypeOnly(TypedValue), + RetWhole(Value), + /// Use the contained Value as the type of the input expression + RetTypeOnly(Value), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -301,7 +301,7 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr<Normalized>, -) -> Result<TypedValue, TypeError> { +) -> Result<Value, TypeError> { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; use Ret::*; @@ -313,7 +313,7 @@ fn type_with( let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value()); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?; - TypedValue::from_valuef_and_type(v, t) + Value::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { let ta = type_with(ctx, ta.clone())?; @@ -331,7 +331,7 @@ fn type_with( let v = type_with(ctx, v)?; return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } - Embed(p) => p.clone().into_typed().into_typedvalue(), + Embed(p) => p.clone().into_typed().into_value(), Var(var) => match ctx.lookup(&var) { Some(typed) => typed.clone(), None => { @@ -352,10 +352,7 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - TypedValue::from_valuef_and_type( - ValueF::PartialExpr(expr), - typ, - ) + Value::from_valuef_and_type(ValueF::PartialExpr(expr), typ) } RetWhole(tt) => tt, } @@ -367,7 +364,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF<TypedValue, Normalized>, + e: &ExprF<Value, Normalized>, ) -> Result<Ret, TypeError> { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -466,10 +463,10 @@ fn type_last_layer( )); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } SomeLit(x) => { @@ -478,10 +475,10 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } RecordType(kts) => Ok(RetWhole(tck_record_type( @@ -545,7 +542,7 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetWhole(TypedValue::from_const(*c))), + Const(c) => Ok(RetWhole(Value::from_const(*c))), Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), @@ -607,43 +604,38 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap<Label, TypedValue>, - kts_r: &HashMap<Label, TypedValue>, - ) -> Result<TypedValue, TypeError> { + kts_l: &HashMap<Label, Value>, + kts_r: &HashMap<Label, Value>, + ) -> Result<Value, TypeError> { use crate::phase::normalize::outer_join; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - inner_l: &TypedValue, - inner_r: &TypedValue| - -> Result<TypedValue, TypeError> { - match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { - ( - ValueF::RecordType(inner_l_kvs), - ValueF::RecordType(inner_r_kvs), - ) => combine_record_types( - ctx, - inner_l_kvs, - inner_r_kvs, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + inner_l: &Value, + inner_r: &Value| + -> Result<Value, TypeError> { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { + ( + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), + ) => { + combine_record_types(ctx, inner_l_kvs, inner_r_kvs) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; - let kts: HashMap<Label, Result<TypedValue, TypeError>> = - outer_join( - |l| Ok(l.clone()), - |r| Ok(r.clone()), - combine, - kts_l, - kts_r, - ); + let kts: HashMap<Label, Result<Value, TypeError>> = outer_join( + |l| Ok(l.clone()), + |r| Ok(r.clone()), + combine, + kts_l, + kts_r, + ); Ok(tck_record_type( ctx, @@ -684,35 +676,30 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap<Label, TypedValue>, - kts_r: &HashMap<Label, TypedValue>, - ) -> Result<TypedValue, TypeError> { + kts_l: &HashMap<Label, Value>, + kts_r: &HashMap<Label, Value>, + ) -> Result<Value, TypeError> { use crate::phase::normalize::intersection_with_key; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - kts_l_inner: &TypedValue, - kts_r_inner: &TypedValue| - -> Result<TypedValue, TypeError> { - match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) - { - ( - ValueF::RecordType(kvs_l_inner), - ValueF::RecordType(kvs_r_inner), - ) => combine_record_types( - ctx, - kvs_l_inner, - kvs_r_inner, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + kts_l_inner: &Value, + kts_r_inner: &Value| + -> Result<Value, TypeError> { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { + ( + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), + ) => { + combine_record_types(ctx, kvs_l_inner, kvs_r_inner) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; let kts = intersection_with_key(combine, kts_l, kts_r); @@ -747,8 +734,8 @@ fn type_last_layer( k_l } else { return Err(mkerr(RecordTypeMismatch( - TypedValue::from_const(k_l), - TypedValue::from_const(k_r), + Value::from_const(k_l), + Value::from_const(k_r), l.clone(), r.clone(), ))); @@ -779,7 +766,7 @@ fn type_last_layer( // Ensure that the records combine without a type error // and if not output the final Const value. combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(TypedValue::from_const(k)))) + .and(Ok(RetTypeOnly(Value::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { @@ -814,7 +801,7 @@ fn type_last_layer( ))); } - Ok(RetTypeOnly(TypedValue::from_const(Type))) + Ok(RetTypeOnly(Value::from_const(Type))) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -941,7 +928,7 @@ fn type_last_layer( }; } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), ))) @@ -952,15 +939,13 @@ fn type_last_layer( /// `type_of` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -pub(crate) fn typecheck( - e: SubExpr<Normalized>, -) -> Result<TypedValue, TypeError> { +pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> { type_with(&TypecheckContext::new(), e) } pub(crate) fn typecheck_with( expr: SubExpr<Normalized>, ty: SubExpr<Normalized>, -) -> Result<TypedValue, TypeError> { +) -> Result<Value, TypeError> { typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 9d2ec85..cef11dd 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -124,9 +124,8 @@ pub use value::Value; // A Dhall value. pub mod value { - use dhall::core::value::TypedValue as TypedThunk; - use dhall::core::value::Value as Thunk; - use dhall::core::valuef::ValueF as DhallValue; + use dhall::core::value::Value as DhallValue; + use dhall::core::valuef::ValueF as DhallValueF; use dhall::phase::{NormalizedSubExpr, Parsed, Typed}; use dhall_syntax::Builtin; @@ -154,7 +153,7 @@ pub mod value { pub(crate) fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() } - pub(crate) fn to_value(&self) -> Thunk { + pub(crate) fn to_value(&self) -> DhallValue { self.0.to_value() } pub(crate) fn as_typed(&self) -> &Typed { @@ -162,21 +161,22 @@ pub mod value { } /// Assumes that the given value has type `Type`. - pub(crate) fn make_simple_type(v: DhallValue) -> Self { + pub(crate) fn make_simple_type(v: DhallValueF) -> Self { Value(Typed::from_valuef_and_type(v, Typed::const_type())) } pub(crate) fn make_builtin_type(b: Builtin) -> Self { - Self::make_simple_type(DhallValue::from_builtin(b)) + Self::make_simple_type(DhallValueF::from_builtin(b)) } pub(crate) fn make_optional_type(t: Value) -> Self { Self::make_simple_type( - DhallValue::from_builtin(Builtin::Optional) + DhallValueF::from_builtin(Builtin::Optional) .app_value(t.to_value()), ) } pub(crate) fn make_list_type(t: Value) -> Self { Self::make_simple_type( - DhallValue::from_builtin(Builtin::List).app_value(t.to_value()), + DhallValueF::from_builtin(Builtin::List) + .app_value(t.to_value()), ) } // Made public for the StaticType derive macro @@ -184,22 +184,17 @@ pub mod value { pub fn make_record_type( kts: impl Iterator<Item = (String, Value)>, ) -> Self { - Self::make_simple_type(DhallValue::RecordType( - kts.map(|(k, t)| { - (k.into(), TypedThunk::from_value(t.to_value())) - }) - .collect(), + Self::make_simple_type(DhallValueF::RecordType( + kts.map(|(k, t)| (k.into(), t.to_value())).collect(), )) } #[doc(hidden)] pub fn make_union_type( kts: impl Iterator<Item = (String, Option<Value>)>, ) -> Self { - Self::make_simple_type(DhallValue::UnionType( - kts.map(|(k, t)| { - (k.into(), t.map(|t| TypedThunk::from_value(t.to_value()))) - }) - .collect(), + Self::make_simple_type(DhallValueF::UnionType( + kts.map(|(k, t)| (k.into(), t.map(|t| t.to_value()))) + .collect(), )) } } |