summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/lib.rs25
-rw-r--r--dhall/src/semantics/resolve/hir.rs20
-rw-r--r--dhall/src/semantics/tck/tir.rs30
-rw-r--r--dhall/src/semantics/tck/typecheck.rs15
-rw-r--r--tests_buffer2
5 files changed, 52 insertions, 40 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index a4987c6..c329c66 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -22,7 +22,9 @@ use crate::error::{EncodeError, Error, TypeError};
use crate::semantics::parse;
use crate::semantics::resolve;
use crate::semantics::resolve::ImportRoot;
-use crate::semantics::{typecheck, typecheck_with, Hir, Nir, NirKind, Tir};
+use crate::semantics::{
+ typecheck, typecheck_with, Hir, Nir, NirKind, Tir, Type,
+};
use crate::syntax::binary;
use crate::syntax::{Builtin, Expr};
@@ -42,7 +44,10 @@ pub struct Resolved(Hir);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(Tir);
+pub struct Typed {
+ hir: Hir,
+ ty: Type,
+}
/// A normalized expression.
///
@@ -92,10 +97,10 @@ impl Parsed {
impl Resolved {
pub fn typecheck(&self) -> Result<Typed, TypeError> {
- Ok(Typed(typecheck(&self.0)?))
+ Ok(Typed::from_tir(typecheck(&self.0)?))
}
pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> {
- Ok(Typed(typecheck_with(&self.0, ty.to_hir())?))
+ Ok(Typed::from_tir(typecheck_with(&self.0, ty.to_hir())?))
}
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> ResolvedExpr {
@@ -104,21 +109,27 @@ impl Resolved {
}
impl Typed {
+ fn from_tir(tir: Tir<'_>) -> Self {
+ Typed {
+ hir: tir.as_hir().clone(),
+ ty: tir.ty().clone(),
+ }
+ }
/// Reduce an expression to its normal form, performing beta reduction
pub fn normalize(&self) -> Normalized {
- Normalized(self.0.rec_eval_closed_expr())
+ Normalized(self.hir.rec_eval_closed_expr())
}
/// Converts a value back to the corresponding AST expression.
fn to_expr(&self) -> ResolvedExpr {
- self.0.to_expr(ToExprOptions {
+ self.hir.to_expr(ToExprOptions {
alpha: false,
normalize: false,
})
}
pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
- Ok(Normalized(self.0.ty().clone().into_nir()))
+ Ok(Normalized(self.ty.clone().into_nir()))
}
}
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 346abbf..d421718 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -48,11 +48,11 @@ impl Hir {
self.span.clone()
}
- /// Converts a HIR expr back to the corresponding AST expression.
+ /// Converts a closed Hir expr back to the corresponding AST expression.
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
hir_to_expr(self, opts, &mut NameEnv::new())
}
- /// Converts a HIR expr back to the corresponding AST expression.
+ /// Converts a closed Hir expr back to the corresponding AST expression.
pub fn to_expr_noopts(&self) -> NormalizedExpr {
let opts = ToExprOptions {
normalize: false,
@@ -70,7 +70,10 @@ impl Hir {
}
/// Typecheck the Hir.
- pub fn typecheck(&self, env: &TyEnv) -> Result<Tir, TypeError> {
+ pub fn typecheck<'hir>(
+ &'hir self,
+ env: &TyEnv,
+ ) -> Result<Tir<'hir>, TypeError> {
type_with(env, self, None)
}
@@ -78,6 +81,17 @@ impl Hir {
pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
Nir::new_thunk(env.into(), self.clone())
}
+ /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
+ /// needed on demand.
+ pub fn eval_closed_expr(&self) -> Nir {
+ self.eval(NzEnv::new())
+ }
+ /// Eval a closed Hir fully and recursively;
+ pub fn rec_eval_closed_expr(&self) -> Nir {
+ let val = self.eval_closed_expr();
+ val.normalize();
+ val
+ }
}
fn hir_to_expr(
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 908bf8f..aeb7bf9 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,7 +1,7 @@
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
use crate::syntax::{Builtin, Const, Span};
-use crate::{NormalizedExpr, ToExprOptions};
+use crate::NormalizedExpr;
/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -17,8 +17,8 @@ pub(crate) struct Type {
/// A hir expression plus its inferred type.
/// Stands for "Typed intermediate representation"
#[derive(Debug, Clone)]
-pub(crate) struct Tir {
- hir: Hir,
+pub(crate) struct Tir<'hir> {
+ hir: &'hir Hir,
ty: Type,
}
@@ -106,12 +106,9 @@ impl Type {
}
}
-impl Tir {
- pub fn from_hir(hir: &Hir, ty: Type) -> Self {
- Tir {
- hir: hir.clone(),
- ty,
- }
+impl<'hir> Tir<'hir> {
+ pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+ Tir { hir, ty }
}
pub fn span(&self) -> Span {
@@ -127,10 +124,6 @@ impl Tir {
pub fn as_hir(&self) -> &Hir {
&self.hir
}
- /// Converts a closed expression back to the corresponding AST expression.
- pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- self.as_hir().to_expr(opts)
- }
pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
self.as_hir().to_expr_tyenv(env)
}
@@ -173,17 +166,6 @@ impl Tir {
.to_universe(),
))
}
- /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
- /// needed on demand.
- pub fn eval_closed_expr(&self) -> Nir {
- self.eval(NzEnv::new())
- }
- /// Eval a closed Tir fully and recursively;
- pub fn rec_eval_closed_expr(&self) -> Nir {
- let val = self.eval_closed_expr();
- val.normalize();
- val
- }
}
impl From<Const> for Universe {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 42a9165..0787b32 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -69,7 +69,7 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
/// layer.
fn type_one_layer(
env: &TyEnv,
- ekind: ExprKind<Tir>,
+ ekind: ExprKind<Tir<'_>>,
span: Span,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
@@ -703,11 +703,11 @@ fn type_one_layer(
/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
/// to compare with.
-pub(crate) fn type_with(
+pub(crate) fn type_with<'hir>(
env: &TyEnv,
- hir: &Hir,
+ hir: &'hir Hir,
annot: Option<Type>,
-) -> Result<Tir, TypeError> {
+) -> Result<Tir<'hir>, TypeError> {
let tir = match hir.kind() {
HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
HirKind::Expr(ExprKind::Var(_)) => {
@@ -799,12 +799,15 @@ pub(crate) fn type_with(
/// Typecheck an expression and return the expression annotated with types if type-checking
/// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(hir: &Hir) -> Result<Tir, TypeError> {
+pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
type_with(&TyEnv::new(), hir, None)
}
/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<Tir, TypeError> {
+pub(crate) fn typecheck_with<'hir>(
+ hir: &'hir Hir,
+ ty: Hir,
+) -> Result<Tir<'hir>, TypeError> {
let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
type_with(&TyEnv::new(), hir, Some(ty))
}
diff --git a/tests_buffer b/tests_buffer
index 1c814ff..db63cde 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -53,6 +53,8 @@ success/
failure/
\(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
unit/FunctionTypeOutputTypeNotAType Bool -> 1
+ unit/NestedAnnotInnerWrong (0 : Bool) : Natural
+ unit/NestedAnnotOuterWrong (0 : Natural) : Bool
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:12:16 +0000