diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/normalize.rs | 44 |
1 files changed, 34 insertions, 10 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 1529784..53d7f86 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -247,6 +247,7 @@ where #[derive(Debug, Clone)] enum WHNF { Closure(Closure), + BoolLit(bool), EmptyListLit(NormalizationContext, InputSubExpr), NEListLit(Vec<(NormalizationContext, Vec<InputSubExpr>)>), RecordLit(NormalizationContext, BTreeMap<Label, InputSubExpr>), @@ -259,6 +260,7 @@ impl WHNF { fn normalize_to_expr(self) -> OutputSubExpr { match self { WHNF::Closure(c) => c.normalize_to_expr(), + WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)), WHNF::EmptyListLit(ctx, e) => rc(ExprF::EmptyListLit( normalize_whnf(&ctx, e).normalize_to_expr(), )), @@ -298,6 +300,7 @@ impl WHNF { match self { WHNF::Closure(c) => WHNF::Closure(c.shift0(delta, label)), WHNF::Expr(e) => WHNF::Expr(shift0(delta, label, &e)), + WHNF::BoolLit(b) => WHNF::BoolLit(b), WHNF::EmptyListLit(ctx, e) => { WHNF::EmptyListLit(ctx, shift0(delta, label, &e)) } @@ -516,6 +519,7 @@ fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> WHNF { ExprF::Builtin(b) => { WHNF::Closure(Closure::AppliedBuiltin(ctx.clone(), b, vec![])) } + ExprF::BoolLit(b) => WHNF::BoolLit(b), ExprF::EmptyListLit(e) => WHNF::EmptyListLit(ctx.clone(), e), ExprF::NEListLit(elts) => WHNF::NEListLit(vec![(ctx.clone(), elts)]), ExprF::RecordLit(kvs) => WHNF::RecordLit(ctx.clone(), kvs), @@ -526,7 +530,7 @@ fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> WHNF { /// Reduces the imput expression to WHNF. See doc on `WHNF` for details. fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF { - let e = match expr.as_ref() { + let expr = match expr.as_ref() { ExprF::Let(x, _, r, b) => { let r = normalize_whnf(ctx, r.clone()); return normalize_whnf(&ctx.insert(x, r), b.clone()); @@ -546,6 +550,7 @@ fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF { vec![], )) } + ExprF::BoolLit(b) => return WHNF::BoolLit(*b), ExprF::EmptyListLit(e) => { return WHNF::EmptyListLit(ctx.clone(), e.clone()) } @@ -558,12 +563,20 @@ fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF { ExprF::UnionType(kvs) => { return WHNF::UnionType(ctx.clone(), kvs.clone()) } - e => e, + ExprF::BoolIf(b, e1, e2) => { + let b = normalize_whnf(ctx, b.clone()); + match b { + WHNF::BoolLit(true) => return normalize_whnf(ctx, e1.clone()), + WHNF::BoolLit(false) => return normalize_whnf(ctx, e2.clone()), + _ => expr, + } + } + _ => expr, }; // Recursively normalize all subexpressions - let expr: ExprF<WHNF, Label, X, Normalized<'static>> = e - .map_ref_with_special_handling_of_binders( + let expr: ExprF<WHNF, Label, X, Normalized<'static>> = + expr.as_ref().map_ref_with_special_handling_of_binders( |e| normalize_whnf(ctx, e.clone()), |x, e| normalize_whnf(&ctx.skip(x), e.clone()), X::clone, @@ -588,6 +601,18 @@ fn normalize_last_layer( Annot(x, _) => return x, Note(_, e) => return e, App(WHNF::Closure(c), a) => return c.app(a), + BinOp(BoolAnd, WHNF::BoolLit(x), WHNF::BoolLit(y)) => { + return WHNF::BoolLit(x && y) + } + BinOp(BoolOr, WHNF::BoolLit(x), WHNF::BoolLit(y)) => { + return WHNF::BoolLit(x || y) + } + BinOp(BoolEQ, WHNF::BoolLit(x), WHNF::BoolLit(y)) => { + return WHNF::BoolLit(x == y) + } + BinOp(BoolNE, WHNF::BoolLit(x), WHNF::BoolLit(y)) => { + return WHNF::BoolLit(x != y) + } BinOp(ListAppend, WHNF::EmptyListLit(_, _), y) => return y, BinOp(ListAppend, x, WHNF::EmptyListLit(_, _)) => return x, BinOp(ListAppend, WHNF::NEListLit(xs), WHNF::NEListLit(ys)) => { @@ -648,16 +673,15 @@ fn normalize_last_layer( Lam(_, _, _) => unreachable!(), App(Builtin(_), _) => unreachable!(), App(Lam(_, _, _), _) => unreachable!(), - BoolIf(BoolLit(true), t, _) => DoneRef(t), - BoolIf(BoolLit(false), _, f) => DoneRef(f), + BoolIf(BoolLit(_), _, _) => unreachable!(), // 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(BoolAnd, BoolLit(_), BoolLit(_)) => unreachable!(), + BinOp(BoolOr, BoolLit(_), BoolLit(_)) => unreachable!(), + BinOp(BoolEQ, BoolLit(_), BoolLit(_)) => unreachable!(), + BinOp(BoolNE, BoolLit(_), BoolLit(_)) => unreachable!(), BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => { Done(NaturalLit(x + y)) } |