From e1a30c6f248c0c17c97598290a0d94993dbb0325 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 10 Apr 2019 19:16:11 +0200 Subject: Add SimpleType and SimpeStaticType. Derive the latter --- dhall/src/expr.rs | 21 ++++++++++ dhall/src/lib.rs | 3 +- dhall/src/traits.rs | 109 +++++++++++++++++++++++++++++++------------------ dhall/src/typecheck.rs | 21 ++++++++-- 4 files changed, 111 insertions(+), 43 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 7baf628..5ff097b 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -36,6 +36,11 @@ derive_other_traits!(Typed); pub struct Normalized(pub(crate) SubExpr, pub(crate) Type); derive_other_traits!(Normalized); +/// An expression of type `Type` (like `Bool` or `Natural -> Text`, but not `Type`) +#[derive(Debug, Clone, Eq)] +pub struct SimpleType(pub(crate) SubExpr); +derive_other_traits!(SimpleType); + #[derive(Debug, Clone, PartialEq, Eq)] pub struct Type(pub(crate) TypeInternal); @@ -44,3 +49,19 @@ pub(crate) enum TypeInternal { Expr(Box), Untyped, } + +// Exposed for the macros +#[doc(hidden)] +impl From for SubExpr { + fn from(x: SimpleType) -> SubExpr { + x.0 + } +} + +// Exposed for the macros +#[doc(hidden)] +impl From> for SimpleType { + fn from(x: SubExpr) -> SimpleType { + SimpleType(x) + } +} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 5c5a641..3bfc46f 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -21,6 +21,7 @@ mod imports; mod normalize; mod traits; mod typecheck; +pub use crate::traits::SimpleStaticType; pub use crate::traits::StaticType; -pub use dhall_generator::StaticType; +pub use dhall_generator::SimpleStaticType; pub mod expr; diff --git a/dhall/src/traits.rs b/dhall/src/traits.rs index 64e07d9..4925457 100644 --- a/dhall/src/traits.rs +++ b/dhall/src/traits.rs @@ -1,77 +1,108 @@ +use crate::expr::*; use dhall_core::*; use dhall_generator::*; +use std::borrow::Cow; #[derive(Debug, Clone)] pub enum ConversionError {} pub trait StaticType { - fn get_type() -> DhallExpr; - // fn as_dhall(&self) -> DhallExpr; - // fn from_dhall(e: DhallExpr) -> Result; + fn get_static_type() -> Type; } -impl StaticType for bool { - fn get_type() -> DhallExpr { - dhall_expr!(Bool) +/// Trait for rust types that can be represented in dhall in +/// a single way, independent of the value. A typical example is `Option`, +/// represented by the dhall expression `Optional Bool`. A typical counterexample +/// is `HashMap` because dhall cannot represent records with a +/// variable number of fields. +pub trait SimpleStaticType { + fn get_simple_static_type() -> SimpleType; +} + +fn mktype(x: SubExpr) -> SimpleType { + SimpleType(x) +} + +impl StaticType for T { + fn get_static_type() -> Type { + crate::expr::Normalized( + T::get_simple_static_type().into(), + Type::const_type(), + ) + .into_type() + } +} + +impl StaticType for SimpleType { + fn get_static_type() -> Type { + Type::const_type() + } +} + +impl SimpleStaticType for bool { + fn get_simple_static_type() -> SimpleType { + mktype(dhall_expr!(Bool)) } } -impl StaticType for Natural { - fn get_type() -> DhallExpr { - dhall_expr!(Natural) +impl SimpleStaticType for Natural { + fn get_simple_static_type() -> SimpleType { + mktype(dhall_expr!(Natural)) } } -impl StaticType for Integer { - fn get_type() -> DhallExpr { - dhall_expr!(Integer) +impl SimpleStaticType for Integer { + fn get_simple_static_type() -> SimpleType { + mktype(dhall_expr!(Integer)) } } -impl StaticType for String { - fn get_type() -> DhallExpr { - dhall_expr!(Text) +impl SimpleStaticType for String { + fn get_simple_static_type() -> SimpleType { + mktype(dhall_expr!(Text)) } } -impl StaticType for (A, B) { - fn get_type() -> DhallExpr { - let ta = A::get_type(); - let tb = B::get_type(); - dhall_expr!({ _1: ta, _2: tb }) +impl SimpleStaticType for (A, B) { + 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_expr!({ _1: ta, _2: tb })) } } -impl StaticType for Option { - fn get_type() -> DhallExpr { - let t = T::get_type(); - dhall_expr!(Optional t) +impl SimpleStaticType for Option { + fn get_simple_static_type() -> SimpleType { + let t: SubExpr<_, _> = T::get_simple_static_type().into(); + mktype(dhall_expr!(Optional t)) } } -impl StaticType for Vec { - fn get_type() -> DhallExpr { - let t = T::get_type(); - dhall_expr!(List t) +impl SimpleStaticType for Vec { + fn get_simple_static_type() -> SimpleType { + let t: SubExpr<_, _> = T::get_simple_static_type().into(); + mktype(dhall_expr!(List t)) } } -impl<'a, T: StaticType> StaticType for &'a T { - fn get_type() -> DhallExpr { - T::get_type() +impl<'a, T: SimpleStaticType> SimpleStaticType for &'a T { + fn get_simple_static_type() -> SimpleType { + T::get_simple_static_type() } } -impl StaticType for std::marker::PhantomData { - fn get_type() -> DhallExpr { - dhall_expr!({}) +impl SimpleStaticType for std::marker::PhantomData { + fn get_simple_static_type() -> SimpleType { + mktype(dhall_expr!({})) } } -impl StaticType for Result { - fn get_type() -> DhallExpr { - let tt = T::get_type(); - let te = E::get_type(); - dhall_expr!(< Ok: tt | Err: te>) +impl SimpleStaticType + for std::result::Result +{ + 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_expr!(< Ok: tt | Err: te>)) } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 998d3ca..f51f1b6 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -42,7 +42,7 @@ impl Normalized { &self.0 } #[inline(always)] - fn into_expr(self) -> SubExpr { + pub(crate) fn into_expr(self) -> SubExpr { self.0 } #[inline(always)] @@ -50,7 +50,7 @@ impl Normalized { &self.1 } #[inline(always)] - fn into_type(self) -> Type { + pub(crate) fn into_type(self) -> Type { crate::expr::Type(TypeInternal::Expr(Box::new(self))) } // Expose the outermost constructor @@ -78,7 +78,7 @@ impl Type { } } #[inline(always)] - fn into_normalized(self) -> Result> { + pub(crate) fn into_normalized(self) -> Result> { use TypeInternal::*; match self.0 { Expr(e) => Ok(*e), @@ -110,6 +110,21 @@ impl Type { Untyped => Untyped, }) } + + #[inline(always)] + pub fn const_sort() -> Self { + Normalized(rc(ExprF::Const(Const::Sort)), UNTYPE).into_type() + } + #[inline(always)] + pub fn const_kind() -> Self { + Normalized(rc(ExprF::Const(Const::Kind)), Type::const_sort()) + .into_type() + } + #[inline(always)] + pub fn const_type() -> Self { + Normalized(rc(ExprF::Const(Const::Type)), Type::const_kind()) + .into_type() + } } const UNTYPE: Type = Type(TypeInternal::Untyped); -- cgit v1.2.3