ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Interactive shell fails to parse names that include literal syntax #125

Closed ecaustin closed 9 years ago

ecaustin commented 9 years ago

When working with a module that contains bindings with names that include literal syntax, e.g. $fMonad[] ∷ Monad [], you cannot interact with those bindings by name.

Attempting to do so throws an expression type checking error: hermit<0> binding-of '$fMonad[] Error in expression: binding-of '$fMonad [] Does not type-check: binding-of '$fMonad []

The parser separates the literal syntax from the name, creating an ill-typed application.

andygill commented 9 years ago

Have you tried

binding-of "$fMonad[]"
ecaustin commented 9 years ago

Yup, that works if you prepend the string with the tick operator to signal that it's a name, i.e. binding-of '"$fMonad[]".

I'll leave it up to you if you want to close the issue or not depending on how hard the fix is to not require double-quotes.

xich commented 9 years ago

The double quotes solution was a quick fix at one point (for the SYB stuff) that never got properly fixed. All the parsers (especially for Core) need rewriting/expanding. On May 21, 2015 6:28 AM, "Evan Austin" notifications@github.com wrote:

Yup, that works if you prepend the string with the tick operator to signal that it's a name, i.e. binding-of '"$fMonad[]".

I'll leave it up to you if you want to close the issue or not depending on how hard the fix is to not require double-quotes.

— Reply to this email directly or view it on GitHub https://github.com/ku-fpg/hermit/issues/125#issuecomment-103987147.[image: Web Bug from https://github.com/notifications/beacon/AABNAKk8xbFcl3pIm-i9MAK8dRMWmAMxks5oLMnhgaJpZM4EiMGk.gif]

ecaustin commented 9 years ago

I'm going to close this since the new shell requires string-like names which is a known work-around to this issue.