sim_lib_logic/
unify.rs

1//! Standalone unification entry point over the kernel `Expr` graph.
2//!
3//! [`unify_exprs`] unifies two terms once and reports the result as a kernel
4//! `ShapeMatch`, the same accept/reject surface used by the `Shape` protocol;
5//! see the [`README`](https://docs.rs/sim-runtime).
6
7use sim_kernel::{Cx, Expr, Result, ShapeMatch};
8
9use crate::{
10    env::LogicEnv,
11    model::{LogicConfig, OccursCheck},
12};
13
14/// Unifies two expressions and reports the result as a kernel `ShapeMatch`.
15///
16/// On success the returned match is accepting and its captures hold the
17/// variable bindings; on a structural mismatch it is a rejecting match. The
18/// occurs-check policy comes from `config`.
19///
20/// # Examples
21///
22/// ```
23/// use std::sync::Arc;
24/// use sim_kernel::{Cx, DefaultFactory, EagerPolicy, Expr, Symbol};
25/// use sim_lib_logic::{LogicConfig, unify_exprs};
26///
27/// let mut cx = Cx::new(Arc::new(EagerPolicy), Arc::new(DefaultFactory));
28/// let left = Expr::List(vec![
29///     Expr::Symbol(Symbol::new("point")),
30///     Expr::Local(Symbol::new("x")),
31/// ]);
32/// let right = Expr::List(vec![
33///     Expr::Symbol(Symbol::new("point")),
34///     Expr::Symbol(Symbol::new("origin")),
35/// ]);
36/// let matched = unify_exprs(&mut cx, &LogicConfig::default(), &left, &right).unwrap();
37/// assert!(matched.accepted);
38/// ```
39pub fn unify_exprs(
40    cx: &mut Cx,
41    config: &LogicConfig,
42    left: &Expr,
43    right: &Expr,
44) -> Result<ShapeMatch> {
45    let mut env = LogicEnv::new();
46    let accepted = env.unify(left, right, occurs_check(config))?;
47    if accepted {
48        env.as_shape_match(cx)
49    } else {
50        Ok(sim_kernel::ShapeMatch::reject("unification failed"))
51    }
52}
53
54pub(crate) fn occurs_check(config: &LogicConfig) -> OccursCheck {
55    config.occurs_check
56}
sim_lib_logic/unify.rs

sim_lib_logic/
unify.rs
