summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/operations/kind.rs97
-rw-r--r--dhall/src/operations/mod.rs6
-rw-r--r--dhall/src/operations/normalization.rs306
-rw-r--r--dhall/src/operations/typecheck.rs (renamed from dhall/src/operations.rs)402
4 files changed, 414 insertions, 397 deletions
diff --git a/dhall/src/operations/kind.rs b/dhall/src/operations/kind.rs
new file mode 100644
index 0000000..5415637
--- /dev/null
+++ b/dhall/src/operations/kind.rs
@@ -0,0 +1,97 @@
+use std::collections::BTreeSet;
+
+use crate::syntax::{trivial_result, Label};
+
+// Definition order must match precedence order for
+// pretty-printing to work correctly
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum BinOp {
+ /// `x ? y`
+ ImportAlt,
+ /// `x || y`
+ BoolOr,
+ /// `x + y`
+ NaturalPlus,
+ /// `x ++ y`
+ TextAppend,
+ /// `x # y`
+ ListAppend,
+ /// `x && y`
+ BoolAnd,
+ /// `x ∧ y`
+ RecursiveRecordMerge,
+ /// `x ⫽ y`
+ RightBiasedRecordMerge,
+ /// `x ⩓ y`
+ RecursiveRecordTypeMerge,
+ /// `x * y`
+ NaturalTimes,
+ /// `x == y`
+ BoolEQ,
+ /// `x != y`
+ BoolNE,
+ /// x === y
+ Equivalence,
+}
+
+/// Operations
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum OpKind<SubExpr> {
+ /// `f a`
+ App(SubExpr, SubExpr),
+ /// Binary operations
+ BinOp(BinOp, SubExpr, SubExpr),
+ /// `if x then y else z`
+ BoolIf(SubExpr, SubExpr, SubExpr),
+ /// `merge x y : t`
+ Merge(SubExpr, SubExpr, Option<SubExpr>),
+ /// `toMap x : t`
+ ToMap(SubExpr, Option<SubExpr>),
+ /// `e.x`
+ Field(SubExpr, Label),
+ /// `e.{ x, y, z }`
+ Projection(SubExpr, BTreeSet<Label>),
+ /// `e.(t)`
+ ProjectionByExpr(SubExpr, SubExpr),
+ /// `x::y`
+ Completion(SubExpr, SubExpr),
+}
+
+impl<SE> OpKind<SE> {
+ pub fn traverse_ref<'a, SE2, Err>(
+ &'a self,
+ mut f: impl FnMut(&'a SE) -> Result<SE2, Err>,
+ ) -> Result<OpKind<SE2>, Err> {
+ // Can't use closures because of borrowing rules
+ macro_rules! expr {
+ ($e:expr) => {
+ f($e)?
+ };
+ }
+ macro_rules! opt {
+ ($e:expr) => {
+ $e.as_ref().map(|e| Ok(expr!(e))).transpose()?
+ };
+ }
+
+ use OpKind::*;
+ Ok(match self {
+ App(f, a) => App(expr!(f), expr!(a)),
+ BinOp(o, x, y) => BinOp(*o, expr!(x), expr!(y)),
+ BoolIf(b, t, f) => BoolIf(expr!(b), expr!(t), expr!(f)),
+ Merge(x, y, t) => Merge(expr!(x), expr!(y), opt!(t)),
+ ToMap(x, t) => ToMap(expr!(x), opt!(t)),
+ Field(e, l) => Field(expr!(e), l.clone()),
+ Projection(e, ls) => Projection(expr!(e), ls.clone()),
+ ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)),
+ Completion(e, x) => Completion(expr!(e), expr!(x)),
+ })
+ }
+
+ pub fn map_ref<'a, SE2>(
+ &'a self,
+ mut f: impl FnMut(&'a SE) -> SE2,
+ ) -> OpKind<SE2> {
+ trivial_result(self.traverse_ref(|x| Ok(f(x))))
+ }
+}
diff --git a/dhall/src/operations/mod.rs b/dhall/src/operations/mod.rs
new file mode 100644
index 0000000..1a3b65b
--- /dev/null
+++ b/dhall/src/operations/mod.rs
@@ -0,0 +1,6 @@
+mod kind;
+mod normalization;
+mod typecheck;
+pub use kind::*;
+pub use normalization::*;
+pub use typecheck::*;
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
new file mode 100644
index 0000000..e3a9415
--- /dev/null
+++ b/dhall/src/operations/normalization.rs
@@ -0,0 +1,306 @@
+use itertools::Itertools;
+use std::collections::HashMap;
+use std::iter::once;
+
+use crate::operations::{BinOp, OpKind};
+use crate::semantics::{
+ merge_maps, ret_kind, ret_op, ret_ref, Nir, NirKind, Ret, TextLit,
+};
+use crate::syntax::{ExprKind, Label, NumKind};
+
+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(
+ once((field.clone(), r.clone())).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(
+ once((field.clone(), r.clone())).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(
+ once((field.clone(), r.clone())).collect(),
+ )),
+ ))),
+ field.clone(),
+ )),
+ None => normalize_field(x, field),
+ },
+ _ => nothing_to_do(),
+ },
+ _ => nothing_to_do(),
+ }
+}
+
+pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
+ use self::BinOp::RightBiasedRecordMerge;
+ 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()))
+ }
+ Op(BinOp(RightBiasedRecordMerge, l, r)) => match r.kind() {
+ RecordLit(kvs) => {
+ let r_keys = kvs.keys().cloned().collect();
+ normalize_operation(&BinOp(
+ RightBiasedRecordMerge,
+ Nir::from_partial_expr(ExprKind::Op(Projection(
+ l.clone(),
+ ls.difference(&r_keys).cloned().collect(),
+ ))),
+ Nir::from_partial_expr(ExprKind::Op(Projection(
+ r.clone(),
+ ls.intersection(&r_keys).cloned().collect(),
+ ))),
+ ))
+ }
+ _ => nothing_to_do(),
+ },
+ _ => 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")
+ }
+ }
+}
diff --git a/dhall/src/operations.rs b/dhall/src/operations/typecheck.rs
index c95159c..91d5059 100644
--- a/dhall/src/operations.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -1,110 +1,15 @@
-use itertools::Itertools;
use std::borrow::Cow;
use std::cmp::max;
-use std::collections::{BTreeSet, HashMap};
-use std::iter::once;
+use std::collections::HashMap;
use crate::builtins::Builtin;
use crate::error::{ErrorBuilder, TypeError};
+use crate::operations::{BinOp, OpKind};
use crate::semantics::{
- merge_maps, mk_span_err, mkerr, ret_kind, ret_op, ret_ref, Binder, Closure,
- Hir, HirKind, Nir, NirKind, Ret, TextLit, Tir, TyEnv, Type,
+ merge_maps, mk_span_err, mkerr, Binder, Closure, Hir, HirKind, Nir,
+ NirKind, Tir, TyEnv, Type,
};
-use crate::syntax::{trivial_result, Const, ExprKind, Label, NumKind, Span};
-
-// Definition order must match precedence order for
-// pretty-printing to work correctly
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum BinOp {
- /// `x ? y`
- ImportAlt,
- /// `x || y`
- BoolOr,
- /// `x + y`
- NaturalPlus,
- /// `x ++ y`
- TextAppend,
- /// `x # y`
- ListAppend,
- /// `x && y`
- BoolAnd,
- /// `x ∧ y`
- RecursiveRecordMerge,
- /// `x ⫽ y`
- RightBiasedRecordMerge,
- /// `x ⩓ y`
- RecursiveRecordTypeMerge,
- /// `x * y`
- NaturalTimes,
- /// `x == y`
- BoolEQ,
- /// `x != y`
- BoolNE,
- /// x === y
- Equivalence,
-}
-
-/// Operations
-#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum OpKind<SubExpr> {
- /// `f a`
- App(SubExpr, SubExpr),
- /// Binary operations
- BinOp(BinOp, SubExpr, SubExpr),
- /// `if x then y else z`
- BoolIf(SubExpr, SubExpr, SubExpr),
- /// `merge x y : t`
- Merge(SubExpr, SubExpr, Option<SubExpr>),
- /// `toMap x : t`
- ToMap(SubExpr, Option<SubExpr>),
- /// `e.x`
- Field(SubExpr, Label),
- /// `e.{ x, y, z }`
- Projection(SubExpr, BTreeSet<Label>),
- /// `e.(t)`
- ProjectionByExpr(SubExpr, SubExpr),
- /// `x::y`
- Completion(SubExpr, SubExpr),
-}
-
-impl<SE> OpKind<SE> {
- pub fn traverse_ref<'a, SE2, Err>(
- &'a self,
- mut f: impl FnMut(&'a SE) -> Result<SE2, Err>,
- ) -> Result<OpKind<SE2>, Err> {
- // Can't use closures because of borrowing rules
- macro_rules! expr {
- ($e:expr) => {
- f($e)?
- };
- }
- macro_rules! opt {
- ($e:expr) => {
- $e.as_ref().map(|e| Ok(expr!(e))).transpose()?
- };
- }
-
- use OpKind::*;
- Ok(match self {
- App(f, a) => App(expr!(f), expr!(a)),
- BinOp(o, x, y) => BinOp(*o, expr!(x), expr!(y)),
- BoolIf(b, t, f) => BoolIf(expr!(b), expr!(t), expr!(f)),
- Merge(x, y, t) => Merge(expr!(x), expr!(y), opt!(t)),
- ToMap(x, t) => ToMap(expr!(x), opt!(t)),
- Field(e, l) => Field(expr!(e), l.clone()),
- Projection(e, ls) => Projection(expr!(e), ls.clone()),
- ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)),
- Completion(e, x) => Completion(expr!(e), expr!(x)),
- })
- }
-
- pub fn map_ref<'a, SE2>(
- &'a self,
- mut f: impl FnMut(&'a SE) -> SE2,
- ) -> OpKind<SE2> {
- trivial_result(self.traverse_ref(|x| Ok(f(x))))
- }
-}
+use crate::syntax::{Const, ExprKind, Span};
fn check_rectymerge(
span: &Span,
@@ -603,300 +508,3 @@ pub fn typecheck_operation(
}
})
}
-
-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(
- once((field.clone(), r.clone())).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(
- once((field.clone(), r.clone())).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(
- once((field.clone(), r.clone())).collect(),
- )),
- ))),
- field.clone(),
- )),
- None => normalize_field(x, field),
- },
- _ => nothing_to_do(),
- },
- _ => nothing_to_do(),
- }
-}
-
-pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
- use self::BinOp::RightBiasedRecordMerge;
- 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()))
- }
- Op(BinOp(RightBiasedRecordMerge, l, r)) => match r.kind() {
- RecordLit(kvs) => {
- let r_keys = kvs.keys().cloned().collect();
- normalize_operation(&BinOp(
- RightBiasedRecordMerge,
- Nir::from_partial_expr(ExprKind::Op(Projection(
- l.clone(),
- ls.difference(&r_keys).cloned().collect(),
- ))),
- Nir::from_partial_expr(ExprKind::Op(Projection(
- r.clone(),
- ls.intersection(&r_keys).cloned().collect(),
- ))),
- ))
- }
- _ => nothing_to_do(),
- },
- _ => 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")
- }
- }
-}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-30 20:46:07 +0000