zxcalc/quantomatic

Quantomatic is a tool for doing automated graph rewriting.

quantomatic's Issues

Edges vanish when renaming, come back later

The GUI isn't keeping edge connections sync'ed with the core when you rename boundary vertices. Re-name a boundary with edges connected, and the edges vanish. Close and re-open and they return.

Empty !-boxes not displayed

It is possible to have a graph with an empty !-box [not sure how you create one with the GUI, but...]

These should be displayed somewhere, so they can be manipulated or deleted.

Deleting rules

there seems to be no way to delete a rule from the ruleset.

Shortcut keys

These are inconsistent. For example, hitting 'E' opens undirected edge mode, but doesn't change tool. Would be good to have (displayed somewhere) hotkeys for all three.

Regression: save and load dialogs should remember previous location

This used to be the case, but it must have gotten clobbered at some point.

Saving rule should complain if !-boxes or boundaries don't match

Right now it just silently accepts it and crashes quanto when it tries to rewrite.

create rule from rewrite sequence

We should make an easy way to create a new rule based on a rewrite sequence. I imagine it working like this: make a graph; press "record"; do rewrites; press "stop record"; a pop-up now prompts for the name of the new rule, and adds it to the rule set.

As a first attempt, the process should complain if the user tries to do anything other than rewrites: i.e. add nodes etc. I can imagine smarter things for later iterations of this feature.

Mac app

The Mac app target doesn't seem to work at all. E.g. it does nothing when you hit "show rewrites".

When a tag is selected in the RulesBar, should other tags be deactivated?

It is unintuitive to have active rules that you can't see. So the natural thing would be to disable all other rules when you switch to a tag.

HOWEVER, we also don't want the active rule set to be changed if a user switches to a tag and back again.

The ideal behaviour is:
user switches to a tag -> only the intersection of the previously-active rules and the rules in the selected tag are active
user switches back to "All rules" -> exactly the same rules are active as were before switching to the tag, except for those where the user has explicitly enabled/disabled rules while in the tag view

So all->tag->all should have no effect
all->tag->disable rule1->all should be the same as all->disable rule1
all->tag->enable rule1->all should be the same as all->enable rule1

Not sure how best to implement this.

Matching multiple self-loops takes a LONG time

I think there is a problem with the matching algorithm when there are !-boxes and self loops. I.e. it finds way too many match combos.

reorder rules in ruleset

Fast normalise should pick rules in the order the are listed in the ruleset. This order should be changable.

GUI: Refresh rules automatically when a new theory is loaded

When a new theory is loaded in the GUI, the current ruleset may not be supported by that theory. The user needs to click on "Refresh Rules" to clear the "Rulesbar" component.
It should be done automatically

change_theory in the console horribly breaks everything

Users can change the current theory using the console. This breaks everything, as the open graphs and visualizations do not match the core's idea of the theory.

Not sure what the right solution to this is - probably just to prevent the user doing that, in the same way we prevent the user from calling quit from the console (this code is in the core).

Crash when rewriting

Attempting to rewrite can sometimes crash the core:

06-Mar-2012 16:39:39 quanto.core.protocol.LoggingOutputStream writeLog
FINEST: Sending message to core: ¤<WO¤:165¤|miriam_test-graph¤;8¤:Vb¤,Ve¤,Vh¤,Vc¤,Va¤,Vg¤,Vd¤,Vf¤>
06-Mar-2012 16:39:39 quanto.core.protocol.LoggingInputStream writeLog
SEVERE: Received invalid message: "
"
06-Mar-2012 16:39:39 quanto.core.protocol.ProtocolReader consumeStream
INFO: Discarding data: "Exception trace for exception - ename_already_exists_exp raised in graph.ML line 361

ProtocolInterface.run_in_textstreams(2)run_in_textstreams'(1)
ProtocolInterface.run_in_textstreams(2)
run(1)
End of trace

"

Toolbar shouldn't get keyboard focus

Often the toolbar can grab keyboard focus, so if I hit the space bar to look for rewrites, it creates a new graph instead.

Save-as should warn before overwrite

Save rulesets for all theories at exit

We should store the ruleset state for all theories (that have been modified) when we exit.

Actually, we should probably just do it when we switch theories.

shift-cmd-S = save as

There should be a short-cut for Save-As. Shift-Cmd-s (Shift-Ctrl-s) is the canonical one.

Rules bar context menu only on right-click

The rules bar context menu should show on right-click, not left-click.

C&P layed out sensibly

When I copy & paste a graph that is layed out by hand, the new graph gets squashed into a single line.

The way I suggest fixing this is to re-use the old coordinates, but shift the origin so it is a bit to the right of the top-right vertex in the remainder of the graph.

Keep a local copy of the open theory visualization

When we exit, we should keep a local copy (ie: in the preferences directory?) of the active theory visualization, so that if the original file is moved, deleted or edited, Quantomatic still starts up properly.

Export rewrite sequences

It would very useful if a rewrite sequence from quanto could be exported (perhaps as tikz compatible with Tikzit) so that proofs done in quanto can be used in publications. A bare sequence of graphs would be the minimum useful thing, but extra information that would be useful would be:

• name of the rule used at each step
• indication of where the rule matched in the LHS
• graphical representation of the rule instance used.

copy and paste broken

Copy and Paste seems broken

