summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs8
-rw-r--r--dhall/src/typecheck.rs132
2 files changed, 63 insertions, 77 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 75d7690..555db2f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -8,19 +8,19 @@ pub struct Parsed(pub(crate) SubExpr<X, Import>, pub(crate) ImportRoot);
pub struct Resolved(pub(crate) SubExpr<X, X>);
#[derive(Debug, Clone)]
-pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type<'static>);
+pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
#[derive(Debug, Clone)]
-pub struct Type<'a>(pub(crate) std::borrow::Cow<'a, TypeInternal>);
+pub struct Type(pub(crate) TypeInternal);
#[derive(Debug, Clone)]
pub(crate) enum TypeInternal {
Expr(Box<Normalized>),
- Universe(usize),
+ Untyped,
}
#[derive(Debug, Clone)]
-pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type<'static>);
+pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type);
impl PartialEq for Parsed {
fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f380448..9eead93 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,6 @@ use dhall_core;
use dhall_core::context::Context;
use dhall_core::*;
use dhall_generator as dhall;
-use std::borrow::Cow;
use self::TypeMessage::*;
@@ -26,8 +25,12 @@ impl Typed {
self.0
}
#[inline(always)]
- pub fn get_type<'a>(&'a self) -> Type<'a> {
- self.1.reborrow()
+ pub fn get_type(&self) -> &Type {
+ &self.1
+ }
+ #[inline(always)]
+ fn get_type_move(self) -> Type {
+ self.1
}
}
impl Normalized {
@@ -40,12 +43,12 @@ impl Normalized {
self.0
}
#[inline(always)]
- pub fn get_type<'a>(&'a self) -> Type<'a> {
- self.1.reborrow()
+ pub fn get_type(&self) -> &Type {
+ &self.1
}
#[inline(always)]
- fn into_type(self) -> Type<'static> {
- crate::expr::Type(Cow::Owned(TypeInternal::Expr(Box::new(self))))
+ fn into_type(self) -> Type {
+ crate::expr::Type(TypeInternal::Expr(Box::new(self)))
}
// Expose the outermost constructor
#[inline(always)]
@@ -58,24 +61,13 @@ impl Normalized {
Normalized(shift(delta, var, &self.0), self.1.clone())
}
}
-impl<'a> Type<'a> {
- #[inline(always)]
- fn into_owned(self) -> Type<'static> {
- Type(Cow::Owned(self.0.into_owned()))
- }
- #[inline(always)]
- fn reborrow<'b>(&'b self) -> Type<'b> {
- match &self.0 {
- Cow::Owned(x) => crate::expr::Type(Cow::Borrowed(x)),
- Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
- }
- }
+impl Type {
#[inline(always)]
- fn as_normalized(&'a self) -> Result<&'a Normalized, TypeError<X>> {
+ fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
use TypeInternal::*;
- match self.0.as_ref() {
+ match &self.0 {
Expr(e) => Ok(e),
- Universe(_) => Err(TypeError::new(
+ Untyped => Err(TypeError::new(
&Context::new(),
rc(ExprF::Const(Const::Sort)),
TypeMessage::Untyped,
@@ -85,9 +77,9 @@ impl<'a> Type<'a> {
#[inline(always)]
fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
use TypeInternal::*;
- match self.0.into_owned() {
+ match self.0 {
Expr(e) => Ok(*e),
- Universe(_) => Err(TypeError::new(
+ Untyped => Err(TypeError::new(
&Context::new(),
rc(ExprF::Const(Const::Sort)),
TypeMessage::Untyped,
@@ -96,29 +88,28 @@ impl<'a> Type<'a> {
}
// Expose the outermost constructor
#[inline(always)]
- fn unroll_ref(&'a self) -> Result<&'a Expr<X, X>, TypeError<X>> {
+ fn unroll_ref(&self) -> Result<&Expr<X, X>, TypeError<X>> {
Ok(self.as_normalized()?.unroll_ref())
}
#[inline(always)]
- pub fn get_type<'b>(&'b self) -> Type<'b> {
+ pub fn get_type(&self) -> &Type {
use TypeInternal::*;
- match self.0.as_ref() {
+ match &self.0 {
Expr(e) => e.get_type(),
- Universe(n) => crate::expr::Type(Cow::Owned(Universe(n + 1))),
+ Untyped => &UNTYPE,
}
}
#[inline(always)]
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
- crate::expr::Type(Cow::Owned(match self.reborrow().0 {
- Cow::Borrowed(Expr(e)) => Expr(Box::new(e.shift(delta, var))),
- Cow::Borrowed(Universe(n)) => Universe(*n),
- Cow::Owned(_) => unreachable!(),
- }))
+ crate::expr::Type(match &self.0 {
+ Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Untyped => Untyped,
+ })
}
}
-const TYPE_OF_SORT: Type<'static> = Type(Cow::Owned(TypeInternal::Universe(4)));
+const UNTYPE: Type = Type(TypeInternal::Untyped);
fn rule(a: Const, b: Const) -> Result<Const, ()> {
use dhall_core::Const::*;
@@ -207,10 +198,8 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
(_, _) => false,
}
}
- match (&*eL0.0, &*eR0.0) {
- (TypeInternal::Universe(l), TypeInternal::Universe(r)) if r == l => {
- true
- }
+ match (&eL0.0, &eR0.0) {
+ (TypeInternal::Untyped, TypeInternal::Untyped) => false,
(TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
let mut ctx = vec![];
go(&mut ctx, l.unroll_ref(), r.unroll_ref())
@@ -283,9 +272,9 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
}
}
-fn ensure_equal<'a, S, F1, F2>(
- x: &Type<'a>,
- y: &Type<'a>,
+fn ensure_equal<S, F1, F2>(
+ x: &Type,
+ y: &Type,
mkerr: F1,
mkmsg: F2,
) -> Result<(), TypeError<S>>
@@ -304,7 +293,7 @@ where
/// Type-check an expression and return the expression alongside its type
/// if type-checking succeeded, or an error if type-checking failed
pub fn type_with(
- ctx: &Context<Label, Type<'static>>,
+ ctx: &Context<Label, Type>,
e: SubExpr<X, X>,
) -> Result<Typed, TypeError<X>> {
use dhall_core::BinOp::*;
@@ -327,7 +316,7 @@ pub fn type_with(
|ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
enum Ret {
- RetType(crate::expr::Type<'static>),
+ RetType(crate::expr::Type),
RetExpr(Expr<X, X>),
}
use Ret::*;
@@ -343,7 +332,7 @@ pub fn type_with(
rc(Pi(
x.clone(),
t.into_normalized()?.into_expr(),
- b.get_type().into_normalized()?.into_expr(),
+ b.get_type_move().into_normalized()?.into_expr(),
)),
)?))
}
@@ -365,7 +354,7 @@ pub fn type_with(
&ctx2,
e.clone(),
InvalidOutputType(
- tB.get_type().into_owned().into_normalized()?,
+ tB.get_type_move().into_normalized()?,
),
));
}
@@ -374,7 +363,7 @@ pub fn type_with(
match rule(kA, kB) {
Err(()) => Err(mkerr(NoDependentTypes(
tA.clone().into_normalized()?,
- tB.get_type().into_owned().into_normalized()?,
+ tB.get_type_move().into_normalized()?,
))),
Ok(k) => Ok(RetExpr(Const(k))),
}
@@ -393,26 +382,26 @@ pub fn type_with(
// message because this should never happen anyway
let kR = ensure_const(
&r.get_type().get_type(),
- InvalidInputType(r.get_type().into_owned().into_normalized()?),
+ InvalidInputType(r.get_type().clone().into_normalized()?),
)?;
- let ctx2 = ctx.insert(f.clone(), r.get_type().into_owned());
+ let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
let b = type_with(&ctx2, b.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kB = ensure_const(
&b.get_type().get_type(),
- InvalidOutputType(b.get_type().into_owned().into_normalized()?),
+ InvalidOutputType(b.get_type().clone().into_normalized()?),
)?;
if let Err(()) = rule(kR, kB) {
return Err(mkerr(NoDependentLet(
- r.get_type().into_owned().into_normalized()?,
- b.get_type().into_owned().into_normalized()?,
+ r.get_type_move().into_normalized()?,
+ b.get_type_move().into_normalized()?,
)));
}
- Ok(RetType(b.get_type().into_owned()))
+ Ok(RetType(b.get_type_move()))
}
_ => match e
.as_ref()
@@ -423,7 +412,7 @@ pub fn type_with(
Let(_, _, _, _) => unreachable!(),
Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
- Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
+ Const(Sort) => Ok(RetType(UNTYPE)),
Var(V(x, n)) => match ctx.lookup(&x, n) {
Some(e) => Ok(RetType(e.clone())),
None => Err(mkerr(UnboundVariable)),
@@ -431,7 +420,7 @@ pub fn type_with(
App(f, args) => {
let mut iter = args.into_iter();
let mut seen_args: Vec<SubExpr<_, _>> = vec![];
- let mut tf = f.get_type().into_owned();
+ let mut tf = f.get_type().clone();
while let Some(a) = iter.next() {
seen_args.push(a.as_expr().clone());
let (x, tx, tb) = match tf.unroll_ref()? {
@@ -469,7 +458,7 @@ pub fn type_with(
t.clone().into_normalized().unwrap(),
)
})?;
- Ok(RetType(x.get_type().into_owned()))
+ Ok(RetType(x.get_type_move()))
}
BoolIf(x, y, z) => {
ensure_equal(
@@ -492,7 +481,7 @@ pub fn type_with(
IfBranchMismatch(y.clone(), z.clone())
})?;
- Ok(RetType(y.get_type().into_owned()))
+ Ok(RetType(y.get_type_move()))
}
EmptyListLit(t) => {
let t = t.normalize().into_type();
@@ -508,23 +497,18 @@ pub fn type_with(
let (_, x) = iter.next().unwrap();
ensure_is_type(
&x.get_type().get_type(),
- InvalidListType(
- x.get_type().into_owned().into_normalized()?,
- ),
+ InvalidListType(x.get_type().clone().into_normalized()?),
)?;
for (i, y) in iter {
ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
InvalidListElement(
i,
- x.get_type()
- .into_owned()
- .into_normalized()
- .unwrap(),
+ x.get_type().clone().into_normalized().unwrap(),
y.clone(),
)
})?;
}
- let t = x.get_type().into_normalized()?.into_expr();
+ let t = x.get_type_move().into_normalized()?.into_expr();
Ok(RetExpr(dhall::expr!(List t)))
}
EmptyOptionalLit(t) => {
@@ -540,10 +524,10 @@ pub fn type_with(
ensure_is_type(
&x.get_type().get_type(),
InvalidOptionalType(
- x.get_type().into_owned().into_normalized()?,
+ x.get_type().clone().into_normalized()?,
),
)?;
- let t = x.get_type().into_normalized()?.into_expr();
+ let t = x.get_type_move().into_normalized()?.into_expr();
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
@@ -565,7 +549,7 @@ pub fn type_with(
)?;
Ok((
k.clone(),
- v.get_type().into_normalized()?.into_expr(),
+ v.get_type_move().into_normalized()?.into_expr(),
))
})
.collect::<Result<_, _>>()?;
@@ -624,14 +608,16 @@ pub fn type_with(
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
- let ctx = Context::new();
- let e = type_with(&ctx, e)?;
- Ok(e.get_type().into_normalized()?.into_expr())
+ let e = type_of_(e)?;
+ Ok(e.get_type_move().into_normalized()?.into_expr())
}
pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
let ctx = Context::new();
- type_with(&ctx, e)
+ let e = type_with(&ctx, e)?;
+ // Ensure the inferred type isn't UNTYPE
+ e.get_type().as_normalized()?;
+ Ok(e)
}
/// The specific type error
@@ -665,14 +651,14 @@ pub enum TypeMessage<S> {
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<S> {
- pub context: Context<Label, Type<'static>>,
+ pub context: Context<Label, Type>,
pub current: SubExpr<S, X>,
pub type_message: TypeMessage<S>,
}
impl<S> TypeError<S> {
pub fn new(
- context: &Context<Label, Type<'static>>,
+ context: &Context<Label, Type>,
current: SubExpr<S, X>,
type_message: TypeMessage<S>,
) -> Self {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 22:58:58 +0000