summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/binary.rs18
-rw-r--r--dhall/src/normalize.rs273
-rw-r--r--dhall/src/typecheck.rs17
-rw-r--r--dhall_core/src/core.rs32
-rw-r--r--dhall_core/src/parser.rs7
-rw-r--r--dhall_generator/src/lib.rs2
6 files changed, 175 insertions, 174 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 6d0f1e9..694043b 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -25,20 +25,20 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
String(s) => match Builtin::parse(s) {
Some(b) => Ok(Expr::Builtin(b)),
None => match s.as_str() {
- "True" => Ok(Expr::BoolLit(true)),
- "False" => Ok(Expr::BoolLit(false)),
- "Type" => Ok(Expr::Const(Const::Type)),
- "Kind" => Ok(Expr::Const(Const::Kind)),
- s => Ok(Expr::Var(V(Label::from(s), 0))),
+ "True" => Ok(BoolLit(true)),
+ "False" => Ok(BoolLit(false)),
+ "Type" => Ok(Const(Const::Type)),
+ "Kind" => Ok(Const(Const::Kind)),
+ s => Ok(Var(V(Label::from(s), 0))),
},
},
- U64(n) => Ok(Expr::Var(V(Label::from("_"), *n as usize))),
+ U64(n) => Ok(Var(V(Label::from("_"), *n as usize))),
F64(x) => Ok(DoubleLit(*x)),
Bool(b) => Ok(BoolLit(*b)),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
let l = Label::from(l.as_str());
- Ok(Expr::Var(V(l, *n as usize)))
+ Ok(Var(V(l, *n as usize)))
}
[U64(0), f, args..] => {
let f = cbor_value_to_dhall(&f)?;
@@ -46,9 +46,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
.iter()
.map(cbor_value_to_dhall)
.collect::<Result<Vec<_>, _>>()?;
- Ok(args
- .into_iter()
- .fold(f, |acc, e| (Expr::App(bx(acc), bx(e)))))
+ Ok(App(bx(f), args))
}
[U64(1), x, y] => {
let x = bx(cbor_value_to_dhall(&x)?);
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5003ccd..9f246e4 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -26,162 +26,145 @@ where
}
Annot(x, _) => normalize_whnf(x),
Note(_, e) => normalize_whnf(e),
- App(f, a) => match (normalize_whnf(f), a) {
- (Lam(x, _, b), a) => {
+ App(f, args) => match (normalize_whnf(f), args.as_slice()) {
+ (f, []) => f,
+ (App(f, args1), args2) => normalize_whnf(&App(
+ f.clone(),
+ args1.iter().chain(args2.iter()).cloned().collect(),
+ )),
+ (Lam(ref x, _, ref b), [a, rest..]) => {
// Beta reduce
- let vx0 = &V(x, 0);
+ let vx0 = &V(x.clone(), 0);
let a2 = shift::<S, S, A>(1, vx0, a);
let b2 = subst::<S, S, A>(vx0, &a2, &b);
let b3 = shift::<S, S, A>(-1, vx0, &b2);
- normalize_whnf(&b3)
+ normalize_whnf(&App(bx(b3), rest.to_vec()))
}
- (Builtin(b), a) => match (b, normalize_whnf(a)) {
- (OptionalSome, a) => OptionalLit(None, vec![a]),
- (OptionalNone, a) => OptionalLit(Some(bx(a)), vec![]),
- (NaturalIsZero, NaturalLit(n)) => BoolLit(n == 0),
- (NaturalEven, NaturalLit(n)) => BoolLit(n % 2 == 0),
- (NaturalOdd, NaturalLit(n)) => BoolLit(n % 2 != 0),
- (NaturalToInteger, NaturalLit(n)) => IntegerLit(n as isize),
- (NaturalShow, NaturalLit(n)) => TextLit(n.to_string().into()),
-
- (b, App(f, x)) => match (b, normalize_whnf(&f), x) {
- // fold/build fusion for `Natural`
- (NaturalBuild, Builtin(NaturalFold), x) => {
- normalize_whnf(&x)
- }
- (NaturalFold, Builtin(NaturalBuild), x) => {
- normalize_whnf(&x)
- }
- (b, f, x) => app(Builtin(b), app(f, *x)),
- },
- (b, a) => app(Builtin(b), a),
- },
- (App(f, x), y) => match (normalize_whnf(&f), x, y) {
- // TODO: use whnf
- (Builtin(b), x, y) => match (b, x, normalize::<S, S, A>(&y)) {
- (ListLength, _, ListLit(_, ys)) => NaturalLit(ys.len()),
- (ListHead, _, ListLit(t, ys)) => {
- OptionalLit(t, ys.into_iter().take(1).collect())
- }
- (ListLast, _, ListLit(t, ys)) => OptionalLit(
- t,
- ys.into_iter().last().into_iter().collect(),
- ),
- (ListReverse, _, ListLit(t, ys)) => {
- let mut xs = ys;
- xs.reverse();
- ListLit(t, xs)
- }
-
- // fold/build fusion for `List`
- (
- ListBuild,
- _,
- App(box App(box Builtin(ListFold), _), box e2),
- ) => normalize_whnf(&e2),
- (
- ListFold,
- _,
- App(box App(box Builtin(ListBuild), _), box e2),
- ) => normalize_whnf(&e2),
-
- // fold/build fusion for `Optional`
- (
- OptionalBuild,
- _,
- App(box App(box Builtin(OptionalFold), _), box e2),
- ) => normalize_whnf(&e2),
- (
- OptionalFold,
- _,
- App(box App(box Builtin(OptionalBuild), _), box e2),
- ) => normalize_whnf(&e2),
-
- (ListBuild, a0, k) => {
- let k = bx(k);
- let a1 = bx(shift(1, &V("a".into(), 0), &a0));
- normalize_whnf(
- &dhall_expr!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
- )
- }
- (OptionalBuild, a0, g) => {
- let g = bx(g);
- normalize_whnf(
- &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)),
- )
- }
- (b, x, y) => app(App(bx(Builtin(b)), x), y),
- },
- (App(f, x), y, z) => match (normalize_whnf(&f), x, y, z) {
- (App(f, x), y, z, w) => {
- match (normalize_whnf(&f), x, y, z, w) {
- (App(f, x), y, z, w, t) => match (
- normalize_whnf(&f),
- x,
- normalize_whnf(&y),
- z,
- w,
- t,
- ) {
- (
- Builtin(ListFold),
- _,
- ListLit(_, xs),
- _,
- cons,
- nil,
- ) => {
- let e2: Expr<_, _> = xs
- .into_iter()
- .rev()
- .fold((**nil).clone(), |acc, x| {
- let x = bx(x);
- let acc = bx(acc);
- dhall_expr!(cons x acc)
- });
- normalize_whnf(&e2)
+ // TODO: this is more normalization than needed
+ (Builtin(b), args) => match (
+ b,
+ args.iter()
+ .map(normalize_whnf)
+ .collect::<Vec<_>>()
+ .as_slice(),
+ ) {
+ (OptionalSome, [a]) => OptionalLit(None, vec![a.clone()]),
+ (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), vec![]),
+ (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0),
+ (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0),
+ (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0),
+ (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize),
+ (NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()),
+ (ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()),
+ (ListHead, [_, ListLit(t, ys)]) => OptionalLit(
+ t.clone(),
+ ys.into_iter().take(1).cloned().collect(),
+ ),
+ (ListLast, [_, ListLit(t, ys)]) => OptionalLit(
+ t.clone(),
+ ys.iter().last().cloned().into_iter().collect(),
+ ),
+ (ListReverse, [_, ListLit(t, ys)]) => {
+ let xs = ys.iter().rev().cloned().collect();
+ ListLit(t.clone(), xs)
+ }
+ (ListBuild, [a0, k]) => {
+ // fold/build fusion
+ let k = match k {
+ App(box Builtin(ListFold), args) => {
+ match args.as_slice() {
+ [_, x, rest..] => {
+ return normalize_whnf(&App(
+ bx(x.clone()),
+ rest.to_vec(),
+ ))
}
- (
- Builtin(OptionalFold),
- _,
- OptionalLit(_, xs),
- _,
- just,
- nothing,
- ) => {
- let e2: Expr<_, _> = xs.into_iter().fold(
- (**nothing).clone(),
- |_, y| {
- let y = bx(y);
- dhall_expr!(just y)
- },
- );
- normalize_whnf(&e2)
+ args => app(Builtin(ListFold), args.to_vec()),
+ }
+ }
+ k => k.clone(),
+ };
+ let k = bx(k);
+ let a0 = bx(a0.clone());
+ let a1 = bx(shift(1, &V("a".into(), 0), &a0));
+ normalize_whnf(
+ &dhall_expr!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
+ )
+ }
+ (OptionalBuild, [a0, g]) => {
+ // fold/build fusion
+ let g = match g {
+ App(box Builtin(OptionalFold), args) => {
+ match args.as_slice() {
+ [_, x, rest..] => {
+ return normalize_whnf(&App(
+ bx(x.clone()),
+ rest.to_vec(),
+ ))
}
- (f, x, y, z, w, t) => app(
- App(
- bx(App(
- bx(App(bx(App(bx(f), x)), bx(y))),
- z,
- )),
- w,
- ),
- (**t).clone(),
- ),
- },
- (f, x, y, z, w) => app(
- App(bx(App(bx(App(bx(f), x)), y)), z),
- (**w).clone(),
- ),
+ args => app(Builtin(OptionalFold), args.to_vec()),
+ }
+ }
+ g => g.clone(),
+ };
+ let g = bx(g);
+ let a0 = bx(a0.clone());
+ normalize_whnf(
+ &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)),
+ )
+ }
+ (ListFold, [_, ListLit(_, xs), _, cons, nil]) => {
+ let e2: Expr<_, _> =
+ xs.into_iter().rev().fold((*nil).clone(), |acc, x| {
+ let x = bx((x).clone());
+ let acc = bx((acc).clone());
+ let cons = bx((cons).clone());
+ dhall_expr!(cons x acc)
+ });
+ normalize_whnf(&e2)
+ }
+ // // fold/build fusion
+ // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // }
+ (OptionalFold, [_, OptionalLit(_, xs), _, just, nothing]) => {
+ let e2: Expr<_, _> =
+ xs.into_iter().fold((*nothing).clone(), |_, y| {
+ let y = bx((y).clone());
+ let just = bx((just).clone());
+ dhall_expr!(just y)
+ });
+ normalize_whnf(&e2)
+ }
+ // // fold/build fusion
+ // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // }
+ (NaturalBuild, [App(f, args)]) => {
+ match (&**f, args.as_slice()) {
+ // fold/build fusion
+ (Builtin(NaturalFold), [x, rest..]) => {
+ normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ }
+ (f, args) => {
+ app(Builtin(NaturalBuild), vec![app(f.clone(), args.to_vec())])
}
}
- (f, x, y, z) => {
- app(App(bx(App(bx(f), x)), y), (**z).clone())
+ }
+ (NaturalFold, [App(f, args)]) => {
+ match (&**f, args.as_slice()) {
+ // fold/build fusion
+ (Builtin(NaturalBuild), [x, rest..]) => {
+ normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ }
+ (f, args) => {
+ app(Builtin(NaturalFold), vec![app(f.clone(), args.to_vec())])
+ }
}
- },
- (f, x, y) => app(App(bx(f), x), (**y).clone()),
+ }
+ (b, args) => App(bx(Builtin(b)), args.to_vec()),
},
- (f, a) => app(f, (**a).clone()),
+ (f, args) => App(bx(f), args.to_vec()),
},
BoolIf(b, t, f) => match normalize_whnf(b) {
BoolLit(true) => normalize_whnf(t),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index c41bd89..ed02619 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -79,7 +79,7 @@ where
}
(&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
if go(ctx, fL, fR) {
- go(ctx, aL, aR)
+ aL.iter().zip(aR.iter()).all(|(aL, aR)| go(ctx, aL, aR))
} else {
false
}
@@ -240,8 +240,13 @@ where
Ok(k) => Ok(Const(k)),
}
}
- App(ref f, ref a) => {
- let tf = normalize(&type_with(ctx, f)?);
+ App(ref f, ref args) => {
+ let (a, args) = match args.split_last() {
+ None => return type_with(ctx, f),
+ Some(x) => x,
+ };
+ let tf =
+ normalize(&type_with(ctx, &App(f.clone(), args.to_vec()))?);
let (x, tA, tB) = match tf {
Pi(x, tA, tB) => (x, tA, tB),
_ => {
@@ -265,7 +270,7 @@ where
Err(TypeError::new(
ctx,
e,
- TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2),
+ TypeMismatch((**f).clone(), nf_A, (*a).clone(), nf_A2),
))
}
}
@@ -435,7 +440,7 @@ where
));
}
}
- Ok(App(bx(Builtin(List)), t))
+ Ok(dhall_expr!(List t))
}
Builtin(ListBuild) => Ok(dhall_expr!(
forall (a: Type) ->
@@ -504,7 +509,7 @@ where
));
}
}
- Ok(App(bx(Builtin(Optional)), t))
+ Ok(dhall_expr!(Optional t))
}
Builtin(OptionalFold) => Ok(dhall_expr!(
forall (a: Type) ->
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index ea23cbd..197907a 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -304,7 +304,7 @@ pub enum Expr<Note, Embed> {
/// `Pi x A B ~ ∀(x : A) -> B`
Pi(Label, Box<Expr<Note, Embed>>, Box<Expr<Note, Embed>>),
/// `App f A ~ f A`
- App(Box<Expr<Note, Embed>>, Box<Expr<Note, Embed>>),
+ App(Box<Expr<Note, Embed>>, Vec<Expr<Note, Embed>>),
/// `Let x Nothing r e ~ let x = r in e`
/// `Let x (Just t) r e ~ let x : t = r in e`
Let(
@@ -646,10 +646,13 @@ impl<S, A: Display> Expr<S, A> {
fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
use crate::Expr::*;
match self {
- &App(ref a, ref b) => {
+ &App(ref a, ref args) => {
a.fmt_d(f)?;
- f.write_str(" ")?;
- b.fmt_e(f)
+ for x in args {
+ f.write_str(" ")?;
+ x.fmt_e(f)?;
+ }
+ Ok(())
}
&Note(_, ref b) => b.fmt_d(f),
a => a.fmt_e(f),
@@ -842,12 +845,12 @@ where
Expr::Pi(var.into(), bx(ty.into()), bx(value.into()))
}
-pub fn app<S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<S, A>
+pub fn app<S, A, Ef, Ex>(f: Ef, x: Vec<Ex>) -> Expr<S, A>
where
Ef: Into<Expr<S, A>>,
Ex: Into<Expr<S, A>>,
{
- Expr::App(bx(f.into()), bx(x.into()))
+ Expr::App(bx(f.into()), x.into_iter().map(|x| x.into()).collect())
}
pub type Double = f64;
@@ -902,7 +905,10 @@ where
Var(V(ref x, n)) => Var(V(map_label(x), n)),
Lam(ref x, ref t, ref b) => Lam(map_label(x), bxmap(t), bxmap(b)),
Pi(ref x, ref t, ref b) => Pi(map_label(x), bxmap(t), bxmap(b)),
- App(ref f, ref a) => App(bxmap(f), bxmap(a)),
+ App(ref f, ref args) => {
+ let args = args.iter().map(&map).collect();
+ App(bxmap(f), args)
+ }
Let(ref l, ref t, ref a, ref b) => {
Let(map_label(l), opt(t), bxmap(a), bxmap(b))
}
@@ -1079,7 +1085,11 @@ pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
let tB2 = shift(d, &V(x.clone(), n2), tB);
Pi(x2.clone(), bx(tA2), bx(tB2))
}
- App(f, a) => app(shift(d, v, f), shift(d, v, a)),
+ App(f, args) => {
+ let f = shift(d, v, f);
+ let args = args.iter().map(|a| shift(d, v, a)).collect();
+ app(f, args)
+ }
Let(f, mt, r, e) => {
let n2 = if x == f { n + 1 } else { *n };
let e2 = shift(d, &V(x.clone(), n2), e);
@@ -1170,10 +1180,10 @@ where
let tA2 = subst(v, e, tA);
Pi(y.clone(), bx(tA2), bx(tB2))
}
- App(f, a) => {
+ App(f, args) => {
let f2 = subst(v, e, f);
- let a2 = subst(v, e, a);
- app(f2, a2)
+ let args = args.iter().map(|a| subst(v, e, a)).collect();
+ app(f2, args)
}
Var(v2) => {
if v == v2 {
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index ddf3f8f..02242bf 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -746,7 +746,12 @@ rule!(annotated_expression<BoxExpr>;
rule!(application_expression<BoxExpr>;
children!(first: expression, rest*: expression) => {
- rest.fold(first, |acc, e| bx(Expr::App(acc, e)))
+ let rest: Vec<_> = rest.map(|x| *x).collect();
+ if rest.is_empty() {
+ first
+ } else {
+ bx(Expr::App(first, rest))
+ }
}
);
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 512df94..0d84053 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -42,7 +42,7 @@ fn dhall_to_tokenstream(
}
App(f, a) => {
let f = dhall_to_tokenstream_bx(f, ctx);
- let a = dhall_to_tokenstream_bx(a, ctx);
+ let a = vec_to_tokenstream(a, ctx);
quote! { App(#f, #a) }
}
Const(c) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 21:35:16 +0000