quantomatic / quantomatic Goto Github PK

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

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

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.

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.

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

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.

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.

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.

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.

Steps:

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

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.

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).

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.

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.

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")

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.

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

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).

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

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

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.

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.

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.

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

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.

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.

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

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!

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).

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

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

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

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.

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

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

"

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

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

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.

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.

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.

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

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

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

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.

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.

Steps:

• In the gui, create a graph
• normalize it

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

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

Also graphs?

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.

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).