Skip to content

Commit

Permalink
remove global bindings! yay!
Browse files Browse the repository at this point in the history
  • Loading branch information
@oflatt
oflatt committed Feb 7, 2024
1 parent 2474c3f commit 4fa8a7a
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 65 deletions.
22 changes: 2 additions & 20 deletions src/actions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ use typechecking::TypeError;
use crate::{ast::Literal, core::ResolvedCall, ExtractReport, Value};

struct ActionCompiler<'a> {
egraph: &'a EGraph,
types: &'a IndexMap<Symbol, ArcSort>,
locals: IndexSet<ResolvedVar>,
instructions: Vec<Instruction>,
Expand Down Expand Up @@ -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);
Expand All @@ -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");
}
}
}
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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]),
Expand Down
31 changes: 10 additions & 21 deletions src/gj.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
})
}

Expand All @@ -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)?;
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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")
}
}
}
Expand Down Expand Up @@ -733,20 +727,15 @@ impl EGraph {
let has_atoms = !cq.query.funcs().collect::<Vec<_>>().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::<Vec<_>>().len()];
Expand Down
25 changes: 1 addition & 24 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,8 +416,6 @@ pub struct EGraph {
pub fact_directory: Option<PathBuf>,
pub seminaive: bool,
type_info: TypeInfo,
// sort, value, and timestamp
pub global_bindings: HashMap<Symbol, (ArcSort, Value, u32)>,
extract_report: Option<ExtractReport>,
/// The run report for the most recent run of a schedule.
recent_run_report: Option<RunReport>,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
}
Expand Down Expand Up @@ -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()]))?;
Expand Down

0 comments on commit 4fa8a7a

Please sign in to comment.