diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/normalize.rs | 41 |
1 files changed, 29 insertions, 12 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 141320f..9847c27 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -3,10 +3,13 @@ use std::collections::BTreeMap; use std::rc::Rc; use dhall_core::context::Context; -use dhall_core::*; +use dhall_core::{ + rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText, + InterpolatedTextContents, Label, Natural, SubExpr, V, X, +}; use dhall_generator as dhall; -use crate::expr::*; +use crate::expr::{Normalized, Typed}; type InputSubExpr = SubExpr<X, Normalized<'static>>; type OutputSubExpr = SubExpr<X, X>; @@ -39,9 +42,7 @@ fn apply_builtin( (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0), (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0), (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0), - (NaturalToInteger, [NaturalLit(n)]) => { - Expr(rc(ExprF::IntegerLit(*n as isize))) - } + (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize), (NaturalShow, [NaturalLit(n)]) => { TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) } @@ -61,12 +62,13 @@ fn apply_builtin( NEListLit(xs) } (ListIndexed, [_, EmptyListLit(t)]) => { - // TODO: avoid passing through Exprs - let t = t.clone().normalize().normalize_to_expr().embed_absurd(); - EmptyListLit(Now::new( - ctx, - dhall::subexpr!({ index : Natural, value : t }), - )) + let mut kts = BTreeMap::new(); + kts.insert( + "index".into(), + Now::from_whnf(AppliedBuiltin(ctx, Natural, vec![])), + ); + kts.insert("value".into(), t.clone()); + EmptyListLit(Now::from_whnf(RecordType(kts))) } (ListIndexed, [_, NEListLit(xs)]) => { let xs = xs @@ -232,11 +234,13 @@ enum WHNF { 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, @@ -291,6 +295,7 @@ impl WHNF { } WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)), WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)), + WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)), WHNF::EmptyOptionalLit(n) => { rc(ExprF::EmptyOptionalLit(n.normalize().normalize_to_expr())) } @@ -310,6 +315,11 @@ impl WHNF { .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)| { @@ -446,9 +456,9 @@ impl WHNF { v.map(|v| v.shift0(delta, label)), ), WHNF::NaturalSuccClosure => WHNF::NaturalSuccClosure, - WHNF::Expr(e) => WHNF::Expr(shift0(delta, label, &e)), WHNF::BoolLit(b) => WHNF::BoolLit(b), WHNF::NaturalLit(n) => WHNF::NaturalLit(n), + WHNF::IntegerLit(n) => WHNF::IntegerLit(n), WHNF::EmptyOptionalLit(n) => { WHNF::EmptyOptionalLit(n.shift0(delta, label)) } @@ -464,6 +474,11 @@ impl WHNF { .map(|(k, v)| (k, v.shift0(delta, label))) .collect(), ), + WHNF::RecordType(kts) => WHNF::RecordType( + kts.into_iter() + .map(|(k, v)| (k, v.shift0(delta, label))) + .collect(), + ), WHNF::UnionType(ctx, kts) => WHNF::UnionType( ctx, kts.into_iter() @@ -498,6 +513,7 @@ impl WHNF { }) .collect(), ), + WHNF::Expr(e) => WHNF::Expr(shift0(delta, label, &e)), } } } @@ -747,6 +763,7 @@ fn normalize_last_layer( expr => expr, }; + // Couldn't do anything useful, so just normalize subexpressions WHNF::Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr()))) } |