Adding more examples to the warn on term holes tests

Author: matheussbernardo

tests/tests.cabal

@@ -2628,7 +2628,9 @@ executable typed-holes
     main-is:          Main.hs
 
     ghc-options:      -fplugin=LiquidHaskell
-    other-modules:    Example1
+    other-modules:    Example0
+                    , Example1
+                    , Example2
     build-depends:    base
                     , liquid-prelude
                     , liquidhaskell

tests/typed-holes/Example0.hs

@@ -0,0 +1,10 @@
+{-@ LIQUID "--expect-error-containing=Hole Found" @-}
+{-@ LIQUID "--warn-on-term-holes" @-}
+
+module Example0 where
+    hole = undefined
+
+    {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
+    listLength :: [a] -> Int
+    listLength [] = hole
+    listLength (_:xs) = 1 + listLength xs

tests/typed-holes/Example1.hs

@@ -1,28 +1,17 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
--- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/
 
 module Example1 where
-    import Prelude hiding ((<>))
-    import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof)
-    
-    hole = undefined
+    import Language.Haskell.Liquid.ProofCombinators (Proof)
 
-    {-@ reflect empty @-}
-    empty  :: [a]
-    empty  = []
+    hole = undefined
 
-    {-@ infix <> @-}
-    {-@ reflect <> @-}
-    (<>) :: [a] -> [a] -> [a]
-    [] <> xs = xs
-    (x:xs) <> ys = x : (xs <> ys)
+    {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
+    listLength :: [a] -> Int
+    listLength [] = 0
+    listLength (_:xs) = 1 + listLength xs
+    {-@ measure listLength @-}
 
-    {-@ leftId  :: x:[a] -> { (empty <> x) == x } @-}
-    leftId :: [a] -> Proof
-    leftId x
-        =   empty <> x
-        === hole
-        === x
-        *** QED
+    {-@ listLengthProof :: xs:[a] -> {listLength xs == len xs} @-}
+    listLengthProof :: [a] -> Proof
+    listLengthProof = hole

tests/typed-holes/Example2.hs

@@ -0,0 +1,28 @@
+{-@ LIQUID "--expect-error-containing=Hole Found" @-}
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--warn-on-term-holes" @-}
+-- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/
+
+module Example2 where
+    import Prelude hiding ((<>))
+    import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof)
+    
+    hole = undefined
+
+    {-@ reflect empty @-}
+    empty  :: [a]
+    empty  = []
+
+    {-@ infix <> @-}
+    {-@ reflect <> @-}
+    (<>) :: [a] -> [a] -> [a]
+    [] <> xs = xs
+    (x:xs) <> ys = x : (xs <> ys)
+
+    {-@ leftId  :: x:[a] -> { (empty <> x) == x } @-}
+    leftId :: [a] -> Proof
+    leftId x
+        =   empty <> x
+        === hole
+        === x
+        *** QED