Draft: more fix for seminaive

src/ast/desugar.rs

@@ -146,7 +146,7 @@ fn flatten_actions(actions: &Vec<Action>, desugar: &mut Desugar) -> Vec<NormActi
                 assert_ne!(*symbol, added);
                 res.push(NormAction::LetVar(*symbol, added));
             }
-            Action::Set(symbol, exprs, rhs) | Action::SetNoTrack(symbol, exprs, rhs) => {
+            Action::Set(symbol, exprs, rhs) => {
                 let set = NormAction::Set(
                     NormExpr::Call(
                         *symbol,
@@ -274,7 +274,7 @@ fn desugar_run_config(desugar: &mut Desugar, run_config: &RunConfig) -> NormRunC
 
 fn add_semi_naive_rule(desugar: &mut Desugar, rule: Rule) -> Option<Rule> {
     let mut new_rule = rule;
-    // only add new rule when there is Call in body to avoid adding same rule.
+    // only add new rule when there is Call or Let in body to avoid adding same rule.
     let mut add_new_rule = false;
 
     for head_slice in new_rule.head.iter_mut() {
@@ -294,7 +294,9 @@ fn add_semi_naive_rule(desugar: &mut Desugar, rule: Rule) -> Option<Rule> {
             }
 
             // move let binding to body.
+            // TODO: maybe it could be optimized by having liveness analysis instead of adding all Let action to head.
             Action::Let(symbol, expr) => {
+                add_new_rule = true;
                 let eq_vec: Vec<Expr> = vec![Expr::Var(*symbol), expr.clone()];
                 new_rule.body.push(Fact::Eq(eq_vec));
             }

src/ast/mod.rs

@@ -680,7 +680,6 @@ impl Display for Fact {
 pub enum Action {
     Let(Symbol, Expr),
     Set(Symbol, Vec<Expr>, Expr),
-    SetNoTrack(Symbol, Vec<Expr>, Expr),
     Delete(Symbol, Vec<Expr>),
     Union(Expr, Expr),
     Panic(String),
@@ -705,7 +704,7 @@ impl NormAction {
             NormAction::Let(symbol, expr) => Action::Let(*symbol, expr.to_expr()),
             NormAction::LetVar(symbol, other) => Action::Let(*symbol, Expr::Var(*other)),
             NormAction::LetLit(symbol, lit) => Action::Let(*symbol, Expr::Lit(lit.clone())),
-            NormAction::Set(NormExpr::Call(head, body), other) => Action::SetNoTrack(
+            NormAction::Set(NormExpr::Call(head, body), other) => Action::Set(
                 *head,
                 body.iter().map(|s| Expr::Var(*s)).collect(),
                 Expr::Var(*other),
@@ -755,9 +754,6 @@ impl ToSexp for Action {
         match self {
             Action::Let(lhs, rhs) => list!("let", lhs, rhs),
             Action::Set(lhs, args, rhs) => list!("set", list!(lhs, ++ args), rhs),
-            Action::SetNoTrack(lhs, args, rhs) => {
-                list!("set-no-track", list!(lhs, ++ args), rhs)
-            }
             Action::Union(lhs, rhs) => list!("union", lhs, rhs),
             Action::Delete(lhs, args) => list!("delete", list!(lhs, ++ args)),
             Action::Panic(msg) => list!("panic", format!("\"{}\"", msg.clone())),
@@ -774,10 +770,6 @@ impl Action {
                 let right = f(rhs);
                 Action::Set(*lhs, args.iter().map(f).collect(), right)
             }
-            Action::SetNoTrack(lhs, args, rhs) => {
-                let right = f(rhs);
-                Action::SetNoTrack(*lhs, args.iter().map(f).collect(), right)
-            }
             Action::Delete(lhs, args) => Action::Delete(*lhs, args.iter().map(f).collect()),
             Action::Union(lhs, rhs) => Action::Union(f(lhs), f(rhs)),
             Action::Panic(msg) => Action::Panic(msg.clone()),
@@ -793,11 +785,6 @@ impl Action {
                 args.iter().map(|e| e.replace_canon(canon)).collect(),
                 rhs.replace_canon(canon),
             ),
-            Action::SetNoTrack(lhs, args, rhs) => Action::SetNoTrack(
-                *lhs,
-                args.iter().map(|e| e.replace_canon(canon)).collect(),
-                rhs.replace_canon(canon),
-            ),
             Action::Delete(lhs, args) => {
                 Action::Delete(*lhs, args.iter().map(|e| e.replace_canon(canon)).collect())
             }

src/ast/parse.lalrpop

@@ -93,7 +93,6 @@ Cost: Option<usize> = {
 
 NonLetAction: Action = {
     "(" "set" "(" <f: Ident> <args:Expr*> ")" <v:Expr> ")" => Action::Set ( f, args, v ),
-    "(" "set-no-track" "(" <f: Ident> <args:Expr*> ")" <v:Expr> ")" => Action::SetNoTrack ( f, args, v ),
     "(" "delete" "(" <f: Ident> <args:Expr*> ")" ")" => Action::Delete ( f, args),
     "(" "union" <e1:Expr> <e2:Expr> ")" => Action::Union(<>),
     "(" "panic" <msg:String> ")" => Action::Panic(msg),

src/lib.rs

@@ -1135,10 +1135,12 @@ impl EGraph {
             // we need to pass in the desugar
             let proofs = self.proof_state.add_proofs(program_desugared);
 
-            let final_desugared =
-                self.proof_state
-                    .desugar
-                    .desugar_program(proofs, false, self.seminaive)?;
+            // set seminaive to false in desugar_program because we don't want to
+            // do the seminaive delta transformation again.
+            let final_desugared = self
+                .proof_state
+                .desugar
+                .desugar_program(proofs, false, false)?;
 
             // revert back to the type info before
             // proofs were added, typecheck again

src/typecheck.rs

@@ -373,7 +373,7 @@ impl<'a> ActionChecker<'a> {
                 self.locals.insert(*v, ty);
                 Ok(())
             }
-            Action::Set(f, args, val) | Action::SetNoTrack(f, args, val) => {
+            Action::Set(f, args, val) => {
                 let fake_call = Expr::Call(*f, args.clone());
                 let (_, ty) = self.infer_expr(&fake_call)?;
                 let fake_instr = self.instructions.pop().unwrap();

tests/semi_naive_set_function.egg

@@ -52,6 +52,17 @@
 (pop)
 (push)
 
+;; issue #142, while the right hand side of set is not a function, but bound to a function.
+(rule ((= f0 (f 0))) ((let a (f 3)) (set (f 0) a)))
+(run 100)
+(check (= (f 0) 3))
+(check (= (f 1) 3))
+(check (= (f 2) 3))
+(check (= (f 3) 3))
+
+(pop)
+(push)
+
 (function g (i64) i64 :merge (max old new))
 (set (g 0) 3)