summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs9
-rw-r--r--dhall/src/tests.rs2
-rw-r--r--dhall/src/traits/dynamic_type.rs8
-rw-r--r--dhall/src/typecheck.rs90
4 files changed, 67 insertions, 42 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index cda1d8d..9e89e3a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -73,6 +73,7 @@ pub struct Type<'a>(pub(crate) TypeInternal<'a>);
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum TypeInternal<'a> {
Expr(Box<Normalized<'a>>),
+ Const(dhall_core::Const),
/// The type of `Sort`
SuperType,
}
@@ -116,8 +117,14 @@ impl<'a> Normalized<'a> {
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<'a> {
- crate::expr::Type(TypeInternal::Expr(Box::new(self)))
+ Type(match self.0.as_ref() {
+ ExprF::Const(c) => TypeInternal::Const(*c),
+ _ => TypeInternal::Expr(Box::new(self)),
+ })
}
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ce24bfc..5cea6aa 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -139,7 +139,7 @@ pub fn run_test(
TypeInference => {
let expr = expr.typecheck()?;
let ty = expr.get_type()?;
- assert_eq_display!(ty.as_normalized()?, &expected);
+ assert_eq_display!(ty.as_normalized()?.as_ref(), &expected);
}
Normalization => {
let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index 28ed76d..d2a5414 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -1,6 +1,6 @@
use crate::expr::*;
use crate::traits::StaticType;
-use crate::typecheck::{TypeError, TypeMessage};
+use crate::typecheck::{type_of_const, TypeError, TypeMessage};
use dhall_core::context::Context;
use dhall_core::{Const, ExprF};
use std::borrow::Cow;
@@ -17,10 +17,10 @@ impl<T: StaticType> DynamicType for T {
impl<'a> DynamicType for Type<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
- use TypeInternal::*;
match &self.0 {
- Expr(e) => e.get_type(),
- SuperType => Err(TypeError::new(
+ TypeInternal::Expr(e) => e.get_type(),
+ TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))),
+ TypeInternal::SuperType => Err(TypeError::new(
&Context::new(),
dhall_core::rc(ExprF::Const(Const::Sort)),
TypeMessage::Untyped,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 86c5ebd..195628b 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,5 +1,6 @@
#![allow(non_snake_case)]
use std::borrow::Borrow;
+use std::borrow::Cow;
use std::fmt;
use std::marker::PhantomData;
@@ -54,11 +55,13 @@ impl Normalized<'static> {
}
}
impl<'a> Type<'a> {
- pub(crate) fn as_normalized(&self) -> Result<&Normalized<'a>, TypeError> {
- use TypeInternal::*;
+ pub(crate) fn as_normalized(
+ &self,
+ ) -> Result<Cow<Normalized<'a>>, TypeError> {
match &self.0 {
- Expr(e) => Ok(e),
- SuperType => Err(TypeError::new(
+ TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)),
+ TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))),
+ TypeInternal::SuperType => Err(TypeError::new(
&Context::new(),
rc(ExprF::Const(Const::Sort)),
TypeMessage::Untyped,
@@ -66,51 +69,47 @@ impl<'a> Type<'a> {
}
}
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
- use TypeInternal::*;
match self.0 {
- Expr(e) => Ok(*e),
- SuperType => Err(TypeError::new(
+ 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,
)),
}
}
+ // Expose the outermost constructor, except if it is Const
+ fn unroll_ref_no_const(&self) -> Result<&Expr<X, X>, TypeError> {
+ match self.as_normalized()? {
+ Cow::Borrowed(e) => Ok(e.unroll_ref()),
+ Cow::Owned(_) => unimplemented!(),
+ }
+ }
// Expose the outermost constructor
- fn unroll_ref(&self) -> Result<&Expr<X, X>, TypeError> {
- Ok(self.as_normalized()?.unroll_ref())
+ fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, TypeError> {
+ match self.as_normalized()? {
+ Cow::Borrowed(e) => Ok(Cow::Borrowed(e.unroll_ref())),
+ Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
+ }
}
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
- crate::expr::Type(match &self.0 {
+ Type(match &self.0 {
Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Const(c) => Const(*c),
SuperType => SuperType,
})
}
fn const_sort() -> Self {
- Normalized(
- rc(ExprF::Const(Const::Sort)),
- Some(Type(TypeInternal::SuperType)),
- PhantomData,
- )
- .into_type()
+ Type(TypeInternal::Const(Const::Sort))
}
fn const_kind() -> Self {
- Normalized(
- rc(ExprF::Const(Const::Kind)),
- Some(Type::const_sort()),
- PhantomData,
- )
- .into_type()
+ Type(TypeInternal::Const(Const::Kind))
}
pub(crate) fn const_type() -> Self {
- Normalized(
- rc(ExprF::Const(Const::Type)),
- Some(Type::const_kind()),
- PhantomData,
- )
- .into_type()
+ Type(TypeInternal::Const(Const::Type))
}
}
impl Type<'static> {
@@ -200,6 +199,7 @@ where
}
match (&eL0.borrow().0, &eR0.borrow().0) {
(TypeInternal::SuperType, TypeInternal::SuperType) => true,
+ (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
(TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
let mut ctx = vec![];
go(&mut ctx, l.as_expr(), r.as_expr())
@@ -208,7 +208,19 @@ where
}
}
-fn type_of_const<'a>(c: Const) -> Type<'a> {
+fn const_to_normalized<'a>(c: Const) -> Normalized<'a> {
+ Normalized(
+ rc(ExprF::Const(c)),
+ Some(Type(match c {
+ Const::Type => TypeInternal::Const(Const::Kind),
+ Const::Kind => TypeInternal::Const(Const::Sort),
+ Const::Sort => TypeInternal::SuperType,
+ })),
+ PhantomData,
+ )
+}
+
+pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> {
match c {
Const::Type => Type::const_kind(),
Const::Kind => Type::const_sort(),
@@ -216,7 +228,7 @@ fn type_of_const<'a>(c: Const) -> Type<'a> {
}
}
-fn type_of_builtin<S>(b: Builtin) -> Expr<S, Normalized<'static>> {
+fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> {
use dhall_core::Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
@@ -293,7 +305,7 @@ macro_rules! ensure_equal {
macro_rules! ensure_matches {
($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => {
- match $x.unroll_ref()? {
+ match $x.unroll_ref_no_const()? {
$pat => $branch,
_ => return Err($err),
}
@@ -302,14 +314,20 @@ macro_rules! ensure_matches {
// Ensure the provided type has type `Type`
macro_rules! ensure_simple_type {
- ($x:expr, $err:expr $(,)*) => {
- ensure_matches!($x.get_type()?, Const(Type) => {}, $err)
- };
+ ($x:expr, $err:expr $(,)*) => {{
+ let k = ensure_is_const!($x.get_type()?, $err);
+ if k != Type {
+ return Err($err);
+ }
+ }};
}
macro_rules! ensure_is_const {
($x:expr, $err:expr $(,)*) => {
- ensure_matches!($x, Const(k) => *k, $err)
+ match $x.unroll_ref()?.as_ref() {
+ Const(k) => *k,
+ _ => return Err($err),
+ }
};
}
@@ -619,7 +637,7 @@ fn type_last_layer(
// TODO: check type of interpolations
TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))),
BinOp(o @ ListAppend, l, r) => {
- match l.get_type()?.as_normalized()?.as_expr().as_ref() {
+ match l.get_type()?.unroll_ref()?.as_ref() {
App(f, args) if args.len() == 1 => match f.as_ref() {
Builtin(List) => {}
_ => return Err(mkerr(BinOpTypeMismatch(o, l))),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 14:12:28 +0000