From c9c1b0f517b69a98b6d1c5ba811449a193d5fa53 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Fri, 26 Jan 2024 12:55:41 -0800 Subject: [PATCH 1/4] Disallow empty all --- tree_unique_args/src/disallow_empty_all.egg | 3 +++ tree_unique_args/src/disallow_empty_all.rs | 7 +++++++ tree_unique_args/src/lib.rs | 2 ++ 3 files changed, 12 insertions(+) create mode 100644 tree_unique_args/src/disallow_empty_all.egg create mode 100644 tree_unique_args/src/disallow_empty_all.rs diff --git a/tree_unique_args/src/disallow_empty_all.egg b/tree_unique_args/src/disallow_empty_all.egg new file mode 100644 index 000000000..0ef2cdc9c --- /dev/null +++ b/tree_unique_args/src/disallow_empty_all.egg @@ -0,0 +1,3 @@ +(rule ((ExprIsValid (All order (Nil)))) + ((panic "UnitExpr should be used instead of an empty All")) + :ruleset error-checking) diff --git a/tree_unique_args/src/disallow_empty_all.rs b/tree_unique_args/src/disallow_empty_all.rs new file mode 100644 index 000000000..0aebd0014 --- /dev/null +++ b/tree_unique_args/src/disallow_empty_all.rs @@ -0,0 +1,7 @@ +#[test] +#[should_panic] +fn empty_all_should_panic() { + let build = "(ExprIsValid (All (Parallel) (Nil)))"; + let check = ""; + let _ = crate::run_test(build, check); +} diff --git a/tree_unique_args/src/lib.rs b/tree_unique_args/src/lib.rs index 1caeddce1..45b478c37 100644 --- a/tree_unique_args/src/lib.rs +++ b/tree_unique_args/src/lib.rs @@ -2,6 +2,7 @@ pub mod ast; pub(crate) mod body_contains; pub(crate) mod conditional_invariant_code_motion; pub(crate) mod deep_copy; +pub(crate) mod disallow_empty_all; pub(crate) mod function_inlining; pub(crate) mod id_analysis; pub mod interpreter; @@ -142,6 +143,7 @@ pub fn run_test(build: &str, check: &str) -> Result { include_str!("sugar.egg"), &util::rules().join("\n"), &id_analysis::id_analysis_rules().join("\n"), + include_str!("disallow_empty_all.egg"), // optimizations include_str!("simple.egg"), include_str!("function_inlining.egg"), From a902058bf71a08d81656bfee188cd7f11634b531 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Fri, 26 Jan 2024 13:08:56 -0800 Subject: [PATCH 2/4] replace unit value/type with empty tuple --- tree_unique_args/src/interpreter.rs | 16 ++++++++-------- tree_unique_args/src/lib.rs | 2 -- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/tree_unique_args/src/interpreter.rs b/tree_unique_args/src/interpreter.rs index 4158a827b..76ee86f7a 100644 --- a/tree_unique_args/src/interpreter.rs +++ b/tree_unique_args/src/interpreter.rs @@ -21,7 +21,7 @@ pub fn typecheck(e: &Expr, arg_ty: &Option) -> Result { Expr::Program(_) => panic!("Found non top level program."), Expr::Num(_) => Ok(Type::Num), Expr::Boolean(_) => Ok(Type::Boolean), - Expr::Unit => Ok(Type::Unit), + Expr::Unit => Ok(Type::Tuple(vec![])), Expr::Add(e1, e2) | Expr::Sub(e1, e2) | Expr::Mul(e1, e2) => { expect_type(e1, Type::Num)?; expect_type(e2, Type::Num)?; @@ -71,7 +71,7 @@ pub fn typecheck(e: &Expr, arg_ty: &Option) -> Result { Expr::Print(e) => { // right now, only print nums expect_type(e, Type::Num)?; - Ok(Type::Unit) + Ok(Type::Tuple(vec![])) } Expr::Read(addr) => { // right now, all memory holds nums. @@ -83,7 +83,7 @@ pub fn typecheck(e: &Expr, arg_ty: &Option) -> Result { Expr::Write(addr, data) => { expect_type(addr, Type::Num)?; expect_type(data, Type::Num)?; - Ok(Type::Unit) + Ok(Type::Tuple(vec![])) } Expr::All(_, exprs) => { let tys = exprs @@ -138,7 +138,7 @@ pub fn interpret(e: &Expr, arg: &Option, vm: &mut VirtualMachine) -> Valu Expr::Program(_) => todo!("interpret programs"), Expr::Num(x) => Value::Num(*x), Expr::Boolean(x) => Value::Boolean(*x), - Expr::Unit => Value::Unit, + Expr::Unit => Value::Tuple(vec![]), Expr::Add(e1, e2) => { let Value::Num(n1) = interpret(e1, arg, vm) else { panic!("add") @@ -219,7 +219,7 @@ pub fn interpret(e: &Expr, arg: &Option, vm: &mut VirtualMachine) -> Valu panic!("print") }; vm.log.push(n); - Value::Unit + Value::Tuple(vec![]) } Expr::Read(e_addr) => { let Value::Num(addr) = interpret(e_addr, arg, vm) else { @@ -233,7 +233,7 @@ pub fn interpret(e: &Expr, arg: &Option, vm: &mut VirtualMachine) -> Valu }; let data = interpret(e_data, arg, vm); vm.mem.insert(addr as usize, data); - Value::Unit + Value::Tuple(vec![]) } Expr::All(_, exprs) => { // this always executes sequentially (which is a valid way to @@ -370,8 +370,8 @@ fn test_interpreter_fib_using_memory() { assert_eq!( res, Value::Tuple(vec![ - Value::Unit, - Value::Unit, + Value::Tuple(vec![]), + Value::Tuple(vec![]), Value::Num(nth + 1), Value::Num(fib_nth) ]) diff --git a/tree_unique_args/src/lib.rs b/tree_unique_args/src/lib.rs index 45b478c37..a66431b9c 100644 --- a/tree_unique_args/src/lib.rs +++ b/tree_unique_args/src/lib.rs @@ -110,7 +110,6 @@ impl Expr { pub enum Value { Num(i64), Boolean(bool), - Unit, Tuple(Vec), } @@ -118,7 +117,6 @@ pub enum Value { pub enum Type { Num, Boolean, - Unit, Tuple(Vec), } From 671b3c46760b791cb52f3e9f0c8bc6c5ee30cf8f Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Fri, 26 Jan 2024 13:13:28 -0800 Subject: [PATCH 3/4] Remove UnitT from type analysis --- tree_unique_args/src/type_analysis.egg | 5 ++--- tree_unique_args/src/type_analysis.rs | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/tree_unique_args/src/type_analysis.egg b/tree_unique_args/src/type_analysis.egg index eaab2f245..249be7c88 100644 --- a/tree_unique_args/src/type_analysis.egg +++ b/tree_unique_args/src/type_analysis.egg @@ -5,7 +5,6 @@ (datatype Type (IntT) (BoolT) - (UnitT) (FuncT Type Type) (TupleT TypeList) ) @@ -38,7 +37,7 @@ :ruleset type-analysis) (rule ((UnitExpr id)) - ((HasType (UnitExpr id) (UnitT))) + ((HasType (UnitExpr id) (TupleT (TNil)))) :ruleset type-analysis) ; Pure Op Compute @@ -113,7 +112,7 @@ ; Effectful Ops (rule ((Print e)) - ((HasType (Print e) (UnitT))) + ((HasType (Print e) (TupleT (TNil)))) :ruleset type-analysis) ; TODO: Read and Write (requires type annotations) diff --git a/tree_unique_args/src/type_analysis.rs b/tree_unique_args/src/type_analysis.rs index 982425038..d0c221dae 100644 --- a/tree_unique_args/src/type_analysis.rs +++ b/tree_unique_args/src/type_analysis.rs @@ -64,7 +64,7 @@ fn switch_int() -> Result<(), egglog::Error> { (check (HasType s1 (IntT))) (check (HasType s2 (BoolT))) - (check (HasType s3 (UnitT))) + (check (HasType s3 (TupleT (TNil)))) "; crate::run_test(build, check) } From ee656407ef342b926107d4ba28a3a80e78413330 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Fri, 26 Jan 2024 15:05:51 -0800 Subject: [PATCH 4/4] All instead of unit --- tree_unique_args/src/ast.rs | 12 +++---- tree_unique_args/src/body_contains.rs | 2 +- tree_unique_args/src/deep_copy.rs | 12 +++---- tree_unique_args/src/disallow_empty_all.egg | 3 -- tree_unique_args/src/disallow_empty_all.rs | 7 ---- tree_unique_args/src/id_analysis.rs | 13 ++++---- tree_unique_args/src/interpreter.rs | 23 ++++++++----- tree_unique_args/src/ir.rs | 10 +++--- tree_unique_args/src/is_valid.rs | 6 ++-- tree_unique_args/src/ivt.egg | 6 ++-- tree_unique_args/src/ivt.rs | 4 +-- tree_unique_args/src/lib.rs | 9 ++---- tree_unique_args/src/purity_analysis.rs | 36 ++++++++++----------- tree_unique_args/src/schema.egg | 2 +- tree_unique_args/src/subst.rs | 12 +++---- tree_unique_args/src/sugar.egg | 6 ++-- tree_unique_args/src/switch_rewrites.rs | 14 ++++---- tree_unique_args/src/type_analysis.egg | 18 ++++------- tree_unique_args/src/type_analysis.rs | 21 ++++++------ tree_unique_args/src/util.egg | 2 +- tree_unique_args/src/util.rs | 10 +++--- 21 files changed, 108 insertions(+), 120 deletions(-) delete mode 100644 tree_unique_args/src/disallow_empty_all.egg delete mode 100644 tree_unique_args/src/disallow_empty_all.rs diff --git a/tree_unique_args/src/ast.rs b/tree_unique_args/src/ast.rs index def00792d..662e04ada 100644 --- a/tree_unique_args/src/ast.rs +++ b/tree_unique_args/src/ast.rs @@ -55,10 +55,6 @@ pub fn tfalse() -> Expr { Boolean(false) } -pub fn unit() -> Expr { - Unit -} - pub fn add(a: Expr, b: Expr) -> Expr { Add(Box::new(a), Box::new(b)) } @@ -99,12 +95,12 @@ pub fn print(a: Expr) -> Expr { Print(Box::new(a)) } -pub fn sequence(args: Vec) -> Expr { - All(Order::Sequential, args) +pub fn sequence(id: Id, args: Vec) -> Expr { + All(id, Order::Sequential, args) } -pub fn parallel(args: Vec) -> Expr { - All(Order::Parallel, args) +pub fn parallel(id: Id, args: Vec) -> Expr { + All(id, Order::Parallel, args) } pub fn switch(arg: Expr, cases: Vec) -> Expr { diff --git a/tree_unique_args/src/body_contains.rs b/tree_unique_args/src/body_contains.rs index a59e6ac3a..de5a3dc8a 100644 --- a/tree_unique_args/src/body_contains.rs +++ b/tree_unique_args/src/body_contains.rs @@ -66,7 +66,7 @@ fn test_body_contains() -> Result<(), egglog::Error> { (let loop (Loop id1 (Num id-outer 1) - (All (Sequential) (Pair + (All id1 (Sequential) (Pair ; pred (LessThan (Num id1 2) (Num id1 3)) ; output diff --git a/tree_unique_args/src/deep_copy.rs b/tree_unique_args/src/deep_copy.rs index 41296cca7..0258cfa7f 100644 --- a/tree_unique_args/src/deep_copy.rs +++ b/tree_unique_args/src/deep_copy.rs @@ -60,13 +60,13 @@ fn test_deep_copy() -> Result<(), egglog::Error> { (let id-outer (Id (i64-fresh!))) (let loop (Loop id1 - (All (Parallel) (Pair (Arg id-outer) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Arg id-outer) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output (Let id2 - (All (Parallel) (Pair + (All id1 (Parallel) (Pair (Add (Get (Arg id1) 0) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))) (Arg id2)))))) @@ -75,13 +75,13 @@ fn test_deep_copy() -> Result<(), egglog::Error> { let check = " (let loop-copied-expected (Loop (Id 4) - (All (Parallel) (Pair (Arg (Id 3)) (Num (Id 3) 0))) - (All (Sequential) (Pair + (All (Id 3) (Parallel) (Pair (Arg (Id 3)) (Num (Id 3) 0))) + (All (Id 4) (Sequential) (Pair ; pred (LessThan (Get (Arg (Id 4)) 0) (Get (Arg (Id 4)) 1)) ; output (Let (Id 5) - (All (Parallel) (Pair + (All (Id 4) (Parallel) (Pair (Add (Get (Arg (Id 4)) 0) (Num (Id 4) 1)) (Sub (Get (Arg (Id 4)) 1) (Num (Id 4) 1)))) (Arg (Id 5))))))) diff --git a/tree_unique_args/src/disallow_empty_all.egg b/tree_unique_args/src/disallow_empty_all.egg deleted file mode 100644 index 0ef2cdc9c..000000000 --- a/tree_unique_args/src/disallow_empty_all.egg +++ /dev/null @@ -1,3 +0,0 @@ -(rule ((ExprIsValid (All order (Nil)))) - ((panic "UnitExpr should be used instead of an empty All")) - :ruleset error-checking) diff --git a/tree_unique_args/src/disallow_empty_all.rs b/tree_unique_args/src/disallow_empty_all.rs deleted file mode 100644 index 0aebd0014..000000000 --- a/tree_unique_args/src/disallow_empty_all.rs +++ /dev/null @@ -1,7 +0,0 @@ -#[test] -#[should_panic] -fn empty_all_should_panic() { - let build = "(ExprIsValid (All (Parallel) (Nil)))"; - let check = ""; - let _ = crate::run_test(build, check); -} diff --git a/tree_unique_args/src/id_analysis.rs b/tree_unique_args/src/id_analysis.rs index 9c7275b00..3d840778f 100644 --- a/tree_unique_args/src/id_analysis.rs +++ b/tree_unique_args/src/id_analysis.rs @@ -54,21 +54,21 @@ fn test_id_analysis() -> Result<(), egglog::Error> { (ExprIsValid (Let let0-id (Num outer-id 0) - (All + (All let0-id (Parallel) (Pair (Let let1-id (Num let0-id 3) (Boolean let1-id true)) - (UnitExpr let0-id) + (All let0-id (Parallel) (Nil)) )))) "; let check = " (check (ExprHasRefId (Num outer-id 0) outer-id)) (check (ExprHasRefId (Boolean let1-id true) let1-id)) - (check (ExprHasRefId (UnitExpr let0-id) let0-id)) + (check (ExprHasRefId (All let0-id (Parallel) (Nil)) let0-id)) (check (ExprHasRefId (Let let1-id @@ -81,7 +81,7 @@ fn test_id_analysis() -> Result<(), egglog::Error> { let1-id (Num let0-id 3) (Boolean let1-id true)) - (UnitExpr let0-id) + (All let0-id (Parallel) (Nil)) ) let0-id )) @@ -90,13 +90,14 @@ fn test_id_analysis() -> Result<(), egglog::Error> { let0-id (Num outer-id 0) (All + let0-id (Parallel) (Pair (Let let1-id (Num let0-id 3) (Boolean let1-id true)) - (UnitExpr let0-id) + (All let0-id (Parallel) (Nil)) ))) outer-id )) @@ -135,7 +136,7 @@ fn test_id_analysis_listexpr_id_conflict_panics() { let build = " (let id1 (Id (i64-fresh!))) (let id2 (Id (i64-fresh!))) - (let conflict-expr (Cons (Num id1 3) (Cons (UnitExpr id2) (Nil)))) + (let conflict-expr (Cons (Num id1 3) (Cons (All id2 (Parallel) (Nil)) (Nil)))) (ListExprIsValid conflict-expr)"; let check = ""; diff --git a/tree_unique_args/src/interpreter.rs b/tree_unique_args/src/interpreter.rs index 76ee86f7a..b85b0329d 100644 --- a/tree_unique_args/src/interpreter.rs +++ b/tree_unique_args/src/interpreter.rs @@ -21,7 +21,6 @@ pub fn typecheck(e: &Expr, arg_ty: &Option) -> Result { Expr::Program(_) => panic!("Found non top level program."), Expr::Num(_) => Ok(Type::Num), Expr::Boolean(_) => Ok(Type::Boolean), - Expr::Unit => Ok(Type::Tuple(vec![])), Expr::Add(e1, e2) | Expr::Sub(e1, e2) | Expr::Mul(e1, e2) => { expect_type(e1, Type::Num)?; expect_type(e2, Type::Num)?; @@ -85,7 +84,7 @@ pub fn typecheck(e: &Expr, arg_ty: &Option) -> Result { expect_type(data, Type::Num)?; Ok(Type::Tuple(vec![])) } - Expr::All(_, exprs) => { + Expr::All(_, _, exprs) => { let tys = exprs .iter() .map(|expr| typecheck(expr, arg_ty)) @@ -138,7 +137,6 @@ pub fn interpret(e: &Expr, arg: &Option, vm: &mut VirtualMachine) -> Valu Expr::Program(_) => todo!("interpret programs"), Expr::Num(x) => Value::Num(*x), Expr::Boolean(x) => Value::Boolean(*x), - Expr::Unit => Value::Tuple(vec![]), Expr::Add(e1, e2) => { let Value::Num(n1) = interpret(e1, arg, vm) else { panic!("add") @@ -235,7 +233,7 @@ pub fn interpret(e: &Expr, arg: &Option, vm: &mut VirtualMachine) -> Valu vm.mem.insert(addr as usize, data); Value::Tuple(vec![]) } - Expr::All(_, exprs) => { + Expr::All(_, _, exprs) => { // this always executes sequentially (which is a valid way to // execute parallel tuples) let vals = exprs @@ -285,6 +283,7 @@ fn test_interpreter() { Id(0), Box::new(Expr::Num(1)), Box::new(Expr::All( + Id(0), Order::Parallel, vec![ // pred: i < 10 @@ -292,6 +291,7 @@ fn test_interpreter() { // output Expr::Get( Box::new(Expr::All( + Id(0), Order::Parallel, vec![ // i = i + 1 @@ -319,6 +319,7 @@ fn test_interpreter_fib_using_memory() { let nth = 10; let fib_nth = 55; let e = Expr::All( + Id(-1), Order::Sequential, vec![ Expr::Write(Box::new(Expr::Num(0)), Box::new(Expr::Num(0))), @@ -327,6 +328,7 @@ fn test_interpreter_fib_using_memory() { Id(0), Box::new(Expr::Num(2)), Box::new(Expr::All( + Id(0), Order::Parallel, vec![ // pred: i < nth @@ -334,6 +336,7 @@ fn test_interpreter_fib_using_memory() { // output Expr::Get( Box::new(Expr::All( + Id(0), Order::Parallel, vec![ // i = i + 1 @@ -443,7 +446,6 @@ impl std::str::FromStr for Expr { ("Boolean", [_id, egglog::ast::Expr::Lit(egglog::ast::Literal::Bool(b))]) => { Ok(Expr::Boolean(*b)) } - ("UnitExpr", [_id]) => Ok(Expr::Unit), ("Add", [x, y]) => Ok(Expr::Add( Box::new(egglog_expr_to_expr(x)?), Box::new(egglog_expr_to_expr(y)?), @@ -482,7 +484,7 @@ impl std::str::FromStr for Expr { Box::new(egglog_expr_to_expr(x)?), Box::new(egglog_expr_to_expr(y)?), )), - ("All", [egglog::ast::Expr::Call(order, empty), xs]) => { + ("All", [id, egglog::ast::Expr::Call(order, empty), xs]) => { if !empty.is_empty() { return Err(ExprParseError::InvalidOrderArguments); } @@ -491,7 +493,11 @@ impl std::str::FromStr for Expr { "Sequential" => Ok(Order::Sequential), s => Err(ExprParseError::InvalidOrder(s.to_owned())), }?; - Ok(Expr::All(order, list_expr_to_vec(xs)?)) + Ok(Expr::All( + egglog_expr_to_id(id)?, + order, + list_expr_to_vec(xs)?, + )) } ("Switch", [pred, branches]) => Ok(Expr::Switch( Box::new(egglog_expr_to_expr(pred)?), @@ -533,7 +539,7 @@ fn test_expr_parser() { let s = "(Loop (Id 1) (Num (Id 0) 1) -(All (Sequential) +(All (Id 1) (Sequential) (Cons (LessThan (Num (Id 1) 2) (Num (Id 1) 3)) (Cons (Switch (Boolean (Id 1) true) (Cons (Num (Id 1) 4) (Cons (Num (Id 1) 5) (Nil)))) (Nil))))) @@ -543,6 +549,7 @@ fn test_expr_parser() { Id(1), Box::new(Expr::Num(1)), Box::new(Expr::All( + Id(1), Order::Sequential, vec![ Expr::LessThan(Box::new(Expr::Num(2)), Box::new(Expr::Num(3))), diff --git a/tree_unique_args/src/ir.rs b/tree_unique_args/src/ir.rs index 5e5c9e148..234c679dc 100644 --- a/tree_unique_args/src/ir.rs +++ b/tree_unique_args/src/ir.rs @@ -48,7 +48,6 @@ impl ESort { pub(crate) enum Constructor { Num, Boolean, - UnitExpr, Add, Sub, Mul, @@ -123,7 +122,6 @@ impl Constructor { match self { Constructor::Num => "Num", Constructor::Boolean => "Boolean", - Constructor::UnitExpr => "UnitExpr", Constructor::Add => "Add", Constructor::Sub => "Sub", Constructor::Mul => "Mul", @@ -152,7 +150,6 @@ impl Constructor { match self { Constructor::Num => vec![f(ReferencingId, "id"), f(Static(Sort::I64), "n")], Constructor::Boolean => vec![f(ReferencingId, "id"), f(Static(Sort::Bool), "b")], - Constructor::UnitExpr => vec![f(ReferencingId, "id")], Constructor::Add => vec![f(SubExpr, "x"), f(SubExpr, "y")], Constructor::Sub => vec![f(SubExpr, "x"), f(SubExpr, "y")], Constructor::Mul => vec![f(SubExpr, "x"), f(SubExpr, "y")], @@ -166,7 +163,11 @@ impl Constructor { Constructor::Print => vec![f(SubExpr, "printee")], Constructor::Read => vec![f(SubExpr, "addr")], Constructor::Write => vec![f(SubExpr, "addr"), f(SubExpr, "data")], - Constructor::All => vec![f(Static(Sort::Order), "order"), f(SubListExpr, "exprs")], + Constructor::All => vec![ + f(ReferencingId, "id"), + f(Static(Sort::Order), "order"), + f(SubListExpr, "exprs"), + ], Constructor::Switch => vec![f(SubExpr, "pred"), f(SubListExpr, "branches")], Constructor::Loop => vec![ f(CapturingId, "id"), @@ -209,7 +210,6 @@ impl Constructor { match self { Constructor::Num => ESort::Expr, Constructor::Boolean => ESort::Expr, - Constructor::UnitExpr => ESort::Expr, Constructor::Add => ESort::Expr, Constructor::Sub => ESort::Expr, Constructor::Mul => ESort::Expr, diff --git a/tree_unique_args/src/is_valid.rs b/tree_unique_args/src/is_valid.rs index 66e0e4d16..832ceeda9 100644 --- a/tree_unique_args/src/is_valid.rs +++ b/tree_unique_args/src/is_valid.rs @@ -36,12 +36,12 @@ fn test_is_valid() -> Result<(), egglog::Error> { (let id-outer (Id (i64-fresh!))) (let loop (Loop id1 - (All (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output - (All (Parallel) (Pair + (All id1 (Parallel) (Pair (Add (Get (Arg id1) 0) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))))))) (ExprIsValid loop) diff --git a/tree_unique_args/src/ivt.egg b/tree_unique_args/src/ivt.egg index b8fe2d171..bbd077393 100644 --- a/tree_unique_args/src/ivt.egg +++ b/tree_unique_args/src/ivt.egg @@ -29,7 +29,7 @@ (rule ((= loop (Loop id in out)) (ExprHasRefId loop outer-id) (ExprIsValid loop) - (= out (All ord (Cons pred (Cons switch (Nil))))) + (= out (All id ord (Cons pred (Cons switch (Nil))))) (= switch (Switch pred branches)) (ExprIsPure pred)) ((LiftSwitch switch in outer-id)) :ruleset ivt) @@ -37,13 +37,13 @@ ; Apply the rule (rule ((= loop (Loop id in out)) (ExprIsValid loop) - (= out (All ord (Cons pred (Cons switch (Nil))))) + (= out (All id ord (Cons pred (Cons switch (Nil))))) (= switch (Switch pred (Cons thn* (Cons els* (Nil))))) ; NB: we don't constrain 'outer-id' here in part because there can only ; be _one_ outer-id that is referenced by it. (See the panic in the rules ; for *HasRefId). (= (Switch pred_ (Cons thn (Cons els (Nil)))) (LiftSwitch switch in outer-id))) ((let new-id (Id (i64-fresh!))) - (let inner (NewLoop new-id in (All ord (Pair pred thn*)))) + (let inner (NewLoop new-id in (All new-id ord (Pair pred thn*)))) (let outer (Switch pred_ (Cons inner (Cons els (Nil))))) (union loop outer)) :ruleset ivt) \ No newline at end of file diff --git a/tree_unique_args/src/ivt.rs b/tree_unique_args/src/ivt.rs index 384c917f5..e47ba7e3d 100644 --- a/tree_unique_args/src/ivt.rs +++ b/tree_unique_args/src/ivt.rs @@ -28,7 +28,7 @@ fn basic_ivt() -> Result { (let switch (Switch pred (Pair (Print (Num loop-id 0)) (Print (Num loop-id 1))))) - (let loop (Loop loop-id (Arg outer-id) (All (Sequential) (Pair pred switch)))) + (let loop (Loop loop-id (Arg outer-id) (All loop-id (Sequential) (Pair pred switch)))) (ExprIsValid loop)"; let check = " (check (= loop @@ -36,7 +36,7 @@ fn basic_ivt() -> Result { (LessThan (Arg outer-id) (Num outer-id 1)) (Cons (Loop new-id (Arg outer-id) - (All (Sequential) + (All new-id (Sequential) (Cons (LessThan (Arg new-id) (Num new-id 1)) (Cons (Print (Num new-id 0)) (Nil))))) (Cons (Print (Num outer-id 1)) (Nil))))))"; diff --git a/tree_unique_args/src/lib.rs b/tree_unique_args/src/lib.rs index a66431b9c..696d2220a 100644 --- a/tree_unique_args/src/lib.rs +++ b/tree_unique_args/src/lib.rs @@ -2,7 +2,6 @@ pub mod ast; pub(crate) mod body_contains; pub(crate) mod conditional_invariant_code_motion; pub(crate) mod deep_copy; -pub(crate) mod disallow_empty_all; pub(crate) mod function_inlining; pub(crate) mod id_analysis; pub mod interpreter; @@ -31,7 +30,6 @@ pub struct Id(i64); pub enum Expr { Num(i64), Boolean(bool), - Unit, Add(Box, Box), Sub(Box, Box), Mul(Box, Box), @@ -48,7 +46,7 @@ pub enum Expr { Print(Box), Read(Box), Write(Box, Box), - All(Order, Vec), + All(Id, Order, Vec), Switch(Box, Vec), Loop(Id, Box, Box), Let(Id, Box, Box), @@ -64,7 +62,7 @@ impl Expr { /// Runs `func` on every child of this expression. pub fn for_each_child(&mut self, mut func: impl FnMut(&mut Expr)) { match self { - Expr::Num(_) | Expr::Boolean(_) | Expr::Unit | Expr::Arg(_) => {} + Expr::Num(_) | Expr::Boolean(_) | Expr::Arg(_) => {} Expr::Add(a, b) | Expr::Sub(a, b) | Expr::Mul(a, b) @@ -82,7 +80,7 @@ impl Expr { Expr::Get(a, _) | Expr::Function(_, a) | Expr::Call(_, a) => { func(a); } - Expr::All(_, children) => { + Expr::All(_, _, children) => { for child in children { func(child); } @@ -141,7 +139,6 @@ pub fn run_test(build: &str, check: &str) -> Result { include_str!("sugar.egg"), &util::rules().join("\n"), &id_analysis::id_analysis_rules().join("\n"), - include_str!("disallow_empty_all.egg"), // optimizations include_str!("simple.egg"), include_str!("function_inlining.egg"), diff --git a/tree_unique_args/src/purity_analysis.rs b/tree_unique_args/src/purity_analysis.rs index 8a864b03f..44ae9b2fd 100644 --- a/tree_unique_args/src/purity_analysis.rs +++ b/tree_unique_args/src/purity_analysis.rs @@ -6,8 +6,8 @@ use strum::IntoEnumIterator; fn is_pure(ctor: &Constructor) -> bool { use Constructor::*; match ctor { - Num | Boolean | UnitExpr | Add | Sub | Mul | LessThan | And | Or | Not | Get | All - | Switch | Loop | Let | Arg | Call | Cons | Nil => true, + Num | Boolean | Add | Sub | Mul | LessThan | And | Or | Not | Get | All | Switch | Loop + | Let | Arg | Call | Cons | Nil => true, Print | Read | Write => false, } } @@ -67,26 +67,26 @@ fn test_purity_analysis() -> Result<(), egglog::Error> { (let id-outer (Id (i64-fresh!))) (let pure-loop (Loop id1 - (All (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output - (All (Parallel) (Pair + (All id1 (Parallel) (Pair (Add (Get (Arg id1) 0) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))))))) (let id2 (Id (i64-fresh!))) (let impure-loop (Loop id2 - (All (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) + (All id2 (Sequential) (Pair ; pred (LessThan (Get (Arg id2) 0) (Get (Arg id2) 1)) ; output - (IgnoreFirst + (IgnoreFirst id2 (Print (Num id2 1)) - (All (Parallel) (Pair + (All id2 (Parallel) (Pair (Add (Get (Arg id2) 0) (Num id2 1)) (Sub (Get (Arg id2) 1) (Num id2 1))))))))) " @@ -117,7 +117,7 @@ fn test_purity_function() -> Result<(), egglog::Error> { (let f2 (Function id_fun2 (Get - (All (Sequential) + (All id_fun2 (Sequential) (Pair (Print (Get (Arg id_fun2) 0)) (Add @@ -126,25 +126,25 @@ fn test_purity_function() -> Result<(), egglog::Error> { 1))) (let pure-loop (Loop id1 - (All (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output - (All (Parallel) + (All id1 (Parallel) (Pair - (Add (Call id_fun1 (All (Sequential) (Cons (Get (Arg id1) 0) (Nil)))) (Num id1 1)) + (Add (Call id_fun1 (All id1 (Sequential) (Cons (Get (Arg id1) 0) (Nil)))) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))))))) (let impure-loop (Loop id2 - (All (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 0) (Num id-outer 0))) + (All id2 (Sequential) (Pair ; pred (LessThan (Get (Arg id2) 0) (Get (Arg id2) 1)) ; output - (All (Parallel) + (All id2 (Parallel) (Pair - (Add (Call id_fun2 (All (Sequential) (Cons (Get (Arg id2) 0) (Nil)))) (Num id2 1)) + (Add (Call id_fun2 (All id2 (Sequential) (Cons (Get (Arg id2) 0) (Nil)))) (Num id2 1)) (Sub (Get (Arg id2) 1) (Num id2 1)))))))) " .to_string(); diff --git a/tree_unique_args/src/schema.egg b/tree_unique_args/src/schema.egg index c0f553385..a22698660 100644 --- a/tree_unique_args/src/schema.egg +++ b/tree_unique_args/src/schema.egg @@ -41,7 +41,7 @@ (datatype Order (Parallel) (Sequential)) ; Perform a list of operations. Only way to create a tuple! -(function All (Order ListExpr) Expr) +(function All (IdSort Order ListExpr) Expr) ; Switch on a list of lazily-evaluated branches. Doesn't create context ; pred branches chosen diff --git a/tree_unique_args/src/subst.rs b/tree_unique_args/src/subst.rs index 0a1916224..ffccb7bda 100644 --- a/tree_unique_args/src/subst.rs +++ b/tree_unique_args/src/subst.rs @@ -52,12 +52,12 @@ fn test_subst() -> Result<(), egglog::Error> { (let id-outer (Id (i64-fresh!))) (let loop1 (Loop id1 - (All (Parallel) (Pair (Arg id-outer) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Arg id-outer) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output - (All (Parallel) (Pair + (All id1 (Parallel) (Pair (Add (Get (Arg id1) 0) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))))))) (let loop1-substed (SubstExpr loop1 (Num id-outer 7))) @@ -66,12 +66,12 @@ fn test_subst() -> Result<(), egglog::Error> { let check = " (let loop1-substed-expected (Loop id1 - (All (Parallel) (Pair (Num id-outer 7) (Num id-outer 0))) - (All (Sequential) (Pair + (All id-outer (Parallel) (Pair (Num id-outer 7) (Num id-outer 0))) + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 1)) ; output - (All (Parallel) (Pair + (All id1 (Parallel) (Pair (Add (Get (Arg id1) 0) (Num id1 1)) (Sub (Get (Arg id1) 1) (Num id1 1)))))))) (run-schedule (saturate always-run)) diff --git a/tree_unique_args/src/sugar.egg b/tree_unique_args/src/sugar.egg index eda9206bf..4b7321631 100644 --- a/tree_unique_args/src/sugar.egg +++ b/tree_unique_args/src/sugar.egg @@ -16,10 +16,10 @@ (rewrite (list5 a b c d e) (Cons a (Cons b (Cons c (Cons d (Cons e (Nil)))))) :ruleset always-run) -(function IgnoreFirst (Expr Expr) Expr) -(rewrite (IgnoreFirst a b) +(function IgnoreFirst (IdSort Expr Expr) Expr) +(rewrite (IgnoreFirst id a b) (Get - (All (Sequential) (Cons a (Cons b (Nil)))) + (All id (Sequential) (Cons a (Cons b (Nil)))) 1) :ruleset always-run) diff --git a/tree_unique_args/src/switch_rewrites.rs b/tree_unique_args/src/switch_rewrites.rs index e3c9e45ea..c416ce594 100644 --- a/tree_unique_args/src/switch_rewrites.rs +++ b/tree_unique_args/src/switch_rewrites.rs @@ -33,8 +33,8 @@ pub(crate) fn rules() -> String { :ruleset switch-rewrites) ; (if E then S1 else S2); S3 ==> if E then S1;S3 else S2;S3 - (rewrite (All ord (Cons (Switch e (Cons S1 (Cons S2 (Nil)))) S3)) - (Switch e (Cons (All ord (Cons S1 S3)) (Cons (All ord (Cons S2 S3)) (Nil)))) + (rewrite (All id ord (Cons (Switch e (Cons S1 (Cons S2 (Nil)))) S3)) + (Switch e (Cons (All id ord (Cons S1 S3)) (Cons (All id ord (Cons S2 S3)) (Nil)))) :ruleset switch-rewrites) {rules_needing_purity}" @@ -80,7 +80,7 @@ fn switch_rewrite_purity() -> crate::Result { let build = " (let switch-id (Id (i64-fresh!))) (let let-id (Id (i64-fresh!))) -(let impure (Let let-id (UnitExpr switch-id) (All (Sequential) (Pair (Boolean let-id true) (Print (Num let-id 1)))))) +(let impure (Let let-id (All switch-id (Parallel) (Nil)) (All let-id (Sequential) (Pair (Boolean let-id true) (Print (Num let-id 1)))))) (let switch (Switch (And (Boolean switch-id false) (Get impure 0)) (Pair (Num switch-id 1) (Num switch-id 2)))) (ExprIsValid switch) @@ -96,7 +96,7 @@ fn switch_rewrite_purity() -> crate::Result { let build = " (let switch-id (Id (i64-fresh!))) (let let-id (Id (i64-fresh!))) -(let impure (Let let-id (UnitExpr switch-id) (All (Sequential) (Cons (Boolean let-id true) (Nil))))) +(let impure (Let let-id (All switch-id (Parallel) (Nil)) (All let-id (Sequential) (Cons (Boolean let-id true) (Nil))))) (let switch (Switch (And (Boolean switch-id false) (Get impure 0)) (Pair (Num switch-id 1) (Num switch-id 2)))) (ExprIsValid switch) @@ -140,11 +140,11 @@ fn switch_pull_in_below() -> Result<(), egglog::Error> { (let s3 (Read (Num id 6))) (let switch (Switch c (Cons s1 (Cons s2 (Nil))))) - (let lhs (All (Sequential) (Cons switch (Cons s3 (Nil))))) + (let lhs (All id (Sequential) (Cons switch (Cons s3 (Nil))))) "; let check = " - (let s1s3 (All (Sequential) (Cons s1 (Cons s3 (Nil))))) - (let s2s3 (All (Sequential) (Cons s2 (Cons s3 (Nil))))) + (let s1s3 (All id (Sequential) (Cons s1 (Cons s3 (Nil))))) + (let s2s3 (All id (Sequential) (Cons s2 (Cons s3 (Nil))))) (let expected (Switch c (Cons s1s3 (Cons s2s3 (Nil))))) (check (= lhs expected)) "; diff --git a/tree_unique_args/src/type_analysis.egg b/tree_unique_args/src/type_analysis.egg index 249be7c88..caed2d306 100644 --- a/tree_unique_args/src/type_analysis.egg +++ b/tree_unique_args/src/type_analysis.egg @@ -36,10 +36,6 @@ ((HasType (Boolean id b) (BoolT))) :ruleset type-analysis) -(rule ((UnitExpr id)) - ((HasType (UnitExpr id) (TupleT (TNil)))) - :ruleset type-analysis) - ; Pure Op Compute (rule ( (Add x y) @@ -155,20 +151,20 @@ :ruleset type-analysis) ; Sequencing -(rule ((All ord (Cons hd tl))) - ((All ord tl)) ; peel off a layer for type checking +(rule ((All id ord (Cons hd tl))) + ((All id ord tl)) ; peel off a layer for type checking :ruleset type-analysis) ; base case: Nil -(rule ((All ord (Nil))) - ((HasType (All ord (Nil)) (TupleT (TNil)))) +(rule ((All id ord (Nil))) + ((HasType (All id ord (Nil)) (TupleT (TNil)))) :ruleset type-analysis) ; rec case (rule ( - (All ord (Cons hd tl)) + (All id ord (Cons hd tl)) (HasType hd ty) - (HasType (All ord tl) (TupleT tylist)) + (HasType (All id ord tl) (TupleT tylist)) ) - ((HasType (All ord (Cons hd tl)) (TupleT (TCons ty tylist)))) + ((HasType (All id ord (Cons hd tl)) (TupleT (TCons ty tylist)))) :ruleset type-analysis) ; If an expr has two different types, panic diff --git a/tree_unique_args/src/type_analysis.rs b/tree_unique_args/src/type_analysis.rs index d0c221dae..2b950998a 100644 --- a/tree_unique_args/src/type_analysis.rs +++ b/tree_unique_args/src/type_analysis.rs @@ -72,17 +72,18 @@ fn switch_int() -> Result<(), egglog::Error> { #[test] fn tuple() -> Result<(), egglog::Error> { let build = " - (let n (Add (Num (Id (i64-fresh!)) 1) (Num (Id (i64-fresh!)) 2))) + (let id (Id (i64-fresh!))) + (let n (Add (Num id 1) (Num id 2))) (let m (Mul n n)) (let s (Sub n m)) (let x (LessThan m n)) (let y (Not x)) (let z (And x (Or y y))) - (let tup1 (All (Sequential) (Nil))) - (let tup2 (All (Sequential) (Cons z (Nil)))) - (let tup3 (All (Parallel) (Cons x (Cons m (Nil))))) - (let tup4 (All (Parallel) (Cons tup2 (Cons tup3 (Nil))))) + (let tup1 (All id (Sequential) (Nil))) + (let tup2 (All id (Sequential) (Cons z (Nil)))) + (let tup3 (All id (Parallel) (Cons x (Cons m (Nil))))) + (let tup4 (All id (Parallel) (Cons tup2 (Cons tup3 (Nil))))) (let get1 (Get tup3 0)) (let get2 (Get tup3 1)) @@ -117,7 +118,7 @@ fn lets() -> Result<(), egglog::Error> { (let ctx (Id (i64-fresh!))) (let nested (Let outer (Num ctx 3) - (Let inner (All (Parallel) (Cons (Arg outer) (Cons (Num outer 2) (Nil)))) + (Let inner (All ctx (Parallel) (Cons (Arg outer) (Cons (Num outer 2) (Nil)))) (Add (Get (Arg inner) 0) (Get (Arg inner) 1))))) "; let check = " @@ -134,7 +135,7 @@ fn loops() -> Result<(), egglog::Error> { (let ctx (Id 0)) (let loop-id (Id 1)) (let l (Loop loop-id (Num ctx 1) - (All (Sequential) + (All loop-id (Sequential) (Cons (LessThan (Num loop-id 2) (Num loop-id 3)) (Cons (Switch (Boolean loop-id true) (Cons (Num loop-id 4) (Cons (Num loop-id 5) (Nil)))) @@ -154,7 +155,7 @@ fn loop_pred_boolean() { (let ctx (Id 0)) (let loop-id (Id 1)) (let l (Loop loop-id (Num ctx 1) - (All (Sequential) + (All loop-id (Sequential) (Cons (Add (Num loop-id 2) (Num loop-id 3)) (Cons (Switch (Boolean loop-id true) (Cons (Num loop-id 4) (Cons (Num loop-id 5) (Nil)))) @@ -171,7 +172,7 @@ fn loop_args1() { let build = " (let ctx (Id 0)) (let loop-id (Id 1)) - (let l (Loop loop-id (Num ctx 1) (All (Sequential) (Nil)))) + (let l (Loop loop-id (Num ctx 1) (All loop-id (Sequential) (Nil)))) (run-schedule (saturate type-analysis))"; let check = ""; @@ -185,7 +186,7 @@ fn loop_args3() { (let ctx (Id 0)) (let loop-id (Id 1)) (let l (Loop loop-id (Num ctx 1) - (All (Sequential) + (All loop-id (Sequential) (Cons (LessThan (Num loop-id 2) (Num loop-id 3)) (Cons (Switch (Boolean loop-id true) (Cons (Num loop-id 4) (Cons (Num loop-id 5) (Nil)))) diff --git a/tree_unique_args/src/util.egg b/tree_unique_args/src/util.egg index e9f802c29..e5c9e58ca 100644 --- a/tree_unique_args/src/util.egg +++ b/tree_unique_args/src/util.egg @@ -3,7 +3,7 @@ (function ListExpr-suffix (ListExpr i64) ListExpr :unextractable) (function Append (ListExpr Expr) ListExpr :unextractable) -(rule ((All order top)) ((union (ListExpr-suffix top 0) top)) :ruleset always-run) +(rule ((All id order top)) ((union (ListExpr-suffix top 0) top)) :ruleset always-run) (rule ((= (ListExpr-suffix top n) (Cons hd tl))) ((union (ListExpr-ith top n) hd) diff --git a/tree_unique_args/src/util.rs b/tree_unique_args/src/util.rs index a8df7d90e..534bd41a5 100644 --- a/tree_unique_args/src/util.rs +++ b/tree_unique_args/src/util.rs @@ -11,7 +11,7 @@ fn ast_size_for_ctor(ctor: Constructor) -> String { Constructor::Cons => format!("(rule ((= list (Cons expr xs)) (= a (Expr-size expr)) (= b (ListExpr-size xs))) ((set (ListExpr-size list) (+ a b))){ruleset})"), // let Get and All's size = children's size (I prefer not +1 here) Constructor::Get => format!("(rule ((= expr (Get tup i)) (= n (Expr-size tup))) ((set (Expr-size expr) n)) {ruleset})"), - Constructor::All => format!("(rule ((= expr (All ord list)) (= n (ListExpr-size list))) ((set (Expr-size expr) n)) {ruleset})"), + Constructor::All => format!("(rule ((= expr (All id ord list)) (= n (ListExpr-size list))) ((set (Expr-size expr) n)) {ruleset})"), _ => { let field_pattern = ctor.filter_map_fields(|field| { let sort = field.sort().name(); @@ -50,7 +50,7 @@ fn test_list_util() -> Result<(), egglog::Error> { let build = &*" (let id (Id 1)) (let list (Cons (Num id 0) (Cons (Num id 1) (Cons (Num id 2) (Cons (Num id 3) (Cons (Num id 4) (Nil))))))) - (let t (All (Sequential) list)) + (let t (All id (Sequential) list)) ".to_string(); let check = &*" (check (= (ListExpr-ith list 1) (Num id 1))) @@ -101,16 +101,16 @@ fn ast_size_test() -> Result<(), egglog::Error> { (let loop (Loop id1 - (All (Parallel) (list5 (Num id-outer 0) + (All id-outer (Parallel) (list5 (Num id-outer 0) (Num id-outer 1) (Num id-outer 2) (Num id-outer 3) (Num id-outer 4))) - (All (Sequential) (Pair + (All id1 (Sequential) (Pair ; pred (LessThan (Get (Arg id1) 0) (Get (Arg id1) 4)) ; output - (All (Parallel) + (All id1 (Parallel) (list5 (Add (Get (Arg id1) 0) inv