concise enum-with-values type

Stream: new members

[Daniel Windham]

@Graham Leach-Krouse and I are working on a binary file parser and there are lots of magic numbers. To stay organized, we parse these numbers into named enum values, and later serialize the enum values back to Nats. Modern software languages usually provide a concise way to define enums with values since it's a common pattern, but we're not sure how to write this concisely in Lean.

Right now we implement this with an inductive enum type, plus two separate functions toNat and fromNat, plus a pair of theorems that toNat $ fromNat and fromNat $ toNat are identities. It's a ton of boilerplate, and we have hundreds (or maybe thousands!) of magic numbers to deal with.

Instead, we'd like to write something like

inductive_with_values Weekday (_: Fin 7) where
  | sunday : Weekday := 0
  | monday : Weekday := 1
  | ...

#eval Weekday.sunday.value  -- 0
#eval Weekday.mk 0  -- Weekday.sunday
#check Weekday.value_of_mk  -- Weekday.value_of_mk (n: Nat) : (Weekday.mk n).value = n
#check Weekday.mk_of_value  -- Weekday.mk_of_value (w: Weekday) : Weekday.mk w.value = w

Also, in some cases, we need to map large number ranges to a common enum label and preserve the original value, e.g.:

inductive_with_values Vehicle (n: Nat) where
  | Volvo : Vehicle := 0
  | Hyundai : Vehicle := 1
  | ...
  | Tesla : Vehicle := 34
  | UnusedCar : Vehicle := n if 34 < n && n < 512
  | Boeing : Vehicle := 512
  | ...
  | Airbus : Vehicle := 528
  | UnusedPlane : Vehicle := n if 528 < n && n < 1024
  | Invalid : Vehicle := n  -- all remaining numbers

#eval Vehicle.mk 36  -- Vehicle.UnusedCar 36
#eval (Vehicle.mk 36).value  -- 36

Does something like this exist already? If not, any suggestions on how we can add it? Neither of us has written any metaprogramming yet. Thanks!

[Eric Wieser]

If your enum values are specifically Fin n, then FinEnum might work for you

[Eric Wieser]

Though it's a rather unloved bit of API that needs some work

[Marcus Rossel]

Here's a makeshift enum macro that covers the basic case:

import Lean
open Lean Parser Command

declare_syntax_cat enum_case
syntax "| " ident " := " term : enum_case

private def split (cases : TSyntaxArray `enum_case) : (Array Ident) × (Array Term) :=
  cases.foldl (init := (#[], #[])) fun (names, values) => fun
    | `(enum_case| | $name := $value) => (names.push name, values.push value)
    | _ => unreachable!

macro "enum" e:ident " : " ty:term (" where")? cases:enum_case* d:optDeriving : command => do
  let (names, values) := split cases
  let eIdent (suffix : Name) := mkIdentFrom e (e.getId ++ suffix)
  `(
    inductive $e:ident $[| $names:ident]* $d:optDeriving
    def $(eIdent `val) : $e → $ty $[| $names:ident => $values]*
    def $(eIdent `ofVal) : $ty → Option $e $[| $values => some $names]* | _ => none
    theorem $(eIdent `ofVal_val) (e : $e) : $(eIdent `ofVal) ($(eIdent `val) e) = e := by cases e <;> rfl
    theorem $(eIdent `val_ofVal) {n : $ty} {e : $e} (h : $(eIdent `ofVal) n = some e) : $(eIdent `val) e = n := by
      unfold $(eIdent `ofVal) at h
      split at h <;> injection h
      all_goals rename_i h; rw [←h]; rfl
  )

enum E : Nat where
  | one := 1
  | two := 2
  deriving Inhabited, BEq

#print E
#print E.val
#print E.ofVal
#check E.ofVal_val
#check E.val_ofVal

Or do you always know that your enum cases cover all possible values of the given type?

[Daniel Windham]

Thanks @Marcus Rossel , this is very helpful! (Sorry for my very delayed reply here.)

I'm trying to generalize this example to retain the original Nat value in the default case. I need to know that this retained value is a Nat that does not match any of the enumerated cases.

