jasonreich / flitersc

Supercompiler for F-liter, based on Bollingbroke & Peyton-Jones (2010)

F-liter Supercompiler

Debug variant.

A reimplementation of the Bollingbroke & Peyton-Jones (2010) compiler for the F-liter language in an attempt to understand it better. Currently packaged as a library and as is.

Try;

$ ghci Supercompiler
λ> ex_mapmap
main  = let x = Nil
        in sc x
sc x = let y = inc
       in
          let z = map y x
          in map y z
map x y = case y of
            Nil  -> Nil
            Cons z p -> let
                            q = x z
                            r = map x p
                        in Cons q r
inc x = let y = 1
        in x + y
λ> sc_wrapper ex_mapmap ("sc", lam "xs" $ fun "sc" @: "xs")
...

It will supercompile the function sc of program ex_mapmap with an unknown input.

Extra debug features

To aid debugging, the Debug.RocketFuel library prematurely terminates supercompilation when a predetermined "fuel" supply is depleted. This a very unsafe implementation of the concept introduced in Whalley's (1994) Automatic isolation of compiler errors.

By default, the fuel tank is infinite (i.e. Nothing).

• fuelTank is a global variable.
• disableTank creates infinite fuel.
• fillTank n creates a finite pool of n units of fuel.
• consumeFuel empty full will consume 1 unit of fuel. If the tank is depleted, it returns empty, otherwise full.
• readTank returns the fuel tank value.

flitersc's Issues

Improve pretty printer.

Remove similarly dull states (see #4)

Turns out there are similar things that should be left. For example;

f x y = case x of
          A  -> B x
          B z -> let p = A
                 in g y p
g x y = case x of
          A  -> B y
          B z -> f z x
main  = let
            x = let x = A
                in B x
            y = let
                    x = A
                    y = A
                in g x y
        in f x y
Terminated: B @[()]

f x y = case x of
          A  -> B x
          B z -> let p = A
                 in g y p
g x y = case x of
          A  -> B y
          B z -> h2 x z
h1 x = B x
h2 x y = case y of
           A  -> h1 y
           B z -> case x of
                    A  -> let p = A
                          in B p
                    B p -> h2 x p
main  = let
            x = let x = A
                in B x
            y = let
                    x = A
                    y = A
                in g x y
        in f x y

Tests: user error (@21404: Failed on optimisation! 52 < 54)

Non-termination on Queens example

sc_wrapper (parseProg "Benchmarks/Queens.hs") ("length", lam "xs" $ fun "length" @: "xs")

Results in non-termination.

Need to inline `h0` into the sc'ed function

Otherwise performance is impacted. Currently impeded if h0 is recursive.

No need to tie forward

If we're using equivalence then the 'future' state will be able to tie back to this one.

Possible problem with mapping

s0 'instanceOf' s1 so there is a mapping m and a list of extra things in s1. So what happens if s1 references heap elements which are brought into s0 but overwrite it?

Probably not a problem outside of proof.

SC.Matching.equivalence is not an equivalence

• Create testable algebraic properties
• Rename function if necessary

Finish with reachability analysis

• Tidy up final programs

Broken `removeLets` function

Exhibits @22.

Fix constructed prog tests

• Increase limits.
• Tell which funcs to sc.

Eliminate identity functions

These seem to be caused by tying unknown variables. E.g. h1 in @5.6744

f x y = case x of
          A  -> y
          B  -> x
main  = let
            x = A
            y = let
                    x = B
                    y = A
                in f x y
        in f x y
Terminated: B

f x y = case x of
          A  -> y
          B  -> h1 x
h1 x = x
main  = let
            x = A
            y = let
                    x = B
                    y = A
                in f x y
        in f x y

Tests: user error (@6744: Failed on optimisation! 25 < 29)