Delete -naive flag and disallow lookup actions in rules

README.md

@@ -33,7 +33,7 @@ make all
 ## Usage
 
 ```
-cargo run [-f fact-path] [-naive] [--to-json] [--to-dot] [--to-svg] <files.egg>
+cargo run [-f fact-path] [--to-json] [--to-dot] [--to-svg] <files.egg>
 ```
 
 or just

src/ast/desugar.rs

@@ -7,11 +7,10 @@ use crate::*;
 pub(crate) fn desugar_program(
     program: Vec<Command>,
     symbol_gen: &mut SymbolGen,
-    seminaive_transform: bool,
 ) -> Result<Vec<NCommand>, Error> {
     let mut res = vec![];
     for command in program {
-        let desugared = desugar_command(command, symbol_gen, seminaive_transform)?;
+        let desugared = desugar_command(command, symbol_gen)?;
         res.extend(desugared);
     }
     Ok(res)
@@ -23,7 +22,6 @@ pub(crate) fn desugar_program(
 pub(crate) fn desugar_command(
     command: Command,
     symbol_gen: &mut SymbolGen,
-    seminaive_transform: bool,
 ) -> Result<Vec<NCommand>, Error> {
     let res = match command {
         Command::SetOption { name, value } => {
@@ -101,11 +99,7 @@ pub(crate) fn desugar_command(
         Command::Include(span, file) => {
             let s = std::fs::read_to_string(&file)
                 .unwrap_or_else(|_| panic!("{span} Failed to read file {file}"));
-            return desugar_program(
-                parse_program(Some(file), &s)?,
-                symbol_gen,
-                seminaive_transform,
-            );
+            return desugar_program(parse_program(Some(file), &s)?, symbol_gen);
         }
         Command::Rule {
             ruleset,
@@ -116,22 +110,12 @@ pub(crate) fn desugar_command(
                 name = rule.to_string().replace('\"', "'").into();
             }
 
-            let mut result = vec![NCommand::NormRule {
+            let result = vec![NCommand::NormRule {
                 ruleset,
                 name,
                 rule: rule.clone(),
             }];
 
-            if seminaive_transform {
-                if let Some(new_rule) = add_semi_naive_rule(symbol_gen, rule) {
-                    result.push(NCommand::NormRule {
-                        ruleset,
-                        name,
-                        rule: new_rule,
-                    });
-                }
-            }
-
             result
         }
         Command::Sort(span, sort, option) => vec![NCommand::Sort(span, sort, option)],
@@ -217,7 +201,7 @@ pub(crate) fn desugar_command(
             vec![NCommand::Pop(span, num)]
         }
         Command::Fail(span, cmd) => {
-            let mut desugared = desugar_command(*cmd, symbol_gen, seminaive_transform)?;
+            let mut desugared = desugar_command(*cmd, symbol_gen)?;
 
             let last = desugared.pop().unwrap();
             desugared.push(NCommand::Fail(span, Box::new(last)));
@@ -320,55 +304,6 @@ fn desugar_birewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec<NC
         .collect()
 }
 
-// TODO(yz): we can delete this code once we enforce that all rule bodies cannot read the database (except EqSort).
-fn add_semi_naive_rule(symbol_gen: &mut SymbolGen, rule: Rule) -> Option<Rule> {
-    let mut new_rule = rule;
-    // Whenever an Let(_, expr@Call(...)) or Set(_, expr@Call(...)) is present in action,
-    // an additional seminaive rule should be created.
-    // Moreover, for each such expr, expr and all variable definitions that it relies on should be moved to trigger.
-    let mut new_head_atoms = vec![];
-    let mut add_new_rule = false;
-
-    let mut var_set = HashSet::default();
-    for head_slice in new_rule.head.0.iter_mut().rev() {
-        match head_slice {
-            Action::Set(span, _, _, expr) => {
-                var_set.extend(expr.vars());
-                if let Expr::Call(..) = expr {
-                    add_new_rule = true;
-
-                    let fresh_symbol = symbol_gen.fresh(&"desugar_snrule".into());
-                    let fresh_var = Expr::Var(span.clone(), fresh_symbol);
-                    let expr = std::mem::replace(expr, fresh_var.clone());
-                    new_head_atoms.push(Fact::Eq(span.clone(), vec![fresh_var, expr]));
-                };
-            }
-            Action::Let(span, symbol, expr) if var_set.contains(symbol) => {
-                var_set.extend(expr.vars());
-                if let Expr::Call(..) = expr {
-                    add_new_rule = true;
-
-                    let var = Expr::Var(span.clone(), *symbol);
-                    new_head_atoms.push(Fact::Eq(span.clone(), vec![var, expr.clone()]));
-                }
-            }
-            _ => (),
-        }
-    }
-
-    if add_new_rule {
-        new_rule.body.extend(new_head_atoms.into_iter().rev());
-        // remove all let action
-        new_rule.head.0.retain_mut(
-            |action| !matches!(action, Action::Let(_ann, var, _) if var_set.contains(var)),
-        );
-        log::debug!("Added a semi-naive desugared rule:\n{}", new_rule);
-        Some(new_rule)
-    } else {
-        None
-    }
-}
-
 fn desugar_simplify(
     expr: &Expr,
     schedule: &Schedule,
@@ -391,7 +326,6 @@ fn desugar_simplify(
                 expr: Expr::Var(span.clone(), lhs),
             },
             symbol_gen,
-            false,
         )
         .unwrap(),
     );

src/ast/remove_globals.rs

@@ -197,6 +197,15 @@ impl<'a> GlobalRemover<'a> {
                     rule: new_rule,
                 }]
             }
+            //Handle the corner case where a global command is wrap in (fail )
+            GenericNCommand::Fail(span, cmd) => {
+                let mut removed = self.remove_globals_cmd(*cmd);
+                let last = removed.pop().unwrap();
+                let boxed_last = Box::new(last);
+                let new_command = GenericNCommand::Fail(span, boxed_last);
+                removed.push(new_command);
+                removed
+            }
             _ => vec![cmd.visit_exprs(&mut replace_global_vars)],
         }
     }

src/gj.rs

@@ -748,27 +748,22 @@ impl EGraph {
                 }
             }
 
-            let do_seminaive = self.seminaive;
             // for the later atoms, we consider everything
             let mut timestamp_ranges =
                 vec![0..u32::MAX; cq.query.funcs().collect::<Vec<_>>().len()];
-            if do_seminaive {
-                for (atom_i, _atom) in cq.query.funcs().enumerate() {
-                    timestamp_ranges[atom_i] = timestamp..u32::MAX;
-
-                    self.gj_for_atom(
-                        Some(atom_i),
-                        &timestamp_ranges,
-                        cq,
-                        include_subsumed,
-                        &mut f,
-                    );
-                    // now we can fix this atom to be "old stuff" only
-                    // range is half-open; timestamp is excluded
-                    timestamp_ranges[atom_i] = 0..timestamp;
-                }
-            } else {
-                self.gj_for_atom(None, &timestamp_ranges, cq, include_subsumed, &mut f);
+            for (atom_i, _atom) in cq.query.funcs().enumerate() {
+                timestamp_ranges[atom_i] = timestamp..u32::MAX;
+
+                self.gj_for_atom(
+                    Some(atom_i),
+                    &timestamp_ranges,
+                    cq,
+                    include_subsumed,
+                    &mut f,
+                );
+                // now we can fix this atom to be "old stuff" only
+                // range is half-open; timestamp is excluded
+                timestamp_ranges[atom_i] = 0..timestamp;
             }
         } else if let Some((mut ctx, program, _)) = Context::new(self, cq, &[], include_subsumed) {
             let mut meausrements = HashMap::<usize, Vec<usize>>::default();

src/lib.rs

@@ -436,7 +436,6 @@ pub struct EGraph {
     timestamp: u32,
     pub run_mode: RunMode,
     pub fact_directory: Option<PathBuf>,
-    pub seminaive: bool,
     type_info: TypeInfo,
     extract_report: Option<ExtractReport>,
     /// The run report for the most recent run of a schedule.
@@ -459,7 +458,6 @@ impl Default for EGraph {
             run_mode: RunMode::Normal,
             interactive_mode: false,
             fact_directory: None,
-            seminaive: true,
             extract_report: None,
             recent_run_report: None,
             overall_run_report: Default::default(),
@@ -1408,8 +1406,7 @@ impl EGraph {
     }
 
     fn process_command(&mut self, command: Command) -> Result<Vec<ResolvedNCommand>, Error> {
-        let program =
-            desugar::desugar_program(vec![command], &mut self.symbol_gen, self.seminaive)?;
+        let program = desugar::desugar_program(vec![command], &mut self.symbol_gen)?;
 
         let program = self
             .type_info

src/main.rs

@@ -9,8 +9,6 @@ struct Args {
     #[clap(short = 'F', long)]
     fact_directory: Option<PathBuf>,
     #[clap(long)]
-    naive: bool,
-    #[clap(long)]
     desugar: bool,
     #[clap(long)]
     resugar: bool,
@@ -101,7 +99,6 @@ fn main() {
         let mut egraph = EGraph::default();
         egraph.set_reserved_symbol(args.reserved_symbol.clone().into());
         egraph.fact_directory.clone_from(&args.fact_directory);
-        egraph.seminaive = !args.naive;
         egraph.run_mode = args.show;
         egraph
     };

src/typechecking.rs

@@ -388,13 +388,72 @@ impl TypeInfo {
         let body: Vec<ResolvedFact> = assignment.annotate_facts(&mapped_query, self);
         let actions: ResolvedActions = assignment.annotate_actions(&mapped_action, self)?;
 
+        Self::check_lookup_actions(&actions)?;
+
         Ok(ResolvedRule {
             span: span.clone(),
             body,
             head: actions,
         })
     }
 
+    fn check_lookup_expr(expr: &GenericExpr<ResolvedCall, ResolvedVar>) -> Result<(), TypeError> {
+        match expr {
+            GenericExpr::Call(span, head, args) => {
+                match head {
+                    ResolvedCall::Func(t) => {
+                        // Only allowed to lookup constructor
+                        if !t.is_datatype {
+                            Err(TypeError::LookupInRuleDisallowed(
+                                head.to_symbol(),
+                                span.clone(),
+                            ))
+                        } else {
+                            Ok(())
+                        }
+                    }
+                    ResolvedCall::Primitive(_) => Ok(()),
+                }?;
+                for arg in args.iter() {
+                    Self::check_lookup_expr(arg)?
+                }
+                Ok(())
+            }
+            _ => Ok(()),
+        }
+    }
+
+    fn check_lookup_actions(actions: &ResolvedActions) -> Result<(), TypeError> {
+        for action in actions.iter() {
+            match action {
+                GenericAction::Let(_, _, rhs) => Self::check_lookup_expr(rhs),
+                GenericAction::Set(_, _, args, rhs) => {
+                    for arg in args.iter() {
+                        Self::check_lookup_expr(arg)?
+                    }
+                    Self::check_lookup_expr(rhs)
+                }
+                GenericAction::Union(_, lhs, rhs) => {
+                    Self::check_lookup_expr(lhs)?;
+                    Self::check_lookup_expr(rhs)
+                }
+                GenericAction::Change(_, _, _, args) => {
+                    for arg in args.iter() {
+                        Self::check_lookup_expr(arg)?
+                    }
+                    Ok(())
+                }
+                GenericAction::Extract(_, expr, variants) => {
+                    Self::check_lookup_expr(expr)?;
+                    Self::check_lookup_expr(variants)
+                }
+                GenericAction::Panic(..) => Ok(()),
+                GenericAction::Expr(_, expr) => Self::check_lookup_expr(expr),
+            }?
+        }
+        Ok(())
+    }
+
     fn typecheck_facts(
         &self,
         symbol_gen: &mut SymbolGen,
@@ -516,6 +575,8 @@ pub enum TypeError {
     InferenceFailure(Expr),
     #[error("{1}\nVariable {0} was already defined")]
     AlreadyDefined(Symbol, Span),
+    #[error("{1}\nValue lookup of non-constructor function {0} in rule is disallowed.")]
+    LookupInRuleDisallowed(Symbol, Span),
     #[error("All alternative definitions considered failed\n{}", .0.iter().map(|e| format!("  {e}\n")).collect::<Vec<_>>().join(""))]
     AllAlternativeFailed(Vec<TypeError>),
 }

tests/array.egg

@@ -20,21 +20,21 @@
 (relation neq (Math Math))
 
 (rule ((neq x y))
-      ((neq y x)))
+      ((set (neq y x) ())))
 
 (rule ((neq x x))
       ((panic "query (neq x x) found something equal to itself")))
 
 
 ; injectivity rules take not equal to not equal.
 (rule  ((neq x y) (= (add x z) e))
-       ((neq (add x z) (add y z))))
+       ((set (neq (add x z) (add y z)) ())))
 (rule  ((= (add x (Num i)) e) (!= i 0))
-       ((neq e x)))
+       ((set (neq e x) ())))
 
 
 (rule ((= (Num a) n1) (= (Num b) n2) (!= a b))
-      ((neq n1 n2)))
+      ((set (neq n1 n2) ())))
 
 ; select gets from store
 (rewrite (select (store mem i e) i) e)
@@ -59,9 +59,9 @@
 (let r3 (Var "r3"))
 (let mem1 (AVar "mem1"))
 
-(neq r1 r2)
-(neq r2 r3)
-(neq r1 r3)
+(set (neq r1 r2) ())
+(set (neq r2 r3) ())
+(set (neq r1 r3) ())
 (let test1 (select (store mem1 r1 (Num 42)) r1))
 (let test2 (select (store mem1 r1 (Num 42)) (add r1 (Num 17))))
 (let test3 (select (store (store mem1 (add r1 r2) (Num 1)) (add r2 r1) (Num 2)) (add r1 r3)))