summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-08-19 21:52:26 +0200
committerNadrieril2019-08-19 21:52:42 +0200
commit26a1fd0f0861038a76a0f9b09eaef16d808d4139 (patch)
treee89770d190a73ce5f1bae7798b77c02b598faed2
parent29016b78736dca857e4e7f7c4dc68ed5e30c28bb (diff)
Use TypedValue instead of Typed in normalize and typecheck
Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized
-rw-r--r--dhall/src/core/context.rs29
-rw-r--r--dhall/src/core/value.rs48
-rw-r--r--dhall/src/core/valuef.rs6
-rw-r--r--dhall/src/error/mod.rs55
-rw-r--r--dhall/src/phase/mod.rs51
-rw-r--r--dhall/src/phase/normalize.rs6
-rw-r--r--dhall/src/phase/typecheck.rs392
-rw-r--r--dhall/src/tests.rs2
-rw-r--r--serde_dhall/src/lib.rs10
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))