jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
39 stars 9 forks source link

expose the formula parser #23

Closed m4lvin closed 1 year ago

m4lvin commented 1 year ago

Given the string ¬K₂K₁M₂¬(¬K₁(¬M₂b → a) ∨ ¬¬¬(¬(c ∨ a) ∧ a)) (from here) there currently is no nice and automatic way to make a Form out of it, even though SMCDEL.Internal.Parse has all the information for doing so.

This can be solved by asking Happy to generate multiple parsers: https://haskell-happy.readthedocs.io/en/latest/using.html#generating-multiple-parsers-from-a-single-grammar