content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--no-totality"    @-}
  
  module Dropwhile where
  
  import Language.Haskell.Liquid.Prelude
  import Prelude hiding (head, dropWhile, (.), filter)
  
  --main :: IO ()
  foo =  
    if head (dropWhile ((/=) 3) (1:::2:::3:::Emp)) == 3
       then ()
       else liquidError "Not going to happen"
  
  -------------------------------------------------------------------------------
  -- | The `head` function returns a value that satisfies the abstract refinement
  -------------------------------------------------------------------------------
  
  {-@ head ::  forall <p :: a -> Bool>. List <p> a -> a<p> @-}
  head (x ::: _) = x
  
  -------------------------------------------------------------------------------
  -- | A List 
  -------------------------------------------------------------------------------
  
  data List a = Emp | (:::) { hd :: a
                            , tl :: List a }
  infixr 5 :::
  
  -------------------------------------------------------------------------------
  -- | A list whose head satisfies an abstract refinement `p`
  -------------------------------------------------------------------------------
  
  -- in the below, `hd :: a<p>` means the "head" is a value of type `a` that
  -- additionally, satisfies `p hd`.
  
  {-@ data List a <p :: a -> Bool> = Emp
                                   | (:::) { hd :: a<p>
                                           , tl :: List a }
    @-}
  
  -- | e.g. a list whose head equals `3`
  
  {-@ type OneList = List <{\v -> v == 3}> Int @-}
  
  {-@ one :: OneList @-}
  one :: List Int
  one = 3 ::: 2 ::: 1 ::: Emp
  
  -------------------------------------------------------------------------------
  -- | dropWhile some predicate `f` is not satisfied
  -------------------------------------------------------------------------------
  
  {-@ dropWhile :: forall <p :: a -> Bool, w :: a -> Bool -> Bool>.
                     {y::a, b::{v:Bool<w y> | not v} |- {v:a | v == y} <: a<p>}
                     (x:a -> Bool<w x>) -> List a -> List <p> a
    @-}
  dropWhile :: (a -> Bool) -> List a -> List a
  dropWhile f (x:::xs)
    | not (f x)    = x ::: xs
    | otherwise    = dropWhile f xs
  dropWhile f Emp  = Emp
  
  -- | This `witness` bound relates the predicate used in dropWhile
  
  {- bound witness @-}
  witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool
  witness p w = \ y b v -> (not b) ==> w y b ==> (v == y) ==> p v
  
  -------------------------------------------------------------------------------
  -- | Drop elements until you hit a `3`
  -------------------------------------------------------------------------------
  
  {-@ dropUntilOne' :: List Int -> OneList @-}
  dropUntilOne' :: List Int -> List Int
  dropUntilOne' = dropWhile (/= 3)
  
  -- | Currently needed for the qual; should be made redundant by `--eliminate`
  
  {-@ eqOne :: x:Int -> {v:Bool | v <=> x /= 3} @-}
  eqOne :: Int -> Bool
  eqOne x = x /= 3
  