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/Prelude.tel b/Prelude.tel index a2caa5d..ed3b3bc 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,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 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/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..b21a809 --- /dev/null +++ b/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)" []