I'm getting stuck trying to dynamically construct an array syntax term from the user-provided data. How can I construct a TSyntax term like [1, 2] given an array of terms or an array of Nats?

Here's a simplified example:

macro "test" e:ident cases:enum_case* : command => do
  let (names, values) := splitArray cases -- values has type Array Term (same as previous post)
  let valuesHardcoded := [1, 2]
  `(
    -- def $e:ident := $values           -- fails, because rhs is expected to have type TSyntax `term
    -- def $e:ident := $valuesHardcoded  -- fails, because rhs is expected to have type TSyntax `term
    def $e:ident := [1, 2]
  )

test D
  | one := 1
  | two := 2

#print D -- def D : List Nat := [1, 2]

---

If it's useful, here is what I'm trying to achieve overall:

-- supporting definition
structure NatOtherThan (excluded : List Nat) where
  val  : Nat
  isOther : ¬excluded.contains val
  deriving BEq, Repr

example : NatOtherThan [1, 3, 4] := ⟨2, by intro h; cases h⟩

-- the user writes this:
enum EE (n: Nat) where
  | one := 1
  | three := 3
  | other := n

-- `enum` is desugared into this inductive type (plus supporting functions)
inductive EE
  | one
  | three
  | rest (n : NatOtherThan [1, 3])
  deriving Inhabited, BEq, Repr

example := (EE.rest ⟨2, by intro h; cases h⟩)

[Graham Leach-Krouse]

I played around with this a bit, and came up with the following, which should add a default "unknown" case and also allow docComments on the constructors. It's my first nontrivial macro though, so I'm guessing that it can be improved quite a bit...

import Lean
open Lean Parser Command

declare_syntax_cat enum_case
syntax (docComment)? " | " ident " := " term : enum_case

private def split (cases : TSyntaxArray `enum_case) : (Array Ident) × (Array Term) × (Array (Lean.TSyntax `Lean.Parser.Command.docComment)) :=
  cases.foldl (init := (#[], #[], #[])) fun (names, values, comments) => fun
    | `(enum_case| | $name := $value) => (names.push name, values.push value, comments.push emptyComment)
    | `(enum_case| $comment:docComment | $name := $value) => (names.push name, values.push value, comments.push comment)
    | _ => unreachable!
  where commentLeader : Lean.Syntax := Lean.Syntax.atom SourceInfo.none "/--"
        commentBody : Lean.Syntax := Lean.Syntax.atom SourceInfo.none "undocumented -/"
        emptyComment : Lean.TSyntax `Lean.Parser.Command.docComment := Lean.TSyntax.mk $
          Lean.Syntax.node SourceInfo.none `Lean.Parser.Command.docComment #[commentLeader, commentBody]

macro "enum" e:ident " : " ty:term (" where")? cases:enum_case* d:optDeriving : command => do
  let (names, values, comments) := split cases
  let eIdent (suffix : Name) := mkIdentFrom e (e.getId ++ suffix)
  `(
    inductive $e:ident $[$comments:docComment | $names:ident]* | unknown (x:$ty) $d:optDeriving
    def $(eIdent `val) : $e → $ty $[| $names:ident => $values]* | unknown x => x
    def $(eIdent `ofVal) : $ty → $e $[| $values => $names]* | x => unknown x

    instance : Coe $e $ty where coe := $(eIdent `val)

    /- theorem $(eIdent `ofVal_val) (e : $e) : $(eIdent `ofVal) ($(eIdent `val) e) = e := by cases e <;> try rfl <;> unfold $(eIdent `val) -/
    theorem $(eIdent `val_ofVal) {n : $ty} {e : $e} (h : $(eIdent `ofVal) n = some e) : $(eIdent `val) e = n := by
      unfold $(eIdent `ofVal) at h
      split at h <;> injection h
      all_goals rename_i h; rw [←h]; rfl
  )

[Marcus Rossel]

Daniel Windham said:

I'm getting stuck trying to dynamically construct an array syntax term from the user-provided data. How can I construct a TSyntax term like [1, 2] given an array of terms or an array of Nats?

What you're looking for is docs#Lean.Quote:

macro "one_two" : term => do
  let vals := [1, 2]
  let stx := Lean.quote vals
  `($stx)

#eval one_two -- [1, 2]

[Daniel Windham]

Perfect, thanks @Marcus Rossel.

[Marcus Rossel]

@Daniel Windham Here's an outline of a macro that follows the example you gave:

Macro

import Lean
open Lean Parser Command

declare_syntax_cat enum_case
syntax "| " ident " := " term : enum_case

private def split (cases : TSyntaxArray `enum_case) : MacroM <| (Array Ident) × (Array Term) :=
  cases.foldlM (init := (#[], #[])) fun (names, values) => fun
    | `(enum_case| | $name := $value) => do
      if name.getId == `other then Macro.throwErrorAt name "enum cases cannot be called 'other'"
      return (names.push name, values.push value)
    | _ => unreachable!

macro "enum" e:ident " : " ty:term (" where")? cases:enum_case* d:optDeriving : command => do
  let (names, values) ← split cases
  let eIdent (suffix : Name) := mkIdentFrom e (e.getId ++ suffix)
  let otherIdent := mkIdent `other
  `(
    inductive $e:ident
      $[| $names:ident]*
      | $otherIdent:ident (n : $ty) : n ∉ $(quote values.toList) → $e
      $d:optDeriving
    def $(eIdent `val) : $e → $ty
      $[| $names:ident => $values]*
      | $otherIdent n _ => n
    def $(eIdent `ofVal) (v : $ty) : $e :=
      match h : v with
      $[| $values => $names]*
      | n => $otherIdent n sorry
  )

enum E : Nat where
  | one := 1
  | two := 2
  deriving Inhabited, BEq

#print E
#print E.val
#print E.ofVal

Notably, I've removed the proofs, because I'm too lazy to figure them out. But I bet that's something you'll figure out.
Also, there's a sorry which should be a proof that the value appearing in other is not one of the other constructors' values. I'm not sure how to get that info in a match statement. I was kind of expecting the hypothesis h to contain that info.

[Eric Wieser]

Often docs#Lean.toExpr is a better choice than Lean.quote

[Eric Wieser]

(with docs#Expr.toSyntax)

[Marcus Rossel]

Eric Wieser said:

Often docs#Lean.toExpr is a better choice than Lean.quote

Why is that?

[Eric Wieser]

There are more docs#Lean.ToExpr instances than docs#Lean.Quote

[Daniel Windham]

Thanks @Marcus Rossel and @Eric Wieser.

@Marcus Rossel, I also find it odd that the match statement doesn't have a hypothesis about n not being a previous value. Perhaps there's a more verbose form of match that captures this. Either way, here's what I've been doing instead. It's a bit more annoying for downstream proofs but it seems fine.

def E.ofValX : Nat → E2 := fun n =>
  if h : [1, 2].contains n then
    match n with
    | 1 => E.one
    | 2 => E.two
  else
    E.other ⟨n, h⟩

[Marcus Rossel]

@Daniel Windham Nice! Here's an updated version of the macro then:

Macro

import Lean
open Lean Parser Command

declare_syntax_cat enum_case
syntax "| " ident " := " term : enum_case

private def split (cases : TSyntaxArray `enum_case) : MacroM <| (Array Ident) × (Array Term) :=
  cases.foldlM (init := (#[], #[])) fun (names, values) => fun
    | `(enum_case| | $name := $value) => do
      if name.getId == `other then Macro.throwErrorAt name "enum cases cannot be called 'other'"
      return (names.push name, values.push value)
    | _ => unreachable!

macro "enum" e:ident " : " ty:term (" where")? cases:enum_case* d:optDeriving : command => do
  let (names, values) ← split cases
  let eIdent (suffix : Name) := mkIdentFrom e (e.getId ++ suffix)
  let otherIdent := mkIdent `other
  `(
    inductive $e:ident
      $[| $names:ident]*
      | $otherIdent:ident (n : $ty) : n ∉ $(quote values.toList) → $e
      $d:optDeriving
    def $(eIdent `val) : $e → $ty
      $[| $names:ident => $values]*
      | $otherIdent n _ => n
    def $(eIdent `ofVal) (v : $ty) : $e :=
      if h : v ∈ $(quote values.toList)
      then match v with $[| $values => $names]*
      else $otherIdent v h
  )

enum E : Nat where
  | one := 1
  | two := 2
  deriving Inhabited, BEq

#print E
#print E.val
#print E.ofVal

[Daniel Windham]

:thumbs_up:

[Daniel Windham]

For the basic case of enums, my macro works great.

But I'm struggling to write a more general macro where each constructor in the generated inductive type declaration is specified in one of two different patterns depending on its input data.

Here's an example:

enum MyEnum (n: Nat)
  | one => 1
  | small => n, 1 < n < 5
  | five => 5
  | big => n, 5 < n

should produce:

inductive MyEnum
  | one
  | small (n: Nat) (h: 1 < n < 5)
  | five
  | big (n: Nat) (h: 5 < n)

If none of the constructors had arguments, this would just be

`(inductive $e:ident $[| $names:ident]*)

If all of the constructors had arguments, this would be

`(inductive $e:ident $[| $names:ident (n : $ty) (h: $conditions)]*)

How can I generalize this to allow a mix of constructors with and without arguments, in any order?

[Marcus Rossel]

I think what I would do is to write the constructors in the form | name : α → β → ... → MyEnum. Then whenever there are no parameters you just omit the α → β → ... → part.

[Daniel Windham]

Hmm - I think I'm missing something obvious here. @Marcus Rossel that approach seems reasonable, but I don't know how to implement it.

Specifically, I can't figure out how to do either of the following:
(a) construct a TSyntax `term from a type. For instance, let t : TSyntax `term := Lean.quote Nat fails
(b) inline conditional logic within a `(...) expression, e.g. something like `(... | $names : $(if $params then `($params → ) ) MyEnum

For (a), is there a way to construct a syntax term with `(...)? Perhaps something like this?

let t: MacroM (TSyntax `term) := `(...)
let u : TSyntax `term := someFn t

[Daniel Windham]

Ah - let u : TSyntax `term <- `(...) does the trick.

If there's a way to do inline conditional logic within a `(...) expression, that would still be good to know.

Thanks!

[Eric Wieser]

You can, ← if x then `(foo) else `(bar)

[Daniel Windham]

@Eric Wieser , that's an example of inlining `(...) expressions within a condition. Is there a way to inline conditions within a `(...) expression? Otherwise for a large `(...) expression, all conditional logic needs to be constructed out of context in a bunch of prior variables, which makes for messy code.

[Marcus Rossel]

If you have an optional syntax object o, then its antiquotation syntax is $[$o]?. This is similar to how $[...]* is used for arrays/lists of syntax. I don't think there's anything specific for conditional expressions.

[Marcus Rossel]

What I was suggesting earlier was therefore to basically do all of the syntax computation beforehand. Given the enum entries, construct the lists names and ctorTypes where ctorTypes[i] is MyEnum when the case has no range and (n : Nat) -> (_ < _ < _) -> MyEnum when it does have a range. Then you can just use the regular syntax:

`(inductive $e:ident $[| $names:ident : $ctorTypes]*)

[Daniel Windham]

@Marcus Rossel thank you, I have that working now! Too bad about having to do all the syntax computation beforehand, but at least I can do what I need =]

[Marcus Rossel]

Would you mind posting your complete macro here? I'd be interested to see how it works :)

[Daniel Windham]

Sure - I haven't put the full pieces together yet but I will post here and tag you when I do!

[Daniel Windham]

Out of curiosity, what is the syntax type for a constructor case within an inductive declaration? Is this something Lean supports?

I could keep the code more organized if I was able to do something like:

def mkConstructor (...) : TSyntax `constructor :=
    if (...) then
        <- `(constructor| | $name:ident)`
    else
        <- `(constructor| | $name:ident (n: Nat) -> (h: _ < n < _))`

let constructors := data.map mkConstructor
`(inductive $e:ident $[constructors]*)

[Marcus Rossel]

Here's the complete syntax for inductive types: https://github.com/leanprover/lean4/blob/6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a/src/Lean/Parser/Command.lean#L161

So you either want ctor or optDeclSig.

[Daniel Windham]

Ah perfect, thanks! I saw that before and couldn't get it working. This works though:

  let x := ← `(ctor| | one (n: Nat) (h: 2 ≤ n ∧ n < 4) : $e:ident)
  let y := ← `(inductive $e:ident where $x)

[Graham Leach-Krouse]

For conditional splices/antiquotations, something like this seems to work:

  let cond  ← `(command| def x:= $(← if true then `(1) else `(2)))

[Daniel Windham]

Nice!

[Marcus Rossel]

I think that's exactly what @Eric Wieser was suggesting :sweat_smile:

[Daniel Windham]

Ah oops! The $(...) syntax was new to me

[Daniel Windham]

@Marcus Rossel / others, I finally got more time to work on this. Thanks again for all your help! Here's the result, starting with examples:

-- can mix literal, guarded, and match-all values. comments are optional
enum E (n: Nat)
  /-- one -/
  | one => 1
  | small => n, 2 ≤ n ∧ n < 4
  /-- four -/
  | four => 4
  /-- other -/
  | other => n

#eval E.four
#eval E.ofVal 4
#eval E.small 2 (by decide)
#eval (E.other 5 (by decide)).val
#eval (E.ofVal 5).val

-- proves round-trip identities for both ofVal ⬝ val and val ⬝ ofVal
#check E.ofVal_val
#check E.val_ofVal

-- works with types other than Nat
enum FinEnum (n: Fin 3)
  | zero => 0
  | one => 1
  | two => 2

#eval FinEnum.zero.val
#eval FinEnum.ofVal 0

-- adds a default case if it isn't given explicitly
enum ImplicitDefault (n: Nat)
  | one => 1
  | two => 2

#eval ImplicitDefault.default 5 (by decide)
#eval ImplicitDefault.ofVal 5

Here's (approximately) what the macro generates for the first example:

inductive E
  | one
  | small (n : Nat) (h: (2 ≤ n ∧ n < 4) ∧ ¬(n = 1))
  | four
  | other (n : Nat) (h: ¬(n = 1) ∧ ¬(2 ≤ n ∧ n < 4) ∧ ¬ (n = 4))
  deriving BEq, Inhabited

instance : Repr E where
  reprPrec := fun e _ => match e with
    | .one => "one"
    | .small n _ => s!"small {n}"
    | .four => "four"
    | .other n _ => s!"other {n}"

def E.val : E → Nat
  | E.one => 1
  | E.small n _ => n
  | E.four => 4
  | E.other n _ => n

def E.ofVal : Nat → E := fun n =>
  if _ : n = 1 then .one else
  if _ : 2 ≤ n ∧ n < 4 then .small n (by omega) else
  if _ : n = 4 then .four else
  if _ : true then .other n (by omega) else
  unreachable!

theorem E.ofVal_val (e : E) : E.ofVal (E.val e) = e := by
  cases e <;> try rfl
  all_goals rename _ => h; simp [E.val, E.ofVal, h]

theorem E.val_ofVal (n : Nat) : E.val (E.ofVal n) = n := by
  unfold E.ofVal
  repeat split; simp only [*, E.val]
  simp only [*, E.val]
  contradiction

And finally, here's the macro:

import Lean
open Lean Parser Command Syntax

declare_syntax_cat enum_case
syntax atomic((docComment)? " | " ident " => " ident ", " term) : enum_case
syntax (docComment)? " | " ident " => " term : enum_case

private inductive EnumCaseValue
  | literalValue (value : Term)
  | parametricValue (value : Ident) (cond : Term)
  deriving Inhabited

private structure EnumCaseParsed where
  name : Ident
  value : EnumCaseValue
  comment : Lean.TSyntax `Lean.Parser.Command.docComment
  deriving Inhabited

private def makeComment (comment: String) : Lean.TSyntax `Lean.Parser.Command.docComment :=
  let commentLeader : Lean.Syntax := Lean.Syntax.atom SourceInfo.none "/--"
  let commentBody : Lean.Syntax := Lean.Syntax.atom SourceInfo.none s!"{comment} -/"
  Lean.TSyntax.mk $ Lean.Syntax.node SourceInfo.none `Lean.Parser.Command.docComment #[commentLeader, commentBody]

private def parseCase (case : TSyntax `enum_case) : EnumCaseParsed :=
  match case with
    | `(enum_case| | $name => $value) => ⟨name, .literalValue value, emptyComment⟩
    | `(enum_case| | $name => $value, $cond) => ⟨name, .parametricValue value cond, emptyComment⟩
    | `(enum_case| $comment:docComment | $name => $value) => ⟨name, .literalValue value, comment⟩
    | `(enum_case| $comment:docComment | $name => $value, $cond) => ⟨name, .parametricValue value cond, comment⟩
    | _ => unreachable!
  where emptyComment := makeComment "undocumented"

private def parseCases (cases : TSyntaxArray `enum_case) : Array EnumCaseParsed :=
  cases.foldl (init := (#[])) fun (parsedCases) => fun (case) =>
    parsedCases.push (parseCase case)

-- TODO: prove termination.
-- Warning: this is not performant if there are many name collisions.
private partial def getUniqueName (base : String) (names : List String) : String :=
  let rec loop (i : Nat) : String :=
    let name := base ++ (if i == 0 then "" else s!"_{i}")
    if name ∈ names then loop (i + 1) else name
  loop 0

private def addCaseDefaults (n: Ident) (cases : Array EnumCaseParsed) : MacroM (Array EnumCaseParsed) := do
  -- Allow the final case to omit the true condition.
  let ⟨name, value, comment⟩ := cases.back
  let trueValue ← `(true)
  let defaultValue := EnumCaseValue.parametricValue n trueValue
  let (cases, lastValue) := match value with
  | .literalValue v      =>
      if v == n then (cases.pop.push ⟨name, defaultValue, comment⟩, defaultValue)
      else (cases, value)
  | .parametricValue _ _ => (cases, value)

  -- Append a default case if the final case is not a catch-all.
  let names := cases.map (·.name.getId.toString)
  let addDefaultCase (n : Ident) (cases : Array EnumCaseParsed) : Array EnumCaseParsed :=
    let defaultName: Ident := mkIdentFrom n (getUniqueName "default" names.toList)
    cases.push ⟨defaultName, defaultValue, makeComment "default case"⟩
  let cases := match lastValue with
  | .literalValue _      => addDefaultCase n cases
  | .parametricValue _ h => if h == trueValue then cases else addDefaultCase n cases

  pure cases

private def validateCases (n: Ident) (cases : Array EnumCaseParsed) : MacroM Unit :=
  -- validate that parametric values use the same name as the enum value
  for case in cases do
    match case.value with
    | .literalValue _      => pure ()
    | .parametricValue v _ => if v != n then
        Macro.throwErrorAt v s!"parametric value {v.getId.toString} must match the enum parameter {n.getId.toString}"

/-
Make the constructor types for the inductive type that an enum desugars to.
Constructors for non-literal cases bind to a value and a proof that the value is
in the case's range. A case's range is limited by both its local condition and
the conditions of all previous cases (since cases are matched greedily). The net
restriction on a case is the conjunction of its local restriction and the
negations of all prior restrictions. A literal constructor's implied restriction
is that of equality with its literal value.

To make these constructor types, we fold over the cases, building the
constructor type for each case and the net restriction after that case.
-/
private def mkCtorTypes (e n : Ident) (ty : Term) (parsedCases : Array EnumCaseParsed) : MacroM (Array Term) := do
  let mkCtorTypeAndCarriedRestrictions (value : EnumCaseValue) (priorRestrictions : Term) : MacroM (Term × Term) := do
    let thisType ← match value with
      | .literalValue _      => `($e)
      | .parametricValue _ h => `(($n:ident: $ty) → (h: $h ∧ $priorRestrictions) → $e)
    let netRestrictions ← match value with
      | .literalValue v      => `(¬($n:ident = $v) ∧ $priorRestrictions)
      | .parametricValue _ h => `(¬($h) ∧ $priorRestrictions)
    pure ⟨thisType, netRestrictions⟩

  let ⟨ctorTypes, _⟩ ← parsedCases.foldlM (init := (#[], ←`(true))) fun (valuesAcc, restrictions) (case) => do
    let (thisType, netRestrictions) ← mkCtorTypeAndCarriedRestrictions case.value restrictions
    return (valuesAcc.push thisType, netRestrictions)

  pure ctorTypes

/--
The `enum` macro defines an enumeration type over a base type. The enumeration
type defines cases that partition the base type. Each case is associated with a
literal value or a guard condition on values. Cases are matched greedily.

An enum type defines constructors for each of its cases. Constructors for
guarded types take a value and a proof that the value is in the case's range. An
enum type also defines functions to convert between the enum type and values of
the base type, and defines proofs that a round-trip in either direction between
a value of the base type and its corresponding enum value is the identity.
-/
macro "enum" e:ident "(" n:ident " : " ty:term ")" (" where")? cases:enum_case* : command => do
  -- Must have at least one case. Don't enforce this in the syntax parser since
  -- it's easier to give a good error message here.
  if cases.size == 0 then Macro.throwErrorAt e "enum must have at least one case"

  let eIdent (suffix : Name) := mkIdentFrom e (e.getId ++ suffix)
  let toStrLit (n : Name) := Lean.Syntax.mkStrLit n.toString

  let rawParsedCases := parseCases cases
  let parsedCases ← addCaseDefaults n rawParsedCases
  let _ ← validateCases n parsedCases

  let comments := parsedCases.map (·.comment)
  let names := parsedCases.map (·.name)
  let ctorTypes ← mkCtorTypes e n ty parsedCases

  let reprCases ← parsedCases.mapM fun ⟨name, value, _⟩ => do match value with
    | .literalValue _      => `(Term.matchAltExpr| | .$name:ident => $(toStrLit name.getId))
    | .parametricValue v _ => `(Term.matchAltExpr| | .$name:ident $v _ => s!"{$(toStrLit name.getId)} {$v}")

  let valCases ← parsedCases.mapM fun ⟨name, value, _⟩ => do match value with
    | .literalValue v      => `(Term.matchAltExpr| | .$name:ident => $v)
    | .parametricValue v _ => `(Term.matchAltExpr| | .$name:ident $v _ => $v)

  let ofValCases: Term ← parsedCases.reverse.foldlM (init := ←`(unreachable!)) fun res case => do
    let ⟨name, value, _⟩ := case
    match value with
    | .literalValue v      => `(if _ : $n = $v then .$name:ident else $res)
    | .parametricValue _ h => `(if _ : $h then .$name:ident $n (by simp; omega) else $res)

  `(
    inductive $e:ident
      $[$comments:docComment | $names:ident : $ctorTypes]*
      deriving Inhabited, BEq
    instance : Repr $e where reprPrec := fun e _ => match e with $reprCases:matchAlt*

    def $(eIdent `val) : $e → $ty $valCases:matchAlt*

    def $(eIdent `ofVal) : $ty → $e := fun $n => $ofValCases

    theorem $(eIdent `ofVal_val) (e : $e) : $(eIdent `ofVal) ($(eIdent `val) e) = e := by
      cases e <;> try rfl
      all_goals rename _ => h; simp [$(eIdent `val): ident, $(eIdent `ofVal): ident, h]

    theorem $(eIdent `val_ofVal) (n : $ty) : $(eIdent `val) ($(eIdent `ofVal) n) = n := by
      unfold $(eIdent `ofVal)
      repeat split; simp only [*, $(eIdent `val): ident]
      simp only [*, $(eIdent `val): ident]
      contradiction
  )