diff options
Diffstat (limited to 'dhall/src/semantics/nze/normalize.rs')
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 100 |
1 files changed, 44 insertions, 56 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 79d55e8..570e106 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -2,14 +2,10 @@ use itertools::Itertools; use std::collections::HashMap; use crate::semantics::NzEnv; -use crate::semantics::{ - Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit, -}; -use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind, -}; +use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; +use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind}; -pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind { +pub fn apply_any(f: Nir, a: Nir) -> NirKind { match f.kind() { NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(), NirKind::AppliedBuiltin(closure) => closure.apply(a), @@ -20,7 +16,7 @@ pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind { } } -pub(crate) fn squash_textlit( +pub fn squash_textlit( elts: impl Iterator<Item = InterpolatedTextContents<Nir>>, ) -> Vec<InterpolatedTextContents<Nir>> { use std::mem::replace; @@ -58,7 +54,7 @@ pub(crate) fn squash_textlit( ret } -pub(crate) fn merge_maps<K, V, F>( +pub fn merge_maps<K, V, F>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, mut f: F, @@ -99,40 +95,40 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use LitKind::{Bool, Natural}; - use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType}; + use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; + use NumKind::{Bool, Natural}; Some(match (o, x.kind(), y.kind()) { - (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y), - (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x), - (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))), - (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))), + (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y), + (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x), + (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))), + (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))), (BoolAnd, _, _) if x == y => Ret::NirRef(x), - (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))), - (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))), - (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y), - (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x), + (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))), + (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))), + (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y), + (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x), (BoolOr, _, _) if x == y => Ret::NirRef(x), - (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y), - (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x), - (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))), - (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))), - (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y), - (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x), - (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))), - (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))), + (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y), + (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x), + (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))), + (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))), + (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y), + (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x), + (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))), + (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))), - (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y), - (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x), - (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => { - Ret::NirKind(Lit(Natural(x + y))) + (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y), + (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x), + (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { + Ret::NirKind(Num(Natural(x + y))) } - (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))), - (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))), - (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y), - (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x), - (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => { - Ret::NirKind(Lit(Natural(x * y))) + (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))), + (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))), + (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y), + (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x), + (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { + Ret::NirKind(Num(Natural(x * y))) } (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y), @@ -211,13 +207,13 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { - use LitKind::Bool; +pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ - EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit, + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, UnionType, }; + use NumKind::Bool; let ret = match expr { ExprKind::Import(..) | ExprKind::Completion(..) => { @@ -235,15 +231,11 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Nir(v.app(a)), - ExprKind::Lit(l) => Ret::NirKind(Lit(l)), + ExprKind::Num(l) => Ret::NirKind(Num(l)), ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - }) if args.len() == 1 => args[0].clone(), + NirKind::ListType(t) => t.clone(), _ => panic!("internal type error"), }; Ret::NirKind(NirKind::EmptyListLit(arg)) @@ -271,12 +263,12 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { } ExprKind::BoolIf(ref b, ref e1, ref e2) => { match b.kind() { - Lit(Bool(true)) => Ret::NirRef(e1), - Lit(Bool(false)) => Ret::NirRef(e2), + Num(Bool(true)) => Ret::NirRef(e1), + Num(Bool(false)) => Ret::NirRef(e2), _ => { match (e1.kind(), e2.kind()) { // Simplify `if b then True else False` - (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b), + (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b), _ if e1 == e2 => Ret::NirRef(e1), _ => Ret::Expr(expr), } @@ -442,12 +434,8 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { ExprKind::ToMap(ref v, ref annot) => match v.kind() { RecordLit(kvs) if kvs.is_empty() => { match annot.as_ref().map(|v| v.kind()) { - Some(NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - })) if args.len() == 1 => { - Ret::NirKind(EmptyListLit(args[0].clone())) + Some(NirKind::ListType(t)) => { + Ret::NirKind(EmptyListLit(t.clone())) } _ => Ret::Expr(expr), } @@ -476,7 +464,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { } /// Normalize Hir into WHNF -pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { +pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { match hir.kind() { HirKind::Var(var) => env.lookup_val(*var), HirKind::Import(hir, _) => normalize_hir_whnf(env, hir), |