From e72bccb2e39691dcdba7d8eb89606f97e68020ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 17 Jul 2016 14:34:47 -0400
Subject: [PATCH] feat(library/vm/vm_list): add to_list

---
 src/library/vm/vm_list.h | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/library/vm/vm_list.h b/src/library/vm/vm_list.h
index b0fdc607ed..004be2ddd3 100644
--- a/src/library/vm/vm_list.h
+++ b/src/library/vm/vm_list.h
@@ -40,6 +40,17 @@ inline bool is_nil(vm_obj const & o) { return is_simple(o); }
 inline vm_obj head(vm_obj const & o) { lean_assert(!is_nil(o)); return cfield(o, 0); }
 inline vm_obj tail(vm_obj const & o) { lean_assert(!is_nil(o)); return cfield(o, 1); }
 
+template<typename A, typename F>
+list<A> to_list(vm_obj const & o, F const & fn) {
+    if (is_simple(o)) {
+        return list<A>();
+    } else if (is_constructor(o)) {
+        return list<A>(fn(cfield(o, 0)), to_list<A>(cfield(o, 1), fn));
+    } else {
+        lean_unreachable();
+    }
+}
+
 void initialize_vm_list();
 void finalize_vm_list();
 }