a-conjecture-of-mine

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

commit 115bb94a3c0fa8c8c4248b5411aec09b4490282b
parent b8ef273476589a2815ef622f9c5d6810c0efde9e
Author: Gark Garcia <37553739+GarkGarcia@users.noreply.github.com>
Date:   Sat,  4 May 2019 11:04:43 -0300

Optimized the counter' function.

The function now only looks for a single counterexample, instead of looking for all of them and returning the first one.

Diffstat:
MHaskell/app/Main.hs | 48+++++++++++++++++++++++++++---------------------
1 file changed, 27 insertions(+), 21 deletions(-)
diff --git a/Haskell/app/Main.hs b/Haskell/app/Main.hs
@@ -8,6 +8,7 @@ module Main where
 import Numeric
 import Numeric.Natural
 import System.Clock
+import Control.Monad(foldM)
 
 main :: IO ()
 main = do
@@ -21,17 +22,10 @@ main = do
         [(max, "")] -> do
             putStrLn "\nLOADING. . ."
             start <- getTime Monotonic
-            
-            case counter' 0 max of
-                Nothing -> do
-                    end <- getTime Monotonic
-                    putStrLn $ "LOADED. . . in " ++ formatMils (end - start) ++ "ms [1 Thread]"
-                    putStrLn $ "\nThe conjecture is proved for all natural numbers smaller or equals to " ++ show max ++ "!"
-                Just counter -> do
-                    end <- getTime Monotonic
-                    putStrLn $ "LOADED. . . in " ++ formatMils (end - start) ++ "ms [1 Thread]"
-                    putStrLn $ "\nThe conjecture is disproved! Here's a counterexample: (" ++ (show $ fst $ counter) 
-                        ++ ", " ++ (show $ snd $ counter) ++ ")"
+            case counter' max of
+                Nothing -> putEnd start ("\nThe conjecture is proved for all natural numbers smaller or equals to " ++ show max ++ "!")
+                Just c  -> putEnd start ("\nThe conjecture is disproved! Here's a counterexample: (" ++ (show $ fst $ c) ++ ", "
+                    ++ (show $ snd $ c) ++ ")")
                 
         _ -> putStrLn $ "\n'" ++ maxStr ++ "' is not a natural number!"
 
@@ -41,12 +35,24 @@ sum' x = case x of
     x -> (x `mod` 10) + sum' (x `div` 10)
 
 test' :: Natural -> Natural -> Bool
-test' a b = ((fromEnum $ sum' (a + b)) - (fromEnum $ sum' a) - (fromEnum $ sum' b)) `mod` 9 == 0
-
-counter' :: Natural -> Natural -> Maybe (Natural, Natural)
-counter' min max = case [(a, b) | a <- [min..max], b <- [a..max], not $ test' a b] of
-    [] -> Nothing
-    fst : _ -> Just fst
-
-formatMils :: TimeSpec -> [Char]
-formatMils t = show (sec t * 10^3 + nsec t `div` 10^6)-
\ No newline at end of file
+test' a b = let s(x) = fromEnum $ sum' x in (s(a + b) - s(a) - s(b)) `mod` 9 == 0
+
+counter' :: Natural -> Maybe (Natural, Natural)
+counter' max = case foldM f max [0..max] of
+    Left (a, b) -> Just (a, b)
+    Right _     -> Nothing
+    where f a b = iter' b max
+
+iter' :: Natural -> Natural -> Either (Natural, Natural) Natural
+iter' a max = case foldM f a [a..max] of
+    Left b  -> Left (a, b)
+    Right _ -> Right (a - 1)
+    where f i b
+            | test' a b = Right (i + 1)
+            | otherwise = Left b
+
+putEnd :: TimeSpec -> String -> IO ()
+putEnd start msg = do
+    end <- getTime Monotonic
+    let t = end - start in putStrLn $ "LOADED. . . in " ++ show (sec t * 10^3 + nsec t `div` 10^6) ++ "ms [1 Thread]"
+    putStrLn $ msg+
\ No newline at end of file