From 1ef75a9ba67e65743cc1b2572aa1f291869b8e55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jan 2014 18:04:22 -0800 Subject: [PATCH] test(tests/lua): add test/example that demonstrates how to collect statistics of used theorems Signed-off-by: Leonardo de Moura --- tests/lua/proof_stats.lua | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 tests/lua/proof_stats.lua diff --git a/tests/lua/proof_stats.lua b/tests/lua/proof_stats.lua new file mode 100644 index 000000000..a66602d6f --- /dev/null +++ b/tests/lua/proof_stats.lua @@ -0,0 +1,23 @@ +parse_lean_cmds([[ +variables a b c d e f : Nat +rewrite_set simple +add_rewrite Nat::mul_assoc Nat::mul_comm Nat::mul_left_comm Nat::add_assoc Nat::add_comm Nat::add_left_comm + Nat::distributer Nat::distributel : simple +]]) +local t = parse_lean("(a + b) * (c + d) * (e + f) * (a + b) * (c + d) * (e + f)") +local t2, pr = simplify(t, "simple") +print(t) +-- Now, we traverse the proof and collect statistics on how often each theorem is used +m = splay_map() +pr:for_each( + function(e, ctx) + if e:is_app() and e:arg(0):is_constant() then + local n = e:arg(0):fields() + local c = m:find(n) + if not c then + c = 0 + end + m:insert(n, c+1) + end + end) +m:for_each(function(k, v) print(tostring(k) .. " ==> " .. tostring(v)) end)