summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/binary.rs14
-rw-r--r--dhall/src/expr.rs3
-rw-r--r--dhall/src/lib.rs1
-rw-r--r--dhall/src/normalize.rs1093
-rw-r--r--dhall/src/typecheck.rs90
5 files changed, 806 insertions, 395 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index c12aa2a..7ded3a5 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -42,12 +42,12 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
Var(V(l, *n as usize))
}
[U64(0), f, args..] => {
- let f = cbor_value_to_dhall(&f)?;
- let args = args
- .iter()
- .map(cbor_value_to_dhall)
- .collect::<Result<Vec<_>, _>>()?;
- App(f, args)
+ let mut f = cbor_value_to_dhall(&f)?;
+ for a in args {
+ let a = cbor_value_to_dhall(&a)?;
+ f = rc(App(f, a))
+ }
+ return Ok(f);
}
[U64(1), x, y] => {
let x = cbor_value_to_dhall(&x)?;
@@ -111,7 +111,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
}
[U64(5), Null, x] => {
let x = cbor_value_to_dhall(&x)?;
- NEOptionalLit(x)
+ SomeLit(x)
}
[U64(5), t, x] => {
let x = cbor_value_to_dhall(&x)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5885359..bb1a4e4 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -107,9 +107,6 @@ impl<'a> Typed<'a> {
pub(crate) fn as_expr(&self) -> &SubExpr<X, Normalized<'a>> {
&self.0
}
- pub(crate) fn into_expr(self) -> SubExpr<X, Normalized<'a>> {
- self.0
- }
}
#[doc(hidden)]
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 544df6e..c85b962 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -3,6 +3,7 @@
#![feature(slice_patterns)]
#![feature(label_break_value)]
#![feature(non_exhaustive)]
+#![feature(bind_by_move_pattern_guards)]
#![cfg_attr(test, feature(custom_inner_attributes))]
#![allow(
clippy::type_complexity,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 1561f01..f092c4d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1,8 +1,18 @@
#![allow(non_snake_case)]
-use crate::expr::*;
-use dhall_core::*;
+use std::collections::BTreeMap;
+use std::rc::Rc;
+
+use dhall_core::context::Context;
+use dhall_core::{
+ rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText,
+ InterpolatedTextContents, Label, Natural, SubExpr, V, X,
+};
use dhall_generator as dhall;
-use std::fmt;
+
+use crate::expr::{Normalized, Typed};
+
+type InputSubExpr = SubExpr<X, Normalized<'static>>;
+type OutputSubExpr = SubExpr<X, X>;
impl<'a> Typed<'a> {
pub fn normalize(self) -> Normalized<'a> {
@@ -19,323 +29,762 @@ impl<'a> Typed<'a> {
}
}
-fn apply_builtin<N, E>(b: Builtin, args: &[Expr<N, E>]) -> WhatNext<N, E>
-where
- N: fmt::Debug + Clone,
- E: fmt::Debug + Clone,
-{
+fn shift0_mut<N, E>(delta: isize, label: &Label, in_expr: &mut SubExpr<N, E>) {
+ let new_expr = shift0(delta, label, &in_expr);
+ std::mem::replace(in_expr, new_expr);
+}
+
+fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
+ let new_expr = shift(delta, var, &in_expr);
+ std::mem::replace(in_expr, new_expr);
+}
+
+fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
use dhall_core::Builtin::*;
- use dhall_core::ExprF::*;
- use WhatNext::*;
- let (ret, rest) = match (b, args) {
- (OptionalNone, [t, rest..]) => (rc(EmptyOptionalLit(t.roll())), rest),
- (NaturalIsZero, [NaturalLit(n), rest..]) => {
- (rc(BoolLit(*n == 0)), rest)
- }
- (NaturalEven, [NaturalLit(n), rest..]) => {
- (rc(BoolLit(*n % 2 == 0)), rest)
- }
- (NaturalOdd, [NaturalLit(n), rest..]) => {
- (rc(BoolLit(*n % 2 != 0)), rest)
- }
- (NaturalToInteger, [NaturalLit(n), rest..]) => {
- (rc(IntegerLit(*n as isize)), rest)
- }
- (NaturalShow, [NaturalLit(n), rest..]) => {
- (rc(TextLit(n.to_string().into())), rest)
- }
- (ListLength, [_, EmptyListLit(_), rest..]) => (rc(NaturalLit(0)), rest),
- (ListLength, [_, NEListLit(ys), rest..]) => {
- (rc(NaturalLit(ys.len())), rest)
- }
- (ListHead, [_, EmptyListLit(t), rest..]) => {
- (rc(EmptyOptionalLit(t.clone())), rest)
- }
- (ListHead, [_, NEListLit(ys), rest..]) => {
- (rc(NEOptionalLit(ys.first().unwrap().clone())), rest)
- }
- (ListLast, [_, EmptyListLit(t), rest..]) => {
- (rc(EmptyOptionalLit(t.clone())), rest)
- }
- (ListLast, [_, NEListLit(ys), rest..]) => {
- (rc(NEOptionalLit(ys.last().unwrap().clone())), rest)
- }
- (ListReverse, [_, EmptyListLit(t), rest..]) => {
- (rc(EmptyListLit(t.clone())), rest)
- }
- (ListReverse, [_, NEListLit(ys), rest..]) => {
- let ys = ys.iter().rev().cloned().collect();
- (rc(NEListLit(ys)), rest)
- }
- (ListIndexed, [_, EmptyListLit(t), rest..]) => (
- dhall::subexpr!([] : List ({ index : Natural, value : t })),
- rest,
+ use WHNF::*;
+
+ let ret = match b {
+ OptionalNone => improved_slice_patterns::match_vec!(args;
+ [t] => EmptyOptionalLit(Now::from_whnf(t)),
),
- (ListIndexed, [_, NEListLit(xs), rest..]) => {
- let xs = xs
- .iter()
- .cloned()
- .enumerate()
- .map(|(i, e)| {
- let i = rc(NaturalLit(i));
- dhall::subexpr!({ index = i, value = e })
- })
- .collect();
- (rc(NEListLit(xs)), rest)
- }
- (ListBuild, [a0, g, rest..]) => {
- 'ret: {
- if let App(f2, args2) = g {
- if let (Builtin(ListFold), [_, x, rest_inner..]) =
- (f2.as_ref(), args2.as_slice())
- {
- // fold/build fusion
- break 'ret (
- rc(App(x.clone(), rest_inner.to_vec())),
- rest,
- );
- }
- };
- let a0 = a0.roll();
- let a1 = shift(1, &V("x".into(), 0), &a0);
- let g = g.roll();
- break 'ret (
- dhall::subexpr!(
- g
- (List a0)
- (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
- ([] : List a0)
+ NaturalIsZero => improved_slice_patterns::match_vec!(args;
+ [NaturalLit(n)] => BoolLit(n == 0),
+ ),
+ NaturalEven => improved_slice_patterns::match_vec!(args;
+ [NaturalLit(n)] => BoolLit(n % 2 == 0),
+ ),
+ NaturalOdd => improved_slice_patterns::match_vec!(args;
+ [NaturalLit(n)] => BoolLit(n % 2 != 0),
+ ),
+ NaturalToInteger => improved_slice_patterns::match_vec!(args;
+ [NaturalLit(n)] => IntegerLit(n as isize),
+ ),
+ NaturalShow => improved_slice_patterns::match_vec!(args;
+ [NaturalLit(n)] => {
+ TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
+ }
+ ),
+ ListLength => improved_slice_patterns::match_vec!(args;
+ [_, EmptyListLit(_)] => NaturalLit(0),
+ [_, NEListLit(xs)] => NaturalLit(xs.len()),
+ ),
+ ListHead => improved_slice_patterns::match_vec!(args;
+ [_, EmptyListLit(n)] => EmptyOptionalLit(n),
+ [_, NEListLit(xs)] => {
+ NEOptionalLit(xs.into_iter().next().unwrap())
+ }
+ ),
+ ListLast => improved_slice_patterns::match_vec!(args;
+ [_, EmptyListLit(n)] => EmptyOptionalLit(n),
+ [_, NEListLit(xs)] => {
+ NEOptionalLit(xs.into_iter().rev().next().unwrap())
+ }
+ ),
+ ListReverse => improved_slice_patterns::match_vec!(args;
+ [_, EmptyListLit(n)] => EmptyListLit(n),
+ [_, NEListLit(xs)] => {
+ let mut xs = xs;
+ xs.reverse();
+ NEListLit(xs)
+ }
+ ),
+ ListIndexed => improved_slice_patterns::match_vec!(args;
+ [_, EmptyListLit(t)] => {
+ let mut kts = BTreeMap::new();
+ kts.insert(
+ "index".into(),
+ Now::from_whnf(
+ WHNF::from_builtin(Natural)
),
- rest,
);
+ kts.insert("value".into(), t);
+ EmptyListLit(Now::from_whnf(RecordType(kts)))
+ },
+ [_, NEListLit(xs)] => {
+ let xs = xs
+ .into_iter()
+ .enumerate()
+ .map(|(i, e)| {
+ let i = NaturalLit(i);
+ let mut kvs = BTreeMap::new();
+ kvs.insert("index".into(), Now::from_whnf(i));
+ kvs.insert("value".into(), e);
+ Now::from_whnf(RecordLit(kvs))
+ })
+ .collect();
+ NEListLit(xs)
}
- }
- (OptionalBuild, [a0, g, rest..]) => {
- 'ret: {
- if let App(f2, args2) = g {
- if let (Builtin(OptionalFold), [_, x, rest_inner..]) =
- (f2.as_ref(), args2.as_slice())
- {
- // fold/build fusion
- break 'ret (
- rc(App(x.clone(), rest_inner.to_vec())),
- rest,
- );
+ ),
+ ListBuild => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [_, WHNF::AppliedBuiltin(ListFold, args)] => {
+ let mut args = args;
+ if args.len() >= 2 {
+ args.remove(1)
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ },
+ [t, g] => g
+ .app(WHNF::from_builtin(List).app(t.clone()))
+ .app(ListConsClosure(Now::from_whnf(t.clone()), None))
+ .app(EmptyListLit(Now::from_whnf(t))),
+ ),
+ ListFold => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [_, WHNF::AppliedBuiltin(ListBuild, args)] => {
+ let mut args = args;
+ if args.len() >= 2 {
+ args.remove(1)
+ } else {
+ unimplemented!()
+ }
+ },
+ [_, EmptyListLit(_), _, _, nil] => nil,
+ [_, NEListLit(xs), _, cons, nil] => {
+ let mut v = nil;
+ for x in xs.into_iter().rev() {
+ v = cons.clone().app(x.normalize()).app(v);
+ }
+ v
+ }
+ ),
+ OptionalBuild => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [_, WHNF::AppliedBuiltin(OptionalFold, args)] => {
+ let mut args = args;
+ if args.len() >= 2 {
+ args.remove(1)
+ } else {
+ unimplemented!()
+ }
+ },
+ [t, g] => g
+ .app(WHNF::from_builtin(Optional).app(t.clone()))
+ .app(OptionalSomeClosure(Now::from_whnf(t.clone())))
+ .app(EmptyOptionalLit(Now::from_whnf(t))),
+ ),
+ OptionalFold => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [_, WHNF::AppliedBuiltin(OptionalBuild, args)] => {
+ let mut args = args;
+ if args.len() >= 2 {
+ args.remove(1)
+ } else {
+ unimplemented!()
+ }
+ },
+ [_, EmptyOptionalLit(_), _, _, nothing] => {
+ nothing
+ },
+ [_, NEOptionalLit(x), _, just, _] => {
+ just.app(x.normalize())
+ }
+ ),
+ NaturalBuild => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [WHNF::AppliedBuiltin(NaturalFold, args)] => {
+ let mut args = args;
+ if args.len() >= 1 {
+ args.remove(0)
+ } else {
+ unimplemented!()
+ }
+ },
+ [g] => g
+ .app(WHNF::from_builtin(Natural))
+ .app(NaturalSuccClosure)
+ .app(NaturalLit(0)),
+ ),
+ NaturalFold => improved_slice_patterns::match_vec!(args;
+ // fold/build fusion
+ [WHNF::AppliedBuiltin(NaturalBuild, args)] => {
+ let mut args = args;
+ if args.len() >= 1 {
+ args.remove(0)
+ } else {
+ unimplemented!()
+ }
+ },
+ [NaturalLit(0), _, _, zero] => zero,
+ [NaturalLit(n), t, succ, zero] => {
+ let fold = WHNF::from_builtin(NaturalFold)
+ .app(NaturalLit(n - 1))
+ .app(t)
+ .app(succ.clone())
+ .app(zero);
+ succ.app(fold)
+ },
+ ),
+ _ => Err(args),
+ };
+
+ match ret {
+ Ok(x) => x,
+ Err(args) => AppliedBuiltin(b, args),
+ }
+}
+
+#[derive(Debug, Clone)]
+enum EnvItem {
+ Expr(WHNF),
+ Skip(usize),
+}
+
+#[derive(Debug, Clone)]
+struct NormalizationContext(Rc<Context<Label, EnvItem>>);
+
+impl NormalizationContext {
+ fn new() -> Self {
+ NormalizationContext(Rc::new(Context::new()))
+ }
+ fn insert(&self, x: &Label, e: WHNF) -> Self {
+ NormalizationContext(Rc::new(
+ self.0.insert(x.clone(), EnvItem::Expr(e)),
+ ))
+ }
+ fn skip(&self, x: &Label) -> Self {
+ NormalizationContext(Rc::new(
+ self.0
+ .map(|l, e| {
+ use EnvItem::*;
+ match e {
+ Expr(e) => {
+ let mut e = e.clone();
+ e.shift0(1, x);
+ Expr(e)
+ }
+ Skip(n) if l == x => Skip(*n + 1),
+ Skip(n) => Skip(*n),
}
- };
- let a0 = a0.roll();
- let g = g.roll();
- break 'ret (
- dhall::subexpr!(
- g
- (Optional a0)
- (λ(x: a0) -> Some x)
- (None a0)
- ),
- rest,
- );
+ })
+ .insert(x.clone(), EnvItem::Skip(0)),
+ ))
+ }
+ fn lookup(&self, var: &V<Label>) -> WHNF {
+ let V(x, n) = var;
+ match self.0.lookup(x, *n) {
+ Some(EnvItem::Expr(e)) => e.clone(),
+ Some(EnvItem::Skip(m)) => {
+ WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m))))
}
+ None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
}
- (ListFold, [_, EmptyListLit(_), _, _, nil, rest..]) => {
- (nil.roll(), rest)
- }
- (ListFold, [_, NEListLit(xs), _, cons, nil, rest..]) => (
- xs.iter().rev().fold(nil.roll(), |acc, x| {
- let x = x.clone();
- let acc = acc.clone();
- let cons = cons.roll();
- dhall::subexpr!(cons x acc)
- }),
- rest,
- ),
- // // fold/build fusion
- // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
- // normalize_ref(&App(bx(x.clone()), rest.to_vec()))
- // }
- (OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => {
- let x = x.clone();
- let just = just.roll();
- (dhall::subexpr!(just x), rest)
+ }
+}
+
+/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
+/// be limited to syntactic expressions: either written by the user or meant to be printed.
+/// The rule is the following: we must _not_ construct values of type `Expr` while normalizing,
+/// but only construct `WHNF`s.
+///
+/// WHNFs store subexpressions unnormalized, to enable lazy normalization. They approximate
+/// what's called Weak Head Normal-Form (WHNF). This 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 full normalization for simple types like integers, but for e.g. a record literal
+/// this means knowing just the field names.
+///
+/// Each variant captures the relevant contexts when it is constructed. Conceptually each
+/// subexpression has its own context, but in practice some contexts can be shared when sensible, to
+/// avoid unnecessary allocations.
+#[derive(Debug, Clone)]
+enum WHNF {
+ /// Closures
+ Lam(Label, Now, (NormalizationContext, InputSubExpr)),
+ AppliedBuiltin(Builtin, Vec<WHNF>),
+ /// `λ(x: a) -> Some x`
+ OptionalSomeClosure(Now),
+ /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
+ /// `λ(xs : List a) -> [ x ] # xs`
+ ListConsClosure(Now, Option<Now>),
+ /// `λ(x : Natural) -> x + 1`
+ NaturalSuccClosure,
+
+ BoolLit(bool),
+ NaturalLit(Natural),
+ IntegerLit(Integer),
+ EmptyOptionalLit(Now),
+ NEOptionalLit(Now),
+ EmptyListLit(Now),
+ NEListLit(Vec<Now>),
+ RecordLit(BTreeMap<Label, Now>),
+ RecordType(BTreeMap<Label, Now>),
+ UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
+ UnionConstructor(
+ NormalizationContext,
+ Label,
+ BTreeMap<Label, Option<InputSubExpr>>,
+ ),
+ UnionLit(
+ Label,
+ Now,
+ (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
+ ),
+ TextLit(Vec<InterpolatedTextContents<Now>>),
+ Expr(OutputSubExpr),
+}
+
+impl WHNF {
+ /// Convert the value back to a (normalized) syntactic expression
+ fn normalize_to_expr(self) -> OutputSubExpr {
+ match self {
+ WHNF::Lam(x, t, (ctx, e)) => {
+ let ctx2 = ctx.skip(&x);
+ rc(ExprF::Lam(
+ x.clone(),
+ t.normalize().normalize_to_expr(),
+ normalize_whnf(ctx2, e).normalize_to_expr(),
+ ))
+ }
+ WHNF::AppliedBuiltin(b, args) => {
+ let mut e = WHNF::Expr(rc(ExprF::Builtin(b)));
+ for v in args {
+ e = e.app(v);
+ }
+ e.normalize_to_expr()
+ }
+ WHNF::OptionalSomeClosure(n) => {
+ let a = n.normalize().normalize_to_expr();
+ dhall::subexpr!(λ(x: a) -> Some x)
+ }
+ WHNF::ListConsClosure(n, None) => {
+ let a = n.normalize().normalize_to_expr();
+ // Avoid accidental capture of the new `x` variable
+ let a1 = shift0(1, &"x".into(), &a);
+ dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
+ }
+ WHNF::ListConsClosure(n, Some(v)) => {
+ let v = v.normalize().normalize_to_expr();
+ let a = n.normalize().normalize_to_expr();
+ dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
+ }
+ WHNF::NaturalSuccClosure => {
+ dhall::subexpr!(λ(x : Natural) -> x + 1)
+ }
+ WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
+ WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
+ WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
+ WHNF::EmptyOptionalLit(n) => {
+ WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone)))
+ .app(n.normalize())
+ .normalize_to_expr()
+ }
+ WHNF::NEOptionalLit(n) => {
+ rc(ExprF::SomeLit(n.normalize().normalize_to_expr()))
+ }
+ WHNF::EmptyListLit(n) => {
+ rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr()))
+ }
+ WHNF::NEListLit(elts) => rc(ExprF::NEListLit(
+ elts.into_iter()
+ .map(|n| n.normalize().normalize_to_expr())
+ .collect(),
+ )),
+ WHNF::RecordLit(kvs) => rc(ExprF::RecordLit(
+ kvs.into_iter()
+ .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+ .collect(),
+ )),
+ WHNF::RecordType(kts) => rc(ExprF::RecordType(
+ kts.into_iter()
+ .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+ .collect(),
+ )),
+ WHNF::UnionType(ctx, kts) => rc(ExprF::UnionType(
+ kts.into_iter()
+ .map(|(k, v)| {
+ (
+ k,
+ v.map(|v| {
+ normalize_whnf(ctx.clone(), v)
+ .normalize_to_expr()
+ }),
+ )
+ })
+ .collect(),
+ )),
+ WHNF::UnionConstructor(ctx, l, kts) => {
+ let kts = kts
+ .into_iter()
+ .map(|(k, v)| {
+ (
+ k,
+ v.map(|v| {
+ normalize_whnf(ctx.clone(), v)
+ .normalize_to_expr()
+ }),
+ )
+ })
+ .collect();
+ rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
+ }
+ WHNF::UnionLit(l, v, (kts_ctx, kts)) => rc(ExprF::UnionLit(
+ l,
+ v.normalize().normalize_to_expr(),
+ kts.into_iter()
+ .map(|(k, v)| {
+ (
+ k,
+ v.map(|v| {
+ normalize_whnf(kts_ctx.clone(), v)
+ .normalize_to_expr()
+ }),
+ )
+ })
+ .collect(),
+ )),
+ WHNF::TextLit(elts) => {
+ fn normalize_textlit(
+ elts: Vec<InterpolatedTextContents<Now>>,
+ ) -> InterpolatedText<OutputSubExpr> {
+ elts.into_iter()
+ .flat_map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ let new_interpolated = match contents {
+ Expr(n) => match n.normalize() {
+ WHNF::TextLit(elts2) => {
+ normalize_textlit(elts2)
+ }
+ e => InterpolatedText::from((
+ String::new(),
+ vec![(
+ e.normalize_to_expr(),
+ String::new(),
+ )],
+ )),
+ },
+ Text(s) => InterpolatedText::from(s),
+ };
+ new_interpolated.into_iter()
+ })
+ .collect()
+ }
+
+ rc(ExprF::TextLit(normalize_textlit(elts)))
+ }
+ WHNF::Expr(e) => e,
}
- (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing, rest..]) => {
- (nothing.roll(), rest)
+ }
+
+ /// Apply to a value
+ fn app(self, val: WHNF) -> WHNF {
+ match (self, val) {
+ (WHNF::Lam(x, _, (ctx, e)), val) => {
+ let ctx2 = ctx.insert(&x, val);
+ normalize_whnf(ctx2, e)
+ }
+ (WHNF::AppliedBuiltin(b, mut args), val) => {
+ args.push(val);
+ apply_builtin(b, args)
+ }
+ (WHNF::OptionalSomeClosure(_), val) => {
+ WHNF::NEOptionalLit(Now::from_whnf(val))
+ }
+ (WHNF::ListConsClosure(t, None), val) => {
+ WHNF::ListConsClosure(t, Some(Now::from_whnf(val)))
+ }
+ (WHNF::ListConsClosure(_, Some(x)), WHNF::EmptyListLit(_)) => {
+ WHNF::NEListLit(vec![x])
+ }
+ (WHNF::ListConsClosure(_, Some(x)), WHNF::NEListLit(mut xs)) => {
+ xs.insert(0, x);
+ WHNF::NEListLit(xs)
+ }
+ (WHNF::NaturalSuccClosure, WHNF::NaturalLit(n)) => {
+ WHNF::NaturalLit(n + 1)
+ }
+ (WHNF::UnionConstructor(ctx, l, kts), val) => {
+ WHNF::UnionLit(l, Now::from_whnf(val), (ctx, kts))
+ }
+ // Can't do anything useful, convert to expr
+ (f, a) => WHNF::Expr(rc(ExprF::App(
+ f.normalize_to_expr(),
+ a.normalize_to_expr(),
+ ))),
}
- // // fold/build fusion
- // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
- // normalize_ref(&App(bx(x.clone()), rest.to_vec()))
- // }
- (NaturalBuild, [g, rest..]) => {
- 'ret: {
- if let App(f2, args2) = g {
- if let (Builtin(NaturalFold), [x, rest_inner..]) =
- (f2.as_ref(), args2.as_slice())
- {
- // fold/build fusion
- break 'ret (
- rc(App(x.clone(), rest_inner.to_vec())),
- rest,
- );
+ }
+
+ fn from_builtin(b: Builtin) -> WHNF {
+ WHNF::AppliedBuiltin(b, vec![])
+ }
+
+ fn shift0(&mut self, delta: isize, label: &Label) {
+ match self {
+ WHNF::NaturalSuccClosure
+ | WHNF::BoolLit(_)
+ | WHNF::NaturalLit(_)
+ | WHNF::IntegerLit(_) => {}
+ WHNF::EmptyOptionalLit(n)
+ | WHNF::NEOptionalLit(n)
+ | WHNF::OptionalSomeClosure(n)
+ | WHNF::EmptyListLit(n) => {
+ n.shift0(delta, label);
+ }
+ WHNF::Lam(_, t, (_, e)) => {
+ t.shift0(delta, label);
+ shift_mut(delta, &V(label.clone(), 1), e);
+ }
+ WHNF::AppliedBuiltin(_, args) => {
+ for x in args.iter_mut() {
+ x.shift0(delta, label);
+ }
+ }
+ WHNF::ListConsClosure(t, v) => {
+ t.shift0(delta, label);
+ for x in v.iter_mut() {
+ x.shift0(delta, label);
+ }
+ }
+ WHNF::NEListLit(elts) => {
+ for x in elts.iter_mut() {
+ x.shift0(delta, label);
+ }
+ }
+ WHNF::RecordLit(kvs) | WHNF::RecordType(kvs) => {
+ for x in kvs.values_mut() {
+ x.shift0(delta, label);
+ }
+ }
+ WHNF::UnionType(_, kts) | WHNF::UnionConstructor(_, _, kts) => {
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ shift0_mut(delta, label, x);
+ }
+ }
+ WHNF::UnionLit(_, v, (_, kts)) => {
+ v.shift0(delta, label);
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ shift0_mut(delta, label, x);
+ }
+ }
+ WHNF::TextLit(elts) => {
+ for x in elts.iter_mut() {
+ use InterpolatedTextContents::{Expr, Text};
+ match x {
+ Expr(n) => n.shift0(delta, label),
+ Text(_) => {}
}
- };
- let g = g.roll();
- break 'ret (
- dhall::subexpr!(g Natural (λ(x : Natural) -> x + 1) 0),
- rest,
- );
+ }
}
+ WHNF::Expr(e) => shift0_mut(delta, label, e),
}
- (NaturalFold, [NaturalLit(0), _, _, zero, rest..]) => {
- (zero.roll(), rest)
- }
- (NaturalFold, [NaturalLit(n), t, succ, zero, rest..]) => {
- let fold = rc(Builtin(NaturalFold));
- let n = rc(NaturalLit(n - 1));
- let t = t.roll();
- let succ = succ.roll();
- let zero = zero.roll();
- (dhall::subexpr!(succ (fold n t succ zero)), rest)
- }
- // (NaturalFold, Some(App(f2, args2)), _) => {
- // match (f2.as_ref(), args2.as_slice()) {
- // // fold/build fusion
- // (Builtin(NaturalBuild), [x, rest..]) => {
- // rc(App(x.clone(), rest.to_vec()))
- // }
- // _ => return rc(App(f, args)),
- // }
- // }
- _ => return DoneAsIs,
- };
- // Put the remaining arguments back and eval again. In most cases
- // ret will not be of a form that can be applied, so this won't go very deep.
- // In lots of cases, there are no remaining args so this cann will just return ret.
- let rest: Vec<SubExpr<N, E>> = rest.iter().map(ExprF::roll).collect();
- Continue(ExprF::App(ret, rest))
+ }
}
-// Small enum to help with being DRY
-enum WhatNext<'a, N, E> {
- // Recurse on this expression
- Continue(Expr<N, E>),
- ContinueSub(SubExpr<N, E>),
- // The following expression is the normal form
- Done(Expr<N, E>),
- DoneRef(&'a Expr<N, E>),
- DoneRefSub(&'a SubExpr<N, E>),
- // The current expression is already in normal form
- DoneAsIs,
+/// Normalize-on-write smart container. Contains either a (partially) normalized value or a
+/// non-normalized value alongside a normalization context.
+/// The name is a pun on std::borrow::Cow.
+#[derive(Debug, Clone)]
+enum Now {
+ Normalized(Box<WHNF>),
+ Unnormalized(NormalizationContext, InputSubExpr),
}
-fn normalize_ref(expr: &Expr<X, Normalized<'static>>) -> Expr<X, X> {
- use dhall_core::BinOp::*;
- use dhall_core::ExprF::*;
- // Recursively normalize all subexpressions
- let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> =
- expr.map_ref_simple(|e| normalize_ref(e.as_ref()));
-
- use WhatNext::*;
- // TODO: match by move
- let what_next = match &expr {
- Let(f, _, r, b) => {
- let vf0 = &V(f.clone(), 0);
- // TODO: use a context
- ContinueSub(subst_shift(vf0, &r.roll(), &b.roll()))
+impl Now {
+ fn new(ctx: NormalizationContext, e: InputSubExpr) -> Now {
+ Now::Unnormalized(ctx, e)
+ }
+
+ fn from_whnf(v: WHNF) -> Now {
+ Now::Normalized(Box::new(v))
+ }
+
+ fn normalize(self) -> WHNF {
+ match self {
+ Now::Normalized(v) => *v,
+ Now::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
+ }
+ }
+
+ fn shift0(&mut self, delta: isize, label: &Label) {
+ match self {
+ Now::Normalized(v) => v.shift0(delta, label),
+ Now::Unnormalized(_, e) => shift0_mut(delta, label, e),
+ }
+ }
+}
+
+/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
+fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
+ match expr.as_ref() {
+ ExprF::Var(v) => ctx.lookup(&v),
+ ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
+ ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
+ // TODO: wasteful to retraverse everything
+ ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()),
+ ExprF::Let(x, _, r, b) => {
+ let r = normalize_whnf(ctx.clone(), r.clone());
+ normalize_whnf(ctx.insert(x, r), b.clone())
+ }
+ ExprF::Lam(x, t, e) => WHNF::Lam(
+ x.clone(),
+ Now::new(ctx.clone(), t.clone()),
+ (ctx, e.clone()),
+ ),
+ ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]),
+ ExprF::BoolLit(b) => WHNF::BoolLit(*b),
+ ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
+ ExprF::OldOptionalLit(None, e) => {
+ WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
}
- Annot(x, _) => DoneRef(x),
- Note(_, e) => DoneRef(e),
- App(f, args) if args.is_empty() => DoneRef(f),
- App(App(f, args1), args2) => Continue(App(
- f.clone(),
- args1
- .iter()
- .cloned()
- .chain(args2.iter().map(ExprF::roll))
+ ExprF::OldOptionalLit(Some(e), _) => {
+ WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
+ }
+ ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())),
+ ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
+ ExprF::NEListLit(elts) => WHNF::NEListLit(
+ elts.iter()
+ .map(|e| Now::new(ctx.clone(), e.clone()))
.collect(),
- )),
- App(Builtin(b), args) => apply_builtin(*b, args),
- App(Lam(x, _, b), args) => {
- let mut iter = args.iter();
- // We know args is nonempty
- let a = iter.next().unwrap();
- // Beta reduce
- let vx0 = &V(x.clone(), 0);
- let b2 = subst_shift(vx0, &a.roll(), &b);
- Continue(App(b2, iter.map(ExprF::roll).collect()))
+ ),
+ ExprF::RecordLit(kvs) => WHNF::RecordLit(
+ kvs.iter()
+ .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
+ .collect(),
+ ),
+ ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()),
+ ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
+ l.clone(),
+ Now::new(ctx.clone(), x.clone()),
+ (ctx, kts.clone()),
+ ),
+ ExprF::TextLit(elts) => WHNF::TextLit(
+ elts.iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+ Text(s) => Text(s.clone()),
+ }
+ })
+ .collect(),
+ ),
+ ExprF::BoolIf(b, e1, e2) => {
+ let b = normalize_whnf(ctx.clone(), b.clone());
+ match b {
+ WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
+ WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
+ b => {
+ let e1 = normalize_whnf(ctx.clone(), e1.clone());
+ let e2 = normalize_whnf(ctx, e2.clone());
+ match (e1, e2) {
+ (WHNF::BoolLit(true), WHNF::BoolLit(false)) => b,
+ (e1, e2) => {
+ normalize_last_layer(ExprF::BoolIf(b, e1, e2))
+ }
+ }
+ }
+ }
}
- App(UnionConstructor(l, kts), args) => {
- let mut iter = args.iter();
- // We know args is nonempty
- let a = iter.next().unwrap();
- let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone()));
- Continue(App(e, iter.map(ExprF::roll).collect()))
+ expr => {
+ // Recursively normalize subexpressions
+ let expr: ExprF<WHNF, 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()),
+ X::clone,
+ |_| unreachable!(),
+ Label::clone,
+ );
+
+ normalize_last_layer(expr)
}
- BoolIf(BoolLit(true), t, _) => DoneRef(t),
- BoolIf(BoolLit(false), _, f) => DoneRef(f),
- // TODO: interpolation
- // TextLit(t) =>
- OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
- OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
- BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)),
- BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)),
- BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
- BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)),
- BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Done(NaturalLit(x + y))
+ }
+}
+
+/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
+fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
+ use dhall_core::BinOp::*;
+ use WHNF::*;
+
+ match expr {
+ ExprF::App(v, a) => v.app(a),
+
+ ExprF::BinOp(BoolAnd, BoolLit(true), y) => y,
+ ExprF::BinOp(BoolAnd, x, BoolLit(true)) => x,
+ ExprF::BinOp(BoolAnd, BoolLit(false), _) => BoolLit(false),
+ ExprF::BinOp(BoolAnd, _, BoolLit(false)) => BoolLit(false),
+ ExprF::BinOp(BoolOr, BoolLit(true), _) => BoolLit(true),
+ ExprF::BinOp(BoolOr, _, BoolLit(true)) => BoolLit(true),
+ ExprF::BinOp(BoolOr, BoolLit(false), y) => y,
+ ExprF::BinOp(BoolOr, x, BoolLit(false)) => x,
+ ExprF::BinOp(BoolEQ, BoolLit(true), y) => y,
+ ExprF::BinOp(BoolEQ, x, BoolLit(true)) => x,
+ ExprF::BinOp(BoolNE, BoolLit(false), y) => y,
+ ExprF::BinOp(BoolNE, x, BoolLit(false)) => x,
+ ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
+ ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
+
+ ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => y,
+ ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => x,
+ ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => NaturalLit(0),
+ ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => NaturalLit(0),
+ ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => y,
+ ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => x,
+ ExprF::BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ NaturalLit(x + y)
}
- BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Done(NaturalLit(x * y))
+ ExprF::BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ NaturalLit(x * y)
}
- BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
- BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
- BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
- BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
- let xs = xs.iter().cloned();
- let ys = ys.iter().cloned();
- Done(NEListLit(xs.chain(ys).collect()))
+
+ ExprF::BinOp(ListAppend, EmptyListLit(_), y) => y,
+ ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => x,
+ ExprF::BinOp(ListAppend, NEListLit(mut xs), NEListLit(mut ys)) => {
+ xs.append(&mut ys);
+ NEListLit(xs)
}
- Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
- match handlers.get(&l) {
- Some(h) => Continue(App(h.clone(), vec![v.clone()])),
- None => DoneAsIs,
- }
+ ExprF::BinOp(TextAppend, TextLit(mut x), TextLit(mut y)) => {
+ x.append(&mut y);
+ TextLit(x)
}
- Merge(RecordLit(handlers), UnionConstructor(l, _), _) => {
- match handlers.get(&l) {
- Some(h) => DoneRefSub(h),
- None => DoneAsIs,
+ ExprF::BinOp(TextAppend, TextLit(x), y) if x.is_empty() => y,
+ ExprF::BinOp(TextAppend, x, TextLit(y)) if y.is_empty() => x,
+
+ ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts),
+ ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
+ Some(r) => r.normalize(),
+ None => {
+ // Couldn't do anything useful, so just normalize subexpressions
+ Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
}
- }
- Field(RecordLit(kvs), l) => match kvs.get(&l) {
- Some(r) => DoneRefSub(r),
- None => DoneAsIs,
},
- Field(UnionType(kts), l) => {
- Done(UnionConstructor(l.clone(), kts.clone()))
+ ExprF::Projection(_, ls) if ls.is_empty() => {
+ RecordLit(std::collections::BTreeMap::new())
}
- Projection(_, ls) if ls.is_empty() => {
- Done(RecordLit(std::collections::BTreeMap::new()))
- }
- Projection(RecordLit(kvs), ls) => Done(RecordLit(
- ls.iter()
- .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+ ExprF::Projection(RecordLit(mut kvs), ls) => RecordLit(
+ ls.into_iter()
+ .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
.collect(),
- )),
- Embed(e) => DoneRefSub(&e.0),
- _ => DoneAsIs,
- };
-
- match what_next {
- Continue(e) => normalize_ref(&e.embed_absurd()),
- ContinueSub(e) => normalize_ref(e.embed_absurd().as_ref()),
- Done(e) => e,
- DoneRef(e) => e.clone(),
- DoneRefSub(e) => e.unroll(),
- DoneAsIs => expr.map_ref_simple(ExprF::roll).map_ref(
- SubExpr::clone,
- X::clone,
- |_| unreachable!(),
- Label::clone,
),
+ ExprF::Merge(RecordLit(mut handlers), e, t) => {
+ let e = match e {
+ UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l)
+ {
+ Some(h) => return h.normalize(),
+ None => UnionConstructor(ctor_ctx, l, kts),
+ },
+ UnionLit(l, v, (kts_ctx, kts)) => match handlers.remove(&l) {
+ Some(h) => {
+ let h = h.normalize();
+ let v = v.normalize();
+ return h.app(v);
+ }
+ None => UnionLit(l, v, (kts_ctx, kts)),
+ },
+ e => e,
+ };
+ // Couldn't do anything useful, so just normalize subexpressions
+ Expr(rc(ExprF::Merge(
+ RecordLit(handlers).normalize_to_expr(),
+ e.normalize_to_expr(),
+ t.map(WHNF::normalize_to_expr),
+ )))
+ }
+ // Couldn't do anything useful, so just normalize subexpressions
+ expr => {
+ Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr())))
+ }
}
}
@@ -348,8 +797,8 @@ fn normalize_ref(expr: &Expr<X, Normalized<'static>>) -> Expr<X, X> {
/// However, `normalize` will not fail if the expression is ill-typed and will
/// leave ill-typed sub-expressions unevaluated.
///
-fn normalize(e: SubExpr<X, Normalized<'static>>) -> SubExpr<X, X> {
- normalize_ref(e.as_ref()).roll()
+fn normalize(e: InputSubExpr) -> OutputSubExpr {
+ normalize_whnf(NormalizationContext::new(), e).normalize_to_expr()
}
#[cfg(test)]
@@ -489,7 +938,7 @@ mod spec_tests {
norm!(success_prelude_Optional_unzip_1, "prelude/Optional/unzip/1");
norm!(success_prelude_Text_concat_0, "prelude/Text/concat/0");
norm!(success_prelude_Text_concat_1, "prelude/Text/concat/1");
- // norm!(success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
+ norm!(success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
norm!(success_prelude_Text_concatMap_1, "prelude/Text/concatMap/1");
// norm!(success_prelude_Text_concatMapSep_0, "prelude/Text/concatMapSep/0");
// norm!(success_prelude_Text_concatMapSep_1, "prelude/Text/concatMapSep/1");
@@ -536,7 +985,7 @@ mod spec_tests {
// norm!(success_unit_IfAlternativesIdentical, "unit/IfAlternativesIdentical");
norm!(success_unit_IfFalse, "unit/IfFalse");
norm!(success_unit_IfNormalizePredicateAndBranches, "unit/IfNormalizePredicateAndBranches");
- // norm!(success_unit_IfTrivial, "unit/IfTrivial");
+ norm!(success_unit_IfTrivial, "unit/IfTrivial");
norm!(success_unit_IfTrue, "unit/IfTrue");
norm!(success_unit_Integer, "unit/Integer");
norm!(success_unit_IntegerNegative, "unit/IntegerNegative");
@@ -603,42 +1052,42 @@ mod spec_tests {
norm!(success_unit_None, "unit/None");
norm!(success_unit_NoneNatural, "unit/NoneNatural");
// norm!(success_unit_OperatorAndEquivalentArguments, "unit/OperatorAndEquivalentArguments");
- // norm!(success_unit_OperatorAndLhsFalse, "unit/OperatorAndLhsFalse");
- // norm!(success_unit_OperatorAndLhsTrue, "unit/OperatorAndLhsTrue");
- // norm!(success_unit_OperatorAndNormalizeArguments, "unit/OperatorAndNormalizeArguments");
- // norm!(success_unit_OperatorAndRhsFalse, "unit/OperatorAndRhsFalse");
- // norm!(success_unit_OperatorAndRhsTrue, "unit/OperatorAndRhsTrue");
+ norm!(success_unit_OperatorAndLhsFalse, "unit/OperatorAndLhsFalse");
+ norm!(success_unit_OperatorAndLhsTrue, "unit/OperatorAndLhsTrue");
+ norm!(success_unit_OperatorAndNormalizeArguments, "unit/OperatorAndNormalizeArguments");
+ norm!(success_unit_OperatorAndRhsFalse, "unit/OperatorAndRhsFalse");
+ norm!(success_unit_OperatorAndRhsTrue, "unit/OperatorAndRhsTrue");
// norm!(success_unit_OperatorEqualEquivalentArguments, "unit/OperatorEqualEquivalentArguments");
- // norm!(success_unit_OperatorEqualLhsTrue, "unit/OperatorEqualLhsTrue");
- // norm!(success_unit_OperatorEqualNormalizeArguments, "unit/OperatorEqualNormalizeArguments");
- // norm!(success_unit_OperatorEqualRhsTrue, "unit/OperatorEqualRhsTrue");
+ norm!(success_unit_OperatorEqualLhsTrue, "unit/OperatorEqualLhsTrue");
+ norm!(success_unit_OperatorEqualNormalizeArguments, "unit/OperatorEqualNormalizeArguments");
+ norm!(success_unit_OperatorEqualRhsTrue, "unit/OperatorEqualRhsTrue");
norm!(success_unit_OperatorListConcatenateLhsEmpty, "unit/OperatorListConcatenateLhsEmpty");
norm!(success_unit_OperatorListConcatenateListList, "unit/OperatorListConcatenateListList");
norm!(success_unit_OperatorListConcatenateNormalizeArguments, "unit/OperatorListConcatenateNormalizeArguments");
norm!(success_unit_OperatorListConcatenateRhsEmpty, "unit/OperatorListConcatenateRhsEmpty");
// norm!(success_unit_OperatorNotEqualEquivalentArguments, "unit/OperatorNotEqualEquivalentArguments");
- // norm!(success_unit_OperatorNotEqualLhsFalse, "unit/OperatorNotEqualLhsFalse");
- // norm!(success_unit_OperatorNotEqualNormalizeArguments, "unit/OperatorNotEqualNormalizeArguments");
- // norm!(success_unit_OperatorNotEqualRhsFalse, "unit/OperatorNotEqualRhsFalse");
+ norm!(success_unit_OperatorNotEqualLhsFalse, "unit/OperatorNotEqualLhsFalse");
+ norm!(success_unit_OperatorNotEqualNormalizeArguments, "unit/OperatorNotEqualNormalizeArguments");
+ norm!(success_unit_OperatorNotEqualRhsFalse, "unit/OperatorNotEqualRhsFalse");
// norm!(success_unit_OperatorOrEquivalentArguments, "unit/OperatorOrEquivalentArguments");
- // norm!(success_unit_OperatorOrLhsFalse, "unit/OperatorOrLhsFalse");
- // norm!(success_unit_OperatorOrLhsTrue, "unit/OperatorOrLhsTrue");
- // norm!(success_unit_OperatorOrNormalizeArguments, "unit/OperatorOrNormalizeArguments");
- // norm!(success_unit_OperatorOrRhsFalse, "unit/OperatorOrRhsFalse");
- // norm!(success_unit_OperatorOrRhsTrue, "unit/OperatorOrRhsTrue");
- // norm!(success_unit_OperatorPlusLhsZero, "unit/OperatorPlusLhsZero");
- // norm!(success_unit_OperatorPlusNormalizeArguments, "unit/OperatorPlusNormalizeArguments");
+ norm!(success_unit_OperatorOrLhsFalse, "unit/OperatorOrLhsFalse");
+ norm!(success_unit_OperatorOrLhsTrue, "unit/OperatorOrLhsTrue");
+ norm!(success_unit_OperatorOrNormalizeArguments, "unit/OperatorOrNormalizeArguments");
+ norm!(success_unit_OperatorOrRhsFalse, "unit/OperatorOrRhsFalse");
+ norm!(success_unit_OperatorOrRhsTrue, "unit/OperatorOrRhsTrue");
+ norm!(success_unit_OperatorPlusLhsZero, "unit/OperatorPlusLhsZero");
+ norm!(success_unit_OperatorPlusNormalizeArguments, "unit/OperatorPlusNormalizeArguments");
norm!(success_unit_OperatorPlusOneAndOne, "unit/OperatorPlusOneAndOne");
- // norm!(success_unit_OperatorPlusRhsZero, "unit/OperatorPlusRhsZero");
- // norm!(success_unit_OperatorTextConcatenateLhsEmpty, "unit/OperatorTextConcatenateLhsEmpty");
- // norm!(success_unit_OperatorTextConcatenateNormalizeArguments, "unit/OperatorTextConcatenateNormalizeArguments");
- // norm!(success_unit_OperatorTextConcatenateRhsEmpty, "unit/OperatorTextConcatenateRhsEmpty");
+ norm!(success_unit_OperatorPlusRhsZero, "unit/OperatorPlusRhsZero");
+ norm!(success_unit_OperatorTextConcatenateLhsEmpty, "unit/OperatorTextConcatenateLhsEmpty");
+ norm!(success_unit_OperatorTextConcatenateNormalizeArguments, "unit/OperatorTextConcatenateNormalizeArguments");
+ norm!(success_unit_OperatorTextConcatenateRhsEmpty, "unit/OperatorTextConcatenateRhsEmpty");
norm!(success_unit_OperatorTextConcatenateTextText, "unit/OperatorTextConcatenateTextText");
- // norm!(success_unit_OperatorTimesLhsOne, "unit/OperatorTimesLhsOne");
- // norm!(success_unit_OperatorTimesLhsZero, "unit/OperatorTimesLhsZero");
- // norm!(success_unit_OperatorTimesNormalizeArguments, "unit/OperatorTimesNormalizeArguments");
- // norm!(success_unit_OperatorTimesRhsOne, "unit/OperatorTimesRhsOne");
- // norm!(success_unit_OperatorTimesRhsZero, "unit/OperatorTimesRhsZero");
+ norm!(success_unit_OperatorTimesLhsOne, "unit/OperatorTimesLhsOne");
+ norm!(success_unit_OperatorTimesLhsZero, "unit/OperatorTimesLhsZero");
+ norm!(success_unit_OperatorTimesNormalizeArguments, "unit/OperatorTimesNormalizeArguments");
+ norm!(success_unit_OperatorTimesRhsOne, "unit/OperatorTimesRhsOne");
+ norm!(success_unit_OperatorTimesRhsZero, "unit/OperatorTimesRhsZero");
norm!(success_unit_OperatorTimesTwoAndTwo, "unit/OperatorTimesTwoAndTwo");
norm!(success_unit_Optional, "unit/Optional");
norm!(success_unit_OptionalBuild, "unit/OptionalBuild");
@@ -675,7 +1124,7 @@ mod spec_tests {
norm!(success_unit_SomeNormalizeArguments, "unit/SomeNormalizeArguments");
norm!(success_unit_Sort, "unit/Sort");
norm!(success_unit_Text, "unit/Text");
- // norm!(success_unit_TextInterpolate, "unit/TextInterpolate");
+ norm!(success_unit_TextInterpolate, "unit/TextInterpolate");
norm!(success_unit_TextLiteral, "unit/TextLiteral");
norm!(success_unit_TextNormalizeInterpolations, "unit/TextNormalizeInterpolations");
norm!(success_unit_TextShow, "unit/TextShow");
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5aaeb08..b26f845 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -44,9 +44,9 @@ impl<'a> Normalized<'a> {
fn unroll_ref(&self) -> &Expr<X, X> {
self.as_expr().as_ref()
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
// shift the type too ?
- Normalized(shift(delta, var, &self.0), self.1.clone(), self.2)
+ Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
}
}
impl Normalized<'static> {
@@ -86,10 +86,10 @@ impl<'a> Type<'a> {
Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
use TypeInternal::*;
Type(match &self.0 {
- Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Expr(e) => Expr(Box::new(e.shift0(delta, label))),
Const(c) => Const(*c),
SuperType => SuperType,
})
@@ -168,11 +168,7 @@ where
eq2
}
}
- (App(fL, aL), App(fR, aR)) => {
- go(ctx, fL, fR)
- && aL.len() == aR.len()
- && aL.iter().zip(aR.iter()).all(|(aL, aR)| go(ctx, aL, aR))
- }
+ (App(fL, aL), App(fR, aR)) => go(ctx, fL, fR) && go(ctx, aL, aR),
(RecordType(ktsL0), RecordType(ktsR0)) => {
ktsL0.len() == ktsR0.len()
&& ktsL0
@@ -378,9 +374,8 @@ fn type_with(
let ret = match e.as_ref() {
Lam(x, t, b) => {
let t = mktype(ctx, t.clone())?;
- let ctx2 = ctx
- .insert(x.clone(), t.clone())
- .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let ctx2 =
+ ctx.insert(x.clone(), t.clone()).map(|_, e| e.shift0(1, x));
let b = type_with(&ctx2, b.clone())?;
Ok(RetExpr(Pi(
x.clone(),
@@ -395,9 +390,8 @@ fn type_with(
mkerr(InvalidInputType(ta.into_normalized()?)),
);
- let ctx2 = ctx
- .insert(x.clone(), ta.clone())
- .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let ctx2 =
+ ctx.insert(x.clone(), ta.clone()).map(|_, e| e.shift0(1, x));
let tb = type_with(&ctx2, tb.clone())?;
let kB = ensure_is_const!(
&tb.get_type()?,
@@ -476,46 +470,22 @@ fn type_last_layer(
Some(e) => Ok(RetType(e.clone())),
None => Err(mkerr(UnboundVariable)),
},
- App(f, args) => {
- let mut tf = f.get_type()?.into_owned();
- // Reconstruct the application `f a0 a1 ...`
- // for error reporting
- let mkf = |args: Vec<_>, i| {
- rc(App(
- f.into_expr(),
- args.into_iter().take(i).map(Typed::into_expr).collect(),
- ))
- };
-
- for (i, a) in args.iter().enumerate() {
- let (x, tx, tb) = ensure_matches!(tf,
- Pi(x, tx, tb) => (x, tx, tb),
- mkerr(NotAFunction(Typed(
- mkf(args, i),
- Some(tf),
- PhantomData
- )))
- );
- let tx = mktype(ctx, tx.embed_absurd())?;
- ensure_equal!(&tx, a.get_type()?, {
- let a = a.clone();
- mkerr(TypeMismatch(
- Typed(mkf(args, i + 1), Some(tf), PhantomData),
- tx.into_normalized()?,
- a,
- ))
- });
- tf = mktype(
- ctx,
- rc(Let(
- x.clone(),
- None,
- a.clone().normalize().embed(),
- tb.embed_absurd(),
- )),
- )?;
- }
- Ok(RetType(tf))
+ App(f, a) => {
+ let tf = f.get_type()?;
+ let (x, tx, tb) = ensure_matches!(tf,
+ Pi(x, tx, tb) => (x, tx, tb),
+ mkerr(NotAFunction(f))
+ );
+ let tx = mktype(ctx, tx.embed_absurd())?;
+ ensure_equal!(a.get_type()?, &tx, {
+ mkerr(TypeMismatch(f, tx.into_normalized()?, a))
+ });
+ Ok(RetExpr(Let(
+ x.clone(),
+ None,
+ a.normalize().embed(),
+ tb.embed_absurd(),
+ )))
}
Annot(x, t) => {
let t = t.normalize().into_type();
@@ -593,13 +563,7 @@ fn type_last_layer(
let e = dhall::subexpr!(Some x : Optional t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
- EmptyOptionalLit(t) => {
- let t = t.normalize();
- ensure_simple_type!(t, mkerr(InvalidOptionalType(t)));
- let t = t.embed();
- Ok(RetExpr(dhall::expr!(Optional t)))
- }
- NEOptionalLit(x) => {
+ SomeLit(x) => {
let tx = x.get_type_move()?;
ensure_simple_type!(
tx,
@@ -706,7 +670,7 @@ fn type_last_layer(
TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))),
BinOp(o @ ListAppend, l, r) => {
match l.get_type()?.unroll_ref()?.as_ref() {
- App(f, args) if args.len() == 1 => match f.as_ref() {
+ App(f, _) => match f.as_ref() {
Builtin(List) => {}
_ => return Err(mkerr(BinOpTypeMismatch(o, l))),
},
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 14:40:00 +0000