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..45b05276f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -733,7 +733,7 @@ impl EGraph { .read() .unwrap() .default_panic_id(), - ); + )?; translated_args[0] = egglog_bridge::MergeFn::Const(self.backend.base_values().get(resolved)); } @@ -1170,6 +1170,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 +2166,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 +2179,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 +2198,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 +2221,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 +2246,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 +2272,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 +2386,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 +2402,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 +2642,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 +2688,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/typechecking.rs b/src/typechecking.rs index a154ff55f..dedb17f68 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 { @@ -992,6 +999,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,