...
 
Commits (9)
# OS junk
Thumbs.db
.DS_Store
# Generated file patterns
*.o
*.hi
......
......@@ -28,7 +28,7 @@ SUBDIRS = runstdtest nofib-analyse $(NoFibSubDirs)
#
SRC_DIST_DIR=$(shell pwd)/nofib
SRC_DIST_NAME=nofib
SRC_DIST_DIRS=docs fibon gc imaginary smp spectral real parallel mk
SRC_DIST_DIRS=docs fibon gc imaginary supercompile smp spectral real parallel mk
dist :: nofib-dist-pre
include $(TOP)/mk/target.mk
......
TOP = ..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = bernouilli exp3_8 gen_regexps integrate paraffins primes queens \
SUBDIRS = bernouilli digits-of-e1 digits-of-e2 exp3_8 gen_regexps integrate paraffins primes queens \
rfib tak wheel-sieve1 wheel-sieve2 x2n1
OTHER_SUBDIRS = digits-of-e1 digits-of-e2
include $(TOP)/mk/target.mk
......@@ -22,6 +22,7 @@ neg_powers =
pascal:: [[Integer]]
pascal = [1,2,1] : map (\line -> zipWith (+) (line++[0]) (0:line)) pascal
{- {-# SUPERCOMPILE bernoulli #-} -}
bernoulli 0 = 1
bernoulli 1 = -(1%2)
bernoulli n | odd n = 0
......@@ -33,6 +34,7 @@ bernoulli n =
| (k,combs)<- zip [2..n] pascal]
where powers = (neg_powers!!(n-1))
{-# SUPERCOMPILE main #-}
main = do
[arg] <- getArgs
let n = (read arg)::Int
......
......@@ -6,5 +6,7 @@ include $(TOP)/mk/boilerplate.mk
SRCS=Main.hs
PROG_ARGS += 500
SRC_SUPERCOMP_HC_OPTS =
include $(TOP)/mk/target.mk
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 450
NORM_OPTS = 1000
SLOW_OPTS = 1400
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 450
NORM_OPTS = 2000
SLOW_OPTS = 2700
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 8
NORM_OPTS = 8
SLOW_OPTS = 9
SRC_SUPERCOMP_HC_OPTS =
......@@ -2,3 +2,6 @@ TOP = ../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
# Seems to loop with this:
#SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 5000
NORM_OPTS = 50000
SLOW_OPTS = 100000
SRC_SUPERCOMP_HC_OPTS =
......@@ -12,3 +12,6 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 17
NORM_OPTS = 17
SLOW_OPTS = 19
# Seems to loop like this:
#SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 1500
NORM_OPTS = 1500
SLOW_OPTS = 5500
SRC_SUPERCOMP_HC_OPTS =
......@@ -8,3 +8,5 @@ SRCS = Main.hs
FAST_OPTS = 10
NORM_OPTS = 10
SLOW_OPTS = 12
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 30
NORM_OPTS = 30
SLOW_OPTS = 35
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,6 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 27 16 8
NORM_OPTS = 24 16 8
SLOW_OPTS = 33 17 8
# Goes off to infinity with +VE information even if rollback is off
SRC_SUPERCOMP_HC_OPTS = -fsupercompiler-no-positive-information
......@@ -6,3 +6,6 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 20000
NORM_OPTS = 100000
SLOW_OPTS = 230000
# Seems to loop with this:
#SRC_SUPERCOMP_HC_OPTS =
......@@ -10,3 +10,6 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 8000
NORM_OPTS = 20000
SLOW_OPTS = 30000
# Seems to loop like this:
#SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 10000
NORM_OPTS = 10000
SLOW_OPTS = 80000
SRC_SUPERCOMP_HC_OPTS =
\ No newline at end of file
......@@ -59,11 +59,15 @@ endif
# All the standard gluing together, as in the comment right at the front
SRC_SUPERCOMP_HC_OPTS = -fsupercompiler-bound-steps
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)
......
......@@ -44,7 +44,7 @@ ifneq "$(HC_FAIL)" "YES"
ifneq "$(NoFibWithGHCi)" "YES"
$(NOFIB_PROG_WAY) : $(OBJS)
@echo ==nofib$(_way)== $(NOFIB_PROG): time to link $(NOFIB_PROG) follows...
@$(TIME) $(HC) $(HC_OPTS) -o $@ $^ $(LIBS)
$(TIME) $(HC) $(HC_OPTS) -o $@ $^ $(LIBS)
endif
endif
......
......@@ -27,6 +27,9 @@ import Data.List
-----------------------------------------------------------------------------
-- Top level stuff
mAX_PROG_NAME_LENGTH :: Int
mAX_PROG_NAME_LENGTH = 20
die :: String -> IO a
die s = hPutStr stderr s >> exitWith (ExitFailure 1)
......@@ -114,12 +117,14 @@ data PerModuleTableSpec =
(a -> Bool) -- Result within reasonable limits?
-- The various per-program aspects of execution that we can generate results for.
size_spec, alloc_spec, runtime_spec, elapsedtime_spec, muttime_spec, mutetime_spec,
size_spec, modsize_spec, alloc_spec, runtime_spec, elapsedtime_spec, muttime_spec, mutetime_spec,
gctime_spec, gcelap_spec,
gcwork_spec, instrs_spec, mreads_spec, mwrite_spec, cmiss_spec,
gc0time_spec, gc0elap_spec, gc1time_spec, gc1elap_spec, balance_spec, totmem_spec
:: PerProgTableSpec
size_spec = SpecP "Binary Sizes" "Size" "binary-sizes" binary_size compile_status always_ok
modsize_spec = SpecP "Module Sizes" "ModSize" "module-sizes" total_module_size compile_status always_ok
modctime_spec = SpecP "Module Compile Times" "ModCTime" "module-ctimes" total_module_ctime compile_status always_ok
alloc_spec = SpecP "Allocations" "Allocs" "allocations" (meanInt allocs) run_status always_ok
runtime_spec = SpecP "Run Time" "Runtime" "run-times" (mean run_time) run_status mean_time_ok
elapsedtime_spec = SpecP "Elapsed Time" "Elapsed" "elapsed-times" (mean elapsed_time) run_status mean_time_ok
......@@ -144,6 +149,8 @@ totmem_spec = SpecP "Total Memory in use" "TotalMem" "total-mem" (meanInt tota
all_specs :: [PerProgTableSpec]
all_specs = [
size_spec,
modsize_spec,
modctime_spec,
alloc_spec,
runtime_spec,
elapsedtime_spec,
......@@ -211,7 +218,7 @@ checkTimes prog results = do
-- These are the per-prog tables we want to generate
per_prog_result_tab :: [PerProgTableSpec]
per_prog_result_tab =
[ size_spec, alloc_spec, runtime_spec, elapsedtime_spec, muttime_spec, mutetime_spec, gctime_spec,
[ size_spec, modsize_spec, modctime_spec, alloc_spec, runtime_spec, elapsedtime_spec, muttime_spec, mutetime_spec, gctime_spec,
gcelap_spec, gc0count_spec, gc0time_spec, gc0elap_spec, gc1count_spec, gc1time_spec, gc1elap_spec,
gcwork_spec, balance_spec, instrs_spec, mreads_spec, mwrite_spec, cmiss_spec, totmem_spec]
......@@ -219,11 +226,12 @@ per_prog_result_tab =
-- aspects, each in its own column. Only works when comparing two runs.
normal_summary_specs :: [PerProgTableSpec]
normal_summary_specs =
[ size_spec, alloc_spec, runtime_spec, elapsedtime_spec, totmem_spec ]
--[ size_spec, modsize_spec, alloc_spec, runtime_spec, elapsedtime_spec, totmem_spec ]
[ modctime_spec, runtime_spec, alloc_spec, modsize_spec ]
cachegrind_summary_specs :: [PerProgTableSpec]
cachegrind_summary_specs =
[ size_spec, alloc_spec, instrs_spec, mreads_spec, mwrite_spec ]
[ size_spec, modsize_spec, alloc_spec, instrs_spec, mreads_spec, mwrite_spec ]
-- Pick an appropriate summary table: if we're cachegrinding, then
-- we're probably not interested in the runtime, but we are interested
......@@ -517,7 +525,7 @@ asciiGenModTable results args (SpecM long_name _ get_result result_ok)
ascii_header :: Int -> [String] -> ShowS
ascii_header w ss
= str "\n-------------------------------------------------------------------------------\n"
. str (rjustify 15 "Program")
. str (rjustify mAX_PROG_NAME_LENGTH "Program")
. str (space 5)
. foldr (.) id (map (str . rjustify w) ss)
. str "\n-------------------------------------------------------------------------------\n"
......@@ -617,7 +625,7 @@ mungeForLaTeX = map transrow
table_layout :: Int -> Int -> Layout
table_layout n w boxes = foldr (.) id $ zipWith ($) fns boxes
where fns = (str . rjustify 15 . show ) :
where fns = (str . rjustify mAX_PROG_NAME_LENGTH . show ) :
(\s -> str (space 5) . str (rjustify w (show s))) :
replicate (n-1) (str . rjustify w . show)
......@@ -678,7 +686,7 @@ show_per_prog_results = show_per_prog_results_width fIELD_WIDTH
show_per_prog_results_width :: Int -> (String, [BoxValue]) -> ShowS
show_per_prog_results_width w (prog,results)
= str (rjustify 15 prog)
= str (rjustify mAX_PROG_NAME_LENGTH prog)
. str (space 5)
. foldr (.) id (map (str . rjustify w . showBox) results)
......@@ -824,7 +832,7 @@ calc_minmax xs
| otherwise = (Percentage (minimum percentages),
Percentage (maximum percentages))
where
percentages = [ if f < 5 then 5 else f | Percentage f <- xs ]
percentages = [ f | Percentage f <- xs ]
-----------------------------------------------------------------------------
......@@ -937,9 +945,18 @@ latexTableLayout boxes =
foldr (.) id . intersperse (str " & ") . map abox $ boxes
where
abox (RunFailed NotDone) = id
abox s = str (foldr transchar "" (show s))
transchar '%' s = s -- leave out the percentage signs
abox s = str (meh (show s))
-- HACK
meh "AccumulatingParam" = "Accumulator"
meh "AccumulatingParam-Peano" = "%"
meh "Generalisation" = "%"
meh "SumSquare-Explicit" = "%"
meh "queens-explicit" = "%"
meh "0.00" = "N/A"
meh s = foldr transchar "" s
transchar '%' s = "\\%" ++ s -- escape the percentage signs
transchar c s = c : s
-- -----------------------------------------------------------------------------
......
......@@ -4,9 +4,10 @@
--
-----------------------------------------------------------------------------
module Slurp (Status(..), Results(..), ResultTable, parse_log) where
module Slurp (Status(..), Results(..), ResultTable, parse_log, total_module_size, total_module_ctime) where
import Control.Monad
import qualified Data.Foldable as Foldable
import qualified Data.Map as Map
import Data.Map (Map)
import Data.List (isPrefixOf)
......@@ -56,6 +57,16 @@ data Results = Results {
total_memory :: [Integer]
}
total_module_size :: Results -> Maybe Int
total_module_size r
| Map.null (module_size r) = Nothing
| otherwise = Just (Foldable.sum (module_size r))
total_module_ctime :: Results -> Maybe Float
total_module_ctime r
| Map.null (compile_time r) = Nothing
| otherwise = Just (Foldable.sum (compile_time r))
emptyResults :: Results
emptyResults = Results {
compile_time = Map.empty,
......
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 1
NORM_OPTS = 1
SLOW_OPTS = 300
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ NORM_OPTS = 1000
SLOW_OPTS = 1700
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -7,3 +7,4 @@ FAST_OPTS = 1
NORM_OPTS = 1
SLOW_OPTS = 1
SRC_SUPERCOMP_HC_OPTS =
......@@ -10,6 +10,7 @@
-}
module QSort(sortLe, sort) where
sortLe :: (a -> a -> Bool) -> [a] -> [a]
sortLe le l = qsort le l []
......
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 20
NORM_OPTS = 20
SLOW_OPTS = 300
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 1993 2000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 8 1000
SRC_RUNTEST_OPTS += +RTS -H30m -RTS
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 7
NORM_OPTS = 7
SLOW_OPTS = 100
SRC_SUPERCOMP_HC_OPTS =
......@@ -8,3 +8,5 @@ SLOW_OPTS = 10
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ SRC_HC_OPTS += -fglasgow-exts
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -2,3 +2,5 @@ TOP = ../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
TOP = ../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 512
NORM_OPTS = 512
SLOW_OPTS = 1500
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ NORM_OPTS = 5000
SLOW_OPTS = 60000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -2,3 +2,5 @@ TOP = ../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 200
NORM_OPTS = 200
SLOW_OPTS = 500
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 13
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 1500000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 8
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -8,3 +8,5 @@ NORM_OPTS = 7
SLOW_OPTS = 11
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 6
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SRC_HC_OPTS += -cpp -fglasgow-exts
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SRC_HC_OPTS += -cpp -fglasgow-exts
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SRC_RUNTEST_OPTS += -o1 nucleic2.stdout1 -o1 nucleic2.stdout2
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -8,3 +8,5 @@ SRC_HC_OPTS += -cpp -fglasgow-exts -H80M
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 14
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 15
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 1000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 1200
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 500
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 6000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ NORM_OPTS = -2100000000 4000001 2100000000
SLOW_OPTS = -2100000000 4000001 2100000000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -9,3 +9,5 @@ SLOW_OPTS = 32 6
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ include $(TOP)/mk/boilerplate.mk
PROG_ARGS = 1600
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ NORM_OPTS = 1 2 1000 500 501 1500
SLOW_OPTS = 1 2 2000 1000 1001 3000
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -10,3 +10,5 @@ SRCS = Main.lhs Mandel.lhs PortablePixmap.lhs
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -11,3 +11,5 @@ PROG_ARGS = holzhausen.prob
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 16
NORM_OPTS = 16
SLOW_OPTS = 64
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ PROG_ARGS = input-data
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -7,3 +7,5 @@ FAST_OPTS = 50
NORM_OPTS = 50
SLOW_OPTS = 52
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -4,3 +4,5 @@ include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
# fast/norm/slow stuff done with separate stdin files
SRC_SUPERCOMP_HC_OPTS =
......@@ -2,3 +2,5 @@ TOP = ../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -6,3 +6,5 @@ include $(TOP)/mk/target.mk
FAST_OPTS = 2000
NORM_OPTS = 2000
SLOW_OPTS = 60000
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
SRC_HC_OPTS += -fglasgow-exts
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -10,3 +10,5 @@ Main_HC_OPTS = -H110m
SRC_RUNTEST_OPTS += +RTS -K3m -H20m -RTS
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -5,3 +5,5 @@ STDIN_FILE = Sort.hs
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -13,3 +13,5 @@ endif
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -7,3 +7,5 @@ PROG_ARGS = 27000.1 27000.2
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
......@@ -3,3 +3,5 @@ include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/target.mk
SRC_SUPERCOMP_HC_OPTS =
TOP = ..
include $(TOP)/mk/boilerplate.mk
#SUBDIRS = compile-time contracts ilya jason neil peter toys
# The ilya tests are for program equivalence
SUBDIRS = neil peter toys
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))
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.