From bbf8d68b0df3ca8b3b8cb7324169f0049736ed89 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 20 Apr 2019 23:52:09 +0200 Subject: Move TypeInternal to typecheck --- dhall/src/expr.rs | 16 ++-------------- dhall/src/typecheck.rs | 38 +++++++++++++++++++++++++++++--------- 2 files changed, 31 insertions(+), 23 deletions(-) diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index bb1a4e4..03aa966 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -63,6 +63,8 @@ pub struct SimpleType<'a>( ); derive_other_traits!(SimpleType); +pub(crate) use crate::typecheck::TypeInternal; + /// A Dhall expression representing a (possibly higher-kinded) type. /// /// This includes [SimpleType]s but also higher-kinded expressions like @@ -70,14 +72,6 @@ derive_other_traits!(SimpleType); #[derive(Debug, Clone, PartialEq, Eq)] pub struct Type<'a>(pub(crate) TypeInternal<'a>); -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum TypeInternal<'a> { - Expr(Box>), - Const(dhall_core::Const), - /// The type of `Sort` - SuperType, -} - // Exposed for the macros #[doc(hidden)] impl<'a> From> for SubExpr { @@ -120,12 +114,6 @@ impl<'a> Normalized<'a> { pub(crate) fn unnote<'b>(self) -> Normalized<'b> { Normalized(self.0, self.1, PhantomData) } - pub(crate) fn into_type(self) -> Type<'a> { - Type(match self.0.as_ref() { - ExprF::Const(c) => TypeInternal::Const(*c), - _ => TypeInternal::Expr(Box::new(self)), - }) - } } #[doc(hidden)] diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b26f845..99fb003 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -48,6 +48,12 @@ impl<'a> Normalized<'a> { // shift the type too ? Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2) } + pub(crate) fn into_type(self) -> Type<'a> { + Type(match self.0.as_ref() { + ExprF::Const(c) => TypeInternal::Const(*c), + _ => TypeInternal::Expr(Box::new(self)), + }) + } } impl Normalized<'static> { fn embed(self) -> SubExpr> { @@ -69,15 +75,7 @@ impl<'a> Type<'a> { } } pub(crate) fn into_normalized(self) -> Result, TypeError> { - match self.0 { - TypeInternal::Expr(e) => Ok(*e), - TypeInternal::Const(c) => Ok(const_to_normalized(c)), - TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + self.0.into_normalized() } // Expose the outermost constructor fn unroll_ref(&self) -> Result>, TypeError> { @@ -111,6 +109,28 @@ impl Type<'static> { } } +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum TypeInternal<'a> { + Expr(Box>), + Const(dhall_core::Const), + /// The type of `Sort` + SuperType, +} + +impl<'a> TypeInternal<'a> { + fn into_normalized(self) -> Result, TypeError> { + match self { + TypeInternal::Expr(e) => Ok(*e), + TypeInternal::Const(c) => Ok(const_to_normalized(c)), + TypeInternal::SuperType => Err(TypeError::new( + &Context::new(), + rc(ExprF::Const(Const::Sort)), + TypeMessage::Untyped, + )), + } + } +} + fn function_check(a: Const, b: Const) -> Result { use dhall_core::Const::*; match (a, b) { -- cgit v1.2.3 From d1f828961bccf9627ef4fb76ca528f039d180ff7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 21 Apr 2019 11:30:58 +0200 Subject: Embrace TypeInternal as a semantic value --- dhall/src/expr.rs | 9 +++++++++ dhall/src/normalize.rs | 1 + dhall/src/tests.rs | 2 +- dhall/src/typecheck.rs | 22 ++++++++++++++-------- 4 files changed, 25 insertions(+), 9 deletions(-) diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 03aa966..44d1612 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -72,6 +72,15 @@ pub(crate) use crate::typecheck::TypeInternal; #[derive(Debug, Clone, PartialEq, Eq)] pub struct Type<'a>(pub(crate) TypeInternal<'a>); +impl<'a> std::fmt::Display for Type<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + match self.0.clone().into_normalized() { + Ok(e) => e.fmt(f), + Err(_) => write!(f, "SuperType"), + } + } +} + // Exposed for the macros #[doc(hidden)] impl<'a> From> for SubExpr { diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index f092c4d..7aa8686 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -322,6 +322,7 @@ enum WHNF { (NormalizationContext, BTreeMap>), ), TextLit(Vec>), + /// This must not contain a value captured by one of the variants above. Expr(OutputSubExpr), } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 7f85b5c..c945b23 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -140,7 +140,7 @@ pub fn run_test( TypeInference => { let expr = expr.typecheck()?; let ty = expr.get_type()?; - assert_eq_display!(ty.as_normalized()?.as_ref(), &expected); + assert_eq_display!(ty.as_ref(), &expected.into_type()); } Normalization => { let expr = expr.skip_typecheck().normalize(); diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 99fb003..b0ea63e 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -61,9 +61,7 @@ impl Normalized<'static> { } } impl<'a> Type<'a> { - pub(crate) fn as_normalized( - &self, - ) -> Result>, TypeError> { + fn as_normalized(&self) -> Result>, TypeError> { match &self.0 { TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), @@ -84,6 +82,9 @@ impl<'a> Type<'a> { Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())), } } + fn internal(&self) -> &TypeInternal { + &self.0 + } fn shift0(&self, delta: isize, label: &Label) -> Self { use TypeInternal::*; Type(match &self.0 { @@ -109,16 +110,21 @@ impl Type<'static> { } } +/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should +/// 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)] pub(crate) enum TypeInternal<'a> { - Expr(Box>), - Const(dhall_core::Const), + Const(Const), /// The type of `Sort` SuperType, + /// This must not contain a value captured by one of the variants above. + Expr(Box>), } impl<'a> TypeInternal<'a> { - fn into_normalized(self) -> Result, TypeError> { + pub(crate) fn into_normalized(self) -> Result, TypeError> { match self { TypeInternal::Expr(e) => Ok(*e), TypeInternal::Const(c) => Ok(const_to_normalized(c)), @@ -348,8 +354,8 @@ macro_rules! ensure_simple_type { macro_rules! ensure_is_const { ($x:expr, $err:expr $(,)*) => { - match $x.unroll_ref()?.as_ref() { - Const(k) => *k, + match $x.internal() { + TypeInternal::Const(k) => *k, _ => return Err($err), } }; -- cgit v1.2.3 From 20f01b79378a41c6e063d33c584d04c756419a26 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 21 Apr 2019 19:38:09 +0200 Subject: Factor out context handling --- dhall/src/traits/dynamic_type.rs | 11 ++++++----- dhall/src/typecheck.rs | 42 ++++++++++++++++++++++++++-------------- 2 files changed, 34 insertions(+), 19 deletions(-) diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index d4faf45..479bed6 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,7 +1,8 @@ use crate::expr::*; use crate::traits::StaticType; -use crate::typecheck::{type_of_const, TypeError, TypeMessage}; -use dhall_core::context::Context; +use crate::typecheck::{ + type_of_const, TypeError, TypeMessage, TypecheckContext, +}; use dhall_core::{Const, ExprF}; use std::borrow::Cow; @@ -21,7 +22,7 @@ impl<'a> DynamicType for Type<'a> { TypeInternal::Expr(e) => e.get_type(), TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), dhall_core::rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, )), @@ -34,7 +35,7 @@ impl<'a> DynamicType for Normalized<'a> { match &self.1 { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), self.0.embed_absurd(), TypeMessage::Untyped, )), @@ -47,7 +48,7 @@ impl<'a> DynamicType for Typed<'a> { match &self.1 { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), self.0.clone(), TypeMessage::Untyped, )), diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b0ea63e..a183944 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -35,7 +35,7 @@ impl<'a> Typed<'a> { fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); ty.ok_or_else(|| { - TypeError::new(&Context::new(), expr, TypeMessage::Untyped) + TypeError::new(&TypecheckContext::new(), expr, TypeMessage::Untyped) }) } } @@ -66,7 +66,7 @@ impl<'a> Type<'a> { TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, )), @@ -129,7 +129,7 @@ impl<'a> TypeInternal<'a> { TypeInternal::Expr(e) => Ok(*e), TypeInternal::Const(c) => Ok(const_to_normalized(c)), TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, )), @@ -137,6 +137,22 @@ impl<'a> TypeInternal<'a> { } } +#[derive(Debug, Clone)] +pub(crate) struct TypecheckContext(Context>); + +impl TypecheckContext { + pub(crate) fn new() -> Self { + TypecheckContext(Context::new()) + } + pub(crate) fn insert_and_shift(&self, x: &Label, t: Type<'static>) -> Self { + TypecheckContext(self.0.insert(x.clone(), t).map(|_, e| e.shift0(1, x))) + } + pub(crate) fn lookup(&self, var: &V