Merge pull request #2594 from ucsd-progsys/fd/qualifiers

Update LF after requiring braces for qualifiers

Author: facundominguez

README.md

@@ -155,10 +155,12 @@ which will produce `tmp/*.json` files.
 
 Then a csv report can be generated from the json files with
 ```
-cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskell -o summary.csv
+cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv
 ```
 On each line, the report will contain the the wall-clock time taken by each test.
-Use `--phase LiquidHaskellCPU` to get the CPU time instead.
+Use `--phase LiquidHaskell` to get the wall-clock time instead. Although in that
+case you need to use the `--measure-timings-j1` option when running the tests,
+which validates modules one at a time.
 
 Comparison charts in `svg` format can be generated by invoking
 

docs/mkDocs/docs/specifications.md

@@ -753,7 +753,7 @@ to the Haskell source. See, [this](https://github.com/ucsd-progsys/liquidhaskell
 Finally, you can specify qualifiers directly inside source (.hs or .lhs)
 files by writing them as shown [here](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/QualTest.hs)
 
-    {-@ qualif Foo(v:Int, a: Int) : (v = a + 100)   @-}
+    {-@ qualif Foo(v:Int, a: Int) { v = a + 100 }  @-}
 
 
 **Note** In addition to these, LiquidHaskell scrapes qualifiers from all

liquid-fixpoint

@@ -30,18 +30,18 @@ assume Data.Vector.map :: (a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector
 
 assume Data.Vector.head :: forall a. {xs: Data.Vector.Vector a | vlen xs > 0} -> a
 
-qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  =  0
-qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  >  0
-qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  >= 0
-
-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v  =  vlen x)
-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v <=  vlen x)
-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v  <  vlen x)
-
-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <  vlen x)
-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <= vlen x)
-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >  vlen x)
-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >= vlen x)
-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v =  vlen x)
+qualif VecEmpty(v: Data.Vector.Vector a)    { vlen v  =  0 }
+qualif VecEmpty(v: Data.Vector.Vector a)    { vlen v  >  0 }
+qualif VecEmpty(v: Data.Vector.Vector a)    { vlen v  >= 0 }
+
+qualif Vlen(v:int, x: Data.Vector.Vector a) { v  =  vlen x }
+qualif Vlen(v:int, x: Data.Vector.Vector a) { v <=  vlen x }
+qualif Vlen(v:int, x: Data.Vector.Vector a) { v  <  vlen x }
+
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v <  vlen x }
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v <= vlen x }
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v >  vlen x }
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v >= vlen x }
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v =  vlen x }
 
 @-}

liquid-vector/src/Data/Vector_LHAssumptions.hs

@@ -152,8 +152,8 @@ testSpecP =
           "embed Set as Set_Set"
 
     , testCase "qualif" $
-       parseSingleSpec "qualif Foo(v:Int): v < 0" @?==
-          "qualif Foo(v: int): v < 0 // defined at <test>:1:8"
+       parseSingleSpec "qualif Foo(v:Int) { v < 0 }" @?==
+          "qualif Foo(v: int) { v < 0 } // defined at <test>:1:8"
 
     , testCase "lazyvar" $
        parseSingleSpec "lazyvar z" @?==
@@ -376,11 +376,10 @@ testSucceeds =
           @?==
           unlines
           [ "predicate ValidChunk V  XS  N  = "
-          , "  (not (len XS == 0) =>"
-          , "     (1 < N && 1 < len XS => len V < len XS)"
-          , "     && (len XS <= N => len V == 1)"
-          , "  )"
-          , "  && (len XS == 0 => len V == 0)"
+          , "  if len XS == 0 "
+          , "     then len V == 0"
+          , "     else (1 < N && 1 < len XS => len V < len XS)"
+          , "          && (len XS <= N => len V == 1)"
           ]
 
 

liquidhaskell-boot/tests/Parser.hs

@@ -14,6 +14,6 @@ measure fst :: (a, b) -> a
 measure snd :: (a, b) -> b
   snd (a, b) = b
 
-qualif Fst(__v:a, __y:b): (__v = (fst __y))
-qualif Snd(__v:a, __y:b): (__v = (snd __y))
+qualif Fst(__v:a, __y:b) { __v = (fst __y) }
+qualif Snd(__v:a, __y:b) { __v = (snd __y) }
 @-}

src/Data/Tuple_LHAssumptions.hs

@@ -41,24 +41,24 @@ define $             f          x = (f x)
 
 assume id        :: x:a -> {v:a | v = x}
 
-qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0))
-qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0))
+qualif IsEmp(v:Bool, xs: [a])  { v <=> (len xs > 0) }
+qualif IsEmp(v:Bool, xs: [a])  { v <=> (len xs = 0) }
 
-qualif ListZ(v: [a])          : (len v =  0)
-qualif ListZ(v: [a])          : (len v >= 0)
-qualif ListZ(v: [a])          : (len v >  0)
+qualif ListZ(v: [a])           { len v =  0 }
+qualif ListZ(v: [a])           { len v >= 0 }
+qualif ListZ(v: [a])           { len v >  0 }
 
