summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs100
-rw-r--r--dhall/src/imports.rs86
-rw-r--r--dhall/src/normalize.rs50
-rw-r--r--dhall/src/traits/deserialize.rs10
-rw-r--r--dhall/src/traits/dynamic_type.rs16
-rw-r--r--dhall/src/traits/static_type.rs40
-rw-r--r--dhall/src/typecheck.rs167
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(_) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:08:57 +0000