summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/value.rs95
-rw-r--r--dhall/src/core/var.rs6
-rw-r--r--dhall/src/phase/normalize.rs97
3 files changed, 62 insertions, 136 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 845596b..036a20c 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -30,13 +30,6 @@ pub enum Value {
Pi(AlphaLabel, TypedThunk, TypedThunk),
// Invariant: the evaluation must not be able to progress further.
AppliedBuiltin(Builtin, Vec<Thunk>),
- /// `λ(x: a) -> Some x`
- OptionalSomeClosure(TypedThunk),
- /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
- /// `λ(xs : List a) -> [ x ] # xs`
- ListConsClosure(TypedThunk, Option<Thunk>),
- /// `λ(x : Natural) -> x + 1`
- NaturalSuccClosure,
Var(AlphaVar),
Const(Const),
@@ -74,47 +67,6 @@ impl Value {
/// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
/// if alpha is `true`
pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
- // Ad-hoc macro to help construct the unapplied closures
- macro_rules! make_expr {
- (Natural) => { rc(ExprF::Builtin(Builtin::Natural)) };
- (var($var:ident)) => {
- rc(ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0)))
- };
- ($var:ident) => { $var };
- (List $($rest:tt)*) => {
- rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::List)),
- make_expr!($($rest)*)
- ))
- };
- (Some $($rest:tt)*) => {
- rc(ExprF::SomeLit(
- make_expr!($($rest)*)
- ))
- };
- (1 + $($rest:tt)*) => {
- rc(ExprF::BinOp(
- dhall_syntax::BinOp::NaturalPlus,
- rc(ExprF::NaturalLit(1)),
- make_expr!($($rest)*)
- ))
- };
- ([ $($head:tt)* ] # $($tail:tt)*) => {
- rc(ExprF::BinOp(
- dhall_syntax::BinOp::ListAppend,
- rc(ExprF::NEListLit(vec![make_expr!($($head)*)])),
- make_expr!($($tail)*)
- ))
- };
- (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
- rc(ExprF::Lam(
- stringify!($var).into(),
- make_expr!($($ty)*),
- make_expr!($($rest)*)
- ))
- };
- }
-
match self {
Value::Lam(x, t, e) => rc(ExprF::Lam(
x.to_label_maybe_alpha(alpha),
@@ -131,27 +83,6 @@ impl Value {
}
e
}
- Value::OptionalSomeClosure(n) => {
- let a = n.normalize_to_expr_maybe_alpha(alpha);
- make_expr!(λ(x: a) -> Some var(x))
- }
- Value::ListConsClosure(a, None) => {
- // Avoid accidental capture of the new `x` variable
- let a1 = a.under_binder(Label::from("x"));
- let a1 = a1.normalize_to_expr_maybe_alpha(alpha);
- let a = a.normalize_to_expr_maybe_alpha(alpha);
- make_expr!(λ(x : a) -> λ(xs : List a1) -> [ var(x) ] # var(xs))
- }
- Value::ListConsClosure(n, Some(v)) => {
- // Avoid accidental capture of the new `xs` variable
- let v = v.under_binder(Label::from("xs"));
- let v = v.normalize_to_expr_maybe_alpha(alpha);
- let a = n.normalize_to_expr_maybe_alpha(alpha);
- make_expr!(λ(xs : List a) -> [ v ] # var(xs))
- }
- Value::NaturalSuccClosure => {
- make_expr!(λ(x : Natural) -> 1 + var(x))
- }
Value::Pi(x, t, e) => rc(ExprF::Pi(
x.to_label_maybe_alpha(alpha),
t.normalize_to_expr_maybe_alpha(alpha),
@@ -257,8 +188,7 @@ impl Value {
pub fn normalize_mut(&mut self) {
match self {
- Value::NaturalSuccClosure
- | Value::Var(_)
+ Value::Var(_)
| Value::Const(_)
| Value::BoolLit(_)
| Value::NaturalLit(_)
@@ -266,7 +196,6 @@ impl Value {
| Value::DoubleLit(_) => {}
Value::EmptyOptionalLit(tth)
- | Value::OptionalSomeClosure(tth)
| Value::EmptyListLit(tth) => {
tth.normalize_mut();
}
@@ -287,12 +216,6 @@ impl Value {
x.normalize_mut();
}
}
- Value::ListConsClosure(t, v) => {
- t.normalize_mut();
- for x in v.iter_mut() {
- x.normalize_mut();
- }
- }
Value::NEListLit(elts) => {
for x in elts.iter_mut() {
x.normalize_mut();
@@ -375,14 +298,6 @@ impl Shift for Value {
.map(|v| Ok(v.shift(delta, var)?))
.collect::<Result<_, _>>()?,
),
- Value::NaturalSuccClosure => Value::NaturalSuccClosure,
- Value::OptionalSomeClosure(tth) => {
- Value::OptionalSomeClosure(tth.shift(delta, var)?)
- }
- Value::ListConsClosure(t, v) => Value::ListConsClosure(
- t.shift(delta, var)?,
- v.as_ref().map(|v| Ok(v.shift(delta, var)?)).transpose()?,
- ),
Value::Pi(x, t, e) => Value::Pi(
x.clone(),
t.shift(delta, var)?,
@@ -516,14 +431,6 @@ impl Subst<Typed> for Value {
t.subst_shift(var, val),
e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
),
- Value::NaturalSuccClosure => Value::NaturalSuccClosure,
- Value::OptionalSomeClosure(tth) => {
- Value::OptionalSomeClosure(tth.subst_shift(var, val))
- }
- Value::ListConsClosure(t, v) => Value::ListConsClosure(
- t.subst_shift(var, val),
- v.as_ref().map(|v| v.subst_shift(var, val)),
- ),
Value::Pi(x, t, e) => Value::Pi(
x.clone(),
t.subst_shift(var, val),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 35bff80..0faa091 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -67,6 +67,12 @@ impl AlphaVar {
alpha: None,
}
}
+ pub fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
+ AlphaVar {
+ normal,
+ alpha: Some(V((), alpha)),
+ }
+ }
}
impl AlphaLabel {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index adbcb02..f11269e 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,19 +1,61 @@
use std::collections::HashMap;
use dhall_syntax::{
- BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents,
+ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
NaiveDouble,
};
use crate::core::context::NormalizationContext;
use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
-use crate::core::var::Subst;
+use crate::core::var::{Shift, Subst};
use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
pub type InputSubExpr = ResolvedSubExpr;
pub type OutputSubExpr = NormalizedSubExpr;
+// Ad-hoc macro to help construct closures
+macro_rules! make_closure {
+ (#$var:ident) => { $var.clone() };
+ (var($var:ident, $n:expr)) => {{
+ let var = crate::core::var::AlphaVar::from_var_and_alpha(
+ Label::from(stringify!($var)).into(),
+ $n
+ );
+ Value::Var(var).into_thunk()
+ }};
+ (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
+ Value::Lam(
+ Label::from(stringify!($var)).into(),
+ TypedThunk::from_thunk_untyped(make_closure!($($ty)*)),
+ make_closure!($($rest)*),
+ ).into_thunk()
+ };
+ (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() };
+ (List $($rest:tt)*) => {
+ Value::from_builtin(Builtin::List)
+ .app_thunk(make_closure!($($rest)*))
+ .into_thunk()
+ };
+ (Some $($rest:tt)*) => {
+ Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+ };
+ (1 + $($rest:tt)*) => {
+ Value::PartialExpr(ExprF::BinOp(
+ dhall_syntax::BinOp::NaturalPlus,
+ make_closure!($($rest)*),
+ Thunk::from_value(Value::NaturalLit(1)),
+ )).into_thunk()
+ };
+ ([ $($head:tt)* ] # $($tail:tt)*) => {
+ Value::PartialExpr(ExprF::BinOp(
+ dhall_syntax::BinOp::ListAppend,
+ Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+ make_closure!($($tail)*),
+ )).into_thunk()
+ };
+}
+
#[allow(clippy::cognitive_complexity)]
pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
use dhall_syntax::Builtin::*;
@@ -179,10 +221,15 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Ok((
r,
f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
- .app_val(ListConsClosure(
- TypedThunk::from_thunk(t.clone()),
- None,
- ))
+ .app_thunk({
+ // Move `t` under new `x` variable
+ let t1 = t.under_binder(Label::from("x"));
+ make_closure!(
+ λ(x : #t) ->
+ λ(xs : List #t1) ->
+ [ var(x, 1) ] # var(xs, 0)
+ )
+ })
.app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
)),
},
@@ -214,9 +261,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Ok((
r,
f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
- .app_val(OptionalSomeClosure(TypedThunk::from_thunk(
- t.clone(),
- )))
+ .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
.app_val(EmptyOptionalLit(TypedThunk::from_thunk(
t.clone(),
))),
@@ -240,7 +285,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
_ => Ok((
r,
f.app_val(Value::from_builtin(Natural))
- .app_val(NaturalSuccClosure)
+ .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
.app_val(NaturalLit(0)),
)),
},
@@ -284,38 +329,6 @@ pub fn apply_any(f: Thunk, a: Thunk) -> Value {
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args)
}
- Value::OptionalSomeClosure(_) => Value::NEOptionalLit(a),
- Value::ListConsClosure(t, None) => {
- Value::ListConsClosure(t.clone(), Some(a))
- }
- Value::ListConsClosure(_, Some(x)) => {
- let a_borrow = a.as_value();
- match &*a_borrow {
- Value::EmptyListLit(_) => Value::NEListLit(vec![x.clone()]),
- Value::NEListLit(xs) => {
- use std::iter::once;
- let xs =
- once(x.clone()).chain(xs.iter().cloned()).collect();
- Value::NEListLit(xs)
- }
- _ => {
- drop(f_borrow);
- drop(a_borrow);
- fallback(f, a)
- }
- }
- }
- Value::NaturalSuccClosure => {
- let a_borrow = a.as_value();
- match &*a_borrow {
- Value::NaturalLit(n) => Value::NaturalLit(n + 1),
- _ => {
- drop(f_borrow);
- drop(a_borrow);
- fallback(f, a)
- }
- }
- }
Value::UnionConstructor(l, kts) => {
Value::UnionLit(l.clone(), a, kts.clone())
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:14:36 +0000