From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/src/semantics/core/value.rs | 7 +--- dhall/src/semantics/phase/mod.rs | 69 +++++++++++++--------------------- dhall/src/semantics/phase/typecheck.rs | 2 +- dhall/src/semantics/tck/typecheck.rs | 9 ++++- 4 files changed, 36 insertions(+), 51 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 3dcbd38..aa819d2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -9,9 +9,7 @@ use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; use crate::semantics::phase::typecheck::{ builtin_to_value, builtin_to_value_env, const_to_value, }; -use crate::semantics::phase::{ - Normalized, NormalizedExpr, ToExprOptions, Typed, -}; +use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -207,9 +205,6 @@ impl Value { self.check_type(ty); self.to_whnf_ignore_type() } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_value(self) - } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 68c32b2..0f8194c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,6 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; +use crate::semantics::tck::tyexpr::TyExpr; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(Value); +pub struct Typed(TyExpr); /// A normalized expression. /// @@ -78,11 +79,14 @@ impl Parsed { } impl Resolved { - pub fn typecheck(self) -> Result { - Ok(typecheck::typecheck(self.0)?.into_typed()) + pub fn typecheck(&self) -> Result { + Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) + Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( + &self.0, + ty.to_expr(), + )?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -97,43 +101,22 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(mut self) -> Normalized { - self.0.normalize_mut(); - Normalized(self.0) - } - - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) + pub fn normalize(&self) -> Normalized { + let mut val = self.0.normalize_whnf_noenv(); + val.normalize_mut(); + Normalized(val) } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self) -> ResolvedExpr { + fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } - /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the - /// process. - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + pub(crate) fn get_type(&self) -> Result { + Ok(Normalized(self.0.get_type()?)) } } @@ -142,19 +125,19 @@ impl Normalized { binary::encode(&self.to_expr()) } + /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr() + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) } + /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr_alpha() - } - pub(crate) fn to_typed(&self) -> Typed { - Typed(self.0.clone()) - } - pub(crate) fn into_typed(self) -> Typed { - Typed(self.0) + self.0.to_expr(ToExprOptions { + alpha: true, + normalize: false, + }) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.0 == other.0 + self.normalize() == other.normalize() } } impl Display for Typed { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f559323..6de65e8 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -336,7 +336,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { // )) Ok(e) } - Embed(p) => Ok(p.clone().into_typed().into_value()), + Embed(p) => Ok(p.clone().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a83f175..5880d92 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -677,7 +677,7 @@ pub(crate) fn type_with( (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } ExprKind::Embed(p) => { - return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv()) + return Ok(p.clone().into_value().to_tyexpr_noenv()) } ekind => { let ekind = ekind.traverse_ref(|e| type_with(env, e))?; @@ -692,3 +692,10 @@ pub(crate) fn type_with( pub(crate) fn typecheck(e: &Expr) -> Result { type_with(&TyEnv::new(), e) } + +pub(crate) fn typecheck_with( + expr: &Expr, + ty: Expr, +) -> Result { + typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty))) +} -- cgit v1.2.3