ucsd-progsys/liquidhaskell
Vedi su GitHubDocument that specs can depend on arguments of enclosing functions
Open
#2442 aperta il 19 nov 2024
documentationgood first issue
Metriche repository
- Star
- (1306 star)
- Metriche merge PR
- (Merge medio 2g 18h) (12 PR mergiate in 30 g)
Descrizione
Today I learned that the meaning of specs of local bindings can depend on arguments of an enclosing function. For instance, in the following function from the test suite, arg0 is available to the spec of bar.
{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
where
{-@ bar :: x:_ -> {v:Int | v = x + arg0} @-}
bar arg1 = arg0 + arg1
It doesn't work for other things than arguments though, e.g. z is not in scope in the following spec.
{-@ foo :: x:_ -> y:_ -> {v:Int | v = x + y} @-}
foo :: Int -> Int -> Int
foo arg0 = bar
where
z = arg0
{-@ bar :: x:_ -> {v:Int | v = x + z} @-}
bar arg1 = arg0 + arg1
We should document the fact that arguments of enclosing functions are in scope. This is also true for other local bindings. See the comments below.