diff options
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/expr.rs | 22 | ||||
-rw-r--r-- | dhall/src/lib.rs | 6 | ||||
-rw-r--r-- | dhall/src/tests.rs | 5 | ||||
-rw-r--r-- | dhall/src/traits/dynamic_type.rs | 56 | ||||
-rw-r--r-- | dhall/src/traits/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 54 |
6 files changed, 96 insertions, 49 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index aa02c28..6458be9 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -66,3 +66,25 @@ impl From<SubExpr<X, X>> for SimpleType { SimpleType(x) } } + +impl Typed { + pub(crate) fn as_expr(&self) -> &SubExpr<X, X> { + &self.0 + } + pub(crate) fn into_expr(self) -> SubExpr<X, X> { + self.0 + } +} + +impl Normalized { + pub(crate) fn as_expr(&self) -> &SubExpr<X, X> { + &self.0 + } + pub(crate) fn into_expr(self) -> SubExpr<X, X> { + self.0 + } + pub(crate) fn into_type(self) -> Type { + crate::expr::Type(TypeInternal::Expr(Box::new(self))) + } +} + diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 8af5af9..6d08d08 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -126,9 +126,9 @@ mod imports; mod normalize; mod traits; mod typecheck; -pub use crate::traits::Deserialize; -pub use crate::traits::SimpleStaticType; -pub use crate::traits::StaticType; +pub use crate::traits::{ + Deserialize, DynamicType, SimpleStaticType, StaticType, +}; pub use dhall_generator::SimpleStaticType; pub mod error; pub mod expr; diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index dcded3a..798f3e9 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -41,6 +41,7 @@ macro_rules! make_spec_test { use crate::error::{Error, Result}; use crate::expr::Parsed; +use crate::DynamicType; use std::path::PathBuf; #[derive(Copy, Clone)] @@ -119,8 +120,8 @@ pub fn run_test( } TypeInference => { let expr = expr.typecheck()?; - let ty = expr.get_type()?.as_normalized()?; - assert_eq_display!(ty, &expected); + let ty = expr.get_type()?; + assert_eq_display!(ty.as_normalized()?, &expected); } Normalization => { let expr = expr.skip_typecheck().normalize(); diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs new file mode 100644 index 0000000..25fe52d --- /dev/null +++ b/dhall/src/traits/dynamic_type.rs @@ -0,0 +1,56 @@ +use crate::expr::*; +use crate::traits::StaticType; +use crate::typecheck::{TypeError, TypeMessage}; +use dhall_core::context::Context; +use dhall_core::{Const, ExprF, X}; +use std::borrow::Cow; + +pub trait DynamicType { + fn get_type<'a>(&'a self) -> Result<Cow<'a, Type>, TypeError<X>>; +} + +impl<T: StaticType> DynamicType for T { + fn get_type<'a>(&'a self) -> Result<Cow<'a, Type>, TypeError<X>> { + Ok(Cow::Owned(T::get_static_type())) + } +} + +impl DynamicType for Type { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError<X>> { + use TypeInternal::*; + match &self.0 { + Expr(e) => e.get_type(), + SuperType => Err(TypeError::new( + &Context::new(), + dhall_core::rc(ExprF::Const(Const::Sort)), + TypeMessage::Untyped, + )), + } + } +} + +impl DynamicType for Normalized { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError<X>> { + match &self.1 { + Some(t) => Ok(Cow::Borrowed(t)), + None => Err(TypeError::new( + &Context::new(), + self.0.clone(), + TypeMessage::Untyped, + )), + } + } +} + +impl DynamicType for Typed { + fn get_type(&self) -> Result<Cow<'_, Type>, TypeError<X>> { + match &self.1 { + Some(t) => Ok(Cow::Borrowed(t)), + None => Err(TypeError::new( + &Context::new(), + self.0.clone(), + TypeMessage::Untyped, + )), + } + } +} diff --git a/dhall/src/traits/mod.rs b/dhall/src/traits/mod.rs index 4ce8f97..315e17a 100644 --- a/dhall/src/traits/mod.rs +++ b/dhall/src/traits/mod.rs @@ -1,4 +1,6 @@ mod deserialize; +mod dynamic_type; mod static_type; pub use deserialize::Deserialize; +pub use dynamic_type::DynamicType; pub use static_type::{SimpleStaticType, StaticType}; diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 0ddb784..3350964 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,7 +1,9 @@ #![allow(non_snake_case)] +use std::borrow::Borrow; use std::fmt; use crate::expr::*; +use crate::traits::DynamicType; use dhall_core; use dhall_core::context::Context; use dhall_core::*; @@ -24,19 +26,6 @@ impl Resolved { } } impl Typed { - fn as_expr(&self) -> &SubExpr<X, X> { - &self.0 - } - fn into_expr(self) -> SubExpr<X, X> { - self.0 - } - pub fn get_type(&self) -> Result<&Type, TypeError<X>> { - self.1.as_ref().ok_or(TypeError::new( - &Context::new(), - self.0.clone(), - TypeMessage::Untyped, - )) - } fn get_type_move(self) -> Result<Type, TypeError<X>> { self.1.ok_or(TypeError::new( &Context::new(), @@ -46,22 +35,6 @@ impl Typed { } } impl Normalized { - fn as_expr(&self) -> &SubExpr<X, X> { - &self.0 - } - pub(crate) fn into_expr(self) -> SubExpr<X, X> { - self.0 - } - pub fn get_type(&self) -> Result<&Type, TypeError<X>> { - self.1.as_ref().ok_or(TypeError::new( - &Context::new(), - self.0.clone(), - TypeMessage::Untyped, - )) - } - pub(crate) fn into_type(self) -> Type { - crate::expr::Type(TypeInternal::Expr(Box::new(self))) - } // Expose the outermost constructor fn unroll_ref(&self) -> &Expr<X, X> { self.as_expr().as_ref() @@ -98,17 +71,6 @@ impl Type { fn unroll_ref(&self) -> Result<&Expr<X, X>, TypeError<X>> { Ok(self.as_normalized()?.unroll_ref()) } - pub fn get_type(&self) -> Result<&Type, TypeError<X>> { - use TypeInternal::*; - match &self.0 { - Expr(e) => e.get_type(), - SuperType => Err(TypeError::new( - &Context::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } - } fn shift(&self, delta: isize, var: &V<Label>) -> Self { use TypeInternal::*; crate::expr::Type(match &self.0 { @@ -165,7 +127,11 @@ 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(eL0: &Type, eR0: &Type) -> bool { +fn prop_equal<T, U>(eL0: T, eR0: U) -> bool +where + T: Borrow<Type>, + U: Borrow<Type>, +{ use dhall_core::ExprF::*; fn go<S, T>( ctx: &mut Vec<(Label, Label)>, @@ -221,7 +187,7 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool { (_, _) => false, } } - match (&eL0.0, &eR0.0) { + match (&eL0.borrow().0, &eR0.borrow().0) { (TypeInternal::SuperType, TypeInternal::SuperType) => true, (TypeInternal::Expr(l), TypeInternal::Expr(r)) => { let mut ctx = vec![]; @@ -405,7 +371,7 @@ pub fn type_with( mkerr(InvalidInputType(r.get_type_move()?.into_normalized()?)), ); - let ctx2 = ctx.insert(f.clone(), r.get_type()?.clone()); + let ctx2 = ctx.insert(f.clone(), r.get_type()?.into_owned()); 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 @@ -441,7 +407,7 @@ pub fn type_with( }, App(f, args) => { let mut seen_args: Vec<SubExpr<_, _>> = vec![]; - let mut tf = f.get_type()?.clone(); + let mut tf = f.get_type()?.into_owned(); for a in args { seen_args.push(a.as_expr().clone()); let (x, tx, tb) = ensure_matches!(tf, |