a-conjecture-of-mine

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

git clone: git://git.pablopie.xyz/a-conjecture-of-mine
Log
Files
Refs

Commit: a9b8ef4734d14a7ba588af776b452d8345ac40df
Parent: c2110a4459ab17c05a203c66502c0d817d17c492
Author: Pablo Emilio Escobar Gaviria <pablo-escobar@riseup.net>
Date: Mon, 20 Jul 2020 11:37:47 -0300

Refactored the build scripts into Make targets

Diffstat

9 files changed, 274 insertions, 43 deletions

Status	File Name	N° Changes	Insertions	Deletions
Deleted	C++/.gitignore	2	0	2
Added	Extra/x86/PROGRAM.S	199	199	0
Modified	Idris/Main.idr	75	45	30
Deleted	Java/.gitignore	4	0	4
Deleted	Kotlin/.gitignore	3	0	3
Deleted	Kotlin/bin.jar	0	0	0
Added	Makefile	30	30	0
Deleted	Rust/.gitignore	2	0	2
Deleted	Wasm/.gitignore	2	0	2

diff --git a/C++/.gitignore b/C++/.gitignore
@@ -1 +0,0 @@
-.vscode-
\ No newline at end of file

diff --git a/Extra/x86/PROGRAM.S b/Extra/x86/PROGRAM.S
@@ -0,0 +1,199 @@
+.model tiny
+
+.stack 1000h
+
+.data
+        sums_cache dw 25000 DUP(0)
+
+.code
+        org 100h
+
+start:
+        mov  ax, @data
+        mov  ds, ax
+
+        call read_uint ; Retrieve user input  
+        call cache_sums
+        call counterexpl
+
+cache_sums:
+        push ax                 ; Preserve the value of max
+
+        mov  si, offset sums_cache
+
+        mov  cx, 2
+        mul  cx                 ; ax = max * 2
+cache_sums.loop:
+        call sum_digits
+        mov  [si], bx
+
+        add  si, 2
+        dec  ax
+
+        cmp  ax, 0
+        ja   cache_sums.loop    ; while ax > 0, keep looping
+
+        pop  ax                 ; Restore the value of max to ax 
+        ret
+
+; Iterate `a` from 0 to `max`
+; At the start of this routine ax holds the value of max
+counterexpl:
+        mov  cx, 9              ; Set the devident to 9
+counterexpl.loop:
+        call iter
+
+        dec  ax                 ; a -= 1
+        cmp  ax, 0              ; if a > 0, keep looping
+        ja   counterexpl.loop
+
+        call ok
+        ret
+
+; Iterate `b` from `a` to 0
+; At the start of this routine ax holds the value of a
+iter:
+        mov  bx, ax
+iter.loop:
+        call test_pair
+
+        dec  bx
+        cmp  bx, 0
+        jae  iter.loop
+        ret
+
+; At the start of this routine ax holds the value of a
+; and bx holds the value of b
+test_pair:
+        ; Preserve bp and sp
+        push bp
+        mov  bp, sp
+
+        sub  sp, 6              ; Make room for 3 words [S(a +  b), S(a) and S(b)]
+        push ax                 ; Preserve the value of a
+
+        ; S(a + b) = sums_cache[a + b]
+        mov  si, offset sums_cache
+        add  si, ax
+        add  si, ax
+        add  si, bx
+        add  si, bx
+        mov  ax, [si]
+        mov  [bp - 6], ax
+
+        ; S(a) = sums_cache[a]
+        sub  si, bx
+        sub  si, bx
+        mov  ax, [si]
+        mov  [bp - 4], ax
+
+        ; S(b) = sums_cache[b]
+        mov  si, offset sums_cache
+        add  si, bx
+        add  si, bx
+        mov  ax, [si]
+        mov  [bp - 2], ax
+
+        ; Store S(a + b) - S(a) - S(b) in ax
+        mov  ax, [bp - 6]
+        sub  ax, [bp - 4]
+        sub  ax, [bp - 2]
+
+        mov  dx, 0              ; Clear the register where the rest will be stored
+        div  cx
+        pop  ax                 ; Restore the value of a to ax
+
+        cmp  dx, 0              ; if (S(a + b) - S(a) - S(b)) % 9 != 0, goto fail
+        jne  fail
+
+        ; Restore bp and sp
+        mov  sp, bp
+        pop  bp
+        ret
+
+sum_digits:
+        push ax
+
+        mov  cx, 10 ; Store the devident in cx
+        mov  bx, 0 ; Clear the register where the result will be stored
+sum_digits.loop:
+        mov  dx, 0 ; Clear the rest of the division
+
+        div  cx ; Divide ax by cx
+        add  bx, dx ; Add the rest of the division ax/cx to bx
+
+        ; Loop until ax equals 0
+        cmp  ax, 0
+        ja   sum_digits.loop
+
+        pop  ax
+        ret
+
+; Reads the first element of the command-line tail and
+; tries to convert it to an unsigned word
+read_uint:
+        mov  ax, 0
+        mov  cx, 10
+        push si
+
+        ; Move the start of the command-line tail to `si`
+        ;mov  si, ds
+        mov  si, 5eh
+
+read_uint.loop:
+        ; Read a character from the command-line tail
+        mov  bh, 0
+        mov  bl, [si]
+
+        ; Jump out of the loop at the end of the first arg
+        cmp  bl, ' '
+        jmp  read_uint.end
+        cmp  bl, 0dh
+        jmp  read_uint.end
+
+        ; Check if it's a numeric character
+        cmp  bl, 30h
+        jb   short invalid_input
+        cmp  bl, 39h
+        ja   short invalid_input
+
+        ; Convert the character code into a decimal digit
+        sub  bx, 30h
+
+        ; ax = ax * 10 + bx
+        mul  cx
+        add  ax, bx
+
+        ; Increment the pointer to the argument string and keep looping
+        inc  si
+        jmp  read_uint.loop
+
+read_uint.end:
+        pop  si
+        ret
+
+;; Exit with exit-code 0
+ok:
+        mov  al, 0
+        call quit
+        ret
+
+;; Exit with exit-code 1
+fail:
+        mov  al, 1
+        call quit
+        ret
+
+;; Exit with exit-code 2
+invalid_input:
+        mov  al, 2
+
+        call quit
+        ret
+
+;; Exit with exit-code `al`  
+quit:
+        mov  ah, 4ch
+        int  21h
+        ret
+

