Module system¶

The module class is the entry point for building modules to be analysed or solved.

class module : public black::pipes::consumer¶

Entry point to build modules.

The module class mantains sets of declarations, requirements (sometimes called assertions), and other elements in a stack that can be manipulated with the push() and pop() member functions.

module is a regular type (also known as value type), i.e., it is default-initializable, copy-constructible, move-constructible, and equality-comparable. Thanks to the underlying usage of persistent data structures, all these operations are also quite fast, so module objects are meant to be freely passed around by value. A dynamic allocation of a small object is still needed for copies, so moving is still preferred when possible.

Equality is checked deeply against the contents of the modules.

Thanks to persistent data structures, equality comparison is relatively cheap, but some attention has to be payed. Because of how the underlying data structures work, it is cheap to compare two copies of the same module, or two modules where one has been derived from a copy of the other by a few edits.

For example, the following is very cheap:

module m = very_large_module();
module m2 = m; // cheap copy

assert(m2 == m); // the cheapest

m2.require(x == y);

assert(m != m2); // still cheap

Comparing two different modules is also usually cheap because of short-curcuiting. However, comparing completely unrelated modules that somehow happen to be equal or very similar is potentially expensive, because all the contents of the modules will have to be compared.

Note

Declarations/definitions that are pending because of calls to declare() or define() with delayed resolution mode are not retained in copies.

Constructors, assignment and comparison

module()¶: Default constructor. Constructs an empty module.

module &operator=(module const&)¶: Copy-assignment operator.

module &operator=(module&&)¶: Move-assignment operator.

bool operator==(module const&) const¶: Equality comparison operator.

Declarations, definitions, and name lookup.

virtual void import(module m) override¶

Imports another module.

The names visible in the imported modules will be visible in this one, but will be shadowed by those with the same name declared in this module.

If two imported modules declare the same names, the module imported last has precedence and shadows the others.

Parameters:: m – the imported module.

object declare(decl d, resolution r = resolution::immediate)¶

Declares a new entity.

Declares an entity of name d.name and type d.type.

The resolution mode r determines when name lookup is applied to unbound variables:

if r is resolution::immediate, any unbound variable present in d.type is resolved immediately using resolved();
if r is resolution::delayed, the name will not be visible until the next call to the resolve() function, which will resolve d.type.

Note

Declarations that are pending because of calls to declare() or with delayed resolution mode are not retained in copies.

Parameters:

d – the decl object describing the new declaration.
r – the resolution mode (see resolution).

Returns:

an object representing the newly declared entity.

object declare(variable name, types::type type, enum role role = role::rigid, resolution r = resolution::immediate)¶

Declares a new entity.

Calls declare(decl{name, type}, r).

Parameters:

name – the name of the entity.
type – the type of the entity.
r – the resolution mode (see resolution)

object define(def d, resolution r = resolution::immediate)¶

Defines a new entity.

Defines an entity of name d.name, type d.type and value d.value. If d.type is an inferred_type term, the type is inferred from d.value, when possible (for now, recursive definitions cannot be type-inferred).

The resolution mode r determines when name lookup is applied to unbound variables:

if r is resolution::immediate, any unbound variable present in d.type is resolved immediately using resolved();
if r is resolution::delayed, the name will not be visible until the next call to the resolve() function, which will resolve d.type.

Note

Definitions that are pending because of calls to define() with delayed resolution mode are not retained in copies.

Parameters:

d – the def object describing the new definition.
r – the resolution mode (see resolution).

Returns:

an object representing the newly defined entity.

object define(variable name, types::type type, term value, resolution r = resolution::immediate)¶

Defines a new entity.

Calls define(def{name, type, value}, r).

Parameters:

name – the name of the entity.
type – the type of the entity.
value – the defining value of the entity.
r – the resolution mode (see resolution)

object define(variable name, term value, resolution r = resolution::immediate)¶

Defines a new entity with an inferred type.

Calls define(def{name, value}, r).

Parameters:

name – the name of the entity.
value – the defining value of the entity.
r – the resolution mode (see resolution)

object define(function_def f, resolution r = resolution::immediate)¶

Defines a new function.

Defines a function of name f.name, parameters described by decl objects in f.parameters, range f.range, and body f.body. If f.type is an inferred_type term, then the range type is inferred from f.body, when possible (for now, recursive definitions cannot be type-inferred).

This function is equivalent to calling define() with a def object specifying a function_type type and a lambda with matching parameters as value.

The resolution mode r determines when name lookup is applied to unbound variables:

if r is resolution::immediate, any unbound variable present in d.type is resolved immediately using resolved();
if r is resolution::delayed, the name will not be visible until the next call to the resolve() function, which will resolve f.type.

Parameters:

f – the function_def object describing the new function.
r – the resolution mode (see resolution).

Returns:

an object representing the newly defined function.

