summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/normalize.rs97
1 files changed, 55 insertions, 42 deletions
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())
}