From daf208326af0a85712775cd0c983da6bac5313a6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 1 Apr 2019 17:23:14 +0200
Subject: [PATCH] test(tests/playground): expander performance tests

---
 tests/playground/expander.lean      | 39 +++++++++++++++++++++++++++++
 tests/playground/view_expander.lean | 37 +++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)
 create mode 100644 tests/playground/expander.lean
 create mode 100644 tests/playground/view_expander.lean

diff --git a/tests/playground/expander.lean b/tests/playground/expander.lean
new file mode 100644
index 0000000000..885bc18372
--- /dev/null
+++ b/tests/playground/expander.lean
@@ -0,0 +1,39 @@
+import init.lean.expander
+
+open Lean
+open Lean.Parser
+open Lean.Expander
+
+def prof {α : Type} (msg : String) (p : IO α) : IO α :=
+let msg₁ := "Time for '" ++ msg ++ "':" in
+let msg₂ := "Memory usage for '" ++ msg ++ "':" in
+allocprof msg₂ (timeit msg₁ p)
+
+def node : SyntaxNodeKind := ⟨`node⟩
+def leaf : SyntaxNodeKind := ⟨`leaf⟩
+
+def node.arity := 4
+
+def mkStx : ℕ → Syntax
+| 0 := Syntax.mkNode leaf []
+| (n+1) := Syntax.mkNode node $ (List.replicate node.arity Syntax.missing).map (λ _, mkStx n)
+
+def cfg : FrontendConfig := {filename := "foo", fileMap := FileMap.fromString "", input := ""}
+
+def test (transformers : List (Name × transformer)) (stx : Syntax) : IO Unit :=
+match expand stx {cfg with transformers := RBMap.fromList transformers _} with
+| Except.ok _ := pure ()
+| Except.error e := throw e.toString
+
+def testNoOp  := test []
+def testNoExp := test [(`node, λ stx, noExpansion)]
+def testSimple := test [(`node, λ stx, match stx.asNode with
+  | some n := pure $ Syntax.mkNode ⟨`node2⟩ n.args
+  | none   := pure Syntax.missing)]
+
+def main (xs : List String) : IO Unit := do
+  let stx := mkStx 11, --xs.head.toNat,
+  prof "testNoOp" $ testNoOp stx,
+  prof "testNoExp" $ testNoExp stx,
+  prof "testSimple" $ testSimple stx,
+  pure ()
diff --git a/tests/playground/view_expander.lean b/tests/playground/view_expander.lean
new file mode 100644
index 0000000000..bff152690e
--- /dev/null
+++ b/tests/playground/view_expander.lean
@@ -0,0 +1,37 @@
+import init.lean.expander
+
+open Lean
+open Lean.Parser
+open Lean.Expander
+
+def prof {α : Type} (msg : String) (p : IO α) : IO α :=
+let msg₁ := "Time for '" ++ msg ++ "':" in
+let msg₂ := "Memory usage for '" ++ msg ++ "':" in
+allocprof msg₂ (timeit msg₁ p)
+
+@[derive HasView] def leaf.Parser : termParser := node! leaf ["foo"]
+@[derive HasView] def node.Parser : termParser := node! node [children: Combinators.many Term.Parser]
+
+def node.arity := 4
+
+def mkStx : ℕ → Syntax
+| 0 := review leaf {}
+| (n+1) := review node $ ⟨(List.replicate node.arity Syntax.missing).map (λ _, mkStx n)⟩
+
+def cfg : FrontendConfig := {filename := "foo", fileMap := FileMap.fromString "", input := ""}
+
+def test (transformers : List (Name × transformer)) (stx : Syntax) : IO Unit :=
+match expand stx {cfg with transformers := RBMap.fromList transformers _} with
+| Except.ok _ := pure ()
+| Except.error e := throw e.toString
+
+def testNoOp  := test []
+def testNoExp := test [(`node, λ stx, noExpansion)]
+def testSimple := test [(`node, λ stx, pure $ Syntax.mkNode ⟨`node2⟩ $ let v := view node stx in v.children)]
+
+def main (xs : List String) : IO Unit := do
+  let stx := mkStx 11, --xs.head.toNat,
+  prof "testNoOp" $ testNoOp stx,
+  prof "testNoExp" $ testNoExp stx,
+  prof "testSimple" $ testSimple stx,
+  pure ()