summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/builtins.rs2
-rw-r--r--dhall/src/semantics/hir.rs8
-rw-r--r--dhall/src/semantics/nze/normalize.rs6
-rw-r--r--dhall/src/semantics/nze/value.rs16
-rw-r--r--dhall/src/semantics/resolve.rs4
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs7
7 files changed, 17 insertions, 29 deletions
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<Value> {
}
}
-pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+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<Hir, Normalized>),
+ // Forbidden ExprKind variants: Var, Import
+ Expr(ExprKind<Hir>),
}
// 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<Value, Normalized>),
+ Expr(ExprKind<Value>),
}
fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
@@ -215,7 +214,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
}
pub(crate) fn normalize_one_layer(
- expr: ExprKind<Value, Normalized>,
+ expr: ExprKind<Value>,
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<RefCell> 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<Value, Normalized>,
- },
+ PartialExpr { env: NzEnv, expr: ExprKind<Value> },
}
/// 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<Value, Normalized>),
+ PartialExpr(ExprKind<Value>),
}
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, Normalized>) -> Value {
+ pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> 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<Value, Normalized>,
- ) -> Self {
+ fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> 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<Hir>;
@@ -102,7 +102,7 @@ fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Hir, Error> {
/// found imports to the provided function.
fn traverse_resolve_expr(
name_env: &mut NameEnv,
- expr: &Expr<Normalized>,
+ expr: &Expr,
f: &mut impl FnMut(Import) -> Result<Hir, Error>,
) -> Result<Hir, Error> {
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<TyExpr, Normalized>),
+ Expr(ExprKind<TyExpr>),
}
// 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<T, S: ToString>(x: S) -> Result<T, TypeError> {
/// layer.
fn type_one_layer(
env: &TyEnv,
- ekind: ExprKind<TyExpr, Normalized>,
+ ekind: ExprKind<TyExpr>,
span: Span,
) -> Result<TyExpr, TypeError> {
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()?;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 01:35:43 +0000