From 5f24ba2f5bff05850522927d25d03f4cf96ab602 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Sat, 2 Aug 2025 01:12:51 +0000 Subject: [PATCH 01/13] Add rationals and rational plus, v1 --- Prelude.tel | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Prelude.tel b/Prelude.tel index a2caa5d..d4555b9 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -115,3 +115,20 @@ max = \a b -> { \p -> and (left p) (right p) } (a,b) fakeRecur = \n t r b -> n (\rec i -> if t i then r rec i else b i) 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 3fb444f79435b88214e8a8eba7e3b516a4e27cfd Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Tue, 5 Aug 2025 21:23:37 +0000 Subject: [PATCH 02/13] Refactor Rational arithmetic --- Prelude.tel | 61 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 50 insertions(+), 11 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index d4555b9..ebd1dc1 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 @@ -83,6 +94,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 @@ -116,19 +129,45 @@ max = \a b -> { \p -> and (left p) (right p) fakeRecur = \n t r b -> n (\rec i -> if t i then r rec i else b i) 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 0513a57002bb65436c97e70d87407f7f9c481563 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Wed, 6 Aug 2025 00:58:16 +0000 Subject: [PATCH 03/13] Add more Rational Arithmetic --- Prelude.tel | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Prelude.tel b/Prelude.tel index ebd1dc1..6799626 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -171,3 +171,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 ef5cd64c588f1eff3817dad54fe4349fa9cba8ac Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 8 Aug 2025 19:11:55 +0000 Subject: [PATCH 04/13] Refactor Rational as a UDT --- Prelude.tel | 109 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 62 insertions(+), 47 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index 6799626..88019ba 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -143,50 +143,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 041fac7edfca4e8719e6712c8dff042a43cd3188 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 8 Aug 2025 21:14:05 +0000 Subject: [PATCH 05/13] Refactor Rational arithmetic --- Prelude.tel | 92 +++++++++++++++++++++++------------------------------ 1 file changed, 40 insertions(+), 52 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index 88019ba..68f8d92 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -129,11 +129,7 @@ max = \a b -> { \p -> and (left p) (right p) fakeRecur = \n t r b -> n (\rec i -> if t i then r rec i else b i) 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) @@ -158,50 +154,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 e548145b5a3c6e2e2ed8de10e334387576003b7e Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 01:59:58 +0000 Subject: [PATCH 06/13] 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 a11a9a8..8bd9ccd 100644 --- a/telomare.cabal +++ b/telomare.cabal @@ -281,6 +281,26 @@ test-suite telomare-sizing-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 20d4a7a4cfc018371366b134f6cb915269c2e801 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 02:44:47 +0000 Subject: [PATCH 07/13] 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 4cce5b8aef21332a3be148efd1473eccc597ff68 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Thu, 14 Aug 2025 02:49:12 +0000 Subject: [PATCH 08/13] 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 f129459b0c701470d9ff2d399977c3b85b738ad2 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 15 Aug 2025 02:35:11 +0000 Subject: [PATCH 09/13] Refactor dDiv --- Prelude.tel | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Prelude.tel b/Prelude.tel index 68f8d92..ed3b3bc 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 3eef05c2e720987f27a8f3413a1e444b3c45f711 Mon Sep 17 00:00:00 2001 From: OswaldoMoper Date: Fri, 15 Aug 2025 02:36:19 +0000 Subject: [PATCH 10/13] 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)" From 8dc4a612e2032b1cefe2a150594abfb9cbb55784 Mon Sep 17 00:00:00 2001 From: hhefesto Date: Tue, 23 Dec 2025 13:13:00 -0600 Subject: [PATCH 11/13] arithmetic tests fail --- test/ArithmeticTests.hs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index edf77ed..80ee23a 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -11,6 +11,7 @@ import Control.Monad (unless) import Data.Bifunctor (second) import Data.List (isInfixOf) import Data.Ratio +import Debug.Trace import PrettyPrint import qualified System.IO.Strict as Strict import Telomare @@ -65,12 +66,15 @@ evalExprString input = do allBindings = fmap (second (tag DummyLoc)) allBindingsUPT uptMaybe = lookup "_tmp_" allBindings termMaybe = fmap ((DummyLoc :<) . LetUPF allBindings) uptMaybe - compiled = compileUnitTest =<< maybeToRight (termMaybe >>= rightToMaybe . process) + compiled = traceShowId (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) + Right compiledExpr -> + case toTelomare compiledExpr of + Just iexpr -> do + result <- simpleEval (SetEnv (Pair (Defer iexpr) Zero)) + pure $ Right (show $ PrettyIExpr result) + Nothing -> pure . Left $ "Unable to turn CompiledExpr to IExpr" assertExpr :: String -> String -> Assertion assertExpr input expected = do From c26e9aa780e96ee0b5d3860cbfb02770ec8685af Mon Sep 17 00:00:00 2001 From: hhefesto Date: Fri, 16 Jan 2026 17:39:18 -0600 Subject: [PATCH 12/13] Arithmetic test suite works --- .gitignore | 1 - app/Repl.hs | 3 ++- hie.yaml | 3 +++ src/Telomare/Eval.hs | 18 ++++++++++++---- test/ArithmeticTests.hs | 47 ++++++++++++++++++----------------------- 5 files changed, 39 insertions(+), 33 deletions(-) diff --git a/.gitignore b/.gitignore index 49e109c..700cb5e 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,5 @@ libgc.so notes.md result result-* -hie.yaml dev-profile* .direnv/ diff --git a/app/Repl.hs b/app/Repl.hs index 08665ae..cc4e427 100644 --- a/app/Repl.hs +++ b/app/Repl.hs @@ -110,7 +110,8 @@ printLastExpr eval bindings = do case lookup "_tmp_" bindings' of Nothing -> putStrLn "Could not find _tmp_ in bindings" Just upt -> do - let compile' x = case compileUnitTestNoAbort x of + let compile' :: Term3 -> Either String IExpr + compile' x = case compileUnitTestNoAbort x of Left err -> Left . show $ err Right r -> case toTelomare r of Just te -> pure $ fromTelomare te diff --git a/hie.yaml b/hie.yaml index 13f95ff..b143616 100644 --- a/hie.yaml +++ b/hie.yaml @@ -29,3 +29,6 @@ cradle: - path: "./test/SizingTests.hs" component: "test:telomare-sizing-test" + + - path: "./test/ArithmeticTests.hs" + component: "test:telomare-arithmetic-test" diff --git a/src/Telomare/Eval.hs b/src/Telomare/Eval.hs index 1fa3944..4441056 100644 --- a/src/Telomare/Eval.hs +++ b/src/Telomare/Eval.hs @@ -173,7 +173,10 @@ funWrap fun app inp = Just z -> ("unexpected runtime value, dumped:\n" <> show z, Left $ GenericRunTimeError "unexpected runtime value" z) Left e -> ("runtime error:\n" <> show e, Left e) -runMainCore :: [(String, String)] -> String -> (CompiledExpr -> IO a) -> IO a +runMainCore :: [(String, String)] -- ^All modules as (Module_Name, Module_Content) + -> String -- ^Module's name with `main` function + -> (CompiledExpr -> IO a) + -> IO a runMainCore modulesStrings s e = let parsedModules :: [(String, Either String [Either AnnotatedUPT (String, AnnotatedUPT)])] parsedModules = (fmap . fmap) parseModule modulesStrings @@ -204,13 +207,20 @@ runMainCore modulesStrings s e = Right (Right g) -> e g Right (Left z) -> error $ "compilation failed somehow, with result:\n" <> show z -runMain_ :: [(String, String)] -> String -> IO String +runMain_ :: [(String, String)] -- ^All modules as (Module_Name, Module_Content) + -> String -- ^Module's name with `main` function + -> IO String runMain_ modulesStrings s = runMainCore modulesStrings s evalLoop_ -runMain :: [(String, String)] -> String -> IO () +runMain :: [(String, String)] -- ^All modules as (Module_Name, Module_Content) + -> String -- ^Module's name with `main` function + -> IO () runMain modulesStrings s = runMainCore modulesStrings s evalLoop -runMainWithInput :: [String] -> [(String, String)] -> String -> IO String +runMainWithInput :: [String] -- ^Inputs + -> [(String, String)] -- ^All modules as (Module_Name, Module_Content) + -> String -- ^Module's name with `main` function + -> IO String runMainWithInput inputList modulesStrings s = runMainCore modulesStrings s (evalLoopWithInput inputList) schemeEval :: IExpr -> IO () diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index 80ee23a..0d29e08 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -8,7 +8,7 @@ module Main where import Common import Control.Comonad.Cofree (Cofree ((:<))) import Control.Monad (unless) -import Data.Bifunctor (second) +import Data.Bifunctor (Bifunctor (first)) import Data.List (isInfixOf) import Data.Ratio import Debug.Trace @@ -24,6 +24,7 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck as QC import Text.Megaparsec (eof, errorBundlePretty, runParser) +import Telomare.Eval (compileUnitTestNoAbort) main :: IO () main = defaultMain tests @@ -32,12 +33,8 @@ tests :: TestTree tests = testGroup "Arithmetic Tests" [ unitTestsNatArithmetic , unitTestsRatArithmetic , qcPropsNatArithmetic - , qcPropsRatArithmetic] - -parseReplExpr :: TelomareParser [(String, UnprocessedParsedTerm)] -parseReplExpr = do - expr <- parseLongExpr <* eof - pure [("_tmp_", forget expr)] + , qcPropsRatArithmetic + ] maybeToRight :: Maybe a -> Either EvalError a maybeToRight (Just x) = Right x @@ -47,34 +44,32 @@ rightToMaybe :: Either String a -> Maybe a rightToMaybe (Right x) = Just x rightToMaybe _ = Nothing -loadPreludeBindings :: IO [(String, UnprocessedParsedTerm)] +loadPreludeBindings :: IO [(String, AnnotatedUPT)] loadPreludeBindings = do preludeResult <- Strict.readFile "Prelude.tel" case parsePrelude preludeResult of Left _ -> pure [] - Right bs -> pure $ fmap (second forget) bs + Right bs -> pure bs evalExprString :: String -> IO (Either String String) evalExprString input = do preludeBindings <- loadPreludeBindings - let parseResult = runParser (parseReplExpr <* eof) "" input + let parseResult = runParser (parseLongExpr <* 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 :<) . LetUPF allBindings) uptMaybe - compiled = traceShowId (compileUnitTest =<< maybeToRight (termMaybe >>= rightToMaybe . process)) - case compiled of + Right aupt -> do + let term = DummyLoc :< LetUPF preludeBindings aupt + compile' :: Term3 -> Either String IExpr + compile' x = case compileUnitTestNoAbort x of + Left err -> Left . show $ err + Right r -> case toTelomare r of + Just te -> pure $ fromTelomare te + Nothing -> Left $ "conversion error from compiled expr:\n" <> prettyPrint r + case process term >>= compile' of Left err -> pure $ Left (show err) - Right compiledExpr -> - case toTelomare compiledExpr of - Just iexpr -> do - result <- simpleEval (SetEnv (Pair (Defer iexpr) Zero)) - pure $ Right (show $ PrettyIExpr result) - Nothing -> pure . Left $ "Unable to turn CompiledExpr to IExpr" + Right iexpr -> case eval iexpr of + Left e -> pure . Left . show $ e + Right result -> pure . Right . show . PrettyIExpr $ result assertExpr :: String -> String -> Assertion assertExpr input expected = do @@ -203,6 +198,4 @@ qcPropsNatArithmetic = testGroup "Property tests on natural arithmetic expressio Right val -> val === show x ] -qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)" - [ - ] +qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)" [] From 96eb5c2ba8d25dd2d605e2f9a23483c1cd15b04c Mon Sep 17 00:00:00 2001 From: hhefesto Date: Fri, 16 Jan 2026 17:45:47 -0600 Subject: [PATCH 13/13] Lint and format --- test/ArithmeticTests.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/ArithmeticTests.hs b/test/ArithmeticTests.hs index 0d29e08..b21a809 100644 --- a/test/ArithmeticTests.hs +++ b/test/ArithmeticTests.hs @@ -15,7 +15,8 @@ import Debug.Trace import PrettyPrint import qualified System.IO.Strict as Strict import Telomare -import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest) +import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest, + compileUnitTestNoAbort) import Telomare.Parser (AnnotatedUPT, TelomareParser, parseLongExpr, parsePrelude) import Telomare.Resolver (process) @@ -24,7 +25,7 @@ import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck as QC import Text.Megaparsec (eof, errorBundlePretty, runParser) -import Telomare.Eval (compileUnitTestNoAbort) + main :: IO () main = defaultMain tests