diff --git a/src/actions.rs b/src/actions.rs index 2a028802..a14f7448 100644 --- a/src/actions.rs +++ b/src/actions.rs @@ -16,20 +16,20 @@ struct ActionCompiler<'a> { impl<'a> ActionCompiler<'a> { fn compile_action(&mut self, action: &GenericCoreAction) { match action { - GenericCoreAction::Let(v, f, args) => { + GenericCoreAction::Let(_ann, v, f, args) => { self.do_call(f, args); self.locals.insert(v.clone()); } - GenericCoreAction::LetAtomTerm(v, at) => { + GenericCoreAction::LetAtomTerm(_ann, v, at) => { self.do_atom_term(at); self.locals.insert(v.clone()); } - GenericCoreAction::Extract(e, b) => { + GenericCoreAction::Extract(_ann, e, b) => { self.do_atom_term(e); self.do_atom_term(b); self.instructions.push(Instruction::Extract(2)); } - GenericCoreAction::Set(f, args, e) => { + GenericCoreAction::Set(_ann, f, args, e) => { let ResolvedCall::Func(func) = f else { panic!("Cannot set primitive- should have been caught by typechecking!!!") }; @@ -39,7 +39,7 @@ impl<'a> ActionCompiler<'a> { self.do_atom_term(e); self.instructions.push(Instruction::Set(func.name)); } - GenericCoreAction::Change(change, f, args) => { + GenericCoreAction::Change(_ann, change, f, args) => { let ResolvedCall::Func(func) = f else { panic!("Cannot change primitive- should have been caught by typechecking!!!") }; @@ -49,12 +49,12 @@ impl<'a> ActionCompiler<'a> { self.instructions .push(Instruction::Change(*change, func.name)); } - GenericCoreAction::Union(arg1, arg2) => { + GenericCoreAction::Union(_ann, arg1, arg2) => { self.do_atom_term(arg1); self.do_atom_term(arg2); self.instructions.push(Instruction::Union(2)); } - GenericCoreAction::Panic(msg) => { + GenericCoreAction::Panic(_ann, msg) => { self.instructions.push(Instruction::Panic(msg.clone())); } } @@ -72,7 +72,7 @@ impl<'a> ActionCompiler<'a> { fn do_atom_term(&mut self, at: &ResolvedAtomTerm) { match at { - ResolvedAtomTerm::Var(var) => { + ResolvedAtomTerm::Var(_ann, var) => { if let Some((i, _ty)) = self.locals.get_full(var) { self.instructions.push(Instruction::Load(Load::Stack(i))); } else { @@ -80,10 +80,10 @@ impl<'a> ActionCompiler<'a> { self.instructions.push(Instruction::Load(Load::Subst(i))); } } - ResolvedAtomTerm::Literal(lit) => { + ResolvedAtomTerm::Literal(_ann, lit) => { self.instructions.push(Instruction::Literal(lit.clone())); } - ResolvedAtomTerm::Global(_var) => { + ResolvedAtomTerm::Global(_ann, _var) => { panic!("Global variables should have been desugared"); } } @@ -301,16 +301,16 @@ impl EGraph { value } _ => { - return Err(Error::NotFoundError(NotFoundError(Expr::Var( - (), - format!("No value found for {f} {:?}", values).into(), + return Err(Error::NotFoundError(NotFoundError(format!( + "No value found for {f} {:?}", + values )))) } } } else { - return Err(Error::NotFoundError(NotFoundError(Expr::Var( - (), - format!("No value found for {f} {:?}", values).into(), + return Err(Error::NotFoundError(NotFoundError(format!( + "No value found for {f} {:?}", + values )))); }; diff --git a/src/ast/desugar.rs b/src/ast/desugar.rs index a9a654d8..4fe3fc1e 100644 --- a/src/ast/desugar.rs +++ b/src/ast/desugar.rs @@ -45,13 +45,22 @@ fn desugar_rewrite( rewrite: &Rewrite, subsume: bool, ) -> Vec { + let span = rewrite.span.clone(); let var = Symbol::from("rewrite_var__"); - let mut head = Actions::singleton(Action::Union((), Expr::Var((), var), rewrite.rhs.clone())); + let mut head = Actions::singleton(Action::Union( + span.clone(), + Expr::Var(span.clone(), var), + rewrite.rhs.clone(), + )); if subsume { match &rewrite.lhs { Expr::Call(_, f, args) => { - head.0 - .push(Action::Change((), Change::Subsume, *f, args.to_vec())); + head.0.push(Action::Change( + span.clone(), + Change::Subsume, + *f, + args.to_vec(), + )); } _ => { panic!("Subsumed rewrite must have a function call on the lhs"); @@ -65,17 +74,23 @@ fn desugar_rewrite( ruleset, name, rule: Rule { - body: [Fact::Eq(vec![Expr::Var((), var), rewrite.lhs.clone()])] - .into_iter() - .chain(rewrite.conditions.clone()) - .collect(), + span: span.clone(), + body: [Fact::Eq( + span.clone(), + vec![Expr::Var(span, var), rewrite.lhs.clone()], + )] + .into_iter() + .chain(rewrite.conditions.clone()) + .collect(), head, }, }] } fn desugar_birewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec { + let span = rewrite.span.clone(); let rw2 = Rewrite { + span, lhs: rewrite.rhs.clone(), rhs: rewrite.lhs.clone(), conditions: rewrite.conditions.clone(), @@ -91,6 +106,7 @@ fn desugar_birewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec Option { let mut new_rule = rule; // Whenever an Let(_, expr@Call(...)) or Set(_, expr@Call(...)) is present in action, @@ -102,24 +118,24 @@ fn add_semi_naive_rule(desugar: &mut Desugar, rule: Rule) -> Option { let mut var_set = HashSet::default(); for head_slice in new_rule.head.0.iter_mut().rev() { match head_slice { - Action::Set(_ann, _, _, expr) => { + Action::Set(span, _, _, expr) => { var_set.extend(expr.vars()); - if let Expr::Call((), _, _) = expr { + if let Expr::Call(..) = expr { add_new_rule = true; let fresh_symbol = desugar.get_fresh(); - let fresh_var = Expr::Var((), fresh_symbol); + let fresh_var = Expr::Var(span.clone(), fresh_symbol); let expr = std::mem::replace(expr, fresh_var.clone()); - new_head_atoms.push(Fact::Eq(vec![fresh_var, expr])); + new_head_atoms.push(Fact::Eq(span.clone(), vec![fresh_var, expr])); }; } - Action::Let(_ann, symbol, expr) if var_set.contains(symbol) => { + Action::Let(span, symbol, expr) if var_set.contains(symbol) => { var_set.extend(expr.vars()); - if let Expr::Call((), _, _) = expr { + if let Expr::Call(..) = expr { add_new_rule = true; - let var = Expr::Var((), *symbol); - new_head_atoms.push(Fact::Eq(vec![var, expr.clone()])); + let var = Expr::Var(span.clone(), *symbol); + new_head_atoms.push(Fact::Eq(span.clone(), vec![var, expr.clone()])); } } _ => (), @@ -140,15 +156,20 @@ fn add_semi_naive_rule(desugar: &mut Desugar, rule: Rule) -> Option { } fn desugar_simplify(desugar: &mut Desugar, expr: &Expr, schedule: &Schedule) -> Vec { + let span = expr.span(); let mut res = vec![NCommand::Push(1)]; let lhs = desugar.get_fresh(); - res.push(NCommand::CoreAction(Action::Let((), lhs, expr.clone()))); + res.push(NCommand::CoreAction(Action::Let( + span.clone(), + lhs, + expr.clone(), + ))); res.push(NCommand::RunSchedule(schedule.clone())); res.extend( desugar_command( Command::QueryExtract { variants: 0, - expr: Expr::Var((), lhs), + expr: Expr::Var(span, lhs), }, desugar, false, @@ -163,6 +184,7 @@ fn desugar_simplify(desugar: &mut Desugar, expr: &Expr, schedule: &Schedule) -> pub(crate) fn desugar_calc( desugar: &mut Desugar, + span: Span, idents: Vec, exprs: Vec, seminaive_transform: bool, @@ -171,7 +193,11 @@ pub(crate) fn desugar_calc( // first, push all the idents for IdentSort { ident, sort } in idents { - res.push(Command::Declare { name: ident, sort }); + res.push(Command::Declare { + span: span.clone(), + name: ident, + sort, + }); } // now, for every pair of exprs we need to prove them equal @@ -182,23 +208,30 @@ pub(crate) fn desugar_calc( // add the two exprs only when they are calls (consts and vars don't need to be populated). if let Expr::Call(..) = expr1 { - res.push(Command::Action(Action::Expr((), expr1.clone()))); + res.push(Command::Action(Action::Expr(expr1.span(), expr1.clone()))); } if let Expr::Call(..) = expr2 { - res.push(Command::Action(Action::Expr((), expr2.clone()))); + res.push(Command::Action(Action::Expr(expr2.span(), expr2.clone()))); } - res.push(Command::RunSchedule(Schedule::Saturate(Box::new( - Schedule::Run(RunConfig { - ruleset: "".into(), - until: Some(vec![Fact::Eq(vec![expr1.clone(), expr2.clone()])]), - }), - )))); + res.push(Command::RunSchedule(Schedule::Saturate( + span.clone(), + Box::new(Schedule::Run( + span.clone(), + RunConfig { + ruleset: "".into(), + until: Some(vec![Fact::Eq( + span.clone(), + vec![expr1.clone(), expr2.clone()], + )]), + }, + )), + ))); - res.push(Command::Check(vec![Fact::Eq(vec![ - expr1.clone(), - expr2.clone(), - ])])); + res.push(Command::Check( + span.clone(), + vec![Fact::Eq(span.clone(), vec![expr1.clone(), expr2.clone()])], + )); res.push(Command::Pop(1)); } @@ -228,7 +261,7 @@ pub(crate) fn desugar_command( constructor, inputs, } => desugar.desugar_function(&FunctionDecl::relation(constructor, inputs)), - Command::Declare { name, sort } => desugar.declare(name, sort), + Command::Declare { span, name, sort } => desugar.declare(span, name, sort), Command::Datatype { name, variants } => desugar_datatype(name, variants), Command::Rewrite(ruleset, rewrite, subsume) => { desugar_rewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite, subsume) @@ -240,7 +273,7 @@ pub(crate) fn desugar_command( let s = std::fs::read_to_string(&file) .unwrap_or_else(|_| panic!("Failed to read file {file}")); return desugar_commands( - desugar.parse_program(&s)?, + desugar.parse_program(Some(file), &s)?, desugar, get_all_proofs, seminaive_transform, @@ -280,7 +313,9 @@ pub(crate) fn desugar_command( } Command::Action(action) => vec![NCommand::CoreAction(action)], Command::Simplify { expr, schedule } => desugar_simplify(desugar, &expr, &schedule), - Command::Calc(idents, exprs) => desugar_calc(desugar, idents, exprs, seminaive_transform)?, + Command::Calc(span, idents, exprs) => { + desugar_calc(desugar, span, idents, exprs, seminaive_transform)? + } Command::RunSchedule(sched) => { vec![NCommand::RunSchedule(sched.clone())] } @@ -290,7 +325,7 @@ pub(crate) fn desugar_command( Command::QueryExtract { variants, expr } => { let fresh = desugar.get_fresh(); let fresh_ruleset = desugar.get_fresh(); - let desugaring = if let Expr::Var((), v) = expr { + let desugaring = if let Expr::Var(_, v) = expr { format!("(extract {v} {variants})") } else { format!( @@ -304,13 +339,13 @@ pub(crate) fn desugar_command( }; desugar.desugar_program( - desugar.parse_program(&desugaring).unwrap(), + desugar.parse_program(None, &desugaring).unwrap(), get_all_proofs, seminaive_transform, )? } - Command::Check(facts) => { - let res = vec![NCommand::Check(facts)]; + Command::Check(span, facts) => { + let res = vec![NCommand::Check(span, facts)]; if get_all_proofs { // TODO check proofs @@ -383,15 +418,24 @@ impl Desugar { Ok(res) } - pub fn parse_program(&self, input: &str) -> Result, Error> { + pub fn parse_program( + &self, + filename: Option, + input: &str, + ) -> Result, Error> { + let filename = filename.unwrap_or_else(|| DEFAULT_FILENAME.to_string()); + let srcfile = Arc::new(SrcFile { + name: filename, + contents: Some(input.to_string()), + }); Ok(self .parser - .parse(input) + .parse(&srcfile, input) .map_err(|e| e.map_token(|tok| tok.to_string()))?) } // TODO declare by creating a new global function. See issue #334 - pub fn declare(&mut self, name: Symbol, sort: Symbol) -> Vec { + pub fn declare(&mut self, span: Span, name: Symbol, sort: Symbol) -> Vec { let fresh = self.get_fresh(); vec![ NCommand::Function(FunctionDecl { @@ -407,7 +451,11 @@ impl Desugar { unextractable: false, ignore_viz: false, }), - NCommand::CoreAction(Action::Let((), name, Expr::Call((), fresh, vec![]))), + NCommand::CoreAction(Action::Let( + span.clone(), + name, + Expr::Call(span.clone(), fresh, vec![]), + )), ] } diff --git a/src/ast/expr.rs b/src/ast/expr.rs index 718032ee..83f96566 100644 --- a/src/ast/expr.rs +++ b/src/ast/expr.rs @@ -105,19 +105,21 @@ impl ToSexp for ResolvedVar { } } -pub type Expr = GenericExpr; -pub(crate) type ResolvedExpr = GenericExpr; +pub type Expr = GenericExpr; +/// A generated expression is an expression that is generated by the system +/// and does not have annotations. +pub(crate) type ResolvedExpr = GenericExpr; /// A [`MappedExpr`] arises naturally when you want a mapping between an expression /// and its flattened form. It records this mapping by annotating each `Head` /// with a `Leaf`, which it maps to in the flattened form. /// A useful operation on `MappedExpr`s is [`MappedExpr::get_corresponding_var_or_lit``]. -pub(crate) type MappedExpr = GenericExpr, Leaf, Ann>; +pub(crate) type MappedExpr = GenericExpr, Leaf>; -#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Clone)] -pub enum GenericExpr { - Lit(Ann, Literal), - Var(Ann, Leaf), - Call(Ann, Head, Vec), +#[derive(Debug, PartialEq, Eq, Hash, Clone)] +pub enum GenericExpr { + Lit(Span, Literal), + Var(Span, Leaf), + Call(Span, Head, Vec), } impl ResolvedExpr { @@ -138,23 +140,29 @@ impl ResolvedExpr { } impl Expr { - pub fn call(op: impl Into, children: impl IntoIterator) -> Self { - Self::Call((), op.into(), children.into_iter().collect()) + pub fn call_no_span(op: impl Into, children: impl IntoIterator) -> Self { + Self::Call( + DUMMY_SPAN.clone(), + op.into(), + children.into_iter().collect(), + ) + } + + pub fn lit_no_span(lit: impl Into) -> Self { + Self::Lit(DUMMY_SPAN.clone(), lit.into()) } - pub fn lit(lit: impl Into) -> Self { - Self::Lit((), lit.into()) + pub fn var_no_span(v: impl Into) -> Self { + Self::Var(DUMMY_SPAN.clone(), v.into()) } } -impl - GenericExpr -{ - pub fn ann(&self) -> Ann { +impl GenericExpr { + pub fn span(&self) -> Span { match self { - GenericExpr::Lit(ann, _) => ann.clone(), - GenericExpr::Var(ann, _) => ann.clone(), - GenericExpr::Call(ann, _, _) => ann.clone(), + GenericExpr::Lit(span, _) => span.clone(), + GenericExpr::Var(span, _) => span.clone(), + GenericExpr::Call(span, _, _) => span.clone(), } } @@ -201,39 +209,36 @@ impl match self { GenericExpr::Lit(..) => f(self), GenericExpr::Var(..) => f(self), - GenericExpr::Call(ann, op, children) => { + GenericExpr::Call(span, op, children) => { let children = children.into_iter().map(|c| c.visit_exprs(f)).collect(); - f(GenericExpr::Call(ann.clone(), op.clone(), children)) + f(GenericExpr::Call(span, op.clone(), children)) } } } - // TODO: Currently, subst_leaf takes a leaf but not an annotation over the leaf, - // so it has to "make up" annotations for the returned GenericExpr. A better - // approach is for subst_leaf to also take the annotation, which we should - // implement after we use real non-() annotations + /// `subst` replaces occurrences of variables and head symbols in the expression. pub fn subst( &self, - subst_leaf: &mut impl FnMut(&Leaf) -> GenericExpr, + subst_leaf: &mut impl FnMut(&Span, &Leaf) -> GenericExpr, subst_head: &mut impl FnMut(&Head) -> Head2, - ) -> GenericExpr { + ) -> GenericExpr { match self { - GenericExpr::Lit(ann, lit) => GenericExpr::Lit(ann.clone(), lit.clone()), - GenericExpr::Var(_ann, v) => subst_leaf(v), - GenericExpr::Call(ann, op, children) => { + GenericExpr::Lit(span, lit) => GenericExpr::Lit(span.clone(), lit.clone()), + GenericExpr::Var(span, v) => subst_leaf(span, v), + GenericExpr::Call(span, op, children) => { let children = children .iter() .map(|c| c.subst(subst_leaf, subst_head)) .collect(); - GenericExpr::Call(ann.clone(), subst_head(op), children) + GenericExpr::Call(span.clone(), subst_head(op), children) } } } pub fn subst_leaf( &self, - subst_leaf: &mut impl FnMut(&Leaf) -> GenericExpr, - ) -> GenericExpr { + subst_leaf: &mut impl FnMut(&Span, &Leaf) -> GenericExpr, + ) -> GenericExpr { self.subst(subst_leaf, &mut |x| x.clone()) } @@ -247,7 +252,7 @@ impl } } -impl GenericExpr { +impl GenericExpr { /// Converts this expression into a /// s-expression (symbolic expression). /// Example: `(Add (Add 2 3) 4)` @@ -266,7 +271,7 @@ impl GenericExpr { } } -impl Display for GenericExpr +impl Display for GenericExpr where Head: Display, Leaf: Display, @@ -281,7 +286,7 @@ where pub(crate) fn parse_expr(s: &str) -> Result> { let parser = ast::parse::ExprParser::new(); parser - .parse(s) + .parse(&DUMMY_FILE, s) .map_err(|e| e.map_token(|tok| tok.to_string())) } diff --git a/src/ast/mod.rs b/src/ast/mod.rs index d1ff066b..30e49bc6 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -1,3 +1,4 @@ +use lazy_static::lazy_static; use std::fmt::Display; pub use symbol_table::GlobalSymbol as Symbol; @@ -51,11 +52,32 @@ pub(crate) enum Ruleset { Combined(Symbol, Vec), } -pub type NCommand = GenericNCommand; +pub(crate) const DEFAULT_FILENAME: &str = ""; +pub(crate) const DUMMY_FILENAME: &str = ""; + +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct SrcFile { + pub name: String, + pub contents: Option, +} + +/// A [`Span`] contains the file name and a pair of offsets representing the start and the end. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct Span(pub Arc, pub usize, pub usize); + +lazy_static! { + pub(crate) static ref DUMMY_FILE: Arc = Arc::new(SrcFile { + name: DUMMY_FILENAME.to_string(), + contents: None + }); + pub(crate) static ref DUMMY_SPAN: Span = Span(DUMMY_FILE.clone(), 0, 0); +} + +pub type NCommand = GenericNCommand; /// [`ResolvedNCommand`] is another specialization of [`GenericNCommand`], which /// adds the type information to heads and leaves of commands. /// [`TypeInfo::typecheck_command`] turns an [`NCommand`] into a [`ResolvedNCommand`]. -pub(crate) type ResolvedNCommand = GenericNCommand; +pub(crate) type ResolvedNCommand = GenericNCommand; /// A [`NCommand`] is a desugared [`Command`], where syntactic sugars /// like [`Command::Datatype`], [`Command::Declare`], and [`Command::Rewrite`] @@ -69,49 +91,45 @@ pub(crate) type ResolvedNCommand = GenericNCommand +pub enum GenericNCommand where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { SetOption { name: Symbol, - value: GenericExpr, + value: GenericExpr, }, - Sort( - Symbol, - Option<(Symbol, Vec>)>, - ), - Function(GenericFunctionDecl), + Sort(Symbol, Option<(Symbol, Vec>)>), + Function(GenericFunctionDecl), AddRuleset(Symbol), UnstableCombinedRuleset(Symbol, Vec), NormRule { name: Symbol, ruleset: Symbol, - rule: GenericRule, + rule: GenericRule, }, - CoreAction(GenericAction), - RunSchedule(GenericSchedule), + CoreAction(GenericAction), + RunSchedule(GenericSchedule), PrintOverallStatistics, - Check(Vec>), + Check(Span, Vec>), CheckProof, PrintTable(Symbol, usize), PrintSize(Option), Output { file: String, - exprs: Vec>, + exprs: Vec>, }, Push(usize), Pop(usize), - Fail(Box>), + Fail(Box>), Input { name: Symbol, file: String, }, } -impl GenericNCommand +impl GenericNCommand where Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, @@ -140,7 +158,9 @@ where GenericNCommand::RunSchedule(schedule) => GenericCommand::RunSchedule(schedule.clone()), GenericNCommand::PrintOverallStatistics => GenericCommand::PrintOverallStatistics, GenericNCommand::CoreAction(action) => GenericCommand::Action(action.clone()), - GenericNCommand::Check(facts) => GenericCommand::Check(facts.clone()), + GenericNCommand::Check(span, facts) => { + GenericCommand::Check(span.clone(), facts.clone()) + } GenericNCommand::CheckProof => GenericCommand::CheckProof, GenericNCommand::PrintTable(name, n) => GenericCommand::PrintFunction(*name, *n), GenericNCommand::PrintSize(name) => GenericCommand::PrintSize(*name), @@ -160,7 +180,7 @@ where pub fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { match self { GenericNCommand::SetOption { name, value } => GenericNCommand::SetOption { @@ -189,9 +209,10 @@ where GenericNCommand::CoreAction(action) => { GenericNCommand::CoreAction(action.visit_exprs(f)) } - GenericNCommand::Check(facts) => { - GenericNCommand::Check(facts.into_iter().map(|fact| fact.visit_exprs(f)).collect()) - } + GenericNCommand::Check(span, facts) => GenericNCommand::Check( + span, + facts.into_iter().map(|fact| fact.visit_exprs(f)).collect(), + ), GenericNCommand::CheckProof => GenericNCommand::CheckProof, GenericNCommand::PrintTable(name, n) => GenericNCommand::PrintTable(name, n), GenericNCommand::PrintSize(name) => GenericNCommand::PrintSize(name), @@ -207,21 +228,15 @@ where } } -pub type Schedule = GenericSchedule; -pub(crate) type ResolvedSchedule = GenericSchedule; +pub type Schedule = GenericSchedule; +pub(crate) type ResolvedSchedule = GenericSchedule; #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub enum GenericSchedule { - Saturate(Box>), - Repeat(usize, Box>), - Run(GenericRunConfig), - Sequence(Vec>), -} - -impl GenericSchedule { - pub fn saturate(self) -> Self { - GenericSchedule::Saturate(Box::new(self)) - } +pub enum GenericSchedule { + Saturate(Span, Box>), + Repeat(Span, usize, Box>), + Run(Span, GenericRunConfig), + Sequence(Span, Vec>), } pub trait ToSexp { @@ -264,43 +279,43 @@ macro_rules! list { }}; } -impl GenericSchedule +impl GenericSchedule where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { match self { - GenericSchedule::Saturate(sched) => { - GenericSchedule::Saturate(Box::new(sched.visit_exprs(f))) - } - GenericSchedule::Repeat(size, sched) => { - GenericSchedule::Repeat(size, Box::new(sched.visit_exprs(f))) + GenericSchedule::Saturate(span, sched) => { + GenericSchedule::Saturate(span, Box::new(sched.visit_exprs(f))) } - GenericSchedule::Run(config) => GenericSchedule::Run(config.visit_exprs(f)), - GenericSchedule::Sequence(scheds) => { - GenericSchedule::Sequence(scheds.into_iter().map(|s| s.visit_exprs(f)).collect()) + GenericSchedule::Repeat(span, size, sched) => { + GenericSchedule::Repeat(span, size, Box::new(sched.visit_exprs(f))) } + GenericSchedule::Run(span, config) => GenericSchedule::Run(span, config.visit_exprs(f)), + GenericSchedule::Sequence(span, scheds) => GenericSchedule::Sequence( + span, + scheds.into_iter().map(|s| s.visit_exprs(f)).collect(), + ), } } } -impl ToSexp for GenericSchedule { +impl ToSexp for GenericSchedule { fn to_sexp(&self) -> Sexp { match self { - GenericSchedule::Saturate(sched) => list!("saturate", sched), - GenericSchedule::Repeat(size, sched) => list!("repeat", size, sched), - GenericSchedule::Run(config) => config.to_sexp(), - GenericSchedule::Sequence(scheds) => list!("seq", ++ scheds), + GenericSchedule::Saturate(_ann, sched) => list!("saturate", sched), + GenericSchedule::Repeat(_ann, size, sched) => list!("repeat", size, sched), + GenericSchedule::Run(_ann, config) => config.to_sexp(), + GenericSchedule::Sequence(_ann, scheds) => list!("seq", ++ scheds), } } } -impl Display for GenericSchedule { +impl Display for GenericSchedule { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{}", self.to_sexp()) } @@ -330,7 +345,7 @@ where /// tool to know when each command has finished running. SetOption { name: Symbol, - value: GenericExpr, + value: GenericExpr, }, /// Declare a user-defined datatype. /// Datatypes can be unioned with [`Action::Union`] either @@ -378,6 +393,7 @@ where /// Note that declare inserts the constant into the database, /// so rules can use the constant directly as a variable. Declare { + span: Span, name: Symbol, sort: Symbol, }, @@ -396,7 +412,7 @@ where /// ``` /// /// Now `MathVec` can be used as an input or output sort. - Sort(Symbol, Option<(Symbol, Vec)>), + Sort(Symbol, Option<(Symbol, Vec>)>), /// Declare an egglog function, which is a database table with a /// a functional dependency (also called a primary key) on its inputs to one output. /// @@ -442,7 +458,7 @@ where /// /// Functions that are not a datatype can be `set` /// with [`Action::Set`]. - Function(GenericFunctionDecl), + Function(GenericFunctionDecl), /// The `relation` is syntactic sugar for a named function which returns the `Unit` type. /// Example: /// ```text @@ -516,7 +532,7 @@ where Rule { name: Symbol, ruleset: Symbol, - rule: GenericRule, + rule: GenericRule, }, /// `rewrite` is syntactic sugar for a specific form of `rule` /// which simply unions the left and right hand sides. @@ -557,7 +573,7 @@ where /// ((union lhs (bitshift-left a 1)) /// (subsume (Mul a 2)))) /// ``` - Rewrite(Symbol, GenericRewrite, Subsume), + Rewrite(Symbol, GenericRewrite, Subsume), /// Similar to [`Command::Rewrite`], but /// generates two rules, one for each direction. /// @@ -574,14 +590,14 @@ where /// (rule ((= lhs (Var x))) /// ((union lhs (Mul (Var x) (Num 0))))) /// ``` - BiRewrite(Symbol, GenericRewrite), + BiRewrite(Symbol, GenericRewrite), /// Perform an [`Action`] on the global database /// (see documentation for [`Action`] for more details). /// Example: /// ```text /// (let xplusone (Add (Var "x") (Num 1))) /// ``` - Action(GenericAction), + Action(GenericAction), /// Runs a [`Schedule`], which specifies /// rulesets and the number of times to run them. /// @@ -596,17 +612,17 @@ where /// then runs `my-ruleset-2` four times. /// /// See [`Schedule`] for more details. - RunSchedule(GenericSchedule), + RunSchedule(GenericSchedule), /// Print runtime statistics about rules /// and rulesets so far. PrintOverallStatistics, // TODO provide simplify docs Simplify { - expr: GenericExpr, - schedule: GenericSchedule, + expr: GenericExpr, + schedule: GenericSchedule, }, // TODO provide calc docs - Calc(Vec, Vec>), + Calc(Span, Vec, Vec>), /// The `query-extract` command runs a query, /// extracting the result for each match that it finds. /// For a simpler extraction command, use [`Action::Extract`] instead. @@ -634,7 +650,7 @@ where /// function. QueryExtract { variants: usize, - expr: GenericExpr, + expr: GenericExpr, }, /// The `check` command checks that the given facts /// match at least once in the current database. @@ -656,7 +672,7 @@ where /// [ERROR] Check failed /// [INFO ] Command failed as expected. /// ``` - Check(Vec>), + Check(Span, Vec>), /// Currently unused, this command will check proofs when they are implemented. CheckProof, /// Print out rows a given function, extracting each of the elements of the function. @@ -677,7 +693,7 @@ where /// Extract and output a set of expressions to a file. Output { file: String, - exprs: Vec>, + exprs: Vec>, }, /// `push` the current egraph `n` times so that it is saved. /// Later, the current database and rules can be restored using `pop`. @@ -704,7 +720,11 @@ where } GenericCommand::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true, false), GenericCommand::Datatype { name, variants } => list!("datatype", name, ++ variants), - GenericCommand::Declare { name, sort } => list!("declare", name, sort), + GenericCommand::Declare { + span: _, + name, + sort, + } => list!("declare", name, sort), GenericCommand::Action(a) => a.to_sexp(), GenericCommand::Sort(name, None) => list!("sort", name), GenericCommand::Sort(name, Some((name2, args))) => { @@ -726,11 +746,11 @@ where } => rule.to_sexp(*ruleset, *name), GenericCommand::RunSchedule(sched) => list!("run-schedule", sched), GenericCommand::PrintOverallStatistics => list!("print-stats"), - GenericCommand::Calc(args, exprs) => list!("calc", list!(++ args), ++ exprs), + GenericCommand::Calc(_ann, args, exprs) => list!("calc", list!(++ args), ++ exprs), GenericCommand::QueryExtract { variants, expr } => { list!("query-extract", ":variants", variants, expr) } - GenericCommand::Check(facts) => list!("check", ++ facts), + GenericCommand::Check(_ann, facts) => list!("check", ++ facts), GenericCommand::CheckProof => list!("check-proof"), GenericCommand::Push(n) => list!("push", n), GenericCommand::Pop(n) => list!("pop", n), @@ -747,7 +767,7 @@ where } } -impl Display for GenericNCommand +impl Display for GenericNCommand where Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, @@ -769,7 +789,7 @@ where name, rule, } => rule.fmt_with_ruleset(f, *ruleset, *name), - GenericCommand::Check(facts) => { + GenericCommand::Check(_ann, facts) => { write!(f, "(check {})", ListDisplay(facts, "\n")) } _ => write!(f, "{}", self.to_sexp()), @@ -795,24 +815,23 @@ impl Display for IdentSort { } } -pub type RunConfig = GenericRunConfig; -pub(crate) type ResolvedRunConfig = GenericRunConfig; +pub type RunConfig = GenericRunConfig; +pub(crate) type ResolvedRunConfig = GenericRunConfig; #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub struct GenericRunConfig { +pub struct GenericRunConfig { pub ruleset: Symbol, - pub until: Option>>, + pub until: Option>>, } -impl GenericRunConfig +impl GenericRunConfig where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { pub fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { Self { ruleset: self.ruleset, @@ -823,7 +842,7 @@ where } } -impl ToSexp for GenericRunConfig +impl ToSexp for GenericRunConfig where Head: Display, Leaf: Display, @@ -842,23 +861,22 @@ where } } -pub type FunctionDecl = GenericFunctionDecl; -pub(crate) type ResolvedFunctionDecl = GenericFunctionDecl; +pub type FunctionDecl = GenericFunctionDecl; +pub(crate) type ResolvedFunctionDecl = GenericFunctionDecl; /// Represents the declaration of a function /// directly parsed from source syntax. #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub struct GenericFunctionDecl +pub struct GenericFunctionDecl where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { pub name: Symbol, pub schema: Schema, - pub default: Option>, - pub merge: Option>, - pub merge_action: GenericActions, + pub default: Option>, + pub merge: Option>, + pub merge_action: GenericActions, pub cost: Option, pub unextractable: bool, /// Globals are desugared to functions, with this flag set to true. @@ -915,7 +933,7 @@ impl FunctionDecl { }, merge: None, merge_action: Actions::default(), - default: Some(Expr::Lit((), Literal::Unit)), + default: Some(Expr::Lit(DUMMY_SPAN.clone(), Literal::Unit)), cost: None, unextractable: false, ignore_viz: false, @@ -923,16 +941,15 @@ impl FunctionDecl { } } -impl GenericFunctionDecl +impl GenericFunctionDecl where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { pub fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, - ) -> GenericFunctionDecl { + f: &mut impl FnMut(GenericExpr) -> GenericExpr, + ) -> GenericFunctionDecl { GenericFunctionDecl { name: self.name, schema: self.schema, @@ -946,9 +963,8 @@ where } } -impl ToSexp for GenericFunctionDecl +impl ToSexp for GenericFunctionDecl where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -996,9 +1012,9 @@ where } } -pub type Fact = GenericFact; -pub(crate) type ResolvedFact = GenericFact; -pub(crate) type MappedFact = GenericFact, Leaf, Ann>; +pub type Fact = GenericFact; +pub(crate) type ResolvedFact = GenericFact; +pub(crate) type MappedFact = GenericFact, Leaf>; /// Facts are the left-hand side of a [`Command::Rule`]. /// They represent a part of a database query. @@ -1011,17 +1027,16 @@ pub(crate) type MappedFact = GenericFact { +pub enum GenericFact { /// Must be at least two things in an eq fact - Eq(Vec>), - Fact(GenericExpr), + Eq(Span, Vec>), + Fact(GenericExpr), } -pub struct Facts(pub Vec>); +pub struct Facts(pub Vec>); -impl Facts +impl Facts where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { @@ -1036,10 +1051,7 @@ where &self, typeinfo: &TypeInfo, fresh_gen: &mut impl FreshGen, - ) -> ( - Query, Leaf>, - Vec>, - ) + ) -> (Query, Leaf>, Vec>) where Leaf: SymbolLike, { @@ -1048,7 +1060,7 @@ where for fact in self.0.iter() { match fact { - GenericFact::Eq(exprs) => { + GenericFact::Eq(span, exprs) => { let mut new_exprs = vec![]; let mut to_equate = vec![]; for expr in exprs { @@ -1058,10 +1070,11 @@ where new_exprs.push(expr); } atoms.push(GenericAtom { + span: span.clone(), head: HeadOrEq::Eq, args: to_equate, }); - new_body.push(GenericFact::Eq(new_exprs)); + new_body.push(GenericFact::Eq(span.clone(), new_exprs)); } GenericFact::Fact(expr) => { let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen); @@ -1074,73 +1087,76 @@ where } } -impl ToSexp for GenericFact +impl ToSexp for GenericFact where Head: Display, Leaf: Display, { fn to_sexp(&self) -> Sexp { match self { - GenericFact::Eq(exprs) => list!("=", ++ exprs), + GenericFact::Eq(_, exprs) => list!("=", ++ exprs), GenericFact::Fact(expr) => expr.to_sexp(), } } } -impl GenericFact +impl GenericFact where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { pub(crate) fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, - ) -> GenericFact { + f: &mut impl FnMut(GenericExpr) -> GenericExpr, + ) -> GenericFact { match self { - GenericFact::Eq(exprs) => { - GenericFact::Eq(exprs.into_iter().map(|expr| expr.visit_exprs(f)).collect()) - } + GenericFact::Eq(span, exprs) => GenericFact::Eq( + span, + exprs.into_iter().map(|expr| expr.visit_exprs(f)).collect(), + ), GenericFact::Fact(expr) => GenericFact::Fact(expr.visit_exprs(f)), } } pub(crate) fn map_exprs( &self, - f: &mut impl FnMut(&GenericExpr) -> GenericExpr, - ) -> GenericFact { + f: &mut impl FnMut(&GenericExpr) -> GenericExpr, + ) -> GenericFact { match self { - GenericFact::Eq(exprs) => GenericFact::Eq(exprs.iter().map(f).collect()), + GenericFact::Eq(span, exprs) => { + GenericFact::Eq(span.clone(), exprs.iter().map(f).collect()) + } GenericFact::Fact(expr) => GenericFact::Fact(f(expr)), } } pub(crate) fn subst( &self, - subst_leaf: &mut impl FnMut(&Leaf) -> GenericExpr, + subst_leaf: &mut impl FnMut(&Span, &Leaf) -> GenericExpr, subst_head: &mut impl FnMut(&Head) -> Head2, - ) -> GenericFact { + ) -> GenericFact { self.map_exprs(&mut |e| e.subst(subst_leaf, subst_head)) } } -impl GenericFact +impl GenericFact where Leaf: Clone + PartialEq + Eq + Display + Hash, Head: Clone + Display, { - pub(crate) fn make_unresolved(self) -> Fact + pub(crate) fn make_unresolved(self) -> GenericFact where Leaf: SymbolLike, Head: SymbolLike, { - self.subst(&mut |v| Expr::Var((), v.to_symbol()), &mut |h| { - h.to_symbol() - }) + self.subst( + &mut |span, v| GenericExpr::Var(span.clone(), v.to_symbol()), + &mut |h| h.to_symbol(), + ) } } -impl Display for GenericFact +impl Display for GenericFact where Head: Display, Leaf: Display, @@ -1191,32 +1207,31 @@ pub enum Change { Subsume, } -pub type Action = GenericAction; -pub(crate) type MappedAction = GenericAction, Symbol, ()>; -pub(crate) type ResolvedAction = GenericAction; +pub type Action = GenericAction; +pub(crate) type MappedAction = GenericAction, Symbol>; +pub(crate) type ResolvedAction = GenericAction; #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub enum GenericAction +pub enum GenericAction where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { /// Bind a variable to a particular datatype or primitive. /// At the top level (in a [`Command::Action`]), this defines a global variable. /// In a [`Command::Rule`], this defines a local variable in the actions. - Let(Ann, Leaf, GenericExpr), + Let(Span, Leaf, GenericExpr), /// `set` a function to a particular result. /// `set` should not be used on datatypes- /// instead, use `union`. Set( - Ann, + Span, Head, - Vec>, - GenericExpr, + Vec>, + GenericExpr, ), /// Delete or subsume (mark as hidden from future rewrites and unextractable) an entry from a function. - Change(Ann, Change, Head, Vec>), + Change(Span, Change, Head, Vec>), /// `union` two datatypes, making them equal /// in the implicit, global equality relation /// of egglog. @@ -1229,11 +1244,7 @@ where /// (extract (Num 1)); Extracts Num 1 /// (extract (Num 2)); Extracts Num 1 /// ``` - Union( - Ann, - GenericExpr, - GenericExpr, - ), + Union(Span, GenericExpr, GenericExpr), /// `extract` a datatype from the egraph, choosing /// the smallest representative. /// By default, each constructor costs 1 to extract @@ -1242,31 +1253,23 @@ where /// The second argument is the number of variants to /// extract, picking different terms in the /// same equivalence class. - Extract( - Ann, - GenericExpr, - GenericExpr, - ), - Panic(Ann, String), - Expr(Ann, GenericExpr), + Extract(Span, GenericExpr, GenericExpr), + Panic(Span, String), + Expr(Span, GenericExpr), // If(Expr, Action, Action), } #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub struct GenericActions< - Head: Clone + Display, - Leaf: Clone + PartialEq + Eq + Display + Hash, - Ann: Clone + Default, ->(pub Vec>); -pub type Actions = GenericActions; -pub(crate) type ResolvedActions = GenericActions; -pub(crate) type MappedActions = - GenericActions, Leaf, Ann>; - -impl Default for GenericActions +pub struct GenericActions( + pub Vec>, +); +pub type Actions = GenericActions; +pub(crate) type ResolvedActions = GenericActions; +pub(crate) type MappedActions = GenericActions, Leaf>; + +impl Default for GenericActions where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { @@ -1275,9 +1278,8 @@ where } } -impl GenericActions +impl GenericActions where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { @@ -1285,7 +1287,7 @@ where self.0.len() } - pub(crate) fn iter(&self) -> impl Iterator> { + pub(crate) fn iter(&self) -> impl Iterator> { self.0.iter() } @@ -1295,15 +1297,14 @@ where pub(crate) fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { Self(self.0.into_iter().map(|a| a.visit_exprs(f)).collect()) } } -impl ToSexp for GenericAction +impl ToSexp for GenericAction where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -1328,44 +1329,43 @@ where } } -impl GenericAction +impl GenericAction where Head: Clone + Display, Leaf: Clone + Eq + Display + Hash, - Ann: Clone + Default, { // Applys `f` to all expressions in the action. pub fn map_exprs( &self, - f: &mut impl FnMut(&GenericExpr) -> GenericExpr, + f: &mut impl FnMut(&GenericExpr) -> GenericExpr, ) -> Self { match self { - GenericAction::Let(ann, lhs, rhs) => { - GenericAction::Let(ann.clone(), lhs.clone(), f(rhs)) + GenericAction::Let(span, lhs, rhs) => { + GenericAction::Let(span.clone(), lhs.clone(), f(rhs)) } - GenericAction::Set(ann, lhs, args, rhs) => { + GenericAction::Set(span, lhs, args, rhs) => { let right = f(rhs); GenericAction::Set( - ann.clone(), + span.clone(), lhs.clone(), args.iter().map(f).collect(), right, ) } - GenericAction::Change(ann, change, lhs, args) => GenericAction::Change( - ann.clone(), + GenericAction::Change(span, change, lhs, args) => GenericAction::Change( + span.clone(), *change, lhs.clone(), args.iter().map(f).collect(), ), - GenericAction::Union(ann, lhs, rhs) => { - GenericAction::Union(ann.clone(), f(lhs), f(rhs)) + GenericAction::Union(span, lhs, rhs) => { + GenericAction::Union(span.clone(), f(lhs), f(rhs)) } - GenericAction::Extract(ann, expr, variants) => { - GenericAction::Extract(ann.clone(), f(expr), f(variants)) + GenericAction::Extract(span, expr, variants) => { + GenericAction::Extract(span.clone(), f(expr), f(variants)) } - GenericAction::Panic(ann, msg) => GenericAction::Panic(ann.clone(), msg.clone()), - GenericAction::Expr(ann, e) => GenericAction::Expr(ann.clone(), f(e)), + GenericAction::Panic(span, msg) => GenericAction::Panic(span.clone(), msg.clone()), + GenericAction::Expr(span, e) => GenericAction::Expr(span.clone(), f(e)), } } @@ -1373,86 +1373,85 @@ where /// bottom-up, collecting the results. pub fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { match self { - GenericAction::Let(ann, lhs, rhs) => { - GenericAction::Let(ann.clone(), lhs.clone(), rhs.visit_exprs(f)) + GenericAction::Let(span, lhs, rhs) => { + GenericAction::Let(span, lhs.clone(), rhs.visit_exprs(f)) } // TODO should we refactor `Set` so that we can map over Expr::Call(lhs, args)? // This seems more natural to oflatt // Currently, visit_exprs does not apply f to the first argument of Set. - GenericAction::Set(ann, lhs, args, rhs) => { + GenericAction::Set(span, lhs, args, rhs) => { let args = args.into_iter().map(|e| e.visit_exprs(f)).collect(); - GenericAction::Set(ann.clone(), lhs.clone(), args, rhs.visit_exprs(f)) + GenericAction::Set(span, lhs.clone(), args, rhs.visit_exprs(f)) } - GenericAction::Change(ann, change, lhs, args) => { + GenericAction::Change(span, change, lhs, args) => { let args = args.into_iter().map(|e| e.visit_exprs(f)).collect(); - GenericAction::Change(ann.clone(), change, lhs.clone(), args) + GenericAction::Change(span, change, lhs.clone(), args) } - GenericAction::Union(ann, lhs, rhs) => { - GenericAction::Union(ann.clone(), lhs.visit_exprs(f), rhs.visit_exprs(f)) + GenericAction::Union(span, lhs, rhs) => { + GenericAction::Union(span, lhs.visit_exprs(f), rhs.visit_exprs(f)) } - GenericAction::Extract(ann, expr, variants) => { - GenericAction::Extract(ann.clone(), expr.visit_exprs(f), variants.visit_exprs(f)) + GenericAction::Extract(span, expr, variants) => { + GenericAction::Extract(span, expr.visit_exprs(f), variants.visit_exprs(f)) } - GenericAction::Panic(ann, msg) => GenericAction::Panic(ann.clone(), msg.clone()), - GenericAction::Expr(ann, e) => GenericAction::Expr(ann.clone(), e.visit_exprs(f)), + GenericAction::Panic(span, msg) => GenericAction::Panic(span, msg.clone()), + GenericAction::Expr(span, e) => GenericAction::Expr(span, e.visit_exprs(f)), } } - pub fn subst(&self, subst: &mut impl FnMut(&Leaf) -> GenericExpr) -> Self { + pub fn subst(&self, subst: &mut impl FnMut(&Span, &Leaf) -> GenericExpr) -> Self { self.map_exprs(&mut |e| e.subst_leaf(subst)) } pub fn map_def_use(self, fvar: &mut impl FnMut(Leaf, bool) -> Leaf) -> Self { macro_rules! fvar_expr { () => { - |s: _| GenericExpr::Var(Ann::default(), fvar(s.clone(), false)) + |span, s: _| GenericExpr::Var(span.clone(), fvar(s.clone(), false)) }; } match self { - GenericAction::Let(ann, lhs, rhs) => { + GenericAction::Let(span, lhs, rhs) => { let lhs = fvar(lhs, true); let rhs = rhs.subst_leaf(&mut fvar_expr!()); - GenericAction::Let(ann.clone(), lhs, rhs) + GenericAction::Let(span, lhs, rhs) } - GenericAction::Set(ann, lhs, args, rhs) => { + GenericAction::Set(span, lhs, args, rhs) => { let args = args .into_iter() .map(|e| e.subst_leaf(&mut fvar_expr!())) .collect(); let rhs = rhs.subst_leaf(&mut fvar_expr!()); - GenericAction::Set(ann.clone(), lhs.clone(), args, rhs) + GenericAction::Set(span, lhs.clone(), args, rhs) } - GenericAction::Change(ann, change, lhs, args) => { + GenericAction::Change(span, change, lhs, args) => { let args = args .into_iter() .map(|e| e.subst_leaf(&mut fvar_expr!())) .collect(); - GenericAction::Change(ann.clone(), change, lhs.clone(), args) + GenericAction::Change(span, change, lhs.clone(), args) } - GenericAction::Union(ann, lhs, rhs) => { + GenericAction::Union(span, lhs, rhs) => { let lhs = lhs.subst_leaf(&mut fvar_expr!()); let rhs = rhs.subst_leaf(&mut fvar_expr!()); - GenericAction::Union(ann.clone(), lhs, rhs) + GenericAction::Union(span, lhs, rhs) } - GenericAction::Extract(ann, expr, variants) => { + GenericAction::Extract(span, expr, variants) => { let expr = expr.subst_leaf(&mut fvar_expr!()); let variants = variants.subst_leaf(&mut fvar_expr!()); - GenericAction::Extract(ann.clone(), expr, variants) + GenericAction::Extract(span, expr, variants) } - GenericAction::Panic(ann, msg) => GenericAction::Panic(ann.clone(), msg.clone()), - GenericAction::Expr(ann, e) => { - GenericAction::Expr(ann.clone(), e.subst_leaf(&mut fvar_expr!())) + GenericAction::Panic(span, msg) => GenericAction::Panic(span, msg.clone()), + GenericAction::Expr(span, e) => { + GenericAction::Expr(span, e.subst_leaf(&mut fvar_expr!())) } } } } -impl Display for GenericAction +impl Display for GenericAction where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -1467,31 +1466,31 @@ pub(crate) struct CompiledRule { pub(crate) program: Program, } -pub type Rule = GenericRule; -pub(crate) type ResolvedRule = GenericRule; +pub type Rule = GenericRule; +pub(crate) type ResolvedRule = GenericRule; #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub struct GenericRule +pub struct GenericRule where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { - pub head: GenericActions, - pub body: Vec>, + pub span: Span, + pub head: GenericActions, + pub body: Vec>, } -impl GenericRule +impl GenericRule where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { pub(crate) fn visit_exprs( self, - f: &mut impl FnMut(GenericExpr) -> GenericExpr, + f: &mut impl FnMut(GenericExpr) -> GenericExpr, ) -> Self { Self { + span: self.span, head: self.head.visit_exprs(f), body: self .body @@ -1502,9 +1501,8 @@ where } } -impl GenericRule +impl GenericRule where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -1552,9 +1550,8 @@ where } } -impl GenericRule +impl GenericRule where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -1577,9 +1574,8 @@ where } } -impl Display for GenericRule +impl Display for GenericRule where - Ann: Clone + Default, Head: Clone + Display + ToSexp, Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp, { @@ -1588,16 +1584,17 @@ where } } -type Rewrite = GenericRewrite; +type Rewrite = GenericRewrite; #[derive(Clone, Debug)] -pub struct GenericRewrite { - pub lhs: GenericExpr, - pub rhs: GenericExpr, - pub conditions: Vec>, +pub struct GenericRewrite { + pub span: Span, + pub lhs: GenericExpr, + pub rhs: GenericExpr, + pub conditions: Vec>, } -impl GenericRewrite { +impl GenericRewrite { /// Converts the rewrite into an s-expression. pub fn to_sexp(&self, ruleset: Symbol, is_bidirectional: bool, subsume: bool) -> Sexp { let mut res = vec![ @@ -1628,15 +1625,14 @@ impl GenericRewrite { } } -impl Display for GenericRewrite { +impl Display for GenericRewrite { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{}", self.to_sexp("".into(), false, false)) } } -impl MappedExpr +impl MappedExpr where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { @@ -1648,29 +1644,29 @@ where // This is error-prone and the complexities can be avoided by treating globals // as nullary functions. match self { - GenericExpr::Var(_ann, v) => { + GenericExpr::Var(span, v) => { if typeinfo.is_global(v.to_symbol()) { - GenericAtomTerm::Global(v.clone()) + GenericAtomTerm::Global(span.clone(), v.clone()) } else { - GenericAtomTerm::Var(v.clone()) + GenericAtomTerm::Var(span.clone(), v.clone()) } } - GenericExpr::Lit(_ann, lit) => GenericAtomTerm::Literal(lit.clone()), - GenericExpr::Call(_ann, head, _) => GenericAtomTerm::Var(head.to.clone()), + GenericExpr::Lit(span, lit) => GenericAtomTerm::Literal(span.clone(), lit.clone()), + GenericExpr::Call(span, head, _) => GenericAtomTerm::Var(span.clone(), head.to.clone()), } } } -impl GenericActions +impl GenericActions where Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { - pub fn new(actions: Vec>) -> Self { + pub fn new(actions: Vec>) -> Self { Self(actions) } - pub fn singleton(action: GenericAction) -> Self { + pub fn singleton(action: GenericAction) -> Self { Self(vec![action]) } } diff --git a/src/ast/parse.lalrpop b/src/ast/parse.lalrpop index 31457aa8..4d55408a 100644 --- a/src/ast/parse.lalrpop +++ b/src/ast/parse.lalrpop @@ -1,10 +1,9 @@ -// TODO: span tracking use crate::ast::*; use crate::Symbol; use crate::Schedule; use ordered_float::OrderedFloat; -grammar; +grammar(srcfile: &Arc); extern { type Error = String; @@ -22,13 +21,13 @@ pub Program: Vec = { (Command)* => <> } -LParen: () = { - "(" => (), - "[" => (), +LParen: usize = { + <@L> "(" => <>, + <@L> "[" => <>, }; -RParen: () = { - ")" => (), - "]" => (), +RParen: usize = { + ")" <@R> => <>, + "]" <@R> => <>, }; List: Vec = { @@ -56,31 +55,39 @@ Command: Command = { )?> )?> RParen => { Command::Function(FunctionDecl { name, schema, merge, merge_action: Actions::new(merge_action.unwrap_or_default()), default, cost, unextractable: unextractable.is_some(), ignore_viz: false }) }, - LParen "declare" RParen => Command::Declare{name, sort}, + "declare" => Command::Declare{span: Span(srcfile.clone(), lo, hi), name, sort}, LParen "relation" > RParen => Command::Relation{constructor, inputs}, LParen "ruleset" RParen => Command::AddRuleset(name), LParen "unstable-combined-ruleset" RParen => Command::UnstableCombinedRuleset(name, subrulesets), - LParen "rule" > > )?> )?> RParen => Command::Rule{ruleset: ruleset.unwrap_or("".into()), name: name.unwrap_or("".to_string()).into(), rule: Rule { head: Actions::new(head), body }}, - LParen "rewrite" + "rule" > > + )?> + )?> + => Command::Rule{ruleset: ruleset.unwrap_or("".into()), name: name.unwrap_or("".to_string()).into(), rule: Rule { span: Span(srcfile.clone(), lo, hi), head: Actions::new(head), body }}, + "rewrite" >)?> )?> - RParen => Command::Rewrite(ruleset.unwrap_or("".into()), Rewrite { lhs, rhs, conditions: conditions.unwrap_or_default() }, subsume.is_some()), - LParen "birewrite" + => Command::Rewrite(ruleset.unwrap_or("".into()), Rewrite { span: Span(srcfile.clone(), lo, hi), lhs, rhs, conditions: conditions.unwrap_or_default() }, subsume.is_some()), + "birewrite" >)?> )?> - RParen => Command::BiRewrite(ruleset.unwrap_or("".into()), Rewrite { lhs, rhs, conditions: conditions.unwrap_or_default() }), - LParen "let" RParen => Command::Action(Action::Let((), name, expr)), + => Command::BiRewrite(ruleset.unwrap_or("".into()), Rewrite { span: Span(srcfile.clone(), lo, hi), lhs, rhs, conditions: conditions.unwrap_or_default() }), + "let" => Command::Action(Action::Let(Span(srcfile.clone(), lo, hi), name, expr)), => Command::Action(<>), - LParen "run" )?> RParen => Command::RunSchedule(Schedule::Repeat(limit, Box::new(Schedule::Run(RunConfig { ruleset : "".into(), until })))), - LParen "run" )?> RParen => Command::RunSchedule(Schedule::Repeat(limit, Box::new(Schedule::Run(RunConfig { ruleset, until })))), + "run" )?> => + Command::RunSchedule(Schedule::Repeat(Span(srcfile.clone(), lo, hi), limit, Box::new( + Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset : "".into(), until })))), + "run" )?> => + Command::RunSchedule(Schedule::Repeat(Span(srcfile.clone(), lo, hi), limit, Box::new( + Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset, until })))), LParen "simplify" RParen => Command::Simplify { expr, schedule }, - LParen "calc" LParen RParen RParen => Command::Calc(idents, exprs), + "calc" LParen RParen => Command::Calc(Span(srcfile.clone(), lo, hi), idents, exprs), LParen "query-extract" )?> RParen => Command::QueryExtract { expr, variants: variants.unwrap_or(0) }, - LParen "check" <(Fact)*> RParen => Command::Check(<>), + "check" => Command::Check(Span(srcfile.clone(), lo, hi), facts), LParen "check-proof" RParen => Command::CheckProof, - LParen "run-schedule" RParen => Command::RunSchedule(Schedule::Sequence(<>)), + "run-schedule" => + Command::RunSchedule(Schedule::Sequence(Span(srcfile.clone(), lo, hi), scheds)), LParen "print-stats" RParen => Command::PrintOverallStatistics, LParen "push" RParen => Command::Push(<>.unwrap_or(1)), LParen "pop" RParen => Command::Pop(<>.unwrap_or(1)), @@ -93,13 +100,20 @@ Command: Command = { } Schedule: Schedule = { - LParen "saturate" RParen => Schedule::Saturate(Box::new(Schedule::Sequence(<>))), - LParen "seq" RParen => Schedule::Sequence(<>), - LParen "repeat" RParen => Schedule::Repeat(limit, Box::new(Schedule::Sequence(scheds))), - LParen "run" )?> RParen => - Schedule::Run(RunConfig { ruleset: "".into(), until }), - LParen "run" )?> RParen => Schedule::Run(RunConfig { ruleset, until }), - => Schedule::Run(RunConfig { ruleset: ident, until: None }), + "saturate" => + Schedule::Saturate(Span(srcfile.clone(), lo, hi), Box::new( + Schedule::Sequence(Span(srcfile.clone(), lo, hi), scheds))), + "seq" => + Schedule::Sequence(Span(srcfile.clone(), lo, hi), scheds), + "repeat" => + Schedule::Repeat(Span(srcfile.clone(), lo, hi), limit, Box::new( + Schedule::Sequence(Span(srcfile.clone(), lo, hi), scheds))), + "run" )?> => + Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset: "".into(), until }), + "run" )?> => + Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset, until }), + => + Schedule::Run(Span(srcfile.clone(), lo, hi), RunConfig { ruleset: ident, until: None }), } Cost: Option = { @@ -108,27 +122,27 @@ Cost: Option = { } NonLetAction: Action = { - LParen "set" LParen RParen RParen => Action::Set ( (), f, args, v ), - LParen "delete" LParen RParen RParen => Action::Change ( (), Change::Delete, f, args), - LParen "subsume" LParen RParen RParen => Action::Change ( (), Change::Subsume, f, args), - LParen "union" RParen => Action::Union((), <>), - LParen "panic" RParen => Action::Panic((), msg), - LParen "extract" RParen => Action::Extract((), expr, Expr::Lit((), Literal::Int(0))), - LParen "extract" RParen => Action::Extract((), expr, variants), - => Action::Expr((), e), + "set" LParen RParen => Action::Set ( Span(srcfile.clone(), lo, hi), f, args, v ), + "delete" LParen RParen => Action::Change ( Span(srcfile.clone(), lo, hi), Change::Delete, f, args), + "subsume" LParen RParen => Action::Change ( Span(srcfile.clone(), lo, hi), Change::Subsume, f, args), + "union" => Action::Union(Span(srcfile.clone(), lo, hi), e1, e2), + "panic" => Action::Panic(Span(srcfile.clone(), lo, hi), msg), + "extract" => Action::Extract(Span(srcfile.clone(), lo, hi), expr, Expr::Lit(Span(srcfile.clone(), lo, hi), Literal::Int(0))), + "extract" => Action::Extract(Span(srcfile.clone(), lo, hi), expr, variants), + => Action::Expr(Span(srcfile.clone(), lo, hi), e), } pub Action: Action = { - LParen "let" RParen => Action::Let((), name, expr), + "let" => Action::Let(Span(srcfile.clone(), lo, hi), name, expr), => <>, } Name: Symbol = { "[" "]" => <> } pub Fact: Fact = { - LParen "=" RParen => { + "=" => { es.push(e); - Fact::Eq(es) + Fact::Eq(Span(srcfile.clone(), lo, hi), es) }, => Fact::Fact(<>), } @@ -138,8 +152,8 @@ Schema: Schema = { } pub Expr: Expr = { - => Expr::Lit((), <>), - => Expr::Var((), <>), + => Expr::Lit(Span(srcfile.clone(), lo, hi), lit), + => Expr::Var(Span(srcfile.clone(), lo, hi), id), => <>, }; @@ -157,7 +171,7 @@ Bool: bool = { } CallExpr: Expr = { - LParen RParen => Expr::Call((), head, tail), + => Expr::Call(Span(srcfile.clone(), lo, hi), head, tail), } ExprList: Vec = { LParen RParen => sexps } diff --git a/src/ast/remove_globals.rs b/src/ast/remove_globals.rs index 00814dea..eca727df 100644 --- a/src/ast/remove_globals.rs +++ b/src/ast/remove_globals.rs @@ -76,7 +76,7 @@ fn resolved_var_to_call(var: &ResolvedVar) -> ResolvedCall { fn replace_global_vars(expr: ResolvedExpr) -> ResolvedExpr { match expr.get_global_var() { Some(resolved_var) => { - GenericExpr::Call(expr.ann(), resolved_var_to_call(&resolved_var), vec![]) + GenericExpr::Call(expr.span(), resolved_var_to_call(&resolved_var), vec![]) } None => expr, } @@ -98,7 +98,7 @@ impl<'a> GlobalRemover<'a> { ) -> Vec { match cmd { GenericNCommand::CoreAction(action) => match action { - GenericAction::Let(ann, name, expr) => { + GenericAction::Let(span, name, expr) => { let ty = expr.output_type(type_info); let func_decl = ResolvedFunctionDecl { @@ -126,13 +126,13 @@ impl<'a> GlobalRemover<'a> { // output is eq-able, so generate a union if ty.is_eq_sort() { GenericNCommand::CoreAction(GenericAction::Union( - ann, - GenericExpr::Call(ann, resolved_call, vec![]), + span.clone(), + GenericExpr::Call(span, resolved_call, vec![]), remove_globals_expr(expr), )) } else { GenericNCommand::CoreAction(GenericAction::Set( - ann, + span, resolved_call, vec![], remove_globals_expr(expr), @@ -156,7 +156,7 @@ impl<'a> GlobalRemover<'a> { globals.insert( resolved_var.clone(), GenericExpr::Var( - (), + expr.span(), ResolvedVar { name: new_name, sort: resolved_var.sort.clone(), @@ -170,14 +170,18 @@ impl<'a> GlobalRemover<'a> { let new_facts: Vec = globals .iter() .map(|(old, new)| { - GenericFact::Eq(vec![ - GenericExpr::Call((), resolved_var_to_call(old), vec![]), - new.clone(), - ]) + GenericFact::Eq( + new.span(), + vec![ + GenericExpr::Call(new.span(), resolved_var_to_call(old), vec![]), + new.clone(), + ], + ) }) .collect(); let new_rule = GenericRule { + span: rule.span, // instrument the old facts and add the new facts to the end body: rule .body diff --git a/src/constraint.rs b/src/constraint.rs index f2aa4f2c..a29edf03 100644 --- a/src/constraint.rs +++ b/src/constraint.rs @@ -9,7 +9,7 @@ use crate::{ sort::I64Sort, typechecking::TypeError, util::{FreshGen, HashSet, SymbolGen}, - ArcSort, CorrespondingVar, Symbol, TypeInfo, + ArcSort, CorrespondingVar, Span, Symbol, TypeInfo, DUMMY_SPAN, }; use core::hash::Hash; // Use immutable hashmap for performance @@ -221,19 +221,20 @@ where impl Assignment { pub(crate) fn annotate_expr( &self, - expr: &GenericExpr, Symbol, ()>, + expr: &GenericExpr, Symbol>, typeinfo: &TypeInfo, ) -> ResolvedExpr { match &expr { - GenericExpr::Lit((), literal) => ResolvedExpr::Lit((), literal.clone()), - GenericExpr::Var((), var) => { + GenericExpr::Lit(span, literal) => ResolvedExpr::Lit(span.clone(), literal.clone()), + GenericExpr::Var(span, var) => { let global_ty = typeinfo.lookup_global(var); let ty = global_ty .clone() - .or_else(|| self.get(&AtomTerm::Var(*var)).cloned()) + // Span is ignored when looking up atom_terms + .or_else(|| self.get(&AtomTerm::Var(DUMMY_SPAN.clone(), *var)).cloned()) .expect("All variables should be assigned before annotation"); ResolvedExpr::Var( - (), + span.clone(), ResolvedVar { name: *var, sort: ty.clone(), @@ -242,7 +243,7 @@ impl Assignment { ) } GenericExpr::Call( - (), + span, CorrespondingVar { head, to: corresponding_var, @@ -258,24 +259,25 @@ impl Assignment { .iter() .map(|arg| arg.output_type(typeinfo)) .chain(once( - self.get(&AtomTerm::Var(*corresponding_var)) + self.get(&AtomTerm::Var(DUMMY_SPAN.clone(), *corresponding_var)) .unwrap() .clone(), )) .collect(); let resolved_call = ResolvedCall::from_resolution(head, &types, typeinfo); - GenericExpr::Call((), resolved_call, args) + GenericExpr::Call(span.clone(), resolved_call, args) } } } pub(crate) fn annotate_fact( &self, - facts: &GenericFact, Symbol, ()>, + facts: &GenericFact, Symbol>, typeinfo: &TypeInfo, ) -> ResolvedFact { match facts { - GenericFact::Eq(facts) => ResolvedFact::Eq( + GenericFact::Eq(span, facts) => ResolvedFact::Eq( + span.clone(), facts .iter() .map(|expr| self.annotate_expr(expr, typeinfo)) @@ -287,7 +289,7 @@ impl Assignment { pub(crate) fn annotate_facts( &self, - mapped_facts: &[GenericFact, Symbol, ()>], + mapped_facts: &[GenericFact, Symbol>], typeinfo: &TypeInfo, ) -> Vec { mapped_facts @@ -302,12 +304,12 @@ impl Assignment { typeinfo: &TypeInfo, ) -> Result { match action { - GenericAction::Let((), var, expr) => { + GenericAction::Let(span, var, expr) => { let ty = self - .get(&AtomTerm::Var(*var)) + .get(&AtomTerm::Var(span.clone(), *var)) .expect("All variables should be assigned before annotation"); Ok(ResolvedAction::Let( - (), + span.clone(), ResolvedVar { name: *var, sort: ty.clone(), @@ -318,7 +320,7 @@ impl Assignment { } // Note mapped_var for set is a dummy variable that does not mean anything GenericAction::Set( - (), + span, CorrespondingVar { head, to: _mapped_var, @@ -340,11 +342,16 @@ impl Assignment { if !matches!(resolved_call, ResolvedCall::Func(_)) { return Err(TypeError::UnboundFunction(*head)); } - Ok(ResolvedAction::Set((), resolved_call, children, rhs)) + Ok(ResolvedAction::Set( + span.clone(), + resolved_call, + children, + rhs, + )) } // Note mapped_var for delete is a dummy variable that does not mean anything GenericAction::Change( - (), + span, change, CorrespondingVar { head, @@ -364,32 +371,33 @@ impl Assignment { ResolvedCall::from_resolution_func_types(head, &types, typeinfo) .ok_or_else(|| TypeError::UnboundFunction(*head))?; Ok(ResolvedAction::Change( - (), + span.clone(), *change, resolved_call, children.clone(), )) } - GenericAction::Union((), lhs, rhs) => Ok(ResolvedAction::Union( - (), + GenericAction::Union(span, lhs, rhs) => Ok(ResolvedAction::Union( + span.clone(), self.annotate_expr(lhs, typeinfo), self.annotate_expr(rhs, typeinfo), )), - GenericAction::Extract((), lhs, rhs) => Ok(ResolvedAction::Extract( - (), + GenericAction::Extract(span, lhs, rhs) => Ok(ResolvedAction::Extract( + span.clone(), self.annotate_expr(lhs, typeinfo), self.annotate_expr(rhs, typeinfo), )), - GenericAction::Panic((), msg) => Ok(ResolvedAction::Panic((), msg.clone())), - GenericAction::Expr((), expr) => { - Ok(ResolvedAction::Expr((), self.annotate_expr(expr, typeinfo))) - } + GenericAction::Panic(span, msg) => Ok(ResolvedAction::Panic(span.clone(), msg.clone())), + GenericAction::Expr(span, expr) => Ok(ResolvedAction::Expr( + span.clone(), + self.annotate_expr(expr, typeinfo), + )), } } pub(crate) fn annotate_actions( &self, - mapped_actions: &GenericActions, Symbol, ()>, + mapped_actions: &GenericActions, Symbol>, typeinfo: &TypeInfo, ) -> Result { let actions = mapped_actions @@ -455,11 +463,11 @@ impl Problem { // bound vars are added to range match action { - CoreAction::Let(var, _, _) => { - self.range.insert(AtomTerm::Var(*var)); + CoreAction::Let(span, var, _, _) => { + self.range.insert(AtomTerm::Var(span.clone(), *var)); } - CoreAction::LetAtomTerm(v, _) => { - self.range.insert(AtomTerm::Var(*v)); + CoreAction::LetAtomTerm(span, v, _) => { + self.range.insert(AtomTerm::Var(span.clone(), *v)); } _ => (), } @@ -472,7 +480,11 @@ impl Problem { rule: &CoreRule, typeinfo: &TypeInfo, ) -> Result<(), TypeError> { - let CoreRule { head, body } = rule; + let CoreRule { + span: _, + head, + body, + } = rule; self.add_query(body, typeinfo)?; self.add_actions(head, typeinfo)?; Ok(()) @@ -481,10 +493,11 @@ impl Problem { pub(crate) fn assign_local_var_type( &mut self, var: Symbol, + span: Span, sort: ArcSort, ) -> Result<(), TypeError> { - self.add_binding(AtomTerm::Var(var), sort); - self.range.insert(AtomTerm::Var(var)); + self.add_binding(AtomTerm::Var(span.clone(), var), sort); + self.range.insert(AtomTerm::Var(span, var)); Ok(()) } } @@ -496,39 +509,43 @@ impl CoreAction { symbol_gen: &mut SymbolGen, ) -> Result>, TypeError> { match self { - CoreAction::Let(symbol, f, args) => { + CoreAction::Let(span, symbol, f, args) => { let mut args = args.clone(); - args.push(AtomTerm::Var(*symbol)); + args.push(AtomTerm::Var(span.clone(), *symbol)); Ok(get_literal_and_global_constraints(&args, typeinfo) - .chain(get_atom_application_constraints(f, &args, typeinfo)?) + .chain(get_atom_application_constraints(f, &args, span, typeinfo)?) .collect()) } - CoreAction::Set(head, args, rhs) => { + CoreAction::Set(span, head, args, rhs) => { let mut args = args.clone(); args.push(rhs.clone()); Ok(get_literal_and_global_constraints(&args, typeinfo) - .chain(get_atom_application_constraints(head, &args, typeinfo)?) + .chain(get_atom_application_constraints( + head, &args, span, typeinfo, + )?) .collect()) } - CoreAction::Change(_change, head, args) => { + CoreAction::Change(span, _change, head, args) => { let mut args = args.clone(); // Add a dummy last output argument let var = symbol_gen.fresh(head); - args.push(AtomTerm::Var(var)); + args.push(AtomTerm::Var(span.clone(), var)); Ok(get_literal_and_global_constraints(&args, typeinfo) - .chain(get_atom_application_constraints(head, &args, typeinfo)?) + .chain(get_atom_application_constraints( + head, &args, span, typeinfo, + )?) .collect()) } - CoreAction::Union(lhs, rhs) => Ok(get_literal_and_global_constraints( + CoreAction::Union(_ann, lhs, rhs) => Ok(get_literal_and_global_constraints( &[lhs.clone(), rhs.clone()], typeinfo, ) .chain(once(Constraint::Eq(lhs.clone(), rhs.clone()))) .collect()), - CoreAction::Extract(e, n) => { + CoreAction::Extract(_ann, e, n) => { // e can be anything Ok( get_literal_and_global_constraints(&[e.clone(), n.clone()], typeinfo) @@ -539,10 +556,13 @@ impl CoreAction { .collect(), ) } - CoreAction::Panic(_) => Ok(vec![]), - CoreAction::LetAtomTerm(v, at) => { + CoreAction::Panic(_ann, _) => Ok(vec![]), + CoreAction::LetAtomTerm(span, v, at) => { Ok(get_literal_and_global_constraints(&[at.clone()], typeinfo) - .chain(once(Constraint::Eq(AtomTerm::Var(*v), at.clone()))) + .chain(once(Constraint::Eq( + AtomTerm::Var(span.clone(), *v), + at.clone(), + ))) .collect()) } } @@ -568,7 +588,7 @@ impl Atom { } SymbolOrEq::Symbol(head) => Ok(literal_constraints .chain(get_atom_application_constraints( - head, &self.args, type_info, + head, &self.args, &self.span, type_info, )?) .collect()), } @@ -578,6 +598,7 @@ impl Atom { fn get_atom_application_constraints( head: &Symbol, args: &[AtomTerm], + span: &Span, type_info: &TypeInfo, ) -> Result>, TypeError> { // An atom can have potentially different semantics due to polymorphism @@ -596,6 +617,7 @@ fn get_atom_application_constraints( constraints.push(Constraint::Impossible( ImpossibleConstraint::ArityMismatch { atom: Atom { + span: span.clone(), head: *head, args: args.to_vec(), }, @@ -620,7 +642,7 @@ fn get_atom_application_constraints( // primitive atom constraints if let Some(primitives) = type_info.primitives.get(head) { for p in primitives { - let constraints = p.get_type_constraints().get(args); + let constraints = p.get_type_constraints(span).get(args); xor_constraints.push(constraints); } } @@ -642,13 +664,13 @@ fn get_literal_and_global_constraints<'a>( ) -> impl Iterator> + 'a { args.iter().filter_map(|arg| { match arg { - AtomTerm::Var(_) => None, + AtomTerm::Var(_, _) => None, // Literal to type constraint - AtomTerm::Literal(lit) => { + AtomTerm::Literal(_, lit) => { let typ = type_info.infer_literal(lit); Some(Constraint::Assign(arg.clone(), typ.clone())) } - AtomTerm::Global(v) => { + AtomTerm::Global(_, v) => { if let Some(typ) = type_info.lookup_global(v) { Some(Constraint::Assign(arg.clone(), typ.clone())) } else { @@ -667,11 +689,12 @@ pub trait TypeConstraint { pub struct SimpleTypeConstraint { name: Symbol, sorts: Vec, + span: Span, } impl SimpleTypeConstraint { - pub fn new(name: Symbol, sorts: Vec) -> SimpleTypeConstraint { - SimpleTypeConstraint { name, sorts } + pub fn new(name: Symbol, sorts: Vec, span: Span) -> SimpleTypeConstraint { + SimpleTypeConstraint { name, sorts, span } } pub fn into_box(self) -> Box { @@ -685,6 +708,7 @@ impl TypeConstraint for SimpleTypeConstraint { vec![Constraint::Impossible( ImpossibleConstraint::ArityMismatch { atom: Atom { + span: self.span.clone(), head: self.name, args: arguments.to_vec(), }, @@ -709,15 +733,17 @@ pub struct AllEqualTypeConstraint { sort: Option, exact_length: Option, output: Option, + span: Span, } impl AllEqualTypeConstraint { - pub fn new(name: Symbol) -> AllEqualTypeConstraint { + pub fn new(name: Symbol, span: Span) -> AllEqualTypeConstraint { AllEqualTypeConstraint { name, sort: None, exact_length: None, output: None, + span, } } @@ -758,6 +784,7 @@ impl TypeConstraint for AllEqualTypeConstraint { return vec![Constraint::Impossible( ImpossibleConstraint::ArityMismatch { atom: Atom { + span: self.span.clone(), head: self.name, args: arguments.to_vec(), }, diff --git a/src/core.rs b/src/core.rs index 15e97de0..c64dc2b3 100644 --- a/src/core.rs +++ b/src/core.rs @@ -10,6 +10,7 @@ //! GJ compiler further compiler core queries to gj's CompiledQueries //! //! Most compiler-time optimizations are expected to be done over CoreRule format. +use std::hash::Hasher; use std::ops::AddAssign; use crate::HashMap; @@ -128,22 +129,62 @@ impl ToSexp for ResolvedCall { } } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone)] pub enum GenericAtomTerm { - Var(Leaf), - Literal(Literal), - Global(Leaf), + Var(Span, Leaf), + Literal(Span, Literal), + Global(Span, Leaf), +} + +// Ignores annotations for equality and hasing +impl PartialEq for GenericAtomTerm +where + Leaf: PartialEq, +{ + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (GenericAtomTerm::Var(_, v1), GenericAtomTerm::Var(_, v2)) => v1 == v2, + (GenericAtomTerm::Literal(_, l1), GenericAtomTerm::Literal(_, l2)) => l1 == l2, + (GenericAtomTerm::Global(_, g1), GenericAtomTerm::Global(_, g2)) => g1 == g2, + _ => false, + } + } +} + +impl Eq for GenericAtomTerm where Leaf: Eq {} + +impl Hash for GenericAtomTerm +where + Leaf: Hash, +{ + fn hash(&self, state: &mut H) { + match self { + GenericAtomTerm::Var(_, v) => v.hash(state), + GenericAtomTerm::Literal(_, l) => l.hash(state), + GenericAtomTerm::Global(_, g) => g.hash(state), + } + } } pub type AtomTerm = GenericAtomTerm; pub type ResolvedAtomTerm = GenericAtomTerm; -impl AtomTerm { - pub fn to_expr(&self) -> Expr { +impl GenericAtomTerm { + pub fn span(&self) -> &Span { match self { - AtomTerm::Var(v) => Expr::Var((), *v), - AtomTerm::Literal(l) => Expr::Lit((), l.clone()), - AtomTerm::Global(v) => Expr::Var((), *v), + GenericAtomTerm::Var(span, _) => span, + GenericAtomTerm::Literal(span, _) => span, + GenericAtomTerm::Global(span, _) => span, + } + } +} + +impl GenericAtomTerm { + pub fn to_expr(&self) -> GenericExpr { + match self { + GenericAtomTerm::Var(span, v) => GenericExpr::Var(span.clone(), v.clone()), + GenericAtomTerm::Literal(span, l) => GenericExpr::Lit(span.clone(), l.clone()), + GenericAtomTerm::Global(span, v) => GenericExpr::Var(span.clone(), v.clone()), } } } @@ -151,9 +192,9 @@ impl AtomTerm { impl ResolvedAtomTerm { pub fn output(&self, typeinfo: &TypeInfo) -> ArcSort { match self { - ResolvedAtomTerm::Var(v) => v.sort.clone(), - ResolvedAtomTerm::Literal(l) => typeinfo.infer_literal(l), - ResolvedAtomTerm::Global(v) => v.sort.clone(), + ResolvedAtomTerm::Var(_, v) => v.sort.clone(), + ResolvedAtomTerm::Literal(_, l) => typeinfo.infer_literal(l), + ResolvedAtomTerm::Global(_, v) => v.sort.clone(), } } } @@ -161,15 +202,16 @@ impl ResolvedAtomTerm { impl std::fmt::Display for AtomTerm { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - AtomTerm::Var(v) => write!(f, "{v}"), - AtomTerm::Literal(lit) => write!(f, "{lit}"), - AtomTerm::Global(g) => write!(f, "{g}"), + AtomTerm::Var(_, v) => write!(f, "{v}"), + AtomTerm::Literal(_, lit) => write!(f, "{lit}"), + AtomTerm::Global(_, g) => write!(f, "{g}"), } } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct GenericAtom { + pub span: Span, pub head: Head, pub args: Vec>, } @@ -189,22 +231,22 @@ where { pub fn vars(&self) -> impl Iterator + '_ { self.args.iter().filter_map(|t| match t { - GenericAtomTerm::Var(v) => Some(v.clone()), - GenericAtomTerm::Literal(_) => None, - GenericAtomTerm::Global(_) => None, + GenericAtomTerm::Var(_, v) => Some(v.clone()), + GenericAtomTerm::Literal(..) => None, + GenericAtomTerm::Global(..) => None, }) } fn subst(&mut self, subst: &HashMap>) { for arg in self.args.iter_mut() { match arg { - GenericAtomTerm::Var(v) => { + GenericAtomTerm::Var(_, v) => { if let Some(at) = subst.get(v) { *arg = at.clone(); } } - GenericAtomTerm::Literal(_) => (), - GenericAtomTerm::Global(_) => (), + GenericAtomTerm::Literal(..) => (), + GenericAtomTerm::Global(..) => (), } } } @@ -213,7 +255,7 @@ impl Atom { pub(crate) fn to_expr(&self) -> Expr { let n = self.args.len(); Expr::Call( - (), + self.span.clone(), self.head, self.args[0..n - 1] .iter() @@ -310,6 +352,7 @@ impl Query { self.atoms.iter().filter_map(|atom| match &atom.head { ResolvedCall::Func(_) => None, ResolvedCall::Primitive(head) => Some(GenericAtom { + span: atom.span.clone(), head: head.primitive.clone(), args: atom.args.clone(), }), @@ -319,6 +362,7 @@ impl Query { pub fn funcs(&self) -> impl Iterator> + '_ { self.atoms.iter().filter_map(|atom| match &atom.head { ResolvedCall::Func(head) => Some(GenericAtom { + span: atom.span.clone(), head: head.name, args: atom.args.clone(), }), @@ -329,13 +373,18 @@ impl Query { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum GenericCoreAction { - Let(Leaf, Head, Vec>), - LetAtomTerm(Leaf, GenericAtomTerm), - Extract(GenericAtomTerm, GenericAtomTerm), - Set(Head, Vec>, GenericAtomTerm), - Change(Change, Head, Vec>), - Union(GenericAtomTerm, GenericAtomTerm), - Panic(String), + Let(Span, Leaf, Head, Vec>), + LetAtomTerm(Span, Leaf, GenericAtomTerm), + Extract(Span, GenericAtomTerm, GenericAtomTerm), + Set( + Span, + Head, + Vec>, + GenericAtomTerm, + ), + Change(Span, Change, Head, Vec>), + Union(Span, GenericAtomTerm, GenericAtomTerm), + Panic(Span, String), } pub type CoreAction = GenericCoreAction; @@ -356,7 +405,11 @@ where { pub(crate) fn subst(&mut self, subst: &HashMap>) { let actions = subst.iter().map(|(symbol, atom_term)| { - GenericCoreAction::LetAtomTerm(symbol.clone(), atom_term.clone()) + GenericCoreAction::LetAtomTerm( + atom_term.span().clone(), + symbol.clone(), + atom_term.clone(), + ) }); let existing_actions = std::mem::take(&mut self.0); self.0 = actions.chain(existing_actions).collect(); @@ -368,7 +421,7 @@ where } #[allow(clippy::type_complexity)] -impl GenericActions +impl GenericActions where Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, @@ -378,25 +431,19 @@ where typeinfo: &TypeInfo, binding: &mut IndexSet, fresh_gen: &mut FG, - ) -> Result< - ( - GenericCoreActions, - MappedActions, - ), - TypeError, - > + ) -> Result<(GenericCoreActions, MappedActions), TypeError> where Leaf: SymbolLike, { let mut norm_actions = vec![]; - let mut mapped_actions: MappedActions = GenericActions(vec![]); + let mut mapped_actions: MappedActions = GenericActions(vec![]); // During the lowering, there are two important guaratees: // Every used variable should be bound. // Every introduced variable should be unbound before. for action in self.0.iter() { match action { - GenericAction::Let(_ann, var, expr) => { + GenericAction::Let(span, var, expr) => { if binding.contains(var) { return Err(TypeError::AlreadyDefined(var.to_symbol())); } @@ -404,15 +451,18 @@ where expr.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions.0); norm_actions.push(GenericCoreAction::LetAtomTerm( + span.clone(), var.clone(), mapped_expr.get_corresponding_var_or_lit(typeinfo), )); - mapped_actions - .0 - .push(GenericAction::Let((), var.clone(), mapped_expr)); + mapped_actions.0.push(GenericAction::Let( + span.clone(), + var.clone(), + mapped_expr, + )); binding.insert(var.clone()); } - GenericAction::Set(_ann, head, args, expr) => { + GenericAction::Set(span, head, args, expr) => { let mut mapped_args = vec![]; for arg in args { let (actions, mapped_arg) = @@ -424,6 +474,7 @@ where expr.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions.0); norm_actions.push(GenericCoreAction::Set( + span.clone(), head.clone(), mapped_args .iter() @@ -433,13 +484,13 @@ where )); let v = fresh_gen.fresh(head); mapped_actions.0.push(GenericAction::Set( - (), + span.clone(), CorrespondingVar::new(head.clone(), v), mapped_args, mapped_expr, )); } - GenericAction::Change(_ann, change, head, args) => { + GenericAction::Change(span, change, head, args) => { let mut mapped_args = vec![]; for arg in args { let (actions, mapped_arg) = @@ -448,6 +499,7 @@ where mapped_args.push(mapped_arg); } norm_actions.push(GenericCoreAction::Change( + span.clone(), *change, head.clone(), mapped_args @@ -457,49 +509,53 @@ where )); let v = fresh_gen.fresh(head); mapped_actions.0.push(GenericAction::Change( - (), + span.clone(), *change, CorrespondingVar::new(head.clone(), v), mapped_args, )); } - GenericAction::Union(_ann, e1, e2) => { + GenericAction::Union(span, e1, e2) => { let (actions1, mapped_e1) = e1.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions1.0); let (actions2, mapped_e2) = e2.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions2.0); norm_actions.push(GenericCoreAction::Union( + span.clone(), mapped_e1.get_corresponding_var_or_lit(typeinfo), mapped_e2.get_corresponding_var_or_lit(typeinfo), )); mapped_actions .0 - .push(GenericAction::Union((), mapped_e1, mapped_e2)); + .push(GenericAction::Union(span.clone(), mapped_e1, mapped_e2)); } - GenericAction::Extract(_ann, e, n) => { + GenericAction::Extract(span, e, n) => { let (actions, mapped_e) = e.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions.0); let (actions, mapped_n) = n.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions.0); norm_actions.push(GenericCoreAction::Extract( + span.clone(), mapped_e.get_corresponding_var_or_lit(typeinfo), mapped_n.get_corresponding_var_or_lit(typeinfo), )); mapped_actions .0 - .push(GenericAction::Extract((), mapped_e, mapped_n)); + .push(GenericAction::Extract(span.clone(), mapped_e, mapped_n)); } - GenericAction::Panic(_ann, string) => { - norm_actions.push(GenericCoreAction::Panic(string.clone())); + GenericAction::Panic(span, string) => { + norm_actions.push(GenericCoreAction::Panic(span.clone(), string.clone())); mapped_actions .0 - .push(GenericAction::Panic((), string.clone())); + .push(GenericAction::Panic(span.clone(), string.clone())); } - GenericAction::Expr(_ann, expr) => { + GenericAction::Expr(span, expr) => { let (actions, mapped_expr) = expr.to_core_actions(typeinfo, binding, fresh_gen)?; norm_actions.extend(actions.0); - mapped_actions.0.push(GenericAction::Expr((), mapped_expr)); + mapped_actions + .0 + .push(GenericAction::Expr(span.clone(), mapped_expr)); } } } @@ -507,9 +563,8 @@ where } } -impl GenericExpr +impl GenericExpr where - Ann: Clone + Default, Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash, { @@ -519,15 +574,15 @@ where fresh_gen: &mut impl FreshGen, ) -> ( Vec, Leaf>>, - MappedExpr, + MappedExpr, ) where Leaf: SymbolLike, { match self { - GenericExpr::Lit(ann, lit) => (vec![], GenericExpr::Lit(ann.clone(), lit.clone())), - GenericExpr::Var(ann, v) => (vec![], GenericExpr::Var(ann.clone(), v.clone())), - GenericExpr::Call(ann, f, children) => { + GenericExpr::Lit(span, lit) => (vec![], GenericExpr::Lit(span.clone(), lit.clone())), + GenericExpr::Var(span, v) => (vec![], GenericExpr::Var(span.clone(), v.clone())), + GenericExpr::Call(span, f, children) => { let fresh = fresh_gen.fresh(f); let mut new_children = vec![]; let mut atoms = vec![]; @@ -540,17 +595,18 @@ where child_exprs.push(child_expr); } let args = { - new_children.push(GenericAtomTerm::Var(fresh.clone())); + new_children.push(GenericAtomTerm::Var(span.clone(), fresh.clone())); new_children }; atoms.push(GenericAtom { + span: span.clone(), head: HeadOrEq::Symbol(f.clone()), args, }); ( atoms, GenericExpr::Call( - ann.clone(), + span.clone(), CorrespondingVar::new(f.clone(), fresh), child_exprs, ), @@ -564,27 +620,27 @@ where typeinfo: &TypeInfo, binding: &mut IndexSet, fresh_gen: &mut FG, - ) -> Result<(GenericCoreActions, MappedExpr), TypeError> + ) -> Result<(GenericCoreActions, MappedExpr), TypeError> where Leaf: Hash + Eq + SymbolLike, { match self { - GenericExpr::Lit(_ann, lit) => Ok(( + GenericExpr::Lit(span, lit) => Ok(( GenericCoreActions::default(), - GenericExpr::Lit((), lit.clone()), + GenericExpr::Lit(span.clone(), lit.clone()), )), - GenericExpr::Var(_ann, v) => { + GenericExpr::Var(span, v) => { let sym = v.to_symbol(); if binding.contains(v) || typeinfo.is_global(sym) { Ok(( GenericCoreActions::default(), - GenericExpr::Var((), v.clone()), + GenericExpr::Var(span.clone(), v.clone()), )) } else { Err(TypeError::Unbound(sym)) } } - GenericExpr::Call(_ann, f, args) => { + GenericExpr::Call(span, f, args) => { let mut norm_actions = vec![]; let mut norm_args = vec![]; let mut mapped_args = vec![]; @@ -599,10 +655,19 @@ where let var = fresh_gen.fresh(f); binding.insert(var.clone()); - norm_actions.push(GenericCoreAction::Let(var.clone(), f.clone(), norm_args)); + norm_actions.push(GenericCoreAction::Let( + span.clone(), + var.clone(), + f.clone(), + norm_args, + )); Ok(( GenericCoreActions::new(norm_actions), - GenericExpr::Call((), CorrespondingVar::new(f.clone(), var), mapped_args), + GenericExpr::Call( + span.clone(), + CorrespondingVar::new(f.clone(), var), + mapped_args, + ), )) } } @@ -618,6 +683,7 @@ where /// constraints. #[derive(Debug, Clone)] pub struct GenericCoreRule { + pub span: Span, pub body: Query, pub head: GenericCoreActions, } @@ -659,7 +725,7 @@ where for atom in result_rule.body.atoms.iter() { if atom.head.is_eq() && atom.args[0] != atom.args[1] { match &atom.args[..] { - [GenericAtomTerm::Var(x), y] | [y, GenericAtomTerm::Var(x)] => { + [GenericAtomTerm::Var(_, x), y] | [y, GenericAtomTerm::Var(_, x)] => { to_subst = Some((x, y)); break; } @@ -683,11 +749,11 @@ where HeadOrEq::Eq => { assert_eq!(atom.args.len(), 2); match (&atom.args[0], &atom.args[1]) { - (GenericAtomTerm::Var(v1), GenericAtomTerm::Var(v2)) => { + (GenericAtomTerm::Var(_, v1), GenericAtomTerm::Var(_, v2)) => { assert_eq!(v1, v2); None } - (GenericAtomTerm::Var(_), _) | (_, GenericAtomTerm::Var(_)) => { + (GenericAtomTerm::Var(..), _) | (_, GenericAtomTerm::Var(..)) => { panic!("equalities between variable and non-variable arguments should have been canonicalized") } (at1, at2) => { @@ -695,11 +761,12 @@ where None } else { Some(GenericAtom { + span: atom.span.clone(), head: value_eq(&atom.args[0], &atom.args[1]), args: vec![ atom.args[0].clone(), atom.args[1].clone(), - GenericAtomTerm::Literal(Literal::Unit), + GenericAtomTerm::Literal(atom.span.clone(), Literal::Unit), ], }) } @@ -707,19 +774,21 @@ where } } HeadOrEq::Symbol(symbol) => Some(GenericAtom { + span: atom.span.clone(), head: symbol, args: atom.args, }), }) .collect(); GenericCoreRule { + span: result_rule.span, body: Query { atoms }, head: result_rule.head, } } } -impl GenericRule +impl GenericRule where Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash + Debug, @@ -732,13 +801,21 @@ where where Leaf: SymbolLike, { - let GenericRule { head, body } = self; + let GenericRule { + span: _, + head, + body, + } = self; let (body, _correspondence) = Facts(body.clone()).to_query(typeinfo, &mut fresh_gen); let mut binding = body.get_vars(); let (head, _correspondence) = head.to_core_actions(typeinfo, &mut binding, &mut fresh_gen)?; - Ok(GenericCoreRule { body, head }) + Ok(GenericCoreRule { + span: self.span.clone(), + body, + head, + }) } fn to_canonicalized_core_rule_impl( diff --git a/src/extract.rs b/src/extract.rs index c89a28b0..e895082b 100644 --- a/src/extract.rs +++ b/src/extract.rs @@ -28,13 +28,14 @@ impl EGraph { /// let mut egraph = EGraph::default(); /// egraph /// .parse_and_run_program( + /// None, /// "(datatype Op (Add i64 i64)) /// (let expr (Add 1 1))", /// ) /// .unwrap(); /// let mut termdag = TermDag::default(); /// let (sort, value) = egraph - /// .eval_expr(&egglog::ast::Expr::Var((), "expr".into())) + /// .eval_expr(&egglog::ast::Expr::var_no_span("expr")) /// .unwrap(); /// let (_, extracted) = egraph.extract(value, &mut termdag, &sort); /// assert_eq!(termdag.to_string(&extracted), "(Add 1 1)"); diff --git a/src/gj.rs b/src/gj.rs index 61661dd8..230d8b08 100644 --- a/src/gj.rs +++ b/src/gj.rs @@ -246,18 +246,18 @@ impl<'b> Context<'b> { let mut values: Vec = vec![]; for arg in args { values.push(match arg { - AtomTerm::Var(v) => { + AtomTerm::Var(_ann, v) => { let i = self.query.vars.get_index_of(v).unwrap(); self.tuple[i] } - AtomTerm::Literal(lit) => self.egraph.eval_lit(lit), - AtomTerm::Global(_g) => panic!("Globals should have been desugared"), + AtomTerm::Literal(_ann, lit) => self.egraph.eval_lit(lit), + AtomTerm::Global(_ann, _g) => panic!("Globals should have been desugared"), }) } if let Some(res) = prim.apply(&values, None) { match out { - AtomTerm::Var(v) => { + AtomTerm::Var(_ann, v) => { let i = self.query.vars.get_index_of(v).unwrap(); if *check { @@ -269,14 +269,14 @@ impl<'b> Context<'b> { self.tuple[i] = res; } - AtomTerm::Literal(lit) => { + AtomTerm::Literal(_ann, lit) => { assert!(check); let val = &self.egraph.eval_lit(lit); if val != &res { return Ok(()); } } - AtomTerm::Global(_g) => { + AtomTerm::Global(_ann, _g) => { panic!("Globals should have been desugared") } } @@ -362,11 +362,12 @@ impl EGraph { .into_iter() .map(|atom| { let args = atom.args.into_iter().map(|arg| match arg { - ResolvedAtomTerm::Var(v) => AtomTerm::Var(v.name), - ResolvedAtomTerm::Literal(lit) => AtomTerm::Literal(lit), - ResolvedAtomTerm::Global(g) => AtomTerm::Global(g.name), + ResolvedAtomTerm::Var(span, v) => AtomTerm::Var(span, v.name), + ResolvedAtomTerm::Literal(span, lit) => AtomTerm::Literal(span, lit), + ResolvedAtomTerm::Global(span, g) => AtomTerm::Global(span, g.name), }); Atom { + span: atom.span, head: atom.head, args: args.collect(), } @@ -389,14 +390,14 @@ impl EGraph { let mut constraints = vec![]; for (i, t) in atom.args.iter().enumerate() { match t { - AtomTerm::Literal(lit) => { + AtomTerm::Literal(_ann, lit) => { let val = self.eval_lit(lit); constraints.push(Constraint::Const(i, val)) } - AtomTerm::Global(_g) => { + AtomTerm::Global(_ann, _g) => { panic!("Globals should have been desugared") } - AtomTerm::Var(_v) => { + AtomTerm::Var(_ann, _v) => { if let Some(j) = atom.args[..i].iter().position(|t2| t == t2) { constraints.push(Constraint::Eq(j, i)); } @@ -423,7 +424,13 @@ impl EGraph { let column = atom .args .iter() - .position(|arg| arg == &AtomTerm::Var(var)) + .position(|arg| { + if let AtomTerm::Var(_, var2) = arg { + &var == var2 + } else { + false + } + }) .unwrap(); self.make_trie_access_for_column(atom, column, timestamp_range, include_subsumed) } @@ -448,12 +455,12 @@ impl EGraph { for (i, atom) in atoms.iter().enumerate() { for (col, arg) in atom.args.iter().enumerate() { match arg { - AtomTerm::Var(var) => vars.entry(*var).or_default().occurences.push(i), - AtomTerm::Literal(lit) => { + AtomTerm::Var(_ann, var) => vars.entry(*var).or_default().occurences.push(i), + AtomTerm::Literal(_ann, lit) => { let val = self.eval_lit(lit); constants.entry(i).or_default().push((col, val)); } - AtomTerm::Global(_g) => { + AtomTerm::Global(_ann, _g) => { panic!("Globals should have been desugared") } } @@ -568,24 +575,24 @@ impl EGraph { let next = extra.iter().position(|p| { assert!(!p.args.is_empty()); p.args[..p.args.len() - 1].iter().all(|a| match a { - AtomTerm::Var(v) => vars.contains_key(v), - AtomTerm::Literal(_) => true, - AtomTerm::Global(_) => true, + AtomTerm::Var(_ann, v) => vars.contains_key(v), + AtomTerm::Literal(_ann, _) => true, + AtomTerm::Global(_ann, _) => true, }) }); if let Some(i) = next { let p = extra.remove(i); let check = match p.args.last().unwrap() { - AtomTerm::Var(v) => match vars.entry(*v) { + AtomTerm::Var(_ann, v) => match vars.entry(*v) { Entry::Occupied(_) => true, Entry::Vacant(e) => { e.insert(Default::default()); false } }, - AtomTerm::Literal(_) => true, - AtomTerm::Global(_) => true, + AtomTerm::Literal(_ann, _) => true, + AtomTerm::Global(_ann, _) => true, }; program.push(Instr::Call { prim: p.head.clone(), @@ -623,24 +630,24 @@ impl EGraph { }; for a in args { - if let AtomTerm::Var(v) = a { + if let AtomTerm::Var(_ann, v) = a { let i = query.vars.get_index_of(v).unwrap(); assert!(tuple_valid[i]); } } match last { - AtomTerm::Var(v) => { + AtomTerm::Var(_ann, v) => { let i = query.vars.get_index_of(v).unwrap(); assert_eq!(*check, tuple_valid[i], "{instr}"); if !*check { tuple_valid[i] = true; } } - AtomTerm::Literal(_) => { + AtomTerm::Literal(_ann, _) => { assert!(*check); } - AtomTerm::Global(_) => { + AtomTerm::Global(_ann, _) => { assert!(*check); } } @@ -736,7 +743,7 @@ impl EGraph { if has_atoms { for atom in cq.query.funcs() { for arg in &atom.args { - if let AtomTerm::Global(_g) = arg { + if let AtomTerm::Global(_ann, _g) = arg { panic!("Globals should have been desugared") } } diff --git a/src/lib.rs b/src/lib.rs index 2a4b06a9..4ffebec5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -73,7 +73,9 @@ pub type Subst = IndexMap; pub trait PrimitiveLike { fn name(&self) -> Symbol; - fn get_type_constraints(&self) -> Box; + /// Constructs a type constraint for the primitive that uses the span information + /// for error localization. + fn get_type_constraints(&self, span: &Span) -> Box; fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option; } @@ -299,12 +301,12 @@ impl Primitive { fn accept(&self, tys: &[Arc]) -> bool { let mut constraints = vec![]; let lits: Vec<_> = (0..tys.len()) - .map(|i| AtomTerm::Literal(Literal::Int(i as i64))) + .map(|i| AtomTerm::Literal(DUMMY_SPAN.clone(), Literal::Int(i as i64))) .collect(); for (lit, ty) in lits.iter().zip(tys.iter()) { constraints.push(Constraint::Assign(lit.clone(), ty.clone())) } - constraints.extend(self.get_type_constraints().get(&lits)); + constraints.extend(self.get_type_constraints(&DUMMY_SPAN).get(&lits)); let problem = Problem { constraints, range: HashSet::default(), @@ -362,14 +364,14 @@ impl PrimitiveLike for SimplePrimitive { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { let sorts: Vec<_> = self .input .iter() .chain(once(&self.output as &ArcSort)) .cloned() .collect(); - SimpleTypeConstraint::new(self.name(), sorts).into_box() + SimpleTypeConstraint::new(self.name(), sorts, span.clone()).into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { (self.f)(values) @@ -482,7 +484,7 @@ impl Default for EGraph { #[derive(Debug, Error)] #[error("Not found: {0}")] -pub struct NotFoundError(Expr); +pub struct NotFoundError(String); /// For each rule, we produce a `SearchResult` /// storing data about that rule's matches. @@ -843,8 +845,8 @@ impl EGraph { // returns whether the egraph was updated fn run_schedule(&mut self, sched: &ResolvedSchedule) -> RunReport { match sched { - ResolvedSchedule::Run(config) => self.run_rules(config), - ResolvedSchedule::Repeat(limit, sched) => { + ResolvedSchedule::Run(span, config) => self.run_rules(span, config), + ResolvedSchedule::Repeat(_span, limit, sched) => { let mut report = RunReport::default(); for _i in 0..*limit { let rec = self.run_schedule(sched); @@ -855,7 +857,7 @@ impl EGraph { } report } - ResolvedSchedule::Saturate(sched) => { + ResolvedSchedule::Saturate(_span, sched) => { let mut report = RunReport::default(); loop { let rec = self.run_schedule(sched); @@ -866,7 +868,7 @@ impl EGraph { } report } - ResolvedSchedule::Sequence(scheds) => { + ResolvedSchedule::Sequence(_span, scheds) => { let mut report = RunReport::default(); for sched in scheds { report = report.union(&self.run_schedule(sched)); @@ -893,7 +895,7 @@ impl EGraph { termdag.to_string(&term) } - fn run_rules(&mut self, config: &ResolvedRunConfig) -> RunReport { + fn run_rules(&mut self, span: &Span, config: &ResolvedRunConfig) -> RunReport { let mut report: RunReport = Default::default(); // first rebuild @@ -908,7 +910,7 @@ impl EGraph { let GenericRunConfig { ruleset, until } = config; if let Some(facts) = until { - if self.check_facts(facts).is_ok() { + if self.check_facts(span, facts).is_ok() { log::info!( "Breaking early because of facts:\n {}!", ListDisplay(facts, "\n") @@ -1135,7 +1137,7 @@ impl EGraph { pub fn eval_expr(&mut self, expr: &Expr) -> Result<(ArcSort, Value), Error> { let fresh_name = self.desugar.get_fresh(); - let command = Command::Action(Action::Let((), fresh_name, expr.clone())); + let command = Command::Action(Action::Let(DUMMY_SPAN.clone(), fresh_name, expr.clone())); self.run_program(vec![command])?; // find the table with the same name as the fresh name let func = self.functions.get(&fresh_name).unwrap(); @@ -1209,8 +1211,9 @@ impl EGraph { } } - fn check_facts(&mut self, facts: &[ResolvedFact]) -> Result<(), Error> { + fn check_facts(&mut self, span: &Span, facts: &[ResolvedFact]) -> Result<(), Error> { let rule = ast::ResolvedRule { + span: span.clone(), head: ResolvedActions::default(), body: facts.to_vec(), }; @@ -1288,13 +1291,13 @@ impl EGraph { log::info!("Overall statistics:\n{}", self.overall_run_report); self.print_msg(format!("Overall statistics:\n{}", self.overall_run_report)); } - ResolvedNCommand::Check(facts) => { - self.check_facts(&facts)?; + ResolvedNCommand::Check(span, facts) => { + self.check_facts(&span, &facts)?; log::info!("Checked fact {:?}.", facts); } ResolvedNCommand::CheckProof => log::error!("TODO implement proofs"), ResolvedNCommand::CoreAction(action) => match &action { - ResolvedAction::Let((), name, contents) => { + ResolvedAction::Let(_, name, contents) => { panic!("Globals should have been desugared away: {name} = {contents}") } _ => { @@ -1385,6 +1388,7 @@ impl EGraph { let mut contents = String::new(); f.read_to_string(&mut contents).unwrap(); + let span: Span = DUMMY_SPAN.clone(); let mut actions: Vec = vec![]; let mut str_buf: Vec<&str> = vec![]; for line in contents.lines() { @@ -1396,10 +1400,10 @@ impl EGraph { let parse = |s: &str| -> Expr { match s.parse::() { - Ok(i) => Expr::Lit((), Literal::Int(i)), + Ok(i) => Expr::Lit(span.clone(), Literal::Int(i)), Err(_) => match s.parse::() { - Ok(f) => Expr::Lit((), Literal::F64(f.into())), - Err(_) => Expr::Lit((), Literal::String(s.into())), + Ok(f) => Expr::Lit(span.clone(), Literal::F64(f.into())), + Err(_) => Expr::Lit(span.clone(), Literal::String(s.into())), }, } }; @@ -1408,10 +1412,10 @@ impl EGraph { actions.push( if function_type.is_datatype || function_type.output.name() == UNIT_SYM.into() { - Action::Expr((), Expr::Call((), func_name, exprs)) + Action::Expr(span.clone(), Expr::Call(span.clone(), func_name, exprs)) } else { let out = exprs.pop().unwrap(); - Action::Set((), func_name, exprs, out) + Action::Set(span.clone(), func_name, exprs, out) }, ); } @@ -1482,12 +1486,20 @@ impl EGraph { Ok(self.flush_msgs()) } - pub fn parse_program(&self, input: &str) -> Result, Error> { - self.desugar.parse_program(input) + pub fn parse_program( + &self, + filename: Option, + input: &str, + ) -> Result, Error> { + self.desugar.parse_program(filename, input) } - pub fn parse_and_run_program(&mut self, input: &str) -> Result, Error> { - let parsed = self.desugar.parse_program(input)?; + pub fn parse_and_run_program( + &mut self, + filename: Option, + input: &str, + ) -> Result, Error> { + let parsed = self.desugar.parse_program(filename, input)?; self.run_program(parsed) } @@ -1611,7 +1623,7 @@ mod tests { use crate::{ constraint::SimpleTypeConstraint, sort::{FromSort, I64Sort, IntoSort, Sort, VecSort}, - EGraph, PrimitiveLike, Value, + EGraph, PrimitiveLike, Span, Value, }; struct InnerProduct { @@ -1624,10 +1636,11 @@ mod tests { "inner-product".into() } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.vec.clone(), self.ele.clone()], + span.clone(), ) .into_box() } @@ -1655,6 +1668,7 @@ mod tests { let mut egraph = EGraph::default(); egraph .parse_and_run_program( + None, " (sort IntVec (Vec i64)) ", @@ -1670,6 +1684,7 @@ mod tests { }); egraph .parse_and_run_program( + None, " (let a (vec-of 1 2 3 4 5 6)) (let b (vec-of 6 5 4 3 2 1)) diff --git a/src/main.rs b/src/main.rs index 2b597814..d4dbf532 100644 --- a/src/main.rs +++ b/src/main.rs @@ -13,8 +13,10 @@ struct Args { desugar: bool, #[clap(long)] resugar: bool, + /// Currently unused. #[clap(long)] proofs: bool, + /// Currently unused. /// Use the rust backend implimentation of eqsat, /// including a rust implementation of the union-find /// data structure and the rust implementation of @@ -60,12 +62,13 @@ fn main() { egraph.fact_directory = args.fact_directory.clone(); egraph.seminaive = !args.naive; egraph.run_mode = args.show; + // NB: both terms_encoding and proofs are currently unused if args.terms_encoding { egraph.enable_terms_encoding(); } if args.proofs { egraph - .parse_and_run_program("(set-option enable_proofs 1)") + .parse_and_run_program(None, "(set-option enable_proofs 1)") .unwrap(); } egraph @@ -78,7 +81,7 @@ fn main() { for line in BufReader::new(stdin).lines() { match line { - Ok(line_str) => match egraph.parse_and_run_program(&line_str) { + Ok(line_str) => match egraph.parse_and_run_program(None, &line_str) { Ok(msgs) => { for msg in msgs { println!("{msg}"); @@ -103,20 +106,13 @@ fn main() { } for (idx, input) in args.inputs.iter().enumerate() { - let program_read = std::fs::read_to_string(input).unwrap_or_else(|_| { + let program = std::fs::read_to_string(input).unwrap_or_else(|_| { let arg = input.to_string_lossy(); panic!("Failed to read file {arg}") }); let mut egraph = mk_egraph(); - let already_enables = program_read.starts_with("(set-option enable_proofs 1)"); - let (program, program_offset) = if args.proofs && !already_enables { - let expr = "(set-option enable_proofs 1)\n"; - (format!("{}{}", expr, program_read), expr.len()) - } else { - (program_read, 0) - }; - - match egraph.parse_and_run_program(&program) { + let program_offset = 0; + match egraph.parse_and_run_program(Some(input.to_str().unwrap().into()), &program) { Ok(msgs) => { for msg in msgs { println!("{msg}"); diff --git a/src/sort/bool.rs b/src/sort/bool.rs index ae5a5902..aa1e8bb5 100644 --- a/src/sort/bool.rs +++ b/src/sort/bool.rs @@ -33,7 +33,10 @@ impl Sort for BoolSort { fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { assert!(value.tag == self.name()); - (1, Expr::Lit((), Literal::Bool(value.bits > 0))) + ( + 1, + GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Bool(value.bits > 0)), + ) } } diff --git a/src/sort/f64.rs b/src/sort/f64.rs index 297d64d7..7b960615 100755 --- a/src/sort/f64.rs +++ b/src/sort/f64.rs @@ -57,7 +57,10 @@ impl Sort for F64Sort { assert!(value.tag == self.name()); ( 1, - Expr::Lit((), Literal::F64(OrderedFloat(f64::from_bits(value.bits)))), + GenericExpr::Lit( + DUMMY_SPAN.clone(), + Literal::F64(OrderedFloat(f64::from_bits(value.bits))), + ), ) } } diff --git a/src/sort/fn.rs b/src/sort/fn.rs index fda8a05a..fdd4efff 100644 --- a/src/sort/fn.rs +++ b/src/sort/fn.rs @@ -62,16 +62,16 @@ impl FunctionSort { name: Symbol, args: &[Expr], ) -> Result { - if let [inputs, Expr::Var((), output)] = args { + if let [inputs, Expr::Var(_, output)] = args { let output_sort = typeinfo .sorts .get(output) .ok_or(TypeError::UndefinedSort(*output))?; let input_sorts = match inputs { - Expr::Call((), first, rest_args) => { + Expr::Call(_, first, rest_args) => { let all_args = once(first).chain(rest_args.iter().map(|arg| { - if let Expr::Var((), arg) = arg { + if let Expr::Var(_, arg) = arg { arg } else { panic!("function sort must be called with list of input sorts"); @@ -88,7 +88,7 @@ impl FunctionSort { .collect::, _>>()? } // an empty list of inputs args is parsed as a unit literal - Expr::Lit((), Literal::Unit) => vec![], + Expr::Lit(_, Literal::Unit) => vec![], _ => panic!("function sort must be called with list of input sorts"), }; @@ -176,7 +176,10 @@ impl Sort for FunctionSort { ) -> Option<(Cost, Expr)> { let ValueFunction(name, inputs) = ValueFunction::load(self, &value); let (cost, args) = inputs.into_iter().try_fold( - (1usize, vec![Expr::Lit((), Literal::String(name))]), + ( + 1usize, + vec![GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::String(name))], + ), |(cost, mut args), (sort, value)| { let (new_cost, term) = extractor.find_best(value, termdag, &sort)?; args.push(termdag.term_to_expr(&term)); @@ -184,7 +187,7 @@ impl Sort for FunctionSort { }, )?; - Some((cost, Expr::call("unstable-fn", args))) + Some((cost, Expr::call_no_span("unstable-fn", args))) } } @@ -212,6 +215,7 @@ struct FunctionCTorTypeConstraint { name: Symbol, function: Arc, string: Arc, + span: Span, } impl TypeConstraint for FunctionCTorTypeConstraint { @@ -221,6 +225,7 @@ impl TypeConstraint for FunctionCTorTypeConstraint { vec![Constraint::Impossible( constraint::ImpossibleConstraint::ArityMismatch { atom: core::Atom { + span: self.span.clone(), head: self.name, args: arguments.to_vec(), }, @@ -252,11 +257,12 @@ impl PrimitiveLike for Ctor { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { Box::new(FunctionCTorTypeConstraint { name: self.name, function: self.function.clone(), string: self.string.clone(), + span: span.clone(), }) } @@ -285,11 +291,11 @@ impl PrimitiveLike for Apply { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { let mut sorts: Vec = vec![self.function.clone()]; sorts.extend(self.function.inputs.clone()); sorts.push(self.function.output.clone()); - SimpleTypeConstraint::new(self.name(), sorts).into_box() + SimpleTypeConstraint::new(self.name(), sorts, span.clone()).into_box() } fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option { @@ -333,9 +339,9 @@ fn call_fn(egraph: &mut EGraph, name: &Symbol, types: Vec, args: Vec (Cost, Expr) { assert!(value.tag == self.name()); - (1, Expr::Lit((), Literal::Int(value.bits as _))) + ( + 1, + GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Int(value.bits as _)), + ) } } @@ -108,8 +111,8 @@ impl PrimitiveLike for CountMatches { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.string.clone()) .with_exact_length(3) .with_output_sort(self.int.clone()) diff --git a/src/sort/macros.rs b/src/sort/macros.rs index 66ea6371..086c2045 100644 --- a/src/sort/macros.rs +++ b/src/sort/macros.rs @@ -42,9 +42,10 @@ macro_rules! add_primitives { fn get_type_constraints( &self, + span: &Span ) -> Box { let sorts = vec![$(self.$param.clone(),)* self.__out.clone() as ArcSort]; - SimpleTypeConstraint::new(self.name(), sorts).into_box() + SimpleTypeConstraint::new(self.name(), sorts, span.clone()).into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { diff --git a/src/sort/map.rs b/src/sort/map.rs index 4edfb20e..a0f9b416 100644 --- a/src/sort/map.rs +++ b/src/sort/map.rs @@ -29,7 +29,7 @@ impl MapSort { name: Symbol, args: &[Expr], ) -> Result { - if let [Expr::Var((), k), Expr::Var((), v)] = args { + if let [Expr::Var(_, k), Expr::Var(_, v)] = args { let k = typeinfo.sorts.get(k).ok_or(TypeError::UndefinedSort(*k))?; let v = typeinfo.sorts.get(v).ok_or(TypeError::UndefinedSort(*v))?; @@ -165,13 +165,13 @@ impl Sort for MapSort { termdag: &mut TermDag, ) -> Option<(Cost, Expr)> { let map = ValueMap::load(self, &value); - let mut expr = Expr::call("map-empty", []); + let mut expr = Expr::call_no_span("map-empty", []); let mut cost = 0usize; for (k, v) in map.iter().rev() { let k = extractor.find_best(*k, termdag, &self.key)?; let v = extractor.find_best(*v, termdag, &self.value)?; cost = cost.saturating_add(k.0).saturating_add(v.0); - expr = Expr::call( + expr = Expr::call_no_span( "map-insert", [expr, termdag.term_to_expr(&k.1), termdag.term_to_expr(&v.1)], ) @@ -210,8 +210,13 @@ impl PrimitiveLike for MapRebuild { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.map.clone(), self.map.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.map.clone(), self.map.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option { @@ -243,8 +248,8 @@ impl PrimitiveLike for TermOrderingMin { "ordering-min".into() } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_exact_length(3) .into_box() } @@ -266,8 +271,8 @@ impl PrimitiveLike for TermOrderingMax { "ordering-max".into() } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_exact_length(3) .into_box() } @@ -287,8 +292,8 @@ impl PrimitiveLike for Ctor { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.map.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new(self.name(), vec![self.map.clone()], span.clone()).into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -307,7 +312,7 @@ impl PrimitiveLike for Insert { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![ @@ -316,6 +321,7 @@ impl PrimitiveLike for Insert { self.map.value(), self.map.clone(), ], + span.clone(), ) .into_box() } @@ -337,10 +343,11 @@ impl PrimitiveLike for Get { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.map.clone(), self.map.key(), self.map.value()], + span.clone(), ) .into_box() } @@ -362,10 +369,11 @@ impl PrimitiveLike for NotContains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.map.clone(), self.map.key(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -391,10 +399,11 @@ impl PrimitiveLike for Contains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.map.clone(), self.map.key(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -419,10 +428,11 @@ impl PrimitiveLike for Remove { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.map.clone(), self.map.key(), self.map.clone()], + span.clone(), ) .into_box() } @@ -445,8 +455,13 @@ impl PrimitiveLike for Length { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.map.clone(), self.i64.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.map.clone(), self.i64.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { diff --git a/src/sort/mod.rs b/src/sort/mod.rs index f9eb396a..e758a52c 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -170,8 +170,8 @@ impl PrimitiveLike for ValueEq { *VALUE_EQ } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_exact_length(3) .with_output_sort(self.unit.clone()) .into_box() diff --git a/src/sort/rational.rs b/src/sort/rational.rs index e7880059..739faf07 100644 --- a/src/sort/rational.rs +++ b/src/sort/rational.rs @@ -109,6 +109,7 @@ impl Sort for RationalSort { add_primitives!(eg, "<=" = |a: R, b: R| -> Opt { if a <= b {Some(())} else {None} }); add_primitives!(eg, ">=" = |a: R, b: R| -> Opt { if a >= b {Some(())} else {None} }); } + fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { assert!(value.tag == self.name()); let rat = R::load(self, &value); @@ -116,11 +117,11 @@ impl Sort for RationalSort { let denom = *rat.denom(); ( 1, - Expr::call( + Expr::call_no_span( "rational", vec![ - Expr::Lit((), Literal::Int(numer)), - Expr::Lit((), Literal::Int(denom)), + GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Int(numer)), + GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Int(denom)), ], ), ) diff --git a/src/sort/set.rs b/src/sort/set.rs index d38a77b5..99e238a5 100644 --- a/src/sort/set.rs +++ b/src/sort/set.rs @@ -28,7 +28,7 @@ impl SetSort { name: Symbol, args: &[Expr], ) -> Result { - if let [Expr::Var((), e)] = args { + if let [Expr::Var(_, e)] = args { let e = typeinfo.sorts.get(e).ok_or(TypeError::UndefinedSort(*e))?; if e.is_eq_container_sort() { @@ -181,12 +181,12 @@ impl Sort for SetSort { termdag: &mut TermDag, ) -> Option<(Cost, Expr)> { let set = ValueSet::load(self, &value); - let mut expr = Expr::call("set-empty", []); + let mut expr = Expr::call_no_span("set-empty", []); let mut cost = 0usize; for e in set.iter().rev() { let e = extractor.find_best(*e, termdag, &self.element)?; cost = cost.saturating_add(e.0); - expr = Expr::call("set-insert", [expr, termdag.term_to_expr(&e.1)]) + expr = Expr::call_no_span("set-insert", [expr, termdag.term_to_expr(&e.1)]) } Some((cost, expr)) } @@ -222,8 +222,8 @@ impl PrimitiveLike for SetOf { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.set.element()) .with_output_sort(self.set.clone()) .into_box() @@ -245,8 +245,8 @@ impl PrimitiveLike for Ctor { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.set.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new(self.name(), vec![self.set.clone()], span.clone()).into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -265,8 +265,13 @@ impl PrimitiveLike for SetRebuild { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.set.clone(), self.set.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.set.clone(), self.set.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option { @@ -289,10 +294,11 @@ impl PrimitiveLike for Insert { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.element(), self.set.clone()], + span.clone(), ) .into_box() } @@ -315,10 +321,11 @@ impl PrimitiveLike for NotContains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.element(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -344,10 +351,11 @@ impl PrimitiveLike for Contains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.element(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -372,10 +380,11 @@ impl PrimitiveLike for Union { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.clone(), self.set.clone()], + span.clone(), ) .into_box() } @@ -398,10 +407,11 @@ impl PrimitiveLike for Intersect { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.clone(), self.set.clone()], + span.clone(), ) .into_box() } @@ -426,8 +436,13 @@ impl PrimitiveLike for Length { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.set.clone(), self.i64.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.set.clone(), self.i64.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -446,10 +461,11 @@ impl PrimitiveLike for Get { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.i64.clone(), self.set.element()], + span.clone(), ) .into_box() } @@ -471,10 +487,11 @@ impl PrimitiveLike for Remove { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.element(), self.set.clone()], + span.clone(), ) .into_box() } @@ -496,10 +513,11 @@ impl PrimitiveLike for Diff { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.set.clone(), self.set.clone(), self.set.clone()], + span.clone(), ) .into_box() } diff --git a/src/sort/string.rs b/src/sort/string.rs index 259a46f1..ce115d6f 100644 --- a/src/sort/string.rs +++ b/src/sort/string.rs @@ -27,7 +27,10 @@ impl Sort for StringSort { fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { assert!(value.tag == self.name); let sym = Symbol::from(NonZeroU32::new(value.bits as _).unwrap()); - (1, Expr::Lit((), Literal::String(sym))) + ( + 1, + GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::String(sym)), + ) } fn register_primitives(self: Arc, typeinfo: &mut TypeInfo) { @@ -71,8 +74,8 @@ impl PrimitiveLike for Add { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.string.clone()) .into_box() } @@ -98,8 +101,8 @@ impl PrimitiveLike for Replace { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.string.clone()) .with_exact_length(4) .into_box() diff --git a/src/sort/unit.rs b/src/sort/unit.rs index 58b8f2f0..31caf14a 100644 --- a/src/sort/unit.rs +++ b/src/sort/unit.rs @@ -27,7 +27,7 @@ impl Sort for UnitSort { fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { assert_eq!(value.tag, self.name); - (1, Expr::Lit((), Literal::Unit)) + (1, GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Unit)) } } @@ -48,8 +48,8 @@ impl PrimitiveLike for NotEqualPrimitive { "!=".into() } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_exact_length(3) .with_output_sort(self.unit.clone()) .into_box() diff --git a/src/sort/vec.rs b/src/sort/vec.rs index 9933799a..b616889d 100644 --- a/src/sort/vec.rs +++ b/src/sort/vec.rs @@ -43,7 +43,7 @@ impl VecSort { name: Symbol, args: &[Expr], ) -> Result { - if let [Expr::Var((), e)] = args { + if let [Expr::Var(_, e)] = args { let e = typeinfo.sorts.get(e).ok_or(TypeError::UndefinedSort(*e))?; if e.is_eq_container_sort() { @@ -183,7 +183,7 @@ impl Sort for VecSort { let mut cost = 0usize; if vec.is_empty() { - Some((cost, Expr::call("vec-empty", []))) + Some((cost, Expr::call_no_span("vec-empty", []))) } else { let elems = vec .into_iter() @@ -194,7 +194,7 @@ impl Sort for VecSort { }) .collect::>>()?; - Some((cost, Expr::call("vec-of", elems))) + Some((cost, Expr::call_no_span("vec-of", elems))) } } } @@ -229,8 +229,13 @@ impl PrimitiveLike for VecRebuild { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.vec.clone(), self.vec.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.vec.clone(), self.vec.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option { @@ -251,8 +256,8 @@ impl PrimitiveLike for VecOf { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.vec.element()) .with_output_sort(self.vec.clone()) .into_box() @@ -274,8 +279,8 @@ impl PrimitiveLike for Append { self.name } - fn get_type_constraints(&self) -> Box { - AllEqualTypeConstraint::new(self.name()) + fn get_type_constraints(&self, span: &Span) -> Box { + AllEqualTypeConstraint::new(self.name(), span.clone()) .with_all_arguments_sort(self.vec.clone()) .into_box() } @@ -296,8 +301,8 @@ impl PrimitiveLike for Ctor { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.vec.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new(self.name(), vec![self.vec.clone()], span.clone()).into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -316,10 +321,11 @@ impl PrimitiveLike for Push { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.vec.element(), self.vec.clone()], + span.clone(), ) .into_box() } @@ -341,8 +347,13 @@ impl PrimitiveLike for Pop { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.vec.clone(), self.vec.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.vec.clone(), self.vec.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -363,10 +374,11 @@ impl PrimitiveLike for NotContains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.vec.element(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -392,10 +404,11 @@ impl PrimitiveLike for Contains { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.vec.element(), self.unit.clone()], + span.clone(), ) .into_box() } @@ -421,8 +434,13 @@ impl PrimitiveLike for Length { self.name } - fn get_type_constraints(&self) -> Box { - SimpleTypeConstraint::new(self.name(), vec![self.vec.clone(), self.i64.clone()]).into_box() + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + self.name(), + vec![self.vec.clone(), self.i64.clone()], + span.clone(), + ) + .into_box() } fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { @@ -442,10 +460,11 @@ impl PrimitiveLike for Get { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.i64.clone(), self.vec.element()], + span.clone(), ) .into_box() } @@ -468,7 +487,7 @@ impl PrimitiveLike for Set { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![ @@ -477,6 +496,7 @@ impl PrimitiveLike for Set { self.vec.element.clone(), self.vec.clone(), ], + span.clone(), ) .into_box() } @@ -500,10 +520,11 @@ impl PrimitiveLike for Remove { self.name } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), vec![self.vec.clone(), self.i64.clone(), self.vec.clone()], + span.clone(), ) .into_box() } @@ -525,6 +546,7 @@ mod tests { let mut egraph = EGraph::default(); let outputs = egraph .parse_and_run_program( + None, r#" (sort IVec (Vec i64)) (let v0 (vec-empty)) @@ -537,13 +559,16 @@ mod tests { // Check extracted expr is parsed as an original expr egraph - .parse_and_run_program(&format!( - r#" + .parse_and_run_program( + None, + &format!( + r#" (check (= v0 {})) (check (= v1 {})) "#, - outputs[0], outputs[1], - )) + outputs[0], outputs[1], + ), + ) .unwrap(); } } diff --git a/src/termdag.rs b/src/termdag.rs index 67f260c1..5f0d47c8 100644 --- a/src/termdag.rs +++ b/src/termdag.rs @@ -1,7 +1,7 @@ use crate::{ - ast::{Expr, Literal}, + ast::Literal, util::{HashMap, HashSet}, - Symbol, + Expr, GenericExpr, Symbol, }; pub type TermId = usize; @@ -109,11 +109,11 @@ impl TermDag { /// This involves inserting every subexpression into this DAG. Because /// TermDags are hashconsed, the resulting term is guaranteed to maximally /// share subterms. - pub fn expr_to_term(&mut self, expr: &Expr) -> Term { + pub fn expr_to_term(&mut self, expr: &GenericExpr) -> Term { let res = match expr { - Expr::Lit((), lit) => Term::Lit(lit.clone()), - Expr::Var((), v) => Term::Var(*v), - Expr::Call((), op, args) => { + GenericExpr::Lit(_, lit) => Term::Lit(lit.clone()), + GenericExpr::Var(_, v) => Term::Var(*v), + GenericExpr::Call(_, op, args) => { let args = args .iter() .map(|a| { @@ -133,17 +133,17 @@ impl TermDag { /// Panics if the term contains subterms that are not in the DAG. pub fn term_to_expr(&self, term: &Term) -> Expr { match term { - Term::Lit(lit) => Expr::Lit((), lit.clone()), - Term::Var(v) => Expr::Var((), *v), + Term::Lit(lit) => Expr::lit_no_span(lit.clone()), + Term::Var(v) => Expr::var_no_span(*v), Term::App(op, args) => { - let args = args + let args: Vec<_> = args .iter() .map(|a| { let term = self.get(*a); self.term_to_expr(&term) }) .collect(); - Expr::Call((), *op, args) + Expr::call_no_span(*op, args) } } } @@ -191,7 +191,7 @@ impl TermDag { #[cfg(test)] mod tests { - use crate::ast; + use crate::{ast, DUMMY_SPAN}; use super::*; @@ -224,7 +224,10 @@ mod tests { ] ); let e2 = td.term_to_expr(&t); - assert_eq!(e, e2); // roundtrip + // This is tested using Sexp's equality because e1 and e2 have different + // annotations. A better way to test this would be to implement a map_ann + // function for GenericExpr. + assert_eq!(e.to_sexp(), e2.to_sexp()); // roundtrip } #[test] @@ -233,7 +236,7 @@ mod tests { let (td, t) = parse_term(s); match_term_app!(t; { ("f", [_, x, _, _]) => - assert_eq!(td.term_to_expr(&td.get(*x)), ast::Expr::Var((), Symbol::new("x"))), + assert_eq!(td.term_to_expr(&td.get(*x)), ast::GenericExpr::Var(DUMMY_SPAN.clone(), Symbol::new("x"))), (head, _) => panic!("unexpected head {}, in {}:{}:{}", head, file!(), line!(), column!()) }) } diff --git a/src/typechecking.rs b/src/typechecking.rs index b40e77fd..56c2c0ad 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -180,7 +180,7 @@ impl TypeInfo { self.declare_sort(*sort, presort_and_args)?; ResolvedNCommand::Sort(*sort, presort_and_args.clone()) } - NCommand::CoreAction(Action::Let(_, var, expr)) => { + NCommand::CoreAction(Action::Let(span, var, expr)) => { let expr = self.typecheck_expr(expr, &Default::default())?; let output_type = expr.output_type(self); self.global_types.insert(*var, output_type.clone()); @@ -190,12 +190,14 @@ impl TypeInfo { // not a global reference, but a global binding is_global_ref: false, }; - ResolvedNCommand::CoreAction(ResolvedAction::Let((), var, expr)) + ResolvedNCommand::CoreAction(ResolvedAction::Let(span.clone(), var, expr)) } NCommand::CoreAction(action) => { ResolvedNCommand::CoreAction(self.typecheck_action(action, &Default::default())?) } - NCommand::Check(facts) => ResolvedNCommand::Check(self.typecheck_facts(facts)?), + NCommand::Check(span, facts) => { + ResolvedNCommand::Check(span.clone(), self.typecheck_facts(facts)?) + } NCommand::Fail(cmd) => ResolvedNCommand::Fail(Box::new(self.typecheck_command(cmd)?)), NCommand::RunSchedule(schedule) => { ResolvedNCommand::RunSchedule(self.typecheck_schedule(schedule)?) @@ -251,8 +253,8 @@ impl TypeInfo { } let mut bound_vars = IndexMap::default(); let output_type = self.sorts.get(&fdecl.schema.output).unwrap(); - bound_vars.insert("old".into(), output_type.clone()); - bound_vars.insert("new".into(), output_type.clone()); + bound_vars.insert("old".into(), (DUMMY_SPAN.clone(), output_type.clone())); + bound_vars.insert("new".into(), (DUMMY_SPAN.clone(), output_type.clone())); Ok(ResolvedFunctionDecl { name: fdecl.name, @@ -275,28 +277,34 @@ impl TypeInfo { fn typecheck_schedule(&self, schedule: &Schedule) -> Result { let schedule = match schedule { - Schedule::Repeat(times, schedule) => { - ResolvedSchedule::Repeat(*times, Box::new(self.typecheck_schedule(schedule)?)) - } - Schedule::Sequence(schedules) => { + Schedule::Repeat(span, times, schedule) => ResolvedSchedule::Repeat( + span.clone(), + *times, + Box::new(self.typecheck_schedule(schedule)?), + ), + Schedule::Sequence(span, schedules) => { let schedules = schedules .iter() .map(|schedule| self.typecheck_schedule(schedule)) .collect::, _>>()?; - ResolvedSchedule::Sequence(schedules) - } - Schedule::Saturate(schedule) => { - ResolvedSchedule::Saturate(Box::new(self.typecheck_schedule(schedule)?)) + ResolvedSchedule::Sequence(span.clone(), schedules) } - Schedule::Run(RunConfig { ruleset, until }) => { + Schedule::Saturate(span, schedule) => ResolvedSchedule::Saturate( + span.clone(), + Box::new(self.typecheck_schedule(schedule)?), + ), + Schedule::Run(span, RunConfig { ruleset, until }) => { let until = until .as_ref() .map(|facts| self.typecheck_facts(facts)) .transpose()?; - ResolvedSchedule::Run(ResolvedRunConfig { - ruleset: *ruleset, - until, - }) + ResolvedSchedule::Run( + span.clone(), + ResolvedRunConfig { + ruleset: *ruleset, + until, + }, + ) } }; @@ -327,7 +335,7 @@ impl TypeInfo { } fn typecheck_rule(&self, rule: &Rule) -> Result { - let Rule { head, body } = rule; + let Rule { span, head, body } = rule; let mut constraints = vec![]; let mut fresh_gen = SymbolGen::new("$".to_string()); @@ -340,6 +348,7 @@ impl TypeInfo { let mut problem = Problem::default(); problem.add_rule( &CoreRule { + span: span.clone(), body: query, head: actions, }, @@ -354,6 +363,7 @@ impl TypeInfo { let actions: ResolvedActions = assignment.annotate_actions(&mapped_action, self)?; Ok(ResolvedRule { + span: span.clone(), body, head: actions, }) @@ -374,7 +384,7 @@ impl TypeInfo { fn typecheck_actions( &self, actions: &Actions, - binding: &IndexMap, + binding: &IndexMap, ) -> Result { let mut binding_set = binding.keys().cloned().collect::>(); let mut fresh_gen = SymbolGen::new("$".to_string()); @@ -386,8 +396,8 @@ impl TypeInfo { problem.add_actions(&actions, self)?; // add bindings from the context - for (var, sort) in binding { - problem.assign_local_var_type(*var, sort.clone())?; + for (var, (span, sort)) in binding { + problem.assign_local_var_type(*var, span.clone(), sort.clone())?; } let assignment = problem @@ -401,9 +411,9 @@ impl TypeInfo { fn typecheck_expr( &self, expr: &Expr, - binding: &IndexMap, + binding: &IndexMap, ) -> Result { - let action = Action::Expr((), expr.clone()); + let action = Action::Expr(DUMMY_SPAN.clone(), expr.clone()); let typechecked_action = self.typecheck_action(&action, binding)?; match typechecked_action { ResolvedAction::Expr(_, expr) => Ok(expr), @@ -414,7 +424,7 @@ impl TypeInfo { fn typecheck_action( &self, action: &Action, - binding: &IndexMap, + binding: &IndexMap, ) -> Result { self.typecheck_actions(&Actions::singleton(action.clone()), binding) .map(|mut v| { @@ -502,15 +512,20 @@ mod test { fn test_arity_mismatch() { let mut egraph = EGraph::default(); - let res = egraph.parse_and_run_program( - " + let prog = " (relation f (i64 i64)) (rule ((f a b c)) ()) - ", - ); - assert!(matches!( - res, - Err(Error::TypeError(TypeError::Arity { expected: 2, .. })) - )); + "; + let res = egraph.parse_and_run_program(None, prog); + match res { + Err(Error::TypeError(TypeError::Arity { + expected: 2, + expr: e, + })) => { + let span = e.span(); + assert_eq!(&prog[span.1..span.2], "(f a b c)"); + } + _ => panic!("Expected arity mismatch, got: {:?}", res), + } } } diff --git a/tests/files.rs b/tests/files.rs index 3ee1f63b..6539b2f9 100644 --- a/tests/files.rs +++ b/tests/files.rs @@ -16,24 +16,32 @@ impl Run { .unwrap_or_else(|err| panic!("Couldn't read {:?}: {:?}", self.path, err)); if !self.resugar { - self.test_program(&program, "Top level error"); + self.test_program( + self.path.to_str().map(String::from), + &program, + "Top level error", + ); } else { let mut egraph = EGraph::default(); egraph.run_mode = RunMode::ShowDesugaredEgglog; egraph.set_reserved_symbol("__".into()); - let desugared_str = egraph.parse_and_run_program(&program).unwrap().join("\n"); + let desugared_str = egraph + .parse_and_run_program(self.path.to_str().map(String::from), &program) + .unwrap() + .join("\n"); self.test_program( + None, &desugared_str, "ERROR after parse, to_string, and parse again.", ); } } - fn test_program(&self, program: &str, message: &str) { + fn test_program(&self, filename: Option, program: &str, message: &str) { let mut egraph = EGraph::default(); egraph.set_reserved_symbol("___".into()); - match egraph.parse_and_run_program(program) { + match egraph.parse_and_run_program(filename, program) { Ok(msgs) => { if self.should_fail() { panic!( diff --git a/tests/integration_test.rs b/tests/integration_test.rs index 88861131..50026050 100644 --- a/tests/integration_test.rs +++ b/tests/integration_test.rs @@ -8,6 +8,7 @@ fn test_subsumed_unextractable_action_extract() { egraph .parse_and_run_program( + None, r#" (datatype Math) (function exp () Math :cost 100) @@ -28,6 +29,7 @@ fn test_subsumed_unextractable_action_extract() { // Then if we make one as subsumed, it should give back the variable term egraph .parse_and_run_program( + None, r#" (subsume (cheap)) (query-extract (exp)) @@ -61,6 +63,7 @@ fn test_subsumed_unextractable_rebuild_arg() { egraph .parse_and_run_program( + None, r#" (datatype Math) (function container (Math) Math) @@ -83,6 +86,7 @@ fn test_subsumed_unextractable_rebuild_arg() { // Then we can union them egraph .parse_and_run_program( + None, r#" (union (cheap-1) (cheap)) "#, @@ -97,6 +101,7 @@ fn test_subsumed_unextractable_rebuild_arg() { // Now verify that if we extract, it still respects the unextractable, even though it's a different values now egraph .parse_and_run_program( + None, r#" (query-extract res) "#, @@ -107,7 +112,7 @@ fn test_subsumed_unextractable_rebuild_arg() { panic!(); }; let expr = termdag.term_to_expr(&term); - assert_eq!(expr, Expr::Call((), GlobalSymbol::from("exp"), vec![])); + assert_eq!(expr, Expr::call_no_span(GlobalSymbol::from("exp"), vec![])); } #[test] @@ -117,6 +122,7 @@ fn test_subsumed_unextractable_rebuild_self() { egraph .parse_and_run_program( + None, r#" (datatype Math) (function container (Math) Math) @@ -132,6 +138,7 @@ fn test_subsumed_unextractable_rebuild_self() { // Then we can union them egraph .parse_and_run_program( + None, r#" (union (exp) x) "#, @@ -145,6 +152,7 @@ fn test_subsumed_unextractable_rebuild_self() { // Now verify that if we extract, it still respects the subsumption, even though it's a different values now egraph .parse_and_run_program( + None, r#" (query-extract x) "#, @@ -155,7 +163,7 @@ fn test_subsumed_unextractable_rebuild_self() { panic!(); }; let expr = termdag.term_to_expr(&term); - assert_eq!(expr, Expr::Call((), GlobalSymbol::from("exp"), vec![])); + assert_eq!(expr, Expr::call_no_span(GlobalSymbol::from("exp"), vec![])); } #[test] @@ -165,6 +173,7 @@ fn test_subsume_unextractable_insert_and_merge() { egraph .parse_and_run_program( + None, r#" (datatype Expr (f Expr) @@ -198,6 +207,7 @@ fn test_subsume_unextractable_action_extract_multiple() { egraph .parse_and_run_program( + None, " (datatype Math (Num i64)) (Num 1) @@ -215,6 +225,7 @@ fn test_subsume_unextractable_action_extract_multiple() { // Then if we make one unextractable, it should only give back one term egraph .parse_and_run_program( + None, " (subsume (Num 2)) (query-extract :variants 2 (Num 1)) @@ -236,6 +247,7 @@ fn test_rewrite_subsumed_unextractable() { egraph .parse_and_run_program( + None, r#" (datatype Math) (function exp () Math :cost 100) @@ -265,6 +277,7 @@ fn test_rewrite_subsumed() { // If we rerite most-exp to another term, that rewrite shouldnt trigger since its been subsumed. egraph .parse_and_run_program( + None, r#" (datatype Math) (function exp () Math :cost 100) @@ -296,6 +309,7 @@ fn test_subsume() { let mut egraph = EGraph::default(); egraph .parse_and_run_program( + None, r#" (datatype Math (Add Math Math) @@ -317,6 +331,7 @@ fn test_subsume() { egraph .parse_and_run_program( + None, r#" ;; add something equal to x that can be extracted: (declare other Math) @@ -337,6 +352,7 @@ fn test_subsume_primitive() { let mut egraph = EGraph::default(); let res = egraph.parse_and_run_program( + None, r#" (function one () i64) (set (one) 1) @@ -352,6 +368,7 @@ fn test_cant_subsume_merge() { let mut egraph = EGraph::default(); let res = egraph.parse_and_run_program( + None, r#" (function one () i64 :merge old) (set (one) 1) diff --git a/web-demo/src/lib.rs b/web-demo/src/lib.rs index 312b301c..548ae2bf 100644 --- a/web-demo/src/lib.rs +++ b/web-demo/src/lib.rs @@ -15,7 +15,7 @@ pub struct Result { #[wasm_bindgen] pub fn run_program(input: &str) -> Result { let mut egraph = egglog::EGraph::default(); - match egraph.parse_and_run_program(input) { + match egraph.parse_and_run_program(Some("web-demo.egg".into()), input) { Ok(outputs) => { let serialized = egraph.serialize_for_graphviz(false, 40, 40); Result {