I had moved countries, apologies for the lack of updates. Will resume shortly.
Haha, that would have been nice!
It's found in test/Pbt/Expr/Utility.hs
. I think I mentioned it in an above comment, it's (mostly) the product of three ratios with a +1 to ensure the denominator is never zero. The function is called utility1
and is reproduced here.
utility1 :: Expr a -> Double
utility1 e =
if reducesToLiteral e
then 0
else
fromIntegral (countUsedLocalVars e * countConstants e * maxFunctionDepth (betaReduce e))
/ fromIntegral (1 + countIdentityFunctions e * countConstantFunctions e * maxFunctionDepth e)
This is in regards to commit gitlab.haskell.org:trac-fizzixnerd/ghc-pbts.git 2d5085e.
I've spent quite a bit of time building a generic gradient [ascent] optimizer. See this file. The most interesting part of it is that it uses affine traversals and generics to allow you to optimize over structures that don't necessarily look like vectors, and can find all the parameters you want to optimize by their type (I used a newtype Optimizable = Optimizable Double
for this).
Other than that, it's basically just a slow optimizer.
I sent it to work on optimizing one of the frequency tables, with a constant size parameter.
Context { ..., newLambdaFreq = 862.96047511123, newLocalVarFreq = 1035.3039872690567, newAppFreq = 2805.4620885532704, newVarFreq = 74.83219254980285, newLitFreq = 519.0509362170233, newCaseFreq = 108.79232601603755, ...}
The solution found above is starting from all frequencies == 1000
. There is still work to be done here, but I'll cut the explanation short since it's not really the purpose of this issue.
I found a GHC panic that I can confirm is in 9.8.1. Unfortunately for me, this means I can only run the optimizer through ghci. I reproduce the panic here, though I will likely end up filing a proper bug report.
To reproduce:
nix develop
[will load ghc 9.4, but I've confirmed it's a similar/same bug on 9.8].cabal test ghc-pbts
will panic when compiling Pbt.Expr
.cabal repl ghc-pbts
will not panic.[1 of 6] Compiling Pbt.Expr ( tests/Pbt/Expr.hs, /home/fizzixnerd/src/ghc-pbts/dist-newstyle/build/x86_64-linux/ghc-9.4.8/ghc-pbts-0.1.0.0/t/ghc-pbts/build/ghc-pbts/ghc-pbts-tmp/Pbt/Expr.o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.8:
Template variable unbound in rewrite rule
Variable: co_aarM :: (k_a6ZO :~~: *) ~# (Any :~~: Any)
Rule "SC:$j1"
Rule bndrs: [k_a6ZO, a_a6ZP, k_a703, a_a704, sc_saWf, sc_saW5,
sc_saW7, sc_saW9, sc_saWb, sc_saWd, sg_saWe, co_aarM, co_Xo]
LHS args: [(Tuple
@((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
@(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))
@(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))
@~(<((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))>_N
:: ((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
~# ((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))))
sc_saW7
sc_saW9
(sc_saWb, sc_saWd))
`cast` (sg_saWe
:: Binder
((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
~R# Binder a_a7bZ),
sc_saWf]
Actual args: [(Tuple
@((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
@(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))
@(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))
@~(<((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))>_N
:: ((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
~# ((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))))
($dTypeable35_Xq
`cast` ((Typeable
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
(GRefl nominal a_a6ZP
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))))_R
:: Typeable a_a6ZP
~R# Typeable
(a_a6ZP |> Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))))
($dTypeable35_Xr
`cast` ((Typeable
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
(GRefl nominal a_a704
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))))_R
:: Typeable a_a704
~R# Typeable
(a_a704 |> Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))))
(idX_a2Hb
`cast` ((Id
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
Univ(phantom phantom (Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
:: a_a6ZP, (a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))))_R
:: Id a_a6ZP
~R# Id
(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))),
idY_a2Hc
`cast` ((Id
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
Univ(phantom phantom (Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
:: a_a704, (a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))))_R
:: Id a_a704
~R# Id
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))))
`cast` ((Binder
(Nth:2 (Sub co_Xt)
; Nth:3 (Sub (Sym co_Xt))))_R
:: Binder
((a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM)))),
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo)))))
~R# Binder a_a7bZ),
case ctx'_sa9h of
{ Context bx_d9ww ds_d9eJ ds_d9eK ds_d9eL ds_d9eM [Dmd=SL] ds_d9eN
ds_d9eO ds_d9eP ds_d9eQ bx_d9wx ->
case ds_d9eM of wild_saTd { I# x_saTe ->
Context
@Int
bx_d9ww
(: @(Int, SomeScopedId)
(case $wlenAcc @(Int, SomeScopedId) ds_d9eJ 0# of ww1_aaxq
{ __DEFAULT ->
I# (+# (*# (*# x_saTe (+# ww1_aaxq 1#)) bx_d9ww) 1#)
},
SomeScopedId
@(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))
($dTypeable35_Xq
`cast` ((Typeable
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
(GRefl nominal a_a6ZP
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))))_R
:: Typeable a_a6ZP
~R# Typeable
(a_a6ZP |> Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))))
(LocalId
@(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))
(idX_a2Hb
`cast` ((Id
(Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
Univ(phantom phantom (Nth:2 (Sub co_aarM)
; Nth:3 (Sub (Sym co_aarM)))
:: a_a6ZP, (a_a6ZP |> Sym (Sym (Nth:3
(Sub (Sym co_aarM)))
; Nth:2
(Sub (Sym co_aarM))))))_R
:: Id a_a6ZP
~R# Id
(a_a6ZP |> Sym (Sym (Nth:3 (Sub (Sym co_aarM)))
; Nth:2 (Sub (Sym co_aarM))))))))
(: @(Int, SomeScopedId)
(case $wlenAcc @(Int, SomeScopedId) ds_d9eJ 0# of ww1_aaxq
{ __DEFAULT ->
I# (+# (*# (*# x_saTe ww1_aaxq) bx_d9ww) 1#)
},
SomeScopedId
@(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))
($dTypeable35_Xr
`cast` ((Typeable
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
(GRefl nominal a_a704
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))))_R
:: Typeable a_a704
~R# Typeable
(a_a704 |> Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))))
(LocalId
@(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))
(idY_a2Hc
`cast` ((Id
(Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
Univ(phantom phantom (Nth:2 (Sub co_Xo)
; Nth:3 (Sub (Sym co_Xo)))
:: a_a704, (a_a704 |> Sym (Sym (Nth:3
(Sub (Sym co_Xo)))
; Nth:2
(Sub (Sym co_Xo))))))_R
:: Id a_a704
~R# Id
(a_a704 |> Sym (Sym (Nth:3 (Sub (Sym co_Xo)))
; Nth:2 (Sub (Sym co_Xo))))))))
ds_d9eJ))
ds_d9eK
ds_d9eL
wild_saTd
ds_d9eN
ds_d9eO
ds_d9eP
ds_d9eQ
bx_d9wx
}
}]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Rules.hs:625:10 in ghc:GHC.Core.Rules
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
I admit I haven't looked through the backlog of bug reports yet since my last update
round 1e54
is known.Adding a checkbox here since that motivated me last time.
I added support for generating case
expressions and boxed and unboxed tuples. Now that I have an optimizer, next steps include running the optimizer over the Context for generating those, and then looking at expressions involving seq
and undefined :: Int
and Int
s, hopefully to find a strictness bug. Odd to be hoping to find bugs, but I guess that's currently my goal, so I won't apologize for it
Until next time.
Matt Walker (2d5085e5) at 04 Mar 18:07
Update optimizer and weights. It works!
Matt Walker (63d2d4ac) at 03 Mar 23:26
Got optimizer optimizing
Matt Walker (e4c55e2f) at 28 Feb 04:50
Formatting
@Mikolaj I've confirmed the bug in 9.8.1 and 9.9.20231121.
@clyring I'll take a look through the backlog and see if I can locate this as a duplicate. Your explanation is very helpful, thank you (and thanks for minimizing it too, faster than I could!) If I understand correctly, GHC.Float.roundDouble @Int
, when not rewritten, uses a different implementation yes? I will try to locate that implementation and see what it looks like.
Matt Walker (dba8b403) at 27 Feb 11:55
Found a bug; added -fno-cse and other flags for unsafePerformIO
Hehe, thanks. I looked at the comment, and have made some amendments. Will post and update later. Thanks for the tips.
I found one!
{-# OPTIONS_GHC #-}
module Main where
(|+|) :: Int -> Int -> Int
(|+|) = (Prelude.+)
isucc :: Int -> Int
isucc = Prelude.succ
(|*|) :: Int -> Int -> Int
(|*|) = (Prelude.*)
idiv :: Int -> Int -> Int
idiv = Prelude.div
(.+) :: Double -> Double -> Double
(.+) = (Prelude.+)
(.*) :: Double -> Double -> Double
(.*) = (Prelude.*)
(./) :: Double -> Double -> Double
(./) = (Prelude./)
itod :: Int -> Double
itod = Prelude.fromIntegral
dtoi :: Double -> Int
dtoi = Prelude.round
(|:|) :: Int -> [Int] -> [Int]
(|:|) = (:)
nil :: [Int]
nil = Prelude.mempty
fmapIntToInt :: (Int -> Int) -> [Int] -> [Int]
fmapIntToInt = Prelude.fmap
fmapIntToDouble :: (Int -> Double) -> [Int] -> [Double]
fmapIntToDouble = Prelude.fmap
fmapDoubleToDouble :: (Double -> Double) -> [Double] -> [Double]
fmapDoubleToDouble = Prelude.fmap
foldlIntoToListInt :: ([Int] -> Int -> [Int]) -> [Int] -> [Int] -> [Int]
foldlIntoToListInt = Prelude.foldl
lengthInt :: [Int] -> Int
lengthInt = Prelude.length
z0 :: Int
z0 = ((\x199980 -> ((\x759565 -> ((isucc) ((\x924550 -> ((\x553186 -> ((dtoi) ((\x508931 -> (1.0e54)) (\x847936 -> ((\x363561 -> (x199980)) ((|*|) ((isucc) (442964306074415104)))))))) ((\x151243 -> ((\x949028 -> ((\x666958 -> ((\x22669 -> (\x64340 -> (isucc))) ((\x277762 -> (())) (\x378938 -> ((isucc) (x199980)))))) (\x892493 -> (x759565)))) (-100.0))) ((\x134979 -> (x199980)) (\x696641 -> (x759565)))))) ((\x365688 -> ((\x592395 -> ((\x698477 -> (42.0)) ((|*|) (7638258429092114432)))) ((\x2397 -> (isucc)) (\x641835 -> ((\x543905 -> ((\x979997 -> (\x681590 -> ((isucc) (x199980)))) (\x874925 -> (-5563047443709351936)))) (\x358654 -> (7911141761824606208))))))) ((\x871176 -> ((\x703764 -> ((\x536509 -> (2138937281242984448)) (isucc))) (()))) ((\x275309 -> (\x172784 -> (isucc))) ((\x217643 -> (1811452823508711424)) (\x991947 -> (\x653132 -> ((isucc) (8416399215203923968))))))))))) ((\x166875 -> ((\x956848 -> ((x166875) ((x166875) ((dtoi) (x956848))))) ((\x487124 -> ((\x581187 -> ((\x226529 -> (x487124)) (\x979119 -> (\x390836 -> (5509058099755335680))))) ((\x690407 -> (\x116322 -> ((dtoi) (28393.0)))) ((\x785097 -> (\x642975 -> (x199980))) ((\x109964 -> (\x653548 -> ((|*|) (-7847816032831493120)))) (\x322259 -> (\x124933 -> ((\x399939 -> ((\x108224 -> ((\x808469 -> (-8491371358049009664)) (\x877055 -> ((\x637630 -> ((\x798503 -> ((x399939) (\x152982 -> (-3955775085709914112)))) (\x301934 -> (6810801650915911680)))) (x487124))))) (x166875))) ((\x28015 -> (\x771311 -> (\x772750 -> (-2786190340597368832)))) ((\x81186 -> (\x340421 -> ((dtoi) (x487124)))) (x487124))))))))))) ((\x158277 -> ((\x673454 -> (42.0)) ((\x952 -> (x166875)) ((\x460904 -> (())) (x199980))))) ((\x503098 -> (\x86095 -> (\x512342 -> (x199980)))) (\x510500 -> ((\x124443 -> ((\x154587 -> ((x166875) (-4232410177602131968))) (\x132088 -> ((x166875) (-4710232329768865792))))) ((idiv) (2932474766467565568))))))))) ((\x553999 -> ((\x592733 -> ((idiv) ((x592733) ((x553999) ((x553999) ((\x393106 -> ((dtoi) (4.2e-5))) ((\x587578 -> (\x871303 -> (x553999))) (x553999)))))))) ((|+|) ((x553999) (-1470072819678219264))))) ((\x624201 -> ((\x907607 -> ((idiv) ((\x34991 -> ((x34991) ((dtoi) ((itod) ((\x417506 -> ((\x753235 -> (x199980)) (x907607))) (\x486242 -> (\x126971 -> (x199980)))))))) ((idiv) (1453475880982245376))))) ((\x170082 -> ((\x726558 -> (\x972126 -> ((\x53832 -> (\x326777 -> (-5657323274424557568))) (isucc)))) ((\x322879 -> (-2084867062826840064)) (\x275989 -> ((\x326994 -> (\x763487 -> (x199980))) (isucc)))))) (())))) ((\x42306 -> ((\x718238 -> (1.0)) ((\x122388 -> (\x498361 -> ((x42306) (x199980)))) (\x486094 -> ((idiv) (8158073927885264896)))))) ((\x460534 -> (isucc)) (isucc)))))))) ((\x306608 -> ((dtoi) ((\x554899 -> ((\x128862 -> ((\x111188 -> ((\x701685 -> (4.2e-5)) (x111188))) ((\x749373 -> (\x253033 -> ((\x694080 -> (\x537189 -> (x554899))) (4200.0)))) ((|*|) (x306608))))) ((dtoi) ((itod) (x306608))))) ((isucc) ((\x816169 -> ((x816169) ((\x828698 -> ((x816169) (x306608))) ((\x917510 -> ((|*|) (x306608))) (\x354371 -> (-2372436635954327552)))))) ((|+|) ((dtoi) ((\x232733 -> ((itod) ((\x115419 -> (-7389496593200066560)) (\x943099 -> (5786210152905857024))))) ((idiv) ((\x115894 -> ((\x859908 -> (x306608)) (\x281347 -> (isucc)))) (\x396521 -> ((\x28017 -> (x306608)) (\x215855 -> (\x79365 -> ((dtoi) (100.0)))))))))))))))) ((\x327014 -> ((\x514037 -> ((\x780919 -> ((\x518139 -> ((dtoi) (-1.0e54))) ((\x362182 -> (x780919)) (x780919)))) ((\x526421 -> ((\x300627 -> (x327014)) (x327014))) ((\x515773 -> (1.0e-6)) (x327014))))) ((\x55348 -> ((\x249379 -> ((\x860584 -> (())) (x55348))) ((\x524444 -> (\x66488 -> (\x559669 -> (2593731879873681408)))) ((itod) ((\x360107 -> (2595904161254361088)) (\x623943 -> (\x487908 -> (2091062300941402112)))))))) ((\x250759 -> ((\x902303 -> ((\x102114 -> (())) ((\x746790 -> ((\x528890 -> ((\x572572 -> ((\x215280 -> (x250759)) ((\x720362 -> ((\x558425 -> (\x239856 -> (x327014))) (\x410481 -> (x250759)))) (\x136158 -> (x327014))))) ((idiv) (5036459139295713280)))) ((\x151319 -> (x327014)) ((\x248045 -> (4200.0)) (x902303))))) ((\x85866 -> (x327014)) ((\x287788 -> (\x722253 -> ((\x498953 -> ((\x606528 -> (x250759)) (x327014))) (x287788)))) (\x229063 -> ((\x666012 -> (\x921179 -> ((\x200697 -> (x250759)) (x327014)))) (x327014)))))))) (100.0))) ((\x947686 -> ((\x265674 -> (-3729925203558540288)) (\x365162 -> ((|+|) (-1960776898682116096))))) (x327014)))))) ((\x692910 -> ((|*|) ((\x517015 -> ((\x275397 -> ((x517015) (7390311090165049344))) (x517015))) ((\x339440 -> (\x972866 -> (-1643297881786008576))) (isucc))))) ((itod) ((\x857674 -> ((\x416518 -> (2442501699968790528)) (\x630019 -> ((\x689991 -> (\x367453 -> (8401326013846427648))) ((\x939937 -> (x857674)) (\x105648 -> (x105648))))))) ((\x498345 -> (\x374131 -> (-7469519551844577280))) (\x522169 -> ((\x122976 -> (-1730429098277190656)) (isucc))))))))))
main = do {
print $ id $ z0;
}
This program when compiled with -O2 prints -9223372036854775807
, and without optimizations prints 1
! Woohoo!
This is on GHC 9.4.8, from nixpkgs (on Ubuntu). I'll hold off an actual bug report until I've worked out the shrinking, but this is pretty exciting to me!
The driver is now working, in terms of the hard and tricky parts of it.
I have also uploaded the code to this GitLab here: https://gitlab.haskell.org/trac-fizzixnerd/ghc-pbts
Some things that will be of interest to the curious diver:
Currently Main.main
just generates random functions Int -> Int
, and given the arguments I'm now realizing I passed to it in the current commit (9ffb4160427c07ee73fa68e8f7d064b6cb9adc3d), it probably can't be possibly be doing anything interesting. That doesn't mean it's not working though!
unsafePerformIO
falsify
requires the properties tested be pure, as far as I can tell. Yup.
So I did something slightly evil. This is my first major foray into unsafePerformIO
territory. It seems to work, however, the way I want it to.
In this function, I call unsafeRunDriver
which is just moduleDance
wrapped in unsafePerformIO
, with a NOINLINE
pragma for good measure to ensure (?) that it's... um... not inlined. Pretty sure this makes it work the way I want. Would appreciate someone's input though, before I start messing with CI running such a thing. (If I don't get that input before tomorrow I'm gonna start messing with it though!
In any case, this means that it will be called over and over again in the Main test, and from the output I can see that it's generating new files in new directories. I am realizing I have not fully ensured that it's making the contents of the files different each time, but I will.
I'm finally at a point where I could attempt to recreate Palka's results. I think that's a good first step to ensure that what I have so far is "useful".
Until next time!
Matt Walker (9ffb4160) at 27 Feb 00:16
Get the driver working!
Matt Walker (674849b1) at 26 Feb 19:50
Documentation and invariance under betaReduction of 'isConstantFunc...
Matt Walker (3416f138) at 25 Feb 19:49
Rename