search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Decompiler improvements meta #90

Open tlringer opened 3 years ago

tlringer commented 3 years ago

Needs triaging into issues. Some ideas to refer to as RanDair continues his work:

  1. Custom tactics & decision procedures (WIP)
  2. Comment & format preservaton
  3. Removing additional arguments to apply and rewrite
  4. Looking directly at old tactic scripts instead of just taking tactics as arguments
  5. Improving performance
  6. Custom tactics that aren't decision procedures (especially non-solving tactics)

Blocked by current work on (1) right now.