Rational arithmetic rebased

.gitignore

@@ -13,6 +13,5 @@ libgc.so
 notes.md
 result
 result-*
-hie.yaml
 dev-profile*
 .direnv/

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,14 @@ 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 -> 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
 
 listEqual = \a b -> let pairsEqual = zipWith dEqual a b
@@ -83,6 +97,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
@@ -115,3 +131,68 @@ 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
+
+dMod = \a b -> dMinus a (dTimes b (dDiv 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 =
+  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)
+
+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

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

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"

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 ()

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/

test/ArithmeticTests.hs

@@ -0,0 +1,202 @@
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+
+module Main where
+
+import Common
+import Control.Comonad.Cofree (Cofree ((:<)))
+import Control.Monad (unless)
+import Data.Bifunctor (Bifunctor (first))
+import Data.List (isInfixOf)
+import Data.Ratio
+import Debug.Trace
+import PrettyPrint
+import qualified System.IO.Strict as Strict
+import Telomare
+import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest,
+                      compileUnitTestNoAbort)
+import Telomare.Parser (AnnotatedUPT, TelomareParser, parseLongExpr,
+                        parsePrelude)
+import Telomare.Resolver (process)
+import Telomare.RunTime (simpleEval)
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck as QC
+import Text.Megaparsec (eof, errorBundlePretty, runParser)
+
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Arithmetic Tests" [ unitTestsNatArithmetic
+                                     , unitTestsRatArithmetic
+                                     , qcPropsNatArithmetic
+                                     , qcPropsRatArithmetic
+                                     ]
+
+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, AnnotatedUPT)]
+loadPreludeBindings = do
+  preludeResult <- Strict.readFile "Prelude.tel"
+  case parsePrelude preludeResult of
+    Left _   -> pure []
+    Right bs -> pure bs
+
+evalExprString :: String -> IO (Either String String)
+evalExprString input = do
+  preludeBindings <- loadPreludeBindings
+  let parseResult = runParser (parseLongExpr <* eof) "" input
+  case parseResult of
+    Left err -> pure $ Left (errorBundlePretty err)
+    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 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
+  res <- evalExprString input
+  case res of
+    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
+-----------------
+
+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]))
+  ]
+
+unitTestsRatArithmetic :: TestTree
+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
+  , 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
+  , testCase "test division by zero" $ assertExpr "rDiv (fromRational 1 2) (fromRational 0 1)" "abort:"
+  ]
+
+---------------------
+------ Property Tests
+---------------------
+
+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)" []