From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/builtins.rs | 2 +- dhall/src/semantics/hir.rs | 8 ++++---- dhall/src/semantics/nze/normalize.rs | 6 ++---- dhall/src/semantics/nze/value.rs | 16 +++++----------- dhall/src/semantics/resolve.rs | 4 ++-- dhall/src/semantics/tck/tyexpr.rs | 3 +-- dhall/src/semantics/tck/typecheck.rs | 7 ++----- 7 files changed, 17 insertions(+), 29 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index d9a3599..cbb5a6e 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -55,7 +55,7 @@ impl BuiltinClosure { } } -pub(crate) fn rc(x: UnspannedExpr) -> Expr { +pub(crate) fn rc(x: UnspannedExpr) -> Expr { Expr::new(x, Span::Artificial) } diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index b45851f..288031c 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -1,7 +1,7 @@ #![allow(dead_code)] use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; -use crate::syntax::{ExprKind, Span, V}; -use crate::{Expr, Normalized, NormalizedExpr, ToExprOptions}; +use crate::syntax::{Expr, ExprKind, Span, V}; +use crate::{NormalizedExpr, ToExprOptions}; /// Stores an alpha-normalized variable. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -13,8 +13,8 @@ pub struct AlphaVar { pub(crate) enum HirKind { /// A resolved variable (i.e. a DeBruijn index) Var(AlphaVar), - // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), + // Forbidden ExprKind variants: Var, Import + Expr(ExprKind), } // An expression with resolved variables and imports. diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index d12146a..03b91a5 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -6,7 +6,6 @@ use crate::semantics::{ Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind, }; use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; -use crate::Normalized; pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { match f.kind() { @@ -90,7 +89,7 @@ enum Ret<'a> { ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprKind), + Expr(ExprKind), } fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { @@ -215,7 +214,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { } pub(crate) fn normalize_one_layer( - expr: ExprKind, + expr: ExprKind, env: &NzEnv, ) -> ValueKind { use ValueKind::{ @@ -233,7 +232,6 @@ pub(crate) fn normalize_one_layer( ExprKind::Lam(..) | ExprKind::Pi(..) | ExprKind::Let(..) - | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index a60be9d..0df3c74 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -12,7 +12,7 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; -use crate::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::{NormalizedExpr, ToExprOptions}; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a Rc to share computation. @@ -34,10 +34,7 @@ pub(crate) enum Thunk { /// A completely unnormalized expression. Thunk { env: NzEnv, body: Hir }, /// A partially normalized expression that may need to go through `normalize_one_layer`. - PartialExpr { - env: NzEnv, - expr: ExprKind, - }, + PartialExpr { env: NzEnv, expr: ExprKind }, } /// An unevaluated subexpression that takes an argument. @@ -96,7 +93,7 @@ pub(crate) enum ValueKind { TextLit(TextLit), Equivalence(Value, Value), /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? - PartialExpr(ExprKind), + PartialExpr(ExprKind), } impl Value { @@ -106,7 +103,7 @@ impl Value { ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind) -> Value { + pub(crate) fn from_partial_expr(e: ExprKind) -> Value { // TODO: env let env = NzEnv::new(); ValueInternal::from_thunk( @@ -389,10 +386,7 @@ impl Thunk { fn new(env: NzEnv, body: Hir) -> Self { Thunk::Thunk { env, body } } - fn from_partial_expr( - env: NzEnv, - expr: ExprKind, - ) -> Self { + fn from_partial_expr(env: NzEnv, expr: ExprKind) -> Self { Thunk::PartialExpr { env, expr } } fn eval(self) -> ValueKind { diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs index 80e5132..fac88d2 100644 --- a/dhall/src/semantics/resolve.rs +++ b/dhall/src/semantics/resolve.rs @@ -6,7 +6,7 @@ use crate::error::{Error, ImportError}; use crate::semantics::{mkerr, Hir, HirKind, NameEnv}; use crate::syntax; use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL}; -use crate::{Normalized, Parsed, ParsedExpr, Resolved}; +use crate::{Parsed, ParsedExpr, Resolved}; type Import = syntax::Import; @@ -102,7 +102,7 @@ fn load_import(env: &mut ResolveEnv, f: &Path) -> Result { /// found imports to the provided function. fn traverse_resolve_expr( name_env: &mut NameEnv, - expr: &Expr, + expr: &Expr, f: &mut impl FnMut(Import) -> Result, ) -> Result { let kind = match expr.kind() { diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a1666a4..d46ab87 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,7 +1,6 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value}; use crate::syntax::{ExprKind, Span}; -use crate::Normalized; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; @@ -10,7 +9,7 @@ pub(crate) type Type = Value; pub(crate) enum TyExprKind { Var(AlphaVar), // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), + Expr(ExprKind), } // An expression with inferred types at every node and resolved variables. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 4e45637..f9ff3d3 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -11,7 +11,6 @@ use crate::semantics::{ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span, }; -use crate::Normalized; fn type_of_recordtype<'a>( span: Span, @@ -51,7 +50,7 @@ pub fn mkerr(x: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind, span: Span, ) -> Result { let span_err = |msg: &str| { @@ -66,9 +65,7 @@ fn type_one_layer( ExprKind::Import(..) => unreachable!( "There should remain no imports in a resolved expression" ), - ExprKind::Var(..) - | ExprKind::Const(Const::Sort) - | ExprKind::Embed(..) => unreachable!(), // Handled in type_with + ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type()?; -- cgit v1.2.3