Skip to content

Commit

Permalink
clean up a bit
Browse files Browse the repository at this point in the history
  • Loading branch information
thma committed Sep 16, 2023
1 parent a5e0910 commit 1512685
Show file tree
Hide file tree
Showing 7 changed files with 112 additions and 137 deletions.
31 changes: 31 additions & 0 deletions app/Main.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@

{-# LANGUAGE QuasiQuotes #-}
module Main where

import Control.Monad.ST
Expand All @@ -12,6 +14,8 @@ import Parser (Environment, Expr(..), parseEnvironment)
import System.IO (hSetEncoding, stdin, stdout, utf8)
import HhiReducer
import Kiselyov
import System.TimeIt
import Text.RawString.QQ

printGraph :: ST s (STRef s (Graph s)) -> ST s String
printGraph graph = do
Expand Down Expand Up @@ -68,6 +72,33 @@ main = do
putStrLn "The result after reducing the graph:"
putStrLn $ runST $ printGraph reducedGraph'

timeIt $ print $ tak 60 10 5

let pEnv = parseEnvironment tak'
aExp = compileBulk pEnv

timeIt $ print $ transLink primitives aExp

let aExp' = compileEta pEnv
timeIt $ print $ transLink primitives aExp'

runTest :: SourceCode -> String
runTest src =
let pEnv = parseEnvironment src
aExp = compileBulk pEnv
--tExp = translate aExp
in show $ transLink primitives aExp --link primitives tExp

tak :: Integer -> Integer -> Integer -> Integer
tak x y z = if y >= x then z else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)

tak' :: SourceCode
tak' = [r|
expected = 4
tak = y(λf x y z -> (if (geq y x) z (f (f (sub1 x) y z) (f (sub1 y) z x) (f (sub1 z) x y ))))
main = tak 60 10 5
|]

--demo

type SourceCode = String
Expand Down
91 changes: 39 additions & 52 deletions benchmark/ReductionBenchmarks.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,13 @@ import Criterion.Main ( defaultMain, bench, nf )
import Parser ( parseEnvironment, Expr(Int, App) )
import LambdaToSKI ( abstractToSKI, compile )
import CLTerm
import Kiselyov
import Kiselyov ( compileBulk, compileEta )
import GraphReduction ( allocate, normalForm, toString, Graph )
import Data.Maybe (fromJust)
import Data.STRef ( STRef )
import Control.Monad.ST ( ST, runST )
import HhiReducer ( primitives, transLink, CExpr(CInt, CApp) )
import Control.Monad.Fix ( fix )
import Kiselyov (compileKi)
import BenchmarkSources

loadTestCase :: SourceCode -> IO CL
Expand All @@ -20,16 +19,17 @@ loadTestCase src = do
expr = compile pEnv abstractToSKI
return expr

loadTestCaseKiselyov :: SourceCode -> IO CL
loadTestCaseKiselyov src = do
loadTestCaseBulk :: SourceCode -> IO CL
loadTestCaseBulk src = do
let pEnv = parseEnvironment src
expr = compileBulk pEnv
return expr

getInt :: Expr -> Integer
getInt (Int i) = i
getInt _ = error "not an int"

loadTestCaseEta :: SourceCode -> IO CL
loadTestCaseEta src = do
let pEnv = parseEnvironment src
expr = compileEta pEnv
return expr

graphTest :: CL -> String
graphTest expr =
Expand All @@ -49,24 +49,8 @@ reduceGraph graph = do
gP <- graph
normalForm gP

splitMain :: CL -> (CL, CL)
splitMain (expr :@ (INT x)) = (expr, INT x)
splitMain expr = error $ "invalid main expression " ++ show expr

reducerTest :: CL -> String
reducerTest (expr :@ (INT x)) =
let fun = transLink primitives expr
in show (CApp fun (CInt x))
reducerTest expr = error "invalid input expression " ++ show expr

runReducerTest :: CL -> CExpr -> String
runReducerTest expr arg =
let fun = transLink primitives expr
in show (CApp fun arg)

toCexpr :: CL -> CExpr
toCexpr (INT x) = CInt x
toCexpr (expr :@ arg) = CApp (toCexpr expr) (toCexpr arg)
reducerTest expr = show $ transLink primitives expr