object define(variable name, std::vector<decl> parameters, types::type range, term body, resolution r = resolution::immediate)¶

Defines a new function.

Calls define(function_def{name, parameters, range, body}, r).

Parameters:

name – the name of the function.
parameters – the parameters of the function.
range – the range (return type) of the function.
body – the body of the function.
r – the resolution mode (see resolution)

object define(variable name, std::vector<decl> parameters, term body, resolution r = resolution::immediate)¶

Defines a new function with an inferred return type.

Calls define(function_def{name, parameters, body}, r).

Parameters:

name – the name of the function.
parameters – the parameters of the function.
body – the body of the function.
r – the resolution mode (see resolution)

virtual void adopt(std::shared_ptr<root const> r) override¶

Adopts a root and all the entities it collects.

Adopts in this module a set of entities, possibly created using other modules, collected by the given root. The entities referred to by the objects become visible in the module as if they were declared or defined by the declare() or define() functions.

If the pointer is nullptr the function does nothing.

Parameters:: r – a shared pointer to the root to be adopted

void adopt(object obj)¶

Adopts an object and its siblings.

The entity represented by the given object is adopted together with all the entities collected by the same root.

The call to m.adopt(obj) is roughly the same as m.adopt(obj.entity()->root.lock()).

If obj.entity()->root is null, the function does nothing. This happens when the object has been returned by a call to declare() or define() with resolution::delayed and resolve() has not been called yet.

Parameters:: obj – the object to adopt.

std::optional<object> lookup(variable x) const¶

Looks up a name in the current module and returns the corresponding object.

Name lookup is performed in this order:

the entities declared, defined, or adopted in the current module, in the reverse order (i.e. most recent entities shadow previous ones);
the entities declared, defined, or adopted in any imported module, with more recently imported modules shadowing previous ones.

Parameters:: x – the variable to look up.
Returns:: the object associated to x in the current module, or an empty optional if the name cannot be found.

term resolved(term t) const¶

Resolves unbound variables in a term by name lookup in the current module.

Returns a term obtained from the given term t where each unbound variable is replaced by the corresponding object as found by lookup(), or is left unchanged if lookup() returns an empty optional.

Parameters:: t – a term.
Returns:: the resolved term

std::shared_ptr<root const> resolve(recursion s = recursion::forbidden)¶

Resolves and completes the declaration/definition of pending entities.

This function completes the declaration or definition of entities declared or defined with declare() or define() where the r parameter was set to resolution::delayed. The terms employed for types and bodies of the entities are resolved similarly to resolved() using name lookup in the current module.

The scope resolution mode determines whether recursion is allowed.

if s is scope::linear, the pending entities do not see each other, and therefore cannot refer recursively to each other or themselves.
if s is scope::recursive, all the pending entities, regardless of the order of declaration/definiton, see each other, and thus can refer recursively to any other entity in the group (themselves included).

The

Note

As also noted in define(), types of recursive definitions cannot be automatically inferred, at the moment.

Parameters:: s – the scope resolution mode (see scope).
Returns:: a shared pointer to the root collecting the entities resolved in this call.

Specifications and requirements

virtual void state(logic::term t, statement s) override¶

Adds a statement to the module.

Statements can be of different kinds:

requirements (statement::requirement): asserts that t holds in any model of the module;
initial states (statement::init): asserts that t holds in the initial state of the module;
transitions (statement::transition): asserts that t holds during any transition of the module;
final states (statement::final): asserts that req must hold at the end of any execution of ht e module.

Parameters:

t – the statement.
s – the kind of statement

inline void require(term req)¶: Same as state(req, statement::requirement).

inline void init(term t)¶: Same as state(req, statement::init).

inline void transition(term t)¶: Same as state(t, statement::transition).

inline void final(term t)¶: Same as state(t, statement::final).

Stack management

virtual void push() override¶: Pushes a new frame on the module’s stack.

virtual void pop(size_t n = 1) override¶

Pops a given number of frames from the module’s stack.

Calls to this function cause any call to the import(), declare(), define(), adopt(), and state() functions, executed after the last n calls to push(), to be undone.

If less than n calls to push() have been issued before (e.g. n==1 and no call to push() happened at all), the module is reset empty, as just after default construction.

Note

Declarations/definitions that are pending because of calls to declare() or define() with delayed resolution mode are not affected by push() and pop() calls until they are resolved with resolve().

Parameters:: n – the number of frames to pop.

Module traversal

void replay(module from, pipes::consumer *target) const¶

Replays all the differences of the current module from a given one.

Issues a sequence of calls to a set of member functions of target for each difference between *this and *from.

