From 9ec570416dde03d91ae1cd8c1fd60175dd4f8363 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 29 May 2019 17:55:54 +0200 Subject: [PATCH] chore(tests/bench): rename benchmarks --- tests/bench/Makefile | 17 ++- .../{expr_const_folding.hs => const_fold.hs} | 0 ...xpr_const_folding.lean => const_fold.lean} | 0 .../{expr_const_folding.ml => const_fold.ml} | 0 ...{expr_const_folding.sml => const_fold.sml} | 0 ...r_const_folding.swift => const_fold.swift} | 0 .../bench/{unionfind2.lean => unionfind.lean} | 0 tests/bench/unionfind1.lean | 132 ------------------ 8 files changed, 8 insertions(+), 141 deletions(-) rename tests/bench/{expr_const_folding.hs => const_fold.hs} (100%) rename tests/bench/{expr_const_folding.lean => const_fold.lean} (100%) rename tests/bench/{expr_const_folding.ml => const_fold.ml} (100%) rename tests/bench/{expr_const_folding.sml => const_fold.sml} (100%) rename tests/bench/{expr_const_folding.swift => const_fold.swift} (100%) rename tests/bench/{unionfind2.lean => unionfind.lean} (100%) delete mode 100644 tests/bench/unionfind1.lean diff --git a/tests/bench/Makefile b/tests/bench/Makefile index 9210f688d5..14fa204ccd 100644 --- a/tests/bench/Makefile +++ b/tests/bench/Makefile @@ -1,7 +1,7 @@ ## CONFIG -LEAN_BENCHES = binarytrees deriv expr_const_folding frontend qsort rbmap rbmap_checkpoint_10 rbmap_shared unionfind2 -CROSS_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared +LEAN_BENCHES = binarytrees deriv const_fold frontend qsort rbmap rbmap_10 rbmap_1 unionfind +CROSS_BENCHES = binarytrees deriv const_fold qsort rbmap rbmap_10 rbmap_1 LEAN_CATS = .lean .no_reuse.lean .no_borrow.lean .no_st.lean CROSS_CATS = .lean .gc.lean .lean.perf .hs .gc.hs .hs.perf .ml .gc.ml .ml.perf .mlton .gc.mlton .mlton.perf .mlkit .gc.mlkit .mlkit.perf @@ -100,14 +100,13 @@ bench/qsort.%.bench: BENCH_PARAMS = 400 bench/rbmap.%.bench: BENCH_PARAMS = 2000000 -rbmap_shared.%.out: rbmap_checkpoint.%.out; ln -f $< $@ -bench/rbmap_shared.%.bench: BENCH_PARAMS = 2000000 1 +rbmap_1.%.out: rbmap_checkpoint.%.out; ln -f $< $@ +bench/rbmap_1.%.bench: BENCH_PARAMS = 2000000 1 -rbmap_checkpoint_10.%.out: rbmap_checkpoint.%.out; ln -f $< $@ -bench/rbmap_checkpoint_10.%.bench: BENCH_PARAMS = 2000000 10 +rbmap_10.%.out: rbmap_checkpoint.%.out; ln -f $< $@ +bench/rbmap_10.%.bench: BENCH_PARAMS = 2000000 10 -bench/unionfind1.%.bench: BENCH_PARAMS = 3000000 -bench/unionfind2.%.bench: BENCH_PARAMS = 3000000 +bench/unionfind.%.bench: BENCH_PARAMS = 3000000 bench/%gc.lean.bench: %lean.out | bench ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS)\ @@ -186,7 +185,7 @@ report_cross.csv: bench_cross BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@ column -s';' -t < $@ -TO_TEX = 's/unionfind2/unionfind/;s/expr_const_folding/const_fold/;s/rbmap_checkpoint/rbmap/;s/rbmap_shared/rbmap_1/;s/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/' +TO_TEX = 's/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/' report_%.tex: report_%.csv tail -n +2 $< | head -n -1 | sed 's/^\([^;]\+\)/\\verb!\1!/;'$(TO_TEX) > $@ echo -n '\midrule ' >> $@ diff --git a/tests/bench/expr_const_folding.hs b/tests/bench/const_fold.hs similarity index 100% rename from tests/bench/expr_const_folding.hs rename to tests/bench/const_fold.hs diff --git a/tests/bench/expr_const_folding.lean b/tests/bench/const_fold.lean similarity index 100% rename from tests/bench/expr_const_folding.lean rename to tests/bench/const_fold.lean diff --git a/tests/bench/expr_const_folding.ml b/tests/bench/const_fold.ml similarity index 100% rename from tests/bench/expr_const_folding.ml rename to tests/bench/const_fold.ml diff --git a/tests/bench/expr_const_folding.sml b/tests/bench/const_fold.sml similarity index 100% rename from tests/bench/expr_const_folding.sml rename to tests/bench/const_fold.sml diff --git a/tests/bench/expr_const_folding.swift b/tests/bench/const_fold.swift similarity index 100% rename from tests/bench/expr_const_folding.swift rename to tests/bench/const_fold.swift diff --git a/tests/bench/unionfind2.lean b/tests/bench/unionfind.lean similarity index 100% rename from tests/bench/unionfind2.lean rename to tests/bench/unionfind.lean diff --git a/tests/bench/unionfind1.lean b/tests/bench/unionfind1.lean deleted file mode 100644 index e45de9703d..0000000000 --- a/tests/bench/unionfind1.lean +++ /dev/null @@ -1,132 +0,0 @@ -def StateT' (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ) -namespace StateT' -variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type} -@[inline] protected def pure (a : α) : StateT' m σ α := λ ⟨_, s⟩, pure (a, s) -@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := λ p, do (a, s') ← x p, f a ((), s') -@[inline] def read : StateT' m σ σ := λ ⟨_, s⟩, pure (s, s) -@[inline] def write (s' : σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), s') -@[inline] def updt (f : σ → σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), f s) -instance : Monad (StateT' m σ) := -{pure := @StateT'.pure _ _ _, bind := @StateT'.bind _ _ _} -end StateT' - -def ExceptT' (m : Type → Type) (ε : Type) (α : Type) := Except Unit Unit → m (Except ε α) -namespace ExceptT' -variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type} -@[inline] protected def pure (a : α) : ExceptT' m ε α := -λ e, match e with - | Except.ok _ := pure (Except.ok a) - | Except.error _ := pure (Except.ok a) -@[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β := -λ e, do v ← x e, match v with - | Except.error e := pure (Except.error e) - | Except.ok a := f a (Except.ok ()) -@[inline] def error (e : ε) : ExceptT' m ε α := -λ e', match e' with - | Except.ok _ := pure (Except.error e) - | Except.error _ := pure (Except.error e) -@[inline] def lift (x : m α) : ExceptT' m ε α := λ e, do {a ← x, pure (Except.ok a)} -instance : Monad (ExceptT' m ε) := -{pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _} -end ExceptT' - -abbreviation Node := Nat - -structure nodeData := -(find : Node) (rank : Nat := 0) - -abbreviation ufData := Array nodeData - -abbreviation M (α : Type) := ExceptT' (StateT' Id ufData) String α -@[inline] def read : M ufData := ExceptT'.lift StateT'.read -@[inline] def write (s : ufData) : M Unit := ExceptT'.lift (StateT'.write s) -@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT'.lift (StateT'.updt f) -@[inline] def error {α : Type} (e : String) : M α := ExceptT'.error e -def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData := -x (Except.ok ()) ((), s) - -def capacity : M Nat := -do d ← read, pure d.size - -def findEntryAux : Nat → Node → M nodeData -| 0 n := error "out of fuel" -| (i+1) n := - do s ← read, - if h : n < s.size then - do { let e := s.fget ⟨n, h⟩, - if e.find = n then pure e - else do e₁ ← findEntryAux i e.find, - updt (λ s, s.set n e₁), - pure e₁ } - else error "invalid Node" - -def findEntry (n : Node) : M nodeData := -do c ← capacity, - findEntryAux c n - -def find (n : Node) : M Node := -do e ← findEntry n, pure e.find - -def mk : M Node := -do n ← capacity, - updt $ λ s, s.push {find := n, rank := 1}, - pure n - -def union (n₁ n₂ : Node) : M Unit := -do r₁ ← findEntry n₁, - r₂ ← findEntry n₂, - if r₁.find = r₂.find then pure () - else updt $ λ s, - if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find } - else if r₁.rank = r₂.rank then - let s₁ := s.set r₁.find { find := r₂.find } in - s₁.set r₂.find { rank := r₂.rank + 1, .. r₂} - else s.set r₂.find { find := r₁.find } - - -def mkNodes : Nat → M Unit -| 0 := pure () -| (n+1) := mk *> mkNodes n - -def checkEq (n₁ n₂ : Node) : M Unit := -do r₁ ← find n₁, r₂ ← find n₂, - unless (r₁ = r₂) $ error "nodes are not equal" - -def mergePackAux : Nat → Nat → Nat → M Unit -| 0 _ _ := pure () -| (i+1) n d := - do c ← capacity, - if (n+d) < c - then union n (n+d) *> mergePackAux i (n+1) d - else pure () - -def mergePack (d : Nat) : M Unit := -do c ← capacity, mergePackAux c 0 d - -def numEqsAux : Nat → Node → Nat → M Nat -| 0 _ r := pure r -| (i+1) n r := - do c ← capacity, - if n < c - then do { n₁ ← find n, numEqsAux i (n+1) (if n = n₁ then r else r+1) } - else pure r - -def numEqs : M Nat := -do c ← capacity, - numEqsAux c 0 0 - -def test (n : Nat) : M Nat := -if n < 2 then error "input must be greater than 1" -else do - mkNodes n, - mergePack 50000, - mergePack 10000, - mergePack 5000, - mergePack 1000, - numEqs - -def main (xs : List String) : IO UInt32 := -let n := xs.head.toNat in -match run (test n) with -| (Except.ok v, s) := IO.println ("ok " ++ toString v) *> pure 0 -| (Except.error e, s) := IO.println ("Error : " ++ e) *> pure 1