Add simple pruning and folding abilities to LMC tools #43
Conversation
There was a problem hiding this comment.
This is a huge improvement in readability over the previous version! The commits were tight and easy to review. Thanks for your patience in me getting to this.
Really, the only thing that bothered me besides the other comment I gave is that some operations in your spec are partial, e.g.
intersectfails to be defined when passed twoNodeIds where both have the form:NorN[F]nodesandfrontierdefined overFoldedLabelGraph?fail to be defined when they are applied to aFoldedLabelGraphwhich is a subtype ofFoldedLabelGraph?
I prefer functions to be total unless otherwise specified, so I would like to see that changed or at least marked partial.
However, ultimately, my issues are matters of taste rather than correctness, so I'll mark this approved and leave it up to you.
| op _[_] : Nat Fold -> NodeId [right id: .Fold prec 20] . | ||
| -------------------------------------------------------- | ||
| A `NodeMap` is a lookup table of `Nat |-> Node`, which supports a lookup `_[_]` and `insert` operation. | ||
| The insert operation is aware of the user defined `Fold`s, and will not create new entries for new nodes that are less general than existing ones. | ||
|
|
There was a problem hiding this comment.
I find the NodeMap? data structure name somewhat misleading. As far as I can tell, a NodeMap? always corresponds to a NodeMap --- in my mind, adding a question mark to the end sort of connotes a partial operation; AFAICT insert which returns one, is not partial.
I know you prefer compact names, so if a more descriptive name is out of the question, I think it would be worth it to just note that this data structure is just an intermediate used to track when fresh nodes have been added to a NodeMap. Also, AFACIT, the NodeSet argument in NodeMap? is always either a singleton Node or .NodeSet. If that is true, I think that would be nice to note as well.
It seems that, at least here, the question mark denotes that essentially the same type but with extra metadata attached to it; FoldedLabeledGraph? seems to use a similar naming convention, though I don't mind as much in that case since I think that may actually not always reduce into a FoldedLabeledGraph, i.e. in case stepping over the frontier fails.
No description provided.