diff options
author | Nadrieril | 2020-04-07 12:22:27 +0100 |
---|---|---|
committer | GitHub | 2020-04-07 12:22:27 +0100 |
commit | 832c99a3b28e70512d580a51fc378473834b2891 (patch) | |
tree | 95b417cb3349bd1896f661a3fce67531c52d5b7b /dhall/src/semantics/nze/normalize.rs | |
parent | d35cb130d80d628807a4247ddf84a8d0230c87ab (diff) | |
parent | 214a3c998a3358849495b54a60d46f626b131f0a (diff) |
Merge pull request #159 from Nadrieril/operations
Factor out operations
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 406 |
1 files changed, 48 insertions, 358 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 570e106..d042f3f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,18 +1,18 @@ -use itertools::Itertools; use std::collections::HashMap; +use crate::operations::{normalize_operation, OpKind}; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; -use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind}; +use crate::syntax::{ExprKind, InterpolatedTextContents}; -pub 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), NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::Op(OpKind::App(f.clone(), a)), } } @@ -81,393 +81,83 @@ where kvs } -// Small helper enum to avoid repetition -enum Ret<'a> { - NirKind(NirKind), - Nir(Nir), - NirRef(&'a Nir), - Expr(ExprKind<Nir>), -} - -fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; - use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; - use NumKind::{Bool, Natural}; - - Some(match (o, x.kind(), y.kind()) { - (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, 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, 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, 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, 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), - (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit( - xs.iter().chain(ys.iter()).cloned().collect(), - )), - - (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x), - (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - Ret::NirKind(NirKind::TextLit(x.concat(y))) - } - (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit( - x.concat(&TextLit::interpolate(y.clone())), - )), - (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit( - TextLit::interpolate(x.clone()).concat(y), - )), +pub type Ret = NirKind; - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - Ret::NirKind(RecordLit(kvs)) - } - (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y), - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )) - }); - Ret::NirKind(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { - let kts = merge_maps( - kts_x, - kts_y, - // If the Label exists for both records, then we hit the recursive case. - |_, l: &Nir, r: &Nir| { - Nir::from_partial_expr(ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - )) - }, - ); - Ret::NirKind(RecordType(kts)) - } - - (Equivalence, _, _) => { - Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone())) - } - - _ => return None, - }) +pub fn ret_nir(x: Nir) -> Ret { + ret_ref(&x) +} +pub fn ret_kind(x: NirKind) -> Ret { + x +} +pub fn ret_ref(x: &Nir) -> Ret { + x.kind().clone() +} +pub fn ret_op(x: OpKind<Nir>) -> Ret { + NirKind::Op(x) } -#[allow(clippy::cognitive_complexity)] pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; - use NumKind::Bool; - let ret = match expr { - ExprKind::Import(..) | ExprKind::Completion(..) => { - unreachable!("This case should have been handled in resolution") - } + match expr { ExprKind::Var(..) | ExprKind::Lam(..) | ExprKind::Pi(..) - | ExprKind::Let(..) => unreachable!( - "This case should have been handled in normalize_hir_whnf" - ), + | ExprKind::Let(..) => { + unreachable!("This case should have been handled in normalize_hir") + } - ExprKind::Annot(x, _) => Ret::Nir(x), - ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)), - 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::Num(l) => Ret::NirKind(Num(l)), - ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), + ExprKind::Const(c) => ret_kind(Const(c)), + ExprKind::Num(l) => ret_kind(Num(l)), + ExprKind::Builtin(b) => { + ret_kind(NirKind::from_builtin_env(b, env.clone())) + } + ExprKind::TextLit(elts) => { + let tlit = TextLit::new(elts.into_iter()); + // Simplify bare interpolation + if let Some(v) = tlit.as_single_expr() { + ret_ref(v) + } else { + ret_kind(NirKind::TextLit(tlit)) + } + } + ExprKind::SomeLit(e) => ret_kind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { NirKind::ListType(t) => t.clone(), _ => panic!("internal type error"), }; - Ret::NirKind(NirKind::EmptyListLit(arg)) + ret_kind(NirKind::EmptyListLit(arg)) } ExprKind::NEListLit(elts) => { - Ret::NirKind(NEListLit(elts.into_iter().collect())) + ret_kind(NEListLit(elts.into_iter().collect())) } ExprKind::RecordLit(kvs) => { - Ret::NirKind(RecordLit(kvs.into_iter().collect())) + ret_kind(RecordLit(kvs.into_iter().collect())) } ExprKind::RecordType(kvs) => { - Ret::NirKind(RecordType(kvs.into_iter().collect())) + ret_kind(RecordType(kvs.into_iter().collect())) } ExprKind::UnionType(kvs) => { - Ret::NirKind(UnionType(kvs.into_iter().collect())) - } - ExprKind::TextLit(elts) => { - let tlit = TextLit::new(elts.into_iter()); - // Simplify bare interpolation - if let Some(v) = tlit.as_single_expr() { - Ret::Nir(v.clone()) - } else { - Ret::NirKind(NirKind::TextLit(tlit)) - } - } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { - match b.kind() { - Num(Bool(true)) => Ret::NirRef(e1), - Num(Bool(false)) => Ret::NirRef(e2), - _ => { - match (e1.kind(), e2.kind()) { - // Simplify `if b then True else False` - (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b), - _ if e1 == e2 => Ret::NirRef(e1), - _ => Ret::Expr(expr), - } - } - } - } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, - - ExprKind::Field(ref v, ref field) => match v.kind() { - RecordLit(kvs) => match kvs.get(field) { - Some(r) => Ret::Nir(r.clone()), - None => Ret::Expr(expr), - }, - UnionType(kts) => { - Ret::NirKind(UnionConstructor(field.clone(), kts.clone())) - } - PartialExpr(ExprKind::Projection(x, _)) => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - x, - y, - )) => match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Nir(r.clone()), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(y.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - }, - PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { - match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(y.clone(), field.clone()), - env, - ) - } - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - } - } - _ => Ret::Expr(expr), - }, - ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::NirKind(RecordLit(HashMap::new())) + ret_kind(UnionType(kvs.into_iter().collect())) } - ExprKind::Projection(ref v, ref ls) => match v.kind() { - RecordLit(kvs) => Ret::NirKind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - PartialExpr(ExprKind::Projection(v2, _)) => { - return normalize_one_layer( - ExprKind::Projection(v2.clone(), ls.clone()), - env, - ) - } - _ => Ret::Expr(expr), - }, - ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() { - RecordType(kts) => { - return normalize_one_layer( - ExprKind::Projection( - v.clone(), - kts.keys().cloned().collect(), - ), - env, - ) - } - _ => Ret::Expr(expr), - }, - - ExprKind::Merge(ref handlers, ref variant, _) => { - match handlers.kind() { - RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => Ret::Nir(h.clone()), - None => Ret::Expr(expr), - }, - UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => Ret::Nir(h.app(v.clone())), - None => Ret::Expr(expr), - }, - EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => Ret::Nir(h.clone()), - None => Ret::Expr(expr), - }, - NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => Ret::Nir(h.app(v.clone())), - None => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - } + ExprKind::Op(ref op) => normalize_operation(op), + ExprKind::Annot(x, _) => ret_nir(x), + ExprKind::Assert(x) => ret_kind(Assert(x)), + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") } - 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::ListType(t)) => { - Ret::NirKind(EmptyListLit(t.clone())) - } - _ => Ret::Expr(expr), - } - } - RecordLit(kvs) => Ret::NirKind(NEListLit( - kvs.iter() - .sorted_by_key(|(k, _)| *k) - .map(|(k, v)| { - let mut rec = HashMap::new(); - rec.insert("mapKey".into(), Nir::from_text(k)); - rec.insert("mapValue".into(), v.clone()); - Nir::from_kind(NirKind::RecordLit(rec)) - }) - .collect(), - )), - _ => Ret::Expr(expr), - }, - }; - - match ret { - Ret::NirKind(v) => v, - Ret::Nir(v) => v.kind().clone(), - Ret::NirRef(v) => v.kind().clone(), - Ret::Expr(expr) => NirKind::PartialExpr(expr), } } /// Normalize Hir into WHNF -pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { +pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind { match hir.kind() { HirKind::Var(var) => env.lookup_val(*var), - HirKind::Import(hir, _) => normalize_hir_whnf(env, hir), + HirKind::Import(hir, _) => normalize_hir(env, hir), HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); NirKind::LamClosure { |