Skip to main content

proto_vulcan/
user.rs

1//! # User extensions
2//!
3//! By defining a struct that implements the `Clone`- `Debug`- and `User`-traits, the search
4//! `State`-monad can be extended with any kind of information that gets cloned along with the
5//! search when it forks, and discarded when branches fail. This can be used to add additional
6//! clone-on-write constraint-stores, for example. The user-defined state can be accessed wherever
7//! `State` is available, such as in in `fngoal |state| { }`-functions and in constraints.
8//!
9//! The `User`-trait provides optional hooks that the user can implement. What hooks there
10//! should be is still largely TBD.
11//!
12//! Another way of extending Proto-vulcan is `LTerm`s that implement `UserUnify`-trait. User
13//! defined state is not available in user defined unification, as `LTerm` is not parametrized
14//! by the user state type.
15
16use crate::engine::Engine;
17use crate::goal::Goal;
18use crate::lterm::LTerm;
19use crate::state::constraint::Constraint;
20use crate::state::{SMap, SResult, State};
21use std::fmt;
22use std::fmt::Debug;
23use std::hash::Hash;
24use std::rc::Rc;
25
26pub trait User: Debug + Clone + Default + 'static {
27    type UserTerm: Debug + Clone + Hash + PartialEq + Eq;
28
29    /// Type of data-structure stored in the Engine-instance. Retrievable
30    /// with Engine::context().
31    type UserContext: Debug;
32
33    /// Process extension to substitution map.
34    fn process_extension<E: Engine<Self>>(
35        state: State<Self, E>,
36        _extension: &SMap<Self, E>,
37    ) -> SResult<Self, E> {
38        Ok(state)
39    }
40
41    // User unification.
42    fn unify<E: Engine<Self>>(
43        _state: State<Self, E>,
44        _extension: &mut SMap<Self, E>,
45        _uwalk: LTerm<Self, E>,
46        _vwalk: LTerm<Self, E>,
47    ) -> SResult<Self, E> {
48        Err(())
49    }
50
51    /// Called before the constraint is added to the state
52    fn with_constraint<E: Engine<Self>>(
53        _state: &mut State<Self, E>,
54        _constraint: &Rc<dyn Constraint<Self, E>>,
55    ) {
56    }
57
58    /// Called after the constraint has been removed from the state
59    fn take_constraint<E: Engine<Self>>(
60        _state: &mut State<Self, E>,
61        _constraint: &Rc<dyn Constraint<Self, E>>,
62    ) {
63    }
64
65    /// Called in reification when constraints are finalized. For example finite domain
66    /// constraints are converted to sequences of integers.
67    fn enforce_constraints<E: Engine<Self>>(_x: LTerm<Self, E>) -> Goal<Self, E> {
68        Goal::Succeed
69    }
70
71    fn finalize<E: Engine<Self>>(_state: &mut State<Self, E>) {}
72
73    fn reify<E: Engine<Self>>(_state: &mut State<Self, E>) {}
74}
75
76#[derive(Debug, Clone)]
77pub struct DefaultUser {}
78
79impl DefaultUser {
80    pub fn new() -> DefaultUser {
81        DefaultUser {}
82    }
83}
84
85impl fmt::Display for DefaultUser {
86    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
87        write!(f, "")
88    }
89}
90
91impl Default for DefaultUser {
92    fn default() -> DefaultUser {
93        DefaultUser {}
94    }
95}
96
97impl User for DefaultUser {
98    type UserTerm = ();
99    type UserContext = ();
100}