print out all optimizations

thma · thma · commit ba94efd6736f · 2023-09-17T11:15:17.000+02:00
diff --git a/app/Main.hs b/app/Main.hs
@@ -17,6 +17,7 @@ import Kiselyov
 import System.TimeIt
 import Text.RawString.QQ  
 
+
 printGraph :: ST s (STRef s (Graph s)) -> ST s String
 printGraph graph = do
   gP <- graph
@@ -32,54 +33,66 @@ main = do
   hSetEncoding stdin utf8 -- this is required to handle UTF-8 characters like λ
   hSetEncoding stdout utf8 -- this is required to handle UTF-8 characters like λ
 
-  -- testSource <-readFile "test/tak.ths"
-  let testSource = "main = (\\x y -> + x x) 3 4"
-  putStrLn "The sourcecode: "
-  putStrLn testSource
+  --let testSource = "main = (\\x y -> + x x) 3 4"
+  mapM_ showCompilations [factorial, fibonacci, ackermann, tak]
+  --demo
 
-  let env = parseEnvironment testSource
+type SourceCode = String
+tak :: SourceCode
+tak = [r| 
+  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 7 4 2 --18 6 3
+|]
+
+ackermann :: SourceCode 
+ackermann = [r|
+  ack  = y(λf n m -> if (is0 n) (+ m 1) (if (is0 m) (f (sub1 n) 1) (f (sub1 n) (f n (sub1 m)))))
+  main = ack 2 2
+|]
+
+factorial :: SourceCode
+factorial = [r| 
+  fact = y(λf n -> if (is0 n) 1 (* n (f (sub1 n))))
+  main = fact 100
+|]
+
+fibonacci :: SourceCode
+fibonacci = [r| 
+  fib  = y(λf n -> if (is0 n) 1 (if (eql n 1) 1 (+ (f (sub1 n)) (f (sub n 2)))))
+  main = fib 10
+|]
+
+showCompilations :: SourceCode -> IO ()
+showCompilations source = do
+  let env = parseEnvironment source
   putStrLn "The parsed environment of named lambda expressions:"
   mapM_ print env
   putStrLn ""
 
   let expr = compile env abstractToSKI
-  putStrLn "The main expression compiled to SICKYB combinator expressions:"
+  putStrLn "The main expression compiled to SICKBY combinator expressions:"
   print expr
   putStrLn ""
 
-  let graph = allocate expr
-  putStrLn "The allocated graph:"
-  putStrLn $ runST $ printGraph graph
-
-  let reducedGraph = reduceGraph graph
-
-  putStrLn "The result after reducing the graph:"
-  putStrLn $ runST $ printGraph reducedGraph
-
+  let expr' = compileEta env
+  putStrLn "The main expression compiled to SICKBY combinator expressions with eta optimization:"
+  print expr'
+  putStrLn ""
 
-  --demo
+  let expr'' = compileBulk env
+  putStrLn "The main expression compiled to SICKBY combinator expressions with bulk combinators:"
+  print expr''
+  putStrLn ""
 
-type SourceCode = String
+  let expr''' = compileBulkLinear env
+  putStrLn "The main expression compiled to SICKBY combinator expressions with bulk combinators and linear elimination:"
+  print expr'''
+  putStrLn ""
 
-loadTestCase :: String -> IO CL
-loadTestCase name = do
-  src <- readFile $ "test/" ++ name ++ ".ths"
-  putStrLn "The source: "
-  putStrLn src
-  let pEnv = parseEnvironment src
-      expr = compile pEnv abstractToSKI
-  return expr
-
-graphReductionDemo :: IO CL -> IO ()
-graphReductionDemo ioexpr = do
-  expr <- ioexpr
-  let graph = allocate expr      
-      result = reduceGraph graph
-      actual = runST $ printGraph result
-  putStrLn "allocated graph:"
-  print expr
-  putStrLn "after graph reduction:"
-  print actual
+  let expr'''' = compileBulkLog env
+  putStrLn "The main expression compiled to SICKBY combinator expressions with bulk combinators and logarithmic elimination:"
+  print expr''''
+  putStrLn ""
 
 
 hhiReductionDemo :: IO CL -> IO ()
@@ -91,18 +104,4 @@ hhiReductionDemo ioexpr = do
   putStrLn "after graph reduction:"
   print actual
 
-demo :: IO ()
-demo = do
-  let testCases =
-       [
-         "factorial"
-       , "fibonacci"
-       , "tak"
-       , "ackermann"
-       , "gaussian"
-       ]
-  putStrLn "Graph-Reduction"
-  mapM_ (loadTestCase >>> graphReductionDemo) testCases
-
-  putStrLn "HHI Reduction"
-  mapM_ (loadTestCase >>> hhiReductionDemo) testCases
+
diff --git a/src/HhiReducer.hs b/src/HhiReducer.hs
@@ -1,12 +1,12 @@
 module HhiReducer where
 
