summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/mod.rs8
-rw-r--r--dhall/src/phase/normalize.rs22
-rw-r--r--dhall/src/phase/typecheck.rs10
3 files changed, 6 insertions, 34 deletions
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 778f990..5a6d4db 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -76,11 +76,6 @@ impl Resolved {
pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
typecheck::typecheck_with(self, ty)
}
- /// Pretends this expression has been typechecked. Use with care.
- #[allow(dead_code)]
- pub(crate) fn skip_typecheck(self) -> Typed {
- typecheck::skip_typecheck(self)
- }
}
impl Typed {
@@ -168,9 +163,6 @@ impl Normalized {
pub(crate) fn to_type(&self) -> Type {
self.0.to_type()
}
- pub(crate) fn to_value(&self) -> Value {
- self.0.to_value()
- }
pub(crate) fn into_typed(self) -> Typed {
self.0
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fd0197d..2a2bf3e 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,13 +5,11 @@ use dhall_syntax::{
NaiveDouble,
};
-use crate::core::context::NormalizationContext;
use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Typed};
-pub(crate) type InputSubExpr = ResolvedSubExpr;
pub(crate) type OutputSubExpr = NormalizedSubExpr;
// Ad-hoc macro to help construct closures
@@ -381,24 +379,6 @@ pub(crate) fn squash_textlit(
ret
}
-/// Reduces the imput expression to a Value. Evaluates as little as possible.
-pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
- match expr.as_ref() {
- ExprF::Embed(e) => return e.to_value(),
- ExprF::Var(v) => return ctx.lookup(v),
- _ => {}
- }
-
- // Thunk subexpressions
- let expr: ExprF<Thunk, Normalized> =
- expr.as_ref().map_ref_with_special_handling_of_binders(
- |e| Thunk::new(ctx.clone(), e.clone()),
- |x, e| Thunk::new(ctx.skip(x), e.clone()),
- );
-
- normalize_one_layer(expr)
-}
-
// Small helper enum to avoid repetition
enum Ret<'a> {
Value(Value),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 7bbad38..dd6da70 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -4,7 +4,7 @@ use dhall_syntax::{
rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
};
-use crate::core::context::{NormalizationContext, TypecheckContext};
+use crate::core::context::TypecheckContext;
use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::{Shift, Subst};
@@ -1009,11 +1009,11 @@ pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
type_of(e.0)
}
-pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
+pub(crate) fn typecheck_with(
+ e: Resolved,
+ ty: &Type,
+) -> Result<Typed, TypeError> {
let expr: SubExpr<_> = e.0;
let ty: SubExpr<_> = ty.to_expr();
type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
-pub(crate) fn skip_typecheck(e: Resolved) -> Typed {
- Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0))
-}