ucsd-progsys/liquidhaskell

Cannot parse specification

Open

#1,781 opened on Oct 22, 2020

View on GitHub
 (0 comments) (0 reactions) (0 assignees)Haskell (1,306 stars) (157 forks)batch import
good first issue

Description

{-@ inline id' @-}
id' x = x

{-@ arith :: { id' ( 2 <= 2 ) } @-}
arith = ()

yields:

/home/zgrannan/rewriting-paper/optimization/arith.hs:4:20: error:  Cannot parse specification:
                                                                       unexpected "( "
                                                                       expecting "&&", "->", "<:", "<=>", "==>", "=>", "||", "~>", ':', '}', or monoPredicateP

This is a contrived example but I've run into similar issues generating LH specifications programmatically.

In general I would expect that if the expression {-@ thm : { x } @-} parses, then {-@ thm : { id' (x) } @-} should also parse (excluding the LH builtin operators not already present in Haskell, such as <=>)

Contributor guide

Tech stack
None
Domain
tooling
Issue type
bug
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-3 hours
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
stale
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
mostly clear
Prerequisites
basic Haskell knowledgefamiliarity with Liquid Haskell
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
20
Research direction
Look into the Liquid Haskell parser, likely in the 'liquidhaskell' source under 'src/Language/Haskell/Liquid/Parse' or similar. Investigate how specifications with function applications inside curly braces are parsed. The issue expects that if 'thm : { x }' parses, 'thm : { id' (x) }' should also parse. Check the parser grammar for the spec language to see why parentheses after a function name cause a parse error.