-import Parser ( Expr(..) ) 
+import Parser ( Expr(..) )
 import Control.Monad.Fix (fix)
-import CLTerm 
+import CLTerm
 import Data.Maybe (fromJust)
 
 -- | a compiled expression
-data CExpr = 
+data CExpr =
     CComb Combinator
   | CApp CExpr CExpr
   | CFun (CExpr -> CExpr)
@@ -73,8 +73,8 @@ primitives = let (-->) = (,) in
   , S      --> comS --CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!(g!x)) -- S F G X = F X (G X)
   , B      --> comB --CFun (\f -> CFun $ \g -> CFun $ \x -> f!(g!x))   -- B F G X = F (G X)
   , C      --> comC --CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!g)     -- C F G X = F X G
-  , R      --> CFun (\f -> CFun $ \g -> CFun $ \x -> g!x!f)     -- R F G X = G X F  
- -- , T      --> CFun (\x -> CFun $ \y -> x)                    -- T X Y = X
+  , R      --> CFun (\f -> CFun $ \g -> CFun $ \x -> g!x!f)            -- R F G X = G X F  
+  , T      --> CFun (CFun . const)                                     -- T X Y = X
   , B'     --> comB' --CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!q!(r!s))      -- B' P Q R S = P Q (R S)
   , C'     --> comC' --CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!(q!s)!r)      -- C' P Q R S = P (Q S) R
   , S'     --> comS' --CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!(q!s)!(r!s))  -- S' P Q R S = P (Q S) (R S)
@@ -108,39 +108,30 @@ resolveBulkLog (BulkCom c n) = breakBulkLog (fromString c) n
     bits n = r:if q == 0 then [] else bits q where (q, r) = divMod n 2
 
 resolveBulk :: Combinator -> CExpr
