SemGuS-git / Semgus-Parser

Library and tool for parsing SemGuS specifications
MIT License
4 stars 1 forks source link

Grammar form should be two separate lists #71

Closed kjcjohnson closed 2 years ago

kjcjohnson commented 2 years ago

After close reading of the SyGuS spec (and attempting to implement SyGuS-to-CHC on-the-fly conversion), I noticed that the parser currently wants the grammar block to be wrapped in a list:

(synth-fun f ((name String)) String
    ( ;; <-- grammar block start here
      ((A Int) (B Bool))
      ((A Int (...))
       (B Bool (...)))
    ) ;; <-- grammar block end here
)

but the SyGuS spec doesn't prescribe this outer wrapping, being just:

(synth-fun f ((name String)) String
      ((A Int) (B Bool)) ;; <-- Nonterminal predeclarations
      ((A Int (...))     ;; <-- Productions
       (B Bool (...)))
)