benchmarks :: IO ()
benchmarks = do
Expand All @@ -75,43 +59,50 @@ benchmarks = do
akk <- loadTestCase ackermann
gau <- loadTestCase gaussian
tak <- loadTestCase tak
facKi <- loadTestCaseKiselyov factorial
fibKi <- loadTestCaseKiselyov fibonacci
akkKi <- loadTestCaseKiselyov ackermann
gauKi <- loadTestCaseKiselyov gaussian
takKi <- loadTestCaseKiselyov BenchmarkSources.tak

let (funFac, argFac) = splitMain fac
(funFib, argFib) = splitMain fib
(funAkk, argAkk) = splitMain akk
(funGau, argGau) = splitMain gau
(funTak, argTak) = splitMain tak
(funFacKi, argFacKi) = splitMain facKi
(funFibKi, argFibKi) = splitMain fibKi
(funAkkKi, argAkkKi) = splitMain akkKi
(funGauKi, argGauKi) = splitMain gauKi
(funTakKi, argTakKi) = splitMain takKi
facEta <- loadTestCaseEta factorial
fibEta <- loadTestCaseEta fibonacci
akkEta <- loadTestCaseEta ackermann
gauEta <- loadTestCaseEta gaussian
takEta <- loadTestCaseEta BenchmarkSources.tak
facBulk <- loadTestCaseBulk factorial
fibBulk <- loadTestCaseBulk fibonacci
akkBulk <- loadTestCaseBulk ackermann
gauBulk <- loadTestCaseBulk gaussian
takBulk <- loadTestCaseBulk BenchmarkSources.tak

-- sanity checks
print $ graphTest fac
print $ reducerTest fac
print $ reducerTest facEta
print $ reducerTest facBulk
print $ show $ fact 100

defaultMain [
bench "factorial Graph-Reduce" $ nf graphTest fac
, bench "factorial HHI-Reduce" $ nf (runReducerTest funFac) (toCexpr argFac)
, bench "factorial HHI-Kiselyov" $ nf (runReducerTest funFacKi) (toCexpr argFacKi)
, bench "factorial HHI-Reduce" $ nf reducerTest fac
, bench "factorial HHI-Eta" $ nf reducerTest facEta
, bench "factorial HHI-Bulk" $ nf reducerTest facBulk
, bench "factorial Native" $ nf fact 100
, bench "fibonacci Graph-Reduce" $ nf graphTest fib
, bench "fibonacci HHI-Reduce" $ nf reducerTest fib
, bench "fibonacci HHI-Kiselyov" $ nf reducerTest fibKi
, bench "fibonacci HHI-Eta" $ nf reducerTest fibEta
, bench "fibonacci HHi-Bulk" $ nf reducerTest fibBulk
, bench "fibonacci Native" $ nf fibo 10
, bench "ackermann Graph-Reduce" $ nf graphTest akk
, bench "ackermann HHI-Reduce" $ nf reducerTest akk
, bench "ackermann HHI-Kiselyov" $ nf reducerTest akkKi
, bench "ackermann HHI-Eta" $ nf reducerTest akkEta
, bench "ackermann HHI-Bulk" $ nf reducerTest akkBulk
, bench "ackermann Native" $ nf ack_2 2
, bench "gaussian Graph-Reduce" $ nf graphTest gau
, bench "gaussian HHI-Reduce" $ nf reducerTest gau
, bench "gaussian HHI-Kiselyov" $ nf reducerTest gauKi
, bench "gaussian HHI-Eta" $ nf reducerTest gauEta
, bench "gaussian HHI-Bulk" $ nf reducerTest gauBulk
, bench "gaussian Native" $ nf gaussianSum 100
, bench "tak Graph-Reduce" $ nf graphTest tak
, bench "tak HHI-Reduce" $ nf reducerTest tak
, bench "tak HHI-Kiselyov" $ nf reducerTest takKi
, bench "tak Native" $ nf tak2 (18,6,3) --tak_18_6 3
, bench "tak HHI-Eta" $ nf reducerTest takEta
, bench "tak HHI-Bulk" $ nf reducerTest takBulk
, bench "tak Native" $ nf tak1 (18,6,3)
]
return ()

