From 4fa8a7ac0560955c6212c7795e3d2e3e64acf800 Mon Sep 17 00:00:00 2001 From: oflatt Date: Wed, 7 Feb 2024 11:55:31 -0800 Subject: [PATCH] remove global bindings! yay! --- src/actions.rs | 22 ++-------------------- src/gj.rs | 31 ++++++++++--------------------- src/lib.rs | 25 +------------------------ 3 files changed, 13 insertions(+), 65 deletions(-) diff --git a/src/actions.rs b/src/actions.rs index 5a1d9043d..0eaadd130 100644 --- a/src/actions.rs +++ b/src/actions.rs @@ -8,7 +8,6 @@ use typechecking::TypeError; use crate::{ast::Literal, core::ResolvedCall, ExtractReport, Value}; struct ActionCompiler<'a> { - egraph: &'a EGraph, types: &'a IndexMap, locals: IndexSet, instructions: Vec, @@ -60,10 +59,6 @@ impl<'a> ActionCompiler<'a> { } } - fn egraph(&self) -> &'a EGraph { - self.egraph - } - fn do_call(&mut self, f: &ResolvedCall, args: &[ResolvedAtomTerm]) { for arg in args { self.do_atom_term(arg); @@ -87,13 +82,8 @@ impl<'a> ActionCompiler<'a> { ResolvedAtomTerm::Literal(lit) => { self.instructions.push(Instruction::Literal(lit.clone())); } - ResolvedAtomTerm::Global(var) => { - assert!( - self.egraph().global_bindings.contains_key(&var.name), - "Global {} not found", - var.name - ); - self.instructions.push(Instruction::Global(var.name)); + ResolvedAtomTerm::Global(_var) => { + panic!("Global variables should have been desugared"); } } } @@ -126,8 +116,6 @@ enum Instruction { Literal(Literal), /// Push a value from the stack or the substitution onto the stack. Load(Load), - /// Push a global bound value onto the stack. - Global(Symbol), /// Pop function arguments off the stack, calls the function, /// and push the result onto the stack. The bool indicates /// whether to make defaults. @@ -171,7 +159,6 @@ impl EGraph { types.insert(var.name, var.sort.clone()); } let mut compiler = ActionCompiler { - egraph: self, types: &types, locals: IndexSet::default(), instructions: Vec::new(), @@ -200,7 +187,6 @@ impl EGraph { types.insert(var.name, var.sort.clone()); } let mut compiler = ActionCompiler { - egraph: self, types: &types, locals: IndexSet::default(), instructions: Vec::new(), @@ -274,10 +260,6 @@ impl EGraph { ) -> Result<(), Error> { for instr in &program.0 { match instr { - Instruction::Global(sym) => { - let (_ty, value, _ts) = self.global_bindings.get(sym).unwrap(); - stack.push(*value); - } Instruction::Load(load) => match load { Load::Stack(idx) => stack.push(stack[*idx]), Load::Subst(idx) => stack.push(subst[*idx]), diff --git a/src/gj.rs b/src/gj.rs index 74c8402ab..78b0da5b1 100644 --- a/src/gj.rs +++ b/src/gj.rs @@ -250,7 +250,7 @@ impl<'b> Context<'b> { self.tuple[i] } AtomTerm::Literal(lit) => self.egraph.eval_lit(lit), - AtomTerm::Global(g) => self.egraph.global_bindings.get(g).unwrap().1, + AtomTerm::Global(_g) => panic!("Globals should have been desugared"), }) } @@ -275,13 +275,8 @@ impl<'b> Context<'b> { return Ok(()); } } - AtomTerm::Global(g) => { - assert!(check); - let (sort, val, _ts) = self.egraph.global_bindings.get(g).unwrap(); - assert!(sort.name() == res.tag); - if val.bits != res.bits { - return Ok(()); - } + AtomTerm::Global(_g) => { + panic!("Globals should have been desugared") } } self.eval(tries, program, stage.next(), f)?; @@ -396,8 +391,8 @@ impl EGraph { let val = self.eval_lit(lit); constraints.push(Constraint::Const(i, val)) } - AtomTerm::Global(g) => { - constraints.push(Constraint::Const(i, self.global_bindings.get(g).unwrap().1)) + AtomTerm::Global(_g) => { + panic!("Globals should have been desugared") } AtomTerm::Var(_v) => { if let Some(j) = atom.args[..i].iter().position(|t2| t == t2) { @@ -453,9 +448,8 @@ impl EGraph { let val = self.eval_lit(lit); constants.entry(i).or_default().push((col, val)); } - AtomTerm::Global(g) => { - let val = self.global_bindings.get(g).unwrap().1; - constants.entry(i).or_default().push((col, val)); + AtomTerm::Global(_g) => { + panic!("Globals should have been desugared") } } } @@ -733,20 +727,15 @@ impl EGraph { let has_atoms = !cq.query.funcs().collect::>().is_empty(); if has_atoms { - // check if any globals updated - let mut global_updated = false; for atom in cq.query.funcs() { for arg in &atom.args { - if let AtomTerm::Global(g) = arg { - panic!("found global var {}", g); - if self.global_bindings.get(g).unwrap().2 > timestamp { - global_updated = true; - } + if let AtomTerm::Global(_g) = arg { + panic!("Globals should have been desugared") } } } - let do_seminaive = self.seminaive && !global_updated; + let do_seminaive = self.seminaive; // for the later atoms, we consider everything let mut timestamp_ranges = vec![0..u32::MAX; cq.query.funcs().collect::>().len()]; diff --git a/src/lib.rs b/src/lib.rs index f44e0e1f0..d43a61ba4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -416,8 +416,6 @@ pub struct EGraph { pub fact_directory: Option, pub seminaive: bool, type_info: TypeInfo, - // sort, value, and timestamp - pub global_bindings: HashMap, extract_report: Option, /// The run report for the most recent run of a schedule. recent_run_report: Option, @@ -445,7 +443,6 @@ impl Default for EGraph { rulesets: Default::default(), ruleset_iteration: Default::default(), desugar: Desugar::default(), - global_bindings: Default::default(), match_limit: usize::MAX, node_limit: usize::MAX, timestamp: 0, @@ -629,15 +626,6 @@ impl EGraph { } } - // now update global bindings - let mut new_global_bindings = std::mem::take(&mut self.global_bindings); - for (_sym, (sort, value, ts)) in new_global_bindings.iter_mut() { - if sort.canonicalize(value, &self.unionfind) { - *ts = self.timestamp; - } - } - self.global_bindings = new_global_bindings; - self.debug_assert_invariants(); Ok(updates) } @@ -1252,18 +1240,7 @@ impl EGraph { ResolvedNCommand::CheckProof => log::error!("TODO implement proofs"), ResolvedNCommand::CoreAction(action) => match &action { ResolvedAction::Let((), name, contents) => { - let value = self.eval_resolved_expr(contents, true)?; - let present = self.global_bindings.insert( - name.name, - ( - contents.output_type(self.type_info()), - value, - self.timestamp, - ), - ); - if present.is_some() { - panic!("Variable {name} was already present in global bindings"); - } + panic!("Globals should have been desugared away: {name} = {contents}") } _ => { self.eval_actions(&ResolvedActions::new(vec![action.clone()]))?;