Better subgoal management

[tsani]

• Subgoals are currently stored in a list, which does not reflect the tree-like structure of proofs. It would be great if subgoals were instead stored in a tree structure.
• It would also be cool if there were a way to visualize this structure as an actual tree drawing. This may be unnecessarily difficult to implement in a CLI, but if we go for some kind of GUI later, then this could be really interesting, and provide a nice way to select subgoals visually.
• Subgoals could also have labels attached to them. We already auto-generate labels based on the pattern head (constructor), so we may as well actually attach this metadata to the subgoal itself. EDIT: we do construct subgoal labels now and attach them to each subgoal.
• undo tactic: solved subgoals could still hang around inside the subgoal tree; instead of deleting them, we can simply check whether they're solved so we don't revisit them accidentally. However, an undo feature could be implemented by adding a command to visit a solved subgoal, and then "unsolve"-ing it. This is somewhat nasty because it would delete all proof below that point in the current branch, even though there's just one operation we want to delete. So perhaps a more sophisticated delete command can be implemented by trying to remove the current subgoal, but then re-checking the following commands to see if they still work. EDIT: an undo feature was implemented by maintaining a history of operations and their inverses. In my opinion, the tree based strategy is superior.

[marcelgoh]

Is this related to the fact that let current_subgoal_index gs = 0 always gets the front of the list, but DynArray.add s.remaining_subgoals g; puts new subgoals at the end (in a queue-like manner)? If we pushed new subgoals to the front of the list instead, perhaps we would stay in the same branch.

[tsani]

@marcelgoh Yep. Using DynArray.insert s.remaining_subgoals 0 g should do the trick.