diff options
author | Nadrieril | 2020-04-06 22:11:54 +0100 |
---|---|---|
committer | Nadrieril | 2020-04-06 22:11:54 +0100 |
commit | fff4c46e09d4edf25eba737f4d71bfdb1dbf4a82 (patch) | |
tree | 30f48f45ba0201859193510c65edfd3634764090 /dhall/src/semantics/nze | |
parent | cd3b11cc8bd7c4397071d1d3b4b9020b7d5ff2ad (diff) |
Extract operation-related code to a new module
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r-- | dhall/src/semantics/nze/nir.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 301 |
2 files changed, 9 insertions, 295 deletions
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 88123d8..5c67c02 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,6 +1,7 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::operations::OpKind; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, @@ -8,7 +9,7 @@ use crate::semantics::{ }; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - NumKind, OpKind, Span, + NumKind, Span, }; use crate::ToExprOptions; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c0e41cb..d042f3f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,11 +1,9 @@ -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, Label, NumKind, OpKind, -}; +use crate::syntax::{ExprKind, InterpolatedTextContents}; pub fn apply_any(f: &Nir, a: Nir) -> NirKind { match f.kind() { @@ -83,306 +81,21 @@ where kvs } -type Ret = NirKind; +pub type Ret = NirKind; -fn ret_nir(x: Nir) -> Ret { +pub fn ret_nir(x: Nir) -> Ret { ret_ref(&x) } -fn ret_kind(x: NirKind) -> Ret { +pub fn ret_kind(x: NirKind) -> Ret { x } -fn ret_ref(x: &Nir) -> Ret { +pub fn ret_ref(x: &Nir) -> Ret { x.kind().clone() } -fn ret_op(x: OpKind<Nir>) -> Ret { +pub fn ret_op(x: OpKind<Nir>) -> Ret { NirKind::Op(x) } -fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { - use BinOp::*; - use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; - use NumKind::{Bool, Natural}; - - match (o, x.kind(), y.kind()) { - (BoolAnd, Num(Bool(true)), _) => ret_ref(y), - (BoolAnd, _, Num(Bool(true))) => ret_ref(x), - (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), - (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))), - (BoolAnd, _, _) if x == y => ret_ref(x), - (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))), - (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))), - (BoolOr, Num(Bool(false)), _) => ret_ref(y), - (BoolOr, _, Num(Bool(false))) => ret_ref(x), - (BoolOr, _, _) if x == y => ret_ref(x), - (BoolEQ, Num(Bool(true)), _) => ret_ref(y), - (BoolEQ, _, Num(Bool(true))) => ret_ref(x), - (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))), - (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))), - (BoolNE, Num(Bool(false)), _) => ret_ref(y), - (BoolNE, _, Num(Bool(false))) => ret_ref(x), - (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))), - (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))), - - (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), - (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), - (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x + y))) - } - (NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))), - (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))), - (NaturalTimes, Num(Natural(1)), _) => ret_ref(y), - (NaturalTimes, _, Num(Natural(1))) => ret_ref(x), - (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x * y))) - } - - (ListAppend, EmptyListLit(_), _) => ret_ref(y), - (ListAppend, _, EmptyListLit(_)) => ret_ref(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => { - ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) - } - - (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x), - (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - ret_kind(NirKind::TextLit(x.concat(y))) - } - (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( - x.concat(&TextLit::interpolate(y.clone())), - )), - (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( - TextLit::interpolate(x.clone()).concat(y), - )), - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(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_kind(RecordLit(kvs)) - } - (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - ))) - }); - ret_kind(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::Op(OpKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ))) - }, - ); - ret_kind(RecordType(kts)) - } - - (Equivalence, _, _) => { - ret_kind(NirKind::Equivalence(x.clone(), y.clone())) - } - - _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), - } -} - -fn normalize_field(v: &Nir, field: &Label) -> Ret { - use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; - use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; - use OpKind::{BinOp, Field, Projection}; - let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); - - match v.kind() { - RecordLit(kvs) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => nothing_to_do(), - }, - UnionType(kts) => { - ret_kind(UnionConstructor(field.clone(), kts.clone())) - } - Op(Projection(x, _)) => normalize_field(x, field), - Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => normalize_field(x, field), - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - _ => nothing_to_do(), - }, - Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ))), - field.clone(), - )), - None => normalize_field(x, field), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - } -} - -fn normalize_operation(opkind: &OpKind<Nir>) -> Ret { - use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, - RecordLit, RecordType, UnionConstructor, UnionLit, - }; - use NumKind::Bool; - use OpKind::*; - let nothing_to_do = || ret_op(opkind.clone()); - - match opkind { - App(v, a) => ret_kind(v.app_to_kind(a.clone())), - BinOp(o, x, y) => normalize_binop(*o, x, y), - BoolIf(b, e1, e2) => { - match b.kind() { - Num(Bool(true)) => ret_ref(e1), - Num(Bool(false)) => ret_ref(e2), - _ => { - match (e1.kind(), e2.kind()) { - // Simplify `if b then True else False` - (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), - _ if e1 == e2 => ret_ref(e1), - _ => nothing_to_do(), - } - } - } - } - Merge(handlers, variant, _) => match handlers.kind() { - RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - ToMap(v, annot) => match v.kind() { - RecordLit(kvs) if kvs.is_empty() => { - match annot.as_ref().map(|v| v.kind()) { - Some(NirKind::ListType(t)) => { - ret_kind(EmptyListLit(t.clone())) - } - _ => nothing_to_do(), - } - } - RecordLit(kvs) => ret_kind(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(), - )), - _ => nothing_to_do(), - }, - Field(v, field) => normalize_field(v, field), - Projection(_, ls) if ls.is_empty() => { - ret_kind(RecordLit(HashMap::new())) - } - Projection(v, ls) => match v.kind() { - RecordLit(kvs) => ret_kind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - Op(Projection(v2, _)) => { - normalize_operation(&Projection(v2.clone(), ls.clone())) - } - _ => nothing_to_do(), - }, - ProjectionByExpr(v, t) => match t.kind() { - RecordType(kts) => normalize_operation(&Projection( - v.clone(), - kts.keys().cloned().collect(), - )), - _ => nothing_to_do(), - }, - Completion(..) => { - unreachable!("This case should have been handled in resolution") - } - } -} - pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, |