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..848a41bec 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -494,6 +494,7 @@ where ruleset: Symbol, rule: GenericRule, }, + For(GenericRule), /// `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 { @@ -1564,6 +1566,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 Display for GenericRule 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 { 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)))