From 3962eaf7e87f66ad54cef79208e9505eb96e9591 Mon Sep 17 00:00:00 2001
From: Yihong Zhang <yz489@cs.washington.edu>
Date: Wed, 4 Dec 2024 19:16:30 -0800
Subject: [PATCH 1/2] support `for` syntax

---
 src/ast/desugar.rs | 19 +++++++++++++++++++
 src/ast/mod.rs     | 14 ++++++++++++++
 src/ast/parse.rs   |  8 ++++++++
 tests/for.egg      | 21 +++++++++++++++++++++
 4 files changed, 62 insertions(+)
 create mode 100644 tests/for.egg

diff --git a/src/ast/desugar.rs b/src/ast/desugar.rs
index a85340e88..51e4ba68f 100644
--- a/src/ast/desugar.rs
+++ b/src/ast/desugar.rs
@@ -134,6 +134,25 @@ pub(crate) fn desugar_command(
 
             result
         }
+        Command::For(rule) => {
+            let ruleset = symbol_gen.fresh(&"implicit_ruleset".into());
+            let span = rule.span.clone();
+            vec![
+                NCommand::AddRuleset(ruleset),
+                NCommand::NormRule {
+                    ruleset,
+                    name: rule.to_string().replace('\"', "'").into(),
+                    rule,
+                },
+                NCommand::RunSchedule(Schedule::Run(
+                    span,
+                    RunConfig {
+                        ruleset,
+                        until: None,
+                    },
+                )),
+            ]
+        }
         Command::Sort(span, sort, option) => vec![NCommand::Sort(span, sort, option)],
         Command::AddRuleset(name) => vec![NCommand::AddRuleset(name)],
         Command::UnstableCombinedRuleset(name, subrulesets) => {
diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index 731a2698a..ed8258fbd 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -494,6 +494,7 @@ where
         ruleset: Symbol,
         rule: GenericRule<Head, Leaf>,
     },
+    For(GenericRule<Head, Leaf>),
     /// `rewrite` is syntactic sugar for a specific form of `rule`
     /// which simply unions the left and right hand sides.
     ///
@@ -704,6 +705,7 @@ where
                 ruleset,
                 rule,
             } => rule.to_sexp(*ruleset, *name),
+            GenericCommand::For(rule) => rule.for_to_sexp(),
             GenericCommand::RunSchedule(sched) => list!("run-schedule", sched),
             GenericCommand::PrintOverallStatistics => list!("print-stats"),
             GenericCommand::QueryExtract {
@@ -1223,6 +1225,9 @@ where
         GenericExpr<Head, Leaf>,
     ),
     /// Delete or subsume (mark as hidden from future rewrites and unextractable) an entry from a function.
+    /// 
+    /// Both `subsume` and `delete` will succeed even when the deleted/subsumed tuple does not exist.
+    /// In this case, `delete` is a no-op, while `subsume` will create a dummy tuple and then subsume it.
     Change(Span, Change, Head, Vec<GenericExpr<Head, Leaf>>),
     /// `union` two datatypes, making them equal
     /// in the implicit, global equality relation
@@ -1564,6 +1569,15 @@ where
         }
         Sexp::List(res)
     }
+
+    pub fn for_to_sexp(&self) -> Sexp {
+        let res = vec![
+            Sexp::Symbol("for".into()),
+            Sexp::List(self.body.iter().map(|f| f.to_sexp()).collect()),
+            Sexp::List(self.head.0.iter().map(|a| a.to_sexp()).collect()),
+        ];
+        Sexp::List(res)
+    }
 }
 
 impl<Head, Leaf> Display for GenericRule<Head, Leaf>
diff --git a/src/ast/parse.rs b/src/ast/parse.rs
index f8ce91426..6345715dd 100644
--- a/src/ast/parse.rs
+++ b/src/ast/parse.rs
@@ -420,6 +420,14 @@ fn command(ctx: &Context) -> Res<Command> {
                 rule: Rule { span, head, body },
             },
         )(ctx),
+        "for" => map(
+            parens(sequences!(
+                text("for"),
+                list(fact),
+                map(list(action), |x, _| Actions::new(x)),
+            )),
+            |((), (body, head)), span| Command::For(Rule { span, head, body }),
+        )(ctx),
         "rewrite" => map(
             parens(sequences!(
                 text("rewrite"),
diff --git a/tests/for.egg b/tests/for.egg
new file mode 100644
index 000000000..73115613c
--- /dev/null
+++ b/tests/for.egg
@@ -0,0 +1,21 @@
+(relation range (i64))
+(relation R (i64 i64))
+
+(range 0)
+(range 1)
+(range 2)
+
+(for ((range x))
+    ((extract x)))
+
+(for ()
+    ((let x1 1)
+     (let x2 2)
+     (R x1 x2)))
+
+(check (R 1 2))
+
+(for ((R x y))
+    ((delete (R x y))))
+
+(fail (check (R 1 2)))

From cee15b6339324a6a1ab2b095b343f4f094669fec Mon Sep 17 00:00:00 2001
From: Yihong Zhang <yz489@cs.washington.edu>
Date: Wed, 4 Dec 2024 19:17:44 -0800
Subject: [PATCH 2/2] remove comments from another PR

---
 src/ast/mod.rs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index ed8258fbd..848a41bec 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -1225,9 +1225,6 @@ where
         GenericExpr<Head, Leaf>,
     ),
     /// Delete or subsume (mark as hidden from future rewrites and unextractable) an entry from a function.
-    /// 
-    /// Both `subsume` and `delete` will succeed even when the deleted/subsumed tuple does not exist.
-    /// In this case, `delete` is a no-op, while `subsume` will create a dummy tuple and then subsume it.
     Change(Span, Change, Head, Vec<GenericExpr<Head, Leaf>>),
     /// `union` two datatypes, making them equal
     /// in the implicit, global equality relation