diff options
| author | Nadrieril | 2020-02-13 19:48:11 +0000 | 
|---|---|---|
| committer | Nadrieril | 2020-02-13 19:48:11 +0000 | 
| commit | 7b649b8647c60f1c02050805520f307edff0a94f (patch) | |
| tree | 73a6a38e430ba257228fd04ee69fc4f5e138ad7f /dhall/src/semantics/tck | |
| parent | 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 (diff) | |
Only store type at root node in tyexpr
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 43 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 12 | 
2 files changed, 26 insertions, 29 deletions
| 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<TyExpr>), -} - -// 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<TyExprKind>, +    hir: Hir,      ty: Option<Type>, -    span: Span,  }  impl TyExpr { -    pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self { +    pub fn new(kind: HirKind, ty: Option<Type>, 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<Type, TypeError> {          match &self.ty { @@ -41,22 +32,24 @@ impl TyExpr {              None => Err(TypeError::new(TypeMessage::Sort)),          }      } +    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> { +        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<NzEnv>) -> 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<TyExpr, TypeError> {      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 { | 
