diff --git a/CHANGELOG.md b/CHANGELOG.md index 38a523588..15f7834c4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ - Add a BigRat to-i64 primitive for integral rationals. - Add f64 exp, log, and sqrt primitives. - Add `RunReport::can_stop` so scheduler progress can be reported separately from database updates. +- Add `EGraph::typecheck_expr_with_bindings_and_output`, `Core::eval_resolved_expr`, and `Core::apply_primitive` for body-defined primitive support, including normal command-path global rewrites for expressions typechecked through the helper. - Allow `unstable-fn` function containers to target primitive overloads. - Desugar `relation`s to `constructor`s to simplify the language and implementation. Relations no longer return unit `()` values. - Refactored API to use [`TermId`] more consistently instead of `Term` where possible, simplifying egglog code. diff --git a/src/ast/remove_globals.rs b/src/ast/remove_globals.rs index e1e77ac6d..15f0353f0 100644 --- a/src/ast/remove_globals.rs +++ b/src/ast/remove_globals.rs @@ -78,7 +78,7 @@ fn replace_global_vars(expr: ResolvedExpr) -> ResolvedExpr { } } -fn remove_globals_expr(expr: ResolvedExpr) -> ResolvedExpr { +pub(crate) fn remove_globals_expr(expr: ResolvedExpr) -> ResolvedExpr { expr.visit_exprs(&mut replace_global_vars) } diff --git a/src/exec_state.rs b/src/exec_state.rs index 70af56435..a8086f40f 100644 --- a/src/exec_state.rs +++ b/src/exec_state.rs @@ -36,6 +36,12 @@ use crate::core_relations::{ BaseValue, BaseValues, ContainerValue, ContainerValues, ExecutionState, ExternalFunctionId, TableId, Value, }; +use crate::{ + ast::{FunctionSubtype, Literal, ResolvedExpr}, + core::ResolvedCall, + sort::{F, S}, + typechecking::FuncType, +}; use egglog_bridge::{ActionRegistry, TableAction}; /// The four contexts a primitive may run in, named after the @@ -101,6 +107,26 @@ pub(crate) trait Internal<'a, 'db: 'a>: 'a { fn raw_exec_state(&mut self) -> &mut ExecutionState<'db> { self.es_mut() } + fn apply_resolved_function(&mut self, _func: &FuncType, _args: &[Value]) -> Option { + None + } + + fn apply_table_function( + &mut self, + subtype: FunctionSubtype, + action: &TableAction, + args: &[Value], + ) -> Option { + match (subtype, self.ctx()) { + (FunctionSubtype::Constructor, Context::Write | Context::Full) => { + action.lookup_or_insert(self.es_mut(), args) + } + (FunctionSubtype::Custom, Context::Read | Context::Full) => { + action.lookup(self.es(), args) + } + _ => None, + } + } } /// Sealed accessor for the [`ActionRegistry`]. Implemented by every @@ -197,6 +223,74 @@ pub trait Core<'a, 'db: 'a>: Internal<'a, 'db> { let mut pure = PureState::wrap(self.raw_exec_state(), ctx); fc.apply(&mut pure, args) } + + /// Dispatch an already type-specialized primitive in the current + /// call-site context. + /// + /// This is a trusted evaluator hook, not an authorization boundary: + /// callers must only pass primitives that were resolved for this same + /// call-site context and whose surrounding expression has already been + /// checked to require no more capability than this state wrapper provides. + /// For example, a primitive body evaluator should typecheck the body under + /// the runtime context it will register for, infer the body's required + /// context, and register the primitive using the matching state wrapper. + fn apply_primitive( + &mut self, + primitive: &crate::core::SpecializedPrimitive, + args: &[Value], + ) -> Option { + let id = primitive.external_id(self.ctx()); + self.es_mut().call_external_func(id, args) + } + + /// Evaluate an already typechecked expression in this primitive call + /// context, using `bindings` for local variables. + /// + /// Primitive calls dispatch through the current call-site context. + /// Table-backed function calls follow the same capability split as + /// `unstable-app`: custom functions require a read-capable state, + /// and constructors require a write-capable state that can mint on miss. + /// + /// This method assumes `expr` came from a trusted preparation pipeline that + /// typechecked it for this exact runtime context and rejected expressions + /// whose required capabilities exceed the receiver's state wrapper. It + /// should not be used to evaluate arbitrary resolved expressions from a + /// wider context inside a less-capable wrapper. + fn eval_resolved_expr( + &mut self, + expr: &ResolvedExpr, + bindings: &[(&str, Value)], + ) -> Option { + match expr { + ResolvedExpr::Lit(_, literal) => Some(match literal { + Literal::Int(x) => self.base_to_value(*x), + Literal::Float(x) => self.base_to_value(F::from(*x)), + Literal::String(x) => self.base_to_value(S::new(x.clone())), + Literal::Bool(x) => self.base_to_value(*x), + Literal::Unit => self.base_to_value(()), + }), + ResolvedExpr::Var(_, resolved_var) => { + assert!( + !resolved_var.is_global_ref, + "global variable {:?} reached direct expression evaluation before remove_globals", + resolved_var.name + ); + bindings + .iter() + .find_map(|(name, value)| (*name == resolved_var.name).then_some(*value)) + } + ResolvedExpr::Call(_, resolved_call, children) => { + let mut values = Vec::with_capacity(children.len()); + for child in children { + values.push(self.eval_resolved_expr(child, bindings)?); + } + match resolved_call { + ResolvedCall::Primitive(primitive) => self.apply_primitive(primitive, &values), + ResolvedCall::Func(func) => self.apply_resolved_function(func, &values), + } + } + } + } } /// Read-side methods — name-indexed table lookup. Implemented for @@ -270,6 +364,15 @@ fn lookup_action<'r>(registry: &'r ActionRegistry, name: &str) -> &'r TableActio .unwrap_or_else(|| panic!("missing table action for table: {name}")) } +fn apply_registered_function<'a, 'db: 'a>( + state: &mut impl RegistrySealed<'a, 'db>, + func: &FuncType, + args: &[Value], +) -> Option { + let action = lookup_action(state.registry(), &func.name).clone(); + state.apply_table_function(func.subtype, &action, args) +} + // ===================================================================== // The four wrapper types — plain structs, methods come from traits. // ===================================================================== @@ -422,6 +525,9 @@ impl<'a, 'db: 'a> Internal<'a, 'db> for ReadState<'a, 'db> { fn ctx(&self) -> Context { self.ctx } + fn apply_resolved_function(&mut self, func: &FuncType, args: &[Value]) -> Option { + apply_registered_function(self, func, args) + } } impl<'a, 'db: 'a> RegistrySealed<'a, 'db> for ReadState<'a, 'db> { fn registry(&self) -> &ActionRegistry { @@ -441,6 +547,9 @@ impl<'a, 'db: 'a> Internal<'a, 'db> for WriteState<'a, 'db> { fn ctx(&self) -> Context { self.ctx } + fn apply_resolved_function(&mut self, func: &FuncType, args: &[Value]) -> Option { + apply_registered_function(self, func, args) + } } impl<'a, 'db: 'a> RegistrySealed<'a, 'db> for WriteState<'a, 'db> { fn registry(&self) -> &ActionRegistry { @@ -460,6 +569,9 @@ impl<'a, 'db: 'a> Internal<'a, 'db> for FullState<'a, 'db> { fn ctx(&self) -> Context { self.ctx } + fn apply_resolved_function(&mut self, func: &FuncType, args: &[Value]) -> Option { + apply_registered_function(self, func, args) + } } impl<'a, 'db: 'a> RegistrySealed<'a, 'db> for FullState<'a, 'db> { fn registry(&self) -> &ActionRegistry { diff --git a/src/lib.rs b/src/lib.rs index dea785248..737a99d59 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -403,6 +403,8 @@ impl Default for EGraph { eg.type_info.add_presort::(span!()).unwrap(); eg.type_info.add_presort::(span!()).unwrap(); eg.type_info.add_presort::(span!()).unwrap(); + eg.type_info.add_presort::(span!()).unwrap(); + eg.type_info.add_presort::(span!()).unwrap(); eg.type_info.add_presort::(span!()).unwrap(); // Add != with a validator that computes inequality result @@ -733,7 +735,7 @@ impl EGraph { .read() .unwrap() .default_panic_id(), - ); + )?; translated_args[0] = egglog_bridge::MergeFn::Const(self.backend.base_values().get(resolved)); } @@ -1170,6 +1172,134 @@ impl EGraph { Ok((sort, value)) } + /// Typecheck an expression under explicit local bindings, an expected + /// output sort, and a primitive call context. + /// + /// `bindings` contains the local variables in scope while resolving `expr`. + /// Each tuple is `(name, span, sort)`, where `span` is used for diagnostics + /// tied to that binding. `output_sort` constrains overload resolution and + /// output-type inference for the expression. Global references are rewritten + /// into the same zero-argument function calls used during command execution. + /// `context` should match the runtime context where the resolved expression + /// will be evaluated. + pub fn typecheck_expr_with_bindings_and_output( + &mut self, + expr: &Expr, + bindings: &[(String, Span, ArcSort)], + output_sort: ArcSort, + context: Context, + ) -> Result { + let mut binding_map = IndexMap::default(); + binding_map.reserve(bindings.len()); + for (name, span, sort) in bindings { + if binding_map + .insert(name.as_str(), (span.clone(), sort.clone())) + .is_some() + { + return Err(TypeError::AlreadyDefined(name.clone(), span.clone())); + } + } + let resolved = self.type_info.typecheck_expr_with_output( + &mut self.parser.symbol_gen, + expr, + &binding_map, + output_sort, + context, + )?; + Ok(remove_globals::remove_globals_expr(resolved)) + } + + /// Replace literal `(unstable-fn "...")` targets with hidden evaluator bindings. + /// + /// The returned expression must be evaluated with the returned bindings in + /// scope before any caller-supplied local bindings. This lets direct + /// execution-state evaluation use the same hidden `ResolvedFunction` value + /// that backend rule lowering injects for `unstable-fn`. + /// + /// For example, a resolved body like `(unstable-app (unstable-fn "f") _0)` + /// cannot evaluate the string literal `"f"` directly. This helper replaces + /// the `(unstable-fn "f")` sub-expression with a fresh hidden variable and + /// returns a binding from that variable to the prepared function value. + pub fn prepare_unstable_fn_targets_for_eval( + &mut self, + expr: &ResolvedExpr, + ) -> Result<(ResolvedExpr, Vec<(String, Value)>), Error> { + let mut bindings = Vec::new(); + let expr = self.prepare_unstable_fn_targets_for_eval_inner(expr, &mut bindings)?; + Ok((expr, bindings)) + } + + fn prepare_unstable_fn_targets_for_eval_inner( + &mut self, + expr: &ResolvedExpr, + bindings: &mut Vec<(String, Value)>, + ) -> Result { + match expr { + ResolvedExpr::Lit(..) | ResolvedExpr::Var(..) => Ok(expr.clone()), + ResolvedExpr::Call(span, resolved_call, children) => { + if let ResolvedCall::Primitive(prim) = resolved_call + && prim.name() == "unstable-fn" + { + let Some(ResolvedExpr::Lit(target_span, Literal::String(name))) = + children.first() + else { + return Err(Error::BackendError(format!( + "{}\nunstable-fn requires a literal string function name", + children + .first() + .map(ResolvedExpr::span) + .unwrap_or_else(|| Span::Panic) + ))); + }; + let panic_id = self.backend.new_panic(format!( + "unstable-fn over `{name}` was applied in a context where its wrapped \ + function is not valid for this call site, if in a rule, add :naive." + )); + let resolved_function = resolve_function_container_target_with_context( + &self.backend, + &self.functions, + &self.type_info, + name, + prim, + panic_id, + )?; + let fn_value = self.backend.base_values().get(resolved_function); + let binding_name = self.parser.symbol_gen.fresh("unstable_fn_target"); + bindings.push((binding_name.clone(), fn_value)); + let mut prepared_children = Vec::with_capacity(children.len()); + prepared_children.push(ResolvedExpr::Var( + target_span.clone(), + ResolvedVar { + name: binding_name, + sort: children[0].output_type(), + is_global_ref: false, + }, + )); + for child in &children[1..] { + prepared_children.push( + self.prepare_unstable_fn_targets_for_eval_inner(child, bindings)?, + ); + } + return Ok(ResolvedExpr::Call( + span.clone(), + resolved_call.clone(), + prepared_children, + )); + } + + let prepared_children = children + .iter() + .map(|child| self.prepare_unstable_fn_targets_for_eval_inner(child, bindings)) + .collect::, _>>()?; + Ok(ResolvedExpr::Call( + span.clone(), + resolved_call.clone(), + prepared_children, + )) + } + } + } + fn eval_resolved_expr(&mut self, span: Span, expr: &ResolvedExpr) -> Result { let unit_id = self.backend.base_values().get_ty::<()>(); let unit_val = self.backend.base_values().get(()); @@ -2038,6 +2168,12 @@ impl EGraph { } } +/// Build the runtime value backing a resolved `(unstable-fn name)` target. +/// +/// For table-backed functions, this captures the table action that +/// `unstable-app` will call later. For primitive targets, this bakes one +/// dispatch id per runtime context so application can choose the entrypoint +/// matching the primitive body's current call-site context. fn resolve_function_container_target_with_context( backend: &egglog_bridge::EGraph, functions: &IndexMap, @@ -2045,17 +2181,17 @@ fn resolve_function_container_target_with_context( name: &str, primitive: &core::SpecializedPrimitive, panic_id: ExternalFunctionId, -) -> ResolvedFunction { - let Some(target_function) = type_info +) -> Result { + let target_function = type_info .get_sorts::() .into_iter() .find(|function| function.name() == primitive.output().name()) - else { - panic!( - "`unstable-fn` output sort `{}` is not a function sort", - primitive.output().name() - ); - }; + .ok_or_else(|| { + Error::BackendError(format!( + "`unstable-fn` output sort `{}` is not a function sort", + primitive.output().name() + )) + })?; let partial_arcsorts: Vec<_> = primitive.input().iter().skip(1).cloned().collect(); let remaining_inputs = target_function.inputs(); @@ -2064,7 +2200,7 @@ fn resolve_function_container_target_with_context( let id = if let Some(func) = functions.get(name) { let func_type = type_info .get_func_type(name) - .unwrap_or_else(|| panic!("No resolution for {name:?}")); + .ok_or_else(|| Error::BackendError(format!("No resolution for {name:?}")))?; let expected_inputs = partial_arcsorts .iter() .chain(remaining_inputs) @@ -2087,13 +2223,13 @@ fn resolve_function_container_target_with_context( .map(|sort| sort.name()) .collect::>() .join(", "); - panic!( + return Err(Error::BackendError(format!( "function container lookup for `{name}` expected ({}) -> {}, found ({}) -> {}", expected_input_names, output.name(), actual_input_names, func_type.output.name(), - ); + ))); } let action = egglog_bridge::TableAction::new(backend, func.backend_id); @@ -2112,18 +2248,23 @@ fn resolve_function_container_target_with_context( .iter() .filter(|primitive| primitive.accept(&signature, type_info)) .collect(); - let context_ids = enum_map::EnumMap::from_fn(|runtime_ctx| { + let mut context_ids = enum_map::EnumMap::from_fn(|_| None); + for runtime_ctx in Context::ALL { let mut ids = candidates .iter() .filter_map(|primitive| primitive.context_ids[runtime_ctx]); + // The first `next` finds the candidate for this runtime context; + // the second detects whether there is more than one such candidate. match (ids.next(), ids.next()) { - (None, _) => None, - (Some(id), None) => Some(id), - (Some(_), Some(_)) => panic!( - "Ambiguous primitive resolution for {name:?} in unstable-fn context {runtime_ctx:?}" - ), + (None, _) => {} + (Some(id), None) => context_ids[runtime_ctx] = Some(id), + (Some(_), Some(_)) => { + return Err(Error::BackendError(format!( + "Ambiguous primitive resolution for {name:?} in unstable-fn context {runtime_ctx:?}" + ))); + } } - }); + } if !context_ids.iter().any(|(_, id)| id.is_some()) { let (output_sort, input_sorts) = signature .split_last() @@ -2133,24 +2274,24 @@ fn resolve_function_container_target_with_context( .map(|sort| sort.name()) .collect::>() .join(", "); - panic!( + return Err(Error::BackendError(format!( "no primitive overload matched expected signature for {name:?}: ({}) -> {}; \ context ids: {context_ids:?}", input_names, output_sort.name(), - ); + ))); } ResolvedFunctionId::Primitive { context_ids } } else { - panic!("No resolution for {name:?}"); + return Err(Error::BackendError(format!("No resolution for {name:?}"))); }; - ResolvedFunction { + Ok(ResolvedFunction { id, partial_arcsorts, name: name.to_owned(), panic_id, - } + }) } struct BackendRule<'a> { @@ -2247,6 +2388,11 @@ impl<'a> BackendRule<'a> { let core::ResolvedAtomTerm::Literal(_, Literal::String(ref name)) = args[0] else { panic!("expected string literal after `unstable-fn`") }; + // Pre-register a panic id used by `FunctionContainer::apply` + // when the wrapped function is applied in a context that + // doesn't admit it. Triggered at runtime via the egglog + // panic side channel so misuse surfaces as an `Err` from + // `run_rules` rather than a thread unwind. let panic_id = self.rb.new_panic(format!( "unstable-fn over `{name}` was applied in a context where its wrapped \ function is not valid for this call site, if in a rule, add :naive." @@ -2258,7 +2404,8 @@ impl<'a> BackendRule<'a> { name, prim, panic_id, - ); + ) + .unwrap_or_else(|err| panic!("{err}")); qe_args[0] = self.rb.egraph().base_value_constant(resolved); } @@ -2497,6 +2644,26 @@ mod tests { } } + #[derive(Clone)] + struct FullOnly; + + impl Primitive for FullOnly { + fn name(&self) -> &str { + "full-only" + } + + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new(self.name(), vec![I64Sort.to_arcsort()], span.clone()) + .into_box() + } + } + + impl FullPrim for FullOnly { + fn apply<'a, 'db>(&self, state: FullState<'a, 'db>, _args: &[Value]) -> Option { + Some(state.base_values().get::(1)) + } + } + #[test] fn test_user_defined_primitive() { let mut egraph = EGraph::default(); @@ -2523,6 +2690,161 @@ mod tests { .unwrap(); } + #[test] + fn test_typecheck_expr_with_bindings_and_output_rejects_mismatch() { + let mut egraph = EGraph::default(); + let mut parser = crate::ast::Parser::default(); + let expr = parser.get_expr_from_string(None, "(+ 1 2)").unwrap(); + + let resolved = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &[], + I64Sort.to_arcsort(), + Context::Pure, + ) + .unwrap(); + assert_eq!(resolved.output_type().name(), I64Sort.name()); + + let err = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &[], + BoolSort.to_arcsort(), + Context::Pure, + ) + .unwrap_err(); + match err { + TypeError::Mismatch { + expected, actual, .. + } => { + assert_eq!(expected.name(), BoolSort.name()); + assert_eq!(actual.name(), I64Sort.name()); + } + other => panic!("expected mismatch, got {other:?}"), + } + + let literal = parser.get_expr_from_string(None, "1").unwrap(); + let err = egraph + .typecheck_expr_with_bindings_and_output( + &literal, + &[], + BoolSort.to_arcsort(), + Context::Pure, + ) + .unwrap_err(); + match err { + TypeError::Mismatch { + expected, actual, .. + } => { + assert_eq!(expected.name(), BoolSort.name()); + assert_eq!(actual.name(), I64Sort.name()); + } + other => panic!("expected literal mismatch, got {other:?}"), + } + } + + #[test] + fn test_typecheck_expr_with_bindings_and_output_uses_explicit_bindings() { + let mut egraph = EGraph::default(); + let mut parser = crate::ast::Parser::default(); + let expr = parser.get_expr_from_string(None, "(+ x 2)").unwrap(); + let bindings = vec![("x".to_string(), span!(), I64Sort.to_arcsort())]; + + let resolved = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &bindings, + I64Sort.to_arcsort(), + Context::Pure, + ) + .unwrap(); + + assert_eq!(resolved.output_type().name(), I64Sort.name()); + } + + #[test] + fn test_typecheck_expr_with_bindings_and_output_uses_context() { + let mut egraph = EGraph::default(); + egraph.add_full_primitive(FullOnly, None); + let mut parser = crate::ast::Parser::default(); + let expr = parser.get_expr_from_string(None, "(full-only)").unwrap(); + + let resolved = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &[], + I64Sort.to_arcsort(), + Context::Full, + ) + .unwrap(); + assert_eq!(resolved.output_type().name(), I64Sort.name()); + + let err = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &[], + I64Sort.to_arcsort(), + Context::Pure, + ) + .unwrap_err(); + match err { + TypeError::UnboundFunction(name, _) => assert_eq!(name, "full-only"), + other => panic!("expected unbound function, got {other:?}"), + } + } + + #[test] + fn test_typecheck_expr_with_bindings_and_output_rejects_duplicate_bindings() { + let mut egraph = EGraph::default(); + let mut parser = crate::ast::Parser::default(); + let expr = parser.get_expr_from_string(None, "x").unwrap(); + let bindings = vec![ + ("x".to_string(), span!(), I64Sort.to_arcsort()), + ("x".to_string(), span!(), BoolSort.to_arcsort()), + ]; + + let err = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &bindings, + I64Sort.to_arcsort(), + Context::Pure, + ) + .unwrap_err(); + + match err { + TypeError::AlreadyDefined(name, _) => assert_eq!(name, "x"), + other => panic!("expected duplicate binding, got {other:?}"), + } + } + + #[test] + fn test_typecheck_expr_with_bindings_and_output_rewrites_globals() { + let mut egraph = EGraph::default(); + egraph.parse_and_run_program(None, "(let $x 1)").unwrap(); + let mut parser = crate::ast::Parser::default(); + let expr = parser.get_expr_from_string(None, "$x").unwrap(); + + let resolved = egraph + .typecheck_expr_with_bindings_and_output( + &expr, + &[], + I64Sort.to_arcsort(), + Context::Read, + ) + .unwrap(); + + match resolved { + ResolvedExpr::Call(_, ResolvedCall::Func(func), children) => { + assert_eq!(func.name, "$x"); + assert!(children.is_empty()); + assert_eq!(func.output.name(), I64Sort.name()); + } + other => panic!("expected global function call rewrite, got {other:?}"), + } + } + // Test that an `EGraph` is `Send` & `Sync` #[test] fn test_egraph_send_sync() { diff --git a/src/sort/either.rs b/src/sort/either.rs new file mode 100644 index 000000000..0f9e5d028 --- /dev/null +++ b/src/sort/either.rs @@ -0,0 +1,290 @@ +use super::*; +use std::any::TypeId; + +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum EitherData { + Left(Value), + Right(Value), +} + +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct EitherContainer { + do_rebuild_left: bool, + do_rebuild_right: bool, + pub data: EitherData, +} + +impl ContainerValue for EitherContainer { + fn rebuild_contents(&mut self, rebuilder: &dyn Rebuilder) -> bool { + match &mut self.data { + EitherData::Left(value) if self.do_rebuild_left => { + let old = *value; + let new = rebuilder.rebuild_val(old); + *value = new; + old != new + } + EitherData::Right(value) if self.do_rebuild_right => { + let old = *value; + let new = rebuilder.rebuild_val(old); + *value = new; + old != new + } + _ => false, + } + } + + fn iter(&self) -> impl Iterator + '_ { + match self.data { + EitherData::Left(value) | EitherData::Right(value) => Some(value).into_iter(), + } + } +} + +#[derive(Clone, Debug)] +pub struct EitherSort { + name: String, + left: ArcSort, + right: ArcSort, +} + +impl EitherSort { + pub fn left(&self) -> ArcSort { + self.left.clone() + } + + pub fn right(&self) -> ArcSort { + self.right.clone() + } +} + +impl Presort for EitherSort { + fn presort_name() -> &'static str { + "Either" + } + + fn reserved_primitives() -> Vec<&'static str> { + vec![ + "either-left", + "either-right", + "either-unwrap-left", + "either-unwrap-right", + "either-match", + ] + } + + fn make_sort( + typeinfo: &mut TypeInfo, + name: String, + args: &[Expr], + ) -> Result { + if let [Expr::Var(left_span, left), Expr::Var(right_span, right)] = args { + let left = typeinfo + .get_sort_by_name(left) + .ok_or(TypeError::UndefinedSort(left.clone(), left_span.clone()))?; + let right = typeinfo + .get_sort_by_name(right) + .ok_or(TypeError::UndefinedSort(right.clone(), right_span.clone()))?; + + Ok(Self { + name, + left: left.clone(), + right: right.clone(), + } + .to_arcsort()) + } else { + panic!("Either sort requires exactly two arguments") + } + } +} + +impl ContainerSort for EitherSort { + type Container = EitherContainer; + + fn name(&self) -> &str { + &self.name + } + + fn inner_sorts(&self) -> Vec { + vec![self.left.clone(), self.right.clone()] + } + + fn is_eq_container_sort(&self) -> bool { + self.left.is_eq_sort() + || self.right.is_eq_sort() + || self.left.is_eq_container_sort() + || self.right.is_eq_container_sort() + } + + fn inner_values( + &self, + container_values: &ContainerValues, + value: Value, + ) -> Vec<(ArcSort, Value)> { + let either = container_values + .get_val::(value) + .unwrap() + .clone(); + match either.data { + EitherData::Left(value) => vec![(self.left.clone(), value)], + EitherData::Right(value) => vec![(self.right.clone(), value)], + } + } + + fn register_primitives(&self, eg: &mut EGraph) { + let arc = self.clone().to_arcsort(); + + add_primitive!(eg, "either-left" = {self.clone(): EitherSort} |left: # (self.left())| -> @EitherContainer (arc) { + EitherContainer { + do_rebuild_left: self.ctx.left.is_eq_sort() || self.ctx.left.is_eq_container_sort(), + do_rebuild_right: self.ctx.right.is_eq_sort() || self.ctx.right.is_eq_container_sort(), + data: EitherData::Left(left), + } + }); + + add_primitive!(eg, "either-right" = {self.clone(): EitherSort} |right: # (self.right())| -> @EitherContainer (arc) { + EitherContainer { + do_rebuild_left: self.ctx.left.is_eq_sort() || self.ctx.left.is_eq_container_sort(), + do_rebuild_right: self.ctx.right.is_eq_sort() || self.ctx.right.is_eq_container_sort(), + data: EitherData::Right(right), + } + }); + + add_primitive!(eg, "either-unwrap-left" = |xs: @EitherContainer (arc)| -?> # (self.left()) { + match xs.data { + EitherData::Left(value) => Some(value), + EitherData::Right(_) => None, + } + }); + + add_primitive!(eg, "either-unwrap-right" = |xs: @EitherContainer (arc)| -?> # (self.right()) { + match xs.data { + EitherData::Left(_) => None, + EitherData::Right(value) => Some(value), + } + }); + + let either = eg.type_info.get_sort_by_name(self.name()).unwrap().clone(); + let fn_sorts = eg.type_info.get_sorts::(); + for left_fn in &fn_sorts { + for right_fn in &fn_sorts { + try_registering_either_match(eg, either.clone(), left_fn.clone(), right_fn.clone()); + } + } + } + + fn reconstruct_termdag( + &self, + container_values: &ContainerValues, + value: Value, + termdag: &mut TermDag, + element_terms: Vec, + ) -> TermId { + assert_eq!(element_terms.len(), 1); + let either = container_values.get_val::(value).unwrap(); + let head = match either.data { + EitherData::Left(_) => "either-left", + EitherData::Right(_) => "either-right", + }; + termdag.app(head.into(), element_terms) + } + + fn serialized_name(&self, container_values: &ContainerValues, value: Value) -> String { + let either = container_values.get_val::(value).unwrap(); + match either.data { + EitherData::Left(_) => "either-left".to_owned(), + EitherData::Right(_) => "either-right".to_owned(), + } + } +} + +pub(crate) fn register_either_primitives_for_function(eg: &mut EGraph, fn_: Arc) { + let eithers = eg + .type_info + .get_arcsorts_by(|sort| sort.value_type() == Some(TypeId::of::())); + let fn_sorts = eg.type_info.get_sorts::(); + for either in eithers { + for other_fn in &fn_sorts { + try_registering_either_match(eg, either.clone(), fn_.clone(), other_fn.clone()); + if !Arc::ptr_eq(&fn_, other_fn) { + try_registering_either_match(eg, either.clone(), other_fn.clone(), fn_.clone()); + } + } + } +} + +fn try_registering_either_match( + eg: &mut EGraph, + either: ArcSort, + left_fn: Arc, + right_fn: Arc, +) { + if either.value_type() != Some(TypeId::of::()) + || left_fn.inputs().len() != 1 + || right_fn.inputs().len() != 1 + || left_fn.inputs()[0].name() != either.inner_sorts()[0].name() + || right_fn.inputs()[0].name() != either.inner_sorts()[1].name() + || left_fn.output().name() != right_fn.output().name() + { + return; + } + + eg.add_pure_primitive( + EitherMatch { + name: "either-match".into(), + either, + left_fn, + right_fn, + }, + None, + ); +} + +#[derive(Clone)] +struct EitherMatch { + name: String, + either: ArcSort, + left_fn: Arc, + right_fn: Arc, +} + +impl Primitive for EitherMatch { + fn name(&self) -> &str { + &self.name + } + + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + &self.name, + vec![ + self.either.clone(), + self.left_fn.clone(), + self.right_fn.clone(), + self.left_fn.output(), + ], + span.clone(), + ) + .into_box() + } +} + +impl PurePrim for EitherMatch { + fn apply<'a, 'db>(&self, mut state: PureState<'a, 'db>, args: &[Value]) -> Option { + let either = state + .container_values() + .get_val::(args[0])? + .clone(); + let left_fn = state + .container_values() + .get_val::(args[1])? + .clone(); + let right_fn = state + .container_values() + .get_val::(args[2])? + .clone(); + + match either.data { + EitherData::Left(value) => state.apply_function(&left_fn, &[value]), + EitherData::Right(value) => state.apply_function(&right_fn, &[value]), + } + } +} diff --git a/src/sort/fn.rs b/src/sort/fn.rs index e7f3f8ed4..7a354d0e6 100644 --- a/src/sort/fn.rs +++ b/src/sort/fn.rs @@ -99,7 +99,7 @@ impl Presort for FunctionSort { } fn reserved_primitives() -> Vec<&'static str> { - vec!["unstable-fn", "unstable-app"] + vec!["unstable-fn", "unstable-app", "unstable-if"] } fn make_sort( @@ -217,6 +217,9 @@ impl Sort for FunctionSort { register_vec_primitives_for_function(eg, self.clone()); register_multiset_primitives_for_function(eg, self.clone()); + register_maybe_primitives_for_function(eg, self.clone()); + register_if_primitives_for_function(eg, self.clone()); + register_either_primitives_for_function(eg, self.clone()); } fn value_type(&self) -> Option { diff --git a/src/sort/maybe.rs b/src/sort/maybe.rs new file mode 100644 index 000000000..a5ef7813d --- /dev/null +++ b/src/sort/maybe.rs @@ -0,0 +1,246 @@ +use super::*; +use std::any::TypeId; + +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct MaybeContainer { + pub do_rebuild: bool, + pub data: Option, +} + +impl ContainerValue for MaybeContainer { + fn rebuild_contents(&mut self, rebuilder: &dyn Rebuilder) -> bool { + if self.do_rebuild { + if let Some(old) = self.data { + let new = rebuilder.rebuild_val(old); + self.data = Some(new); + old != new + } else { + false + } + } else { + false + } + } + + fn iter(&self) -> impl Iterator + '_ { + self.data.iter().copied() + } +} + +#[derive(Clone, Debug)] +pub struct MaybeSort { + name: String, + element: ArcSort, +} + +impl MaybeSort { + pub fn element(&self) -> ArcSort { + self.element.clone() + } +} + +impl Presort for MaybeSort { + fn presort_name() -> &'static str { + "Maybe" + } + + fn reserved_primitives() -> Vec<&'static str> { + vec![ + "maybe-none", + "maybe-some", + "maybe-unwrap", + "maybe-unwrap-or", + "maybe-f64-merge-with-tol", + "unstable-maybe-match", + ] + } + + fn make_sort( + typeinfo: &mut TypeInfo, + name: String, + args: &[Expr], + ) -> Result { + if let [Expr::Var(span, element)] = args { + let element = typeinfo + .get_sort_by_name(element) + .ok_or(TypeError::UndefinedSort(element.clone(), span.clone()))?; + + Ok(Self { + name, + element: element.clone(), + } + .to_arcsort()) + } else { + panic!("Maybe sort requires exactly one argument") + } + } +} + +impl ContainerSort for MaybeSort { + type Container = MaybeContainer; + + fn name(&self) -> &str { + &self.name + } + + fn inner_sorts(&self) -> Vec { + vec![self.element.clone()] + } + + fn is_eq_container_sort(&self) -> bool { + self.element.is_eq_sort() || self.element.is_eq_container_sort() + } + + fn inner_values( + &self, + container_values: &ContainerValues, + value: Value, + ) -> Vec<(ArcSort, Value)> { + let val = container_values + .get_val::(value) + .unwrap() + .clone(); + val.data + .iter() + .map(|v| (self.element.clone(), *v)) + .collect() + } + + fn register_primitives(&self, eg: &mut EGraph) { + let arc = self.clone().to_arcsort(); + + add_primitive!(eg, "maybe-none" = {self.clone(): MaybeSort} || -> @MaybeContainer (arc) { MaybeContainer { + do_rebuild: self.ctx.is_eq_container_sort(), + data: None, + } }); + + add_primitive!(eg, "maybe-some" = {self.clone(): MaybeSort} |x: # (self.element())| -> @MaybeContainer (arc) { MaybeContainer { + do_rebuild: self.ctx.is_eq_container_sort(), + data: Some(x), + } }); + + add_primitive!(eg, "maybe-unwrap" = |xs: @MaybeContainer (arc)| -?> # (self.element()) { xs.data }); + add_primitive!(eg, "maybe-unwrap-or" = |xs: @MaybeContainer (arc), default: # (self.element())| -> # (self.element()) { + xs.data.unwrap_or(default) + }); + + if self.element().name() == "f64" { + add_primitive!(eg, "maybe-f64-merge-with-tol" = |old: @MaybeContainer (arc), new: @MaybeContainer (arc), tol: F| -?> @MaybeContainer (arc) {{ + match (old.data, new.data) { + (None, _) | (_, None) => Some(MaybeContainer { data: None, ..old }), + (Some(old_value), Some(new_value)) => { + let old_f = state.base_values().unwrap::(old_value).0.0; + let new_f = state.base_values().unwrap::(new_value).0.0; + let tolerance = tol.0.0.abs(); + let merged = + old_f == new_f || + (old_f == 0.0 && new_f == -0.0) || + (old_f == -0.0 && new_f == 0.0) || + (old_f - new_f).abs() <= tolerance; + merged.then_some(old) + } + } + }}); + } + + let maybe = eg.type_info.get_sort_by_name(self.name()).unwrap().clone(); + for fn_sort in eg.type_info.get_sorts::() { + try_registering_maybe_match(eg, maybe.clone(), fn_sort); + } + } + + fn reconstruct_termdag( + &self, + _container_values: &ContainerValues, + _value: Value, + termdag: &mut TermDag, + element_terms: Vec, + ) -> TermId { + match element_terms.as_slice() { + [] => termdag.app("maybe-none".into(), vec![]), + [value] => termdag.app("maybe-some".into(), vec![*value]), + _ => panic!("Maybe sort expected at most one element"), + } + } + + fn serialized_name(&self, container_values: &ContainerValues, value: Value) -> String { + let maybe = container_values.get_val::(value).unwrap(); + if maybe.data.is_some() { + "maybe-some".to_owned() + } else { + "maybe-none".to_owned() + } + } +} + +pub(crate) fn try_registering_maybe_match(eg: &mut EGraph, maybe: ArcSort, fn_: Arc) { + if maybe.value_type() != Some(TypeId::of::()) + || fn_.inputs().len() != 1 + || fn_.inputs()[0].name() != maybe.inner_sorts()[0].name() + { + return; + } + + eg.add_pure_primitive( + MaybeMatch { + name: "unstable-maybe-match".into(), + maybe, + fn_, + }, + None, + ); +} + +pub(crate) fn register_maybe_primitives_for_function(eg: &mut EGraph, fn_: Arc) { + for maybe in eg + .type_info + .get_arcsorts_by(|sort| sort.value_type() == Some(TypeId::of::())) + { + try_registering_maybe_match(eg, maybe, fn_.clone()); + } +} + +#[derive(Clone)] +struct MaybeMatch { + name: String, + maybe: ArcSort, + fn_: Arc, +} + +impl Primitive for MaybeMatch { + fn name(&self) -> &str { + &self.name + } + + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + &self.name, + vec![ + self.maybe.clone(), + self.fn_.clone(), + self.fn_.output(), + self.fn_.output(), + ], + span.clone(), + ) + .into_box() + } +} + +impl PurePrim for MaybeMatch { + fn apply<'a, 'db>(&self, mut state: PureState<'a, 'db>, args: &[Value]) -> Option { + let maybe = state + .container_values() + .get_val::(args[0])? + .clone(); + let fc = state + .container_values() + .get_val::(args[1])? + .clone(); + + match maybe.data { + Some(value) => state.apply_function(&fc, &[value]), + None => Some(args[2]), + } + } +} diff --git a/src/sort/mod.rs b/src/sort/mod.rs index 2dd56d99a..65757d1cb 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -43,6 +43,10 @@ mod r#fn; pub use r#fn::*; mod multiset; pub use multiset::*; +mod maybe; +pub use maybe::*; +mod either; +pub use either::*; mod pair; pub use pair::*; diff --git a/src/sort/unit.rs b/src/sort/unit.rs index 8e7858537..6b6d62e4e 100644 --- a/src/sort/unit.rs +++ b/src/sort/unit.rs @@ -19,3 +19,70 @@ impl BaseSort for UnitSort { termdag.lit(Literal::Unit) } } + +pub(crate) fn try_registering_if(eg: &mut EGraph, fn_: Arc, output: ArcSort) { + if !fn_.inputs().is_empty() || fn_.output().name() != UnitSort.name() { + return; + } + + eg.add_pure_primitive( + IfPrim { + name: "unstable-if".into(), + fn_, + output, + }, + None, + ); +} + +pub(crate) fn register_if_primitives_for_function(eg: &mut EGraph, fn_: Arc) { + for output in eg.type_info.get_arcsorts_by(|_| true) { + try_registering_if(eg, fn_.clone(), output); + } +} + +pub(crate) fn register_if_primitives_for_output(eg: &mut EGraph, output: ArcSort) { + for fn_ in eg.type_info.get_sorts::() { + try_registering_if(eg, fn_, output.clone()); + } +} + +#[derive(Clone)] +struct IfPrim { + name: String, + fn_: Arc, + output: ArcSort, +} + +impl Primitive for IfPrim { + fn name(&self) -> &str { + &self.name + } + + fn get_type_constraints(&self, span: &Span) -> Box { + SimpleTypeConstraint::new( + &self.name, + vec![ + self.fn_.clone(), + self.output.clone(), + self.output.clone(), + self.output.clone(), + ], + span.clone(), + ) + .into_box() + } +} + +impl PurePrim for IfPrim { + fn apply<'a, 'db>(&self, mut state: PureState<'a, 'db>, args: &[Value]) -> Option { + let fc = state + .container_values() + .get_val::(args[0])? + .clone(); + match state.apply_function(&fc, &[]) { + Some(_) => Some(args[1]), + None => Some(args[2]), + } + } +} diff --git a/src/typechecking.rs b/src/typechecking.rs index a154ff55f..e53f6a3ff 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -5,7 +5,9 @@ use crate::{ core::{CoreActionContext, CoreRule, GenericActionsExt, ResolvedCall}, *, }; -use ast::{ResolvedAction, ResolvedExpr, ResolvedFact, ResolvedRule, ResolvedVar, Rule}; +use ast::{ + MappedExprExt, ResolvedAction, ResolvedExpr, ResolvedFact, ResolvedRule, ResolvedVar, Rule, +}; use core_relations::ExternalFunction; use egglog_ast::generic_ast::GenericAction; use egglog_bridge::ActionRegistry; @@ -186,6 +188,11 @@ impl PrimitiveWithId { }; problem.solve(|sort| sort.name()).is_ok() } + + /// Returns whether this primitive has a runtime entrypoint for `context`. + pub fn is_valid_in_context(&self, context: Context) -> bool { + self.context_ids[context].is_some() + } } impl Debug for PrimitiveWithId { @@ -254,8 +261,13 @@ impl EGraph { match self.type_info.sorts.entry(name.to_owned()) { HEntry::Occupied(_) => Err(TypeError::SortAlreadyBound(name.to_owned(), span)), HEntry::Vacant(e) => { + let is_function_sort = + sort.value_type() == Some(std::any::TypeId::of::()); e.insert(sort.clone()); - sort.register_primitives(self); + sort.clone().register_primitives(self); + if !is_function_sort { + register_if_primitives_for_output(self, sort); + } Ok(()) } } @@ -992,6 +1004,54 @@ impl TypeInfo { } } + pub(crate) fn typecheck_expr_with_output( + &self, + symbol_gen: &mut SymbolGen, + expr: &Expr, + binding: &IndexMap<&str, (Span, ArcSort)>, + output_sort: ArcSort, + context: Context, + ) -> Result { + let action = Action::Expr(expr.span(), expr.clone()); + let mut binding_set: IndexSet = + binding.keys().copied().map(str::to_string).collect(); + let mut ctx = CoreActionContext::new(self, &mut binding_set, symbol_gen, false); + let (actions, mapped_action) = Actions::singleton(action).to_core_actions(&mut ctx)?; + let mut problem = Problem::default(); + + problem.add_actions(&actions, self, symbol_gen, context)?; + + for (var, (span, sort)) in binding { + problem.assign_local_var_type(var, span.clone(), sort.clone())?; + } + + let [GenericAction::Expr(_, mapped_expr)] = mapped_action.0.as_slice() else { + unreachable!("typechecking an expression should produce one expression action") + }; + let output_atom = mapped_expr.get_corresponding_var_or_lit(self); + problem.add_binding(output_atom, output_sort.clone()); + + let assignment = problem + .solve(|sort: &ArcSort| sort.name()) + .map_err(|e| e.to_type_error())?; + + let annotated_actions = assignment.annotate_actions(&mapped_action, self, context)?; + match annotated_actions.0.into_iter().next().unwrap() { + ResolvedAction::Expr(_, resolved_expr) => { + let actual = resolved_expr.output_type(); + if actual.name() != output_sort.name() { + return Err(TypeError::Mismatch { + expr: expr.clone(), + expected: output_sort, + actual, + }); + } + Ok(resolved_expr) + } + _ => unreachable!(), + } + } + fn typecheck_standalone_action( &self, symbol_gen: &mut SymbolGen, diff --git a/tests/either.egg b/tests/either.egg new file mode 100644 index 000000000..9e328f469 --- /dev/null +++ b/tests/either.egg @@ -0,0 +1,33 @@ +(sort IntOrFloat (Either i64 f64)) +(sort I64ToString (UnstableFn (i64) String)) +(sort F64ToString (UnstableFn (f64) String)) + +(check (= (either-left 20) (either-left 20))) +(check (= (either-right 1.0) (either-right 1.0))) +(check (= (either-unwrap-left (either-left 20)) 20)) +(check (= (either-unwrap-right (either-right 1.0)) 1.0)) +(fail (either-unwrap-left (either-right 1.0))) +(fail (either-unwrap-right (either-left 20))) + +(check (= (either-match (either-left 20) (unstable-fn "to-string") (unstable-fn "to-string")) "20")) +(check (= (either-match (either-right 1.0) (unstable-fn "to-string") (unstable-fn "to-string")) "1.0")) + +(sort MaybeInt (Maybe i64)) +(sort IntOrMaybe (Either i64 MaybeInt)) +(sort I64ToI64 (UnstableFn (i64) i64)) +(sort MaybeIntToI64 (UnstableFn (MaybeInt) i64)) + +(check (= (either-match (either-left 1) (unstable-fn "+" 1) (unstable-fn "maybe-unwrap")) 2)) +(check (= (either-match (either-right (maybe-some 5)) (unstable-fn "+" 1) (unstable-fn "maybe-unwrap")) 5)) + +(sort LateI64ToF64 (UnstableFn (i64) f64)) +(sort LateF64ToF64 (UnstableFn (f64) f64)) +(sort LateIntOrFloat (Either i64 f64)) + +(function late-left () LateIntOrFloat :no-merge) +(set (late-left) (either-left 9)) +(check (= (either-match (late-left) (unstable-fn "to-f64") (unstable-fn "+" 1.0)) 9.0)) + +(function late-right () LateIntOrFloat :no-merge) +(set (late-right) (either-right 4.0)) +(check (= (either-match (late-right) (unstable-fn "to-f64") (unstable-fn "+" 1.0)) 5.0)) diff --git a/tests/fn.egg b/tests/fn.egg new file mode 100644 index 000000000..52a1646ff --- /dev/null +++ b/tests/fn.egg @@ -0,0 +1,30 @@ +(sort MaybeInt (Maybe i64)) +(sort IntThunk (UnstableFn () i64)) +(sort MaybeF64 (Maybe f64)) +(sort F64Thunk (UnstableFn () f64)) +(sort F64ToF64 (UnstableFn (f64) f64)) +(sort I64ToI64 (UnstableFn (i64) i64)) +(sort UnitThunk (UnstableFn () Unit)) +(sort UnitToF64 (UnstableFn (Unit) f64)) + +(function none-int () MaybeInt :no-merge) +(set (none-int) (maybe-none)) + +(function merge-plus () i64 :merge (unstable-app (unstable-fn "+" old) new)) +(set (merge-plus) 1) +(set (merge-plus) 2) +(check (= (merge-plus) 3)) + +(check (= (unstable-app (unstable-fn "+" 1.0) 2.0) 3.0)) +(check (= (unstable-maybe-match (maybe-some 3.0) (unstable-fn "+" 4.0) 0.0) 7.0)) +(check (= (unstable-if (unstable-fn "<=" 1 2) 10 20) 10)) +(check (= (unstable-if (unstable-fn "<" 2 1) 10 20) 20)) +(check (= (unstable-if (unstable-fn "<=" 1 2) (maybe-some 3) (none-int)) (maybe-some 3))) + +(sort LateIfPair (Pair i64 i64)) + +(let late-then (pair 1 2)) +(let late-else (pair 3 4)) + +(check (= (unstable-if (unstable-fn "<=" 1 2) late-then late-else) late-then)) +(check (= (unstable-if (unstable-fn "<" 2 1) late-then late-else) late-else)) diff --git a/tests/maybe.egg b/tests/maybe.egg new file mode 100644 index 000000000..766a557b2 --- /dev/null +++ b/tests/maybe.egg @@ -0,0 +1,57 @@ +(sort MaybeFloat (Maybe f64)) +(sort MaybeInt (Maybe i64)) +(sort MaybeMaybeInt (Maybe MaybeInt)) +(sort IntToInt (UnstableFn (i64) i64)) +(sort MaybeIntToInt (UnstableFn (MaybeInt) i64)) + +(function none-float () MaybeFloat :no-merge) +(set (none-float) (maybe-none)) +(function none-int () MaybeInt :no-merge) +(set (none-int) (maybe-none)) + +(check (= (none-float) (maybe-none))) +(check (= (maybe-some 1.0) (maybe-some 1.0))) +(check (= 1.0 (maybe-unwrap (maybe-some 1.0)))) +(check (= 2.0 (maybe-unwrap-or (none-float) 2.0))) +(check (= 7 (maybe-unwrap-or (maybe-some 7) 2))) +(fail (maybe-unwrap (none-float))) + +(datatype Math + (Num i64)) +(sort MaybeMath (Maybe Math)) + +(let $a (Num 1)) +(let $b (Num 1)) +(union $a $b) +(run 1) +(check (= (maybe-some $a) (maybe-some $b))) + +(function merge-none () MaybeFloat :merge (maybe-f64-merge-with-tol old new 1e-6)) +(set (merge-none) (maybe-none)) +(set (merge-none) (maybe-some 1.0)) +(check (= (merge-none) (maybe-none))) + +(function merge-close () MaybeFloat :merge (maybe-f64-merge-with-tol old new 1e-6)) +(set (merge-close) (maybe-some 1.0)) +(set (merge-close) (maybe-some 1.0000005)) +(check (= (merge-close) (maybe-some 1.0))) + +(function merge-zero () MaybeFloat :merge (maybe-f64-merge-with-tol old new 1e-6)) +(set (merge-zero) (maybe-some 0.0)) +(set (merge-zero) (maybe-some -0.0)) +(check (= (merge-zero) (maybe-some 0.0))) + +(function merge-bad () MaybeFloat :merge (maybe-f64-merge-with-tol old new 1e-6)) +(set (merge-bad) (maybe-some 1.0)) +(fail (set (merge-bad) (maybe-some 2.0))) + +(check (= (unstable-maybe-match (maybe-some 2) (unstable-fn "+" 1) 0) 3)) +(check (= (unstable-maybe-match (none-int) (unstable-fn "+" 1) 7) 7)) +(fail (unstable-maybe-match (maybe-some (none-int)) (unstable-fn "maybe-unwrap") 0)) + +(sort LateF64ToString (UnstableFn (f64) String)) +(sort LateMaybeFloat (Maybe f64)) + +(function late-some-float () LateMaybeFloat :no-merge) +(set (late-some-float) (maybe-some 4.0)) +(check (= (unstable-maybe-match (late-some-float) (unstable-fn "to-string") "none") "4.0")) diff --git a/tests/snapshots/files__proof_unsupported_files.snap b/tests/snapshots/files__proof_unsupported_files.snap index d4fc6e54f..3ac7be308 100644 --- a/tests/snapshots/files__proof_unsupported_files.snap +++ b/tests/snapshots/files__proof_unsupported_files.snap @@ -16,10 +16,12 @@ datatypes.egg delete.egg eggcc-2mm.egg eggcc-extraction.egg +either.egg eqsat-basic-multiset.egg extract-vec-bench.egg factoring-multisets.egg fibonacci.egg +fn.egg fusion.egg hardboiled_conv1d_128.egg hardboiled_conv1d_32.egg @@ -35,6 +37,7 @@ looking_up_nonconstructor_in_rewrite_good.egg luminal-llama.egg map.egg math.egg +maybe.egg merge_read.egg multiset.egg nested-container-dirty-propagation.egg diff --git a/tests/snapshots/files__shared_snapshot_either.snap b/tests/snapshots/files__shared_snapshot_either.snap new file mode 100644 index 000000000..537107ab3 --- /dev/null +++ b/tests/snapshots/files__shared_snapshot_either.snap @@ -0,0 +1,6 @@ +--- +source: tests/files.rs +expression: snapshot_content_across_treatments +--- +((late-left 1) + (late-right 1)) diff --git a/tests/snapshots/files__shared_snapshot_fn.snap b/tests/snapshots/files__shared_snapshot_fn.snap new file mode 100644 index 000000000..f6d9d9d02 --- /dev/null +++ b/tests/snapshots/files__shared_snapshot_fn.snap @@ -0,0 +1,6 @@ +--- +source: tests/files.rs +expression: snapshot_content_across_treatments +--- +((merge-plus 1) + (none-int 1)) diff --git a/tests/snapshots/files__shared_snapshot_maybe.snap b/tests/snapshots/files__shared_snapshot_maybe.snap new file mode 100644 index 000000000..055f09488 --- /dev/null +++ b/tests/snapshots/files__shared_snapshot_maybe.snap @@ -0,0 +1,12 @@ +--- +source: tests/files.rs +expression: snapshot_content_across_treatments +--- +((Num 1) + (late-some-float 1) + (merge-bad 1) + (merge-close 1) + (merge-none 1) + (merge-zero 1) + (none-float 1) + (none-int 1))