<commit_before>module Ex where

-- Testing "existential-types"

{-@ foldN :: forall a <p :: x0:Int -> x1:a -> Bool>. 
                (i:Int -> a<p i> -> exists [j : {v: Int | v = i + 1}]. a<p j>) 
              -> n:{v: Int | v >= 0}
              -> (exists [z : {v: Int | v = 0}]. a <p z>) 
              -> a <p n>
  @-}

foldN :: (Int -> a -> a) -> Int -> a -> a
foldN f n = go 0 
  where go i x | i < n     = go (i+1) (f i x)
               | otherwise = x


fooBar :: (Int -> a -> a) -> Int -> a -> a
fooBar f n = go 0
  where go i x | i < n     = go (i+1) (f i x)
               | otherwise = x


{-@ count :: m: {v: Int | v > 0 } -> {v: Int | v = m} @-}
count :: Int -> Int
count m = foldN (\_ n -> n + 1) m 0

goo x y = x

moo = goo "st" True<commit_msg>passed all tests. next ex+lists<commit_after>module Ex where

-- Testing "existential-types"

{-@ foldN :: forall a <p :: x0:Int -> x1:a -> Bool>. 
                (i:Int -> a<p i> -> exists [j : {v: Int | v = i + 1}]. a<p j>) 
              -> n:{v: Int | v >= 0}
              -> (exists [z : {v: Int | v = 0}]. a <p z>) 
              -> a <p n>
  @-}

foldN :: (Int -> a -> a) -> Int -> a -> a
foldN f n = go 0 
  where go i x | i < n     = go (i+1) (f i x)
               | otherwise = x


fooBar :: (Int -> a -> a) -> Int -> a -> a
fooBar f n = go 0
  where go i x | i < n     = go (i+1) (f i x)
               | otherwise = x


{-@ count :: m: {v: Int | v > 0 } -> {v: Int | v = m} @-}
count :: Int -> Int
count m = foldN (\_ n -> n + 1) m 0

{'fraction_non_alphanumeric': 0.21282220753469927, 'fraction_numerical': 0.015862524785194978, 'mean_word_length': 1.3400309119010818, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7449142', 'n_tokens_mistral': 645, 'n_tokens_neox': 609, 'n_words': 233}