{-@ LIQUID "--higherorder" @-} {-@ LIQUID "--totality" @-} {-@ LIQUID "--exactdc" @-} {-@ LIQUID "--no-measure-fields" @-} {-@ LIQUID "--eliminate=all" @-} module DivideAndQunquer where import Prelude hiding (error, map, take, drop) import Language.Haskell.Liquid.ProofCombinators {-@ reflect mapReduce @-} mapReduce :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> b mapReduce n f op N = f N mapReduce n f op is = reduce op (map f (chunk n is)) chunk :: Int -> List a -> List (List a) map :: (a -> b) -> List a -> List b reduce :: (b -> b -> b) -> List b -> b {-@ mapReduceTheorem :: n:Int -> f:(List a -> b) -> op:(b -> b -> b) -> is:List a -> distributionThm:(is1:List a -> is2:List a -> {op (f is1) (f is2) == f (append is1 is2)} ) -> { f is == mapReduce n f op is } / [llen is] @-} mapReduceTheorem :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> (List a -> List a -> Proof) -> Proof mapReduceTheorem n f op N _ = mapReduce n f op N ==. f N *** QED mapReduceTheorem n f op is _ | llen is <= n || n <= 1 = mapReduce n f op is ==. reduce op (map f (chunk n is)) ==. reduce op (map f (C is N)) ==. reduce op (f is `C` map f N) ==. reduce op (f is `C` N) ==. f is *** QED mapReduceTheorem n f op is distributionThm = undefined {- = mapReduce n f op is ==. reduce op (map f (chunk n is)) ==. reduce op (map f (C (take n is) (chunk n (drop n is)))) ==. reduce op (f (take n is) `C` map f (chunk n (drop n is))) ==. op (f (take n is)) (reduce op (map f (chunk n (drop n is)))) ==. op (f (take n is)) (mapReduce n f op (drop n is)) ==. op (f (take n is)) (f (drop n is)) ? mapReduceTheorem n f op (drop n is) distributionThm ==. f (append (take n is) (drop n is)) ? distributionThm (take n is) (drop n is) ==. f is ? appendTakeDrop n is *** QED -} ------------------------------------------------------------------------------- ----------- List Definition -------------------------------------------------- ------------------------------------------------------------------------------- {-@ data List [llen] a = N | C {lhead :: a, ltail :: List a} @-} data List a = N | C a (List a) llen :: List a -> Int {-@ measure llen @-} {-@ llen :: List a -> Nat @-} llen N = 0 llen (C _ xs) = 1 + llen xs ------------------------------------------------------------------------------- ----------- List Manipulation ------------------------------------------------ ------------------------------------------------------------------------------- {-@ reflect map @-} {-@ map :: (a -> b) -> xs:List a -> {v:List b | llen v == llen xs } @-} map _ N = N map f (C x xs) = f x `C` map f xs {-@ reflect append @-} append :: List a -> List a -> List a append N ys = ys append (C x xs) ys = x `C` (append xs ys) {-@ reflect reduce @-} {-@ reduce :: (b -> b -> b) -> is:{List b | 1 <= llen is } -> b @-} reduce _ (C x N) = x reduce op (C x xs) = op x (reduce op xs) {-@ reflect chunk @-} {-@ chunk :: i:Int -> xs:List a -> {v:List (List a) | (1 <= llen v) && (if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs)) } / [llen xs] @-} chunk i xs | i <= 1 = C xs N | llen xs <= i = C xs N | otherwise = C (take i xs) (chunk i (drop i xs)) {-@ reflect drop @-} {-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-} drop :: Int -> List a -> List a drop i N = N drop i (C x xs) | i == 0 = C x xs | otherwise = drop (i-1) xs {-@ reflect take @-} {-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-} take :: Int -> List a -> List a take i N = N take i (C x xs) | i == 0 = N | otherwise = C x (take (i-1) xs) -- | Helper Theorem {-@ appendTakeDrop :: i:Nat -> xs:{List a | i <= llen xs} -> {xs == append (take i xs) (drop i xs) } @-} appendTakeDrop :: Int -> List a -> Proof appendTakeDrop i N = append (take i N) (drop i N) ==. append N N ==. N *** QED appendTakeDrop i (C x xs) | i == 0 = append (take 0 (C x xs)) (drop 0 (C x xs)) ==. append N (C x xs) ==. C x xs *** QED | otherwise = append (take i (C x xs)) (drop i (C x xs)) ==. append (C x (take (i-1) xs)) (drop (i-1) xs) ==. C x (append (take (i-1) xs) (drop (i-1) xs)) ==. C x xs ? appendTakeDrop (i-1) xs *** QED