diff options
author | Nadrieril | 2020-02-18 18:39:10 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-18 18:39:10 +0000 |
commit | ebe43bd6f1fd6feb1564ab9837399de7808b67b5 (patch) | |
tree | 57313cde64f7718c18619769bedcf399f6c7f3a5 /dhall/src/semantics | |
parent | da69fe3eef7e001a1a0bdd2a2f3ebefccc3426e3 (diff) |
Borrow relevant Hir from Tir
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/resolve/hir.rs | 20 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tir.rs | 30 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 15 |
3 files changed, 32 insertions, 33 deletions
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)) } |