summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/expr.rs2
-rw-r--r--dhall/src/normalize.rs165
-rw-r--r--dhall/src/typecheck.rs12
3 files changed, 79 insertions, 100 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index e7beafa..b2f2bec 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -47,7 +47,7 @@ derive_other_traits!(Typed);
#[derive(Debug, Clone)]
pub(crate) struct PartiallyNormalized<'a>(
- pub(crate) crate::normalize::Value<crate::normalize::WHNF>,
+ pub(crate) crate::normalize::Value,
pub(crate) Option<Type<'static>>,
pub(crate) PhantomData<&'a ()>,
);
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d58ea7a..3b21b86 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -70,12 +70,12 @@ impl<'a> PartiallyNormalized<'a> {
self.2,
)
}
- pub(crate) fn into_whnf(self) -> Value<WHNF> {
+ pub(crate) fn into_whnf(self) -> Value {
self.0
}
}
-fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
+fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
use dhall_core::Builtin::*;
use Value::*;
@@ -264,7 +264,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value<WHNF>>) -> Value<WHNF> {
#[derive(Debug, Clone)]
enum EnvItem {
- Expr(Value<WHNF>),
+ Expr(Value),
Skip(V<Label>),
}
@@ -302,7 +302,7 @@ impl NormalizationContext {
fn new() -> Self {
NormalizationContext(Rc::new(Context::new()))
}
- fn insert(&self, x: &Label, e: Value<WHNF>) -> Self {
+ fn insert(&self, x: &Label, e: Value) -> Self {
NormalizationContext(Rc::new(
self.0.insert(x.clone(), EnvItem::Expr(e)),
))
@@ -314,7 +314,7 @@ impl NormalizationContext {
.insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
))
}
- fn lookup(&self, var: &V<Label>) -> Value<WHNF> {
+ fn lookup(&self, var: &V<Label>) -> Value {
let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Expr(e)) => e.clone(),
@@ -355,53 +355,41 @@ impl NormalizationContext {
}
}
+/// A semantic value.
#[derive(Debug, Clone)]
-pub(crate) struct WHNF;
-#[derive(Debug, Clone)]
-pub(crate) enum NF {}
-
-/// A semantic value. `Form` should be either `WHNF` or `NF`.
-/// `NF` stands for Normal Form and indicates that all subexpressions are normalized.
-/// `WHNF` stands for Weak Head Normal-Form and indicates that subexpressions may not be normalized.
-///
-/// Weak Head Normal-Form means that the expression is normalized as
-/// little as possible, but just enough to know the first constructor of the normal form. This is
-/// identical to normal form for simple types like integers, but for e.g. a record literal
-/// this means knowing just the field names.
-#[derive(Debug, Clone)]
-pub(crate) enum Value<Form> {
+pub(crate) enum Value {
/// Closures
- Lam(Label, Thunk<Form>, Thunk<Form>),
- AppliedBuiltin(Builtin, Vec<Value<Form>>),
+ Lam(Label, Thunk, Thunk),
+ AppliedBuiltin(Builtin, Vec<Value>),
/// `λ(x: a) -> Some x`
- OptionalSomeClosure(TypeThunk<Form>),
+ OptionalSomeClosure(TypeThunk),
/// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
/// `λ(xs : List a) -> [ x ] # xs`
- ListConsClosure(TypeThunk<Form>, Option<Thunk<Form>>),
+ ListConsClosure(TypeThunk, Option<Thunk>),
/// `λ(x : Natural) -> x + 1`
NaturalSuccClosure,
- Pi(Label, TypeThunk<Form>, TypeThunk<Form>),
+ Pi(Label, TypeThunk, TypeThunk),
Var(V<Label>),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
IntegerLit(Integer),
- EmptyOptionalLit(TypeThunk<Form>),
- NEOptionalLit(Thunk<Form>),
- EmptyListLit(TypeThunk<Form>),
- NEListLit(Vec<Thunk<Form>>),
- RecordLit(BTreeMap<Label, Thunk<Form>>),
- RecordType(BTreeMap<Label, TypeThunk<Form>>),
- UnionType(BTreeMap<Label, Option<TypeThunk<Form>>>),
- UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk<Form>>>),
- UnionLit(Label, Thunk<Form>, BTreeMap<Label, Option<TypeThunk<Form>>>),
- TextLit(Vec<InterpolatedTextContents<Thunk<Form>>>),
+ EmptyOptionalLit(TypeThunk),
+ NEOptionalLit(Thunk),
+ EmptyListLit(TypeThunk),
+ NEListLit(Vec<Thunk>),
+ RecordLit(BTreeMap<Label, Thunk>),
+ RecordType(BTreeMap<Label, TypeThunk>),
+ UnionType(BTreeMap<Label, Option<TypeThunk>>),
+ UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
+ UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
+ TextLit(Vec<InterpolatedTextContents<Thunk>>),
/// This must not contain a value captured by one of the variants above.
Expr(OutputSubExpr),
}
-impl Value<NF> {
+impl Value {
/// Convert the value back to a (normalized) syntactic expression
pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
match self {
@@ -493,7 +481,7 @@ impl Value<NF> {
)),
Value::TextLit(elts) => {
fn normalize_textlit(
- elts: Vec<InterpolatedTextContents<Thunk<NF>>>,
+ elts: Vec<InterpolatedTextContents<Thunk>>,
) -> InterpolatedText<OutputSubExpr> {
elts.into_iter()
.flat_map(|contents| {
@@ -523,14 +511,8 @@ impl Value<NF> {
Value::Expr(e) => e,
}
}
-}
-
-impl Value<WHNF> {
- pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
- self.normalize().normalize_to_expr()
- }
- pub(crate) fn normalize(&self) -> Value<NF> {
+ pub(crate) fn normalize(&self) -> Value {
match self {
Value::Lam(x, t, e) => {
Value::Lam(x.clone(), t.normalize(), e.normalize())
@@ -613,7 +595,7 @@ impl Value<WHNF> {
}
/// Apply to a value
- pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
+ pub(crate) fn app(self, val: Value) -> Value {
match (self, val) {
(Value::Lam(x, _, e), val) => {
let val =
@@ -651,7 +633,7 @@ impl Value<WHNF> {
}
}
- pub(crate) fn from_builtin(b: Builtin) -> Value<WHNF> {
+ pub(crate) fn from_builtin(b: Builtin) -> Value {
Value::AppliedBuiltin(b, vec![])
}
@@ -846,41 +828,44 @@ impl Value<WHNF> {
/// Contains either a (partially) normalized value or a
/// non-normalized value alongside a normalization context.
#[derive(Debug, Clone)]
-pub(crate) enum Thunk<Form> {
- Value(Box<Value<Form>>),
- Unnormalized(Form, NormalizationContext, InputSubExpr),
+pub(crate) enum Thunk {
+ // Normal form, i.e. completely normalized
+ NF(Box<Value>),
+ // Weak Head Normal Form, i.e. subexpressions may not be normalized
+ WHNF(Box<Value>),
+ Unnormalized(NormalizationContext, InputSubExpr),
}
-impl Thunk<WHNF> {
- fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk<WHNF> {
- Thunk::Unnormalized(WHNF, ctx, e)
+impl Thunk {
+ fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+ Thunk::Unnormalized(ctx, e)
}
- fn from_whnf(v: Value<WHNF>) -> Thunk<WHNF> {
- Thunk::Value(Box::new(v))
+ fn from_whnf(v: Value) -> Thunk {
+ Thunk::WHNF(Box::new(v))
}
- pub(crate) fn normalize_whnf(&self) -> Value<WHNF> {
+ pub(crate) fn normalize_whnf(&self) -> Value {
match self {
- Thunk::Value(v) => (**v).clone(),
- Thunk::Unnormalized(_, ctx, e) => {
+ Thunk::WHNF(v) => (**v).clone(),
+ Thunk::NF(v) => (**v).clone(),
+ Thunk::Unnormalized(ctx, e) => {
normalize_whnf(ctx.clone(), e.clone())
}
}
}
- fn normalize(&self) -> Thunk<NF> {
- Thunk::Value(Box::new(self.normalize_whnf().normalize()))
+ fn normalize(&self) -> Thunk {
+ Thunk::NF(Box::new(self.normalize_whnf().normalize()))
}
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
- Thunk::Value(v) => Thunk::Value(Box::new(v.shift(delta, var))),
- Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
- marker.clone(),
- ctx.shift(delta, var),
- e.clone(),
- ),
+ Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.shift(delta, var))),
+ Thunk::NF(v) => Thunk::NF(Box::new(v.shift(delta, var))),
+ Thunk::Unnormalized(ctx, e) => {
+ Thunk::Unnormalized(ctx.shift(delta, var), e.clone())
+ }
}
}
@@ -890,50 +875,49 @@ impl Thunk<WHNF> {
val: &PartiallyNormalized<'static>,
) -> Self {
match self {
- Thunk::Value(v) => Thunk::Value(Box::new(v.subst_shift(var, val))),
- Thunk::Unnormalized(marker, ctx, e) => Thunk::Unnormalized(
- marker.clone(),
- ctx.subst_shift(var, val),
- e.clone(),
- ),
+ Thunk::WHNF(v) => Thunk::WHNF(Box::new(v.subst_shift(var, val))),
+ Thunk::NF(v) => Thunk::NF(Box::new(v.subst_shift(var, val))),
+ Thunk::Unnormalized(ctx, e) => {
+ Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+ }
}
}
-}
-impl Thunk<NF> {
- pub(crate) fn to_nf(&self) -> Value<NF> {
+ pub(crate) fn to_nf(&self) -> Value {
match self {
- Thunk::Value(v) => (**v).clone(),
- Thunk::Unnormalized(m, _, _) => match *m {},
+ Thunk::NF(v) => (**v).clone(),
+ Thunk::WHNF(_) | Thunk::Unnormalized(_, _) => {
+ self.normalize_whnf().normalize()
+ }
}
}
}
/// A thunk in type position.
#[derive(Debug, Clone)]
-pub(crate) enum TypeThunk<Form> {
- Thunk(Thunk<Form>),
+pub(crate) enum TypeThunk {
+ Thunk(Thunk),
Type(Type<'static>),
}
-impl TypeThunk<WHNF> {
- fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk<WHNF> {
+impl TypeThunk {
+ fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk {
TypeThunk::from_thunk(Thunk::new(ctx, e))
}
- fn from_whnf(v: Value<WHNF>) -> TypeThunk<WHNF> {
+ fn from_whnf(v: Value) -> TypeThunk {
TypeThunk::from_thunk(Thunk::from_whnf(v))
}
- fn from_thunk(th: Thunk<WHNF>) -> TypeThunk<WHNF> {
+ fn from_thunk(th: Thunk) -> TypeThunk {
TypeThunk::Thunk(th)
}
- pub(crate) fn from_type(t: Type<'static>) -> TypeThunk<WHNF> {
+ pub(crate) fn from_type(t: Type<'static>) -> TypeThunk {
TypeThunk::Type(t)
}
- fn normalize(&self) -> TypeThunk<NF> {
+ fn normalize(&self) -> TypeThunk {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
TypeThunk::Type(t) => TypeThunk::Type(t.clone()),
@@ -957,10 +941,8 @@ impl TypeThunk<WHNF> {
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
}
}
-}
-impl TypeThunk<NF> {
- pub(crate) fn to_nf(&self) -> Value<NF> {
+ pub(crate) fn to_nf(&self) -> Value {
match self {
TypeThunk::Thunk(th) => th.to_nf(),
// TODO: let's hope for the best with the unwrap
@@ -975,10 +957,7 @@ impl TypeThunk<NF> {
}
/// Reduces the imput expression to Value. See doc on `Value` for details.
-fn normalize_whnf(
- ctx: NormalizationContext,
- expr: InputSubExpr,
-) -> Value<WHNF> {
+fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
match expr.as_ref() {
ExprF::Var(v) => ctx.lookup(&v),
ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
@@ -1074,7 +1053,7 @@ fn normalize_whnf(
}
expr => {
// Recursively normalize subexpressions
- let expr: ExprF<Value<WHNF>, Label, X, X> = expr
+ let expr: ExprF<Value, Label, X, X> = expr
.map_ref_with_special_handling_of_binders(
|e| normalize_whnf(ctx.clone(), e.clone()),
|x, e| normalize_whnf(ctx.skip(x), e.clone()),
@@ -1089,7 +1068,7 @@ fn normalize_whnf(
}
/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
+fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
use dhall_core::BinOp::*;
use Value::*;
@@ -1173,7 +1152,7 @@ fn normalize_last_layer(expr: ExprF<Value<WHNF>, Label, X, X>) -> Value<WHNF> {
Expr(rc(ExprF::Merge(
RecordLit(handlers).normalize_to_expr(),
e.normalize_to_expr(),
- t.map(<Value<WHNF>>::normalize_to_expr),
+ t.map(<Value>::normalize_to_expr),
)))
}
// Couldn't do anything useful, so just normalize subexpressions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 4f0dcd9..38da955 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,7 @@ use std::fmt;
use std::marker::PhantomData;
use crate::expr::*;
-use crate::normalize::{TypeThunk, Value, WHNF};
+use crate::normalize::{TypeThunk, Value};
use crate::traits::DynamicType;
use dhall_core;
use dhall_core::context::Context;
@@ -99,7 +99,7 @@ impl<'a> Type<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
self.0.into_normalized()
}
- fn normalize_whnf(self) -> Result<Value<WHNF>, TypeError> {
+ fn normalize_whnf(self) -> Result<Value, TypeError> {
self.0.normalize_whnf()
}
pub(crate) fn partially_normalize(
@@ -110,7 +110,7 @@ impl<'a> Type<'a> {
fn internal(&self) -> &TypeInternal<'a> {
&self.0
}
- fn internal_whnf(&self) -> Option<&Value<WHNF>> {
+ fn internal_whnf(&self) -> Option<&Value> {
self.0.whnf()
}
pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -143,7 +143,7 @@ impl Type<'static> {
}
}
-impl TypeThunk<WHNF> {
+impl TypeThunk {
fn normalize_to_type(
self,
ctx: &TypecheckContext,
@@ -178,7 +178,7 @@ impl<'a> TypeInternal<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
Ok(self.partially_normalize()?.normalize())
}
- fn normalize_whnf(self) -> Result<Value<WHNF>, TypeError> {
+ fn normalize_whnf(self) -> Result<Value, TypeError> {
Ok(self.partially_normalize()?.into_whnf())
}
fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> {
@@ -193,7 +193,7 @@ impl<'a> TypeInternal<'a> {
}
})
}
- fn whnf(&self) -> Option<&Value<WHNF>> {
+ fn whnf(&self) -> Option<&Value> {
match self {
TypeInternal::PNzed(e) => Some(&e.0),
_ => None,