From adcb95933e65888b6b8aa3a4a8481068d0ff7c2b Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Sat, 2 Aug 2025 01:12:51 +0000 Subject: [PATCH 01/10] Add rationals and rational plus, v1 --- Prelude.tel | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Prelude.tel b/Prelude.tel index f849300..a2ecfbf 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -103,3 +103,20 @@ max = \a b -> { \p -> or (left p) (right p) , \recur p -> recur (left (left p), left (right p)) , \p -> if (left p) then b else a } (a,b) + +Rational = \n d -> + if dEqual d 0 then ("E", "Denominator cannot be zero") + else if dEqual n d then ("R", (1,1)) + else ("R", (n,d)) + +-- TODO: implement decimal arithmetic instead of Church arithmetic +rPlus = \a b -> + if not (dEqual (left a) "R") then a + else if not (dEqual (left b) "R") then b + else let n1 = d2c (left (right a)) + d1 = d2c (right (right a)) + n2 = d2c (left (right b)) + d2 = d2c (right (right b)) + num = plus (times n1 d2) (times n2 d1) + den = times d1 d2 + in ("R", (c2d num, c2d den)) From e0111d6af723dae2e4ed4292cd6fa9b4e56148b9 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Tue, 5 Aug 2025 21:23:37 +0000 Subject: [PATCH 02/10] Refactor Rational arithmetic --- Prelude.tel | 61 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 50 insertions(+), 11 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index a2ecfbf..6552de5 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -15,10 +15,16 @@ d2c = \n f b -> { id c2d = \c -> c succ 0 +dPlus = \a b -> d2c b succ a + plus = \m n f x -> m f (n f x) +dTimes = \a b -> d2c b (\x -> dPlus a x) 0 + times = \m n f -> m (n f) +dPow = \a b -> d2c b (dTimes a) (succ 0) + pow = \m n -> n m dMinus = \a b -> d2c b (\x -> left x) a @@ -61,6 +67,11 @@ dEqual = \a b -> let equalsOne = \x -> if x then (not (left x)) else 0 in if a then equalsOne (d2c (left a) (\x -> left x) b) else not b +dDiv = \a b -> { \p -> dMinus (left p) (right p) + , \recur p -> succ (recur (dMinus (left p) (right p), right p)) + , \p -> if (dEqual (left p) (right p)) then succ 0 else 0 + } (a, b) + listLength = foldr (\a b -> succ b) 0 listEqual = \a b -> let pairsEqual = zipWith dEqual a b @@ -78,6 +89,8 @@ take = \n l -> let lengthed = n (\x -> (0,x)) 0 factorial = \n -> foldr (\a b -> times (d2c a) b) $1 (range 1 (n,0)) +dFactorial = \n -> factorial n succ 0 + quicksort = { \l -> right l , \recur l -> let t = left l test = \x -> dMinus x t @@ -104,19 +117,45 @@ max = \a b -> { \p -> or (left p) (right p) , \p -> if (left p) then b else a } (a,b) +dMod = \a b -> + { \p -> dMinus (left p) (right p) + , \recur p -> recur (dMinus (left p) (right p), right p) + , \p -> left p + } (a, b) + +gcd = \a b -> + { \p -> not (dEqual (right p) 0) + , \recur p -> recur (right p, dMod (left p) (right p)) + , \p -> left p + } (a,b) + +lcm = \a b -> dDiv (dTimes a b) (gcd a b) + Rational = \n d -> if dEqual d 0 then ("E", "Denominator cannot be zero") - else if dEqual n d then ("R", (1,1)) - else ("R", (n,d)) + else + let g = gcd n d + num = dDiv n g + den = dDiv d g + in ("R", (num,den)) --- TODO: implement decimal arithmetic instead of Church arithmetic rPlus = \a b -> - if not (dEqual (left a) "R") then a + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dPlus (dTimes n1 d2) (dTimes n2 d1) + den = dTimes d1 d2 + in Rational num den + +rTimes = \a b -> + if not (dEqual (left a) "R") then a else if not (dEqual (left b) "R") then b - else let n1 = d2c (left (right a)) - d1 = d2c (right (right a)) - n2 = d2c (left (right b)) - d2 = d2c (right (right b)) - num = plus (times n1 d2) (times n2 d1) - den = times d1 d2 - in ("R", (c2d num, c2d den)) + else let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dTimes n1 n2 + den = dTimes d1 d2 + in Rational num den + From 95aec27755c6b943826111801965e860d92a374b Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Wed, 6 Aug 2025 00:58:16 +0000 Subject: [PATCH 03/10] Add more Rational Arithmetic --- Prelude.tel | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Prelude.tel b/Prelude.tel index 6552de5..f9f5638 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -159,3 +159,22 @@ rTimes = \a b -> den = dTimes d1 d2 in Rational num den +rMinus = \a b -> + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dMinus (dTimes n1 d2) (dTimes n2 d1) + den = dTimes d1 d2 + in Rational num den + +rDiv = \a b -> + if not (dEqual (left a) "R") then a + else if not (dEqual (left b) "R") then b + else let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dTimes n1 d2 + den = dTimes d1 n2 + in Rational num den From 3ae930712db31476e7c00b92583eb16c78cb336b Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 8 Aug 2025 19:11:55 +0000 Subject: [PATCH 04/10] Refactor Rational as a UDT --- Prelude.tel | 109 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 62 insertions(+), 47 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index f9f5638..b4710f4 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -131,50 +131,65 @@ gcd = \a b -> lcm = \a b -> dDiv (dTimes a b) (gcd a b) -Rational = \n d -> - if dEqual d 0 then ("E", "Denominator cannot be zero") - else - let g = gcd n d - num = dDiv n g - den = dDiv d g - in ("R", (num,den)) - -rPlus = \a b -> - let n1 = left (right a) - d1 = right (right a) - n2 = left (right b) - d2 = right (right b) - num = dPlus (dTimes n1 d2) (dTimes n2 d1) - den = dTimes d1 d2 - in Rational num den - -rTimes = \a b -> - if not (dEqual (left a) "R") then a - else if not (dEqual (left b) "R") then b - else let n1 = left (right a) - d1 = right (right a) - n2 = left (right b) - d2 = right (right b) - num = dTimes n1 n2 - den = dTimes d1 d2 - in Rational num den - -rMinus = \a b -> - let n1 = left (right a) - d1 = right (right a) - n2 = left (right b) - d2 = right (right b) - num = dMinus (dTimes n1 d2) (dTimes n2 d1) - den = dTimes d1 d2 - in Rational num den - -rDiv = \a b -> - if not (dEqual (left a) "R") then a - else if not (dEqual (left b) "R") then b - else let n1 = left (right a) - d1 = right (right a) - n2 = left (right b) - d2 = right (right b) - num = dTimes n1 d2 - den = dTimes d1 n2 - in Rational num den +Rational = + let wrapper = \h -> ( + \n d -> if dEqual d 0 + then abort "Denominator cannot be zero" + else + let g = gcd n d + num = dDiv n g + den = dDiv d g + in (h, (num, den)) + , \i -> if dEqual (left i) h + then right i + else abort "Not a Rational" + ) + in wrapper (# wrapper) + +-- Rational = \n d -> +-- if dEqual d 0 then ("E", "Denominator cannot be zero") +-- else +-- let g = gcd n d +-- num = dDiv n g +-- den = dDiv d g +-- in ("R", (num,den)) + +-- rPlus = \a b -> +-- let n1 = left (right a) +-- d1 = right (right a) +-- n2 = left (right b) +-- d2 = right (right b) +-- num = dPlus (dTimes n1 d2) (dTimes n2 d1) +-- den = dTimes d1 d2 +-- in Rational num den + +-- rTimes = \a b -> +-- if not (dEqual (left a) "R") then a +-- else if not (dEqual (left b) "R") then b +-- else let n1 = left (right a) +-- d1 = right (right a) +-- n2 = left (right b) +-- d2 = right (right b) +-- num = dTimes n1 n2 +-- den = dTimes d1 d2 +-- in Rational num den + +-- rMinus = \a b -> +-- let n1 = left (right a) +-- d1 = right (right a) +-- n2 = left (right b) +-- d2 = right (right b) +-- num = dMinus (dTimes n1 d2) (dTimes n2 d1) +-- den = dTimes d1 d2 +-- in Rational num den + +-- rDiv = \a b -> +-- if not (dEqual (left a) "R") then a +-- else if not (dEqual (left b) "R") then b +-- else let n1 = left (right a) +-- d1 = right (right a) +-- n2 = left (right b) +-- d2 = right (right b) +-- num = dTimes n1 d2 +-- den = dTimes d1 n2 +-- in Rational num den From 7a5467f03288c343d0fcd242f926d4b52243009b Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 8 Aug 2025 21:14:05 +0000 Subject: [PATCH 05/10] Refactor Rational arithmetic --- Prelude.tel | 92 +++++++++++++++++++++++------------------------------ 1 file changed, 40 insertions(+), 52 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index b4710f4..25e17ed 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -117,11 +117,7 @@ max = \a b -> { \p -> or (left p) (right p) , \p -> if (left p) then b else a } (a,b) -dMod = \a b -> - { \p -> dMinus (left p) (right p) - , \recur p -> recur (dMinus (left p) (right p), right p) - , \p -> left p - } (a, b) +dMod = \a b -> dMinus a (dTimes b (dDiv a b)) gcd = \a b -> { \p -> not (dEqual (right p) 0) @@ -146,50 +142,42 @@ Rational = ) in wrapper (# wrapper) --- Rational = \n d -> --- if dEqual d 0 then ("E", "Denominator cannot be zero") --- else --- let g = gcd n d --- num = dDiv n g --- den = dDiv d g --- in ("R", (num,den)) - --- rPlus = \a b -> --- let n1 = left (right a) --- d1 = right (right a) --- n2 = left (right b) --- d2 = right (right b) --- num = dPlus (dTimes n1 d2) (dTimes n2 d1) --- den = dTimes d1 d2 --- in Rational num den - --- rTimes = \a b -> --- if not (dEqual (left a) "R") then a --- else if not (dEqual (left b) "R") then b --- else let n1 = left (right a) --- d1 = right (right a) --- n2 = left (right b) --- d2 = right (right b) --- num = dTimes n1 n2 --- den = dTimes d1 d2 --- in Rational num den - --- rMinus = \a b -> --- let n1 = left (right a) --- d1 = right (right a) --- n2 = left (right b) --- d2 = right (right b) --- num = dMinus (dTimes n1 d2) (dTimes n2 d1) --- den = dTimes d1 d2 --- in Rational num den - --- rDiv = \a b -> --- if not (dEqual (left a) "R") then a --- else if not (dEqual (left b) "R") then b --- else let n1 = left (right a) --- d1 = right (right a) --- n2 = left (right b) --- d2 = right (right b) --- num = dTimes n1 d2 --- den = dTimes d1 n2 --- in Rational num den +toRational = right Rational + +fromRational = left Rational + +rPlus = \a b -> + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dPlus (dTimes n1 d2) (dTimes n2 d1) + den = dTimes d1 d2 + in fromRational num den + +rTimes = \a b -> + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dTimes n1 n2 + den = dTimes d1 d2 + in fromRational num den + +rMinus = \a b -> + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dMinus (dTimes n1 d2) (dTimes n2 d1) + den = dTimes d1 d2 + in fromRational num den + +rDiv = \a b -> + let n1 = left (right a) + d1 = right (right a) + n2 = left (right b) + d2 = right (right b) + num = dTimes n1 d2 + den = dTimes d1 n2 + in fromRational num den From ec9c40f422ffe842bbc5de6a17af2b7942b8b91b Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 01:59:58 +0000 Subject: [PATCH 06/10] Add arithmetic test suite --- telomare.cabal | 20 ++++++++ test/ArithmeticTests.hs | 104 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 124 insertions(+) create mode 100644 test/ArithmeticTests.hs diff --git a/telomare.cabal b/telomare.cabal index 4cd6f0f..8c3729f 100644 --- a/telomare.cabal +++ b/telomare.cabal @@ -224,6 +224,26 @@ test-suite telomare-resolver-test ghc-options: -threaded -rtsopts -with-rtsopts=-N default-language: Haskell2010 +test-suite telomare-arithmetic-test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: ArithmeticTests.hs + other-modules: Common + build-depends: base + , containers + , free + , megaparsec + , QuickCheck + , strict + , tasty + , tasty-hunit + , tasty-quickcheck + , telomare + , unix + + ghc-options: -threaded -rtsopts -with-rtsopts=-N + default-language: Haskell2010 + benchmark telomare-serializer-benchmark type: exitcode-stdio-1.0 hs-source-dirs: bench/ diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs new file mode 100644 index 0000000..e879048 --- /dev/null +++ b/test/ArithmeticTests.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Main where + +import Common +import Control.Comonad.Cofree (Cofree ((:<))) +import Data.Bifunctor (second) +import PrettyPrint +import qualified System.IO.Strict as Strict +import Telomare +import Telomare.Eval (compileUnitTest, EvalError (CompileConversionError)) +import Telomare.RunTime (simpleEval) +import Telomare.Resolver (process) +import Telomare.Parser (parseLongExpr, TelomareParser, parsePrelude, AnnotatedUPT) +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck as QC +import Text.Megaparsec (runParser, errorBundlePretty, eof) + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "Arithmetic Tests" [ unitTestsNatArithmetic + , unitTestsRatArithmetic + , qcPropsNatArithmetic + , qcPropsRatArithmetic] + +parseReplExpr :: TelomareParser [(String, UnprocessedParsedTerm)] +parseReplExpr = do + expr <- parseLongExpr <* eof + pure [("_tmp_", forget expr)] + +maybeToRight :: Maybe a -> Either EvalError a +maybeToRight (Just x) = Right x +maybeToRight Nothing = Left CompileConversionError + +rightToMaybe :: Either String a -> Maybe a +rightToMaybe (Right x) = Just x +rightToMaybe _ = Nothing + +loadPreludeBindings :: IO [(String, UnprocessedParsedTerm)] +loadPreludeBindings = do + preludeResult <- Strict.readFile "Prelude.tel" + case parsePrelude preludeResult of + Left _ -> pure [] + Right bs -> pure $ fmap (second forget) bs + +evalExprString :: String -> IO (Either String String) +evalExprString input = do + preludeBindings <- loadPreludeBindings + let parseResult = runParser (parseReplExpr <* eof) "" input + case parseResult of + Left err -> pure $ Left (errorBundlePretty err) + Right exprBindings -> do + let allBindingsUPT = preludeBindings ++ exprBindings + allBindings :: [(String, Cofree UnprocessedParsedTermF LocTag)] + allBindings = fmap (second (tag DummyLoc)) allBindingsUPT + uptMaybe = lookup "_tmp_" allBindings + termMaybe = fmap (DummyLoc :<) . fmap (LetUPF allBindings) $ uptMaybe + compiled = compileUnitTest =<< maybeToRight (termMaybe >>= rightToMaybe . process) + case compiled of + Left err -> pure $ Left (show err) + Right iexpr -> do + result <- simpleEval (SetEnv (Pair (Defer iexpr) Zero)) + pure $ Right (show $ PrettyIExpr result) + +assertExpr :: String -> String -> Assertion +assertExpr input expected = do + res <- evalExprString input + case res of + Left err -> assertFailure $ "Evaluation failed: " <> err + Right val -> val @?= expected + +----------------- +------ Unit Tests +----------------- + +unitTestsNatArithmetic :: TestTree +unitTestsNatArithmetic = testGroup "Unit tests on natural arithmetic expresions" + [ testCase "test addition" $ assertExpr "dPlus 1 2" "3" + ] + +unitTestsRatArithmetic :: TestTree +unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" + [ + ] + +--------------------- +------ Property Tests +--------------------- + +qcPropsNatArithmetic = testGroup "Property tests on natural arithmetic expressions (QuickCheck)" + [ + ] + +qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)" + [ + ] From b038c1cae9c31b71057a6a4821669342a8fd91a4 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 02:44:47 +0000 Subject: [PATCH 07/10] Add Arithmetic Unit Tests --- test/ArithmeticTests.hs | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index e879048..b17f722 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -21,6 +21,7 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck as QC import Text.Megaparsec (runParser, errorBundlePretty, eof) +import Data.Ratio main :: IO () main = defaultMain tests @@ -77,18 +78,42 @@ assertExpr input expected = do Left err -> assertFailure $ "Evaluation failed: " <> err Right val -> val @?= expected +rationalToString :: Ratio Integer -> String +rationalToString r = "(" <> show (numerator r) <> "," <> show (denominator r) <> ")" + ----------------- ------ Unit Tests ----------------- unitTestsNatArithmetic :: TestTree unitTestsNatArithmetic = testGroup "Unit tests on natural arithmetic expresions" - [ testCase "test addition" $ assertExpr "dPlus 1 2" "3" + [ testCase "test addition" $ assertExpr "dPlus 1 2" (show (1 + 2)) + , testCase "test subtraction" $ assertExpr "dMinus 5 3" (show (5 - 3)) + , testCase "test multiplication" $ assertExpr "dTimes 3 4" (show (3 * 4)) + , testCase "test division" $ assertExpr "dDiv 8 2" (show (8 `div` 2)) + , testCase "test modulo" $ assertExpr "dMod 10 3" (show (10 `mod` 3)) + , testCase "test gcd" $ assertExpr "gcd 48 18" (show (gcd 48 18)) + , testCase "test lcm" $ assertExpr "lcm 12 15" (show (lcm 12 15)) + , testCase "test exponentiation" $ assertExpr "dPow 2 3" (show (2 ^ 3)) + , testCase "test factorial" $ assertExpr "dFactorial 5" (show (product [1..5])) + , testCase "test equality" $ assertExpr "dEqual 3 3" (show 1) + , testCase "test inequality" $ assertExpr "dEqual 3 4" (show 0) ] unitTestsRatArithmetic :: TestTree unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" - [ + [ testCase "test addition" $ do + let exp = rationalToString (1 % 2 + 1 % 2) + assertExpr "right (rPlus (fromRational 1 2) (fromRational 1 2))" exp + , testCase "test subtraction" $ do + let exp = rationalToString (1 % 2 - 1 % 2) + assertExpr "right (rMinus (fromRational 1 2) (fromRational 1 2))" exp + , testCase "test multiplication" $ do + let exp = rationalToString ((1 % 2) * (1 % 2)) + assertExpr "right (rTimes (fromRational 1 2) (fromRational 1 2))" exp + , testCase "test division" $ do + let exp = rationalToString ((1 % 2) / (1 % 2)) + assertExpr "right (rDiv (fromRational 1 2) (fromRational 1 2))" exp ] --------------------- From f89e9f3c98e61af66f7d285af3a87be16cae39f2 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 02:49:12 +0000 Subject: [PATCH 08/10] Formatting --- test/ArithmeticTests.hs | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index b17f722..8b46932 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -1,8 +1,6 @@ -{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE PartialTypeSignatures #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} module Main where @@ -10,18 +8,19 @@ module Main where import Common import Control.Comonad.Cofree (Cofree ((:<))) import Data.Bifunctor (second) +import Data.Ratio import PrettyPrint import qualified System.IO.Strict as Strict import Telomare -import Telomare.Eval (compileUnitTest, EvalError (CompileConversionError)) -import Telomare.RunTime (simpleEval) +import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest) +import Telomare.Parser (AnnotatedUPT, TelomareParser, parseLongExpr, + parsePrelude) import Telomare.Resolver (process) -import Telomare.Parser (parseLongExpr, TelomareParser, parsePrelude, AnnotatedUPT) +import Telomare.RunTime (simpleEval) import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck as QC -import Text.Megaparsec (runParser, errorBundlePretty, eof) -import Data.Ratio +import Text.Megaparsec (eof, errorBundlePretty, runParser) main :: IO () main = defaultMain tests @@ -49,7 +48,7 @@ loadPreludeBindings :: IO [(String, UnprocessedParsedTerm)] loadPreludeBindings = do preludeResult <- Strict.readFile "Prelude.tel" case parsePrelude preludeResult of - Left _ -> pure [] + Left _ -> pure [] Right bs -> pure $ fmap (second forget) bs evalExprString :: String -> IO (Either String String) @@ -59,11 +58,11 @@ evalExprString input = do case parseResult of Left err -> pure $ Left (errorBundlePretty err) Right exprBindings -> do - let allBindingsUPT = preludeBindings ++ exprBindings + let allBindingsUPT = preludeBindings <> exprBindings allBindings :: [(String, Cofree UnprocessedParsedTermF LocTag)] allBindings = fmap (second (tag DummyLoc)) allBindingsUPT uptMaybe = lookup "_tmp_" allBindings - termMaybe = fmap (DummyLoc :<) . fmap (LetUPF allBindings) $ uptMaybe + termMaybe = fmap ((DummyLoc :<) . LetUPF allBindings) uptMaybe compiled = compileUnitTest =<< maybeToRight (termMaybe >>= rightToMaybe . process) case compiled of Left err -> pure $ Left (show err) @@ -75,7 +74,7 @@ assertExpr :: String -> String -> Assertion assertExpr input expected = do res <- evalExprString input case res of - Left err -> assertFailure $ "Evaluation failed: " <> err + Left err -> assertFailure $ "Evaluation failed: " <> err Right val -> val @?= expected rationalToString :: Ratio Integer -> String @@ -121,9 +120,9 @@ unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" --------------------- qcPropsNatArithmetic = testGroup "Property tests on natural arithmetic expressions (QuickCheck)" - [ + [ ] qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)" - [ + [ ] From 28ce4ca9dacfd772cf053dd17dd089f7d3a8d8d2 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 15 Aug 2025 02:35:11 +0000 Subject: [PATCH 09/10] Refactor dDiv --- Prelude.tel | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index 25e17ed..d6b7b65 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -67,10 +67,13 @@ dEqual = \a b -> let equalsOne = \x -> if x then (not (left x)) else 0 in if a then equalsOne (d2c (left a) (\x -> left x) b) else not b -dDiv = \a b -> { \p -> dMinus (left p) (right p) - , \recur p -> succ (recur (dMinus (left p) (right p), right p)) - , \p -> if (dEqual (left p) (right p)) then succ 0 else 0 - } (a, b) +dDiv = \a b -> if (dEqual b 0) + then abort "Undefined" + else + { \p -> dMinus (left p) (right p) + , \recur p -> succ (recur (dMinus (left p) (right p), right p)) + , \p -> if (dEqual (left p) (right p)) then succ 0 else 0 + } (a, b) listLength = foldr (\a b -> succ b) 0 From 32f07b5dfcab808c0966071ecda5f6e97f590de7 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 15 Aug 2025 02:36:19 +0000 Subject: [PATCH 10/10] Add Natural arithmetic property Tests and some Unit Tests --- test/ArithmeticTests.hs | 86 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 81 insertions(+), 5 deletions(-) diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index 8b46932..edf77ed 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -7,7 +7,9 @@ module Main where import Common import Control.Comonad.Cofree (Cofree ((:<))) +import Control.Monad (unless) import Data.Bifunctor (second) +import Data.List (isInfixOf) import Data.Ratio import PrettyPrint import qualified System.IO.Strict as Strict @@ -74,12 +76,24 @@ assertExpr :: String -> String -> Assertion assertExpr input expected = do res <- evalExprString input case res of - Left err -> assertFailure $ "Evaluation failed: " <> err + Left err -> unless (expected `isInfixOf` err) . assertFailure $ "Evaluation failed: " <> err Right val -> val @?= expected rationalToString :: Ratio Integer -> String rationalToString r = "(" <> show (numerator r) <> "," <> show (denominator r) <> ")" +genInt :: Gen Int +genInt = choose (0, 100) + +genInt2 :: Gen Int +genInt2 = choose (0, 85) + +genInt3 :: Gen Int +genInt3 = choose (0, 16) + +genInt4 :: Gen Int +genInt4 = choose (0, 6) + ----------------- ------ Unit Tests ----------------- @@ -88,19 +102,23 @@ unitTestsNatArithmetic :: TestTree unitTestsNatArithmetic = testGroup "Unit tests on natural arithmetic expresions" [ testCase "test addition" $ assertExpr "dPlus 1 2" (show (1 + 2)) , testCase "test subtraction" $ assertExpr "dMinus 5 3" (show (5 - 3)) + , testCase "test substraction lower limit" $ assertExpr "dMinus 0 1" "0" , testCase "test multiplication" $ assertExpr "dTimes 3 4" (show (3 * 4)) , testCase "test division" $ assertExpr "dDiv 8 2" (show (8 `div` 2)) + , testCase "test division by zero" $ assertExpr "dDiv 1 0" "abort:" + , testCase "test equality" $ assertExpr "dEqual 3 3" "1" + , testCase "test inequality" $ assertExpr "dEqual 3 4" "0" , testCase "test modulo" $ assertExpr "dMod 10 3" (show (10 `mod` 3)) , testCase "test gcd" $ assertExpr "gcd 48 18" (show (gcd 48 18)) , testCase "test lcm" $ assertExpr "lcm 12 15" (show (lcm 12 15)) , testCase "test exponentiation" $ assertExpr "dPow 2 3" (show (2 ^ 3)) + , testCase "test exponentiation with zero exponent" $ assertExpr "dPow 5 0" "1" + , testCase "test raise zero to the zero power" $ assertExpr "dPow 0 0" "1" , testCase "test factorial" $ assertExpr "dFactorial 5" (show (product [1..5])) - , testCase "test equality" $ assertExpr "dEqual 3 3" (show 1) - , testCase "test inequality" $ assertExpr "dEqual 3 4" (show 0) ] unitTestsRatArithmetic :: TestTree -unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" +unitTestsRatArithmetic = testGroup "Unit tests on rational arithmetic expresions" [ testCase "test addition" $ do let exp = rationalToString (1 % 2 + 1 % 2) assertExpr "right (rPlus (fromRational 1 2) (fromRational 1 2))" exp @@ -113,6 +131,7 @@ unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" , testCase "test division" $ do let exp = rationalToString ((1 % 2) / (1 % 2)) assertExpr "right (rDiv (fromRational 1 2) (fromRational 1 2))" exp + , testCase "test division by zero" $ assertExpr "rDiv (fromRational 1 2) (fromRational 0 1)" "abort:" ] --------------------- @@ -120,7 +139,64 @@ unitTestsRatArithmetic = testGroup "Unit tests on natural arithmetic expresions" --------------------- qcPropsNatArithmetic = testGroup "Property tests on natural arithmetic expressions (QuickCheck)" - [ + [ QC.testProperty "Commutative Additive" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt + y <- generate genInt + res <- evalExprString + ( "dEqual (dPlus " <> show x <> " " <> show y <> + ") (dPlus " <> show y <> " " <> show x <> ")" ) + pure $ case res of + Left err -> err === "1" + Right val -> val === "1" + , QC.testProperty "Associative Additive" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt2 + y <- generate genInt2 + z <- generate genInt2 + res <- evalExprString + ( "dEqual (dPlus (dPlus " <> show x <> " " <> show y + <> ")" <> show z <> ") (dPlus " <> show x <> "(dPlus " + <> show y <> " " <> show z <>"))" ) + pure $ case res of + Left err -> err === "1" + Right val -> val === "1" + , QC.testProperty "Neutral Additive" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt + res <- evalExprString ("dPlus " <> show x <> " 0") + pure $ case res of + Left err -> err === show x + Right val -> val === show x + , QC.testProperty "Commutative Multiplicative" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt3 + y <- generate genInt3 + res <- evalExprString + ( "dEqual (dTimes " <> show x <> " " <> show y <> + ") (dTimes " <> show y <> " " <> show x <> ")" ) + pure $ case res of + Left err -> err === "1" + Right val -> val === "1" + , QC.testProperty "Associative Multiplicative" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt4 + y <- generate genInt4 + z <- generate genInt4 + res <- evalExprString + ( "dEqual (dTimes (dTimes " <> show x <> " " <> show y + <> ")" <> show z <> ") (dTimes " <> show x <> "(dTimes " + <> show y <> " " <> show z <>"))" ) + pure $ case res of + Left err -> err === "1" + Right val -> val === "1" + , QC.testProperty "Neutral Multiplicative" $ + \() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do + x <- generate genInt + res <- evalExprString ("dTimes " <> show x <> " 1") + pure $ case res of + Left err -> err === show x + Right val -> val === show x ] qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)"