Large inductive enum timeouts

Stream: lean4

[Pedro Oliveira]

Whilst creating some libclang bindings I've come across a problem: I want to port a large enum from libclang (https://clang.llvm.org/doxygen/group__CINDEX.html#gaaccc432245b4cd9f2d470913f9ef0013) and I thought that an inductive type would fit best.

1   inductive CursorKind where
2   | UnexposedDecl
3   | StructDecl
4   | UnionDecl
...
285 | ConceptDecl
286 | FirstExtraDecl
287 | LastExtraDecl
288 | OverloadCandidate

This compiles fine, but when I create a simple fromNat function for CursorKind:

def fromNat : Nat → CursorKind
| 1 => UnexposedDecl
| 2 => StructDecl
| 3 => UnionDecl
...
| 604 => ConceptDecl
| 700 => OverloadCandidate
| _ => OverloadCandidate

The compiler seems to struggle with this definition:

CursorKind.lean:293:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:293:0: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:293:0: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:292:4: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

I don't feel like setting the maximum heartbeats will help. What's the alternative to an inductive type here?

[Mario Carneiro]

it sounds like the issue is not the inductive type but rather the Nat pattern match

[Mario Carneiro]

does it work if you replace all the match arms by ()?

[Pedro Oliveira]

I think that it's the Nat pattern match too

[Pedro Oliveira]

When I replace the match arms, since they're all just redundant alternatives I can't actually compile the program

[Mario Carneiro]

I mean the RHS of the arms

[Pedro Oliveira]

Same error message as before:

CursorKind.lean:293:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:293:0: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:293:0: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
CursorKind.lean:292:4: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)```

[Pedro Oliveira]

Seems to be the Nat patterns

[Mario Carneiro]

Probably increasing the timeout will actually work, although it's not a great solution

[Mario Carneiro]

You could put all the options in an array and index into it

[Pedro Oliveira]

Yeah, I personally dislike increasing the timeout though. Another solution is just to use raw numbers instead of naturals, or to generate lots of constants

[Mario Carneiro]

Oh I see, it's just a bunch of constants

[Mario Carneiro]

that will probably work better

[Mario Carneiro]

you can use a macro to automate that kind of thing

[Pedro Oliveira]

Ill try this out

[Pedro Oliveira]

Although I can't see why lean struggles to pattern match the Nats

[Pedro Oliveira]

I ended up just writing a macro for enumerations:

syntax enumPair := ident "=" term
syntax "enum" ident "where" enumPair,+ : command

macro_rules
| `(enum $name:ident where $[$a = $b],*) => do
  let defs ← (a.zip b).foldlM (init := ← `(namespace $name)) fun ns (a, b) =>
    `($ns
      def $a := $b)
  `($defs:command
    end $name)

enum CursorKind where
  CXCursor_UnexposedDecl = 1,
  CXCursor_StructDecl = 2,
  CXCursor_UnionDecl = 3,
  CXCursor_ClassDecl = 4,
  CXCursor_EnumDecl = 5,
  CXCursor_FieldDecl = 6,
  CXCursor_EnumConstantDecl = 7,
  CXCursor_FunctionDecl = 8,
  CXCursor_VarDecl = 9,
  CXCursor_ParmDecl = 10,
  CXCursor_ObjCInterfaceDecl = 11,
  ...
  CXCursor_FirstExtraDecl = CXCursor_ModuleImportDecl,
  CXCursor_LastExtraDecl = CXCursor_ConceptDecl,
  CXCursor_OverloadCandidate = 700