diff --git a/Cargo.lock b/Cargo.lock index 7fb4336..1ae1a16 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -330,7 +330,7 @@ checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" [[package]] name = "egglog" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "chrono", "clap", @@ -362,7 +362,7 @@ dependencies = [ [[package]] name = "egglog-add-primitive" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "quote", "syn 2.0.108", @@ -371,7 +371,7 @@ dependencies = [ [[package]] name = "egglog-ast" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "ordered-float", ] @@ -379,7 +379,7 @@ dependencies = [ [[package]] name = "egglog-bridge" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "anyhow", "dyn-clone", @@ -402,7 +402,7 @@ dependencies = [ [[package]] name = "egglog-concurrency" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "arc-swap", "bumpalo", @@ -414,7 +414,7 @@ dependencies = [ [[package]] name = "egglog-core-relations" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "anyhow", "bumpalo", @@ -457,7 +457,7 @@ dependencies = [ [[package]] name = "egglog-numeric-id" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "rayon", ] @@ -465,7 +465,7 @@ dependencies = [ [[package]] name = "egglog-reports" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "clap", "hashbrown 0.16.0", @@ -479,7 +479,7 @@ dependencies = [ [[package]] name = "egglog-union-find" version = "2.0.0" -source = "git+https://github.com/egraphs-good/egglog.git?rev=a2da717fd2f5eb8e8cd7c68163e5a160da05e637#a2da717fd2f5eb8e8cd7c68163e5a160da05e637" +source = "git+https://github.com/egraphs-good/egglog.git?rev=5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd#5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd" dependencies = [ "crossbeam", "egglog-concurrency", diff --git a/Cargo.toml b/Cargo.toml index 944e6e7..52f260a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,9 +17,9 @@ default = ["bin"] bin = ["egglog/bin"] [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog.git", rev = "a2da717fd2f5eb8e8cd7c68163e5a160da05e637", default-features = false } -egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", rev = "a2da717fd2f5eb8e8cd7c68163e5a160da05e637", default-features = false } -egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", rev = "a2da717fd2f5eb8e8cd7c68163e5a160da05e637", default-features = false } +egglog = { git = "https://github.com/egraphs-good/egglog.git", rev = "5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd", default-features = false } +egglog-ast = { git = "https://github.com/egraphs-good/egglog.git", rev = "5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd", default-features = false } +egglog-reports = { git = "https://github.com/egraphs-good/egglog.git", rev = "5294cdc66a7b90a9a1480cb2d930f2ee5785c8dd", default-features = false } num = "0.4.3" lazy_static = "1.4" diff --git a/src/lib.rs b/src/lib.rs index 806576f..79c2907 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -19,6 +19,15 @@ //! - [`(get-size!)` primitive](https://github.com/egraphs-good/egglog-experimental/blob/main/tests/web-demo/node-limit.egg) //! for inspecting total tuple counts or counts for specific tables //! - [Multi-extraction](https://github.com/egraphs-good/egglog-experimental/blob/main/tests/web-demo/multi-extract.egg) +//! - Body-defined primitives with `(primitive name (InputSort*) OutputSort body)`. +//! Body variables are positional (`_0`, `_1`, ...), and a partial primitive +//! body result propagates as primitive failure. The registered primitive uses +//! the minimum capability needed by its body (`pure`, `read`, `write`, or +//! `full`). Bodies may call built-in or previously registered primitives, +//! table-backed functions, and globals; applying those primitives is allowed +//! only in a compatible runtime context. A global reference makes the defined +//! primitive read-capable because globals lower to zero-argument function +//! lookups. //! //! Each bullet links to a runnable demo so you can explore the feature quickly. //! The rest of this crate exposes the Rust APIs and helpers that back these extensions. @@ -40,6 +49,7 @@ mod multi_extract; pub use multi_extract::*; mod size; pub use size::*; +mod primitive; mod table_stats; pub use table_stats::*; @@ -92,6 +102,9 @@ pub fn new_experimental_egraph() -> EGraph { .add_command("print-table-stats".into(), Arc::new(PrintTableStatsCommand)) .unwrap(); egraph + .add_command("primitive".into(), Arc::new(primitive::RegisterPrimitive)) + .unwrap(); + egraph } // Create a parser with experimental macros diff --git a/src/primitive.rs b/src/primitive.rs new file mode 100644 index 0000000..d92704a --- /dev/null +++ b/src/primitive.rs @@ -0,0 +1,290 @@ +use egglog::ast::{Expr, FunctionSubtype, Literal}; +use egglog::constraint::SimpleTypeConstraint; +use egglog::prelude::Span; +use egglog::sort::FunctionSort; +use egglog::{ + ArcSort, CommandOutput, Context, Core, EGraph, Error, FullPrim, FullState, Primitive, PurePrim, + PureState, ReadPrim, ReadState, ResolvedCall, ResolvedExpr, TypeError, UserDefinedCommand, + Value, WritePrim, WriteState, +}; +use std::sync::Arc; + +pub(crate) struct RegisterPrimitive; + +impl UserDefinedCommand for RegisterPrimitive { + fn update(&self, egraph: &mut EGraph, args: &[Expr]) -> Result, Error> { + if args.len() != 4 { + return Err(backend_error( + args.first().map(Expr::span).unwrap_or_else(|| Span::Panic), + format!("primitive expects 4 arguments, got {}", args.len()), + )); + } + + let (name_span, name) = decode_atom(&args[0], "primitive name")?; + ensure_name_available(egraph, &name, &name_span)?; + + let input_sort_names = decode_input_sort_names(&args[1])?; + let input_var_names: Vec<_> = (0..input_sort_names.len()) + .map(|index| format!("_{index}")) + .collect(); + + let input_sorts = input_sort_names + .iter() + .map(|(span, sort_name)| resolve_sort(egraph, sort_name, span)) + .collect::, _>>()?; + let (output_span, output_name) = decode_atom(&args[2], "output sort")?; + let output_sort = resolve_sort(egraph, &output_name, &output_span)?; + + let bindings: Vec<_> = input_var_names + .iter() + .zip(&input_sorts) + .map(|(name, sort)| (name.clone(), args[3].span(), sort.clone())) + .collect(); + + let mut last_error = None; + let mut typechecked_body = None; + for context in [Context::Pure, Context::Read, Context::Write, Context::Full] { + match egraph.typecheck_expr_with_bindings_and_output( + &args[3], + &bindings, + output_sort.clone(), + context, + ) { + Ok(resolved) + if matches!( + (required_context(egraph, &resolved), context), + (Context::Pure, _) + | (Context::Read, Context::Read | Context::Full) + | (Context::Write, Context::Write | Context::Full) + | (Context::Full, Context::Full) + ) => + { + typechecked_body = Some((resolved, context)); + break; + } + Ok(_) => {} + Err(err) => last_error = Some(err), + } + } + let Some((body, context)) = typechecked_body else { + return Err(last_error + .expect("primitive body typechecking always tries at least one context") + .into()); + }; + + let (body, hidden_bindings) = egraph.prepare_unstable_fn_targets_for_eval(&body)?; + let primitive = DefinedPrimitive { + name, + input_vars: input_var_names, + input: input_sorts, + output: output_sort, + body, + hidden_bindings, + }; + match context { + Context::Pure => egraph.add_pure_primitive(primitive, None), + Context::Read => egraph.add_read_primitive(primitive, None), + Context::Write => egraph.add_write_primitive(primitive, None), + Context::Full => egraph.add_full_primitive(primitive, None), + } + Ok(vec![]) + } +} + +#[derive(Clone)] +struct DefinedPrimitive { + name: String, + input_vars: Vec, + input: Vec, + output: ArcSort, + body: ResolvedExpr, + hidden_bindings: Vec<(String, Value)>, +} + +impl Primitive for DefinedPrimitive { + fn name(&self) -> &str { + &self.name + } + + fn get_type_constraints(&self, span: &Span) -> Box { + let mut sorts = self.input.clone(); + sorts.push(self.output.clone()); + SimpleTypeConstraint::new(self.name(), sorts, span.clone()).into_box() + } +} + +impl PurePrim for DefinedPrimitive { + fn apply<'a, 'db>(&self, mut state: PureState<'a, 'db>, args: &[Value]) -> Option { + self.eval(&mut state, args) + } +} + +impl ReadPrim for DefinedPrimitive { + fn apply<'a, 'db>(&self, mut state: ReadState<'a, 'db>, args: &[Value]) -> Option { + self.eval(&mut state, args) + } +} + +impl WritePrim for DefinedPrimitive { + fn apply<'a, 'db>(&self, mut state: WriteState<'a, 'db>, args: &[Value]) -> Option { + self.eval(&mut state, args) + } +} + +impl FullPrim for DefinedPrimitive { + fn apply<'a, 'db>(&self, mut state: FullState<'a, 'db>, args: &[Value]) -> Option { + self.eval(&mut state, args) + } +} + +impl DefinedPrimitive { + fn eval<'a, 'db>(&self, state: &mut impl Core<'a, 'db>, args: &[Value]) -> Option + where + 'db: 'a, + { + let mut bindings: Vec<_> = self + .hidden_bindings + .iter() + .map(|(name, value)| (name.as_str(), *value)) + .collect(); + bindings.extend( + self.input_vars + .iter() + .map(String::as_str) + .zip(args.iter().copied()), + ); + state.eval_resolved_expr(&self.body, &bindings) + } +} + +fn decode_atom(expr: &Expr, position: &str) -> Result<(Span, String), Error> { + match expr { + Expr::Var(span, name) => Ok((span.clone(), name.clone())), + _ => Err(backend_error( + expr.span(), + format!("{position} must be an atom"), + )), + } +} + +fn decode_input_sort_names(expr: &Expr) -> Result, Error> { + match expr { + Expr::Lit(_, Literal::Unit) => Ok(vec![]), + Expr::Var(span, name) => Ok(vec![(span.clone(), name.clone())]), + Expr::Call(span, head, args) => { + let mut names = Vec::with_capacity(args.len() + 1); + names.push((span.clone(), head.clone())); + for arg in args { + match arg { + Expr::Var(arg_span, name) => names.push((arg_span.clone(), name.clone())), + _ => { + return Err(backend_error( + arg.span(), + "input sort list must only contain sort atoms".to_string(), + )); + } + } + } + Ok(names) + } + _ => Err(backend_error( + expr.span(), + "input sort list must be (), a sort atom, or a flat list of sort atoms".to_string(), + )), + } +} + +fn ensure_name_available(egraph: &mut EGraph, name: &str, span: &Span) -> Result<(), Error> { + if egraph.get_sort_by_name(name).is_some() { + return Err(TypeError::SortAlreadyBound(name.to_owned(), span.clone()).into()); + } + if egraph.type_info().get_func_type(name).is_some() { + return Err(TypeError::FunctionAlreadyBound(name.to_owned(), span.clone()).into()); + } + if egraph.type_info().get_prims(name).is_some() { + return Err(TypeError::PrimitiveAlreadyBound(name.to_owned(), span.clone()).into()); + } + Ok(()) +} + +fn resolve_sort(egraph: &EGraph, name: &str, span: &Span) -> Result { + egraph + .get_sort_by_name(name) + .cloned() + .ok_or_else(|| TypeError::UndefinedSort(name.to_owned(), span.clone()).into()) +} + +fn required_context(egraph: &mut EGraph, expr: &ResolvedExpr) -> Context { + match expr { + ResolvedExpr::Lit(_, _) | ResolvedExpr::Var(_, _) => Context::Pure, + ResolvedExpr::Call(_, resolved_call, children) => { + let call_context = match resolved_call { + ResolvedCall::Primitive(primitive) if primitive.name() == "unstable-fn" => { + match children.first() { + Some(ResolvedExpr::Lit(_, Literal::String(name))) => { + let type_info = egraph.type_info(); + if let Some(func) = type_info.get_func_type(name) { + match func.subtype { + FunctionSubtype::Constructor => Context::Write, + FunctionSubtype::Custom => Context::Read, + } + } else if let Ok(fn_sort) = Arc::downcast::( + primitive.output().clone().as_arc_any(), + ) { + let types: Vec<_> = primitive + .input() + .iter() + .skip(1) + .cloned() + .chain(fn_sort.inputs().iter().cloned()) + .chain(std::iter::once(fn_sort.output())) + .collect(); + + let can_run_in = |context| { + type_info.get_prims(name).into_iter().flatten().any(|p| { + p.accept(&types, type_info) + && p.is_valid_in_context(context) + }) + }; + if can_run_in(Context::Pure) { + Context::Pure + } else if can_run_in(Context::Read) && !can_run_in(Context::Write) { + Context::Read + } else if can_run_in(Context::Write) && !can_run_in(Context::Read) { + Context::Write + } else { + Context::Full + } + } else { + Context::Full + } + } + _ => Context::Full, + } + } + ResolvedCall::Primitive(_) => Context::Pure, + ResolvedCall::Func(func) => match func.subtype { + FunctionSubtype::Constructor => Context::Write, + FunctionSubtype::Custom => Context::Read, + }, + }; + let mut context = call_context; + for child in children { + context = match (context, required_context(egraph, child)) { + (Context::Full, _) | (_, Context::Full) => Context::Full, + (Context::Read, Context::Write) | (Context::Write, Context::Read) => { + Context::Full + } + (Context::Read, _) | (_, Context::Read) => Context::Read, + (Context::Write, _) | (_, Context::Write) => Context::Write, + (Context::Pure, Context::Pure) => Context::Pure, + }; + } + context + } + } +} + +fn backend_error(span: Span, message: String) -> Error { + Error::BackendError(format!("{span}\n{message}")) +} diff --git a/tests/fail-typecheck/primitive-bad-positional-var.egg b/tests/fail-typecheck/primitive-bad-positional-var.egg new file mode 100644 index 0000000..452bdb2 --- /dev/null +++ b/tests/fail-typecheck/primitive-bad-positional-var.egg @@ -0,0 +1 @@ +(primitive bad (i64 i64) i64 (+ _0 _2)) diff --git a/tests/fail-typecheck/primitive-direct-function-body-in-rule.egg b/tests/fail-typecheck/primitive-direct-function-body-in-rule.egg new file mode 100644 index 0000000..939d37f --- /dev/null +++ b/tests/fail-typecheck/primitive-direct-function-body-in-rule.egg @@ -0,0 +1,6 @@ +(sort IntToInt (UnstableFn (i64) i64)) +(function f (i64) i64 :no-merge) +(relation R (i64)) + +(primitive apply-direct-fn (i64) i64 (unstable-app (unstable-fn "f") _0)) +(rule ((R x) (= y (apply-direct-fn x))) ((R y))) diff --git a/tests/fail-typecheck/primitive-global-body-in-seminaive-rule.egg b/tests/fail-typecheck/primitive-global-body-in-seminaive-rule.egg new file mode 100644 index 0000000..1c7bed2 --- /dev/null +++ b/tests/fail-typecheck/primitive-global-body-in-seminaive-rule.egg @@ -0,0 +1,6 @@ +(let $offset 1) +(relation Out (i64)) + +(primitive add-offset i64 i64 (+ _0 $offset)) + +(rule ((= x (add-offset 4))) ((Out x))) diff --git a/tests/fail-typecheck/primitive-hidden-table-dependency.egg b/tests/fail-typecheck/primitive-hidden-table-dependency.egg new file mode 100644 index 0000000..ccd02b3 --- /dev/null +++ b/tests/fail-typecheck/primitive-hidden-table-dependency.egg @@ -0,0 +1,14 @@ +;; Regression for a seminaive hidden dependency: this used to compile a call to +;; f inside via-f, so the rule depended only on via-f and missed later writes to f. +(function f (i64) i64 :no-merge) +(relation seed (i64)) +(relation out (i64)) + +(primitive via-f (i64) i64 (f _0)) + +(rule ((seed x)) ((out (via-f x)))) +(seed 1) +(run 1) +(set (f 1) 9) +(run 1) +(check (out 9)) diff --git a/tests/fail-typecheck/primitive-malformed-input-sorts.egg b/tests/fail-typecheck/primitive-malformed-input-sorts.egg new file mode 100644 index 0000000..8ca3a6b --- /dev/null +++ b/tests/fail-typecheck/primitive-malformed-input-sorts.egg @@ -0,0 +1 @@ +(primitive bad (i64 (i64)) i64 _0) diff --git a/tests/fail-typecheck/primitive-missing-unstable-fn-target.egg b/tests/fail-typecheck/primitive-missing-unstable-fn-target.egg new file mode 100644 index 0000000..0411699 --- /dev/null +++ b/tests/fail-typecheck/primitive-missing-unstable-fn-target.egg @@ -0,0 +1,2 @@ +(sort IntToInt (UnstableFn (i64) i64)) +(primitive bad (i64) i64 (unstable-app (unstable-fn "missing") _0)) diff --git a/tests/fail-typecheck/primitive-output-context-eqsort-mismatch.egg b/tests/fail-typecheck/primitive-output-context-eqsort-mismatch.egg new file mode 100644 index 0000000..f7bf1c4 --- /dev/null +++ b/tests/fail-typecheck/primitive-output-context-eqsort-mismatch.egg @@ -0,0 +1,2 @@ +(sort Math) +(primitive bad (i64) Math _0) diff --git a/tests/fail-typecheck/primitive-output-context-mismatch.egg b/tests/fail-typecheck/primitive-output-context-mismatch.egg new file mode 100644 index 0000000..ae79070 --- /dev/null +++ b/tests/fail-typecheck/primitive-output-context-mismatch.egg @@ -0,0 +1,2 @@ +(sort IntMap (Map i64 i64)) +(primitive bad () IntMap 1) diff --git a/tests/fail-typecheck/primitive-read-body-in-seminaive-rule.egg b/tests/fail-typecheck/primitive-read-body-in-seminaive-rule.egg new file mode 100644 index 0000000..2052573 --- /dev/null +++ b/tests/fail-typecheck/primitive-read-body-in-seminaive-rule.egg @@ -0,0 +1,7 @@ +(datatype Foo (MkFoo i64)) +(relation R (i64)) + +(primitive foo-size () i64 (get-size! "MkFoo")) + +(R 0) +(rule ((R x) (= n (foo-size))) ((R n))) diff --git a/tests/fail-typecheck/primitive-unresolved-body-symbol.egg b/tests/fail-typecheck/primitive-unresolved-body-symbol.egg new file mode 100644 index 0000000..5d169b4 --- /dev/null +++ b/tests/fail-typecheck/primitive-unresolved-body-symbol.egg @@ -0,0 +1 @@ +(primitive bad (i64) i64 (missing _0)) diff --git a/tests/primitive-constructor-body.egg b/tests/primitive-constructor-body.egg new file mode 100644 index 0000000..4b71bab --- /dev/null +++ b/tests/primitive-constructor-body.egg @@ -0,0 +1,7 @@ +(datatype Foo (MkFoo i64)) + +(primitive make-foo (i64) Foo (MkFoo _0)) + +(check (= (get-size! "MkFoo") 0)) +(let foo (make-foo 7)) +(check (= (get-size! "MkFoo") 1)) diff --git a/tests/primitive-function-container.egg b/tests/primitive-function-container.egg new file mode 100644 index 0000000..72d0c27 --- /dev/null +++ b/tests/primitive-function-container.egg @@ -0,0 +1,10 @@ +(sort IntToInt (UnstableFn (i64) i64)) +(function f (i64) i64 :no-merge) + +(primitive apply-fn (IntToInt i64) i64 (unstable-app _0 _1)) +(primitive apply-direct-fn (i64) i64 (unstable-app (unstable-fn "f") _0)) + +(set (f 1) 9) +(let $f (unstable-fn "f")) +(check (= (apply-fn $f 1) 9)) +(check (= (apply-direct-fn 1) 9)) diff --git a/tests/primitive-global-body.egg b/tests/primitive-global-body.egg new file mode 100644 index 0000000..a7a90b0 --- /dev/null +++ b/tests/primitive-global-body.egg @@ -0,0 +1,9 @@ +(let $offset 1) +(relation Out (i64)) + +(primitive add-offset i64 i64 (+ _0 $offset)) + +(check (= (add-offset 4) 5)) +(rule ((= x (add-offset 4))) ((Out x)) :naive) +(run 1) +(check (Out 5)) diff --git a/tests/primitive-map-empty-output-context.egg b/tests/primitive-map-empty-output-context.egg new file mode 100644 index 0000000..bc91351 --- /dev/null +++ b/tests/primitive-map-empty-output-context.egg @@ -0,0 +1,8 @@ +(sort IntMap (Map i64 i64)) +(primitive empty-int-map () IntMap (map-empty)) +(check (= (empty-int-map) (map-empty))) + +(sort Num) +(sort Map[Num,BigRat] (Map Num BigRat)) +(primitive empty-num-rat-map Unit Map[Num,BigRat] (map-empty)) +(check (= (empty-num-rat-map ()) (map-empty))) diff --git a/tests/primitive-overload-output-context.egg b/tests/primitive-overload-output-context.egg new file mode 100644 index 0000000..36f57f4 --- /dev/null +++ b/tests/primitive-overload-output-context.egg @@ -0,0 +1,5 @@ +(primitive add-float (f64 f64) f64 (+ _0 _1)) +(check (= (add-float 1.0 2.0) 3.0)) + +(primitive add-int (i64 i64) i64 (+ _0 _1)) +(check (= (add-int 1 2) 3)) diff --git a/tests/primitive-read-body.egg b/tests/primitive-read-body.egg new file mode 100644 index 0000000..be40cd3 --- /dev/null +++ b/tests/primitive-read-body.egg @@ -0,0 +1,7 @@ +(datatype Foo (MkFoo i64)) + +(primitive foo-size () i64 (get-size! "MkFoo")) +(check (= (foo-size) 0)) + +(MkFoo 1) +(check (= (foo-size) 1)) diff --git a/tests/primitive-table-backed-body.egg b/tests/primitive-table-backed-body.egg new file mode 100644 index 0000000..2195885 --- /dev/null +++ b/tests/primitive-table-backed-body.egg @@ -0,0 +1,11 @@ +(function f (i64) i64 :no-merge) +(relation out (i64)) + +(primitive via-f (i64) i64 (f _0)) + +(set (f 1) 9) +(check (= (via-f 1) 9)) + +(rule ((= x (via-f 1))) ((out x)) :naive) +(run 1) +(check (out 9)) diff --git a/tests/primitive.egg b/tests/primitive.egg new file mode 100644 index 0000000..c7b85dd --- /dev/null +++ b/tests/primitive.egg @@ -0,0 +1,13 @@ +(primitive add (i64 i64) i64 (+ _0 _1)) +(check (= (add 2 3) 5)) + +(primitive five () i64 5) +(check (= (five) 5)) + +(primitive add1-div (i64 i64) i64 (+ (/ _0 _1) 1)) +(check (= (add1-div 4 2) 3)) +(fail (check (= (add1-div 4 0) 0))) + +(sort IntMap (Map i64 i64)) +(primitive singleton-map (i64) IntMap (map-insert (map-empty) _0 (+ _0 1))) +(check (= (singleton-map 2) (map-insert (map-empty) 2 3)))