diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/typecheck.rs | 155 |
1 files changed, 72 insertions, 83 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e7231e9..2c3a36f 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -140,24 +140,14 @@ impl Type<'static> { /// be limited to syntactic expressions: either written by the user or meant to be printed. /// The rule is the following: we must _not_ construct values of type `Expr` while typechecking, /// but only construct `TypeInternal`s. -#[derive(Debug, Clone, PartialEq, Eq)] +#[derive(Debug, Clone)] pub(crate) enum TypeInternal<'a> { Const(Const), - Pi( - TypecheckContext, - Const, - Label, - Box<Type<'static>>, - Box<Type<'static>>, - ), - RecordType(TypecheckContext, Const, BTreeMap<Label, Type<'static>>), - UnionType( - TypecheckContext, - Const, - BTreeMap<Label, Option<Type<'static>>>, - ), - ListType(TypecheckContext, Box<Type<'static>>), - OptionalType(TypecheckContext, Box<Type<'static>>), + Pi(Const, Label, Box<Type<'static>>, Box<Type<'static>>), + RecordType(Const, BTreeMap<Label, Type<'static>>), + UnionType(Const, BTreeMap<Label, Option<Type<'static>>>), + ListType(Box<Type<'static>>), + OptionalType(Box<Type<'static>>), /// The type of `Sort` SuperType, /// This must not contain a value captured by one of the variants above. @@ -166,9 +156,9 @@ pub(crate) enum TypeInternal<'a> { impl<'a> TypeInternal<'a> { pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { - let (ctx, e, t) = match self { - TypeInternal::Expr(e) => return Ok(*e), - TypeInternal::Const(c) => return Ok(const_to_normalized(c)), + Ok(match self { + TypeInternal::Expr(e) => *e, + TypeInternal::Const(c) => const_to_normalized(c), TypeInternal::SuperType => { return Err(TypeError::new( &TypecheckContext::new(), @@ -176,47 +166,46 @@ impl<'a> TypeInternal<'a> { TypeMessage::Untyped, )) } - TypeInternal::Pi(ctx, c, x, t, e) => { - (ctx, ExprF::Pi(x, *t, *e), const_to_type(c)) - } - TypeInternal::RecordType(ctx, c, kts) => { - (ctx, ExprF::RecordType(kts), const_to_type(c)) - } - TypeInternal::UnionType(ctx, c, kts) => { - (ctx, ExprF::UnionType(kts), const_to_type(c)) - } - TypeInternal::ListType(ctx, t) => { - return Ok(Typed( - rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - t.embed()?, - )), - Some(Type::const_type()), - ctx, - PhantomData, - ) - .normalize()) - } - TypeInternal::OptionalType(ctx, t) => { - return Ok(Typed( - rc(ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), - t.embed()?, - )), - Some(Type::const_type()), - ctx, - PhantomData, - ) - .normalize()) - } - }; - let typed = Typed( - rc(e.traverse_ref_simple(|e| e.clone().embed())?), - Some(t), - ctx, - PhantomData, - ); - Ok(typed.normalize()) + TypeInternal::Pi(c, x, t, e) => Normalized( + rc(ExprF::Pi( + x, + t.into_normalized()?.into_expr(), + e.into_normalized()?.into_expr(), + )), + Some(const_to_type(c)), + PhantomData, + ), + TypeInternal::RecordType(c, kts) => Normalized( + rc(ExprF::RecordType(kts).traverse_ref_simple(|e| { + Ok(e.clone().into_normalized()?.into_expr()) + })?), + Some(const_to_type(c)), + PhantomData, + ), + TypeInternal::UnionType(c, kts) => Normalized( + rc(ExprF::UnionType(kts).traverse_ref_simple(|e| { + Ok(e.clone().into_normalized()?.into_expr()) + })?), + Some(const_to_type(c)), + PhantomData, + ), + TypeInternal::ListType(t) => Normalized( + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + t.into_normalized()?.into_expr(), + )), + Some(Type::const_type()), + PhantomData, + ), + TypeInternal::OptionalType(t) => Normalized( + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::Optional)), + t.into_normalized()?.into_expr(), + )), + Some(Type::const_type()), + PhantomData, + ), + }) } fn shift0(&self, delta: isize, label: &Label) -> Self { self.shift(delta, &V(label.clone(), 0)) @@ -225,22 +214,19 @@ impl<'a> TypeInternal<'a> { use TypeInternal::*; match self { Expr(e) => Expr(Box::new(e.shift(delta, var))), - Pi(ctx, c, x, t, e) => Pi( - ctx.clone(), + Pi(c, x, t, e) => Pi( *c, x.clone(), Box::new(t.shift(delta, var)), Box::new(e.shift(delta, &var.shift0(1, x))), ), - RecordType(ctx, c, kts) => RecordType( - ctx.clone(), + RecordType(c, kts) => RecordType( *c, kts.iter() .map(|(k, v)| (k.clone(), v.shift(delta, var))) .collect(), ), - UnionType(ctx, c, kts) => UnionType( - ctx.clone(), + UnionType(c, kts) => UnionType( *c, kts.iter() .map(|(k, v)| { @@ -248,18 +234,26 @@ impl<'a> TypeInternal<'a> { }) .collect(), ), - ListType(ctx, t) => { - ListType(ctx.clone(), Box::new(t.shift(delta, var))) - } - OptionalType(ctx, t) => { - OptionalType(ctx.clone(), Box::new(t.shift(delta, var))) - } + ListType(t) => ListType(Box::new(t.shift(delta, var))), + OptionalType(t) => OptionalType(Box::new(t.shift(delta, var))), Const(c) => Const(*c), SuperType => SuperType, } } } +impl<'a> Eq for TypeInternal<'a> {} +impl<'a> PartialEq for TypeInternal<'a> { + fn eq(&self, other: &Self) -> bool { + let self_nzed = self.clone().into_normalized(); + let other_nzed = other.clone().into_normalized(); + match (self_nzed, other_nzed) { + (Ok(x), Ok(y)) => x == y, + _ => false, + } + } +} + #[derive(Debug, Clone)] pub(crate) enum TypedOrType { Typed(Typed<'static>), @@ -621,7 +615,6 @@ impl TypeIntermediate { }; Ok(TypedOrType::Type(Type(TypeInternal::Pi( - ctx.clone(), k, x.clone(), Box::new(ta.clone()), @@ -650,7 +643,6 @@ impl TypeIntermediate { let k = k.unwrap_or(dhall_core::Const::Type); Ok(TypedOrType::Type(Type(TypeInternal::RecordType( - ctx.clone(), k, kts.clone(), )))) @@ -681,7 +673,6 @@ impl TypeIntermediate { // an union type with only unary variants also has type Type let k = k.unwrap_or(dhall_core::Const::Type); Ok(TypedOrType::Type(Type(TypeInternal::UnionType( - ctx.clone(), k, kts.clone(), )))) @@ -691,10 +682,9 @@ impl TypeIntermediate { t, mkerr(ctx, InvalidListType(t.clone().into_normalized()?))?, ); - Ok(TypedOrType::Type(Type(TypeInternal::ListType( - ctx.clone(), - Box::new(t.clone()), - )))) + Ok(TypedOrType::Type(Type(TypeInternal::ListType(Box::new( + t.clone(), + ))))) } TypeIntermediate::OptionalType(ctx, t) => { ensure_simple_type!( @@ -705,7 +695,6 @@ impl TypeIntermediate { )?, ); Ok(TypedOrType::Type(Type(TypeInternal::OptionalType( - ctx.clone(), Box::new(t.clone()), )))) } @@ -868,7 +857,7 @@ fn type_last_layer( App(f, a) => { let tf = f.get_type()?.into_owned(); let (x, tx, tb) = match tf.into_internal() { - TypeInternal::Pi(_, _, x, tx, tb) => (x, tx, tb), + TypeInternal::Pi(_, x, tx, tb) => (x, tx, tb), _ => return Err(mkerr(NotAFunction(f))), }; ensure_equal!(a.get_type()?, tx.as_ref(), { @@ -1010,14 +999,14 @@ fn type_last_layer( )) } Field(r, x) => match r.get_type()?.internal() { - TypeInternal::RecordType(_, _, kts) => match kts.get(&x) { + TypeInternal::RecordType(_, kts) => match kts.get(&x) { Some(t) => Ok(RetType(t.clone())), None => Err(mkerr(MissingRecordField(x, r))), }, TypeInternal::Const(_) => { let r = r.normalize_to_type()?; match r.internal() { - TypeInternal::UnionType(_, _, kts) => match kts.get(&x) { + TypeInternal::UnionType(_, kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > // TODO: use "_" instead of x (i.e. compare types using equivalence in tests) Some(Some(t)) => Ok(RetType( |