-qualif CmpLen(v:[a], xs:[b])  : (len v  =  len xs )
-qualif CmpLen(v:[a], xs:[b])  : (len v  >= len xs )
-qualif CmpLen(v:[a], xs:[b])  : (len v  >  len xs )
-qualif CmpLen(v:[a], xs:[b])  : (len v  <= len xs )
-qualif CmpLen(v:[a], xs:[b])  : (len v  <  len xs )
+qualif CmpLen(v:[a], xs:[b])   { len v  =  len xs  }
+qualif CmpLen(v:[a], xs:[b])   { len v  >= len xs  }
+qualif CmpLen(v:[a], xs:[b])   { len v  >  len xs  }
+qualif CmpLen(v:[a], xs:[b])   { len v  <= len xs  }
+qualif CmpLen(v:[a], xs:[b])   { len v  <  len xs  }
 
-qualif EqLen(v:int, xs: [a])  : (v = len xs )
-qualif LenEq(v:[a], x: int)   : (x = len v )
+qualif EqLen(v:int, xs: [a])   { v = len xs  }
+qualif LenEq(v:[a], x: int)    { x = len v  }
 
-qualif LenDiff(v:[a], x:int)  : (len v  = x + 1)
-qualif LenDiff(v:[a], x:int)  : (len v  = x - 1)
-qualif LenAcc(v:int, xs:[a], n: int): (v = len xs  + n)
+qualif LenDiff(v:[a], x:int)   { len v  = x + 1 }
+qualif LenDiff(v:[a], x:int)   { len v  = x - 1 }
+qualif LenAcc(v:int, xs:[a], n: int) { v = len xs  + n }
 
 @-}

src/GHC/Base_LHAssumptions.hs

@@ -52,8 +52,8 @@ assume break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) +
 assume reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)}
 
 //  Copy-pasted from len.hquals
-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))
-qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))
+qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) + len([ys])) }
+qualif LenSum(v:[a], xs:[b], ys:[c]) { len([v]) = (len([xs]) - len([ys])) }
 
 assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a
 

src/GHC/List_LHAssumptions.hs

@@ -25,38 +25,38 @@ type IncrListD a D = [a]<{\x y -> (x+D) <= y}>
 
 // BOT: Do not delete EVER!
 
-qualif Bot(v:@(0))    : (0 = 1)
-qualif Bot(v:obj)     : (0 = 1)
-qualif Bot(v:a)       : (0 = 1)
-qualif Bot(v:bool)    : (0 = 1)
-qualif Bot(v:int)     : (0 = 1)
+qualif Bot(v:@(0))     { 0 = 1 }
+qualif Bot(v:obj)      { 0 = 1 }
+qualif Bot(v:a)        { 0 = 1 }
+qualif Bot(v:bool)     { 0 = 1 }
+qualif Bot(v:int)      { 0 = 1 }
 
-qualif CmpZ(v:a)      : (v <  0)
-qualif CmpZ(v:a)      : (v <= 0)
-qualif CmpZ(v:a)      : (v >  0)
-qualif CmpZ(v:a)      : (v >= 0)
-qualif CmpZ(v:a)      : (v  = 0)
-qualif CmpZ(v:a)      : (v != 0)
+qualif CmpZ(v:a)       { v <  0 }
+qualif CmpZ(v:a)       { v <= 0 }
+qualif CmpZ(v:a)       { v >  0 }
+qualif CmpZ(v:a)       { v >= 0 }
+qualif CmpZ(v:a)       { v  = 0 }
+qualif CmpZ(v:a)       { v != 0 }
 
-qualif Cmp(v:a, x:a)  : (v <  x)
-qualif Cmp(v:a, x:a)  : (v <= x)
-qualif Cmp(v:a, x:a)  : (v >  x)
-qualif Cmp(v:a, x:a)  : (v >= x)
-qualif Cmp(v:a, x:a)  : (v  = x)
-qualif Cmp(v:a, x:a)  : (v != x)
+qualif Cmp(v:a, x:a)   { v <  x }
+qualif Cmp(v:a, x:a)   { v <= x }
+qualif Cmp(v:a, x:a)   { v >  x }
+qualif Cmp(v:a, x:a)   { v >= x }
+qualif Cmp(v:a, x:a)   { v  = x }
+qualif Cmp(v:a, x:a)   { v != x }
 
-qualif One(v:int)     : v = 1
-qualif True1(v:Bool)   : (v)
-qualif False1(v:Bool)  : (~ v)
+qualif One(v:int)      { v = 1 }
+qualif True1(v:Bool)    { v }
+qualif False1(v:Bool)   { ~ v }
 
 //  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
-qualif Papp(v:a, p:Pred a) : (papp1 p v)
+qualif Papp(v:a, p:Pred a)  { papp1 p v }
 
 //  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
-qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x)
+qualif Papp2(v:a, x:b, p:Pred a b)  { papp2 p v x }
 
 //  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
-qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y)
+qualif Papp3(v:a, x:b, y:c, p:Pred a b c)  { papp3 p v x y }
 
 //  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
 //  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])

src/Prelude_LHAssumptions.hs

@@ -61,5 +61,5 @@ loop lo hi base f = go lo base
 {-@ initUpto :: n:Nat -> (IdVec n) @-}
 initUpto n   = loop 0 n empty (\i acc -> set i i acc)
 
-{-@ qualif Foo(v:Int): v < 0 @-}
+{-@ qualif Foo(v:Int) { v < 0  } @-}