Rational arithmetic [DO NOT MERGE YET]

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
@@ -78,6 +92,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
@@ -103,3 +119,68 @@ 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)
+
+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

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/

test/ArithmeticTests.hs

@@ -0,0 +1,204 @@
+{-# 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 (second)
+import Data.List (isInfixOf)
+import Data.Ratio
+import PrettyPrint
+import qualified System.IO.Strict as Strict
+import Telomare
+import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest)
+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]
+
+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 :<) . 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  -> 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)"
+  [
+  ]