summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
authorNadrieril2020-04-06 22:11:54 +0100
committerNadrieril2020-04-06 22:11:54 +0100
commitfff4c46e09d4edf25eba737f4d71bfdb1dbf4a82 (patch)
tree30f48f45ba0201859193510c65edfd3634764090 /dhall/src/semantics/nze
parentcd3b11cc8bd7c4397071d1d3b4b9020b7d5ff2ad (diff)
Extract operation-related code to a new module
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/nir.rs3
-rw-r--r--dhall/src/semantics/nze/normalize.rs301
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,