a-conjecture-of-mine

An exercise on polyglossy: the same problem solved on multiple languages

commit c64b0a508beb5e2010927c141593415840358da8
parent 73b681f35dfccb4ed1a15453731e0fc5a4649a1e
Author: Pablo Escobar Gaviria <gark.garcia@protonmail.com>
Date:   Mon,  9 Dec 2019 09:36:39 -0200

Cleaned the Haskell implementation.

Diffstat:
MHaskell/app/Main.hs | 74++++++++++++++++++++++++++++++++++++++------------------------------------
1 file changed, 38 insertions(+), 36 deletions(-)
diff --git a/Haskell/app/Main.hs b/Haskell/app/Main.hs
@@ -16,14 +16,14 @@ import qualified Data.Map
 main :: IO Int
 main = do
     args <- getArgs
-
-    if length args > 0
-        then case readDec (args !! 0) :: [(Natural, String)] of
-            [(max, "")] ->
-                if counter' max then exitFailure else exitSuccess
-            _ -> exitInvalidInput
-            
-        else exitInvalidInput
+        
+    case head' args >>= Just . readDec of
+        Just [(max, "")] ->
+            if counter' max then exitFailure else exitSuccess
+        _ -> exitInvalidInput
+    
+    where head' [] = Nothing
+          head' xs = Just (head xs)
 
 -- Calculates the sum of the digits of `n`.
 sum' :: Natural -> Int
@@ -31,44 +31,46 @@ sum' n
     | n < 10 = fromEnum n
     | otherwise = fromEnum (n `mod` 10) + sum' (n `div` 10)
 
-test' :: Natural -> Natural -> Map Natural Int -> Maybe (Map Natural Int)
-test' a b sums =
-    case lookup a of
-        Just sa ->
-            case lookup b of
-                Just sb ->
-                    case lookup $ a + b of
-                        Just sab ->
-                            if (sab - sa - sb) `mod` 9 == 0
-                                then Just sums
-                                else Nothing
-                        Nothing  -> retry $ a + b
-                Nothing -> retry b
-        Nothing -> retry a
+-- Returns `Just updated` if the if the conjecture holds for pair, where
+-- `updated` is an updated versions of the sums cache provided by `sums`.
+-- Otherwise returns `Nothing`.
+test' :: Map Natural Int -> (Natural, Natural) -> Maybe (Map Natural Int)
+test' sums pair =
+    case diff sums pair of
+        Left updated ->
+            test' updated pair
+
+        Right dif ->
+            if dif `mod` 9 == 0 then Just sums else Nothing
+
+-- Given a cache of the image of `sum'`, attemps to lookup `sum' a`, `sum' b`
+-- and `sum' $ a + b`.
+-- If the lookup succeeds, returns `Right (sum' (a + b) - sum' a - sum' a)`.
+-- Otherwise inserts the value that caused the failure to `sums` and returns
+-- `Left sums`.
+diff :: Map Natural Int -> (Natural, Natural) -> Either (Map Natural Int) Int
+diff sums (a, b) = do
+    sa  <- lookupOrInsert a
+    sb  <- lookupOrInsert b
+    sab <- lookupOrInsert $ a + b
 
-    where retry x = test' a b $ insert x (sum' x) sums
-          lookup x = Data.Map.lookup x sums
+    pure $ sab - sa - sb
+    where lookupOrInsert x =
+            case Data.Map.lookup x sums of
+                Just sx -> Right sx
+                
+                Nothing -> Left (insert x (sum' x) sums)
 
 -- Checks if there is any counterexample in
--- [(a, b) | a <- [0..max], b <- [0..max]].
+-- [(a, b) | a <- [0..max], b <- [a..max]].
 --
 -- Returns `True` if a counter example was found.
 -- Otherwise returns `False`.
 counter' :: Natural -> Bool
 counter' max =
-    case foldM f empty [0..max] of
+    case foldM test' empty [(a, b) | a <- [0..max], b <- [a..max]] of
         Nothing -> True
         Just _  -> False
-    where f accSums a = iter' a max accSums
-
--- Checks if there is any counter example in [(a, b)| b <- [a..max]].
--- Returns `Nothing` if a counter example was found.
---
--- Otherwise returns `Just accSums`, where `accSums` maps every
--- computed value to the sum of it's digits.
-iter' :: Natural -> Natural -> Map Natural Int -> Maybe (Map Natural Int)
-iter' a max sums = foldM f sums [a..max]
-    where f accSums b = test' a b accSums
 
 exitInvalidInput :: IO Int
 exitInvalidInput = exitWith $ ExitFailure 2 
\ No newline at end of file