Skip to content

Commit 59c2e33

Browse files
sfultongsfultong
authored
Merge pull request #142 from hhefesto/rationalArithmeticRebased
Rational arithmetic rebased
2 parents e6fe9b9 + 96eb5c2 commit 59c2e33

7 files changed

Lines changed: 322 additions & 6 deletions

File tree

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,5 @@ libgc.so
1313
notes.md
1414
result
1515
result-*
16-
hie.yaml
1716
dev-profile*
1817
.direnv/

‎Prelude.tel‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,16 @@ d2c = \n f b -> { id
1515

1616
c2d = \c -> c succ 0
1717

18+
dPlus = \a b -> d2c b succ a
19+
1820
plus = \m n f x -> m f (n f x)
1921

22+
dTimes = \a b -> d2c b (\x -> dPlus a x) 0
23+
2024
times = \m n f -> m (n f)
2125

26+
dPow = \a b -> d2c b (dTimes a) (succ 0)
27+
2228
pow = \m n -> n m
2329

2430
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
6167
in if a then equalsOne (d2c (left a) (\x -> left x) b)
6268
else not b
6369

70+
dDiv = \a b -> if (dEqual b 0)
71+
then abort "Undefined"
72+
else
73+
{ \p -> dMinus (left p) (right p)
74+
, \recur p -> succ (recur (dMinus (left p) (right p), right p))
75+
, \p -> if (dEqual (left p) (right p)) then succ 0 else 0
76+
} (a, b)
77+
6478
listLength = foldr (\a b -> succ b) 0
6579

6680
listEqual = \a b -> let pairsEqual = zipWith dEqual a b
@@ -83,6 +97,8 @@ take = \n l -> let lengthed = n (\x -> (0,x)) 0
8397

8498
factorial = \n -> foldr (\a b -> times (d2c a) b) $1 (range 1 (n,0))
8599

100+
dFactorial = \n -> factorial n succ 0
101+
86102
quicksort = { \l -> right l
87103
, \recur l -> let t = left l
88104
test = \x -> dMinus x t
@@ -115,3 +131,68 @@ max = \a b -> { \p -> and (left p) (right p)
115131
} (a,b)
116132

117133
fakeRecur = \n t r b -> n (\rec i -> if t i then r rec i else b i) b
134+
135+
dMod = \a b -> dMinus a (dTimes b (dDiv a b))
136+
137+
gcd = \a b ->
138+
{ \p -> not (dEqual (right p) 0)
139+
, \recur p -> recur (right p, dMod (left p) (right p))
140+
, \p -> left p
141+
} (a,b)
142+
143+
lcm = \a b -> dDiv (dTimes a b) (gcd a b)
144+
145+
Rational =
146+
let wrapper = \h -> (
147+
\n d -> if dEqual d 0
148+
then abort "Denominator cannot be zero"
149+
else
150+
let g = gcd n d
151+
num = dDiv n g
152+
den = dDiv d g
153+
in (h, (num, den))
154+
, \i -> if dEqual (left i) h
155+
then right i
156+
else abort "Not a Rational"
157+
)
158+
in wrapper (# wrapper)
159+
160+
toRational = right Rational
161+
162+
fromRational = left Rational
163+
164+
rPlus = \a b ->
165+
let n1 = left (right a)
166+
d1 = right (right a)
167+
n2 = left (right b)
168+
d2 = right (right b)
169+
num = dPlus (dTimes n1 d2) (dTimes n2 d1)
170+
den = dTimes d1 d2
171+
in fromRational num den
172+
173+
rTimes = \a b ->
174+
let n1 = left (right a)
175+
d1 = right (right a)
176+
n2 = left (right b)
177+
d2 = right (right b)
178+
num = dTimes n1 n2
179+
den = dTimes d1 d2
180+
in fromRational num den
181+
182+
rMinus = \a b ->
183+
let n1 = left (right a)
184+
d1 = right (right a)
185+
n2 = left (right b)
186+
d2 = right (right b)
187+
num = dMinus (dTimes n1 d2) (dTimes n2 d1)
188+
den = dTimes d1 d2
189+
in fromRational num den
190+
191+
rDiv = \a b ->
192+
let n1 = left (right a)
193+
d1 = right (right a)
194+
n2 = left (right b)
195+
d2 = right (right b)
196+
num = dTimes n1 d2
197+
den = dTimes d1 n2
198+
in fromRational num den

‎app/Repl.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,8 @@ printLastExpr eval bindings = do
110110
case lookup "_tmp_" bindings' of
111111
Nothing -> putStrLn "Could not find _tmp_ in bindings"
112112
Just upt -> do
113-
let compile' x = case compileUnitTestNoAbort x of
113+
let compile' :: Term3 -> Either String IExpr
114+
compile' x = case compileUnitTestNoAbort x of
114115
Left err -> Left . show $ err
115116
Right r -> case toTelomare r of
116117
Just te -> pure $ fromTelomare te

‎hie.yaml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,6 @@ cradle:
2929

3030
- path: "./test/SizingTests.hs"
3131
component: "test:telomare-sizing-test"
32+
33+
- path: "./test/ArithmeticTests.hs"
34+
component: "test:telomare-arithmetic-test"

‎src/Telomare/Eval.hs‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,10 @@ funWrap fun app inp =
173173
Just z -> ("unexpected runtime value, dumped:\n" <> show z, Left $ GenericRunTimeError "unexpected runtime value" z)
174174
Left e -> ("runtime error:\n" <> show e, Left e)
175175

176-
runMainCore :: [(String, String)] -> String -> (CompiledExpr -> IO a) -> IO a
176+
runMainCore :: [(String, String)] -- ^All modules as (Module_Name, Module_Content)
177+
-> String -- ^Module's name with `main` function
178+
-> (CompiledExpr -> IO a)
179+
-> IO a
177180
runMainCore modulesStrings s e =
178181
let parsedModules :: [(String, Either String [Either AnnotatedUPT (String, AnnotatedUPT)])]
179182
parsedModules = (fmap . fmap) parseModule modulesStrings
@@ -204,13 +207,20 @@ runMainCore modulesStrings s e =
204207
Right (Right g) -> e g
205208
Right (Left z) -> error $ "compilation failed somehow, with result:\n" <> show z
206209

207-
runMain_ :: [(String, String)] -> String -> IO String
210+
runMain_ :: [(String, String)] -- ^All modules as (Module_Name, Module_Content)
211+
-> String -- ^Module's name with `main` function
212+
-> IO String
208213
runMain_ modulesStrings s = runMainCore modulesStrings s evalLoop_
209214

210-
runMain :: [(String, String)] -> String -> IO ()
215+
runMain :: [(String, String)] -- ^All modules as (Module_Name, Module_Content)
216+
-> String -- ^Module's name with `main` function
217+
-> IO ()
211218
runMain modulesStrings s = runMainCore modulesStrings s evalLoop
212219

213-
runMainWithInput :: [String] -> [(String, String)] -> String -> IO String
220+
runMainWithInput :: [String] -- ^Inputs
221+
-> [(String, String)] -- ^All modules as (Module_Name, Module_Content)
222+
-> String -- ^Module's name with `main` function
223+
-> IO String
214224
runMainWithInput inputList modulesStrings s = runMainCore modulesStrings s (evalLoopWithInput inputList)
215225

216226
schemeEval :: IExpr -> IO ()

‎telomare.cabal‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,6 +281,26 @@ test-suite telomare-sizing-test
281281
ghc-options: -threaded -rtsopts -with-rtsopts=-N
282282
default-language: Haskell2010
283283

284+
test-suite telomare-arithmetic-test
285+
type: exitcode-stdio-1.0
286+
hs-source-dirs: test
287+
main-is: ArithmeticTests.hs
288+
other-modules: Common
289+
build-depends: base
290+
, containers
291+
, free
292+
, megaparsec
293+
, QuickCheck
294+
, strict
295+
, tasty
296+
, tasty-hunit
297+
, tasty-quickcheck
298+
, telomare
299+
, unix
300+
301+
ghc-options: -threaded -rtsopts -with-rtsopts=-N
302+
default-language: Haskell2010
303+
284304
benchmark telomare-serializer-benchmark
285305
type: exitcode-stdio-1.0
286306
hs-source-dirs: bench/

‎test/ArithmeticTests.hs‎

Lines changed: 202 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
{-# LANGUAGE FlexibleInstances #-}
2+
{-# LANGUAGE MultiParamTypeClasses #-}
3+
{-# LANGUAGE PartialTypeSignatures #-}
4+
{-# LANGUAGE ScopedTypeVariables #-}
5+
6+
module Main where
7+
8+
import Common
9+
import Control.Comonad.Cofree (Cofree ((:<)))
10+
import Control.Monad (unless)
11+
import Data.Bifunctor (Bifunctor (first))
12+
import Data.List (isInfixOf)
13+
import Data.Ratio
14+
import Debug.Trace
15+
import PrettyPrint
16+
import qualified System.IO.Strict as Strict
17+
import Telomare
18+
import Telomare.Eval (EvalError (CompileConversionError), compileUnitTest,
19+
compileUnitTestNoAbort)
20+
import Telomare.Parser (AnnotatedUPT, TelomareParser, parseLongExpr,
21+
parsePrelude)
22+
import Telomare.Resolver (process)
23+
import Telomare.RunTime (simpleEval)
24+
import Test.Tasty
25+
import Test.Tasty.HUnit
26+
import Test.Tasty.QuickCheck as QC
27+
import Text.Megaparsec (eof, errorBundlePretty, runParser)
28+
29+
30+
main :: IO ()
31+
main = defaultMain tests
32+
33+
tests :: TestTree
34+
tests = testGroup "Arithmetic Tests" [ unitTestsNatArithmetic
35+
, unitTestsRatArithmetic
36+
, qcPropsNatArithmetic
37+
, qcPropsRatArithmetic
38+
]
39+
40+
maybeToRight :: Maybe a -> Either EvalError a
41+
maybeToRight (Just x) = Right x
42+
maybeToRight Nothing = Left CompileConversionError
43+
44+
rightToMaybe :: Either String a -> Maybe a
45+
rightToMaybe (Right x) = Just x
46+
rightToMaybe _ = Nothing
47+
48+
loadPreludeBindings :: IO [(String, AnnotatedUPT)]
49+
loadPreludeBindings = do
50+
preludeResult <- Strict.readFile "Prelude.tel"
51+
case parsePrelude preludeResult of
52+
Left _ -> pure []
53+
Right bs -> pure bs
54+
55+
evalExprString :: String -> IO (Either String String)
56+
evalExprString input = do
57+
preludeBindings <- loadPreludeBindings
58+
let parseResult = runParser (parseLongExpr <* eof) "" input
59+
case parseResult of
60+
Left err -> pure $ Left (errorBundlePretty err)
61+
Right aupt -> do
62+
let term = DummyLoc :< LetUPF preludeBindings aupt
63+
compile' :: Term3 -> Either String IExpr
64+
compile' x = case compileUnitTestNoAbort x of
65+
Left err -> Left . show $ err
66+
Right r -> case toTelomare r of
67+
Just te -> pure $ fromTelomare te
68+
Nothing -> Left $ "conversion error from compiled expr:\n" <> prettyPrint r
69+
case process term >>= compile' of
70+
Left err -> pure $ Left (show err)
71+
Right iexpr -> case eval iexpr of
72+
Left e -> pure . Left . show $ e
73+
Right result -> pure . Right . show . PrettyIExpr $ result
74+
75+
assertExpr :: String -> String -> Assertion
76+
assertExpr input expected = do
77+
res <- evalExprString input
78+
case res of
79+
Left err -> unless (expected `isInfixOf` err) . assertFailure $ "Evaluation failed: " <> err
80+
Right val -> val @?= expected
81+
82+
rationalToString :: Ratio Integer -> String
83+
rationalToString r = "(" <> show (numerator r) <> "," <> show (denominator r) <> ")"
84+
85+
genInt :: Gen Int
86+
genInt = choose (0, 100)
87+
88+
genInt2 :: Gen Int
89+
genInt2 = choose (0, 85)
90+
91+
genInt3 :: Gen Int
92+
genInt3 = choose (0, 16)
93+
94+
genInt4 :: Gen Int
95+
genInt4 = choose (0, 6)
96+
97+
-----------------
98+
------ Unit Tests
99+
-----------------
100+
101+
unitTestsNatArithmetic :: TestTree
102+
unitTestsNatArithmetic = testGroup "Unit tests on natural arithmetic expresions"
103+
[ testCase "test addition" $ assertExpr "dPlus 1 2" (show (1 + 2))
104+
, testCase "test subtraction" $ assertExpr "dMinus 5 3" (show (5 - 3))
105+
, testCase "test substraction lower limit" $ assertExpr "dMinus 0 1" "0"
106+
, testCase "test multiplication" $ assertExpr "dTimes 3 4" (show (3 * 4))
107+
, testCase "test division" $ assertExpr "dDiv 8 2" (show (8 `div` 2))
108+
, testCase "test division by zero" $ assertExpr "dDiv 1 0" "abort:"
109+
, testCase "test equality" $ assertExpr "dEqual 3 3" "1"
110+
, testCase "test inequality" $ assertExpr "dEqual 3 4" "0"
111+
, testCase "test modulo" $ assertExpr "dMod 10 3" (show (10 `mod` 3))
112+
, testCase "test gcd" $ assertExpr "gcd 48 18" (show (gcd 48 18))
113+
, testCase "test lcm" $ assertExpr "lcm 12 15" (show (lcm 12 15))
114+
, testCase "test exponentiation" $ assertExpr "dPow 2 3" (show (2 ^ 3))
115+
, testCase "test exponentiation with zero exponent" $ assertExpr "dPow 5 0" "1"
116+
, testCase "test raise zero to the zero power" $ assertExpr "dPow 0 0" "1"
117+
, testCase "test factorial" $ assertExpr "dFactorial 5" (show (product [1..5]))
118+
]
119+
120+
unitTestsRatArithmetic :: TestTree
121+
unitTestsRatArithmetic = testGroup "Unit tests on rational arithmetic expresions"
122+
[ testCase "test addition" $ do
123+
let exp = rationalToString (1 % 2 + 1 % 2)
124+
assertExpr "right (rPlus (fromRational 1 2) (fromRational 1 2))" exp
125+
, testCase "test subtraction" $ do
126+
let exp = rationalToString (1 % 2 - 1 % 2)
127+
assertExpr "right (rMinus (fromRational 1 2) (fromRational 1 2))" exp
128+
, testCase "test multiplication" $ do
129+
let exp = rationalToString ((1 % 2) * (1 % 2))
130+
assertExpr "right (rTimes (fromRational 1 2) (fromRational 1 2))" exp
131+
, testCase "test division" $ do
132+
let exp = rationalToString ((1 % 2) / (1 % 2))
133+
assertExpr "right (rDiv (fromRational 1 2) (fromRational 1 2))" exp
134+
, testCase "test division by zero" $ assertExpr "rDiv (fromRational 1 2) (fromRational 0 1)" "abort:"
135+
]
136+
137+
---------------------
138+
------ Property Tests
139+
---------------------
140+
141+
qcPropsNatArithmetic = testGroup "Property tests on natural arithmetic expressions (QuickCheck)"
142+
[ QC.testProperty "Commutative Additive" $
143+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
144+
x <- generate genInt
145+
y <- generate genInt
146+
res <- evalExprString
147+
( "dEqual (dPlus " <> show x <> " " <> show y <>
148+
") (dPlus " <> show y <> " " <> show x <> ")" )
149+
pure $ case res of
150+
Left err -> err === "1"
151+
Right val -> val === "1"
152+
, QC.testProperty "Associative Additive" $
153+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
154+
x <- generate genInt2
155+
y <- generate genInt2
156+
z <- generate genInt2
157+
res <- evalExprString
158+
( "dEqual (dPlus (dPlus " <> show x <> " " <> show y
159+
<> ")" <> show z <> ") (dPlus " <> show x <> "(dPlus "
160+
<> show y <> " " <> show z <>"))" )
161+
pure $ case res of
162+
Left err -> err === "1"
163+
Right val -> val === "1"
164+
, QC.testProperty "Neutral Additive" $
165+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
166+
x <- generate genInt
167+
res <- evalExprString ("dPlus " <> show x <> " 0")
168+
pure $ case res of
169+
Left err -> err === show x
170+
Right val -> val === show x
171+
, QC.testProperty "Commutative Multiplicative" $
172+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
173+
x <- generate genInt3
174+
y <- generate genInt3
175+
res <- evalExprString
176+
( "dEqual (dTimes " <> show x <> " " <> show y <>
177+
") (dTimes " <> show y <> " " <> show x <> ")" )
178+
pure $ case res of
179+
Left err -> err === "1"
180+
Right val -> val === "1"
181+
, QC.testProperty "Associative Multiplicative" $
182+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
183+
x <- generate genInt4
184+
y <- generate genInt4
185+
z <- generate genInt4
186+
res <- evalExprString
187+
( "dEqual (dTimes (dTimes " <> show x <> " " <> show y
188+
<> ")" <> show z <> ") (dTimes " <> show x <> "(dTimes "
189+
<> show y <> " " <> show z <>"))" )
190+
pure $ case res of
191+
Left err -> err === "1"
192+
Right val -> val === "1"
193+
, QC.testProperty "Neutral Multiplicative" $
194+
\() -> withMaxSuccess 16 . QC.idempotentIOProperty $ do
195+
x <- generate genInt
196+
res <- evalExprString ("dTimes " <> show x <> " 1")
197+
pure $ case res of
198+
Left err -> err === show x
199+
Right val -> val === show x
200+
]
201+
202+
qcPropsRatArithmetic = testGroup "Property tests on rational arithmetic expressions (QuickCheck)" []

0 commit comments

Comments
 (0)