From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:39:10 +0000 Subject: Borrow relevant Hir from Tir --- dhall/src/lib.rs | 25 ++++++++++++++++++------- dhall/src/semantics/resolve/hir.rs | 20 +++++++++++++++++--- dhall/src/semantics/tck/tir.rs | 30 ++++++------------------------ dhall/src/semantics/tck/typecheck.rs | 15 +++++++++------ tests_buffer | 2 ++ 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 { - Ok(Typed(typecheck(&self.0)?)) + Ok(Typed::from_tir(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - 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 { - 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 { + pub fn typecheck<'hir>( + &'hir self, + env: &TyEnv, + ) -> Result, TypeError> { type_with(env, self, None) } @@ -78,6 +81,17 @@ impl Hir { pub fn eval(&self, env: impl Into) -> 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 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(span: Span, msg: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind>, span: Span, ) -> Result { 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, -) -> Result { +) -> Result, 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 { +pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result, 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 { +pub(crate) fn typecheck_with<'hir>( + hir: &'hir Hir, + ty: Hir, +) -> Result, 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 -- cgit v1.2.3