From 7b649b8647c60f1c02050805520f307edff0a94f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 19:48:11 +0000 Subject: Only store type at root node in tyexpr --- dhall/src/semantics/tck/tyexpr.rs | 43 +++++++++++++++--------------------- dhall/src/semantics/tck/typecheck.rs | 12 ++++++---- 2 files changed, 26 insertions(+), 29 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index d46ab87..b49ea3e 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,39 +1,30 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value}; -use crate::syntax::{ExprKind, Span}; +use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv}; +use crate::syntax::Span; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; -#[derive(Debug, Clone)] -pub(crate) enum TyExprKind { - Var(AlphaVar), - // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), -} - -// An expression with inferred types at every node and resolved variables. +// A hir expression plus its inferred type. #[derive(Clone)] pub(crate) struct TyExpr { - kind: Box, + hir: Hir, ty: Option, - span: Span, } impl TyExpr { - pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { + pub fn new(kind: HirKind, ty: Option, span: Span) -> Self { TyExpr { - kind: Box::new(kind), + hir: Hir::new(kind, span), ty, - span, } } - pub fn kind(&self) -> &TyExprKind { - &*self.kind + pub fn kind(&self) -> &HirKind { + self.hir.kind() } pub fn span(&self) -> Span { - self.span.clone() + self.as_hir().span() } pub fn get_type(&self) -> Result { match &self.ty { @@ -41,22 +32,24 @@ impl TyExpr { None => Err(TypeError::new(TypeMessage::Sort)), } } + pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { + Ok(self.get_type()?.to_tyexpr_tyenv(env)) + } pub fn to_hir(&self) -> Hir { - let kind = match self.kind() { - TyExprKind::Var(v) => HirKind::Var(v.clone()), - TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())), - }; - Hir::new(kind, self.span()) + self.as_hir().clone() + } + pub fn as_hir(&self) -> &Hir { + &self.hir } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - self.to_hir().to_expr(opts) + self.as_hir().to_expr(opts) } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Value { - Value::new_thunk(env.into(), self.to_hir()) + self.as_hir().eval(&env.into()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c52cfda..c854552 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, - TyExpr, TyExprKind, Type, Value, ValueKind, + TyExpr, Type, Value, ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -758,18 +758,22 @@ fn type_one_layer( } }; - Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span)) + Ok(TyExpr::new( + HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), + Some(ty), + span, + )) } /// `type_with` typechecks an expressio in the provided environment. pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))), + HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) + (HirKind::Expr(ExprKind::Const(Const::Sort)), None) } HirKind::Expr(ekind) => { let ekind = match ekind { -- cgit v1.2.3