pub mod desugar;
+mod expr;
+pub mod parse;
+pub(crate) mod remove_globals;
+
+use crate::{
+ core::{GenericAtom, GenericAtomTerm, HeadOrEq, Query, ResolvedCall},
+ *,
+};
+pub use expr::*;
+pub use parse::*;
+use std::fmt::Display;
+pub use symbol_table::GlobalSymbol as Symbol;
+
+#[derive(Clone, Debug)]
+pub(crate) enum Ruleset {
+ Rules(Symbol, IndexMap<Symbol, CompiledRule>),
+ Combined(Symbol, Vec<Symbol>),
+}
+
+pub type NCommand = GenericNCommand<Symbol, Symbol>;
+pub(crate) type ResolvedNCommand = GenericNCommand<ResolvedCall, ResolvedVar>;
+
+#[derive(Debug, Clone, Eq, PartialEq, Hash)]
+pub enum GenericNCommand<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ SetOption {
+ name: Symbol,
+ value: GenericExpr<Head, Leaf>,
+ },
+ Sort(
+ Span,
+ Symbol,
+ Option<(Symbol, Vec<GenericExpr<Symbol, Symbol>>)>,
+ ),
+ Function(GenericFunctionDecl<Head, Leaf>),
+ AddRuleset(Symbol),
+ UnstableCombinedRuleset(Symbol, Vec<Symbol>),
+ NormRule {
+ name: Symbol,
+ ruleset: Symbol,
+ rule: GenericRule<Head, Leaf>,
+ },
+ CoreAction(GenericAction<Head, Leaf>),
+ RunSchedule(GenericSchedule<Head, Leaf>),
+ PrintOverallStatistics,
+ Check(Span, Vec<GenericFact<Head, Leaf>>),
+ PrintTable(Span, Symbol, usize),
+ PrintSize(Span, Option<Symbol>),
+ Output {
+ span: Span,
+ file: String,
+ exprs: Vec<GenericExpr<Head, Leaf>>,
+ },
+ Push(usize),
+ Pop(Span, usize),
+ Fail(Span, Box<GenericNCommand<Head, Leaf>>),
+ Input {
+ span: Span,
+ name: Symbol,
+ file: String,
+ },
+}
+
+impl<Head, Leaf> GenericNCommand<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub fn to_command(&self) -> GenericCommand<Head, Leaf> {
+ match self {
+ GenericNCommand::SetOption { name, value } => GenericCommand::SetOption {
+ name: *name,
+ value: value.clone(),
+ },
+ GenericNCommand::Sort(span, name, params) => {
+ GenericCommand::Sort(span.clone(), *name, params.clone())
+ }
+ GenericNCommand::Function(f) => GenericCommand::Function(f.clone()),
+ GenericNCommand::AddRuleset(name) => GenericCommand::AddRuleset(*name),
+ GenericNCommand::UnstableCombinedRuleset(name, others) => {
+ GenericCommand::UnstableCombinedRuleset(*name, others.clone())
+ }
+ GenericNCommand::NormRule {
+ name,
+ ruleset,
+ rule,
+ } => GenericCommand::Rule {
+ name: *name,
+ ruleset: *ruleset,
+ rule: rule.clone(),
+ },
+ GenericNCommand::RunSchedule(schedule) => GenericCommand::RunSchedule(schedule.clone()),
+ GenericNCommand::PrintOverallStatistics => GenericCommand::PrintOverallStatistics,
+ GenericNCommand::CoreAction(action) => GenericCommand::Action(action.clone()),
+ GenericNCommand::Check(span, facts) => {
+ GenericCommand::Check(span.clone(), facts.clone())
+ }
+ GenericNCommand::PrintTable(span, name, n) => {
+ GenericCommand::PrintFunction(span.clone(), *name, *n)
+ }
+ GenericNCommand::PrintSize(span, name) => {
+ GenericCommand::PrintSize(span.clone(), *name)
+ }
+ GenericNCommand::Output { span, file, exprs } => GenericCommand::Output {
+ span: span.clone(),
+ file: file.to_string(),
+ exprs: exprs.clone(),
+ },
+ GenericNCommand::Push(n) => GenericCommand::Push(*n),
+ GenericNCommand::Pop(span, n) => GenericCommand::Pop(span.clone(), *n),
+ GenericNCommand::Fail(span, cmd) => {
+ GenericCommand::Fail(span.clone(), Box::new(cmd.to_command()))
+ }
+ GenericNCommand::Input { span, name, file } => GenericCommand::Input {
+ span: span.clone(),
+ name: *name,
+ file: file.clone(),
+ },
+ }
+ }
+
+ pub fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ match self {
+ GenericNCommand::SetOption { name, value } => GenericNCommand::SetOption {
+ name,
+ value: f(value.clone()),
+ },
+ GenericNCommand::Sort(span, name, params) => GenericNCommand::Sort(span, name, params),
+ GenericNCommand::Function(func) => GenericNCommand::Function(func.visit_exprs(f)),
+ GenericNCommand::AddRuleset(name) => GenericNCommand::AddRuleset(name),
+ GenericNCommand::UnstableCombinedRuleset(name, rulesets) => {
+ GenericNCommand::UnstableCombinedRuleset(name, rulesets)
+ }
+ GenericNCommand::NormRule {
+ name,
+ ruleset,
+ rule,
+ } => GenericNCommand::NormRule {
+ name,
+ ruleset,
+ rule: rule.visit_exprs(f),
+ },
+ GenericNCommand::RunSchedule(schedule) => {
+ GenericNCommand::RunSchedule(schedule.visit_exprs(f))
+ }
+ GenericNCommand::PrintOverallStatistics => GenericNCommand::PrintOverallStatistics,
+ GenericNCommand::CoreAction(action) => {
+ GenericNCommand::CoreAction(action.visit_exprs(f))
+ }
+ GenericNCommand::Check(span, facts) => GenericNCommand::Check(
+ span,
+ facts.into_iter().map(|fact| fact.visit_exprs(f)).collect(),
+ ),
+ GenericNCommand::PrintTable(span, name, n) => {
+ GenericNCommand::PrintTable(span, name, n)
+ }
+ GenericNCommand::PrintSize(span, name) => GenericNCommand::PrintSize(span, name),
+ GenericNCommand::Output { span, file, exprs } => GenericNCommand::Output {
+ span,
+ file,
+ exprs: exprs.into_iter().map(f).collect(),
+ },
+ GenericNCommand::Push(n) => GenericNCommand::Push(n),
+ GenericNCommand::Pop(span, n) => GenericNCommand::Pop(span, n),
+ GenericNCommand::Fail(span, cmd) => {
+ GenericNCommand::Fail(span, Box::new(cmd.visit_exprs(f)))
+ }
+ GenericNCommand::Input { span, name, file } => {
+ GenericNCommand::Input { span, name, file }
+ }
+ }
+ }
+}
+
+pub type Schedule = GenericSchedule<Symbol, Symbol>;
+pub(crate) type ResolvedSchedule = GenericSchedule<ResolvedCall, ResolvedVar>;
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum GenericSchedule<Head, Leaf> {
+ Saturate(Span, Box<GenericSchedule<Head, Leaf>>),
+ Repeat(Span, usize, Box<GenericSchedule<Head, Leaf>>),
+ Run(Span, GenericRunConfig<Head, Leaf>),
+ Sequence(Span, Vec<GenericSchedule<Head, Leaf>>),
+}
+
+pub trait ToSexp {
+ fn to_sexp(&self) -> Sexp;
+}
+
+impl ToSexp for str {
+ fn to_sexp(&self) -> Sexp {
+ Sexp::Symbol(String::from(self))
+ }
+}
+
+impl ToSexp for Symbol {
+ fn to_sexp(&self) -> Sexp {
+ Sexp::Symbol(self.to_string())
+ }
+}
+
+impl ToSexp for usize {
+ fn to_sexp(&self) -> Sexp {
+ Sexp::Symbol(self.to_string())
+ }
+}
+
+impl ToSexp for Sexp {
+ fn to_sexp(&self) -> Sexp {
+ self.clone()
+ }
+}
+
+macro_rules! list {
+ ($($e:expr,)* ++ $tail:expr) => {{
+ let mut list: Vec<Sexp> = vec![$($e.to_sexp(),)*];
+ list.extend($tail.iter().map(|e| e.to_sexp()));
+ Sexp::List(list)
+ }};
+ ($($e:expr),*) => {{
+ let list: Vec<Sexp> = vec![ $($e.to_sexp(),)* ];
+ Sexp::List(list)
+ }};
+}
+
+impl<Head, Leaf> GenericSchedule<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ match self {
+ GenericSchedule::Saturate(span, sched) => {
+ GenericSchedule::Saturate(span, Box::new(sched.visit_exprs(f)))
+ }
+ 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<Head: Display, Leaf: Display> ToSexp for GenericSchedule<Head, Leaf> {
+ fn to_sexp(&self) -> Sexp {
+ match self {
+ 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<Head: Display, Leaf: Display> Display for GenericSchedule<Head, Leaf> {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_sexp())
+ }
+}
+
+pub type Command = GenericCommand<Symbol, Symbol>;
+
+pub type Subsume = bool;
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Subdatatypes {
+ Variants(Vec<Variant>),
+ NewSort(Symbol, Vec<Expr>),
+}
+
+#[derive(Debug, Clone)]
+pub enum GenericCommand<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ SetOption {
+ name: Symbol,
+ value: GenericExpr<Head, Leaf>,
+ },
+ Datatype {
+ span: Span,
+ name: Symbol,
+ variants: Vec<Variant>,
+ },
+ Datatypes {
+ span: Span,
+ datatypes: Vec<(Span, Symbol, Subdatatypes)>,
+ },
+ Sort(Span, Symbol, Option<(Symbol, Vec<Expr>)>),
+ Function(GenericFunctionDecl<Head, Leaf>),
+ Relation {
+ span: Span,
+ constructor: Symbol,
+ inputs: Vec<Symbol>,
+ },
+ AddRuleset(Symbol),
+ UnstableCombinedRuleset(Symbol, Vec<Symbol>),
+ Rule {
+ name: Symbol,
+ ruleset: Symbol,
+ rule: GenericRule<Head, Leaf>,
+ },
+ Rewrite(Symbol, GenericRewrite<Head, Leaf>, Subsume),
+ BiRewrite(Symbol, GenericRewrite<Head, Leaf>),
+ Action(GenericAction<Head, Leaf>),
+ RunSchedule(GenericSchedule<Head, Leaf>),
+ PrintOverallStatistics,
+ Simplify {
+ span: Span,
+ expr: GenericExpr<Head, Leaf>,
+ schedule: GenericSchedule<Head, Leaf>,
+ },
+ QueryExtract {
+ span: Span,
+ variants: usize,
+ expr: GenericExpr<Head, Leaf>,
+ },
+ Check(Span, Vec<GenericFact<Head, Leaf>>),
+ PrintFunction(Span, Symbol, usize),
+ PrintSize(Span, Option<Symbol>),
+ Input {
+ span: Span,
+ name: Symbol,
+ file: String,
+ },
+ Output {
+ span: Span,
+ file: String,
+ exprs: Vec<GenericExpr<Head, Leaf>>,
+ },
+ Push(usize),
+ Pop(Span, usize),
+ Fail(Span, Box<GenericCommand<Head, Leaf>>),
+ Include(Span, String),
+}
+
+impl<Head, Leaf> ToSexp for GenericCommand<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn to_sexp(&self) -> Sexp {
+ match self {
+ GenericCommand::SetOption { name, value } => list!("set-option", name, value),
+ GenericCommand::Rewrite(name, rewrite, subsume) => {
+ rewrite.to_sexp(*name, false, *subsume)
+ }
+ GenericCommand::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true, false),
+ GenericCommand::Datatype {
+ span: _,
+ name,
+ variants,
+ } => list!("datatype", name, ++ variants),
+ GenericCommand::Action(a) => a.to_sexp(),
+ GenericCommand::Sort(_span, name, None) => list!("sort", name),
+ GenericCommand::Sort(_span, name, Some((name2, args))) => {
+ list!("sort", name, list!( name2, ++ args))
+ }
+ GenericCommand::Function(f) => f.to_sexp(),
+ GenericCommand::Relation {
+ span: _,
+ constructor,
+ inputs,
+ } => list!("relation", constructor, list!(++ inputs)),
+ GenericCommand::AddRuleset(name) => list!("ruleset", name),
+ GenericCommand::UnstableCombinedRuleset(name, others) => {
+ list!("unstable-combined-ruleset", name, ++ others)
+ }
+ GenericCommand::Rule {
+ name,
+ ruleset,
+ rule,
+ } => rule.to_sexp(*ruleset, *name),
+ GenericCommand::RunSchedule(sched) => list!("run-schedule", sched),
+ GenericCommand::PrintOverallStatistics => list!("print-stats"),
+ GenericCommand::QueryExtract {
+ span: _,
+ variants,
+ expr,
+ } => {
+ list!("query-extract", ":variants", variants, expr)
+ }
+ GenericCommand::Check(_ann, facts) => list!("check", ++ facts),
+ GenericCommand::Push(n) => list!("push", n),
+ GenericCommand::Pop(_span, n) => list!("pop", n),
+ GenericCommand::PrintFunction(_span, name, n) => list!("print-function", name, n),
+ GenericCommand::PrintSize(_span, name) => list!("print-size", ++ name),
+ GenericCommand::Input {
+ span: _,
+ name,
+ file,
+ } => {
+ list!("input", name, format!("\"{}\"", file))
+ }
+ GenericCommand::Output {
+ span: _,
+ file,
+ exprs,
+ } => {
+ list!("output", format!("\"{}\"", file), ++ exprs)
+ }
+ GenericCommand::Fail(_span, cmd) => list!("fail", cmd),
+ GenericCommand::Include(_span, file) => list!("include", format!("\"{}\"", file)),
+ GenericCommand::Simplify {
+ span: _,
+ expr,
+ schedule,
+ } => list!("simplify", schedule, expr),
+ GenericCommand::Datatypes { span: _, datatypes } => {
+ let datatypes: Vec<_> = datatypes
+ .iter()
+ .map(|(_, name, variants)| match variants {
+ Subdatatypes::Variants(variants) => list!(name, ++ variants),
+ Subdatatypes::NewSort(head, args) => {
+ list!("sort", name, list!(head, ++ args))
+ }
+ })
+ .collect();
+ list!("datatype*", ++ datatypes)
+ }
+ }
+ }
+}
+
+impl<Head, Leaf> Display for GenericNCommand<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_command())
+ }
+}
+
+impl<Head, Leaf> Display for GenericCommand<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+ match self {
+ GenericCommand::Rule {
+ ruleset,
+ name,
+ rule,
+ } => rule.fmt_with_ruleset(f, *ruleset, *name),
+ GenericCommand::Check(_ann, facts) => {
+ write!(f, "(check {})", ListDisplay(facts, "\n"))
+ }
+ _ => write!(f, "{}", self.to_sexp()),
+ }
+ }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct IdentSort {
+ pub ident: Symbol,
+ pub sort: Symbol,
+}
+
+impl ToSexp for IdentSort {
+ fn to_sexp(&self) -> Sexp {
+ list!(self.ident, self.sort)
+ }
+}
+
+impl Display for IdentSort {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_sexp())
+ }
+}
+
+pub type RunConfig = GenericRunConfig<Symbol, Symbol>;
+pub(crate) type ResolvedRunConfig = GenericRunConfig<ResolvedCall, ResolvedVar>;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct GenericRunConfig<Head, Leaf> {
+ pub ruleset: Symbol,
+ pub until: Option<Vec<GenericFact<Head, Leaf>>>,
+}
+
+impl<Head, Leaf> GenericRunConfig<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ Self {
+ ruleset: self.ruleset,
+ until: self
+ .until
+ .map(|until| until.into_iter().map(|fact| fact.visit_exprs(f)).collect()),
+ }
+ }
+}
+
+impl<Head: Display, Leaf: Display> ToSexp for GenericRunConfig<Head, Leaf>
+where
+ Head: Display,
+ Leaf: Display,
+{
+ fn to_sexp(&self) -> Sexp {
+ let mut res = vec![Sexp::Symbol("run".into())];
+ if self.ruleset != "".into() {
+ res.push(Sexp::Symbol(self.ruleset.to_string()));
+ }
+ if let Some(until) = &self.until {
+ res.push(Sexp::Symbol(":until".into()));
+ res.extend(until.iter().map(|fact| fact.to_sexp()));
+ }
+
+ Sexp::List(res)
+ }
+}
+
+pub type FunctionDecl = GenericFunctionDecl<Symbol, Symbol>;
+pub(crate) type ResolvedFunctionDecl = GenericFunctionDecl<ResolvedCall, ResolvedVar>;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct GenericFunctionDecl<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub name: Symbol,
+ pub schema: Schema,
+ pub default: Option<GenericExpr<Head, Leaf>>,
+ pub merge: Option<GenericExpr<Head, Leaf>>,
+ pub merge_action: GenericActions<Head, Leaf>,
+ pub cost: Option<usize>,
+ pub unextractable: bool,
+ pub ignore_viz: bool,
+ pub span: Span,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Variant {
+ pub span: Span,
+ pub name: Symbol,
+ pub types: Vec<Symbol>,
+ pub cost: Option<usize>,
+}
+
+impl ToSexp for Variant {
+ fn to_sexp(&self) -> Sexp {
+ let mut res = vec![Sexp::Symbol(self.name.to_string())];
+ if !self.types.is_empty() {
+ res.extend(self.types.iter().map(|s| Sexp::Symbol(s.to_string())));
+ }
+ if let Some(cost) = self.cost {
+ res.push(Sexp::Symbol(":cost".into()));
+ res.push(Sexp::Symbol(cost.to_string()));
+ }
+ Sexp::List(res)
+ }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Schema {
+ pub input: Vec<Symbol>,
+ pub output: Symbol,
+}
+
+impl ToSexp for Schema {
+ fn to_sexp(&self) -> Sexp {
+ list!(list!(++ self.input), self.output)
+ }
+}
+
+impl Schema {
+ pub fn new(input: Vec<Symbol>, output: Symbol) -> Self {
+ Self { input, output }
+ }
+}
+
+impl FunctionDecl {
+ pub fn relation(span: Span, name: Symbol, input: Vec<Symbol>) -> Self {
+ Self {
+ name,
+ schema: Schema {
+ input,
+ output: Symbol::from("Unit"),
+ },
+ merge: None,
+ merge_action: Actions::default(),
+ default: Some(Expr::Lit(DUMMY_SPAN.clone(), Literal::Unit)),
+ cost: None,
+ unextractable: false,
+ ignore_viz: false,
+ span,
+ }
+ }
+}
+
+impl<Head, Leaf> GenericFunctionDecl<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> GenericFunctionDecl<Head, Leaf> {
+ GenericFunctionDecl {
+ name: self.name,
+ schema: self.schema,
+ default: self.default.map(|expr| expr.visit_exprs(f)),
+ merge: self.merge.map(|expr| expr.visit_exprs(f)),
+ merge_action: self.merge_action.visit_exprs(f),
+ cost: self.cost,
+ unextractable: self.unextractable,
+ ignore_viz: self.ignore_viz,
+ span: self.span,
+ }
+ }
+}
+
+impl<Head, Leaf> ToSexp for GenericFunctionDecl<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn to_sexp(&self) -> Sexp {
+ let mut res = vec![
+ Sexp::Symbol("function".into()),
+ Sexp::Symbol(self.name.to_string()),
+ ];
+
+ if let Sexp::List(contents) = self.schema.to_sexp() {
+ res.extend(contents);
+ } else {
+ unreachable!();
+ }
+
+ if let Some(cost) = self.cost {
+ res.extend(vec![
+ Sexp::Symbol(":cost".into()),
+ Sexp::Symbol(cost.to_string()),
+ ]);
+ }
+
+ if self.unextractable {
+ res.push(Sexp::Symbol(":unextractable".into()));
+ }
+
+ if !self.merge_action.is_empty() {
+ res.push(Sexp::Symbol(":on_merge".into()));
+ res.push(Sexp::List(
+ self.merge_action.iter().map(|a| a.to_sexp()).collect(),
+ ));
+ }
+
+ if let Some(merge) = &self.merge {
+ res.push(Sexp::Symbol(":merge".into()));
+ res.push(merge.to_sexp());
+ }
+
+ if let Some(default) = &self.default {
+ res.push(Sexp::Symbol(":default".into()));
+ res.push(default.to_sexp());
+ }
+
+ Sexp::List(res)
+ }
+}
+
+pub type Fact = GenericFact<Symbol, Symbol>;
+pub(crate) type ResolvedFact = GenericFact<ResolvedCall, ResolvedVar>;
+pub(crate) type MappedFact<Head, Leaf> = GenericFact<CorrespondingVar<Head, Leaf>, Leaf>;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum GenericFact<Head, Leaf> {
+ Eq(Span, Vec<GenericExpr<Head, Leaf>>),
+ Fact(GenericExpr<Head, Leaf>),
+}
+
+pub struct Facts<Head, Leaf>(pub Vec<GenericFact<Head, Leaf>>);
+
+impl<Head, Leaf> Facts<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub(crate) fn to_query(
+ &self,
+ typeinfo: &TypeInfo,
+ fresh_gen: &mut impl FreshGen<Head, Leaf>,
+ ) -> (Query<HeadOrEq<Head>, Leaf>, Vec<MappedFact<Head, Leaf>>)
+ where
+ Leaf: SymbolLike,
+ {
+ let mut atoms = vec![];
+ let mut new_body = vec![];
+
+ for fact in self.0.iter() {
+ match fact {
+ GenericFact::Eq(span, exprs) => {
+ let mut new_exprs = vec![];
+ let mut to_equate = vec![];
+ for expr in exprs {
+ let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen);
+ atoms.extend(child_atoms);
+ to_equate.push(expr.get_corresponding_var_or_lit(typeinfo));
+ new_exprs.push(expr);
+ }
+ atoms.push(GenericAtom {
+ span: span.clone(),
+ head: HeadOrEq::Eq,
+ args: to_equate,
+ });
+ new_body.push(GenericFact::Eq(span.clone(), new_exprs));
+ }
+ GenericFact::Fact(expr) => {
+ let (child_atoms, expr) = expr.to_query(typeinfo, fresh_gen);
+ atoms.extend(child_atoms);
+ new_body.push(GenericFact::Fact(expr));
+ }
+ }
+ }
+ (Query { atoms }, new_body)
+ }
+}
+
+impl<Head: Display, Leaf: Display> ToSexp for GenericFact<Head, Leaf>
+where
+ Head: Display,
+ Leaf: Display,
+{
+ fn to_sexp(&self) -> Sexp {
+ match self {
+ GenericFact::Eq(_, exprs) => list!("=", ++ exprs),
+ GenericFact::Fact(expr) => expr.to_sexp(),
+ }
+ }
+}
+
+impl<Head, Leaf> GenericFact<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub(crate) fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> GenericFact<Head, Leaf> {
+ match self {
+ 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<Head2, Leaf2>(
+ &self,
+ f: &mut impl FnMut(&GenericExpr<Head, Leaf>) -> GenericExpr<Head2, Leaf2>,
+ ) -> GenericFact<Head2, Leaf2> {
+ match self {
+ GenericFact::Eq(span, exprs) => {
+ GenericFact::Eq(span.clone(), exprs.iter().map(f).collect())
+ }
+ GenericFact::Fact(expr) => GenericFact::Fact(f(expr)),
+ }
+ }
+
+ pub(crate) fn subst<Leaf2, Head2>(
+ &self,
+ subst_leaf: &mut impl FnMut(&Span, &Leaf) -> GenericExpr<Head2, Leaf2>,
+ subst_head: &mut impl FnMut(&Head) -> Head2,
+ ) -> GenericFact<Head2, Leaf2> {
+ self.map_exprs(&mut |e| e.subst(subst_leaf, subst_head))
+ }
+}
+
+impl<Head, Leaf> GenericFact<Head, Leaf>
+where
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+ Head: Clone + Display,
+{
+ pub(crate) fn make_unresolved(self) -> GenericFact<Symbol, Symbol>
+ where
+ Leaf: SymbolLike,
+ Head: SymbolLike,
+ {
+ self.subst(
+ &mut |span, v| GenericExpr::Var(span.clone(), v.to_symbol()),
+ &mut |h| h.to_symbol(),
+ )
+ }
+}
+
+impl<Head, Leaf> Display for GenericFact<Head, Leaf>
+where
+ Head: Display,
+ Leaf: Display,
+{
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_sexp())
+ }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct CorrespondingVar<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub head: Head,
+ pub to: Leaf,
+}
+
+impl<Head, Leaf> CorrespondingVar<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub fn new(head: Head, leaf: Leaf) -> Self {
+ Self { head, to: leaf }
+ }
+}
+
+impl<Head, Leaf> Display for CorrespondingVar<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{} -> {}", self.head, self.to)
+ }
+}
+
+#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash)]
+pub enum Change {
+ Delete,
+ Subsume,
+}
+
+pub type Action = GenericAction<Symbol, Symbol>;
+pub(crate) type MappedAction = GenericAction<CorrespondingVar<Symbol, Symbol>, Symbol>;
+pub(crate) type ResolvedAction = GenericAction<ResolvedCall, ResolvedVar>;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum GenericAction<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ Let(Span, Leaf, GenericExpr<Head, Leaf>),
+ Set(
+ Span,
+ Head,
+ Vec<GenericExpr<Head, Leaf>>,
+ GenericExpr<Head, Leaf>,
+ ),
+ Change(Span, Change, Head, Vec<GenericExpr<Head, Leaf>>),
+ Union(Span, GenericExpr<Head, Leaf>, GenericExpr<Head, Leaf>),
+ Extract(Span, GenericExpr<Head, Leaf>, GenericExpr<Head, Leaf>),
+ Panic(Span, String),
+ Expr(Span, GenericExpr<Head, Leaf>),
+ }
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+
+pub struct GenericActions<Head: Clone + Display, Leaf: Clone + PartialEq + Eq + Display + Hash>(
+ pub Vec<GenericAction<Head, Leaf>>,
+);
+pub type Actions = GenericActions<Symbol, Symbol>;
+pub(crate) type ResolvedActions = GenericActions<ResolvedCall, ResolvedVar>;
+pub(crate) type MappedActions<Head, Leaf> = GenericActions<CorrespondingVar<Head, Leaf>, Leaf>;
+
+impl<Head, Leaf> Default for GenericActions<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ fn default() -> Self {
+ Self(vec![])
+ }
+}
+
+impl<Head, Leaf> GenericActions<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub(crate) fn len(&self) -> usize {
+ self.0.len()
+ }
+
+ pub(crate) fn iter(&self) -> impl Iterator<Item = &GenericAction<Head, Leaf>> {
+ self.0.iter()
+ }
+
+ pub(crate) fn is_empty(&self) -> bool {
+ self.0.is_empty()
+ }
+
+ pub(crate) fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ Self(self.0.into_iter().map(|a| a.visit_exprs(f)).collect())
+ }
+}
+
+impl<Head, Leaf> ToSexp for GenericAction<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn to_sexp(&self) -> Sexp {
+ match self {
+ GenericAction::Let(_ann, lhs, rhs) => list!("let", lhs, rhs),
+ GenericAction::Set(_ann, lhs, args, rhs) => list!("set", list!(lhs, ++ args), rhs),
+ GenericAction::Union(_ann, lhs, rhs) => list!("union", lhs, rhs),
+ GenericAction::Change(_ann, change, lhs, args) => {
+ list!(
+ match change {
+ Change::Delete => "delete",
+ Change::Subsume => "subsume",
+ },
+ list!(lhs, ++ args)
+ )
+ }
+ GenericAction::Extract(_ann, expr, variants) => list!("extract", expr, variants),
+ GenericAction::Panic(_ann, msg) => list!("panic", format!("\"{}\"", msg.clone())),
+ GenericAction::Expr(_ann, e) => e.to_sexp(),
+ }
+ }
+}
+
+impl<Head, Leaf> GenericAction<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + Eq + Display + Hash,
+{
+ pub fn map_exprs(
+ &self,
+ f: &mut impl FnMut(&GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ match self {
+ GenericAction::Let(span, lhs, rhs) => {
+ GenericAction::Let(span.clone(), lhs.clone(), f(rhs))
+ }
+ GenericAction::Set(span, lhs, args, rhs) => {
+ let right = f(rhs);
+ GenericAction::Set(
+ span.clone(),
+ lhs.clone(),
+ args.iter().map(f).collect(),
+ right,
+ )
+ }
+ GenericAction::Change(span, change, lhs, args) => GenericAction::Change(
+ span.clone(),
+ *change,
+ lhs.clone(),
+ args.iter().map(f).collect(),
+ ),
+ GenericAction::Union(span, lhs, rhs) => {
+ GenericAction::Union(span.clone(), f(lhs), f(rhs))
+ }
+ GenericAction::Extract(span, expr, variants) => {
+ GenericAction::Extract(span.clone(), f(expr), f(variants))
+ }
+ GenericAction::Panic(span, msg) => GenericAction::Panic(span.clone(), msg.clone()),
+ GenericAction::Expr(span, e) => GenericAction::Expr(span.clone(), f(e)),
+ }
+ }
+
+ pub fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ match self {
+ GenericAction::Let(span, lhs, rhs) => {
+ GenericAction::Let(span, lhs.clone(), rhs.visit_exprs(f))
+ }
+ GenericAction::Set(span, lhs, args, rhs) => {
+ let args = args.into_iter().map(|e| e.visit_exprs(f)).collect();
+ GenericAction::Set(span, lhs.clone(), args, rhs.visit_exprs(f))
+ }
+ GenericAction::Change(span, change, lhs, args) => {
+ let args = args.into_iter().map(|e| e.visit_exprs(f)).collect();
+ GenericAction::Change(span, change, lhs.clone(), args)
+ }
+ GenericAction::Union(span, lhs, rhs) => {
+ GenericAction::Union(span, lhs.visit_exprs(f), rhs.visit_exprs(f))
+ }
+ GenericAction::Extract(span, expr, variants) => {
+ GenericAction::Extract(span, expr.visit_exprs(f), variants.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(&Span, &Leaf) -> GenericExpr<Head, Leaf>) -> 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 {
+ () => {
+ |span, s: _| GenericExpr::Var(span.clone(), fvar(s.clone(), false))
+ };
+ }
+ match self {
+ GenericAction::Let(span, lhs, rhs) => {
+ let lhs = fvar(lhs, true);
+ let rhs = rhs.subst_leaf(&mut fvar_expr!());
+ GenericAction::Let(span, lhs, 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(span, lhs.clone(), args, rhs)
+ }
+ GenericAction::Change(span, change, lhs, args) => {
+ let args = args
+ .into_iter()
+ .map(|e| e.subst_leaf(&mut fvar_expr!()))
+ .collect();
+ GenericAction::Change(span, change, lhs.clone(), args)
+ }
+ GenericAction::Union(span, lhs, rhs) => {
+ let lhs = lhs.subst_leaf(&mut fvar_expr!());
+ let rhs = rhs.subst_leaf(&mut fvar_expr!());
+ GenericAction::Union(span, lhs, rhs)
+ }
+ GenericAction::Extract(span, expr, variants) => {
+ let expr = expr.subst_leaf(&mut fvar_expr!());
+ let variants = variants.subst_leaf(&mut fvar_expr!());
+ GenericAction::Extract(span, expr, variants)
+ }
+ GenericAction::Panic(span, msg) => GenericAction::Panic(span, msg.clone()),
+ GenericAction::Expr(span, e) => {
+ GenericAction::Expr(span, e.subst_leaf(&mut fvar_expr!()))
+ }
+ }
+ }
+}
+
+impl<Head, Leaf> Display for GenericAction<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_sexp())
+ }
+}
+
+#[derive(Clone, Debug)]
+pub(crate) struct CompiledRule {
+ pub(crate) query: CompiledQuery,
+ pub(crate) program: Program,
+}
+
+pub type Rule = GenericRule<Symbol, Symbol>;
+pub(crate) type ResolvedRule = GenericRule<ResolvedCall, ResolvedVar>;
+
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct GenericRule<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub span: Span,
+ pub head: GenericActions<Head, Leaf>,
+ pub body: Vec<GenericFact<Head, Leaf>>,
+}
+
+impl<Head, Leaf> GenericRule<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub(crate) fn visit_exprs(
+ self,
+ f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+ ) -> Self {
+ Self {
+ span: self.span,
+ head: self.head.visit_exprs(f),
+ body: self
+ .body
+ .into_iter()
+ .map(|bexpr| bexpr.visit_exprs(f))
+ .collect(),
+ }
+ }
+}
+
+impl<Head, Leaf> GenericRule<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ pub(crate) fn fmt_with_ruleset(
+ &self,
+ f: &mut std::fmt::Formatter<'_>,
+ ruleset: Symbol,
+ name: Symbol,
+ ) -> std::fmt::Result {
+ let indent = " ".repeat(7);
+ write!(f, "(rule (")?;
+ for (i, fact) in self.body.iter().enumerate() {
+ if i > 0 {
+ write!(f, "{}", indent)?;
+ }
+
+ if i != self.body.len() - 1 {
+ writeln!(f, "{}", fact)?;
+ } else {
+ write!(f, "{}", fact)?;
+ }
+ }
+ write!(f, ")\n (")?;
+ for (i, action) in self.head.0.iter().enumerate() {
+ if i > 0 {
+ write!(f, "{}", indent)?;
+ }
+ if i != self.head.0.len() - 1 {
+ writeln!(f, "{}", action)?;
+ } else {
+ write!(f, "{}", action)?;
+ }
+ }
+ let ruleset = if ruleset != "".into() {
+ format!(":ruleset {}", ruleset)
+ } else {
+ "".into()
+ };
+ let name = if name != "".into() {
+ format!(":name \"{}\"", name)
+ } else {
+ "".into()
+ };
+ write!(f, ")\n{} {} {})", indent, ruleset, name)
+ }
+}
+
+impl<Head, Leaf> GenericRule<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ pub fn to_sexp(&self, ruleset: Symbol, name: Symbol) -> Sexp {
+ let mut res = vec![
+ Sexp::Symbol("rule".into()),
+ Sexp::List(self.body.iter().map(|f| f.to_sexp()).collect()),
+ Sexp::List(self.head.0.iter().map(|a| a.to_sexp()).collect()),
+ ];
+ if ruleset != "".into() {
+ res.push(Sexp::Symbol(":ruleset".into()));
+ res.push(Sexp::Symbol(ruleset.to_string()));
+ }
+ if name != "".into() {
+ res.push(Sexp::Symbol(":name".into()));
+ res.push(Sexp::Symbol(format!("\"{}\"", name)));
+ }
+ Sexp::List(res)
+ }
+}
+
+impl<Head, Leaf> Display for GenericRule<Head, Leaf>
+where
+ Head: Clone + Display + ToSexp,
+ Leaf: Clone + PartialEq + Eq + Display + Hash + ToSexp,
+{
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ self.fmt_with_ruleset(f, "".into(), "".into())
+ }
+}
+
+pub type Rewrite = GenericRewrite<Symbol, Symbol>;
+
+#[derive(Clone, Debug)]
+pub struct GenericRewrite<Head, Leaf> {
+ pub span: Span,
+ pub lhs: GenericExpr<Head, Leaf>,
+ pub rhs: GenericExpr<Head, Leaf>,
+ pub conditions: Vec<GenericFact<Head, Leaf>>,
+}
+
+impl<Head: Display, Leaf: Display> GenericRewrite<Head, Leaf> {
+ pub fn to_sexp(&self, ruleset: Symbol, is_bidirectional: bool, subsume: bool) -> Sexp {
+ let mut res = vec![
+ Sexp::Symbol(if is_bidirectional {
+ "birewrite".into()
+ } else {
+ "rewrite".into()
+ }),
+ self.lhs.to_sexp(),
+ self.rhs.to_sexp(),
+ ];
+ if subsume {
+ res.push(Sexp::Symbol(":subsume".into()));
+ }
+
+ if !self.conditions.is_empty() {
+ res.push(Sexp::Symbol(":when".into()));
+ res.push(Sexp::List(
+ self.conditions.iter().map(|f| f.to_sexp()).collect(),
+ ));
+ }
+
+ if ruleset != "".into() {
+ res.push(Sexp::Symbol(":ruleset".into()));
+ res.push(Sexp::Symbol(ruleset.to_string()));
+ }
+ Sexp::List(res)
+ }
+}
+
+impl<Head: Display, Leaf: Display> Display for GenericRewrite<Head, Leaf> {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "{}", self.to_sexp("".into(), false, false))
+ }
+}
+
+impl<Head, Leaf: Clone> MappedExpr<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub(crate) fn get_corresponding_var_or_lit(&self, typeinfo: &TypeInfo) -> GenericAtomTerm<Leaf>
+ where
+ Leaf: SymbolLike,
+ {
+ match self {
+ GenericExpr::Var(span, v) => {
+ if typeinfo.is_global(v.to_symbol()) {
+ GenericAtomTerm::Global(span.clone(), v.clone())
+ } else {
+ GenericAtomTerm::Var(span.clone(), v.clone())
+ }
+ }
+ GenericExpr::Lit(span, lit) => GenericAtomTerm::Literal(span.clone(), lit.clone()),
+ GenericExpr::Call(span, head, _) => GenericAtomTerm::Var(span.clone(), head.to.clone()),
+ }
+ }
+}
+
+impl<Head, Leaf> GenericActions<Head, Leaf>
+where
+ Head: Clone + Display,
+ Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+ pub fn new(actions: Vec<GenericAction<Head, Leaf>>) -> Self {
+ Self(actions)
+ }
+
+ pub fn singleton(action: GenericAction<Head, Leaf>) -> Self {
+ Self(vec![action])
+ }
+}
+
