ucsd-progsys/liquidhaskell

Cannot parse specification

Open

#1781 aperta il 22 ott 2020

Vedi su GitHub
 (0 commenti) (0 reazioni) (0 assegnatari)Haskell (157 fork)batch import
good first issue

Metriche repository

Star
 (1306 star)
Metriche merge PR
 (Merge medio 2g 18h) (12 PR mergiate in 30 g)

Descrizione

{-@ 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 <=>)

Guida contributor

Direzione di ricerca
Esplora il codice sorgente del parser di Liquid Haskell per capire perché la specifica non viene analizzata. Concentrati sulla gestione delle parentesi nei tipi di raffinamento e traccia il percorso dell'errore a partire da `parseSpec`. Cerca come viene analizzata l'applicazione di funzione all'interno delle parentesi.
Tech stack
Nessuno
Dominio
backend
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
HaskellLiquid Haskell
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
60