a call to target.import(m) for each module m imported in *this but not in from.
a call to target.adopt(objs, s), for each set of entities declared/defined/adopted in *this but not in from.
a call to target.state(t, s) for each term t of kind s stated with state() in*thisbut not infrom.
a call totarget.push()for each frame level pushed in*thisbut not infrom(in the suitable order w.r.t. the previous items).
a call totarget.pop(n)for eachnframes that have to be popped fromfromto make it a subset of*this`.

The types of the arguments of each call are the same as the corresponding member functions of module with the same name.

The calls are arranged in such a way that, for any pair of modules m and from, if m has no pending declaration/definitions, and the following call is issued:

m.replay(from, &from);

then m == from is guaranteed to hold.

Note that a copy construction is sufficient to achieve the same equality. The purpose of this function is rather to be used with target objects of different types, as a way of observing the changes made to a module w.r.t. to from.

This can also be used as a general iteration mechanism over all the constituent elements of the module (e.g. by providing an empty from module).

If target == nullptr, the function does nothing.

Note

Declarations/definitions that are pending because of calls to declare() or define() with delayed resolution mode are not replayed by replay, until they are resolved with resolve().

Note

This function can be very efficient for the intended use cases, but the same caveat of the equality comparison operator apply, see the discussion above. For instance, if *this and *from are equal, but they are unrelated (i.e. one has not been obtained as a copy of the other), replay() may take some time to realize there is nothing to replay.

Parameters:

from – the module starting point of the replay.
target – a pointer to the object where replay calls are issued.

struct impl_t¶

struct frame_t¶

struct req_t¶

struct decl¶

The specification of an entity to be declared in a module.

Constructors

inline decl(variable name, logic::types::type type, enum role role)¶: Constructs the object.

inline decl(logic::variable name, logic::types::type type)¶: Constructs the object with a default role of role::rigid.

Public Functions

bool operator==(decl const&) const = default¶: Equality comparison.

inline size_t hash() const¶: Hash function.

Public Members

logic::variable name¶: The name of the entity.

logic::types::type type¶: The type of the entity.

enum role role¶: The role of the entity. The role is ignored when decl is used in lambda terms.

struct def¶

The specification of an entity to be defined in a module.

Constructors

def(variable name, types::type type, term value)¶: Constructs the def object.

def(variable name, type value)¶: Constructs the def object with the type set to inferred_type(), to be inferred automatically from value.

Public Members

variable name¶: the name of the entity.

types::type type¶: the type of the entity.

term value¶: the defining value of the entity.

struct function_def¶

The specification of a function to be defined in a module.

Constructors

inline function_def(variable name, std::vector<decl> parms, type range, term body)¶: Constructs a function_def.

inline function_def(variable name, std::vector<decl> parms, term body)¶: Constructs a function_def where the type is set to inferred_type(), to be inferred automatically from the function body.

Public Members

variable name¶: the name of the function.

std::vector<decl> parameters¶: the parameters of the function.

type range¶: the range (return type) of the function.

term body¶: the body of the function.

enum class black::logic::role : uint8_t¶

Which role a declaration have in a module.

Values:

enumerator rigid¶: rigid declaration, does not change over time

enumerator input¶: input variable of the module

enumerator state¶: state variable of the module

enumerator output¶: output variable of the module

enum class black::logic::resolution : bool¶

The resolution behavior of declarations and definitions in module.

Used in functions module::declare() and module::define() to specify whether a declared/defined entity must be resolved immediately or at the next call to module::resolve().

Values:

enumerator delayed¶: wait the next call to module::resolve().

enumerator immediate¶: resolve immediately.

enum class black::logic::recursion : bool¶

The scope resolution mode for module::resolve() and root::mode

Values:

enumerator forbidden¶: Non-recursive name resolution.

enumerator allowed¶: Recursive name resolution.

enum class black::logic::statement : uint8_t¶

Kind of statements that can be given to module::state().

Values:

enumerator requirement¶: A requirement.

enumerator init¶: A constraint on the initial state.

enumerator transition¶: A constraint on the transition relation.

enumerator final¶: A constraint on the final state.

struct entity¶

Internal representation of an entity declared or defined in a module.

An entity object represents an entity declared or defined in a module. Entity objects are stored internally in modules and are usually not handled explicitly during normal usage of the API.

Entities are created in groups by collecting them at each call to resolve(), or declare()/define() with resolution::immediate. The lifetime of each entity in such groups is managed exclusively by root objects whose pointers are returned by the corresponding resolve() call, and pointed by the entity::root field. Therefore as long as the root object is alive, the corresponding entity instances are safe to use.

Constructors

inline entity()¶: Constructs an empty entity.

inline explicit entity(decl d)¶: Constructs the entity from a decl.

inline explicit entity(def d)¶: Constructs the entity from a def.

Public Members

std::weak_ptr<struct root const> root¶: The pointer to the root managing this entity object.

variable name¶: The name of the entity.

types::type type¶: The type of the entity.

std::optional<term> value¶: The value of the entity. Empty if the entity is declared.

std::optional<enum role> role¶: The role of the entity Empty if the entity is defined.