diff options
author | Nadrieril | 2019-05-04 14:19:43 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-04 14:19:43 +0200 |
commit | b6f57069b75febf1d312a98efcd6544c9db2fe59 (patch) | |
tree | d787d82502e4b62c01937c459295da3dda8ba62d /dhall/src | |
parent | 68d1e5f42e3cf4cf132d1cd7d1d1775e48cf2a43 (diff) |
Remove dummy lifetimes
Diffstat (limited to '')
-rw-r--r-- | dhall/src/expr.rs | 100 | ||||
-rw-r--r-- | dhall/src/imports.rs | 86 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 50 | ||||
-rw-r--r-- | dhall/src/traits/deserialize.rs | 10 | ||||
-rw-r--r-- | dhall/src/traits/dynamic_type.rs | 16 | ||||
-rw-r--r-- | dhall/src/traits/static_type.rs | 40 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 167 |
7 files changed, 202 insertions, 267 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index b0b6215..db426ce 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -1,19 +1,18 @@ use crate::imports::ImportRoot; use crate::normalize::{Thunk, Value}; use dhall_syntax::*; -use std::marker::PhantomData; macro_rules! derive_other_traits { ($ty:ident) => { - impl<'a> std::cmp::PartialEq for $ty<'a> { + impl std::cmp::PartialEq for $ty { fn eq(&self, other: &Self) -> bool { self.0 == other.0 } } - impl<'a> std::cmp::Eq for $ty<'a> {} + impl std::cmp::Eq for $ty {} - impl<'a> std::fmt::Display for $ty<'a> { + impl std::fmt::Display for $ty { fn fmt( &self, f: &mut std::fmt::Formatter, @@ -25,41 +24,33 @@ macro_rules! derive_other_traits { } #[derive(Debug, Clone)] -pub(crate) struct Parsed<'a>( - pub(crate) SubExpr<Span<'a>, Import>, +pub(crate) struct Parsed( + pub(crate) SubExpr<Span, Import>, pub(crate) ImportRoot, ); derive_other_traits!(Parsed); #[derive(Debug, Clone)] -pub(crate) struct Resolved<'a>( - pub(crate) SubExpr<Span<'a>, Normalized<'static>>, -); +pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>); derive_other_traits!(Resolved); pub(crate) use self::typed::TypedInternal; #[derive(Debug, Clone)] -pub(crate) struct Typed<'a>( - pub(crate) TypedInternal, - pub(crate) PhantomData<&'a ()>, -); +pub(crate) struct Typed(pub(crate) TypedInternal); #[derive(Debug, Clone)] -pub(crate) struct Normalized<'a>( - pub(crate) TypedInternal, - pub(crate) PhantomData<&'a ()>, -); +pub(crate) struct Normalized(pub(crate) TypedInternal); -impl<'a> std::cmp::PartialEq for Normalized<'a> { +impl std::cmp::PartialEq for Normalized { fn eq(&self, other: &Self) -> bool { self.to_expr() == other.to_expr() } } -impl<'a> std::cmp::Eq for Normalized<'a> {} +impl std::cmp::Eq for Normalized {} -impl<'a> std::fmt::Display for Normalized<'a> { +impl std::fmt::Display for Normalized { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) } @@ -73,18 +64,17 @@ mod typed { }; use dhall_syntax::{Const, Label, SubExpr, V, X}; use std::borrow::Cow; - use std::marker::PhantomData; #[derive(Debug, Clone)] pub(crate) enum TypedInternal { // The `Sort` higher-kinded type doesn't have a type Sort, // Any other value, along with its type - Value(Thunk, Option<Type<'static>>), + Value(Thunk, Option<Type>), } impl TypedInternal { - pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { TypedInternal::Value(th, Some(t)) } @@ -113,22 +103,19 @@ mod typed { } } - pub(crate) fn to_type(&self) -> Type<'static> { + pub(crate) fn to_type(&self) -> Type { match self { TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)), TypedInternal::Value(th, _) => match &*th.as_value() { Value::Const(c) => Type(TypeInternal::Const(*c)), - _ => Type(TypeInternal::Typed(Box::new(Typed( - self.clone(), - PhantomData, - )))), + _ => { + Type(TypeInternal::Typed(Box::new(Typed(self.clone())))) + } }, } } - pub(crate) fn get_type( - &self, - ) -> Result<Cow<'_, Type<'static>>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { match self { TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)), TypedInternal::Value(_, None) => Err(TypeError::new( @@ -152,11 +139,7 @@ mod typed { } } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { TypedInternal::Value(th, t) => TypedInternal::Value( th.subst_shift(var, val), @@ -175,10 +158,7 @@ mod typed { /// /// For a more general notion of "type", see [Type]. #[derive(Debug, Clone)] -pub struct SimpleType<'a>( - pub(crate) SubExpr<X, X>, - pub(crate) PhantomData<&'a ()>, -); +pub struct SimpleType(pub(crate) SubExpr<X, X>); derive_other_traits!(SimpleType); pub(crate) use crate::typecheck::TypeInternal; @@ -188,9 +168,9 @@ pub(crate) use crate::typecheck::TypeInternal; /// This includes [SimpleType]s but also higher-kinded expressions like /// `Type`, `Kind` and `{ x: Type }`. #[derive(Debug, Clone, PartialEq, Eq)] -pub struct Type<'a>(pub(crate) TypeInternal<'a>); +pub struct Type(pub(crate) TypeInternal); -impl<'a> std::fmt::Display for Type<'a> { +impl std::fmt::Display for Type { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_normalized().fmt(f) } @@ -198,31 +178,31 @@ impl<'a> std::fmt::Display for Type<'a> { // Exposed for the macros #[doc(hidden)] -impl<'a> From<SimpleType<'a>> for SubExpr<X, X> { - fn from(x: SimpleType<'a>) -> SubExpr<X, X> { +impl From<SimpleType> for SubExpr<X, X> { + fn from(x: SimpleType) -> SubExpr<X, X> { x.0 } } // Exposed for the macros #[doc(hidden)] -impl<'a> From<SubExpr<X, X>> for SimpleType<'a> { - fn from(x: SubExpr<X, X>) -> SimpleType<'a> { - SimpleType(x, PhantomData) +impl From<SubExpr<X, X>> for SimpleType { + fn from(x: SubExpr<X, X>) -> SimpleType { + SimpleType(x) } } // Exposed for the macros #[doc(hidden)] -impl<'a> From<Normalized<'a>> for Typed<'a> { - fn from(x: Normalized<'a>) -> Typed<'a> { - Typed(x.0, x.1) +impl From<Normalized> for Typed { + fn from(x: Normalized) -> Typed { + Typed(x.0) } } -impl<'a> Normalized<'a> { - pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { - Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData) +impl Normalized { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + Normalized(TypedInternal::from_thunk_and_type(th, t)) } // Deprecated pub(crate) fn as_expr(&self) -> SubExpr<X, X> { @@ -235,19 +215,19 @@ impl<'a> Normalized<'a> { self.0.to_value() } #[allow(dead_code)] - pub(crate) fn unnote<'b>(self) -> Normalized<'b> { - Normalized(self.0, PhantomData) + pub(crate) fn unnote(self) -> Normalized { + Normalized(self.0) } } -impl<'a> Typed<'a> { - pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { - Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData) +impl Typed { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + Typed(TypedInternal::from_thunk_and_type(th, t)) } pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - Typed(TypedInternal::from_thunk_untyped(th), PhantomData) + Typed(TypedInternal::from_thunk_untyped(th)) } pub(crate) fn const_sort() -> Self { - Typed(TypedInternal::Sort, PhantomData) + Typed(TypedInternal::Sort) } } diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index 306d4e6..87642a2 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -20,7 +20,7 @@ pub enum ImportRoot { LocalDir(PathBuf), } -type ImportCache = HashMap<Import, Normalized<'static>>; +type ImportCache = HashMap<Import, Normalized>; type ImportStack = Vec<Import>; @@ -29,7 +29,7 @@ fn resolve_import( root: &ImportRoot, import_cache: &mut ImportCache, import_stack: &ImportStack, -) -> Result<Normalized<'static>, ImportError> { +) -> Result<Normalized, ImportError> { use self::ImportRoot::*; use dhall_syntax::FilePrefix::*; use dhall_syntax::ImportLocation::*; @@ -56,7 +56,7 @@ fn load_import( f: &Path, import_cache: &mut ImportCache, import_stack: &ImportStack, -) -> Result<Normalized<'static>, Error> { +) -> Result<Normalized, Error> { Ok( do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? .typecheck()? @@ -64,57 +64,51 @@ fn load_import( ) } -fn do_resolve_expr<'a>( - Parsed(expr, root): Parsed<'a>, +fn do_resolve_expr( + Parsed(expr, root): Parsed, import_cache: &mut ImportCache, import_stack: &ImportStack, -) -> Result<Resolved<'a>, ImportError> { - let resolve = - |import: &Import| -> Result<Normalized<'static>, ImportError> { - if import_stack.contains(import) { - return Err(ImportError::ImportCycle( - import_stack.clone(), - import.clone(), - )); - } - match import_cache.get(import) { - Some(expr) => Ok(expr.clone()), - None => { - // Copy the import stack and push the current import - let mut import_stack = import_stack.clone(); - import_stack.push(import.clone()); - - // Resolve the import recursively - let expr = resolve_import( - import, - &root, - import_cache, - &import_stack, - )?; - - // Add the import to the cache - import_cache.insert(import.clone(), expr.clone()); - Ok(expr) - } +) -> Result<Resolved, ImportError> { + let resolve = |import: &Import| -> Result<Normalized, ImportError> { + if import_stack.contains(import) { + return Err(ImportError::ImportCycle( + import_stack.clone(), + import.clone(), + )); + } + match import_cache.get(import) { + Some(expr) => Ok(expr.clone()), + None => { + // Copy the import stack and push the current import + let mut import_stack = import_stack.clone(); + import_stack.push(import.clone()); + + // Resolve the import recursively + let expr = + resolve_import(import, &root, import_cache, &import_stack)?; + + // Add the import to the cache + import_cache.insert(import.clone(), expr.clone()); + Ok(expr) } - }; + } + }; let expr = expr.traverse_embed(resolve)?; Ok(Resolved(expr)) } fn skip_resolve_expr( - Parsed(expr, _root): Parsed<'_>, -) -> Result<Resolved<'_>, ImportError> { - let resolve = - |import: &Import| -> Result<Normalized<'static>, ImportError> { - Err(ImportError::UnexpectedImport(import.clone())) - }; + Parsed(expr, _root): Parsed, +) -> Result<Resolved, ImportError> { + let resolve = |import: &Import| -> Result<Normalized, ImportError> { + Err(ImportError::UnexpectedImport(import.clone())) + }; let expr = expr.traverse_embed(resolve)?; Ok(Resolved(expr)) } -impl<'a> Parsed<'a> { - pub fn parse_file(f: &Path) -> Result<Parsed<'a>, Error> { +impl Parsed { + pub fn parse_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = String::new(); File::open(f)?.read_to_string(&mut buffer)?; let expr = parse_expr(&*buffer)?; @@ -122,14 +116,14 @@ impl<'a> Parsed<'a> { Ok(Parsed(expr.unnote().note_absurd(), root)) } - pub fn parse_str(s: &'a str) -> Result<Parsed<'a>, Error> { + pub fn parse_str(s: &str) -> Result<Parsed, Error> { let expr = parse_expr(s)?; let root = ImportRoot::LocalDir(std::env::current_dir()?); Ok(Parsed(expr, root)) } #[allow(dead_code)] - pub fn parse_binary_file(f: &Path) -> Result<Parsed<'a>, Error> { + pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = Vec::new(); File::open(f)?.read_to_end(&mut buffer)?; let expr = crate::binary::decode(&buffer)?; @@ -137,12 +131,12 @@ impl<'a> Parsed<'a> { Ok(Parsed(expr.note_absurd(), root)) } - pub fn resolve(self) -> Result<Resolved<'a>, ImportError> { + pub fn resolve(self) -> Result<Resolved, ImportError> { crate::imports::do_resolve_expr(self, &mut HashMap::new(), &Vec::new()) } #[allow(dead_code)] - pub fn skip_resolve(self) -> Result<Resolved<'a>, ImportError> { + pub fn skip_resolve(self) -> Result<Resolved, ImportError> { crate::imports::skip_resolve_expr(self) } } diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index ab9812d..4636859 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -11,10 +11,10 @@ use dhall_syntax::{ use crate::expr::{Normalized, Type, Typed, TypedInternal}; -type InputSubExpr = SubExpr<X, Normalized<'static>>; +type InputSubExpr = SubExpr<X, Normalized>; type OutputSubExpr = SubExpr<X, X>; -impl<'a> Typed<'a> { +impl Typed { /// Reduce an expression to its normal form, performing beta reduction /// /// `normalize` does not type-check the expression. You may want to type-check @@ -24,7 +24,7 @@ impl<'a> Typed<'a> { /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. /// - pub fn normalize(self) -> Normalized<'a> { + pub fn normalize(self) -> Normalized { let internal = match self.0 { TypedInternal::Sort => TypedInternal::Sort, TypedInternal::Value(thunk, t) => { @@ -35,19 +35,15 @@ impl<'a> Typed<'a> { TypedInternal::Value(thunk, t) } }; - Normalized(internal, self.1) + Normalized(internal) } pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { - Typed(self.0.shift(delta, var), self.1) + Typed(self.0.shift(delta, var)) } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { - Typed(self.0.subst_shift(var, val), self.1) + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { + Typed(self.0.subst_shift(var, val)) } pub(crate) fn to_value(&self) -> Value { @@ -74,11 +70,7 @@ impl EnvItem { } } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)), EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()), @@ -133,7 +125,7 @@ impl NormalizationContext { NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var)))) } - fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { NormalizationContext(Rc::new( self.0.map(|_, e| e.subst_shift(var, val)), )) @@ -512,11 +504,7 @@ impl Value { } } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { Value::Lam(x, t, e) => Value::Lam( x.clone(), @@ -724,7 +712,7 @@ mod thunk { } } - fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { ThunkInternal::Unnormalized(ctx, e) => { ThunkInternal::Unnormalized( @@ -823,11 +811,7 @@ mod thunk { self.0.borrow().shift(delta, var).into_thunk() } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { self.0.borrow().subst_shift(var, val).into_thunk() } } @@ -839,7 +823,7 @@ pub(crate) use thunk::Thunk; #[derive(Debug, Clone)] pub(crate) enum TypeThunk { Thunk(Thunk), - Type(Type<'static>), + Type(Type), } impl TypeThunk { @@ -851,7 +835,7 @@ impl TypeThunk { TypeThunk::Thunk(th) } - pub(crate) fn from_type(t: Type<'static>) -> TypeThunk { + pub(crate) fn from_type(t: Type) -> TypeThunk { TypeThunk::Type(t) } @@ -880,11 +864,7 @@ impl TypeThunk { } } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { match self { TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)), TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)), diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs index 99ca5ee..e3ff2d5 100644 --- a/dhall/src/traits/deserialize.rs +++ b/dhall/src/traits/deserialize.rs @@ -12,7 +12,7 @@ pub trait Deserialize<'de>: Sized { fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self>; } -impl<'de: 'a, 'a> Deserialize<'de> for Parsed<'a> { +impl<'de> Deserialize<'de> for Parsed { /// Simply parses the provided string. Ignores the /// provided type. fn from_str(s: &'de str, _: Option<&Type>) -> Result<Self> { @@ -20,7 +20,7 @@ impl<'de: 'a, 'a> Deserialize<'de> for Parsed<'a> { } } -impl<'de: 'a, 'a> Deserialize<'de> for Resolved<'a> { +impl<'de> Deserialize<'de> for Resolved { /// Parses and resolves the provided string. Ignores the /// provided type. fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> { @@ -28,7 +28,7 @@ impl<'de: 'a, 'a> Deserialize<'de> for Resolved<'a> { } } -impl<'de: 'a, 'a> Deserialize<'de> for Typed<'a> { +impl<'de> Deserialize<'de> for Typed { /// Parses, resolves and typechecks the provided string. fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> { let resolved = Resolved::from_str(s, ty)?; @@ -39,14 +39,14 @@ impl<'de: 'a, 'a> Deserialize<'de> for Typed<'a> { } } -impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> { +impl<'de> Deserialize<'de> for Normalized { /// Parses, resolves, typechecks and normalizes the provided string. fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> { Ok(Typed::from_str(s, ty)?.normalize()) } } -impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> { +impl<'de> Deserialize<'de> for Type { fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> { Ok(Normalized::from_str(s, ty)?.to_type()) } diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index b8f6f6d..858642e 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -7,29 +7,29 @@ use dhall_syntax::{Const, ExprF}; use std::borrow::Cow; pub trait DynamicType { - fn get_type<'a>(&'a self) -> Result<Cow<'a, Type<'static>>, TypeError>; + fn get_type<'a>(&'a self) -> Result<Cow<'a, Type>, TypeError>; } impl<T: StaticType> DynamicType for T { - fn get_type<'a>(&'a self) -> Result<Cow<'a, Type<'static>>, TypeError> { + fn get_type<'a>(&'a self) -> Result<Cow<'a, Type>, TypeError> { Ok(Cow::Owned(T::get_static_type())) } } -impl<'a> DynamicType for Type<'a> { - fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { +impl DynamicType for Type { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { self.get_type() } } -impl<'a> DynamicType for Normalized<'a> { - fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { +impl DynamicType for Normalized { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { self.0.get_type() } } -impl<'a> DynamicType for Typed<'a> { - fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { +impl DynamicType for Typed { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { self.0.get_type() } } diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index 1255d1c..f90b8df 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -11,7 +11,7 @@ use dhall_syntax::*; /// For now the only interesting impl is [SimpleType] itself, who /// has a statically-known type which is not itself a [SimpleType]. pub trait StaticType { - fn get_static_type() -> Type<'static>; + fn get_static_type() -> Type; } /// A Rust type that can be represented as a Dhall type. @@ -29,15 +29,15 @@ pub trait StaticType { /// The `Simple` in `SimpleStaticType` indicates that the returned type is /// a [SimpleType]. pub trait SimpleStaticType { - fn get_simple_static_type<'a>() -> SimpleType<'a>; + fn get_simple_static_type() -> SimpleType; } -fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> { +fn mktype(x: SubExpr<X, X>) -> SimpleType { x.into() } impl<T: SimpleStaticType> StaticType for T { - fn get_static_type() -> Type<'static> { + fn get_static_type() -> Type { crate::expr::Normalized::from_thunk_and_type( crate::normalize::Thunk::from_normalized_expr( T::get_simple_static_type().into(), @@ -48,64 +48,64 @@ impl<T: SimpleStaticType> StaticType for T { } } -impl<'a> StaticType for SimpleType<'a> { +impl StaticType for SimpleType { /// By definition, a [SimpleType] has type `Type`. /// This returns the Dhall expression `Type` - fn get_static_type() -> Type<'static> { + fn get_static_type() -> Type { Type::const_type() } } impl SimpleStaticType for bool { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Bool)) } } impl SimpleStaticType for Natural { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Natural)) } } impl SimpleStaticType for u32 { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Natural)) } } impl SimpleStaticType for u64 { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Natural)) } } impl SimpleStaticType for Integer { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Integer)) } } impl SimpleStaticType for i32 { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Integer)) } } impl SimpleStaticType for i64 { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Integer)) } } impl SimpleStaticType for String { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!(Text)) } } impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { let ta: SubExpr<_, _> = A::get_simple_static_type().into(); let tb: SubExpr<_, _> = B::get_simple_static_type().into(); mktype(dhall::subexpr!({ _1: ta, _2: tb })) @@ -113,27 +113,27 @@ impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) { } impl<T: SimpleStaticType> SimpleStaticType for Option<T> { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { let t: SubExpr<_, _> = T::get_simple_static_type().into(); mktype(dhall::subexpr!(Optional t)) } } impl<T: SimpleStaticType> SimpleStaticType for Vec<T> { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { let t: SubExpr<_, _> = T::get_simple_static_type().into(); mktype(dhall::subexpr!(List t)) } } impl<'a, T: SimpleStaticType> SimpleStaticType for &'a T { - fn get_simple_static_type<'b>() -> SimpleType<'b> { + fn get_simple_static_type() -> SimpleType { T::get_simple_static_type() } } impl<T> SimpleStaticType for std::marker::PhantomData<T> { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { mktype(dhall::subexpr!({})) } } @@ -141,7 +141,7 @@ impl<T> SimpleStaticType for std::marker::PhantomData<T> { impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType for std::result::Result<T, E> { - fn get_simple_static_type<'a>() -> SimpleType<'a> { + fn get_simple_static_type() -> SimpleType { let tt: SubExpr<_, _> = T::get_simple_static_type().into(); let te: SubExpr<_, _> = E::get_simple_static_type().into(); mktype(dhall::subexpr!(< Ok: tt | Err: te>)) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 69491c8..74de59b 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -14,21 +14,18 @@ use dhall_syntax::*; use self::TypeMessage::*; -impl<'a> Resolved<'a> { - pub fn typecheck(self) -> Result<Typed<'static>, TypeError> { +impl Resolved { + pub fn typecheck(self) -> Result<Typed, TypeError> { type_of(self.0.unnote()) } - pub fn typecheck_with( - self, - ty: &Type, - ) -> Result<Typed<'static>, TypeError> { + pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> { let expr: SubExpr<_, _> = self.0.unnote(); let ty: SubExpr<_, _> = ty.to_expr().embed_absurd(); type_of(rc(ExprF::Annot(expr, ty))) } /// Pretends this expression has been typechecked. Use with care. #[allow(dead_code)] - pub fn skip_typecheck(self) -> Typed<'a> { + pub fn skip_typecheck(self) -> Typed { Typed::from_thunk_untyped(Thunk::new( NormalizationContext::new(), self.0.unnote(), @@ -36,8 +33,8 @@ impl<'a> Resolved<'a> { } } -impl<'a> Typed<'a> { - fn to_type(&self) -> Type<'a> { +impl Typed { + fn to_type(&self) -> Type { match &self.to_value() { Value::Const(c) => Type(TypeInternal::Const(*c)), _ => Type(TypeInternal::Typed(Box::new(self.clone()))), @@ -45,17 +42,17 @@ impl<'a> Typed<'a> { } } -impl<'a> Normalized<'a> { +impl Normalized { fn shift(&self, delta: isize, var: &V<Label>) -> Self { - Normalized(self.0.shift(delta, var), self.1) + Normalized(self.0.shift(delta, var)) } - pub(crate) fn to_type(self) -> Type<'a> { + pub(crate) fn to_type(self) -> Type { self.0.to_type() } } -impl<'a> Type<'a> { - pub(crate) fn to_normalized(&self) -> Normalized<'a> { +impl Type { + pub(crate) fn to_normalized(&self) -> Normalized { self.0.to_normalized() } pub(crate) fn to_expr(&self) -> SubExpr<X, X> { @@ -64,13 +61,13 @@ impl<'a> Type<'a> { pub(crate) fn to_value(&self) -> Value { self.0.to_value() } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { self.0.get_type() } fn as_const(&self) -> Option<Const> { self.0.as_const() } - fn internal(&self) -> &TypeInternal<'a> { + fn internal(&self) -> &TypeInternal { &self.0 } fn internal_whnf(&self) -> Option<Value> { @@ -79,11 +76,7 @@ impl<'a> Type<'a> { pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Type(self.0.shift(delta, var)) } - pub(crate) fn subst_shift( - &self, - var: &V<Label>, - val: &Typed<'static>, - ) -> Self { + pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { Type(self.0.subst_shift(var, val)) } @@ -99,10 +92,7 @@ impl<'a> Type<'a> { } impl TypeThunk { - fn to_type( - &self, - ctx: &TypecheckContext, - ) -> Result<Type<'static>, TypeError> { + fn to_type(&self, ctx: &TypecheckContext) -> Result<Type, TypeError> { match self { TypeThunk::Type(t) => Ok(t.clone()), TypeThunk::Thunk(th) => { @@ -118,20 +108,20 @@ impl TypeThunk { /// The rule is the following: we must _not_ construct values of type `Expr` while typechecking, /// but only construct `TypeInternal`s. #[derive(Debug, Clone)] -pub(crate) enum TypeInternal<'a> { +pub(crate) enum TypeInternal { Const(Const), /// This must not contain a Const value. - Typed(Box<Typed<'a>>), + Typed(Box<Typed>), } -impl<'a> TypeInternal<'a> { - fn to_typed(&self) -> Typed<'a> { +impl TypeInternal { + fn to_typed(&self) -> Typed { match self { TypeInternal::Typed(e) => e.as_ref().clone(), TypeInternal::Const(c) => const_to_typed(*c), } } - fn to_normalized(&self) -> Normalized<'a> { + fn to_normalized(&self) -> Normalized { self.to_typed().normalize() } fn to_expr(&self) -> SubExpr<X, X> { @@ -140,7 +130,7 @@ impl<'a> TypeInternal<'a> { fn to_value(&self) -> Value { self.to_typed().to_value() } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { + pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { Ok(match self { TypeInternal::Typed(e) => e.get_type()?, TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?), @@ -165,7 +155,7 @@ impl<'a> TypeInternal<'a> { Const(c) => Const(*c), } } - fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self { use TypeInternal::*; match self { Typed(e) => Typed(Box::new(e.subst_shift(var, val))), @@ -174,8 +164,8 @@ impl<'a> TypeInternal<'a> { } } -impl<'a> Eq for TypeInternal<'a> {} -impl<'a> PartialEq for TypeInternal<'a> { +impl Eq for TypeInternal {} +impl PartialEq for TypeInternal { fn eq(&self, other: &Self) -> bool { self.to_normalized() == other.to_normalized() } @@ -183,8 +173,8 @@ impl<'a> PartialEq for TypeInternal<'a> { #[derive(Debug, Clone)] pub(crate) enum EnvItem { - Type(V<Label>, Type<'static>), - Value(Normalized<'static>), + Type(V<Label>, Type), + Value(Normalized), } impl EnvItem { @@ -204,7 +194,7 @@ impl TypecheckContext { pub(crate) fn new() -> Self { TypecheckContext(Context::new()) } - pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self { + pub(crate) fn insert_type(&self, x: &Label, t: Type) -> Self { TypecheckContext( self.0.map(|_, e| e.shift(1, &x.into())).insert( x.clone(), @@ -212,17 +202,10 @@ impl TypecheckContext { ), ) } - pub(crate) fn insert_value( - &self, - x: &Label, - t: Normalized<'static>, - ) -> Self { + pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self { TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t))) } - pub(crate) fn lookup( - &self, - var: &V<Label>, - ) -> Option<Cow<'_, Type<'static>>> { + pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> { let V(x, n) = var; match self.0.lookup(x, *n) { Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)), @@ -276,8 +259,8 @@ fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool { // Equality up to alpha-equivalence (renaming of bound variables) fn prop_equal<T, U>(eL0: T, eR0: U) -> bool where - T: Borrow<Type<'static>>, - U: Borrow<Type<'static>>, + T: Borrow<Type>, + U: Borrow<Type>, { use dhall_syntax::ExprF::*; fn go<'a, S, T>( @@ -340,7 +323,7 @@ where } } -fn const_to_typed<'a>(c: Const) -> Typed<'a> { +fn const_to_typed(c: Const) -> Typed { match c { Const::Sort => Typed::const_sort(), _ => Typed::from_thunk_and_type( @@ -350,11 +333,11 @@ fn const_to_typed<'a>(c: Const) -> Typed<'a> { } } -fn const_to_type<'a>(c: Const) -> Type<'a> { +fn const_to_type(c: Const) -> Type { Type(TypeInternal::Const(c)) } -fn type_of_const<'a>(c: Const) -> Result<Type<'a>, TypeError> { +fn type_of_const(c: Const) -> Result<Type, TypeError> { match c { Const::Type => Ok(Type::const_kind()), Const::Kind => Ok(Type::const_sort()), @@ -472,15 +455,15 @@ macro_rules! ensure_simple_type { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum TypeIntermediate { - Pi(TypecheckContext, Label, Type<'static>, Type<'static>), - RecordType(TypecheckContext, BTreeMap<Label, Type<'static>>), - UnionType(TypecheckContext, BTreeMap<Label, Option<Type<'static>>>), - ListType(TypecheckContext, Type<'static>), - OptionalType(TypecheckContext, Type<'static>), + Pi(TypecheckContext, Label, Type, Type), + RecordType(TypecheckContext, BTreeMap<Label, Type>), + UnionType(TypecheckContext, BTreeMap<Label, Option<Type>>), + ListType(TypecheckContext, Type), + OptionalType(TypecheckContext, Type), } impl TypeIntermediate { - fn typecheck(self) -> Result<Typed<'static>, TypeError> { + fn typecheck(self) -> Result<Typed, TypeError> { let mkerr = |ctx, msg| TypeError::new(ctx, msg); Ok(match &self { TypeIntermediate::Pi(ctx, x, ta, tb) => { @@ -638,32 +621,32 @@ impl TypeIntermediate { /// and turn it into a type, typechecking it along the way. fn mktype( ctx: &TypecheckContext, - e: SubExpr<X, Normalized<'static>>, -) -> Result<Type<'static>, TypeError> { + e: SubExpr<X, Normalized>, +) -> Result<Type, TypeError> { Ok(type_with(ctx, e)?.to_type()) } -fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> { +fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> { mktype(&TypecheckContext::new(), rc(ExprF::Builtin(b))) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetTyped(Typed<'static>), + RetTyped(Typed), /// Use the contained Type as the type of the input expression - RetType(Type<'static>), + RetType(Type), /// Returns an expression that must be typechecked and /// turned into a Type first. - RetExpr(Expr<X, Normalized<'static>>), + RetExpr(Expr<X, Normalized>), } /// Type-check an expression and return the expression alongside its type if type-checking /// succeeded, or an error if type-checking failed fn type_with( ctx: &TypecheckContext, - e: SubExpr<X, Normalized<'static>>, -) -> Result<Typed<'static>, TypeError> { + e: SubExpr<X, Normalized>, +) -> Result<Typed, TypeError> { use dhall_syntax::ExprF::*; use Ret::*; @@ -736,12 +719,12 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF<Typed<'static>, Label, X, Normalized<'static>>, + e: ExprF<Typed, Label, X, Normalized>, ) -> Result<Ret, TypeError> { use dhall_syntax::BinOp::*; use dhall_syntax::Builtin::*; use dhall_syntax::ExprF::*; - let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, msg); + let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg); use Ret::*; match e { @@ -1011,9 +994,7 @@ fn type_last_layer( /// `typeOf` 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<X, Normalized<'static>>, -) -> Result<Typed<'static>, TypeError> { +fn type_of(e: SubExpr<X, Normalized>) -> Result<Typed, TypeError> { let ctx = TypecheckContext::new(); let e = type_with(&ctx, e)?; // Ensure `e` has a type (i.e. `e` is not `Sort`) @@ -1023,27 +1004,27 @@ fn type_of( /// The specific type error #[derive(Debug)] -pub(crate) enum TypeMessage<'a> { +pub(crate) enum TypeMessage { UnboundVariable(V<Label>), - InvalidInputType(Normalized<'a>), - InvalidOutputType(Normalized<'a>), - NotAFunction(Typed<'a>), - TypeMismatch(Typed<'a>, Normalized<'a>, Typed<'a>), - AnnotMismatch(Typed<'a>, Normalized<'a>), + InvalidInputType(Normalized), + InvalidOutputType(Normalized), + NotAFunction(Typed), + TypeMismatch(Typed, Normalized, Typed), + AnnotMismatch(Typed, Normalized), Untyped, - InvalidListElement(usize, Normalized<'a>, Typed<'a>), - InvalidListType(Normalized<'a>), - InvalidOptionalType(Normalized<'a>), - InvalidPredicate(Typed<'a>), - IfBranchMismatch(Typed<'a>, Typed<'a>), - IfBranchMustBeTerm(bool, Typed<'a>), - InvalidFieldType(Label, Type<'a>), - NotARecord(Label, Normalized<'a>), - MissingRecordField(Label, Typed<'a>), - MissingUnionField(Label, Normalized<'a>), - BinOpTypeMismatch(BinOp, Typed<'a>), - NoDependentTypes(Normalized<'a>, Normalized<'a>), - InvalidTextInterpolation(Typed<'a>), + InvalidListElement(usize, Normalized, Typed), + InvalidListType(Normalized), + InvalidOptionalType(Normalized), + InvalidPredicate(Typed), + IfBranchMismatch(Typed, Typed), + IfBranchMustBeTerm(bool, Typed), + InvalidFieldType(Label, Type), + NotARecord(Label, Normalized), + MissingRecordField(Label, Typed), + MissingUnionField(Label, Normalized), + BinOpTypeMismatch(BinOp, Typed), + NoDependentTypes(Normalized, Normalized), + InvalidTextInterpolation(Typed), Sort, Unimplemented, } @@ -1051,14 +1032,14 @@ pub(crate) enum TypeMessage<'a> { /// A structured type error that includes context #[derive(Debug)] pub struct TypeError { - type_message: TypeMessage<'static>, + type_message: TypeMessage, context: TypecheckContext, } impl TypeError { pub(crate) fn new( context: &TypecheckContext, - type_message: TypeMessage<'static>, + type_message: TypeMessage, ) -> Self { TypeError { context: context.clone(), @@ -1073,7 +1054,7 @@ impl From<TypeError> for std::option::NoneError { } } -impl ::std::error::Error for TypeMessage<'static> { +impl ::std::error::Error for TypeMessage { fn description(&self) -> &str { match *self { // UnboundVariable => "Unbound variable", @@ -1086,7 +1067,7 @@ impl ::std::error::Error for TypeMessage<'static> { } } -impl fmt::Display for TypeMessage<'static> { +impl fmt::Display for TypeMessage { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { match self { // UnboundVariable(_) => { |