summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs22
-rw-r--r--dhall/src/lib.rs6
-rw-r--r--dhall/src/tests.rs5
-rw-r--r--dhall/src/traits/dynamic_type.rs56
-rw-r--r--dhall/src/traits/mod.rs2
-rw-r--r--dhall/src/typecheck.rs54
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,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 05:09:52 +0000