Crate grabapl_template_semantics

Source

Expand description

This library defines the ‘pluggable’ parts of a grabapl implementation.

These are all contained in the Semantics trait, which this library implements for the TheSemantics holder type.

For the non-pluggable parts of a grabapl implementation, see the grabapl crate and documentation.

§Type Systems

The example semantics we’re defining here is made up of a node and edge type system as follows:

§Node Type System

We have the following node values (also known as concrete node values) - see NodeValue:

i32 - representing integers (1, 2, -3, etc.)
String - representing strings (“hello”, “world”, “”, etc.)

We have the following node types (also known as abstract node values) - see NodeType:

Integer - representing nodes that hold integer values
String - representing nodes that hold string values
Any - a wildcard type that matches any node type, i.e., it represents nodes that can hold both integer and string values

See NodeConcreteToAbstract for the implementation of getting the most precise node type of a node value.

The type system on those types is induced by the following partially ordered set, visualized as a Hasse diagram:

          Any
         /   \
        /     \
    Integer  String

In other words, Integer and String are subtypes of Any, Any is a supertype of both, and a String is not a subtype of Integer and vice versa. See NodeSubtyping for the implementation of this type system.

§Edge Type System

We have the following edge values (also known as concrete edge values) - see EdgeValue:

() (the unit type) - representing no interesting value besides presence (i.e., just the singleton value () of the unit type)
String - representing strings (“next”, “parent”, etc.)
i32 - representing integers (1, 2, -3, etc.)

We have the following edge types (also known as abstract edge values) - see EdgeType:

(), the unit type - representing edges that do not carry any additional value besides presence
ExactString(s) - representing edges that carry the specific string value s, e.g., ExactString("next") represents exactly those edges with a string value of "next".
String - representing edges that carry a string value
Integer - representing edges that carry an integer value
Any - a wildcard type that matches any edge type, i.e., it represents edges that can carry (), string, and integer values)

See EdgeConcreteToAbstract for the implementation of getting the most precise edge type of an edge value.

The type system on those types is induced by the following partially ordered set, visualized as a Hasse diagram:

              ____Any____
             /     |     \
            /      |      \
          ()   String      Integer
               / ... \
ExactString("a") ...  ExactString("zzzz...")

In other words, all types are subtypes of Any, ExactString(s) is a subtype of String for any string s, and String and Integer and () are not subtypes of each other. and there are no other relationships between the types. See EdgeSubtyping for the implementation of this type system. The notion of storing a concrete string value inside a type is closely related to (but much weaker than) refinement types.

§Operations and Queries

Additionally, every Semantics implementation can define its own set of “builtin” operations and queries. These are arbitrary Rust functions (or any other language through FFI and/or interpreters) that operate on the graph.

§Builtin Operations

Builtin operations are defined by the BuiltinOperation trait, which we have implemented for the TheOperation enum.

Builtin operations can be used to manipulate the graph, e.g., adding nodes or edges, removing them, changing their values, etc., but also for anything side-effectful, like printing a trace to the console.

There is a set of generic operations that are defined in the LibBuiltinOperation enum, which can be used to perform common operations on the graph independent of the custom semantics.

See the BuiltinOperation trait for more details on how to implement operations.

§Builtin Queries

Queries are defined by the BuiltinQuery trait, which we have implemented for the TheQuery enum.

Queries can be used to retrieve information from the graph that is used to decide which branch of two to take. Essentially, these are the if conditions of traditional programming languages. Notably, queries do not return a first-class node value, but rather a value only visible in how the control flow of the program proceeds.

See the BuiltinQuery trait for more details on how to implement queries.

For queries that are supposed to change the statically known abstract graph, see [TODO: link to GraphShapeQuery

§Optional Features

See the syntax module if you want to use this semantics in concjuction with grabapl’s pluggable syntax parser and interpreter.

§Usage

Once the semantics is defined, it can be used to build user defined operations and run operations on concrete graphs.

Continue in template/README.md for the next steps.

§Your Turn

Feel free to copy this crate and adjust the semantics to your liking!

Modules§

syntax: Defines the textual syntax of our semantics for plugging into grabapl’s syntax parser.

Structs§

EdgeConcreteToAbstract: Defines the most precise edge type of an edge value via its ConcreteToAbstract implementation.
EdgeJoiner: Defines the join operation for edge types via its AbstractJoin implementation.
EdgeSubtyping: Defines the subtyping relationships between edge types via its AbstractMatcher implementation.
NodeConcreteToAbstract: Defines the most precise node type of a node value via its ConcreteToAbstract implementation.
NodeJoiner: Defines the join operation for node types via its AbstractJoin implementation.
NodeSubtyping: Defines the subtyping relationships between node types via its AbstractMatcher implementation.
TheSemantics: Defines the semantics of a client implementation via its Semantics implementation.

Enums§

EdgeType: The edge types used in our example semantics.
EdgeValue: The edge values used in our example semantics.
IntComparison: The different ways to compare integer values.
NodeType: The node types used in our example semantics.
NodeValue: The node values used in our example semantics.
TheOperation: A value of this type represents a specific builtin operation in the semantics.
TheQuery: A value of this type represents a specific builtin query in the semantics.

Crate grabapl_template_semanticsCopy item path