feat(bin/lean-gdb): show expr_cell members

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