Struct Scope 

pub struct Scope<T: Hash + Eq> { /* private fields */ }

Utility to implement lookup scopes.

Scope implements the logic needed to support name lookup in a local scope, similar to what may many need in simple programming languages or in logical formalisms. It supports looking up by name elements of any given type and implements Stack to support incremental interfaces, e.g., in SAT or SMT solvers.

A call to lookup() method produces an instance of LookupSet which can be used to further filter and navigate the objects found by name. LookupSet in turn is in charge of emitting detailed error diagnostics when a lookup fails, helping to standardize such diagnostics across all formally and its clients.

Example:

use formally::{support::*, smt::*};

let mut scope = Scope::new();
scope.push();
scope.add("x", Loc::new(42));

println!("x: {}", scope.lookup(Identifier::from("x")).one()?);

scope.pop();
assert!(scope.lookup(Identifier::from("x")).all()?.is_empty());

Here the LookupSet::one() method requires a single result to exist and emits detailed diagnostics if this is not the case. See its documentation for details.

The element type needs to implement Hash and Eq. These are used to ensure that if the same element is added twice under the same name, it is treated as a single entry.

Scope objects support being nested under other Scope objects. Nesting simulates how one would implement a nested scope in a typical language, such as the scope under a function definition that sees its arguments locally but the elements declared outside globally. Elements defined in the local Scope shadow the ones defined in the parent, but if no element is defined at all with a given name, lookup is delegated to the parent.

Example:

use formally::{support::*, smt::*};

let mut parent = Scope::new();
parent.add("x", term!(p));
parent.add("x", term!(q));
parent.add("y", term!(and p q));

let mut scope = Scope::new().with_parent(parent);

scope.add("x", term!(=> p q));

scope.lookup("x").one()?;
scope.lookup("y").one()?;

Note that the first call to one() succeeds here because the only element declared in scope with name "x" shadows all the elements with the same name in parent. The second one succeeds as well because "y" is found in the parent.

Implementations

impl<T: Hash + Eq> Scope<T>

pub fn new() -> Self

Construct an empty Scope

pub fn with_parent(self, parent: Scope<T>) -> Scope<T>

Construct a new Scope similar to self but nested under a different parent.

pub fn set_parent(&mut self, parent: Scope<T>)

Set a new parent to the current Scope.

pub fn add(&mut self, name: &str, element: T)

Add an element to the Scope under the given name.

pub fn lookup<'i>( &self, name: impl Into<Identifier<'i>>, ) -> LookupSet<'_, 'i, T, &T>

impl<T: Clone + Hash + Eq> Scope<T>

pub fn merge(&mut self, other: &Scope<T>)

Clone all the elements of the given scope into self, registering them under the same names.

Trait Implementations

impl<T: Hash + Eq> Clone for Scope<T>

where Stacked<HashTrieMapSync<String, HashTrieSetSync<T>>>: Clone, Option<Arc<Scope<T>>>: Clone,

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: Hash + Eq> Default for Scope<T>

where Stacked<HashTrieMapSync<String, HashTrieSetSync<T>>>: Default, Option<Arc<Scope<T>>>: Default,

fn default() -> Self

Returns the “default value” for a type.

impl<T: Hash + Eq> Stack for Scope<T>

fn push(&mut self) -> Result<()>

Push the current state of the object to the stack.

fn pop_n(&mut self, n: usize) -> Result<()>

Pop n frames from the stack, restoring the state of the nth topmost frame.

fn pop(&mut self) -> Result<()>

Shortcut for pop_n(1)