-resolveBulk (BulkCom "B" n) = iterate (comB' !) comB !! (n-1) 
+resolveBulk (BulkCom "B" n) = iterate (comB' !) comB !! (n-1)
 resolveBulk (BulkCom "C" n) = iterate (comC' !) comC !! (n-1)
-resolveBulk (BulkCom "S" n) = iterate (comS' !) comS !! (n-1) 
+resolveBulk (BulkCom "S" n) = iterate (comS' !) comS !! (n-1)
 resolveBulk anyOther = error $ "not a known combinator: " ++ show anyOther
 
 comI :: CExpr
 comI = CFun id
 
 comS :: CExpr
-comS = CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!(g!x)) -- S F G X = F X (G X)
+comS = CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!(g!x))                    -- S F G X = F X (G X)
 
 comS' :: CExpr
 comS' = CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!(q!s)!(r!s))  -- S' P Q R S = P (Q S) (R S)
 
-comS2 :: CExpr
-comS2 = comS' ! comS
-
-comS3 = comS' ! comS2
-comS4 = comS' ! comS3
-
-comB = CFun (\f -> CFun $ \g -> CFun $ \x -> f!(g!x))   -- B F G X = F (G X)
+comB :: CExpr
+comB = CFun (\f -> CFun $ \g -> CFun $ \x -> f!(g!x))                      -- B F G X = F (G X)
+comB' :: CExpr
 comB' = CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!q!(r!s))      -- B' P Q R S = P Q (R S)
 
-comB2 = comB' ! comB
-comB3 = comB' ! comB2
-
-comC = CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!g)     -- C F G X = F X G
+comC :: CExpr
+comC = CFun (\f -> CFun $ \g -> CFun $ \x -> f!x!g)                        -- C F G X = F X G
+comC' :: CExpr
 comC' = CFun (\p -> CFun $ \q -> CFun $ \r -> CFun $ \s -> p!(q!s)!r)      -- C' P Q R S = P (Q S) R
 
-comC2 = comC' ! comC
-comC3 = comC' ! comC2
-
-
 arith :: (Integer -> Integer -> Integer) -> CExpr
 arith op = CFun $ \(CInt a) -> CFun $ \(CInt b) -> CInt (op a b)
 
diff --git a/src/Kiselyov.hs b/src/Kiselyov.hs
@@ -3,9 +3,10 @@ module Kiselyov
   (
     deBruijn,
     bulkOpt,
-    --compileKiEither,
     compileBulk,
     compileEta,
+    compileBulkLinear,
+    compileBulkLog,
     optK,
     optEta
   )
@@ -39,11 +40,6 @@ bulk :: Combinator -> Int -> CL
 bulk c 1 = Com c
 bulk c n = Com $ BulkCom (show c) n
 
--- compileKiEither :: Environment -> (Environment -> DB -> ([Bool],CL)) -> Either String CL
--- 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
-
 compileEta :: Environment -> CL
 compileEta env = case lookup "main" env of
   Nothing   -> error "main function missing"
@@ -54,6 +50,16 @@ compileBulk env = case lookup "main" env of
   Nothing   -> error "main function missing"
   Just main -> snd $ bulkOpt bulk env (deBruijn main)
 
+compileBulkLinear :: Environment -> CL
+compileBulkLinear env = case lookup "main" env of
+  Nothing   -> error "main function missing"
+  Just main -> snd $ bulkOpt breakBulkLinear env (deBruijn main)  
+
+compileBulkLog :: Environment -> CL
+compileBulkLog env = case lookup "main" env of
+  Nothing   -> error "main function missing"
+  Just main -> snd $ bulkOpt breakBulkLog env (deBruijn main)  
+
 convertBool :: (([Bool], CL) -> ([Bool], CL) -> CL) -> Environment -> DB -> ([Bool], CL)
 convertBool (#) env = \case
   N Z -> (True:[], Com I)
@@ -107,45 +113,45 @@ 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
 
-bulkLookup :: String -> Environment -> ([Bool], CL)
-bulkLookup s env = case lookup s env of
+bulkLookup :: String -> Environment -> (Combinator -> Int -> CL) -> ([Bool], CL)
+bulkLookup s env bulkFun = case lookup s env of
   Nothing -> ([], Com (fromString s))
-  Just t -> bulkOpt bulk env (deBruijn t)
+  Just t -> bulkOpt bulkFun env (deBruijn t)
 
 bulkOpt :: (Combinator -> Int -> CL) -> Environment -> DB -> ([Bool], CL)
-bulkOpt bulk env = \case
+bulkOpt bulkFun env = \case
   N Z -> ([True], Com I)
   N (Su e) -> first (False:) $ rec env $ N e
   L e -> case rec env e of
     ([], d) -> ([], Com K :@ d)
     (False:g, d) -> ([], Com K) ## (g, d)
     (True:g, d) -> (g, d)
   A e1 e2 -> rec env e1 ## rec env e2
-  Free s -> bulkLookup s env --([], Com s)
+  Free s -> bulkLookup s env bulkFun--([], Com s)
   IN i -> ([False], INT i)
   where
-  rec = bulkOpt bulk
+  rec = bulkOpt bulkFun
   ([], d1) ## ([], d2) = ([], d1 :@ d2)
   ([], d1) ## ([True], Com I) = ([True], d1)
-  ([], d1) ## (g2, Com I) | and g2 = (g2, bulk B (length g2 - 1) :@ d1)
+  ([], d1) ## (g2, Com I) | and g2 = (g2, bulkFun B (length g2 - 1) :@ d1)
   ([], d1) ## (g2@(h:_), d2) = first (pre++) $ ([], fun1 d1) ## (post, d2)
     where
     fun1 = case h of
-      True -> (bulk B (length pre) :@)
+      True -> (bulkFun B (length pre) :@)
       False -> id
     (pre, post) = span (h ==) g2
 
   ([True], Com I) ## ([], d2) = ([True], Com T :@ d2)
   (g1@(h:_), d1) ## ([], d2) = first (pre++) $ case h of
-    True -> ([], Com C :@ bulk C (length pre) :@ d2) ## (post, d1)
+    True -> ([], Com C :@ bulkFun C (length pre) :@ d2) ## (post, d1)
     False -> (post, d1) ## ([], d2)
     where
     (pre, post) = span (h ==) g1
 
   ([True], Com I) ## (False:g2, d2) = first (True:) $ ([], Com T) ## (g2, d2)
   (False:g1, d1) ## ([True], Com I) = (True:g1, d1)
   (g1, d1) ## (g2, Com I) | and g2, let n = length g2, all not $ take n g1 =
-    first (g2++) $ ([], bulk B $ n - 1) ## (drop n g1, d1)
+    first (g2++) $ ([], bulkFun B $ n - 1) ## (drop n g1, d1)
   (g1, d1) ## (g2, d2) = pre $ fun1 (drop count g1, d1) ## (drop count g2, d2)
     where
     (h, count) = headGroup $ zip g1 g2
@@ -155,11 +161,38 @@ bulkOpt bulk env = \case
       (True, False) -> apply C
       (True, True) -> apply S
     pre = first (replicate count (uncurry (||) h) ++)
-    apply s = (([], bulk s count) ##)
+    apply s = (([], bulkFun 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))
 
+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
+
+
+
+breakBulkLog :: Combinator -> Int -> CL
+breakBulkLog c 1 = Com c
+breakBulkLog B n = foldr (:@) (Com B) $ map (bs!!) $ 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
+  bs = [sbi, Com B :@ (Com B :@ prime c) :@ sbi]
+  prime c = Com B :@ (Com B :@ Com c) :@ Com B
+
+bits :: Int -> [Int]
+bits n = r:if q == 0 then [] else bits q where (q, r) = divMod n 2
+
+sbi :: CL
+sbi = Com S :@ Com B :@ Com I
