Skip to content

Commit

Permalink
Fix support for nullary unstable functions
Browse files Browse the repository at this point in the history
This resolves egraphs-good#382 by adding parsing support for defining sorts of 0 argument
unstable functions.

It does this by handling that input `()` as the `Unit` constructor.

If we ever want to remove the Unit constructor, we could move the return type
to the list of argument types, to make sure it always has at least one value.

This would also make parsing it more similar to other datatypes.

For now I just kept it the same to make the change minimal.
  • Loading branch information
saulshanabrook committed Jun 6, 2024
1 parent fb4a9f1 commit 0c0c6ae
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 20 deletions.
41 changes: 25 additions & 16 deletions src/sort/fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -62,27 +62,36 @@ impl FunctionSort {
name: Symbol,
args: &[Expr],
) -> Result<ArcSort, TypeError> {
if let [Expr::Call((), first, rest_args), Expr::Var((), output)] = args {
if let [inputs, Expr::Var((), output)] = args {
let output_sort = typeinfo
.sorts
.get(output)
.ok_or(TypeError::UndefinedSort(*output))?;
let all_args = once(first).chain(rest_args.iter().map(|arg| {
if let Expr::Var((), arg) = arg {
arg
} else {
panic!("function sort must be called with list of input sorts");

let input_sorts = match inputs {
Expr::Call((), first, rest_args) => {
let all_args = once(first).chain(rest_args.iter().map(|arg| {
if let Expr::Var((), arg) = arg {
arg
} else {
panic!("function sort must be called with list of input sorts");
}
}));
all_args
.map(|arg| {
typeinfo
.sorts
.get(arg)
.ok_or(TypeError::UndefinedSort(*arg))
.map(|s| s.clone())
})
.collect::<Result<Vec<_>, _>>()?
}
}));
let input_sorts = all_args
.map(|arg| {
typeinfo
.sorts
.get(arg)
.ok_or(TypeError::UndefinedSort(*arg))
.map(|s| s.clone())
})
.collect::<Result<Vec<_>, _>>()?;
// an empty list of inputs args is parsed as a unit literal
Expr::Lit((), Literal::Unit) => vec![],
_ => panic!("function sort must be called with list of input sorts"),
};

Ok(Arc::new(Self {
name,
inputs: input_sorts,
Expand Down
11 changes: 7 additions & 4 deletions tests/unstable-fn.egg
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@

(let x (Cons (Num 1) (Cons (Num 2) (Cons (Num 3) (Nil)))))
(let squared-x (list-map-math x square-fn))
(run 100)
(run-schedule (saturate (run)))
(check (= squared-x (Cons (Num 1) (Cons (Num 4) (Cons (Num 9) (Nil))))))

;; Test that we can partially apply a function in a rewrite rule
Expand All @@ -39,7 +39,7 @@
(rewrite (list-multiply-by l i) (list-map-math l (unstable-fn "Mul" i)))

(let doubled-x (list-multiply-by x (Num 2)))
(run 100)
(run-schedule (saturate (run)))
(check (= doubled-x (Cons (Num 2) (Cons (Num 4) (Cons (Num 6) (Nil))))))

;; Test we can define a higher order compose function
Expand All @@ -50,7 +50,7 @@
(let square-of-double (unstable-fn "composed-math" square-fn (unstable-fn "Mul" (Num 2))))

(let squared-doubled-x (list-map-math x square-of-double))
(run 100)
(run-schedule (saturate (run)))
(check (= squared-doubled-x (Cons (Num 4) (Cons (Num 16) (Cons (Num 36) (Nil))))))


Expand All @@ -61,5 +61,8 @@
(rewrite (composed-i64-math f g v) (unstable-app f (Num (unstable-app g v))))

(let res (composed-i64-math square-fn (unstable-fn "*" 2) 4))
(run 100)
(run-schedule (saturate (run)))
(check (= res (Num 64)))

;; Verify that function parsing works with a function with no args
(sort TestNullaryFunction (UnstableFn () Math))

0 comments on commit 0c0c6ae

Please sign in to comment.