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 | |
parent | da69fe3eef7e001a1a0bdd2a2f3ebefccc3426e3 (diff) |
Borrow relevant Hir from Tir
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/lib.rs | 25 | ||||
-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 |
4 files changed, 50 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)) } |