diff options
| -rw-r--r-- | dhall/src/core/context.rs | 29 | ||||
| -rw-r--r-- | dhall/src/core/value.rs | 48 | ||||
| -rw-r--r-- | dhall/src/core/valuef.rs | 6 | ||||
| -rw-r--r-- | dhall/src/error/mod.rs | 55 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 51 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 6 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 392 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 2 | ||||
| -rw-r--r-- | serde_dhall/src/lib.rs | 10 |
9 files changed, 260 insertions, 339 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index e1a23a9..851e4c4 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,16 +3,15 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::value::Value; +use crate::core::value::{TypedValue, Value}; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::TypeError; -use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] enum CtxItem { - Kept(AlphaVar, Type), - Replaced(Value, Type), + Kept(AlphaVar, TypedValue), + Replaced(Value, TypedValue), } #[derive(Debug, Clone)] @@ -22,12 +21,16 @@ impl TypecheckContext { pub fn new() -> Self { TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_type(&self, x: &Label, t: Type) -> Self { + pub fn insert_type(&self, x: &Label, t: TypedValue) -> 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: Typed) -> Result<Self, TypeError> { + pub fn insert_value( + &self, + x: &Label, + e: TypedValue, + ) -> Result<Self, TypeError> { let mut vec = self.0.as_ref().clone(); vec.push(( x.clone(), @@ -35,7 +38,7 @@ impl TypecheckContext { )); Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V<Label>) -> Option<Typed> { + pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> { let mut var = var.clone(); let mut shift_map: HashMap<Label, _> = HashMap::new(); for (l, i) in self.0.iter().rev() { @@ -48,7 +51,7 @@ impl TypecheckContext { } CtxItem::Replaced(th, t) => (th, t), }; - return Some(Typed::from_value_and_type(th, t)); + return Some(TypedValue::from_value_and_type(th, t)); } Some(newvar) => var = newvar, }; @@ -99,7 +102,7 @@ impl TypecheckContext { ))) } } - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) .unwrap() } @@ -124,8 +127,8 @@ impl Shift for TypecheckContext { } } -impl Subst<Typed> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +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), @@ -141,8 +144,8 @@ impl Subst<Typed> for CtxItem { } } -impl Subst<Typed> for TypecheckContext { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for TypecheckContext { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { self.subst_shift(var, val) } } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 213a2bd..f4cb6b6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -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, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] enum Form { @@ -35,12 +35,12 @@ use Form::{Unevaled, NF, WHNF}; struct ValueInternal { form: Form, value: ValueF, - ty: Option<Type>, + ty: Option<TypedValue>, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, /// sharing computation automatically. Uses a RefCell to share computation. -/// Can optionally store a Type from typechecking to preserve type information through +/// Can optionally store a type from typechecking to preserve type information through /// normalization. #[derive(Clone)] pub struct Value(Rc<RefCell<ValueInternal>>); @@ -96,7 +96,7 @@ impl ValueInternal { } } - fn get_type(&self) -> Result<&Type, TypeError> { + fn get_type(&self) -> Result<&TypedValue, TypeError> { match &self.ty { Some(t) => Ok(t), None => Err(TypeError::new( @@ -116,7 +116,7 @@ impl Value { } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value { ValueInternal { form: Unevaled, value: v, @@ -128,7 +128,7 @@ impl Value { Value::from_valuef(ValueF::PartialExpr(e)) } // TODO: avoid using this function - pub(crate) fn with_type(self, t: Type) -> Value { + pub(crate) fn with_type(self, t: TypedValue) -> Value { let vint = self.as_internal(); ValueInternal { form: vint.form, @@ -221,7 +221,7 @@ impl Value { apply_any(self.clone(), th) } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> { Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } } @@ -231,18 +231,10 @@ impl TypedValue { TypedValue::from_value_untyped(Value::from_valuef(v)) } - pub(crate) fn from_type(t: Type) -> TypedValue { - t.into_typedvalue() - } - pub(crate) fn normalize_nf(&self) -> ValueF { self.0.normalize_nf().clone() } - pub(crate) fn to_typed(&self) -> Typed { - self.clone().into_typed() - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, @@ -250,11 +242,11 @@ impl TypedValue { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { + pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self { TypedValue(th.with_type(t)) } pub fn from_value_simple_type(th: Value) -> Self { - TypedValue::from_value_and_type(th, Type::const_type()) + TypedValue::from_value_and_type(th, TypedValue::const_type()) } pub(crate) fn from_value_untyped(th: Value) -> Self { TypedValue(th) @@ -265,7 +257,10 @@ impl TypedValue { Err(_) => TypedValue::from_valuef(ValueF::Const(c)), } } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + 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)) } @@ -286,9 +281,6 @@ impl TypedValue { pub(crate) fn to_value(&self) -> Value { self.0.clone() } - pub(crate) fn to_type(&self) -> Type { - self.clone().into_typed().into_type() - } pub(crate) fn into_typed(self) -> Typed { Typed::from_typedvalue(self) } @@ -303,7 +295,7 @@ impl TypedValue { self.0.normalize_mut() } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> { self.0.get_type() } } @@ -330,14 +322,14 @@ impl Shift for TypedValue { } } -impl Subst<Typed> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for Value { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { Value(self.0.subst_shift(var, val)) } } -impl Subst<Typed> for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for ValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, @@ -347,8 +339,8 @@ impl Subst<Typed> for ValueInternal { } } -impl Subst<Typed> for TypedValue { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { TypedValue(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 0ba1d59..b948eb1 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -8,7 +8,7 @@ use dhall_syntax::{ use crate::core::value::{TypedValue, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::OutputSubExpr; -use crate::phase::{Normalized, Typed}; +use crate::phase::Normalized; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. @@ -327,8 +327,8 @@ impl Shift for ValueF { } } -impl Subst<Typed> for ValueF { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> 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 34a89c0..0f2f5fc 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,8 +3,9 @@ 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::phase::resolve::ImportStack; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::NormalizedSubExpr; pub type Result<T> = std::result::Result<T, Error>; @@ -48,28 +49,28 @@ pub struct TypeError { #[derive(Debug)] pub(crate) enum TypeMessage { UnboundVariable(V<Label>), - InvalidInputType(Typed), - InvalidOutputType(Typed), - NotAFunction(Typed), - TypeMismatch(Typed, Typed, Typed), - AnnotMismatch(Typed, Typed), + InvalidInputType(TypedValue), + InvalidOutputType(TypedValue), + NotAFunction(TypedValue), + TypeMismatch(TypedValue, TypedValue, TypedValue), + AnnotMismatch(TypedValue, TypedValue), Untyped, FieldCollision(Label), - InvalidListElement(usize, Typed, Typed), - InvalidListType(Typed), - InvalidOptionalType(Typed), - InvalidPredicate(Typed), - IfBranchMismatch(Typed, Typed), - IfBranchMustBeTerm(bool, Typed), - InvalidFieldType(Label, Type), - NotARecord(Label, Typed), - MustCombineRecord(Typed), - MissingRecordField(Label, Typed), - MissingUnionField(Label, Typed), - BinOpTypeMismatch(BinOp, Typed), - InvalidTextInterpolation(Typed), - Merge1ArgMustBeRecord(Typed), - Merge2ArgMustBeUnion(Typed), + 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), MergeEmptyNeedsAnnotation, MergeHandlerMissingVariant(Label), MergeVariantMissingHandler(Label), @@ -79,14 +80,14 @@ pub(crate) enum TypeMessage { ProjectionMustBeRecord, ProjectionMissingEntry, Sort, - RecordMismatch(Typed, Typed), + RecordMismatch(TypedValue, TypedValue), RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Type), - RecordTypeMismatch(Type, Type, Type, Type), + RecordTypeMergeRequiresRecordType(TypedValue), + RecordTypeMismatch(TypedValue, TypedValue, TypedValue, TypedValue), UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Typed), - EquivalenceTypeMismatch(Typed, Typed), - AssertMismatch(Typed, Typed), + EquivalenceArgumentMustBeTerm(bool, TypedValue), + EquivalenceTypeMismatch(TypedValue, TypedValue), + AssertMismatch(TypedValue, TypedValue), AssertMustTakeEquivalence, } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index a38e9d3..e58e689 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -1,5 +1,4 @@ use std::borrow::Cow; -use std::cell::Ref; use std::fmt::Display; use std::path::Path; @@ -42,8 +41,6 @@ pub struct Typed(TypedValue); #[derive(Debug, Clone)] pub struct Normalized(Typed); -pub type Type = Typed; - impl Parsed { pub fn parse_file(f: &Path) -> Result<Parsed, Error> { parse::parse_file(f) @@ -72,10 +69,10 @@ impl Parsed { impl Resolved { pub fn typecheck(self) -> Result<Typed, TypeError> { - typecheck::typecheck(self) + Ok(typecheck::typecheck(self.0)?.into_typed()) } - pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> { - typecheck::typecheck_with(self, ty) + pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> { + Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) } } @@ -93,17 +90,11 @@ impl Typed { Normalized(self) } - pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { - Typed(TypedValue::from_value_and_type(th, t)) - } - pub(crate) fn from_value_untyped(th: Value) -> Self { - Typed(TypedValue::from_value_untyped(th)) - } pub(crate) fn from_const(c: Const) -> Self { Typed(TypedValue::from_const(c)) } - pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - Typed(TypedValue::from_valuef_and_type(v, t)) + pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { + Typed(TypedValue::from_valuef_and_type(v, t.into_typedvalue())) } pub(crate) fn from_typedvalue(th: TypedValue) -> Self { Typed(th) @@ -112,14 +103,6 @@ impl Typed { Typed::from_const(Const::Type) } - /// 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 fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() } @@ -129,27 +112,17 @@ impl Typed { pub fn to_value(&self) -> Value { self.0.to_value() } - // Deprecated - pub fn to_type(&self) -> Type { - self.clone() - } - // Deprecated - pub(crate) fn into_type(self) -> Type { - self - } pub(crate) fn into_typedvalue(self) -> TypedValue { self.0 } - pub(crate) fn as_const(&self) -> Option<Const> { - self.0.as_const() - } pub(crate) fn normalize_mut(&mut self) { self.0.normalize_mut() } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { - self.0.get_type() + #[allow(dead_code)] + pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> { + Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed())) } } @@ -165,10 +138,6 @@ impl Normalized { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.0.to_expr_alpha() } - #[allow(dead_code)] - pub(crate) fn to_type(&self) -> Type { - self.0.to_type() - } pub(crate) fn into_typed(self) -> Typed { self.0 } @@ -186,8 +155,8 @@ impl Shift for Normalized { } } -impl Subst<Typed> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<TypedValue> for Typed { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { Typed(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 785a75f..dabfe87 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -8,7 +8,7 @@ use dhall_syntax::{ use crate::core::value::{TypedValue, Value}; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr}; pub(crate) type OutputSubExpr = NormalizedSubExpr; @@ -327,7 +327,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 = Typed::from_value_untyped(a); + let val = TypedValue::from_value_untyped(a); e.subst_shift(&x.into(), &val).to_whnf() } ValueF::AppliedBuiltin(b, args) => { @@ -663,7 +663,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { TypedValue::from_value_untyped(e), )), ExprF::Let(x, _, v, b) => { - let v = Typed::from_value_untyped(v); + let v = TypedValue::from_value_untyped(v); Ret::Value(b.subst_shift(&x.into(), &v)) } ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index c303ada..07c4ad8 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -9,14 +9,14 @@ use crate::core::value::{TypedValue, Value}; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::{Normalized, Resolved, Type, Typed}; +use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: Type, - te: Type, -) -> Result<Typed, TypeError> { + tx: TypedValue, + te: TypedValue, +) -> Result<TypedValue, TypeError> { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); @@ -37,21 +37,16 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Typed::from_value_and_type( - ValueF::Pi( - x.into(), - TypedValue::from_type(tx), - TypedValue::from_type(te), - ) - .into_value(), - Type::from_const(k), + Ok(TypedValue::from_value_and_type( + ValueF::Pi(x.into(), tx, te).into_value(), + TypedValue::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Type), TypeError>>, -) -> Result<Typed, TypeError> { + kts: impl IntoIterator<Item = Result<(Label, TypedValue), TypeError>>, +) -> Result<TypedValue, TypeError> { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -62,36 +57,32 @@ fn tck_record_type( match (k, t.get_type()?.as_const()) { (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x.clone(), t.clone()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), } - let entry = new_kts.entry(x.clone()); + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } - Entry::Vacant(_) => { - entry.or_insert_with(|| TypedValue::from_type(t.clone())) - } + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } // An empty record type has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); + let k = k.unwrap_or(Const::Type); - Ok(Typed::from_value_and_type( + Ok(TypedValue::from_value_and_type( ValueF::RecordType(new_kts).into_value(), - Type::from_const(k), + TypedValue::from_const(k), )) } -fn tck_union_type( +fn tck_union_type<Iter>( ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Option<Type>), TypeError>>, -) -> Result<Typed, TypeError> { + kts: Iter, +) -> Result<TypedValue, TypeError> +where + Iter: IntoIterator<Item = Result<(Label, Option<TypedValue>), TypeError>>, +{ use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -106,46 +97,43 @@ fn tck_union_type( _ => { return Err(TypeError::new( ctx, - InvalidFieldType(x.clone(), t.clone()), + InvalidFieldType(x, t.clone()), )) } } } - let entry = new_kts.entry(x.clone()); + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } - Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypedValue::from_type(t.clone())) - }), + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } // An empty union type has type Type; // an union type with only unary variants also has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); + let k = k.unwrap_or(Const::Type); - Ok(Typed::from_value_and_type( + Ok(TypedValue::from_value_and_type( ValueF::UnionType(new_kts).into_value(), - Type::from_const(k), + TypedValue::from_const(k), )) } fn function_check(a: Const, b: Const) -> Const { - use dhall_syntax::Const::Type; use std::cmp::max; - if b == Type { - Type + if b == Const::Type { + Const::Type } else { max(a, b) } } -pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> { +pub(crate) fn type_of_const(c: Const) -> Result<TypedValue, TypeError> { match c { - Const::Type => Ok(Type::from_const(Const::Kind)), - Const::Kind => Ok(Type::from_const(Const::Sort)), + Const::Type => Ok(TypedValue::from_const(Const::Kind)), + Const::Kind => Ok(TypedValue::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -293,25 +281,16 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { } } -/// Takes an expression that is meant to contain a Type -/// and turn it into a type, typechecking it along the way. -pub(crate) fn mktype( - ctx: &TypecheckContext, - e: SubExpr<Normalized>, -) -> Result<Type, TypeError> { - Ok(type_with(ctx, e)?.to_type()) -} - -pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> { - mktype(&TypecheckContext::new(), SubExpr::from_builtin(b)) +pub(crate) fn builtin_to_type(b: Builtin) -> Result<TypedValue, TypeError> { + type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetWhole(Typed), - /// Use the contained Type as the type of the input expression - RetTypeOnly(Type), + RetWhole(TypedValue), + /// Use the contained TypedValue as the type of the input expression + RetTypeOnly(TypedValue), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -321,28 +300,24 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr<Normalized>, -) -> Result<Typed, TypeError> { +) -> Result<TypedValue, TypeError> { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; use Ret::*; Ok(match e.as_ref() { Lam(x, t, b) => { - let tx = mktype(ctx, t.clone())?; + let tx = type_with(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = ValueF::Lam( - x.clone().into(), - TypedValue::from_type(tx.clone()), - b.to_value(), - ); + 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)?.to_type(); - Typed::from_value_and_type(Value::from_valuef(v), t) + let t = tck_pi_type(ctx, x.clone(), tx, tb)?; + TypedValue::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { - let ta = mktype(ctx, ta.clone())?; + let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); - let tb = mktype(&ctx2, tb.clone())?; + let tb = type_with(&ctx2, tb.clone())?; return tck_pi_type(ctx, x.clone(), ta, tb); } Let(x, t, v, e) => { @@ -355,9 +330,9 @@ 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(), + Embed(p) => p.clone().into_typed().into_typedvalue(), Var(var) => match ctx.lookup(&var) { - Some(typed) => typed, + Some(typed) => typed.clone(), None => { return Err(TypeError::new( ctx, @@ -376,7 +351,7 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - Typed::from_value_and_type( + TypedValue::from_value_and_type( Value::from_partial_expr(expr), typ, ) @@ -391,7 +366,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF<Typed, Normalized>, + e: &ExprF<TypedValue, Normalized>, ) -> Result<Ret, TypeError> { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -410,22 +385,24 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &*tf.as_whnf() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) - } + let tf_borrow = tf.as_whnf(); + let (x, tx, tb) = match &*tf_borrow { + ValueF::Pi(x, tx, tb) => (x, tx, tb), _ => return Err(mkerr(NotAFunction(f.clone()))), }; - if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone()))); + if a.get_type()?.as_ref() != tx { + return Err(mkerr(TypeMismatch( + f.clone(), + tx.clone(), + a.clone(), + ))); } - Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) + Ok(RetTypeOnly(tb.subst_shift(&x.into(), a))) } Annot(x, t) => { - let t = t.to_type(); - if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t))); + if t != x.get_type()?.as_ref() { + return Err(mkerr(AnnotMismatch(x.clone(), t.clone()))); } Ok(RetTypeOnly(x.get_type()?.into_owned())) } @@ -433,14 +410,11 @@ fn type_last_layer( match &*t.as_whnf() { ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { - return Err(mkerr(AssertMismatch( - x.to_typed(), - y.to_typed(), - ))) + return Err(mkerr(AssertMismatch(x.clone(), y.clone()))) } _ => return Err(mkerr(AssertMustTakeEquivalence)), } - Ok(RetTypeOnly(t.to_type())) + Ok(RetTypeOnly(t.clone())) } BoolIf(x, y, z) => { if x.get_type()?.as_ref() != &builtin_to_type(Bool)? { @@ -462,7 +436,6 @@ fn type_last_layer( Ok(RetTypeOnly(y.get_type()?.into_owned())) } EmptyListLit(t) => { - let t = t.to_type(); match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} @@ -470,7 +443,7 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidListType(t.clone()))) } } - Ok(RetTypeOnly(t)) + Ok(RetTypeOnly(t.clone())) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); @@ -492,15 +465,12 @@ fn type_last_layer( )); } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.to_value()) - .into_value(), - Typed::from_const(Type), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::List) + .app_value(t.to_value()) + .into_value(), + TypedValue::from_const(Type), + ))) } SomeLit(x) => { let t = x.get_type()?.into_owned(); @@ -508,38 +478,31 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t.to_value()) - .into_value(), - Typed::from_const(Type).into_type(), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::Optional) + .app_value(t.to_value()) + .into_value(), + TypedValue::from_const(Type), + ))) } RecordType(kts) => Ok(RetWhole(tck_record_type( ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))), + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?)), UnionType(kts) => Ok(RetWhole(tck_union_type( ctx, - kts.iter() - .map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))), + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), + )?)), + RecordLit(kvs) => Ok(RetTypeOnly(tck_record_type( + ctx, + kvs.iter() + .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), )?)), - RecordLit(kvs) => Ok(RetTypeOnly( - tck_record_type( - ctx, - kvs.iter() - .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), - )? - .into_type(), - )), Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { - Ok(RetTypeOnly(tth.to_type())) + Ok(RetTypeOnly(tth.clone())) }, None => Err(mkerr(MissingRecordField(x.clone(), r.clone()))), @@ -554,9 +517,9 @@ fn type_last_layer( tck_pi_type( ctx, "_".into(), - t.to_type(), + t.clone(), r.under_binder(Label::from("_")), - )?.to_type() + )? )) }, Some(None) => { @@ -579,12 +542,12 @@ fn type_last_layer( } // _ => Err(mkerr(NotARecord( // x, - // r.to_type()?, + // r?, // ))), } } - Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)), + Const(c) => Ok(RetWhole(TypedValue::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)?)), IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), @@ -635,13 +598,10 @@ fn type_last_layer( let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union - Ok(RetTypeOnly( - tck_record_type( - ctx, - kts.iter().map(|(x, v)| Ok((x.clone(), v.to_type()))), - )? - .into_type(), - )) + Ok(RetTypeOnly(tck_record_type( + ctx, + kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), + )?)) } BinOp(RecursiveRecordMerge, l, r) => { // A recursive function to dig down into @@ -650,42 +610,46 @@ fn type_last_layer( ctx: &TypecheckContext, kts_l: &HashMap<Label, TypedValue>, kts_r: &HashMap<Label, TypedValue>, - ) -> Result<Typed, TypeError> { + ) -> Result<TypedValue, TypeError> { use crate::phase::normalize::outer_join; - // If the Label exists for both records and Type for the values + // 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<Typed, 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) + 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()), + )), } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; + }; - let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join( - |l| Ok(l.to_type()), - |r| Ok(r.to_type()), - combine, - kts_l, - kts_r, - ); + let kts: HashMap<Label, Result<TypedValue, TypeError>> = + outer_join( + |l| Ok(l.clone()), + |r| Ok(r.clone()), + combine, + kts_l, + kts_r, + ); Ok(tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) + )?) }; let l_type = l.get_type()?; @@ -723,36 +687,40 @@ fn type_last_layer( ctx: &TypecheckContext, kts_l: &HashMap<Label, TypedValue>, kts_r: &HashMap<Label, TypedValue>, - ) -> Result<Typed, TypeError> { + ) -> Result<TypedValue, TypeError> { use crate::phase::normalize::intersection_with_key; - // If the Label exists for both records and Type for the values + // 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<Typed, 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) + 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()), + )), } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; + }; let kts = intersection_with_key(combine, kts_l, kts_r); Ok(tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) + )?) }; // Extract the Const of the LHS @@ -780,8 +748,8 @@ fn type_last_layer( k_l } else { return Err(mkerr(RecordTypeMismatch( - Typed::from_const(k_l), - Typed::from_const(k_r), + TypedValue::from_const(k_l), + TypedValue::from_const(k_r), l.clone(), r.clone(), ))); @@ -812,7 +780,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(Typed::from_const(k)))) + .and(Ok(RetTypeOnly(TypedValue::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { @@ -847,7 +815,7 @@ fn type_last_layer( ))); } - Ok(RetTypeOnly(Typed::from_const(Type).into_type())) + Ok(RetTypeOnly(TypedValue::from_const(Type))) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -892,17 +860,14 @@ fn type_last_layer( }; let mut inferred_type = None; - for (x, handler) in handlers { + for (x, handler_type) in handlers { let handler_return_type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &*handler_type.as_whnf() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_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), _ => { return Err(mkerr(NotAFunction( handler_type.clone(), @@ -910,11 +875,11 @@ fn type_last_layer( } }; - if &variant_type != &tx { + if variant_type != tx { return Err(mkerr(TypeMismatch( - handler_type, - tx, - variant_type, + handler_type.clone(), + tx.clone(), + variant_type.clone(), ))); } @@ -927,7 +892,7 @@ fn type_last_layer( } } // Union alternative without type - Some(None) => handler.to_type(), + Some(None) => handler_type.clone(), None => { return Err(mkerr(MergeHandlerMissingVariant( x.clone(), @@ -951,14 +916,13 @@ fn type_last_layer( match (inferred_type, type_annot) { (Some(ref t1), Some(t2)) => { - let t2 = t2.to_type(); - if t1 != &t2 { + if t1 != t2 { return Err(mkerr(MergeAnnotMismatch)); } - Ok(RetTypeOnly(t2)) + Ok(RetTypeOnly(t2.clone())) } (Some(t), None) => Ok(RetTypeOnly(t)), - (None, Some(t)) => Ok(RetTypeOnly(t.to_type())), + (None, Some(t)) => Ok(RetTypeOnly(t.clone())), (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)), } } @@ -978,34 +942,26 @@ fn type_last_layer( }; } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), - record_type.get_type()?.into_owned(), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), + record_type.get_type()?.into_owned(), + ))) } } } -/// `typeOf` is the same as `type_with` with an empty context, meaning that the +/// `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. -fn type_of(e: SubExpr<Normalized>) -> Result<Typed, TypeError> { - let ctx = TypecheckContext::new(); - type_with(&ctx, e) -} - -pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> { - type_of(e.0) +pub(crate) fn typecheck( + e: SubExpr<Normalized>, +) -> Result<TypedValue, TypeError> { + type_with(&TypecheckContext::new(), e) } pub(crate) fn typecheck_with( - e: Resolved, - ty: &Type, -) -> Result<Typed, TypeError> { - let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr(); - type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) + expr: SubExpr<Normalized>, + ty: SubExpr<Normalized>, +) -> Result<TypedValue, TypeError> { + typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 44e22e4..be4805d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -181,7 +181,7 @@ pub fn run_test( assert_eq_display!(expr, expected); } Typecheck => { - expr.typecheck_with(&expected.to_type())?.get_type()?; + expr.typecheck_with(&expected.into_typed())?.get_type()?; } TypeInference => { let expr = expr.typecheck()?; diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 48f311e..31643d0 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -127,7 +127,7 @@ 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::phase::{NormalizedSubExpr, Parsed, Type, Typed}; + use dhall::phase::{NormalizedSubExpr, Parsed, Typed}; use dhall_syntax::Builtin; use super::de::{Error, Result}; @@ -147,7 +147,7 @@ pub mod value { let resolved = Parsed::parse_str(s)?.resolve()?; let typed = match ty { None => resolved.typecheck()?, - Some(t) => resolved.typecheck_with(&t.to_type())?, + Some(t) => resolved.typecheck_with(t.as_typed())?, }; Ok(Value(typed)) } @@ -157,13 +157,13 @@ pub mod value { pub(crate) fn to_value(&self) -> Thunk { self.0.to_value() } - pub(crate) fn to_type(&self) -> Type { - self.0.to_type() + pub(crate) fn as_typed(&self) -> &Typed { + &self.0 } /// Assumes that the given value has type `Type`. pub(crate) fn make_simple_type(v: DhallValue) -> Self { - Value(Typed::from_valuef_and_type(v, Type::const_type())) + 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)) |