septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Variable interpolation in symbols #109

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

This PRQ changes the AST and internal representation of symbolic variables so that tokens of the form #<int> are parsed and stored as argument placeholders. This allows the Starling pretty printer, among other things, to interpolate arguments into those positions.

The pretty printer representation of a symbol %{foo #1 bar #2 baz}(x, y) has now changed to

(sym "foo x bar y baz")

This change will make it much easier immediately to work with symbolic proofs, but is mainly here to facilitate Grasshopper.

Summary of changes:

There is currently no way to represent a # in a Starling symbol. If this becomes a problem we can change the parser to interpret ## as a #.

MattWindsor91 commented 7 years ago

@BenSimner is this one you could check? If not then @septract is leading on Grasshopper so maybe this would be in scope for him to check

septract commented 7 years ago

This all looks good to me - @CaptainHayashi please go ahead and merge if you're happy.