diff --git a/Idris/Main.idr b/Idris/Main.idr
@@ -3,37 +3,52 @@
 -- Let S: N -> N be the sum of the digits of a positive integer.
 -- For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.
 
-module Main
-
-data Every : (Nat -> Type) -> Nat -> Type  where
-    Base :  {P : Nat -> Type} -> Every P Z
-    Succ :  (n : Nat)
-         -> {P : Nat -> Type} 
-         -> Every P n 
-         -> P (S n) 
-         -> Every P (S n)
+module Main where
+
+import Numeric (readDec)
+import Numeric.Natural
+import System.Environment
+import System.Exit
+import Control.Monad (foldM)
+import Data.Vector (Vector, unsafeIndex, generate)
+
+main : IO Int
+main = do
+    args <- getArgs
+        
+    case readDec <$> head' args of
+        Just [(max, "")] =>
+            if counterexempl max then exitFailure else exitSuccess
+
+        _ => exitInvalidInput
+    
+    where head' [] = Nothing
+          head' xs = Just (head xs)
 
 -- Calculates the sum of the digits of `n`.
-sumDigits : Nat -> Int
+sumDigits : Int -> Int
 sumDigits = sumDigitsTail 0
-    where
-        sumDigitsTail : Int -> Nat -> Int
-        sumDigitsTail acc Z = acc
-        sumDigitsTail acc n = sumDigitsTail (acc + fromNat n `mod` 10) 
-                                            (n `div` 10)
-
-diff : Nat -> Nat -> Int
-diff a b = (sumDigits (a + b) - sumDigits a - sumDigits b) `mod` 9
-
--- TODO: Prove this
-test : (a : Nat) -> (b : Nat) -> diff a b = 0
-test = ?test
-
-iter : (a : Nat) -> Every (test a) a
-iter Z = Base (test a)
-iter (S b) = Succ n (test b) (iter b) (test a b)
-
-conjecture : (max : Nat) -> Every iter max
-conjecture Z = Base iter
-conjecture (S a) = Succ a iter (conjecture a) (iter a)
+    where sumDigitsTail acc n
+              | n == 0 = acc
+              | otherwise = sumDigitsTail (acc + (n `mod` 10)) (n `div` 10)
+
+-- Returns `True` if the if the conjecture holds for pair.
+-- Otherwise returns `False`.
+test' : Vector Int -> (Int, Int) -> Bool
+test' sums (a, b) = diff `mod` 9 == 0
+    where diff = sums ! (a + b) - sums ! a - sums ! b
+          (!) = unsafeIndex
+
+-- Checks if there is any counterexample in
+-- [(a, b) | a <- [0..max], b <- [a..max]].
+--
+-- Returns `True` if a counter example was found.
+-- Otherwise returns `False`.
+counterexempl : Int -> Bool
+counterexempl max =
+    all (test' sums) [(a, b) | a <- [0..max], b <- [a..max]]
+    where sums = generate (2 * max + 1) sumDigits
+
+exitInvalidInput : IO Int
+exitInvalidInput = exitWith $ ExitFailure 2

diff --git a/Java/.gitignore b/Java/.gitignore
@@ -1,4 +0,0 @@
-.idea
-out
-src/META-INF
-Java.iml

diff --git a/Kotlin/.gitignore b/Kotlin/.gitignore
@@ -1,2 +0,0 @@
-.idea
-out-
\ No newline at end of file

diff --git a/Kotlin/bin.jar b/Kotlin/bin.jar
Binary files differ.

diff --git a/Makefile b/Makefile
@@ -0,0 +1,30 @@
+c:
+	gcc -pthread -o bin/c C/main.c
+
+elixir:
+	elixirc -o bin/elixir Elixir/main.ex
+
+go:
+	cd Go/ ; go build ; mv ./Go ../bin/go ; cd ..
+
+haskell:
+	ghc --make -O -o bin/haskell Haskell/Main.hs \
+	    && rm Haskell/*.o Haskell/*.hi
+
+java:
+	javac Java/Main.java
+	jar cfe bin/java.jar Main Java/Main.class && rm Java/*.class
+
+kotlin:
+	kotlinc Kotlin/main.kt -d bin/kotlin.jar
+
+ocaml:
+	ocamlfind ocamlopt -thread -package threads -o bin/ocaml -linkpkg OCaml/main.ml \
+	    && rm OCaml/*.cmi OCaml/*.cmx OCaml/*.o
+
+rust:
+	rustc -v -o bin/rust Rust/main.rs
+
+wasm:
+	wat2wasm Wasm/main.wat -o bin/wasm.wasm
+

diff --git a/Rust/.gitignore b/Rust/.gitignore
@@ -1,2 +0,0 @@
-/target
-**/*.rs.bk

diff --git a/Wasm/.gitignore b/Wasm/.gitignore
@@ -1,2 +0,0 @@
-test
-*.wasm