A slightly experimental add-on for Alloy involving the idea of routes to a particular part of a tree.
- data Route inner outer
- routeModify :: Route inner outer -> (inner -> inner) -> outer -> outer
- routeModifyM :: Monad m => Route inner outer -> (inner -> m inner) -> outer -> m outer
- routeGet :: Route inner outer -> outer -> inner
- routeSet :: Route inner outer -> inner -> outer -> outer
- (@->) :: Route mid outer -> Route inner mid -> Route inner outer
- identityRoute :: Route a a
- routeId :: Route inner outer -> [Int]
- routeList :: Int -> Route a [a]
- makeRoute :: [Int] -> (forall m. Monad m => (inner -> m inner) -> outer -> m outer) -> Route inner outer
- routeDataMap :: Ord k => Int -> Route (k, v) (Map k v)
- routeDataSet :: Ord k => Int -> Route k (Set k)
- class AlloyARoute t o o' where
- data BaseOpARoute m outer = BaseOpARoute
- baseOpARoute :: BaseOpARoute m outer
- data (t :-@ opT) m outer = ((t, Route t outer) -> m t) :-@ (opT m outer)
- type OneOpARoute t = t :-@ BaseOpARoute
- type TwoOpARoute s t = s :-@ (t :-@ BaseOpARoute)
A Route is a way of navigating to a particular node in a tree structure.
Let's say that you have some binary tree structure:
data BinTree a = Leaf a | Branch (BinTree a) (BinTree a)
Suppose you then have a big binary tree of integers, potentially with duplicate values, and you want to be able to modify a particular integer. You can't modify in-place, because this is a functional language. So you instead want to be able to apply a modify function to the whole tree that really just modifies the particular integer, deep within the tree.
To do this you can use a route:
myRoute :: Route Int (BinTree Int)
You apply it as follows (for example, to increment the integer):
routeModify myRoute (+1) myTree
This will only work if the route is valid on the given tree.
The usual way that you get routes is via the traversal functions in the module.
Another useful aspect is composition. If your tree was in a tree of trees:
routeToInnerTree :: Route (BinTree Int) (BinTree (BinTree Int))
You could compose this with the earlier route:
routeToInnerTree @-> myRoute :: Route Int (BinTree (BinTree Int))
These routes are a little like zippers, but rather than building a new data type to contain the zipped version and the re-use aspect, this is just a simple add-on to apply a modification function in a particular part of the tree. Multiple routes can be used to modify the same tree, which is also useful.
Routes support Eq, Show and Ord. All these instances represent a route as a list of integers: a route-map. [0,2,1] means first child (zero-based), then third child, then second child of the given data-type. Routes are ordered using the standard list ordering (lexicographic) over this representation.
Applies a pure modification function using the given route.
Applies a monadic modification function using the given route.
Given a route, gets the value in the large data structure that is pointed to by that route.
Given a route, sets the value in the large data structure that is pointed to by that route.
Composes two routes together. The outer-to-mid route goes on the left hand side, and the mid-to-inner goes on the right hand side to form an outer-to-inner route.
The identity route. This has various obvious properties:
routeGet identityRoute == id routeSet identityRoute == const routeModify identityRoute == id identityRoute @-> route == route route @-> identityRoute == route
Gets the integer-list version of a route. See the documentation of
Given an index (zero is the first item), forms a route to that index item in the list. So for example:
routeModify (routeList 3) (*10) [0,1,2,3,4,5] == [0,1,2,30,4,5]
Given the integer list of identifiers and the modification function, forms
a Route. It is up to you to make sure that the integer list is valid as described
in the documentation of
Route, otherwise routes constructed this way and via
the Alloy functions may exhibit strange behaviours when compared.
Constructs a Route to the key-value pair at the given index (zero-based) in the ordered map. Routes involving maps are difficult because Map hides its internal representation. This route secretly boxes the Map into a list of pairs and back again when used. The identifiers for map entries (as used in the integer list) are simply the index into the map as passed to this function.
Constructs a Route to the value at the given index (zero-based) in the ordered
set. See the documentation for
routeDataMap, which is nearly identical to
An extension to
AlloyA that adds in
Routes. The opsets are now parameterised
over both the monad/functor, and the outer-type of the route.
The type that extends an applicative/monadic opset (opT) in the given
functor/monad (m) to be applied to the given type (t) with routes to the
outer type (outer). This is for use with the
A handy synonym for a monadic/applicative opset with only one item, to use with