<commit_before>\begin{code}

{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE CPP, NoImplicitPrelude, MagicHash #-}
{-# OPTIONS_HADDOCK hide #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  GHC.List
-- Copyright   :  (c) The University of Glasgow 1994-2002
-- License     :  see libraries/base/LICENSE
-- 
-- Maintainer  :  <EMAIL>
-- Stability   :  internal
-- Portability :  non-portable (GHC Extensions)
--
-- The List data type and its operations
--
-----------------------------------------------------------------------------

-- #hide
module GHC.List (
   -- [] (..),          -- Not Haskell 98; built in syntax

   map, (++), filter, concat,
   head, last, tail, init, null, length, (!!),
   foldl, scanl, scanl1, foldr, foldr1, scanr, scanr1,
   iterate, repeat, replicate, cycle,
   take, drop, splitAt, takeWhile, dropWhile, span, break,
   reverse, and, or,
   any, all, elem, notElem, lookup,
   concatMap,
   zip, zip3, zipWith, zipWith3, unzip, unzip3,
   errorEmptyList,

#ifndef USE_REPORT_PRELUDE
   -- non-standard, but hidden when creating the Prelude
   -- export list.
   takeUInt_append
#endif

 ) where

import Data.Maybe
import GHC.Base
import GHC.Num
import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)

infixl 9  !!
infix  4 `elem`, `notElem`




\end{code}

%*********************************************************
%*                                                      *
\subsection{List-manipulation functions}
%*                                                      *
%*********************************************************

\begin{code}
-- | Extract the first element of a list, which must be non-empty.
{-@ assert head         :: xs:{v: [a] | len(v) > 0} -> a @-}
head                    :: [a] -> a
head (x:_)              =  x
head []                 =  errorEmptyList "head"

badHead :: a
badHead = error "errorEmptyList head" -- errorEmptyList "head"

-- This rule is useful in cases like 
--      head [y | (x,y) <- ps, x==t]
{- RULES
"head/build"    forall (g::forall b.(a->b->b)->b->b) .
                head (build g) = g (\x _ -> x) badHead
"head/augment"  forall xs (g::forall b. (a->b->b) -> b -> b) . 
                head (augment g xs) = g (\x _ -> x) (head xs)
 -}

-- | Extract the elements after the head of a list, which must be non-empty.
{-@ assert tail         :: xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = (len(xs) - 1)}  @-}
tail                    :: [a] -> [a]
tail (_:xs)             =  xs
tail []                 =  liquidError "tail" -- errorEmptyList "tail"

-- | Extract the last element of a list, which must be finite and non-empty.
{-@ assert last         :: xs:{v: [a] | len(v) > 0} -> a @-}
last                    :: [a] -> a
#ifdef USE_REPORT_PRELUDE
last [x]                =  x
last (_:xs)             =  last xs
last []                 =  liquidError "last" -- errorEmptyList "last"
#else
-- eliminate repeated cases
last []                 =  liquidError "last" -- errorEmptyList "last"
last (x:xs)             =  last' x xs
  where last' y []     = y
        last' _ (y:ys) = last' y ys
#endif

-- | Return all the elements of a list except the last one.
-- The list must be non-empty.
{-@ assert init         :: xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) - 1}  @-}
init                    :: [a] -> [a]
#ifdef USE_REPORT_PRELUDE
init [x]                =  []
init (x:xs)             =  x : init xs
init []                 =  liquidError "init" -- errorEmptyList "init"
#else
-- eliminate repeated cases
init []                 =  liquidError "init" --errorEmptyList "init"
init (x:xs)             =  init' x xs
  where init' _ []     = []
        init' y (z:zs) = y : init' z zs
#endif

-- | Test whether a list is empty.
{-@ assert null :: xs:[a] -> {v: Bool | (Prop(v) <=> len(xs) = 0) }  @-}
null                    :: [a] -> Bool
null []                 =  True
null (_:_)              =  False

-- | /O(n)/. 'length' returns the length of a finite list as an 'Int'.
-- It is an instance of the more general 'Data.List.genericLength',
-- the result type of which may be any kind of number.<commit_msg>blasted -<commit_after>\begin{code}

