From 08e1d8ece4314b56d64fa08595c2e043b97896d1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 17:19:31 +0100 Subject: Split off operations from main expr enum --- dhall/src/semantics/nze/normalize.rs | 182 ++++++++++++++++++++--------------- 1 file changed, 104 insertions(+), 78 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 570e106..ebf4ae1 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,7 +3,9 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; -use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind}; +use crate::syntax::{ + BinOp, ExprKind, InterpolatedTextContents, NumKind, OpKind, +}; pub fn apply_any(f: Nir, a: Nir) -> NirKind { match f.kind() { @@ -12,7 +14,7 @@ pub fn apply_any(f: Nir, a: Nir) -> NirKind { NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f, a))), } } @@ -173,11 +175,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::BinOp( + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )) + ))) }); Ret::NirKind(RecordLit(kvs)) } @@ -188,11 +190,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { 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( + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), - )) + ))) }, ); Ret::NirKind(RecordType(kts)) @@ -216,7 +218,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NumKind::Bool; let ret = match expr { - ExprKind::Import(..) | ExprKind::Completion(..) => { + ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { unreachable!("This case should have been handled in resolution") } ExprKind::Var(..) @@ -230,7 +232,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { 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::Op(OpKind::App(v, a)) => Ret::Nir(v.app(a)), ExprKind::Num(l) => Ret::NirKind(Num(l)), ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { @@ -261,7 +263,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { Ret::NirKind(NirKind::TextLit(tlit)) } } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { + ExprKind::Op(OpKind::BoolIf(ref b, ref e1, ref e2)) => { match b.kind() { Num(Bool(true)) => Ret::NirRef(e1), Num(Bool(false)) => Ret::NirRef(e2), @@ -275,12 +277,14 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { } } } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, + ExprKind::Op(OpKind::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() { + ExprKind::Op(OpKind::Field(ref v, ref field)) => match v.kind() { RecordLit(kvs) => match kvs.get(field) { Some(r) => Ret::Nir(r.clone()), None => Ret::Expr(expr), @@ -288,53 +292,65 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { UnionType(kts) => { Ret::NirKind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(ExprKind::Projection(x, _)) => { + PartialExpr(ExprKind::Op(OpKind::Projection(x, _))) => { return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), + ExprKind::Op(OpKind::Field(x.clone(), field.clone())), env, ) } - PartialExpr(ExprKind::BinOp( + PartialExpr(ExprKind::Op(OpKind::BinOp( BinOp::RightBiasedRecordMerge, x, y, - )) => match (x.kind(), y.kind()) { + ))) => 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()), + ExprKind::Op(OpKind::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(), + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::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()), + ExprKind::Op(OpKind::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( + PartialExpr(ExprKind::Op(OpKind::BinOp( + BinOp::RecursiveRecordMerge, + x, + y, + ))) => match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::BinOp( BinOp::RecursiveRecordMerge, Nir::from_kind(RecordLit( Some((field.clone(), r.clone())) @@ -342,19 +358,24 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { .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( + ), + ))), + field.clone(), + ))), + None => { + return normalize_one_layer( + ExprKind::Op(OpKind::Field( + y.clone(), + field.clone(), + )), + env, + ) + } + }, + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::BinOp( BinOp::RecursiveRecordMerge, x.clone(), Nir::from_kind(RecordLit( @@ -362,52 +383,57 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { .into_iter() .collect(), )), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - } - } + ), + ))), + field.clone(), + ))), + None => { + return normalize_one_layer( + ExprKind::Op(OpKind::Field( + x.clone(), + field.clone(), + )), + env, + ) + } + }, + _ => Ret::Expr(expr), + }, _ => Ret::Expr(expr), }, - ExprKind::Projection(_, ref ls) if ls.is_empty() => { + ExprKind::Op(OpKind::Projection(_, ref ls)) if ls.is_empty() => { Ret::NirKind(RecordLit(HashMap::new())) } - ExprKind::Projection(ref v, ref ls) => match v.kind() { + ExprKind::Op(OpKind::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, _)) => { + PartialExpr(ExprKind::Op(OpKind::Projection(v2, _))) => { return normalize_one_layer( - ExprKind::Projection(v2.clone(), ls.clone()), + ExprKind::Op(OpKind::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, - ) + ExprKind::Op(OpKind::ProjectionByExpr(ref v, ref t)) => { + match t.kind() { + RecordType(kts) => { + return normalize_one_layer( + ExprKind::Op(OpKind::Projection( + v.clone(), + kts.keys().cloned().collect(), + )), + env, + ) + } + _ => Ret::Expr(expr), } - _ => Ret::Expr(expr), - }, + } - ExprKind::Merge(ref handlers, ref variant, _) => { + ExprKind::Op(OpKind::Merge(ref handlers, ref variant, _)) => { match handlers.kind() { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { @@ -431,7 +457,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { _ => Ret::Expr(expr), } } - ExprKind::ToMap(ref v, ref annot) => match v.kind() { + ExprKind::Op(OpKind::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)) => { -- cgit v1.2.3 From 7efdbd11db0f54f065d4dc41f0cab4b158d4515c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 18:33:58 +0100 Subject: Factor our operations in normalization --- dhall/src/semantics/nze/normalize.rs | 553 ++++++++++++++++------------------- 1 file changed, 255 insertions(+), 298 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index ebf4ae1..bf37a3c 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -4,7 +4,7 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; use crate::syntax::{ - BinOp, ExprKind, InterpolatedTextContents, NumKind, OpKind, + BinOp, ExprKind, InterpolatedTextContents, Label, NumKind, OpKind, }; pub fn apply_any(f: Nir, a: Nir) -> NirKind { @@ -83,79 +83,82 @@ where kvs } -// Small helper enum to avoid repetition -enum Ret<'a> { - NirKind(NirKind), - Nir(Nir), - NirRef(&'a Nir), - Expr(ExprKind), +type Ret = NirKind; + +fn ret_nir(x: Nir) -> Ret { + ret_ref(&x) +} +fn ret_kind(x: NirKind) -> Ret { + x +} +fn ret_ref(x: &Nir) -> Ret { + x.kind().clone() +} +fn ret_expr(x: ExprKind) -> Ret { + NirKind::PartialExpr(x) } -fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; +fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { + use BinOp::*; 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))), + (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::NirRef(y), - (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x), + (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), + (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - Ret::NirKind(Num(Natural(x + y))) + ret_kind(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(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::NirKind(Num(Natural(x * y))) + ret_kind(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(), - )), + (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::NirRef(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x), + (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::NirKind(NirKind::TextLit(x.concat(y))) + ret_kind(NirKind::TextLit(x.concat(y))) } - (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit( + (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( x.concat(&TextLit::interpolate(y.clone())), )), - (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit( + (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( TextLit::interpolate(x.clone()).concat(y), )), (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) + ret_ref(x) } (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) + ret_ref(y) } (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let mut kvs = kvs2.clone(); @@ -163,15 +166,15 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::NirKind(RecordLit(kvs)) + ret_kind(RecordLit(kvs)) } - (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y), + (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) + ret_ref(x) } (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) + ret_ref(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { @@ -181,7 +184,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { v2.clone(), ))) }); - Ret::NirKind(RecordLit(kvs)) + ret_kind(RecordLit(kvs)) } (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { @@ -197,276 +200,153 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { ))) }, ); - Ret::NirKind(RecordType(kts)) + ret_kind(RecordType(kts)) } (Equivalence, _, _) => { - Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone())) + ret_kind(NirKind::Equivalence(x.clone(), y.clone())) } _ => return None, }) } -#[allow(clippy::cognitive_complexity)] -pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { - use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, - UnionType, - }; - use NumKind::Bool; - - let ret = match expr { - ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { - unreachable!("This case should have been handled in resolution") - } - ExprKind::Var(..) - | ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) => unreachable!( - "This case should have been handled in normalize_hir_whnf" - ), +fn normalize_field(v: &Nir, field: &Label) -> Option { + use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; + use ExprKind::Op; + use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; + use OpKind::{BinOp, Field, Projection}; - 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::Op(OpKind::App(v, a)) => Ret::Nir(v.app(a)), - ExprKind::Num(l) => Ret::NirKind(Num(l)), - ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), - ExprKind::EmptyListLit(t) => { - let arg = match t.kind() { - NirKind::ListType(t) => t.clone(), - _ => panic!("internal type error"), - }; - Ret::NirKind(NirKind::EmptyListLit(arg)) - } - ExprKind::NEListLit(elts) => { - Ret::NirKind(NEListLit(elts.into_iter().collect())) - } - ExprKind::RecordLit(kvs) => { - Ret::NirKind(RecordLit(kvs.into_iter().collect())) - } - ExprKind::RecordType(kvs) => { - Ret::NirKind(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::Op(OpKind::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::Op(OpKind::BinOp(o, ref x, ref y)) => { - match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - } + Some(match v.kind() { + RecordLit(kvs) => match kvs.get(field) { + Some(r) => ret_nir(r.clone()), + None => return None, + }, + UnionType(kts) => { + ret_kind(UnionConstructor(field.clone(), kts.clone())) } - - ExprKind::Op(OpKind::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::Op(OpKind::Projection(x, _))) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field(x.clone(), field.clone())), - env, - ) - } - PartialExpr(ExprKind::Op(OpKind::BinOp( - BinOp::RightBiasedRecordMerge, - x, - y, - ))) => match (x.kind(), y.kind()) { + PartialExpr(Op(Projection(x, _))) => return normalize_field(x, field), + PartialExpr(Op(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::Op(OpKind::Field( - x.clone(), - field.clone(), - )), - env, - ) - } + Some(r) => ret_nir(r.clone()), + None => return normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RightBiasedRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - y.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(y, field), }, - _ => Ret::Expr(expr), - }, - PartialExpr(ExprKind::Op(OpKind::BinOp( - BinOp::RecursiveRecordMerge, - x, - y, - ))) => match (x.kind(), y.kind()) { + _ => return None, + } + } + PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { + match (x.kind(), y.kind()) { (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RecursiveRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - y.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(y, field), }, (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RecursiveRecordMerge, + x.clone(), + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - x.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(x, field), }, - _ => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - }, - ExprKind::Op(OpKind::Projection(_, ref ls)) if ls.is_empty() => { - Ret::NirKind(RecordLit(HashMap::new())) - } - ExprKind::Op(OpKind::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::Op(OpKind::Projection(v2, _))) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Projection(v2.clone(), ls.clone())), - env, - ) - } - _ => Ret::Expr(expr), - }, - ExprKind::Op(OpKind::ProjectionByExpr(ref v, ref t)) => { - match t.kind() { - RecordType(kts) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Projection( - v.clone(), - kts.keys().cloned().collect(), - )), - env, - ) - } - _ => Ret::Expr(expr), + _ => return None, } } + _ => return None, + }) +} - ExprKind::Op(OpKind::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), +fn normalize_operation(opkind: &OpKind) -> Option { + use ExprKind::Op; + use NirKind::{ + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, + PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + }; + use NumKind::Bool; + use OpKind::*; + + Some(match opkind { + App(v, a) => ret_nir(v.app(a.clone())), + BinOp(o, x, y) => return 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), + _ => return None, + } + } } } - ExprKind::Op(OpKind::ToMap(ref v, ref annot)) => match v.kind() { + Merge(handlers, variant, _) => match handlers.kind() { + RecordLit(kvs) => match variant.kind() { + UnionConstructor(l, _) => match kvs.get(l) { + Some(h) => ret_nir(h.clone()), + None => return None, + }, + UnionLit(l, v, _) => match kvs.get(l) { + Some(h) => ret_nir(h.app(v.clone())), + None => return None, + }, + EmptyOptionalLit(_) => match kvs.get(&"None".into()) { + Some(h) => ret_nir(h.clone()), + None => return None, + }, + NEOptionalLit(v) => match kvs.get(&"Some".into()) { + Some(h) => ret_nir(h.app(v.clone())), + None => return None, + }, + _ => return None, + }, + _ => return None, + }, + 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::NirKind(EmptyListLit(t.clone())) + ret_kind(EmptyListLit(t.clone())) } - _ => Ret::Expr(expr), + _ => return None, } } - RecordLit(kvs) => Ret::NirKind(NEListLit( + RecordLit(kvs) => ret_kind(NEListLit( kvs.iter() .sorted_by_key(|(k, _)| *k) .map(|(k, v)| { @@ -477,23 +357,100 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { }) .collect(), )), - _ => Ret::Expr(expr), + _ => return None, + }, + Field(v, field) => return 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(), + )), + PartialExpr(Op(Projection(v2, _))) => { + return normalize_operation(&Projection(v2.clone(), ls.clone())) + } + _ => return None, + }, + ProjectionByExpr(v, t) => match t.kind() { + RecordType(kts) => { + return normalize_operation(&Projection( + v.clone(), + kts.keys().cloned().collect(), + )) + } + _ => return None, }, + Completion(..) => { + unreachable!("This case should have been handled in resolution") + } + }) +} + +pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { + use NirKind::{ + NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; - match ret { - Ret::NirKind(v) => v, - Ret::Nir(v) => v.kind().clone(), - Ret::NirRef(v) => v.kind().clone(), - Ret::Expr(expr) => NirKind::PartialExpr(expr), + match expr { + ExprKind::Var(..) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) => { + unreachable!("This case should have been handled in normalize_hir") + } + + ExprKind::Const(c) => ret_nir(Nir::from_const(c)), + ExprKind::Num(l) => ret_kind(Num(l)), + ExprKind::Builtin(b) => ret_nir(Nir::from_builtin_env(b, env)), + 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_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_kind(NirKind::EmptyListLit(arg)) + } + ExprKind::NEListLit(elts) => { + ret_kind(NEListLit(elts.into_iter().collect())) + } + ExprKind::RecordLit(kvs) => { + ret_kind(RecordLit(kvs.into_iter().collect())) + } + ExprKind::RecordType(kvs) => { + ret_kind(RecordType(kvs.into_iter().collect())) + } + ExprKind::UnionType(kvs) => { + ret_kind(UnionType(kvs.into_iter().collect())) + } + ExprKind::Op(ref op) => match normalize_operation(op) { + Some(ret) => ret, + None => ret_expr(expr), + }, + ExprKind::Annot(x, _) => ret_nir(x), + ExprKind::Assert(_) => ret_expr(expr), + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") + } } } /// 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 { -- cgit v1.2.3 From 28c36acc8af1e3ece9512c98aa9fd70fedf1b252 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 18:47:17 +0100 Subject: Avoid a few allocations --- dhall/src/semantics/nze/normalize.rs | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index bf37a3c..f6782af 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -7,14 +7,14 @@ use crate::syntax::{ BinOp, ExprKind, InterpolatedTextContents, Label, NumKind, OpKind, }; -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::Op(OpKind::App(f, a))), + _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f.clone(), a))), } } @@ -219,7 +219,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { Some(match v.kind() { RecordLit(kvs) => match kvs.get(field) { - Some(r) => ret_nir(r.clone()), + Some(r) => ret_ref(r), None => return None, }, UnionType(kts) => { @@ -229,7 +229,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { PartialExpr(Op(BinOp(RightBiasedRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_nir(r.clone()), + Some(r) => ret_ref(r), None => return normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { @@ -299,7 +299,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { use OpKind::*; Some(match opkind { - App(v, a) => ret_nir(v.app(a.clone())), + App(v, a) => ret_kind(v.app_to_kind(a.clone())), BinOp(o, x, y) => return normalize_binop(*o, x, y), BoolIf(b, e1, e2) => { match b.kind() { @@ -318,19 +318,19 @@ fn normalize_operation(opkind: &OpKind) -> Option { Merge(handlers, variant, _) => match handlers.kind() { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => ret_nir(h.clone()), + Some(h) => ret_ref(h), None => return None, }, UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => ret_nir(h.app(v.clone())), + Some(h) => ret_kind(h.app_to_kind(v.clone())), None => return None, }, EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => ret_nir(h.clone()), + Some(h) => ret_ref(h), None => return None, }, NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => ret_nir(h.app(v.clone())), + Some(h) => ret_kind(h.app_to_kind(v.clone())), None => return None, }, _ => return None, @@ -391,7 +391,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NirKind::{ - NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, + Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; match expr { @@ -402,14 +402,16 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { unreachable!("This case should have been handled in normalize_hir") } - ExprKind::Const(c) => ret_nir(Nir::from_const(c)), + ExprKind::Const(c) => ret_kind(Const(c)), ExprKind::Num(l) => ret_kind(Num(l)), - ExprKind::Builtin(b) => ret_nir(Nir::from_builtin_env(b, env)), + 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_nir(v.clone()) + ret_ref(v) } else { ret_kind(NirKind::TextLit(tlit)) } -- cgit v1.2.3 From 4ed17cb88df732d3ce3d09e2bfd0b7c855309094 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 19:08:51 +0100 Subject: Fix normalization bug --- dhall/src/semantics/nze/normalize.rs | 98 ++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index f6782af..532d2e4 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -97,13 +97,16 @@ fn ret_ref(x: &Nir) -> Ret { fn ret_expr(x: ExprKind) -> Ret { NirKind::PartialExpr(x) } +fn ret_op(x: OpKind) -> Ret { + ret_expr(ExprKind::Op(x)) +} -fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { +fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { use BinOp::*; use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; use NumKind::{Bool, Natural}; - Some(match (o, x.kind(), y.kind()) { + 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))), @@ -207,33 +210,34 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { ret_kind(NirKind::Equivalence(x.clone(), y.clone())) } - _ => return None, - }) + _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), + } } -fn normalize_field(v: &Nir, field: &Label) -> Option { +fn normalize_field(v: &Nir, field: &Label) -> Ret { use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; use ExprKind::Op; use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; use OpKind::{BinOp, Field, Projection}; + let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); - Some(match v.kind() { + match v.kind() { RecordLit(kvs) => match kvs.get(field) { Some(r) => ret_ref(r), - None => return None, + None => nothing_to_do(), }, UnionType(kts) => { ret_kind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(Op(Projection(x, _))) => return normalize_field(x, field), + PartialExpr(Op(Projection(x, _))) => normalize_field(x, field), PartialExpr(Op(BinOp(RightBiasedRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (_, RecordLit(kvs)) => match kvs.get(field) { Some(r) => ret_ref(r), - None => return normalize_field(x, field), + None => normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RightBiasedRecordMerge, Nir::from_kind(RecordLit( @@ -244,16 +248,16 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { y.clone(), )))), field.clone(), - ))), - None => return normalize_field(y, field), + )), + None => normalize_field(y, field), }, - _ => return None, + _ => nothing_to_do(), } } PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RecursiveRecordMerge, Nir::from_kind(RecordLit( @@ -264,11 +268,11 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { y.clone(), )))), field.clone(), - ))), - None => return normalize_field(y, field), + )), + None => normalize_field(y, field), }, (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RecursiveRecordMerge, x.clone(), @@ -279,17 +283,17 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { )), )))), field.clone(), - ))), - None => return normalize_field(x, field), + )), + None => normalize_field(x, field), }, - _ => return None, + _ => nothing_to_do(), } } - _ => return None, - }) + _ => nothing_to_do(), + } } -fn normalize_operation(opkind: &OpKind) -> Option { +fn normalize_operation(opkind: &OpKind) -> Ret { use ExprKind::Op; use NirKind::{ EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, @@ -297,10 +301,11 @@ fn normalize_operation(opkind: &OpKind) -> Option { }; use NumKind::Bool; use OpKind::*; + let nothing_to_do = || ret_op(opkind.clone()); - Some(match opkind { + match opkind { App(v, a) => ret_kind(v.app_to_kind(a.clone())), - BinOp(o, x, y) => return normalize_binop(*o, x, y), + BinOp(o, x, y) => normalize_binop(*o, x, y), BoolIf(b, e1, e2) => { match b.kind() { Num(Bool(true)) => ret_ref(e1), @@ -310,7 +315,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { // Simplify `if b then True else False` (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), _ if e1 == e2 => ret_ref(e1), - _ => return None, + _ => nothing_to_do(), } } } @@ -319,23 +324,23 @@ fn normalize_operation(opkind: &OpKind) -> Option { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { Some(h) => ret_ref(h), - None => return None, + None => nothing_to_do(), }, UnionLit(l, v, _) => match kvs.get(l) { Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => return None, + None => nothing_to_do(), }, EmptyOptionalLit(_) => match kvs.get(&"None".into()) { Some(h) => ret_ref(h), - None => return None, + None => nothing_to_do(), }, NEOptionalLit(v) => match kvs.get(&"Some".into()) { Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => return None, + None => nothing_to_do(), }, - _ => return None, + _ => nothing_to_do(), }, - _ => return None, + _ => nothing_to_do(), }, ToMap(v, annot) => match v.kind() { RecordLit(kvs) if kvs.is_empty() => { @@ -343,7 +348,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { Some(NirKind::ListType(t)) => { ret_kind(EmptyListLit(t.clone())) } - _ => return None, + _ => nothing_to_do(), } } RecordLit(kvs) => ret_kind(NEListLit( @@ -357,9 +362,9 @@ fn normalize_operation(opkind: &OpKind) -> Option { }) .collect(), )), - _ => return None, + _ => nothing_to_do(), }, - Field(v, field) => return normalize_field(v, field), + Field(v, field) => normalize_field(v, field), Projection(_, ls) if ls.is_empty() => { ret_kind(RecordLit(HashMap::new())) } @@ -370,23 +375,21 @@ fn normalize_operation(opkind: &OpKind) -> Option { .collect(), )), PartialExpr(Op(Projection(v2, _))) => { - return normalize_operation(&Projection(v2.clone(), ls.clone())) + normalize_operation(&Projection(v2.clone(), ls.clone())) } - _ => return None, + _ => nothing_to_do(), }, ProjectionByExpr(v, t) => match t.kind() { - RecordType(kts) => { - return normalize_operation(&Projection( - v.clone(), - kts.keys().cloned().collect(), - )) - } - _ => return None, + 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, env: &NzEnv) -> NirKind { @@ -436,10 +439,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { ExprKind::UnionType(kvs) => { ret_kind(UnionType(kvs.into_iter().collect())) } - ExprKind::Op(ref op) => match normalize_operation(op) { - Some(ret) => ret, - None => ret_expr(expr), - }, + ExprKind::Op(ref op) => normalize_operation(op), ExprKind::Annot(x, _) => ret_nir(x), ExprKind::Assert(_) => ret_expr(expr), ExprKind::Import(..) => { -- cgit v1.2.3 From cd3b11cc8bd7c4397071d1d3b4b9020b7d5ff2ad Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 21:33:45 +0100 Subject: Only need to store OpKind in Nir --- dhall/src/semantics/nze/normalize.rs | 138 +++++++++++++++++------------------ 1 file changed, 65 insertions(+), 73 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 532d2e4..c0e41cb 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -14,7 +14,7 @@ pub fn apply_any(f: &Nir, a: Nir) -> NirKind { NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f.clone(), a))), + _ => NirKind::Op(OpKind::App(f.clone(), a)), } } @@ -94,11 +94,8 @@ fn ret_kind(x: NirKind) -> Ret { fn ret_ref(x: &Nir) -> Ret { x.kind().clone() } -fn ret_expr(x: ExprKind) -> Ret { - NirKind::PartialExpr(x) -} fn ret_op(x: OpKind) -> Ret { - ret_expr(ExprKind::Op(x)) + NirKind::Op(x) } fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { @@ -216,8 +213,7 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { fn normalize_field(v: &Nir, field: &Label) -> Ret { use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; - use ExprKind::Op; - use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; + use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; use OpKind::{BinOp, Field, Projection}; let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); @@ -229,75 +225,70 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret { UnionType(kts) => { ret_kind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(Op(Projection(x, _))) => normalize_field(x, field), - PartialExpr(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(PartialExpr(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(), - } - } - PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { - match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(PartialExpr(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(PartialExpr(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(), - } - } + 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) -> Ret { - use ExprKind::Op; use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, + RecordLit, RecordType, UnionConstructor, UnionLit, }; use NumKind::Bool; use OpKind::*; @@ -374,7 +365,7 @@ fn normalize_operation(opkind: &OpKind) -> Ret { .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) .collect(), )), - PartialExpr(Op(Projection(v2, _))) => { + Op(Projection(v2, _)) => { normalize_operation(&Projection(v2.clone(), ls.clone())) } _ => nothing_to_do(), @@ -394,7 +385,8 @@ fn normalize_operation(opkind: &OpKind) -> Ret { pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NirKind::{ - Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, + Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, + UnionType, }; match expr { @@ -441,7 +433,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { } ExprKind::Op(ref op) => normalize_operation(op), ExprKind::Annot(x, _) => ret_nir(x), - ExprKind::Assert(_) => ret_expr(expr), + ExprKind::Assert(x) => ret_kind(Assert(x)), ExprKind::Import(..) => { unreachable!("This case should have been handled in resolution") } -- cgit v1.2.3 From fff4c46e09d4edf25eba737f4d71bfdb1dbf4a82 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 22:11:54 +0100 Subject: Extract operation-related code to a new module --- dhall/src/semantics/nze/normalize.rs | 301 +---------------------------------- 1 file changed, 7 insertions(+), 294 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') 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) -> Ret { +pub fn ret_op(x: OpKind) -> 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) -> 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, env: &NzEnv) -> NirKind { use NirKind::{ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, -- cgit v1.2.3