Commit 5d0863d4 authored by batterseapower's avatar batterseapower

First draft of supercompilation nofib tests

parent d77043e5
......@@ -59,11 +59,17 @@ endif
# All the standard gluing together, as in the comment right at the front
ifeq "$(SRC_SUPERCOMP_HC_OPTS" ""
SRC_SUPERCOMP_HC_OPTS = -fsupercompiler-bound-steps
endif
HC_OPTS = $(BOOTSTRAPPING_PACKAGE_CONF_HC_OPTS) $(SRC_HC_OPTS) $(WAY$(_way)_HC_OPTS) $($*_HC_OPTS) $(EXTRA_HC_OPTS)
ifeq "$(HC_VERSION_GE_6_13)" "YES"
HC_OPTS += -rtsopts
endif
ifeq "$(NoFibSupercompile)" "YES"
HC_OPTS += -O2 -fsupercompilation $(SRC_SUPERCOMP_HC_OPTS)
endif
HC_POST_OPTS = $(SRC_HC_POST_OPTS) $(WAY$(_way)_HC_POST_OPTS) $($*_HC_POST_OPTS) $(EXTRA_HC_POST_OPTS)
HC_PRE_OPTS = $(SRC_HC_PRE_OPTS) $(WAY$(_way)_HC_PRE_OPTS) $($*_HC_PRE_OPTS) $(EXTRA_HC_PRE_OPTS)
......
TOP = ..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = compile-time contracts ilya jason neil peter toys trivial
include $(TOP)/mk/target.mk
module Main where
main :: IO ()
main = print (length (f1 0))
{-# SUPERCOMPILE f1 #-}
f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 :: Int -> [Int]
f1 x = concatMap f2 [y, y + 1]
where y = (x + 1) * 2
f2 x = concatMap f3 [y, y + 1]
where y = (x + 1) * 2
f3 x = concatMap f4 [y, y + 1]
where y = (x + 1) * 2
f4 x = concatMap f5 [y, y + 1]
where y = (x + 1) * 2
f5 x = concatMap f6 [y, y + 1]
where y = (x + 1) * 2
f6 x = concatMap f7 [y, y + 1]
where y = (x + 1) * 2
f7 x = concatMap f8 [y, y + 1]
where y = (x + 1) * 2
f8 x = concatMap f9 [y, y + 1]
where y = (x + 1) * 2
f9 x = concatMap f10 [y, y + 1]
where y = (x + 1) * 2
f10 x = concatMap f11 [y, y + 1]
where y = (x + 1) * 2
f11 x = concatMap f12 [y, y + 1]
where y = (x + 1) * 2
f12 x = [x + 1]
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
TOP = ../..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = ConcatMapSpec SimonSpec
include $(TOP)/mk/target.mk
module Main where
main :: IO ()
main = print (length (f1 0))
{-# SUPERCOMPILE f1 #-}
f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 :: Int -> [Int]
f1 x = f2 y ++ f2 (y + 1)
where y = (x + 1) * 2
f2 x = f3 y ++ f3 (y + 1)
where y = (x + 1) * 2
f3 x = f4 y ++ f4 (y + 1)
where y = (x + 1) * 2
f4 x = f5 y ++ f5 (y + 1)
where y = (x + 1) * 2
f5 x = f6 y ++ f6 (y + 1)
where y = (x + 1) * 2
f6 x = f7 y ++ f7 (y + 1)
where y = (x + 1) * 2
f7 x = f8 y ++ f8 (y + 1)
where y = (x + 1) * 2
f8 x = f9 y ++ f9 (y + 1)
where y = (x + 1) * 2
f9 x = f10 y ++ f10 (y + 1)
where y = (x + 1) * 2
f10 x = f11 y ++ f11 (y + 1)
where y = (x + 1) * 2
f11 x = f12 y ++ f12 (y + 1)
where y = (x + 1) * 2
f12 x = [x + 1]
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
main :: IO ()
main = print (my_head_check [1, 2])
-- my_head : {xs | not (null xs)} -> Ok
my_head xs = case xs of y:_ -> y
{-# SUPERCOMPILE my_head_check #-}
my_head_check xs = my_head (case not (null xs) of
True -> xs
False -> error "UNR")
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
main :: IO ()
main = print (idList [1, 2])
sameLength xs ys = case xs of
[] -> case ys of [] -> True
(_:_) -> False
(_:as) -> case ys of [] -> False
(_:bs) -> sameLength as bs
-- idList : xs -> {rs | sameLength xs rs}
idList_rec idList xs = case xs of
[] -> []
y:ys -> y:idList ys
-- Programatically generated version:
-- idList_check idList xs
-- = let rs = idList_rec idList_ok xs
-- in case sameLength xs rs of True -> rs
-- where idList_ok xs = if sameLength xs rs then rs else error "UNR"
-- where rs = idList xs
-- An example with less work sharing but exactly the same issues:
{-# SUPERCOMPILE idList_check #-}
idList_check idList xs
= case sameLength xs (idList_rec idList_ok xs) of True -> idList_rec idList_ok xs
where idList_ok xs = if sameLength xs (idList xs) then idList xs else error "UNR"
{-# SUPERCOMPILE idList #-}
idList = root idList
{-
-- Here is why this doesn't work. First, the above program in g-function form:
sameLength xs ys = case xs of
[] -> case ys of [] -> True
(_:_) -> False
(_:as) -> case ys of [] -> False
(_:bs) -> sameLength as bs
sameLength [] ys = sameLengthNil ys
sameLength (_:as) ys = sameLengthCons as ys
sameLengthNil [] = True
sameLengthNil (_:_) = False
sameLengthCons as [] = False
sameLengthCons as (_:bs) = sameLength as bs
idList_rec idList [] = []
idList_rec idList (y:ys) = y:idList ys
idList_ok idList xs = let rs_ok = idList xs in if sameLength xs rs_ok then rs_ok else error "UNR"
idList_check idList xs
= let rs_rec = idList_rec (idList_ok idList) xs
in case sameLength xs rs_rec of True -> rs_rec
-- Now the drive sequence:
h0 idList xs = let rs_rec = idList_rec (idList_ok idList) xs
in case sameLength xs rs_rec of True -> rs_rec
=> case xs of
[] -> h1 idList = let rs_rec = idList_rec (idList_ok idList) []
in case sameLength [] rs_rec of True -> rs_rec
=> []
(a:as) -> h2 idList a as = let rs_rec = idList_rec (idList_ok idList) (a:as)
in case sameLength (a:as) rs_rec of True -> rs_rec
=> let rs_rec = a : idList_ok idList as
in case sameLengthCons as rs_rec of True -> rs_rec
=> let rs_rec1 = idList_ok idList as
in case sameLength as rs_rec1 of True -> a:rs_rec1
=> case as of
[] -> h3 idList a = let rs_rec1 = idList_ok idList []
in case sameLength [] rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok = idList [] in if sameLength [] rs_ok then rs_ok else error "UNR"
in case sameLengthNil rs_rec1 of True -> a:rs_rec1
=> a:[]
(a1:as1) -> h4 idList a a1 as1 = let rs_rec1 = idList_ok idList (a1:as1)
in case sameLength (a1:as1) rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok2 = idList as1 in if sameLength as1 rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
=> case as1 of
[] -> h5 idList a a1 = let rs_rec1 = let rs_ok2 = idList [] in if sameLength [] rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons [] rs_rec1 of True -> a:rs_rec1
=> a:a1:[]
(a2:as2) -> h6 idList a a1 a2 as2 = let rs_rec1 = let rs_ok2 = idList (a2:as2) in if sameLength (a2:as2) rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
=> let rs_rec1 = let rs_ok3 = idList as2 in if sameLength as2 rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
=> case as2 of
[] -> h7 idList a a1 a2 = ...
(a3:as3) -> h8 idList a a1 a2 a3 as3 = let rs_rec1 = let rs_ok3 = idList (a3:as3) in if sameLength (a3:as3) rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:a3:as3) rs_rec1 of True -> a:rs_rec1
-- Interesting stuff. You can see that we don't get tieback due to growing things:
-- Zeroeth time around (ish, this is a bit of a lie as the zeroeth time we haven't unfolded idList_ok yet):
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
-- First time around:
let rs_rec1 = let rs_ok2 = idList (a2:as2) in if sameLength (a2:as2) rs_ok2 then (a1:rs_ok2) else error "UNR"
in case sameLengthCons (a2:as2) rs_rec1 of True -> a:rs_rec1
-- Second time around:
let rs_rec1 = let rs_ok3 = idList (a3:as3) in if sameLength (a3:as3) rs_ok3 then (a1:a2:rs_ok3) else error "UNR"
in case sameLengthCons (a2:a3:as3) rs_rec1 of True -> a:rs_rec1
-- The same thing, without let:
-- Zeroeth time around (ish, this is a bit of a lie as the zeroeth time we haven't unfolded idList_ok yet):
case sameLengthCons as1 (if sameLength (a1:as1) (idList (a1:as1)) then idList (a1:as1) else error "UNR") of
True -> a:if sameLength (a1:as1) (idList (a1:as1)) then idList (a1:as1) else error "UNR"
-- First time around:
case sameLengthCons (a2:as2) (if sameLength (a2:as2) (idList (a2:as2)) then (a1:idList (a2:as2)) else error "UNR") of
True -> a:if sameLength (a2:as2) (idList (a2:as2)) then (a1:idList (a2:as2)) else error "UNR"
-- Second time around:
case sameLengthCons (a2:a3:as3) (if sameLength (a3:as3) (idList (a3:as3)) then (a1:a2:idList (a3:as3)) else error "UNR") of
True -> a:if sameLength (a3:as3) (idList (a3:as3)) then (a1:a2:idList (a3:as3)) else error "UNR"
-- Voightlander story:
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then rs_ok else error "UNR"
in case sameLengthCons as1 rs_rec1 of True -> a:rs_rec1
-- 1) Generalise:
gen1 = rs_ok
gen2 = as1
let rs_rec1 = let rs_ok = idList (a1:as1) in if sameLength (a1:as1) rs_ok then gen1 else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 2) Evaluate:
let rs_rec1 = let rs_ok1 = idList as1 in if sameLength as1 rs_ok1 then a1:gen1 else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 3) We are stuck, so case split on as1:
-- 3a) Evaluate nil case normally
=> case sameLengthCons gen2 (a1:gen1) of True -> a:a1:gen1
=> case sameLength gen2 gen1 of True -> a:a1:gen1
-- 3ai) Generate gen2 based float
case sameLength <_> gen1 of True -> a:a1:gen1
-- 3b) Generalise the cons case
gen1' = a1:gen1
let rs_rec1 = let rs_ok1 = idList (a2:as2) in if sameLength (a2:as2) rs_ok1 then gen1' else error "UNR"
in case sameLengthCons gen2 rs_rec1 of True -> a:rs_rec1
-- 3bi) Tie back to the generalised verson, with:
gen2 = gen2
gen1 = gen1'
a1 = a2
as1 = as2
-- 3bii) Expand float:
case sameLength gen2 (a1:gen1) of True -> a:a2:gen1'
??? seems wrong
-}
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
main :: IO ()
main = print (idList_check [1, 2])
sameLength xs ys = case xs of
[] -> case ys of [] -> True
(_:_) -> False
(_:as) -> case ys of [] -> False
(_:bs) -> sameLength as bs
-- idList : xs -> {rs | sameLength xs rs}
idList xs = case xs of [] -> []
(a:as) -> a : idList as
{-# SUPERCOMPILE idList_check #-}
idList_check xs = let rs = idList xs
in case sameLength xs rs of True -> rs
{-
In g-function form:
sameLength [] ys = sameLengthNil ys
sameLength (a:as) ys = sameLengthCons as ys
sameLengthNil [] = True
sameLengthNil (b:bs) = False
sameLengthCons as [] = False
sameLengthCons as (b:bs) = sameLength as bs
Here is the sketch:
h0 xs = let rs = idList xs
in ok rs (sameLength xs rs)
=> case xs of
[] -> h1 = let rs = idList []
in ok rs (sameLength [] rs)
==> []
(a:as) -> h2 a as = let rs = idList (a:as)
in ok rs (sameLength (a:as) rs)
=> let rs1 = idList as
in ok (a:rs1) (sameLength (a:as) (a:rs1))
=> let rs1 = idList as
in ok (a:rs1) (sameLength as rs1)
=> case as of
[] -> h1 a = let rs1 = idList []
in ok (a:rs1) (sameLength [] rs1)
=> a:[]
(a1:as1) -> h2 a a1 as1 = let rs1 = idList (a1:as1)
in ok (a:rs1) (sameLength (a1:as1) rs1)
=> let rs2 = idList as1
in ok (a:a1:rs2) (sameLength (a1:as1) (a1:rs2))
=> let rs2 = idList as1
in ok (a:a1:rs2) (sameLength as1 rs2)
=> case as1 of
[] -> h3 a a1 = let rs2 = idList []
in ok (a:a1:rs2) (sameLength [] rs2)
=> a:a1:[]
(a2:as2) -> h4 a a1 a2 as2 = let rs2 = idList (a2:as2)
in ok (a:a1:rs2) (sameLength (a2:as2) rs2)
=> let rs3 = idList as2
in ok (a:a1:a2:rs3) (sameLength (a2:as2) (a2:rs3))
=> let rs3 = idList as2
in ok (a:a1:a2:rs3) (sameLength as2 rs3)
Generalise the argument to "ok" to get tieback. Only issue is that (without speculation) that will force rs2 to be resid for work duplication reasons.
However, if we do call by name things will work smoothly and "BAD will vanish". We hope!
-}
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
main :: IO ()
main = print (last [1, 2])
null xs = case xs of
_:_ -> False
[] -> True
not b = if b then False else True
-- lst : {xs | not (null xs)} -> Ok
last_rec last xs = case xs of
y:ys -> case ys of
[] -> y
z:zs -> last ys
last_check last xs = last_rec last_ok (if not (null xs) then xs else error "UNR")
where last_ok xs = last (case not (null xs) of True -> xs)
{-# SUPERCOMPILE last #-}
last = last_check last
\ No newline at end of file
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
TOP = ../..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = Head-Contract IdList-SameLength-Koen IdList-SameLength Last-Contract Zip-Contract
include $(TOP)/mk/target.mk
module Main where
main :: IO ()
main = print (zip_wrap [1,2,3] [4,5,6])
sameLength xs ys = case xs of
[] -> case ys of
[] -> True
b:bs -> False
a:as -> case ys of
[] -> False
b:bs -> sameLength as bs
zip xs ys = case xs of
[] -> case ys of
[] -> []
a:as -> case ys of
b:bs -> (a,b) : zip as bs
{-# SUPERCOMPILE zip_wrap #-}
zip_wrap xs ys = zip xs (case sameLength xs ys of True -> ys; False -> error "UNR")
{-
h0 xs ys = zipp xs (case sameLength xs ys of True -> ys; False -> error "UNR")
=> case xs of
[] -> h1 ys = case (case sameLength [] ys of True -> ys; False -> error "UNR") of
[] -> []
=> case (case (case ys of
[] -> True
b:bs -> False) of True -> ys; False -> error "UNR") of
[] -> []
=> case ys of
[] -> h2 = case (case True of True -> []; False -> error "UNR") of [] -> []
=> []
b:bs -> h3 b bs = case (case False of True -> b:bs; False -> error "UNR") of [] -> []
=> error "UNR"
a:as -> h4 a as ys = case (case sameLength (a:as) ys of True -> ys; False -> error "UNR") of
b:bs -> (a,b) : zipp as bs
=> case (case (case ys of [] -> False
b:bs -> sameLength as bs) of True -> ys; False -> error "UNR") of
b:bs -> (a,b) : zipp as bs
=> case ys of [] -> h5 a as = case (case False of True -> []; False -> error "UNR") of
b:bs -> (a,b) : zipp as bs
=> case (error "UNR") of
b:bs -> (a,b) : zipp as bs
=> error "UNR"
b:bs -> h6 a as b bs = ... ctd at left margin ...
-- NB: I renamed the as and bs variables at this point for convenience
h6 a xs b ys = case (case sameLength xs ys of True -> b:ys; False -> error "UNR") of
b:ys -> (a,b) : zipp xs ys
=> case (case sameLength xs ys of True -> b:ys; False -> error "UNR") of
b:ys -> (a,b) : zipp xs ys
=> case (case (case xs of
[] -> case ys of
[] -> True
b:bs -> False
a:as -> case ys of
[] -> False
b:bs -> sameLength as bs) of True -> b:ys; False -> error "UNR") of
b:ys -> (a,b) : zipp xs ys
=> case xs of
[] -> h7 a b ys = case (case (case ys of
[] -> True
b:bs -> False) of True -> b:ys; False -> error "UNR") of
b:ys -> (a,b) : zipp [] ys
=> case ys of
[] -> h8 a xs b = case (case True of True -> b:[]; False -> error "UNR") of
b:ys -> (a,b) : zipp [] []
=> (a,b) : zipp [] []
=> (a,b) : []
b':bs -> h9 a xs b b' bs = case (case False of True -> b:b':bs; False -> error "UNR") of
b:ys -> (a,b) : zipp xs (b':bs)
=> error "UNR"
a':as -> h10 a a' as b ys = case (case (case ys of
[] -> False
b:bs -> sameLength as bs) of True -> b:ys; False -> error "UNR") of
b:ys -> (a,b) : zipp (a':as) ys
=> case ys of
[] -> h11 a a' as b = case (case False of True -> b:[]; False -> error "UNR") of
b:ys -> (a,b) : zipp (a':as) []
=> error "UNR"
b':bs -> h12 a a' as b b' bs = ... ctd at left margin ...
-- NB: I renamed as and bs again
h12 a a' xs b b' ys = case (case sameLength xs ys of True -> b:b':ys; False -> error "UNR") of
b:ys -> (a,b) : zipp (a':xs) ys
-- Now we are here, it is clear what the problem is. We are generating one specialisation of zipp_wrap for each possible length of
-- the twin lists passed in. There is no bound to this number, so the specialisation process will not terminate. Drat!
--
-- This happens because every time we unwrap sameLength we gain knowledge about another layer of the input lists, which accumulates
-- as we get deeper into the list (we can never throw it away because we don't actually pattern match on it until we evaluate the
-- thing in the outermost case -- the zipp call.. its kind of a space leak thing?).
-- Interestingly, we could tie back at h12 if we REALLY smart about matching (NB: in reality would probably tie back a bit earlier?):
-- h12 a a' xs b b' ys = h6 a (a':xs) b (b':ys)
-- Note that making this tieback requires us to spot that:
-- sameLength xs ys <==> sameLength (a':xs) (b':ys)
-- This is hardly realistic! But if we could do it we would close the loop and would prove the proposition.
-}
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
import Prelude hiding (map, filter, foldr, (++), (.))
main :: IO ()
main = print (root (<= 2) (+1) [1, 2, 3, 4])
foldr c n xs = case xs of [] -> n; (y:ys) -> c y (foldr c n ys)
(++) xs ys = foldr (:) ys xs
map f = foldr (\x xs -> f x : xs) []
filter p = foldr (\x xs -> if p x then x : xs else xs) []
(.) f g x = f (g x)
{-# SUPERCOMPILE root #-}
root p f xs = (filter p (map f xs), map f (filter (p . f) xs))
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
import Prelude hiding (foldr, map, iterate)
main :: IO ()
main = print (case root (+1) 0 of (as, bs) -> (case as of a:_ -> a, case bs of b:_ -> b))
foldr c n xs = case xs of [] -> n; (y:ys) -> c y (foldr c n ys)
map f = foldr (\x xs -> f x : xs) []
iterate f x = x : iterate f (f x)
{-# SUPERCOMPILE root #-}
root f x = (iterate f (f x), map f (iterate f x))
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
module Main where
import Prelude hiding (foldr, map, length, (++), concat, plus, sum)
main :: IO ()
main = print (root ["A", "BC"])
foldr c n xs = case xs of [] -> n; (y:ys) -> c y (foldr c n ys)
map f = foldr (\x xs -> f x : xs) []
length = foldr (\_ -> S) Z
(++) xs ys = foldr (:) ys xs
concat = foldr (++) []
plus n m = case n of Z -> m; S o -> S (plus o m)
sum = foldr plus Z
{-# SUPERCOMPILE root #-}
root xs = (length (concat xs), sum (map length xs))
data Nat = Z | S Nat
deriving (Eq, Show)
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRCS = Main.hs
TOP = ../..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = FilterMap-MapFilterCompose Iterate-MapIterate LengthConcat-SumMapLength Map-JoinComposeReturn MapAppend-AppendMapMap MapCompose-ComposeMapMap MapConcat-ConcatMapMap
include $(TOP)/mk/target.mk
module Main where
import Prelude hiding (foldr, (++), map, (.), return, join)
main :: IO ()
main = print (root (+1) [1, 2, 3])
foldr c n xs = case xs of [] -> n; (y:ys) -> c y (foldr c n ys)
(++) xs ys = foldr (:) ys xs
map f = foldr (\x xs -> f x : xs) []
(.) f g x = f (g x)
return x = [x]
join m k = foldr ((++) . k) [] m -- This is really >>= for the list monad
{-# SUPERCOMPILE root #-}