Copy some graph and press paste. The graph is now marked as edited but the pasted part does not appear. (It doesn't seem to be there, even after doing a "relayout graph")

Tool selection in rule view

When you select a tool like "Directed Edge Mode" while editing a rule, it should change the tool setting for the LHS and the RHS.

Option to re-layout graph

There should be an option in one of the menus to re-layout the graph (using the dot layout).

Vertex stuck in the upper left corner after a normalization

Steps:

• In the gui, create a graph
• normalize it

Result: The last vertex of the rewritten graph is stuck in the upper left corner.

Move the implementation of UI data to the interface

UI data should not be attached to graphs but to the controller.

make the separator a bit darker or something

The separator between the graph view and the rule list needs to be a bit more visible. The number of times I've resized the rule list instead selecting the graph is getting annoying.

Expected ESC got \ua

When trying to attach a rewrite to a vertex with a single self_loop, core crashes with error message as in the title.

Steps to reproduce.
In the gui,
- Create a new red vertex with a self-loop
- Normalize the graph or just try to list the rewrites.
Boom!

Sort out the output of CDATA

Output_user_data is currently using a modified version of Isabelle's XML lib.
Would be better to keep everything in Quanto and not have to modify the General/xml.ML

"Thinking" indicator when core busy

The core often takes quite a long time to generate the list of rewrites, but the gui gives no indication that this is what's happening, as opposed to I just didn't press the key hard enough. FIX: make some visible indicator that the gui is waiting for the core.

Renaming bug when angle variables in pattern and target are the same

Applying the spider rule (with angles alpha and beta) to connected vertices labelled alpha and 0 results in a merged vertex labelled 0. Oops.

Will post examples if I get a chance.

new rule via reversing old rule

It should be possible to create a new rule by reversing an existing rule - i.e just exchanging the left- and right-hand sides.

Right-click on rule; "New rule by reverse", prompt for name (prepopulate field with "old-name-rev"); add rule to rule set.

Auto-save rulesets every so often

Crashes happen. We should make it as painless as possible.

Also graphs?

Get rid of stupid white box in background

The whole background should just be white.

There is the issue of what happens when you hold down CTRL and drag to consider - this moves the view, moving the origin away from the top left. Nodes cannot (currently) be moved above or left of (20,20).

Displayed graph names should refresh more often

The graph name displayed in the drop-down, as well as across the top of the window should refresh more often. For example, it should refresh whenever:

1. a graph is saved, so the asterisk next to the name is removed
2. a graph is modified, so the asterisk is placed next to the name
3. the user does a "save as" to give the graph a new name

Zoom in gui

Would be very useful to zoom in and out in gui when working with large graphs.

Complain when dot not found

If something is done that requires the dot executable for layout, and it could not be found, Quantomatic should complain and/or it should have a fallback.

If there is a fallback, it should complain quietly (like the "Rewriting" status bar when you normalise a graph).

Issues with saving graphs

Open a graph.

Add a node. "Save" does not become ungreyed.

Edit a node label. "Save" does not become ungreyed.

Move a node around. "Save" does not become ungreyed.

Unbang a vertex. "Save" does not become ungreyed.

Banging and deleting nodes and dropping, killing and copying !-boxes does make save become ungreyed.

All the above actions should ungrey save.

unification and fresh names

If you have a rule where the LHS has a vertex is labelled a+b, and in the RHS a and b occur on different vertices, when the rule is matched, "a" will grab whatever is labelling the vertex and the rewritten graph will contain "b" as a variable. If you apply the rule multiple times the same b will occur multiple times. If b is already in the graph it makes no difference.

Solution: need to check if b already occurs and use a fresh name in this situation.

Wrong vertices highlighted when choosing rewrites

When the menu to choose rewrites appears, mousing over the choices highlights virtually all of the graph. Looks like the its highlighting the inverse of what it should.

linrat_expr parsing -1/2

The current parser doesn't recognise -1/2 as a valid expression. It prefers -(1/2). Would be nice to do the right thing here.

Rule creation from the gui does not work in substr_linrat theory

Steps:

• In the gui, load the substr_linrat theory
• Create a rule
• Activate it

rewriting and undo

There seems to be a lot of spurious undo steps. When I do a rewrite and then press undo, it doesn't undo the rewrite, it just fucks around with the layout. After about 10 undos I get back to the graph I had before the rewrite, although the layout is now screwed up.

Fast normalise should be cancellable

The loop in "fast normalise" is entirely in the GUI, so it should be possible to do some threading magic to allow the user to cancel it if it is taking too long.

Possibly something like the "rewriting" bar when doing an ordinary normalisation, but in the middle of the graph view?

Need to consider interleaving commands, I guess - what happens if the user does something else while this is happening. What happens with ordinary normalisation? What if the user tries to change the theory?

Modal dialog is a possibility (although dialogs are generally not very nice).

Vertex positions and undo

Vertex positions should interact well with undo/redo.

Moving a vertex then undoing should move it back.

Rewriting then undoing should give the original layout back.

Renaming edge nodes and !-boxes

It should be possible to rename edge nodes and !-boxes when creating rules

No menus for ruleset buttons

Make the buttons on the ruleset editor apply the action to "selection" by default, instead of showing a menu. This is by far the more common action, and if you want to do something to all rules, it's pretty easy to hit "CTRL+A", then click the button.

Re-name rules

Should be able to change the names of rules once they are created.

Unsaved files should default to save-as on CTRL-S

The expected behaviour if you type CTRL-S (or command-S) on an unsaved file is that it opens the save-as dialogue.