Expand Down Expand Up @@ -145,8 +136,4 @@ takN = fix (\f x y z -> (if y >= x then z else f (f (x-1) y z) (f (y-1) z x) (f

tak1 (x,y,z) = takN x y z

tak2 :: (Integer, Integer, Integer) -> Integer
tak2 (x,y,z) = takInt x y z
where
takInt x y z = if y >= x then z else takInt (takInt (x-1) y z) (takInt (y-1) z x) (takInt (z-1) x y )

1 change: 1 addition & 0 deletions lambda-ski.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ executable lambda-ski-exe
, lambda-ski
, parsec
, raw-strings-qq
, timeit
default-language: GHC2021

test-suite lambda-ski-test
Expand Down
1 change: 1 addition & 0 deletions package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ executables:
- -with-rtsopts=-N
dependencies:
- lambda-ski
- timeit

benchmark:
main: Main.hs
Expand Down
65 changes: 9 additions & 56 deletions src/Kiselyov.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,10 @@
module Kiselyov
(
deBruijn,
--convert,
--plain,
--bulkPlain,
--breakBulkLinear,
breakBulkLog,
bulkOpt,
compileKi,
compileKiEither,
compileBulk,
compileEta,
optK,
optEta
)
Expand Down Expand Up @@ -40,38 +35,6 @@ deBruijn = go [] where
t `App` u -> A (go binds t) (go binds u)
Int i -> IN i

{--
convert :: ((Int, CL) -> (Int, CL) -> CL) -> DB -> (Int, CL)
convert (#) = \case
N Z -> (1, Com I)
N (Su e) -> (n + 1, (0, Com K) # t) where t@(n, _) = rec $ N e
L e -> case rec e of
(0, d) -> (0, Com K :@ d)
(n, d) -> (n - 1, d)
A e1 e2 -> (max n1 n2, t1 # t2) where
t1@(n1, _) = rec e1
t2@(n2, _) = rec e2
Free s -> (0, Com (fromString s))
IN i -> (0, INT i)
where rec = convert (#)
plain :: DB -> (Int, CL)
plain = convert (#) where
(0 , d1) # (0 , d2) = d1 :@ d2
(0 , d1) # (n , d2) = (0, Com B :@ d1) # (n - 1, d2)
(n , d1) # (0 , d2) = (0, Com R :@ d2) # (n - 1, d1)
(n1, d1) # (n2, d2) = (n1 - 1, (0, Com S) # (n1 - 1, d1)) # (n2 - 1, d2)
bulkPlain :: (Combinator -> Int -> CL) -> DB -> (Int, CL)
bulkPlain bulk = convert (#) where
(a, x) # (b, y) = case (a, b) of
(0, 0) -> x :@ y
(0, n) -> bulk B n :@ x :@ y
(n, 0) -> bulk C n :@ x :@ y
(n, m) | n == m -> bulk S n :@ x :@ y
| n < m -> bulk B (m - n) :@ (bulk S n :@ x) :@ y
| otherwise -> bulk C (n - m) :@ (bulk B (n - m) :@ bulk S m :@ x) :@ y
--}
bulk :: Combinator -> Int -> CL
bulk c 1 = Com c
bulk c n = Com $ BulkCom (show c) n
Expand All @@ -81,9 +44,9 @@ compileKiEither env convertFun = case lookup "main" env of
Nothing -> Left $ error "main function missing in " ++ show env
Just main -> Right $ snd $ convertFun env $ deBruijn main

compileKi :: Environment -> (Environment -> DB -> ([Bool],CL)) -> CL
compileKi env convertFun =
case compileKiEither env convertFun of
compileEta :: Environment -> CL
compileEta env =
case compileKiEither env optEta of
Left err -> error $ show err
Right cl -> cl

Expand Down Expand Up @@ -145,26 +108,14 @@ zipWithDefault d f [] ys = f d <$> ys
zipWithDefault d f xs [] = flip f d <$> xs
zipWithDefault d f (x:xt) (y:yt) = f x y : zipWithDefault d f xt yt


-- breakBulkLinear :: Combinator -> Int -> CL
-- breakBulkLinear B n = iterate (comB' :@) (Com B) !! (n - 1)
-- breakBulkLinear C n = iterate (comC' :@) (Com C) !! (n - 1)
-- breakBulkLinear S n = iterate (comS' :@) (Com S) !! (n - 1)

-- comB' :: CL
-- comB' = Com B:@ Com B
-- comC' :: CL
-- comC' = Com B :@ (Com B :@ Com C) :@ Com B
-- comS' :: CL
-- comS' = Com B :@ (Com B :@ Com S) :@ Com B

bits :: Integral t => t -> [t]
bits n = r:if q == 0 then [] else bits q where (q, r) = divMod n 2

breakBulkLog :: Combinator -> Int -> CL
breakBulkLog c 1 = Com c
breakBulkLog B n = foldr (((:@)) . (bs!!)) (Com B) (init $ bits n) where
breakBulkLog B n = foldr ((:@) . (bs!!)) (Com B) (init $ bits n) where
bs = [sbi, Com B :@ (Com B :@ Com B) :@ sbi]
breakBulkLog c n = (foldr (:@) (prime c) $ map (bs!!) $ init $ bits n) :@ Com I where
breakBulkLog c n = foldr ((:@) . (bs!!)) (prime c) (init $ bits n) :@ Com I where
bs = [sbi, Com B :@ (Com B :@ prime c) :@ sbi]
prime c = Com B :@ (Com B :@ Com c) :@ Com B

Expand Down Expand Up @@ -221,7 +172,9 @@ bulkOpt bulk env = \case
pre = first (replicate count (uncurry (||) h) ++)
apply s = (([], bulk s count) ##)

first :: (t -> a) -> (t, b) -> (a, b)
first f (x, y) = (f x, y);

headGroup :: Eq a => [a] -> (a, Int)
headGroup (h:t) = (h, 1 + length (takeWhile (== h) t))

58 changes: 30 additions & 28 deletions test/ReducerKiselyovSpec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,37 +15,39 @@ main = hspec spec

spec :: Spec
spec =
describe "hhi inspired Reducer (Kiselyov compiler)" $ do
it "computes factorial" $
verify factorial
it "computes fibonacci" $
verify fibonacci
it "computes gaussian sum" $
verify gaussian
it "computes ackermann function" $
verify ackermann
it "computes tak " $
verify tak
describe "hhi inspired Reducer (Kiselyov Abstraction)" $ do
it "computes factorial Opt Eta" $
verify factorial compileEta
it "computes fibonacci Opt Eta" $
verify fibonacci compileEta
it "computes gaussian sum Opt Eta" $
verify gaussian compileEta
it "computes ackermann function Opt Eta" $
verify ackermann compileEta
it "computes tak Opt Eta" $
verify tak compileEta
it "computes factorial BulkOpt" $
verify factorial compileBulk
it "computes fibonacci BulkOpt" $
verify fibonacci compileBulk
it "computes gaussian sum BulkOpt" $
verify gaussian compileBulk
it "computes ackermann function BulkOpt" $
verify ackermann compileBulk
it "computes tak BulkOpt" $
verify tak compileBulk

verify :: SourceCode -> IO ()
verify src = do
--showCode src
src `shouldSatisfy` runTest
verify :: SourceCode -> (Environment -> CL) -> IO ()
verify src compileFun = do
src `shouldSatisfy` runTest compileFun

showCode :: SourceCode -> IO ()
showCode src = do
runTest :: (Environment -> CL) -> SourceCode -> Bool
runTest compileFun src =
let pEnv = parseEnvironment src
aExp = compileBulk pEnv
putStrLn "The source: "
putStrLn src
putStrLn "The result of the kiselyov compiler:"
print aExp

runTest :: SourceCode -> Bool
runTest src =
let pEnv = parseEnvironment src
aExp = compileBulk pEnv
aExp = compileFun pEnv
tExp = translate aExp
expected = translate $ toCL $ fromJust (lookup "expected" pEnv)
actual = link primitives tExp
in show expected == show actual
actual' = transLink primitives aExp
in show expected == show actual
&& show expected == show actual'
2 changes: 1 addition & 1 deletion test/TestSources.hs
Original file line number Diff line number Diff line change
Expand Up @@ -37,5 +37,5 @@ tak :: SourceCode
tak = [r|
expected = 4
tak = y(λf x y z -> (if (geq y x) z (f (f (sub1 x) y z) (f (sub1 y) z x) (f (sub1 z) x y ))))
main = tak 18 6 3
main = tak 7 4 2 --18 6 3
|]

0 comments on commit 1512685

Please sign in to comment.