seminaive transform for replace

egraphs-good · Sep 8, 2023 · c9b20c0 · c9b20c0
1 parent 4176de6
commit c9b20c0
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/src/ast/desugar.rs b/src/ast/desugar.rs
@@ -411,6 +411,17 @@ fn add_semi_naive_rule(desugar: &mut Desugar, rule: Rule) -> Option<Rule> {
                     new_head_atoms.push(Fact::Eq(vec![fresh_var, expr]));
                 };
             }
+            Action::Replace { new_output, .. } => {
+                var_set.extend(new_output.vars());
+                if let Expr::Call(_, _) = new_output {
+                    add_new_rule = true;
+
+                    let fresh_symbol = desugar.get_fresh();
+                    let fresh_var = Expr::Var(fresh_symbol);
+                    let new_output = std::mem::replace(new_output, fresh_var.clone());
+                    new_head_atoms.push(Fact::Eq(vec![fresh_var, new_output]));
+                };
+            }
             Action::Let(symbol, expr) if var_set.contains(symbol) => {
                 var_set.extend(expr.vars());
                 if let Expr::Call(_, _) = expr {