ucsd-progsys/liquidhaskell

Cannot parse specification

Open

#1,781 创建于 2020年10月22日

在 GitHub 查看
 (0 评论) (0 反应) (0 负责人)Haskell (1,306 star) (157 fork)batch import
good first issue

描述

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

贡献者指南