#![allow(non_snake_case)] use std::collections::BTreeMap; use dhall_core::context::Context; use dhall_core::*; use dhall_generator as dhall; use crate::expr::*; type InputSubExpr = SubExpr>; type OutputSubExpr = SubExpr; impl<'a> Typed<'a> { pub fn normalize(self) -> Normalized<'a> { Normalized(normalize(self.0), self.1, self.2) } /// Pretends this expression is normalized. Use with care. #[allow(dead_code)] pub fn skip_normalize(self) -> Normalized<'a> { Normalized( self.0.unroll().squash_embed(|e| e.0.clone()), self.1, self.2, ) } } fn apply_builtin( ctx: &NormalizationContext, b: Builtin, args: &[WHNF], ) -> Option { let args: Vec<_> = args .iter() .map(|val| val.clone().normalize_to_expr().unroll()) .collect(); use dhall_core::Builtin::*; use dhall_core::ExprF::*; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => rc(EmptyOptionalLit(t.roll())), (NaturalIsZero, [NaturalLit(n)]) => rc(BoolLit(*n == 0)), (NaturalEven, [NaturalLit(n)]) => rc(BoolLit(*n % 2 == 0)), (NaturalOdd, [NaturalLit(n)]) => rc(BoolLit(*n % 2 != 0)), (NaturalToInteger, [NaturalLit(n)]) => rc(IntegerLit(*n as isize)), (NaturalShow, [NaturalLit(n)]) => rc(TextLit(n.to_string().into())), (ListLength, [_, EmptyListLit(_)]) => rc(NaturalLit(0)), (ListLength, [_, NEListLit(ys)]) => rc(NaturalLit(ys.len())), (ListHead, [_, EmptyListLit(t)]) => rc(EmptyOptionalLit(t.clone())), (ListHead, [_, NEListLit(ys)]) => { rc(NEOptionalLit(ys.first().unwrap().clone())) } (ListLast, [_, EmptyListLit(t)]) => rc(EmptyOptionalLit(t.clone())), (ListLast, [_, NEListLit(ys)]) => { rc(NEOptionalLit(ys.last().unwrap().clone())) } (ListReverse, [_, EmptyListLit(t)]) => rc(EmptyListLit(t.clone())), (ListReverse, [_, NEListLit(ys)]) => { let ys = ys.iter().rev().cloned().collect(); rc(NEListLit(ys)) } (ListIndexed, [_, EmptyListLit(t)]) => { dhall::subexpr!([] : List ({ index : Natural, value : t })) } (ListIndexed, [_, NEListLit(xs)]) => { let xs = xs .iter() .cloned() .enumerate() .map(|(i, e)| { let i = rc(NaturalLit(i)); dhall::subexpr!({ index = i, value = e }) }) .collect(); rc(NEListLit(xs)) } (ListBuild, [a0, g]) => { '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 = shift0(1, &"x".into(), &a0); let g = g.roll(); break 'ret dhall::subexpr!( g (List a0) (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs) ([] : List a0) ); } } (OptionalBuild, [a0, g]) => { '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, // ); // } // }; let a0 = a0.roll(); let g = g.roll(); break 'ret dhall::subexpr!( g (Optional a0) (λ(x: a0) -> Some x) (None a0) ); } } (ListFold, [_, EmptyListLit(_), _, _, nil]) => nil.roll(), (ListFold, [_, NEListLit(xs), _, cons, nil]) => { 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) }) } // // fold/build fusion // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) // } (OptionalFold, [_, NEOptionalLit(x), _, just, _]) => { let x = x.clone(); let just = just.roll(); dhall::subexpr!(just x) } (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing]) => { nothing.roll() } // // fold/build fusion // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) // } (NaturalBuild, [g]) => { // '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, // ); // } // }; // } let g = g.roll(); dhall::subexpr!(g Natural (λ(x : Natural) -> x + 1) 0) } (NaturalFold, [NaturalLit(0), _, _, zero]) => zero.roll(), (NaturalFold, [NaturalLit(n), t, succ, zero]) => { 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)) } // (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 None, }; Some(normalize_whnf(ctx, ret.embed_absurd())) } #[derive(Debug, Clone)] enum EnvItem { Expr(WHNF), Skip(usize), } #[derive(Debug, Clone)] struct NormalizationContext(Context); impl NormalizationContext { fn new() -> NormalizationContext { NormalizationContext(Context::new()) } fn insert(&self, x: &Label, e: WHNF) -> NormalizationContext { NormalizationContext(self.0.insert(x.clone(), EnvItem::Expr(e))) } fn skip(&self, x: &Label) -> NormalizationContext { NormalizationContext( self.0 .map(|l, e| { use EnvItem::*; match e { Expr(e) => Expr(e.clone().shift0(1, x)), Skip(n) if l == x => Skip(*n + 1), Skip(n) => Skip(*n), } }) .insert(x.clone(), EnvItem::Skip(0)), ) } fn lookup(&self, var: &V