From 4770300abffe2ed97d51ea0e8a8a4993aa113caf Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Tue, 19 Nov 2024 16:40:33 -0300 Subject: [PATCH] stuff --- .gitignore | 1 + book/church_mul.hvml | 57 ++++++ book/pseudo_metavar_bin.hvml | 312 +++++++++++++++++++++++++++++-- book/pseudo_metavar_factors.hs | 88 +++++++++ book/pseudo_metavar_factors.hvml | 139 ++++++++++++++ src/HVML/Collapse.hs | 3 +- src/HVML/Main.hs | 7 +- 7 files changed, 587 insertions(+), 20 deletions(-) create mode 100644 book/church_mul.hvml create mode 100644 book/pseudo_metavar_factors.hs create mode 100644 book/pseudo_metavar_factors.hvml diff --git a/.gitignore b/.gitignore index b29e6ad..ded4d2f 100644 --- a/.gitignore +++ b/.gitignore @@ -18,4 +18,5 @@ cabal.sandbox.config .sys.txt .out.hvm tmp/ +TIMES/ .main* diff --git a/book/church_mul.hvml b/book/church_mul.hvml new file mode 100644 index 0000000..955cac0 --- /dev/null +++ b/book/church_mul.hvml @@ -0,0 +1,57 @@ +@main = + !c2_0 = λf !&0{f0 f1}=f λx(f0 (f1 x)) + !c2_1 = λf !&1{f0 f1}=f λx(f0 (f1 x)) + (c2_0 c2_1) + +//data T { #T{x y z} } + +//@main = #T{(+ 1 1) (+ 1 1) (+ 7 7)} + +//@main = 12 + +//@main = λt(t &0{(+ 5 5) 2} &0{* 20}) + + + +//#Pair{ &0{* 2} &0{λ$x(+ 5 5) $x} } + + +//@main = #Pair{* 5} + +//@main = λt(t &0{&0{1 2} &0{3 4}}) + +//@main = λt(t (+ 1 2) (+ 3 4)) + +//@main = λt(t &0{1 2}) + +//@main = + //!f = λx λt (t λx(x) x) + //(f 7) + + +//! 0x34 {f g} = a +//! 0x44 {c d} = 0x42 (f 0x54 (g {d e})) +//#0x9 λa #0x2B λb c + +//Collapsing term: term_new(LAM,0x000000,0x000000009) (at 0x0) +//Current paths: fromList [] +//Collapsing term: term_new(LAM,0x000000,0x00000002b) (at 0xa) +//Current paths: fromList [] +//Collapsing term: term_new(DP0,0x000001,0x000000044) (at 0x2c) +//Current paths: fromList [] +//Collapsing term: term_new(APP,0x000000,0x000000042) (at 0x46) +//Current paths: fromList [(1,[0])] +//Collapsing term: term_new(DP0,0x000001,0x000000034) (at 0x42) +//Current paths: fromList [(1,[0])] +//Collapsing term: term_new(VAR,0x000000,0x000000009) (at 0x36) +//Current paths: fromList [(1,[0,0])] +//Collapsing term: term_new(APP,0x000000,0x000000054) (at 0x43) +//Current paths: fromList [(1,[0,0])] +//Collapsing term: term_new(DP1,0x000001,0x000000034) (at 0x54) +//Current paths: fromList [(1,[0,0])] +//Collapsing term: term_new(VAR,0x000000,0x000000009) (at 0x36) +//Current paths: fromList [(1,[1,0,0])] +//Collapsing term: term_new(SUP,0x000001,0x00000004b) (at 0x55) +//Current paths: fromList [(1,[1,0,0])] +//Collapsing term: term_new(VAR,0x000000,0x000000049) (at 0x4c) +//Current paths: fromList [(1,[0,0])] diff --git a/book/pseudo_metavar_bin.hvml b/book/pseudo_metavar_bin.hvml index 0c50616..dd70b79 100644 --- a/book/pseudo_metavar_bin.hvml +++ b/book/pseudo_metavar_bin.hvml @@ -1,15 +1,33 @@ -// This shows how to use a 'pseudo-metavar' to invert the binary add function, -// and solve the equation: 'X + 1234560 = 1234567'. Run it with collapse mode: -// $ hvml run pseudo_metavar_nat.hvml -C -s - +// Bitstrings data Bin { #O{pred} #I{pred} #E } +// Pairs +data Pair { #Pair{fst snd} } + // If-Then-Else @if(b t f) = ~b { 0: f k: t } +// Not +@not(a) = ~a { + 0: 1 + _: 0 +} + +// And +@and(a b) = ~a { + 0: 0 + _: b +} + +// Or +@or(a b) = ~a { + 0: b + _: 1 +} + // Converts a Bin to an U32 @u32(b) = ~b{ #O: λp (+ (* 2 @u32(p)) 0) @@ -28,9 +46,21 @@ data Bin { #O{pred} #I{pred} #E } // Bin Equality @eq(a b) = ~a{ - #E: ~b { #O: λ_ 0 #I: λ_ 0 #E: 1 } - #O: λap ~b{ #O: λbp @eq(ap bp) #I: λ_ 0 #E: 0 } - #I: λap ~b{ #O: λ_ 0 #I: λbp @eq(ap bp) #E: 0 } + #E: ~b { + #O: λ_ 0 + #I: λ_ 0 + #E: 1 + } + #O: λap ~b{ + #O: λbp @eq(ap bp) + #I: λ_ 0 + #E: 0 + } + #I: λap ~b{ + #O: λ_ 0 + #I: λbp @eq(ap bp) + #E: 0 + } } // Increments a Bin @@ -40,30 +70,278 @@ data Bin { #O{pred} #I{pred} #E } #E: #E } +// Decrements a Bin +@dec(a) = ~a{ + #O: λp #O{@dec(p)} + #I: λp #I{p} + #E: #E +} + // Adds two Bins @add(a b) = ~a { #O: λap ~b { #O: λbp #O{@add(ap bp)} #I: λbp #I{@add(ap bp)} - #E: #E + #E: #O{ap} } #I: λap ~b { #O: λbp #I{@add(ap bp)} #I: λbp #O{@inc(@add(ap bp))} - #E: #E + #E: #I{ap} } #E: #E } -// Enumerates all Bins of given size -@all(s) = ~s{ +// Muls two Bins +@mul(a b) = ~b { + #E: #E + #O: λbp #O{@mul(a bp)} + #I: λbp !&0{a0 a1}=a @add(a0 #O{@mul(a1 bp)}) +} + +// Concatenates two Bins +@cat(a b) = ~a { + #O: λap #O{@cat(ap b)} + #I: λap #I{@cat(ap b)} + #E: b +} + +// Lt two Bins (a < b) +@lt(a b) = @lt_go(0 a b) + +@lt_go(k a b) = ~a { + #E: ~b { + #E: k + #O: λ_ 1 + #I: λ_ 1 + } + #O: λap ~b { + #E: 0 + #O: λbp @lt_go(k ap bp) + #I: λbp @lt_go(1 ap bp) + } + #I: λap ~b { + #E: 0 + #O: λbp @lt_go(0 ap bp) + #I: λbp @lt_go(k ap bp) + } +} + +// Take the first N bits of a Bin +@take(n b) = ~n { 0: #E - p: !&0{p0 p1}=p &0{#O{@all(p0)} #I{@all(p1)}} + p: ~b { + #O: λbp #O{@take(p bp)} + #I: λbp #I{@take(p bp)} + #E: #E + } } -@S = 64 -@X = @all(@S) +// Enums all Bins of given size (label 1) +@all1(s) = ~s{ + 0: #E + p: !&1{p0 p1}=p + &1{ + #O{@all1(p0)} + #I{@all1(p1)} + } +} + +// Enums all Bins of given size (label 2) +@all2(s) = ~s{ + 0: #E + p: !&2{p0 p1}=p &2{ + #O{@all2(p0)} + #I{@all2(p1)} + } +} + +//// 4: +//@K = 1 +//@H = 2 +//@S = 4 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 3) @bin(@H 0)) +//@B = @cat(@bin(@H 3) @bin(@H 0)) +//@P = @bin(@S 9) + +//// 6: +//@K = 2 +//@H = 3 +//@S = 6 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 5) @bin(@H 0)) +//@B = @cat(@bin(@H 5) @bin(@H 0)) +//@P = @bin(@S 25) + +//// 8: +//@K = 3 +//@H = 4 +//@S = 8 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 13) @bin(@H 0)) +//@B = @cat(@bin(@H 13) @bin(@H 0)) +//@P = @bin(@S 169) + +//// 10: +//@K = 4 +//@H = 5 +//@S = 10 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 31) @bin(@H 0)) +//@B = @cat(@bin(@H 19) @bin(@H 0)) +//@P = @bin(@S 589) + +//// 12: +//@K = 5 +//@H = 6 +//@S = 12 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 53) @bin(@H 0)) +//@B = @cat(@bin(@H 37) @bin(@H 0)) +//@P = @bin(@S 1961) + +//// 14: +//@K = 6 +//@H = 7 +//@S = 14 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 109) @bin(@H 0)) +//@B = @cat(@bin(@H 97) @bin(@H 0)) +//@P = @bin(@S 10573) + +//// 16: +//@K = 7 +//@H = 8 +//@S = 16 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 173) @bin(@H 0)) +//@B = @cat(@bin(@H 233) @bin(@H 0)) +//@P = @bin(@S 40309) + +//// 18: +//@K = 8 +//@H = 9 +//@S = 18 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 449) @bin(@H 0)) +//@B = @cat(@bin(@H 389) @bin(@H 0)) +//@P = @bin(@S 174661) + +//// 20: +//@K = 9 +//@H = 10 +//@S = 20 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 769) @bin(@H 0)) +//@B = @cat(@bin(@H 569) @bin(@H 0)) +//@P = @bin(@S 437561) + +//// 22: +//@K = 10 +//@H = 11 +//@S = 22 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 1423) @bin(@H 0)) +//@B = @cat(@bin(@H 1229) @bin(@H 0)) +//@P = @bin(@S 1748867) + +//// 24: +//@K = 11 +//@H = 12 +//@S = 24 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 2437) @bin(@H 0)) +//@B = @cat(@bin(@H 2333) @bin(@H 0)) +//@P = @bin(@S 5685521) + +//// 26: +//@K = 12 +//@H = 13 +//@S = 26 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 4987) @bin(@H 0)) +//@B = @cat(@bin(@H 6203) @bin(@H 0)) +//@P = @bin(@S 30934361) + +//// 28: +//@K = 13 +//@H = 14 +//@S = 28 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 13513) @bin(@H 0)) +//@B = @cat(@bin(@H 13721) @bin(@H 0)) +//@P = @bin(@S 185411873) + +//// 30: +//@K = 14 +//@H = 15 +//@S = 30 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@A = @cat(@bin(@K 24923) @bin(@H 0)) +//@B = @cat(@bin(@H 19489) @bin(@H 0)) +//@P = @bin(@S 485724347) + +// 32: +@K = 15 +@H = 16 +@S = 32 +@X = @cat(@all1(@H) @bin(@H 0)) +@Y = @cat(@all2(@H) @bin(@H 0)) +@A = @cat(@bin(@K 47791) @bin(@H 0)) +@B = @cat(@bin(@H 54881) @bin(@H 0)) +@P = @bin(@S 2622817871) + +// 21536832 +//4294967296 + +@main = + ! cond = @eq(@mul(@X @Y) @P) + ! not1 = @not(@eq(@X @bin(@S 1))) + @if(@and(cond not1) λt(t @u32(@X) @u32(@Y)) *) + + //λt(t @u32(@X) @u32(@mul(@X @B))) + +// Solve: X * Y = P mod 2^32 +//@main = + //! solved = @eq(@mul(@X @Y) @P) + //@if(solved λt(t (@X) (@Y)) *) + +//@main = @lt(@bin(32 155) @bin(32 155)) + +//@main = @u32(@mul(@bin(32 1234) @bin(32 4321))) + + + + +// printing all solutions +// 4 bits -> 23416 itrs ~ +// 8 bits -> 137738 itrs ~ 538 +// 9 bits -> 334663 itrs ~ 653 +// 10 bits -> 813044 itrs ~ 793 +// 11 bits -> 2002681 itrs ~ 977 +// 12 bits -> 4799018 itrs ~ 1171 +// 16 bits -> 138896024 itrs ~ 2119 + +// 8 bits -> 3813 itrs +// 16 bits -> 26944 itrs +// 32 bits -> 250514 itrs +// 64 bits -> 2652646 itrs +// 128 bits -> 31219719 itrs (1 second) +// 256 bits -> 430236928 itrs (10 seconds) -@main = - ! ok = @eq(@add(@X @bin(@S 1234560)) @bin(@S 1234567)) - @if(ok @u32(@X) *) +//2048 bits -> diff --git a/book/pseudo_metavar_factors.hs b/book/pseudo_metavar_factors.hs new file mode 100644 index 0000000..368f77f --- /dev/null +++ b/book/pseudo_metavar_factors.hs @@ -0,0 +1,88 @@ +import Control.Monad (forM_, when) +import Data.Time.Clock (getCurrentTime, diffUTCTime) +import System.Exit (exitSuccess) +import Text.Printf (printf) + +data Bin = O Bin | I Bin | E deriving (Show, Eq) + +if' :: Bool -> a -> a -> a +if' True t _ = t +if' False _ f = f + +not' :: Bool -> Bool +not' False = True +not' _ = False + +and' :: Bool -> Bool -> Bool +and' False _ = False +and' _ b = b + +or' :: Bool -> Bool -> Bool +or' False b = b +or' _ _ = True + +u32 :: Bin -> Int +u32 (O p) = 2 * u32 p + 0 +u32 (I p) = 2 * u32 p + 1 +u32 E = 0 + +bin :: Int -> Int -> Bin +bin 0 _ = E +bin s n = case n `mod` 2 of + 0 -> O (bin (s-1) (n `div` 2)) + _ -> I (bin (s-1) (n `div` 2)) + +eq :: Bin -> Bin -> Bool +eq E E = True +eq (O a) (O b) = eq a b +eq (I a) (I b) = eq a b +eq _ _ = False + +inc :: Bin -> Bin +inc (O p) = I p +inc (I p) = O (inc p) +inc E = E + +dec :: Bin -> Bin +dec (O p) = I (dec p) +dec (I p) = O p +dec E = E + +add :: Bin -> Bin -> Bin +add (O a) (O b) = O (add a b) +add (O a) (I b) = I (add a b) +add (I a) (O b) = I (add a b) +add (I a) (I b) = O (inc (add a b)) +add E b = E +add a E = E + +mul :: Bin -> Bin -> Bin +mul _ E = E +mul a (O b) = O (mul a b) +mul a (I b) = add a (O (mul a b)) + +cat :: Bin -> Bin -> Bin +cat (O a) b = O (cat a b) +cat (I a) b = I (cat a b) +cat E b = b + +k = 14 +h = 15 +s = 30 +p = I(I(I(O(O(O(I(I(O(I(O(I(O(O(O(O(I(O(I(I(O(O(I(O(O(I(O(I(O(I(E)))))))))))))))))))))))))))))) + +--INJECT-- + +main :: IO () +main = do + start <- getCurrentTime + forM_ [0..2^h-1] $ \a -> do + forM_ [0..2^h-1] $ \b -> do + let binA = cat (bin h a) (bin h 0) + let binB = cat (bin h b) (bin h 0) + when (eq (mul binA binB) p) $ do + end <- getCurrentTime + let duration = diffUTCTime end start + putStrLn $ "FACT: " ++ show a ++ " " ++ show b + putStrLn $ "TIME: " ++ printf "%.7f seconds" (realToFrac duration :: Double) + exitSuccess diff --git a/book/pseudo_metavar_factors.hvml b/book/pseudo_metavar_factors.hvml new file mode 100644 index 0000000..62b70d0 --- /dev/null +++ b/book/pseudo_metavar_factors.hvml @@ -0,0 +1,139 @@ +// Bitstrings +data Bin { #O{pred} #I{pred} #E } + +// If-Then-Else +@if(b t f) = ~b { + 0: f + k: t +} + +// Not +@not(a) = ~a { + 0: 1 + _: 0 +} + +// And +@and(a b) = ~a { + 0: 0 + _: b +} + +// Or +@or(a b) = ~a { + 0: b + _: 1 +} + +// Converts a Bin to an U32 +@u32(b) = ~b{ + #O: λp (+ (* 2 @u32(p)) 0) + #I: λp (+ (* 2 @u32(p)) 1) + #E: 0 +} + +// Converts an U32 to a Bin of given size +@bin(s n) = ~s{ + 0: #E + p: !&0{n0 n1}=n ~(% n0 2) { + 0: #O{@bin(p (/ n1 2))} + k: #I{@bin(p (/ n1 2))} + } +} + +// Bin Equality +@eq(a b) = ~a{ + #E: ~b { + #O: λ_ 0 + #I: λ_ 0 + #E: 1 + } + #O: λap ~b{ + #O: λbp @eq(ap bp) + #I: λ_ 0 + #E: 0 + } + #I: λap ~b{ + #O: λ_ 0 + #I: λbp @eq(ap bp) + #E: 0 + } +} + +// Increments a Bin +@inc(a) = ~a{ + #O: λp #I{p} + #I: λp #O{@inc(p)} + #E: #E +} + +// Decrements a Bin +@dec(a) = ~a{ + #O: λp #O{@dec(p)} + #I: λp #I{p} + #E: #E +} + +// Adds two Bins +@add(a b) = ~a { + #O: λap ~b { + #O: λbp #O{@add(ap bp)} + #I: λbp #I{@add(ap bp)} + #E: #E + } + #I: λap ~b { + #O: λbp #I{@add(ap bp)} + #I: λbp #O{@inc(@add(ap bp))} + #E: #E + } + #E: #E +} + +// Muls two Bins +@mul(a b) = ~b { + #E: #E + #O: λbp #O{@mul(a bp)} + #I: λbp !&0{a0 a1}=a @add(a0 #O{@mul(a1 bp)}) +} + +// Concatenates two Bins +@cat(a b) = ~a { + #O: λap #O{@cat(ap b)} + #I: λap #I{@cat(ap b)} + #E: b +} + +// Enums all Bins of given size (label 1) +@all1(s) = ~s{ + 0: #E + p: !&1{p0 p1}=p &1{ #O{@all1(p0)} #I{@all1(p1)} } +} + +// Enums all Bins of given size (label 2) +@all2(s) = ~s{ + 0: #E + p: !&2{p0 p1}=p &2{ #O{@all2(p0)} #I{@all2(p1)} } +} + +// 20: +//@K = 9 +//@H = 10 +//@S = 20 +//@X = @cat(@all1(@H) @bin(@H 0)) +//@Y = @cat(@all2(@H) @bin(@H 0)) +//@P = #1{#1{#1{#1{#0{#1{#1{#0{#1{#1{#0{#0{#1{#0{#1{#0{#0{#0{#1{#1{#2}}}}}}}}}}}}}}}}}}}} + +//// 30: +@K = 14 +@H = 15 +@S = 30 +@X = @cat(@all1(@H) @bin(@H 0)) +@Y = @cat(@all2(@H) @bin(@H 0)) +@P = #1{#1{#1{#0{#0{#0{#1{#1{#0{#1{#0{#1{#0{#0{#0{#0{#1{#0{#1{#1{#0{#0{#1{#0{#0{#1{#0{#1{#0{#1{#2}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} + +//INJECT// + +@main = + ! cond = @eq(@mul(@X @Y) @P) + ! not1 = @not(@eq(@X @bin(@S 1))) + @if(@and(cond not1) λt(t @u32(@X) @u32(@Y)) *) diff --git a/src/HVML/Collapse.hs b/src/HVML/Collapse.hs index 15b239b..1c5498b 100644 --- a/src/HVML/Collapse.hs +++ b/src/HVML/Collapse.hs @@ -268,12 +268,13 @@ pqPut (k,v) = pqUnion (PQNode (k,v) PQLeaf PQLeaf) flatten :: Collapse a -> [a] flatten term = go term (PQLeaf :: PQ (Collapse a)) where - go (CSup k a b) pq = go CEra (pqPut (k,a) $ pqPut (k,b) $ pq) + go (CSup k a b) pq = go CEra (pqPut (k,b) $ pqPut (k,a) $ pq) go (CVal x) pq = x : go CEra pq go CEra pq = case pqPop pq of Just ((k,v),pq) -> go v pq Nothing -> [] + -- Core Collapser -- -------------- diff --git a/src/HVML/Main.hs b/src/HVML/Main.hs index 27f8d2b..673e7f9 100644 --- a/src/HVML/Main.hs +++ b/src/HVML/Main.hs @@ -121,10 +121,13 @@ cliRun filePath compiled collapse showStats = do core <- doExtractCoreAt rxAt book 0 return [(doLiftDups core)] - -- Print results + -- Print all collapsed results forM_ vals $ \ term -> putStrLn $ coreToString term + -- Prints just the first collapsed result + -- putStrLn $ coreToString (head vals) + -- Prints total time end <- getCPUTime @@ -135,7 +138,7 @@ cliRun filePath compiled collapse showStats = do let time = fromIntegral (end - init) / (10^12) :: Double let mips = (fromIntegral itrs / 1000000.0) / time printf "WORK: %llu interactions\n" itrs - printf "TIME: %.3f seconds\n" time + printf "TIME: %.7f seconds\n" time printf "SIZE: %llu nodes\n" size printf "PERF: %.3f MIPS\n" mips return ()