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/semantics/tck/tir.rs | 30 ++++++------------------------ dhall/src/semantics/tck/typecheck.rs | 15 +++++++++------ 2 files changed, 15 insertions(+), 30 deletions(-) (limited to 'dhall/src/semantics/tck') 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)) } -- cgit v1.2.3