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 } => {
@@ -103,8 +101,7 @@ pub(crate) fn desugar_command(
                 .unwrap_or_else(|_| panic!("{span} Failed to read file {file}"));
             return desugar_program(
                 parse_program(Some(file), &s)?,
-                symbol_gen,
-                seminaive_transform,
+                symbol_gen
             );
         }
         Command::Rule {
@@ -116,22 +113,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 +204,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 +307,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,
@@ -390,8 +328,7 @@ fn desugar_simplify(
                 variants: 0,
                 expr: Expr::Var(span.clone(), lhs),
             },
-            symbol_gen,
-            false,
+            symbol_gen
         )
         .unwrap(),
     );

src/ast/remove_globals.rs

@@ -196,6 +196,15 @@ impl<'a> GlobalRemover<'a> {
                     ruleset,
                     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(),
@@ -1409,7 +1407,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)?;
+            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

@@ -367,6 +367,19 @@ impl TypeInfo {
         let (query, mapped_query) = Facts(body.clone()).to_query(self, symbol_gen);
         constraints.extend(query.get_constraints(self)?);
 
+        //Disallowing Let/Set actions to look up non-constructor functions in rules
+        for action in head.iter() {
+            match action {
+                GenericAction::Let(_, _, Expr::Call(_, symbol, _)) => {
+                    return Err(TypeError::LookupInRuleDisallowed(*symbol, span.clone()));
+                }
+                GenericAction::Set(_, _, _, Expr::Call(_, symbol, _)) => {
+                    return Err(TypeError::LookupInRuleDisallowed(*symbol, span.clone()));
+                }
+                _ => ()
+            }
+        }
+
         let mut binding = query.get_vars();
         let (actions, mapped_action) = head.to_core_actions(self, &mut binding, symbol_gen)?;
 
@@ -516,6 +529,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>),
 }