liquidhaskell-0.9.0.2.1: tests/errors/ElabLocation3.hs
module ElabLocation3 where
{-@ LIQUID "--expect-error-containing=ElabLocation3.hs:174:1-5" @-}
{-@ LIQUID "--reflection" @-}
import Language.Haskell.Liquid.ProofCombinators
import Prelude hiding (id)
{-@ type Pos = {v:Int | 0 < v} @-}
{-@ incr :: Pos -> Pos @-}
incr :: Int -> Int
incr x = x + 2
{-@
data Monkey =
M { number :: Nat,
items :: [Int],
operation :: Int -> Int,
testMod :: {n:Int | n > 0 },
ifTrue :: Nat,
ifFalse :: Nat,
count :: Nat
}
@-}
data Monkey =
M { number :: Int,
items :: [Int],
operation :: Int -> Int,
testMod :: Int,
ifTrue :: Int,
ifFalse :: Int,
count :: Int }
{-@ myCount :: _ -> Nat @-}
myCount :: Monkey -> Int
myCount M { count = k} = k
showMonkey :: Monkey -> String
showMonkey (M n i o m ifT ifF count) =
"#" ++ (show n) ++ " items " ++ (show i) ++ " examined " ++ (show count) ++ "\n"
instance Show Monkey where show = showMonkey
{-@ type MonkeyIR X = {m:Monkey | number m < X && ifTrue m < X && ifFalse m < X } @-}
-- fst = item
-- snd = destination
{-@ type MonkeyItem X = (Int, {n:Nat | n < X}) @-}
{-@ turn :: x:Int -> {worry:Int | worry /= 0 } -> {modulus:Int | modulus /= 0} -> m:MonkeyIR x -> {d:[MonkeyItem x] | len d = len (items m)} @-}
turn :: Int -> Int -> Int -> Monkey -> [(Int, Int)]
turn _ worry modulus (M _ oldItems op m dTrue dFalse _) =
map toDestination oldItems where
toDestination i = let newWorry = (( op i ) `div` worry) `mod` modulus in
(newWorry, if newWorry `mod` m == 0 then dTrue else dFalse)
-- What I would like to do:
-- measure countOfItems :: [Monkey] -> Int
-- countOfItems [] = 0
-- countOfItems (m:ms) = len (items m) + countOfItems ms
--
-- -> {m2:[MonkeyIR x] | len m2 = len m && countOfItems m2 = countOfItems m + len mi}
--
-- But this measure gets applied to all lists, which doesn't work
{-@ data MonkeyList = Empty | MCons { headMonkey :: MonkeyIR 8, barrel :: MonkeyList } @-}
data MonkeyList =
Empty |
MCons Monkey MonkeyList
{-@ measure mLen :: MonkeyList -> Int
mLen Empty = 0
mLen (MCons m ms) = 1 + mLen ms
@-}
{-@ measure countOfItems :: MonkeyList -> Int
countOfItems Empty = 0
countOfItems (MCons m ms) = len (items m) + countOfItems ms @-}
{-
{-@ distribute2 :: m:MonkeyList -> {mi:[MonkeyItem 8] | len mi <= mLen m}
-> {m2:MonkeyList | mLen m2 = mLen m && countOfItems m2 = countOfItems m + len mi} @-}
distribute2 :: MonkeyList -> [(Int,Int)] -> MonkeyList
distribute2 Empty [] = Empty
distribute2 Empty _ = error "Shouldn't happen"
distribute2 (MCons m ms) destinations =
MCons (m {items = (items m) ++ newItems}) (distribute2 ms (filter (notP toMe) destinations)) where
newItems = map fst (filter toMe destinations)
toMe (_,d) = d == number m
-}
{-@ distribute :: x:Int -> m:[MonkeyIR x] -> mi:[MonkeyItem x]
-> {m2:[MonkeyIR x] | len m2 = len m} @-}
distribute :: Int -> [Monkey] -> [(Int,Int)] -> [Monkey]
distribute _ [] _ = []
distribute x (m:ms) destinations =
(m {items = (items m) ++ newItems}):(distribute x ms destinations) where
newItems = map fst (filter toMe destinations)
toMe (_,d) = d == number m
-- Monkey N's turn in the round
{-@ roundN :: x:Int ->
{worry:Int | worry /= 0 } ->
{modulus:Int | modulus /= 0} ->
{before:[MonkeyIR x] | len before = x} ->
{n:Nat | n < x } ->
{after:[m:MonkeyIR x] | len after = x} @-}
roundN :: Int -> Int -> Int -> [Monkey] -> Int -> [Monkey]
roundN x worry modulus monkeys n =
let m = (monkeys !! n)
destinations = turn x worry modulus m
newCount = (myCount m) + length (items m)
afterRemoval = (take n monkeys) ++ [(m {items = [], count = newCount} )] ++ (drop (n+1) monkeys) in
distribute x afterRemoval destinations
-- One round of all monkeys
-- Complicated by the need to prove termination.
{-@ round :: x:Int -> {worry:Int | worry /= 0} -> {modulus:Int | modulus /= 0 } ->
{before:[MonkeyIR x] | len before = x} ->
{after:[MonkeyIR x] | len after = x} @-}
round :: Int -> Int -> Int -> [Monkey] -> [Monkey]
round x worry modulus monkeys = go 0 monkeys where
{-@ go :: {n:Int | n >= 0 && n <= x} -> {m:[MonkeyIR x] | len m = x} -> {m2:[MonkeyIR x] | len m2 = x} / [ x - n ] @-}
go n ms = if n == x then ms
else go (n+1) (roundN x worry modulus ms n)
{-@ m0 :: MonkeyIR 4 @-}
m0 = M { number=0, items=[79,98], operation=(\o -> o * 19), testMod=23, ifTrue=2, ifFalse=3, count=0 }
{-@ m1 :: MonkeyIR 4 @-}
m1 = M { number=1, items=[54,65,75,74], operation=(\o -> o + 6), testMod=19, ifTrue=2, ifFalse=0, count=0 }
{-@ m2 :: MonkeyIR 4 @-}
m2 = M { number=2, items=[79,60,97], operation=(\o -> o * o), testMod=13, ifTrue=1, ifFalse=3, count=0 }
{-@ m3 :: MonkeyIR 4 @-}
m3 = M { number=3, items=[74], operation=(\o -> o + 3), testMod=17, ifTrue=0, ifFalse=1, count=0 }
{-@ example :: {m:[MonkeyIR 4] | len m = 4} @-}
example :: [Monkey]
example = [ m0, m1, m2, m3 ]
{-@ i0 :: MonkeyIR 8 @-}
i0 = M { number=0, items=[59,74,65,86], operation=(\o -> o * 19), testMod=7, ifTrue=6, ifFalse=2, count=0 }
{-@ i1 :: MonkeyIR 8 @-}
i1 = M { number=1, items=[62,84,72,91,68,78,51], operation=(\o -> o + 1), testMod=2, ifTrue=2, ifFalse=0, count=0 }
{-@ i2 :: MonkeyIR 8 @-}
i2 = M { number=2, items=[78,84,96], operation=(\o -> o + 8), testMod=19, ifTrue=6, ifFalse=5, count=0 }
{-@ i3 :: MonkeyIR 8 @-}
i3 = M { number=3, items=[97,86], operation=(\o -> o * o), testMod=3, ifTrue=1, ifFalse=0, count=0 }
{-@ i4 :: MonkeyIR 8 @-}
i4 = M { number=4, items=[50], operation=(\o -> o + 6), testMod=13, ifTrue=3, ifFalse=1, count=0 }
{-@ i5 :: MonkeyIR 8 @-}
i5 = M { number=5, items=[73,65,69,65,51], operation=(\o -> o * 17), testMod=11, ifTrue=4, ifFalse=7, count=0 }
{-@ i6 :: MonkeyIR 8 @-}
i6 = M { number=6, items=[69, 82, 97, 93, 82, 84, 58, 63], operation=(\o -> o + 5), testMod=5, ifTrue=5, ifFalse=7, count=0 }
{-@ i7 :: MonkeyIR 8 @-}
i7 = M { number=7, items=[81, 78, 82, 76, 79, 80], operation=(\o -> o + 3), testMod=17, ifTrue=3, ifFalse=4, count=0 }
{-@ input :: {m:[MonkeyIR 8] | len m = 8} @-}
input :: [Monkey]
input = [ i0, i1, i2, i3, i4, i5, i6, i7 ]
{-@ assume iterate :: (a -> a) -> a -> {l:[a] | len l >= 1000000 } @-}
computeModulus :: [Monkey] -> Int
computeModulus ms = foldl1 (*) (map testMod ms)
id z = z
part1 :: () -> IO ()
part1 _ = do
putStrLn "Part 1"
let m1 = computeModulus example in do
putStrLn $ "Working mod " ++ show m1
let allRounds = iterate {- (Main.round 4 3 m1) -} id example in
print $ allRounds !! 20
let m2 = computeModulus input in do
putStrLn $ "Working mod " ++ show m2
let allRounds2 = iterate {- (Main.round 8 3 m2) -} id input in
print $ allRounds2 !! 20
part2 :: () -> IO ()
part2 _ = do
putStrLn "Part 2"
let m1 = computeModulus example in do
putStrLn $ "Working mod " ++ show m1
let allRounds = iterate {- (Main.round 4 1 m1) -} id example in do
print $ allRounds !! 1000
print $ allRounds !! 2000
print $ allRounds !! 3000
print $ allRounds !! 4000
print $ allRounds !! 5000
print $ allRounds !! 6000
print $ allRounds !! 7000
print $ allRounds !! 8000
print $ allRounds !! 9000
print $ allRounds !! 10000
let m2 = computeModulus input in do
putStrLn $ "Working mod " ++ show m2
let allRounds2 = iterate {- (Main.round 8 1 m2) -} id input in
print $ allRounds2 !! 10000
mymain :: IO ()
mymain = part1 () >> part2 ()