{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE CPP, NoImplicitPrelude, MagicHash #-}
{-# OPTIONS_HADDOCK hide #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  GHC.List
-- Copyright   :  (c) The University of Glasgow 1994-2002
-- License     :  see libraries/base/LICENSE
-- 
-- Maintainer  :  <EMAIL>
-- Stability   :  internal
-- Portability :  non-portable (GHC Extensions)
--
-- The List data type and its operations
--
-----------------------------------------------------------------------------

-- #hide
module GHC.List (
   -- [] (..),          -- Not Haskell 98; built in syntax

   map, (++), filter, concat,
   head, last, tail, init, null, length, (!!),
   foldl, scanl, scanl1, foldr, foldr1, scanr, scanr1,
   iterate, repeat, replicate, cycle,
   take, drop, splitAt, takeWhile, dropWhile, span, break,
   reverse, and, or,
   any, all, elem, notElem, lookup,
   concatMap,
   zip, zip3, zipWith, zipWith3, unzip, unzip3,
   errorEmptyList,

#ifndef USE_REPORT_PRELUDE
   -- non-standard, but hidden when creating the Prelude
   -- export list.
   takeUInt_append
#endif

 ) where

import Data.Maybe
import GHC.Base
import GHC.Num
import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)

infixl 9  !!
infix  4 `elem`, `notElem`




\end{code}

%*********************************************************
%*                                                      *
\subsection{List-manipulation functions}
%*                                                      *
%*********************************************************

\begin{code}
-- | Extract the first element of a list, which must be non-empty.
{-@ assert head         :: xs:{v: [a] | len(v) > 0} -> a @-}
head                    :: [a] -> a
head (x:_)              =  x
head []                 =  errorEmptyList "head"

badHead :: a
badHead = error "errorEmptyList head" -- errorEmptyList "head"

-- This rule is useful in cases like 
--      head [y | (x,y) <- ps, x==t]
{- RULES
"head/build"    forall (g::forall b.(a->b->b)->b->b) .
                head (build g) = g (\x _ -> x) badHead
"head/augment"  forall xs (g::forall b. (a->b->b) -> b -> b) . 
                head (augment g xs) = g (\x _ -> x) (head xs)
 -}

-- | Extract the elements after the head of a list, which must be non-empty.
{-@ assert tail         :: xs:{v: [a] | len v > 0} -> {v: [a] | len v = len xs - 1}  @-}
tail                    :: [a] -> [a]
tail (_:xs)             =  xs
tail []                 =  liquidError "tail" -- errorEmptyList "tail"

-- | Extract the last element of a list, which must be finite and non-empty.
{-@ assert last         :: xs:{v: [a] | len v > 0} -> a @-}
last                    :: [a] -> a
#ifdef USE_REPORT_PRELUDE
last [x]                =  x
last (_:xs)             =  last xs
last []                 =  liquidError "last" -- errorEmptyList "last"
#else
-- eliminate repeated cases
last []                 =  liquidError "last" -- errorEmptyList "last"
last (x:xs)             =  last' x xs
  where last' y []     = y
        last' _ (y:ys) = last' y ys
#endif

-- | Return all the elements of a list except the last one.
-- The list must be non-empty.
{-@ assert init         :: xs:{v: [a] | len v > 0} -> {v: [a] | len v = len xs - 1}  @-}
init                    :: [a] -> [a]
#ifdef USE_REPORT_PRELUDE
init [x]                =  []
init (x:xs)             =  x : init xs
init []                 =  liquidError "init" -- errorEmptyList "init"
#else
-- eliminate repeated cases
init []                 =  liquidError "init" --errorEmptyList "init"
init (x:xs)             =  init' x xs
  where init' _ []     = []
        init' y (z:zs) = y : init' z zs
#endif

-- | Test whether a list is empty.
{-@ assert null :: xs:[a] -> {v: Bool | (Prop(v) <=> len(xs) = 0) }  @-}
null                    :: [a] -> Bool
null []                 =  True
null (_:_)              =  False

-- | /O(n)/. 'length' returns the length of a finite list as an 'Int'.
-- It is an instance of the more general 'Data.List.genericLength',
-- the result type of which may be any kind of number.
{'fraction_non_alphanumeric': 0.20893908446473627, 'fraction_numerical': 0.0060074492370539466, 'mean_word_length': 1.6921086675291073, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 55, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6677510', 'n_tokens_mistral': 2765, 'n_tokens_neox': 2624, 'n_words': 837}