From 52f9ecfc4dac65d305fd920e8c7f748889a0804f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 12 Aug 2019 23:24:48 +0200 Subject: Move api into its own crate --- dhall/src/core/mod.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs index a202e72..0667df8 100644 --- a/dhall/src/core/mod.rs +++ b/dhall/src/core/mod.rs @@ -1,4 +1,4 @@ -pub(crate) mod context; -pub(crate) mod thunk; -pub(crate) mod value; -pub(crate) mod var; +pub mod context; +pub mod thunk; +pub mod value; +pub mod var; -- cgit v1.3.1 From 1ed3123aeb3c9272b6810605a7ee781c42095f09 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:20:35 +0200 Subject: Swap Typed and TypeThunk --- dhall/src/core/thunk.rs | 125 ++++++++++++++++++++++++++++++++++++++++-------- dhall/src/phase/mod.rs | 95 ++++++++++-------------------------- 2 files changed, 129 insertions(+), 91 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index f41579c..740ecbc 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -1,15 +1,18 @@ +use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{ExprF, X}; +use dhall_syntax::{Const, ExprF, X}; -use crate::core::context::NormalizationContext; +use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; -use crate::phase::{Type, Typed}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -42,7 +45,16 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub struct TypeThunk(Typed); +pub enum TypeThunk { + // Any value, along with (optionally) its type + Untyped(Thunk), + Typed(Thunk, Box), + // One of the base higher-kinded typed. + // Used to avoid storing the same tower ot Type->Kind->Sort + // over and over again. Also enables having Sort as a type + // even though it doesn't itself have a type. + Const(Const), +} impl ThunkInternal { fn into_thunk(self) -> Thunk { @@ -190,39 +202,94 @@ impl TypeThunk { } pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk(Typed::from_thunk_untyped(th)) + TypeThunk::from_thunk_untyped(th) } pub fn from_type(t: Type) -> TypeThunk { - TypeThunk(t) + t.into_typethunk() } - pub fn normalize_mut(&mut self) { - self.0.normalize_mut() + pub fn normalize_nf(&self) -> Value { + match self { + TypeThunk::Const(c) => Value::Const(*c), + TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + thunk.normalize_nf().clone() + } + } } - pub fn normalize_nf(&self) -> Value { - self.0.to_value().normalize() + pub fn to_typed(&self) -> Typed { + self.clone().into_typed() } - pub fn to_value(&self) -> Value { - self.0.to_value() + pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub fn to_thunk(&self) -> Thunk { - self.0.to_thunk() + pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + TypeThunk::Typed(th, Box::new(t)) + } + pub fn from_thunk_untyped(th: Thunk) -> Self { + TypeThunk::Untyped(th) + } + pub fn from_const(c: Const) -> Self { + TypeThunk::Const(c) + } + pub fn from_value_untyped(v: Value) -> Self { + TypeThunk::from_thunk_untyped(Thunk::from_value(v)) } + // TODO: Avoid cloning if possible + pub fn to_value(&self) -> Value { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), + TypeThunk::Const(c) => Value::Const(*c), + } + } + pub fn to_expr(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr() + } + pub fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr_maybe_alpha(true) + } + pub fn to_thunk(&self) -> Thunk { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), + TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + } + } pub fn to_type(&self) -> Type { - self.0.to_type() + self.clone().into_typed().into_type() + } + pub fn into_typed(self) -> Typed { + Typed::from_typethunk(self) + } + pub fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_value() { + Value::Const(c) => Some(*c), + _ => None, + } } - pub fn to_typed(&self) -> Typed { - self.0.clone() + pub fn normalize_mut(&mut self) { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + th.normalize_mut() + } + TypeThunk::Const(_) => {} + } } - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + pub fn get_type(&self) -> Result, TypeError> { + match self { + TypeThunk::Untyped(_) => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, + )), + TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + } } } @@ -254,7 +321,14 @@ impl Shift for ThunkInternal { impl Shift for TypeThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypeThunk(self.0.shift(delta, var)?)) + Some(match self { + TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.shift(delta, var)?, + Box::new(t.shift(delta, var)?), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + }) } } @@ -293,7 +367,16 @@ impl Subst for ThunkInternal { impl Subst for TypeThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypeThunk(self.0.subst_shift(var, val)) + match self { + TypeThunk::Untyped(th) => { + TypeThunk::Untyped(th.subst_shift(var, val)) + } + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.subst_shift(var, val), + Box::new(t.subst_shift(var, val)), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + } } } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index ccedff2..0b05227 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -4,14 +4,12 @@ use std::path::Path; use dhall_syntax::{Const, Import, Span, SubExpr, X}; -use crate::core::context::TypecheckContext; -use crate::core::thunk::Thunk; +use crate::core::thunk::{Thunk, TypeThunk}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{EncodeError, Error, ImportError, TypeError, TypeMessage}; +use crate::error::{EncodeError, Error, ImportError, TypeError}; use resolve::ImportRoot; -use typecheck::type_of_const; pub(crate) mod binary; pub(crate) mod normalize; @@ -33,16 +31,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub enum Typed { - // Any value, along with (optionally) its type - Untyped(Thunk), - Typed(Thunk, Box), - // One of the base higher-kinded typed. - // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a type - // even though it doesn't itself have a type. - Const(Const), -} +pub struct Typed(TypeThunk); /// A normalized expression. /// @@ -105,83 +94,63 @@ impl Typed { /// /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. - pub fn normalize(self) -> Normalized { - match &self { - Typed::Const(_) => {} - Typed::Untyped(thunk) | Typed::Typed(thunk, _) => { - thunk.normalize_nf(); - } - } + pub fn normalize(mut self) -> Normalized { + self.normalize_mut(); Normalized(self) } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - Typed::Typed(th, Box::new(t)) + Typed(TypeThunk::from_thunk_and_type(th, t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - Typed::Untyped(th) + Typed(TypeThunk::from_thunk_untyped(th)) } pub fn from_const(c: Const) -> Self { - Typed::Const(c) + Typed(TypeThunk::from_const(c)) } pub fn from_value_untyped(v: Value) -> Self { - Typed::from_thunk_untyped(Thunk::from_value(v)) + Typed(TypeThunk::from_value_untyped(v)) + } + pub fn from_typethunk(th: TypeThunk) -> Self { + Typed(th) } - // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.to_value(), - Typed::Const(c) => Value::Const(*c), - } + self.0.to_value() } pub fn to_expr(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr() + self.0.to_expr() } pub fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr_maybe_alpha(true) + self.0.to_expr_alpha() } pub fn to_thunk(&self) -> Thunk { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.clone(), - Typed::Const(c) => Thunk::from_value(Value::Const(*c)), - } + self.0.to_thunk() } // Deprecated pub fn to_type(&self) -> Type { - self.clone().into_type() + self.clone() } // Deprecated pub fn into_type(self) -> Type { self } + pub fn into_typethunk(self) -> TypeThunk { + self.0 + } pub fn to_normalized(&self) -> Normalized { self.clone().normalize() } pub fn as_const(&self) -> Option { - // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), - _ => None, - } + self.0.as_const() } pub fn normalize_mut(&mut self) { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.normalize_mut(), - Typed::Const(_) => {} - } + self.0.normalize_mut() } pub fn get_type(&self) -> Result, TypeError> { - match self { - Typed::Untyped(_) => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - Typed::Typed(_, t) => Ok(Cow::Borrowed(t)), - Typed::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), - } + self.0.get_type() } } @@ -208,14 +177,7 @@ impl Normalized { impl Shift for Typed { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - Typed::Untyped(th) => Typed::Untyped(th.shift(delta, var)?), - Typed::Typed(th, t) => Typed::Typed( - th.shift(delta, var)?, - Box::new(t.shift(delta, var)?), - ), - Typed::Const(c) => Typed::Const(*c), - }) + Some(Typed(self.0.shift(delta, var)?)) } } @@ -227,14 +189,7 @@ impl Shift for Normalized { impl Subst for Typed { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - Typed::Untyped(th) => Typed::Untyped(th.subst_shift(var, val)), - Typed::Typed(th, t) => Typed::Typed( - th.subst_shift(var, val), - Box::new(t.subst_shift(var, val)), - ), - Typed::Const(c) => Typed::Const(*c), - } + Typed(self.0.subst_shift(var, val)) } } -- cgit v1.3.1 From fb0120dffe8e9552c3da7b994ad850f66dc612a3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:21:54 +0200 Subject: s/TypeThunk/TypedThunk/g --- dhall/src/core/thunk.rs | 68 +++++++++++++++++++++++--------------------- dhall/src/core/value.rs | 24 ++++++++-------- dhall/src/phase/mod.rs | 16 +++++------ dhall/src/phase/normalize.rs | 34 +++++++++++----------- dhall/src/phase/typecheck.rs | 40 +++++++++++++++----------- serde_dhall/src/lib.rs | 6 ++-- 6 files changed, 99 insertions(+), 89 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 740ecbc..38c54f7 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -45,7 +45,7 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub enum TypeThunk { +pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), @@ -196,23 +196,23 @@ impl Thunk { } } -impl TypeThunk { - pub fn from_value(v: Value) -> TypeThunk { - TypeThunk::from_thunk(Thunk::from_value(v)) +impl TypedThunk { + pub fn from_value(v: Value) -> TypedThunk { + TypedThunk::from_thunk(Thunk::from_value(v)) } - pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk::from_thunk_untyped(th) + pub fn from_thunk(th: Thunk) -> TypedThunk { + TypedThunk::from_thunk_untyped(th) } - pub fn from_type(t: Type) -> TypeThunk { + pub fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } pub fn normalize_nf(&self) -> Value { match self { - TypeThunk::Const(c) => Value::Const(*c), - TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } } @@ -227,23 +227,23 @@ impl TypeThunk { } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - TypeThunk::Typed(th, Box::new(t)) + TypedThunk::Typed(th, Box::new(t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - TypeThunk::Untyped(th) + TypedThunk::Untyped(th) } pub fn from_const(c: Const) -> Self { - TypeThunk::Const(c) + TypedThunk::Const(c) } pub fn from_value_untyped(v: Value) -> Self { - TypeThunk::from_thunk_untyped(Thunk::from_value(v)) + TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), - TypeThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), + TypedThunk::Const(c) => Value::Const(*c), } } pub fn to_expr(&self) -> NormalizedSubExpr { @@ -254,8 +254,8 @@ impl TypeThunk { } pub fn to_thunk(&self) -> Thunk { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), - TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), + TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), } } pub fn to_type(&self) -> Type { @@ -274,21 +274,21 @@ impl TypeThunk { pub fn normalize_mut(&mut self) { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.normalize_mut() } - TypeThunk::Const(_) => {} + TypedThunk::Const(_) => {} } } pub fn get_type(&self) -> Result, TypeError> { match self { - TypeThunk::Untyped(_) => Err(TypeError::new( + TypedThunk::Untyped(_) => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, )), - TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), - TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } } @@ -319,15 +319,17 @@ impl Shift for ThunkInternal { } } -impl Shift for TypeThunk { +impl Shift for TypedThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.shift(delta, var)?) + } + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.shift(delta, var)?, Box::new(t.shift(delta, var)?), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), }) } } @@ -365,17 +367,17 @@ impl Subst for ThunkInternal { } } -impl Subst for TypeThunk { +impl Subst for TypedThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - TypeThunk::Untyped(th) => { - TypeThunk::Untyped(th.subst_shift(var, val)) + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.subst_shift(var, val)) } - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.subst_shift(var, val), Box::new(t.subst_shift(var, val)), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), } } } @@ -387,9 +389,9 @@ impl std::cmp::PartialEq for Thunk { } impl std::cmp::Eq for Thunk {} -impl std::cmp::PartialEq for TypeThunk { +impl std::cmp::PartialEq for TypedThunk { fn eq(&self, other: &Self) -> bool { self.to_value() == other.to_value() } } -impl std::cmp::Eq for TypeThunk {} +impl std::cmp::Eq for TypedThunk {} diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0b68bf6..8486d6e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, X, }; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, @@ -26,15 +26,15 @@ use crate::phase::Typed; #[derive(Debug, Clone, PartialEq, Eq)] pub enum Value { /// Closures - Lam(AlphaLabel, TypeThunk, Thunk), - Pi(AlphaLabel, TypeThunk, TypeThunk), + Lam(AlphaLabel, TypedThunk, Thunk), + Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypeThunk), + OptionalSomeClosure(TypedThunk), /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypeThunk, Option), + ListConsClosure(TypedThunk, Option), /// `λ(x : Natural) -> x + 1` NaturalSuccClosure, @@ -44,20 +44,20 @@ pub enum Value { NaturalLit(Natural), IntegerLit(Integer), DoubleLit(NaiveDouble), - EmptyOptionalLit(TypeThunk), + EmptyOptionalLit(TypedThunk), NEOptionalLit(Thunk), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypeThunk), + EmptyListLit(TypedThunk), NEListLit(Vec), RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Thunk, HashMap>), // Invariant: this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), - Equivalence(TypeThunk, TypeThunk), + Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 0b05227..27a6901 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, Import, Span, SubExpr, X}; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; @@ -31,7 +31,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TypeThunk); +pub struct Typed(TypedThunk); /// A normalized expression. /// @@ -100,18 +100,18 @@ impl Typed { } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - Typed(TypeThunk::from_thunk_and_type(th, t)) + Typed(TypedThunk::from_thunk_and_type(th, t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - Typed(TypeThunk::from_thunk_untyped(th)) + Typed(TypedThunk::from_thunk_untyped(th)) } pub fn from_const(c: Const) -> Self { - Typed(TypeThunk::from_const(c)) + Typed(TypedThunk::from_const(c)) } pub fn from_value_untyped(v: Value) -> Self { - Typed(TypeThunk::from_value_untyped(v)) + Typed(TypedThunk::from_value_untyped(v)) } - pub fn from_typethunk(th: TypeThunk) -> Self { + pub fn from_typethunk(th: TypedThunk) -> Self { Typed(th) } @@ -135,7 +135,7 @@ impl Typed { pub fn into_type(self) -> Type { self } - pub fn into_typethunk(self) -> TypeThunk { + pub fn into_typethunk(self) -> TypedThunk { self.0 } pub fn to_normalized(&self) -> Normalized { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 405677a..644f98c 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ }; use crate::core::context::NormalizationContext; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::Subst; use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed}; @@ -22,7 +22,7 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { // 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(TypeThunk::from_thunk(t.clone())))) + Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone())))) } (NaturalIsZero, [n, r..]) => match &*n.as_value() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), @@ -144,10 +144,10 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypeThunk::from_value(Value::from_builtin(Natural)), + TypedThunk::from_value(Value::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypeThunk::from_value(RecordType(kts))))) + Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts))))) } NEListLit(xs) => { let xs = xs @@ -179,10 +179,10 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { r, f.app_val(Value::from_builtin(List).app_thunk(t.clone())) .app_val(ListConsClosure( - TypeThunk::from_thunk(t.clone()), + TypedThunk::from_thunk(t.clone()), None, )) - .app_val(EmptyListLit(TypeThunk::from_thunk(t.clone()))), + .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))), )), }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() { @@ -213,10 +213,10 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { _ => Ok(( r, f.app_val(Value::from_builtin(Optional).app_thunk(t.clone())) - .app_val(OptionalSomeClosure(TypeThunk::from_thunk( + .app_val(OptionalSomeClosure(TypedThunk::from_thunk( t.clone(), ))) - .app_val(EmptyOptionalLit(TypeThunk::from_thunk( + .app_val(EmptyOptionalLit(TypedThunk::from_thunk( t.clone(), ))), )), @@ -618,7 +618,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypeThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( + TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( RecursiveRecordTypeMerge, v1.to_thunk(), v2.to_thunk(), @@ -628,8 +628,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (Equivalence, _, _) => Ret::Value(Value::Equivalence( - TypeThunk::from_thunk(x.clone()), - TypeThunk::from_thunk(y.clone()), + TypedThunk::from_thunk(x.clone()), + TypedThunk::from_thunk(y.clone()), )), _ => return None, @@ -649,12 +649,12 @@ pub fn normalize_one_layer(expr: ExprF) -> Value { ExprF::Annot(x, _) => Ret::Thunk(x), ExprF::Assert(_) => Ret::Expr(expr), ExprF::Lam(x, t, e) => { - Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e)) + Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e)) } ExprF::Pi(x, t, e) => Ret::Value(Pi( x.into(), - TypeThunk::from_thunk(t), - TypeThunk::from_thunk(e), + TypedThunk::from_thunk(t), + TypedThunk::from_thunk(e), )), ExprF::Let(x, _, v, b) => { let v = Typed::from_thunk_untyped(v); @@ -673,7 +673,7 @@ pub fn normalize_one_layer(expr: ExprF) -> Value { let t_borrow = t.as_value(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::Value(EmptyListLit(TypeThunk::from_thunk( + Ret::Value(EmptyListLit(TypedThunk::from_thunk( args[0].clone(), ))) } @@ -691,12 +691,12 @@ pub fn normalize_one_layer(expr: ExprF) -> Value { } ExprF::RecordType(kts) => Ret::Value(RecordType( kts.into_iter() - .map(|(k, t)| (k, TypeThunk::from_thunk(t))) + .map(|(k, t)| (k, TypedThunk::from_thunk(t))) .collect(), )), ExprF::UnionType(kts) => Ret::Value(UnionType( kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t)))) + .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t)))) .collect(), )), ExprF::TextLit(elts) => { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 299997a..a19e1ca 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ }; use crate::core::context::{NormalizationContext, TypecheckContext}; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -44,8 +44,12 @@ fn tck_pi_type( let k = function_check(ka, kb); Ok(Typed::from_thunk_and_type( - Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te)) - .into_thunk(), + Value::Pi( + x.into(), + TypedThunk::from_type(tx), + TypedThunk::from_type(te), + ) + .into_thunk(), Type::from_const(k), )) } @@ -77,7 +81,7 @@ fn tck_record_type( return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } Entry::Vacant(_) => { - entry.or_insert_with(|| TypeThunk::from_type(t.clone())) + entry.or_insert_with(|| TypedThunk::from_type(t.clone())) } }; } @@ -119,7 +123,7 @@ fn tck_union_type( return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypeThunk::from_type(t.clone())) + t.as_ref().map(|t| TypedThunk::from_type(t.clone())) }), }; } @@ -334,7 +338,7 @@ fn type_with( let b = type_with(&ctx2, b.clone())?; let v = Value::Lam( x.clone().into(), - TypeThunk::from_type(tx.clone()), + TypedThunk::from_type(tx.clone()), b.to_thunk(), ); let tb = b.get_type()?.into_owned(); @@ -658,8 +662,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::outer_join; @@ -667,8 +671,8 @@ fn type_last_layer( // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. let combine = |k: &Label, - inner_l: &TypeThunk, - inner_r: &TypeThunk| + inner_l: &TypedThunk, + inner_r: &TypedThunk| -> Result { match (inner_l.to_value(), inner_r.to_value()) { ( @@ -686,7 +690,9 @@ fn type_last_layer( let kts: HashMap> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r), + |k: &Label, l: &TypedThunk, r: &TypedThunk| { + combine(k, l, r) + }, &kts_l, &kts_r, ); @@ -729,8 +735,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::intersection_with_key; @@ -738,8 +744,8 @@ fn type_last_layer( // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. let combine = |k: &Label, - kts_l_inner: &TypeThunk, - kts_r_inner: &TypeThunk| + kts_l_inner: &TypedThunk, + kts_r_inner: &TypedThunk| -> Result { match (kts_l_inner.to_value(), kts_r_inner.to_value()) { ( @@ -755,7 +761,9 @@ fn type_last_layer( }; let kts = intersection_with_key( - |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r), + |k: &Label, l: &TypedThunk, r: &TypedThunk| { + combine(k, l, r) + }, &kts_l, &kts_r, ); diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 19aabec..14d8b47 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -124,7 +124,7 @@ pub use value::Value; // A Dhall value. pub mod value { - use dhall::core::thunk::{Thunk, TypeThunk}; + use dhall::core::thunk::{Thunk, TypedThunk}; use dhall::core::value::Value as DhallValue; use dhall::phase::{NormalizedSubExpr, Parsed, Type, Typed}; use dhall_syntax::Builtin; @@ -185,7 +185,7 @@ pub mod value { ) -> Self { Self::from_dhall_value(DhallValue::RecordType( kts.map(|(k, t)| { - (k.into(), TypeThunk::from_thunk(t.to_thunk())) + (k.into(), TypedThunk::from_thunk(t.to_thunk())) }) .collect(), )) @@ -196,7 +196,7 @@ pub mod value { ) -> Self { Self::from_dhall_value(DhallValue::UnionType( kts.map(|(k, t)| { - (k.into(), t.map(|t| TypeThunk::from_thunk(t.to_thunk()))) + (k.into(), t.map(|t| TypedThunk::from_thunk(t.to_thunk()))) }) .collect(), )) -- cgit v1.3.1 From cbd62bb57bcc94e0133c57437488a5af22a0b1c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:34:38 +0200 Subject: Typos --- dhall/src/core/thunk.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 38c54f7..c18014e 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -49,9 +49,9 @@ pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), - // One of the base higher-kinded typed. + // One of the base higher-kinded types. // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a type + // over and over again. Also enables having Sort as a value // even though it doesn't itself have a type. Const(Const), } -- cgit v1.3.1 From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 20:54:15 +0200 Subject: Stop tracking the absence of Embed values at the type level --- dhall/src/core/thunk.rs | 12 ++++++------ dhall/src/core/value.rs | 10 +++++----- dhall/src/phase/mod.rs | 4 ++-- dhall/src/phase/normalize.rs | 21 +++++++++++---------- dhall/src/phase/typecheck.rs | 11 ++++------- dhall_syntax/src/core/context.rs | 2 +- dhall_syntax/src/core/expr.rs | 16 ++-------------- dhall_syntax/src/core/visitor.rs | 15 +-------------- dhall_syntax/src/printer.rs | 6 ------ 9 files changed, 32 insertions(+), 65 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index c18014e..4d193f9 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF, X}; +use dhall_syntax::{Const, ExprF}; use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; @@ -12,7 +12,7 @@ use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; use crate::phase::typecheck::type_of_const; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -30,7 +30,7 @@ enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. - PartialExpr(ExprF), + PartialExpr(ExprF), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized Value(Marker, Value), @@ -123,7 +123,7 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF) -> Thunk { + pub fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } @@ -309,7 +309,7 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +356,7 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8486d6e..88d7a20 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, X, + NaiveDouble, Natural, }; use crate::core::thunk::{Thunk, TypedThunk}; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; -use crate::phase::Typed; +use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the @@ -59,7 +59,7 @@ pub enum Value { TextLit(Vec>), Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } impl Value { @@ -475,7 +475,7 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +500,7 @@ impl Subst for Value { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, )) } // Retry normalizing since substituting may allow progress diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 8c93889..7364949 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::fmt::Display; use std::path::Path; -use dhall_syntax::{Const, Import, SubExpr, X}; +use dhall_syntax::{Const, Import, SubExpr}; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; @@ -20,7 +20,7 @@ pub(crate) mod typecheck; pub type ParsedSubExpr = SubExpr; pub type DecodedSubExpr = SubExpr; pub type ResolvedSubExpr = SubExpr; -pub type NormalizedSubExpr = SubExpr; +pub type NormalizedSubExpr = SubExpr; #[derive(Debug, Clone)] pub struct Parsed(ParsedSubExpr, ImportRoot); diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 644f98c..f1045a5 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -2,14 +2,14 @@ use std::collections::HashMap; use dhall_syntax::{ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, - NaiveDouble, X, + NaiveDouble, }; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::Subst; -use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; pub type InputSubExpr = ResolvedSubExpr; pub type OutputSubExpr = NormalizedSubExpr; @@ -86,7 +86,7 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { // Empty string literal. [] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = + let txt: InterpolatedText = std::iter::empty().collect(); let s = txt.to_string(); Ok(( @@ -98,10 +98,11 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { // interpolations, there is a single Text item) in the literal. [InterpolatedTextContents::Text(s)] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = std::iter::once( - InterpolatedTextContents::Text(s.clone()), - ) - .collect(); + let txt: InterpolatedText = + std::iter::once(InterpolatedTextContents::Text( + s.clone(), + )) + .collect(); let s = txt.to_string(); Ok(( r, @@ -376,7 +377,7 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { } // Thunk subexpressions - let expr: ExprF = + let expr: ExprF = expr.as_ref().map_ref_with_special_handling_of_binders( |e| Thunk::new(ctx.clone(), e.clone()), |x, e| Thunk::new(ctx.skip(x), e.clone()), @@ -391,7 +392,7 @@ enum Ret<'a> { Value(Value), Thunk(Thunk), ThunkRef(&'a Thunk), - Expr(ExprF), + Expr(ExprF), } /// Performs an intersection of two HashMaps. @@ -636,7 +637,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { }) } -pub fn normalize_one_layer(expr: ExprF) -> Value { +pub fn normalize_one_layer(expr: ExprF) -> Value { use Value::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index ecf9793..96ff246 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -2,7 +2,6 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr, - X, }; use crate::core::context::{NormalizationContext, TypecheckContext}; @@ -214,7 +213,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr { +fn type_of_builtin(b: Builtin) -> Expr { use dhall_syntax::Builtin::*; match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -398,7 +397,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -598,9 +597,7 @@ fn type_last_layer( } } Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => { - Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?)) - } + Builtin(b) => Ok(RetTypeOnly(mktype(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)?)), @@ -1016,7 +1013,7 @@ pub fn typecheck(e: Resolved) -> Result { pub fn typecheck_with(e: Resolved, ty: &Type) -> Result { let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr().absurd(); + let ty: SubExpr<_> = ty.to_expr(); type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } pub fn skip_typecheck(e: Resolved) -> Typed { diff --git a/dhall_syntax/src/core/context.rs b/dhall_syntax/src/core/context.rs index eeec121..6844baa 100644 --- a/dhall_syntax/src/core/context.rs +++ b/dhall_syntax/src/core/context.rs @@ -4,7 +4,7 @@ use std::hash::Hash; /// A `(Context a)` associates `Text` labels with values of type `a` /// -/// The `Context` is used for type-checking when `(a = Expr X)` +/// The `Context` is used for type-checking when `(a = Expr)` /// /// * You create a `Context` using `empty` and `insert` /// * You transform a `Context` using `fmap` diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index 0cbece3..e08d816 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -10,9 +10,9 @@ pub type Double = NaiveDouble; /// An empty type #[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum X {} +pub enum Void {} -pub fn trivial_result(x: Result) -> T { +pub fn trivial_result(x: Result) -> T { match x { Ok(x) => x, Err(e) => match e {}, @@ -351,12 +351,6 @@ impl Expr { } } -impl Expr { - pub fn absurd(&self) -> Expr { - self.visit(&mut visitor::AbsurdVisitor) - } -} - impl SubExpr { pub fn as_ref(&self) -> &Expr { &self.0.as_ref().0 @@ -416,12 +410,6 @@ impl SubExpr { } } -impl SubExpr { - pub fn absurd(&self) -> SubExpr { - SubExpr::from_expr_no_span(self.as_ref().absurd()) - } -} - impl Clone for SubExpr { fn clone(&self) -> Self { SubExpr(Rc::clone(&self.0)) diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs index 50ec68a..e39e95b 100644 --- a/dhall_syntax/src/core/visitor.rs +++ b/dhall_syntax/src/core/visitor.rs @@ -243,7 +243,7 @@ impl<'a, T, SE1, SE2, E1, E2> ExprFFallibleVisitor<'a, SE1, SE2, E1, E2> where T: ExprFInFallibleVisitor<'a, SE1, SE2, E1, E2>, { - type Error = X; + type Error = Void; fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result { Ok(self.0.visit_subexpr(subexpr)) @@ -379,16 +379,3 @@ where (self.0)(embed) } } - -pub struct AbsurdVisitor; - -impl<'a, 'b, E> ExprFInFallibleVisitor<'a, SubExpr, SubExpr, X, E> - for &'b mut AbsurdVisitor -{ - fn visit_subexpr(&mut self, subexpr: &'a SubExpr) -> SubExpr { - SubExpr::from_expr_no_span(subexpr.as_ref().visit(&mut **self)) - } - fn visit_embed(self, embed: &'a X) -> E { - match *embed {} - } -} diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index 95eafe5..25d4ca8 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -491,9 +491,3 @@ impl Display for V