From dad7de5578312ea02daebc15aeaf55feb0fa1611 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 7 Nov 2016 14:12:35 -0500
Subject: [PATCH] feat(bin/lean-gdb): show expr_cell members

---
 bin/lean-gdb.py | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/bin/lean-gdb.py b/bin/lean-gdb.py
index b530c110d9..a093a87090 100644
--- a/bin/lean-gdb.py
+++ b/bin/lean-gdb.py
@@ -59,9 +59,47 @@ class LeanBufferPrinter:
     def display_hint(self):
         return 'array'
 
+class LeanExprPrinter:
+    """Print a lean::expr object."""
+
+    expr_kinds = [
+        'lean::expr_var',
+        'lean::expr_sort',
+        'lean::expr_const',
+        'lean::expr_mlocal',
+        'lean::expr_mlocal',
+        'lean::expr_app',
+        'lean::expr_binding',
+        'lean::expr_binding',
+        'lean::expr_let',
+        'lean::expr_macro',
+    ]
+
+    def __init__(self, val):
+        kind = val['m_ptr']['m_kind']
+        subtype = gdb.lookup_type(LeanExprPrinter.expr_kinds[kind])
+        self.val = val['m_ptr'].cast(subtype.pointer()).dereference()
+
+    def to_string(self):
+        return str(self.val.type)
+
+    def children(self):
+        def deep_fields(v):
+            for f in v.type.fields():
+                if f.is_base_class:
+                    for g in deep_fields(v[f]):
+                        yield g
+                elif f.name == 'm_kind':
+                    yield (f.name, v[f].cast(gdb.lookup_type('lean::expr_kind')))
+                else:
+                    yield (f.name, v[f])
+
+        return deep_fields(self.val)
+
 def build_pretty_printer():
     pp = gdb.printing.RegexpCollectionPrettyPrinter("lean")
     pp.add_printer('name', '^lean::name$', LeanNamePrinter)
+    pp.add_printer('expr', '^lean::expr$', LeanExprPrinter)
     pp.add_printer('list', '^lean::list', LeanListPrinter)
     pp.add_printer('buffer', '^lean::buffer', LeanBufferPrinter)
     return pp