From 035f6fd4d952470828f58943f45f3c2b1d1a723f Mon Sep 17 00:00:00 2001 From: Folkert Date: Fri, 24 Jan 2020 23:09:12 +0100 Subject: [PATCH] switch to using BDD simplification --- Cargo.lock | 23 +++++++++++++++++++++++ Cargo.toml | 1 + src/uniqueness/boolean_algebra.rs | 30 ++++++++++++++++++++++++++++++ src/uniqueness/mod.rs | 4 ++-- tests/test_uniqueness_infer.rs | 23 +++++++++++------------ 5 files changed, 67 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index eb226120e5..1e752b379d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -34,6 +34,15 @@ dependencies = [ "typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)", ] +[[package]] +name = "boolean_expression" +version = "0.3.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +dependencies = [ + "itertools 0.4.19 (registry+https://github.com/rust-lang/crates.io-index)", + "smallvec 0.1.8 (registry+https://github.com/rust-lang/crates.io-index)", +] + [[package]] name = "bumpalo" version = "2.6.0" @@ -390,6 +399,11 @@ name = "inlinable_string" version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" +[[package]] +name = "itertools" +version = "0.4.19" +source = "registry+https://github.com/rust-lang/crates.io-index" + [[package]] name = "lazy_static" version = "1.4.0" @@ -746,6 +760,7 @@ dependencies = [ name = "roc" version = "0.1.0" dependencies = [ + "boolean_expression 0.3.10 (registry+https://github.com/rust-lang/crates.io-index)", "bumpalo 2.6.0 (registry+https://github.com/rust-lang/crates.io-index)", "cranelift 0.52.0 (registry+https://github.com/rust-lang/crates.io-index)", "cranelift-codegen 0.52.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -809,6 +824,11 @@ name = "slab" version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" +[[package]] +name = "smallvec" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" + [[package]] name = "smallvec" version = "1.1.0" @@ -934,6 +954,7 @@ dependencies = [ "checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2" "checksum bitflags 1.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693" "checksum bitmaps 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)" = "81e039a80914325b37fde728ef7693c212f0ac913d5599607d7b95a9484aae0b" +"checksum boolean_expression 0.3.10 (registry+https://github.com/rust-lang/crates.io-index)" = "c32d4ff2e41efaa15713e03e15dc99b1bd7e1aa0f60513e2717d0669e12cc913" "checksum bumpalo 2.6.0 (registry+https://github.com/rust-lang/crates.io-index)" = "ad807f2fc2bf185eeb98ff3a901bd46dc5ad58163d0fa4577ba0d25674d71708" "checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5" "checksum bytes 0.5.3 (registry+https://github.com/rust-lang/crates.io-index)" = "10004c15deb332055f7a4a208190aed362cf9a7c2f6ab70a305fba50e1105f38" @@ -976,6 +997,7 @@ dependencies = [ "checksum inkwell 0.1.0 (git+https://github.com/TheDan64/inkwell?branch=llvm8-0)" = "" "checksum inkwell_internals 0.1.0 (git+https://github.com/TheDan64/inkwell?branch=llvm8-0)" = "" "checksum inlinable_string 0.1.10 (registry+https://github.com/rust-lang/crates.io-index)" = "ee79c89e76de0c42c07b2d2815a47d6951b365dd16abc8689bef5d5a36d8acd9" +"checksum itertools 0.4.19 (registry+https://github.com/rust-lang/crates.io-index)" = "c4a9b56eb56058f43dc66e58f40a214b2ccbc9f3df51861b63d51dec7b65bc3f" "checksum lazy_static 1.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" "checksum libc 0.2.66 (registry+https://github.com/rust-lang/crates.io-index)" = "d515b1f41455adea1313a4a2ac8a8a477634fbae63cc6100e3aebb207ce61558" "checksum llvm-sys 80.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "cf2969773884a5701f0c255e2a14d48d4522a66db898ec1088cb21879a228377" @@ -1025,6 +1047,7 @@ dependencies = [ "checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3" "checksum sized-chunks 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "6f59f81ec9833a580d2448e958d16bd872637798f3ab300b693c48f136fb76ff" "checksum slab 0.4.2 (registry+https://github.com/rust-lang/crates.io-index)" = "c111b5bd5695e56cffe5129854aa230b39c93a305372fdbb2668ca2394eea9f8" +"checksum smallvec 0.1.8 (registry+https://github.com/rust-lang/crates.io-index)" = "fcc8d19212aacecf95e4a7a2179b26f7aeb9732a915cf01f05b0d3e044865410" "checksum smallvec 1.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "44e59e0c9fa00817912ae6e4e6e3c4fe04455e75699d06eedc7d85917ed8e8f4" "checksum syn 0.15.44 (registry+https://github.com/rust-lang/crates.io-index)" = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" "checksum syn 1.0.14 (registry+https://github.com/rust-lang/crates.io-index)" = "af6f3550d8dff9ef7dc34d384ac6f107e5d31c8f57d9f28e0081503f547ac8f5" diff --git a/Cargo.toml b/Cargo.toml index 135d0a236d..b7785f540a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,6 +13,7 @@ wyhash = "0.3" tokio = { version = "0.2", features = ["blocking", "fs", "sync", "rt-threaded"] } bumpalo = "2.6" inlinable_string = "0.1.0" +boolean_expression = "0.3.10" # NOTE: Breaking API changes get pushed directly to this Inkwell branch, so be # very careful when running `cargo update` to get a new revision into Cargo.lock. # diff --git a/src/uniqueness/boolean_algebra.rs b/src/uniqueness/boolean_algebra.rs index 9eb26aa2f8..1e8f2aea02 100644 --- a/src/uniqueness/boolean_algebra.rs +++ b/src/uniqueness/boolean_algebra.rs @@ -10,6 +10,29 @@ // > Boolean Equations" by Frank Markham Brown. use crate::collections::{ImMap, ImSet}; use crate::subs::Variable; +use boolean_expression::Expr; + +fn bool_to_expr(b: Bool) -> Expr { + match b { + Zero => Expr::Const(false), + One => Expr::Const(true), + And(a, b) => Expr::And(Box::new(bool_to_expr(*a)), Box::new(bool_to_expr(*b))), + Or(a, b) => Expr::Or(Box::new(bool_to_expr(*a)), Box::new(bool_to_expr(*b))), + Not(a) => Expr::Not(Box::new(bool_to_expr(*a))), + Variable(v) => Expr::Terminal(v), + } +} + +fn expr_to_bool(e: Expr) -> Bool { + match e { + Expr::Const(false) => Zero, + Expr::Const(true) => One, + Expr::And(a, b) => And(Box::new(expr_to_bool(*a)), Box::new(expr_to_bool(*b))), + Expr::Or(a, b) => Or(Box::new(expr_to_bool(*a)), Box::new(expr_to_bool(*b))), + Expr::Not(a) => Not(Box::new(expr_to_bool(*a))), + Expr::Terminal(v) => Variable(v), + } +} #[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub enum Bool { @@ -154,11 +177,18 @@ impl Bool { } pub fn simplify(term: Bool) -> Bool { + /* let normalized = normalize_term(term); let a = term_to_sop(normalized); let b = normalize_sop(a); let after_bcf = bcf(b); sop_to_term_vector(simplify_sop_vector(after_bcf)) + */ + + let expr = bool_to_expr(term); + let simplified = expr.simplify_via_bdd(); + + expr_to_bool(simplified) } #[inline(always)] diff --git a/src/uniqueness/mod.rs b/src/uniqueness/mod.rs index 0aeb6fe7d3..94e23593c0 100644 --- a/src/uniqueness/mod.rs +++ b/src/uniqueness/mod.rs @@ -685,7 +685,7 @@ pub fn constrain_expr( var_usage, env, region, - &loc_when_pattern.pattern, + &loc_pattern.pattern, loc_expr, PExpected::ForReason( PReason::WhenMatch { index }, @@ -718,7 +718,7 @@ pub fn constrain_expr( var_usage, env, region, - &loc_when_pattern.pattern, + &loc_pattern.pattern, loc_expr, PExpected::ForReason( PReason::WhenMatch { index }, diff --git a/tests/test_uniqueness_infer.rs b/tests/test_uniqueness_infer.rs index 11f2cfa717..6456ef2544 100644 --- a/tests/test_uniqueness_infer.rs +++ b/tests/test_uniqueness_infer.rs @@ -1197,18 +1197,17 @@ mod test_infer_uniq { ); } - // TODO fails because of bug in boolean simplifier - // #[test] - // fn sharing_analysis_record_update_use_twice_access() { - // infer_eq( - // indoc!( - // r#" - // \r -> { r & x: r.x, y: r.y } - // "# - // ), - // "Attr.Attr * (Attr.Attr Attr.Shared { x : (Attr.Attr Attr.Shared a), y : (Attr.Attr Attr.Shared b) }c -> Attr.Attr Attr.Shared { x : (Attr.Attr Attr.Shared a), y : (Attr.Attr Attr.Shared b) }c)" , - // ); - // } + #[test] + fn sharing_analysis_record_update_use_twice_access() { + infer_eq( + indoc!( + r#" + \r -> { r & x: r.x, y: r.y } + "# + ), + "Attr.Attr * (Attr.Attr Attr.Shared { x : (Attr.Attr Attr.Shared a), y : (Attr.Attr Attr.Shared b) }c -> Attr.Attr Attr.Shared { x : (Attr.Attr Attr.Shared a), y : (Attr.Attr Attr.Shared b) }c)" , + ); + } #[test] fn sharing_analysis_record_update_duplicate_field() {