Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Distinguish datatypes from other tables #223

Merged
merged 8 commits into from
Sep 12, 2023
Merged

Distinguish datatypes from other tables #223

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
0acee28
desugar function declarations
oflatt Sep 3, 2023
18aaaf2
get rid of unit
oflatt Sep 3, 2023
7f4b58e
Merge branch 'oflatt-desugar-merge-action' into oflatt-distinguish-da…
oflatt Sep 3, 2023
9d47f2c
okay we still need unit
oflatt Sep 3, 2023
8f78900
make unit work again- as well as reading datatypes
oflatt Sep 3, 2023
b6fe9c4
enforce difference between set and union
oflatt Sep 3, 2023
5d47d73
sprinkle a little docs
oflatt Sep 3, 2023
f6df3ff
writle a little documentation
oflatt Sep 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 22 additions & 5 deletions src/ast/desugar.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ fn desugar_datatype(name: Symbol, variants: Vec<Variant>) -> Vec<NCommand> {
vec![NCommand::Sort(name, None)]
.into_iter()
.chain(variants.into_iter().map(|variant| {
NCommand::Function(FunctionDecl {
NCommand::Function(NormFunctionDecl {
name: variant.name,
schema: Schema {
input: variant.types,
Expand Down Expand Up @@ -513,6 +513,9 @@ pub(crate) fn rewrite_name(rewrite: &Rewrite) -> String {
rewrite.to_string().replace('\"', "'")
}

/// Desugars a single command into the normalized form.
/// Gets rid of a bunch of syntactic sugar, but also
/// makes rules into a SSA-like format (see [`NormFact`]).
pub(crate) fn desugar_command(
command: Command,
desugar: &mut Desugar,
Expand All @@ -523,9 +526,11 @@ pub(crate) fn desugar_command(
Command::SetOption { name, value } => {
vec![NCommand::SetOption { name, value }]
}
Command::Function(fdecl) => {
vec![NCommand::Function(fdecl)]
}
Command::Function(fdecl) => desugar.desugar_function(&fdecl),
Command::Relation {
constructor,
inputs,
} => desugar.desugar_function(&FunctionDecl::relation(constructor, inputs)),
Command::Declare { name, sort } => desugar.declare(name, sort),
Command::Datatype { name, variants } => desugar_datatype(name, variants),
Command::Rewrite(ruleset, rewrite) => {
Expand Down Expand Up @@ -781,7 +786,7 @@ impl Desugar {
pub fn declare(&mut self, name: Symbol, sort: Symbol) -> Vec<NCommand> {
let fresh = self.get_fresh();
vec![
NCommand::Function(FunctionDecl {
NCommand::Function(NormFunctionDecl {
name: fresh,
schema: Schema {
input: vec![],
Expand All @@ -796,4 +801,16 @@ impl Desugar {
NCommand::NormAction(NormAction::Let(name, NormExpr::Call(fresh, vec![]))),
]
}

pub fn desugar_function(&mut self, fdecl: &FunctionDecl) -> Vec<NCommand> {
vec![NCommand::Function(NormFunctionDecl {
name: fdecl.name,
schema: fdecl.schema.clone(),
default: fdecl.default.clone(),
merge: fdecl.merge.clone(),
merge_action: flatten_actions(&fdecl.merge_action, self),
cost: fdecl.cost,
unextractable: fdecl.unextractable,
})]
}
}
72 changes: 68 additions & 4 deletions src/ast/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ pub enum NCommand {
value: Expr,
},
Sort(Symbol, Option<(Symbol, Vec<Expr>)>),
Function(FunctionDecl),
Function(NormFunctionDecl),
AddRuleset(Symbol),
NormRule {
name: Symbol,
Expand Down Expand Up @@ -132,7 +132,7 @@ impl NCommand {
value: value.clone(),
},
NCommand::Sort(name, params) => Command::Sort(*name, params.clone()),
NCommand::Function(f) => Command::Function(f.clone()),
NCommand::Function(f) => Command::Function(f.to_fdecl()),
NCommand::AddRuleset(name) => Command::AddRuleset(*name),
NCommand::NormRule {
name,
Expand Down Expand Up @@ -335,7 +335,29 @@ pub enum Command {
sort: Symbol,
},
Sort(Symbol, Option<(Symbol, Vec<Expr>)>),
/// Declare an egglog function.
/// The function is a datatype when:
/// - The output is not a primitive
/// - No merge function is provided
/// - No default is provided
Function(FunctionDecl),
Comment on lines +340 to 343
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh I wasn't aware you could have functions with non primitive return values and custom merge functions...

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's currently a very under-tested feature! I plan to use it more in the future though, it's essential for encoding proofs.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It can be used to simulate the choice construct in Datalog literature by setting :merge old (as is used in proofs)

/// Declare an egglog relation, which is simply sugar
/// for a function returning the `Unit` type.
/// Example:
/// ```lisp
/// (relation path (i64 i64))
/// (relation edge (i64 i64))
/// ```

/// Desugars to:
/// ```lisp
/// (function path (i64 i64) Unit :default ())
/// (function edge (i64 i64) Unit :default ())
/// ```
Relation {
constructor: Symbol,
inputs: Vec<Symbol>,
},
AddRuleset(Symbol),
Rule {
name: Symbol,
Expand Down Expand Up @@ -387,6 +409,10 @@ impl ToSexp for Command {
Command::Sort(name, None) => list!("sort", name),
Command::Sort(name, Some((name2, args))) => list!("sort", name, list!( name2, ++ args)),
Command::Function(f) => f.to_sexp(),
Command::Relation {
constructor,
inputs,
} => list!("relation", constructor, list!(++ inputs)),
Command::AddRuleset(name) => list!("ruleset", name),
Command::Rule {
name,
Expand Down Expand Up @@ -498,12 +524,43 @@ impl NormRunConfig {
}
}

/// A normalized function declaration- the desugared
/// version of a [`FunctionDecl`].
/// TODO so far only the merge action is normalized,
/// not the default value or merge expression.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct NormFunctionDecl {
pub name: Symbol,
pub schema: Schema,
// todo desugar default, merge
pub default: Option<Expr>,
pub merge: Option<Expr>,
pub merge_action: Vec<NormAction>,
pub cost: Option<usize>,
pub unextractable: bool,
}

impl NormFunctionDecl {
pub fn to_fdecl(&self) -> FunctionDecl {
FunctionDecl {
name: self.name,
schema: self.schema.clone(),
default: self.default.clone(),
merge: self.merge.clone(),
merge_action: self.merge_action.iter().map(|a| a.to_action()).collect(),
cost: self.cost,
unextractable: self.unextractable,
}
}
}

/// Represents the declaration of a function
/// directly parsed from source syntax.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct FunctionDecl {
pub name: Symbol,
pub schema: Schema,
pub default: Option<Expr>,
// TODO we should desugar merge and merge action
pub merge: Option<Expr>,
pub merge_action: Vec<Action>,
pub cost: Option<usize>,
Expand Down Expand Up @@ -559,7 +616,7 @@ impl FunctionDecl {
},
merge: None,
merge_action: vec![],
default: None,
default: Some(Expr::Lit(Literal::Unit)),
Comment on lines -562 to +619
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am curious why the relation now needs a default to work? It does make it a little more cumbersome to define relations with the function syntax. Would you ever want to define a function that returns Unit but doesn't have this as a default?

Copy link
Member Author

@oflatt oflatt Sep 8, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good question-
Unit is a primitive just like i64. Before, we had special logic for making default units, making them special in a weird way. Now, I make it explicit that the relation syntax is sugar for this function for convenience.

You can still have a function that returns Unit without this default and use set everywhere. But this is more convenient

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I see.

Is it true then that using a function that does not return a default as an action is a no-op? And that's why you needed the special case before and now with it removed you have added a default?

As a test, this rule seems to have no effect, when there is no default (based on the viz):

(datatype Expr)

(function trigger () Expr)

(function foo () i64)

(trigger)

(rule ((= x (trigger))) ((foo)))

(run 1)

But it does when there is a default:

(datatype Expr)

(function trigger () Expr)

(function foo () i64 : default 10)

(trigger)

(rule ((= x (trigger))) ((foo)))

(run 1)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, shouldn't you get an exception when there isn't a default?
Otherwise, the action might fail halfway-through!

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, so if I am understanding that correctly, only functions with defaults can be used as actions?

cost: None,
unextractable: false,
}
Expand Down Expand Up @@ -710,8 +767,15 @@ impl Display for Fact {
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Action {
Let(Symbol, Expr),
/// `set` a table to a particular result.
/// `set` should not be used on datatypes-
/// instead, use `union`.
Set(Symbol, Vec<Expr>, Expr),
Delete(Symbol, Vec<Expr>),
/// `union` two datatypes, making them equal
/// in the implicit, global equality relation
/// of egglog.
/// All rules match modulo this equality relation.
Union(Expr, Expr),
Extract(Expr, Expr),
Panic(String),
Expand Down
4 changes: 2 additions & 2 deletions src/ast/parse.lalrpop
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ Command: Command = {
Command::Function(FunctionDecl { name, schema, merge, merge_action: merge_action.unwrap_or_default(), default, cost, unextractable: unextractable.is_some() })
},
LParen "declare" <name:Ident> <sort:Ident> RParen => Command::Declare{name, sort},
LParen "relation" <name:Ident> <types:List<Type>> RParen => Command::Function(FunctionDecl::relation(name, types)),
LParen "relation" <constructor:Ident> <inputs:List<Type>> RParen => Command::Relation{constructor, inputs},
LParen "ruleset" <name:Ident> RParen => Command::AddRuleset(name),
LParen "rule" <body:List<Fact>> <head:List<Action>> <ruleset:(":ruleset" <Ident>)?> <name:(":name" <String>)?> RParen => Command::Rule{ruleset: ruleset.unwrap_or("".into()), name: name.unwrap_or("".to_string()).into(), rule: Rule { head, body }},
LParen "rewrite" <lhs:Expr> <rhs:Expr>
Expand Down Expand Up @@ -140,7 +140,7 @@ pub Expr: Expr = {
};

Literal: Literal = {
// "(" ")" => Literal::Unit, // shouldn't need unit literals for now
"(" ")" => Literal::Unit,
<Num> => Literal::Int(<>),
<F64> => Literal::F64(<>),
<SymString> => Literal::String(<>),
Expand Down
147 changes: 69 additions & 78 deletions src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -440,8 +440,8 @@ impl EGraph {
self.unionfind.n_unions() - n_unions + function.clear_updates()
}

pub fn declare_function(&mut self, decl: &FunctionDecl) -> Result<(), Error> {
let function = Function::new(self, decl)?;
pub fn declare_function(&mut self, decl: &NormFunctionDecl) -> Result<(), Error> {
let function = Function::new(self, &decl.to_fdecl())?;
let old = self.functions.insert(decl.name, function);
if old.is_some() {
panic!(
Expand All @@ -453,31 +453,6 @@ impl EGraph {
Ok(())
}

pub fn declare_constructor(
&mut self,
variant: Variant,
sort: impl Into<Symbol>,
) -> Result<(), Error> {
let name = variant.name;
let sort = sort.into();
self.declare_function(&FunctionDecl {
name,
schema: Schema {
input: variant.types,
output: sort,
},
merge: None,
merge_action: vec![],
default: None,
cost: variant.cost,
unextractable: false,
})?;
// if let Some(ctors) = self.sorts.get_mut(&sort) {
// ctors.push(name);
// }
Ok(())
}

pub fn eval_lit(&self, lit: &Literal) -> Value {
match lit {
Literal::Int(i) => i.store(&self.type_info().get_sort()).unwrap(),
Expand Down Expand Up @@ -1034,57 +1009,7 @@ impl EGraph {
}
}
NCommand::Input { name, file } => {
let func = self.functions.get_mut(&name).unwrap();
let is_unit = func.schema.output.name().as_str() == "Unit";

let mut filename = self.fact_directory.clone().unwrap_or_default();
filename.push(file.as_str());

// check that the function uses supported types
for t in &func.schema.input {
match t.name().as_str() {
"i64" | "String" => {}
s => panic!("Unsupported type {} for input", s),
}
}
match func.schema.output.name().as_str() {
"i64" | "String" | "Unit" => {}
s => panic!("Unsupported type {} for input", s),
}

log::info!("Opening file '{:?}'...", filename);
let mut f = File::open(filename).unwrap();
let mut contents = String::new();
f.read_to_string(&mut contents).unwrap();

let mut actions: Vec<Action> = vec![];
let mut str_buf: Vec<&str> = vec![];
for line in contents.lines() {
str_buf.clear();
str_buf.extend(line.split('\t').map(|s| s.trim()));
if str_buf.is_empty() {
continue;
}

let parse = |s: &str| -> Expr {
if let Ok(i) = s.parse() {
Expr::Lit(Literal::Int(i))
} else {
Expr::Lit(Literal::String(s.into()))
}
};

let mut exprs: Vec<Expr> = str_buf.iter().map(|&s| parse(s)).collect();

actions.push(if is_unit {
Action::Expr(Expr::Call(name, exprs))
} else {
let out = exprs.pop().unwrap();
Action::Set(name, exprs, out)
});
}
self.eval_actions(&actions)?;
log::info!("Read {} facts into {name} from '{file}'.", actions.len())
self.input_file(name, file)?;
}
NCommand::Output { file, exprs } => {
let mut filename = self.fact_directory.clone().unwrap_or_default();
Expand All @@ -1111,6 +1036,72 @@ impl EGraph {
Ok(())
}

fn input_file(&mut self, name: Symbol, file: String) -> Result<(), Error> {
let function_type = self
.type_info()
.func_types
.get(&name)
.unwrap_or_else(|| panic!("Unrecognzed function name {}", name))
.clone();
let func = self.functions.get_mut(&name).unwrap();

let mut filename = self.fact_directory.clone().unwrap_or_default();
filename.push(file.as_str());

// check that the function uses supported types

for t in &func.schema.input {
match t.name().as_str() {
"i64" | "String" => {}
s => panic!("Unsupported type {} for input", s),
}
}

if !function_type.is_datatype {
match func.schema.output.name().as_str() {
"i64" | "String" | "Unit" => {}
s => panic!("Unsupported type {} for input", s),
}
}

log::info!("Opening file '{:?}'...", filename);
let mut f = File::open(filename).unwrap();
let mut contents = String::new();
f.read_to_string(&mut contents).unwrap();

let mut actions: Vec<Action> = vec![];
let mut str_buf: Vec<&str> = vec![];
for line in contents.lines() {
str_buf.clear();
str_buf.extend(line.split('\t').map(|s| s.trim()));
if str_buf.is_empty() {
continue;
}

let parse = |s: &str| -> Expr {
if let Ok(i) = s.parse() {
Expr::Lit(Literal::Int(i))
} else {
Expr::Lit(Literal::String(s.into()))
}
};

let mut exprs: Vec<Expr> = str_buf.iter().map(|&s| parse(s)).collect();

actions.push(
if function_type.is_datatype || function_type.output.name() == UNIT_SYM.into() {
Action::Expr(Expr::Call(name, exprs))
} else {
let out = exprs.pop().unwrap();
Action::Set(name, exprs, out)
},
);
}
self.eval_actions(&actions)?;
log::info!("Read {} facts into {name} from '{file}'.", actions.len());
Ok(())
}

pub fn clear(&mut self) {
for f in self.functions.values_mut() {
f.clear();
Expand Down
Loading