refactor: rename NestedOccurence to IndTypeFormer

leanprover · Sep 13, 2024 · 29d2785 · 29d2785
1 parent b9b0f5c
commit 29d2785
Show file tree

Hide file tree

Showing 7 changed files with 141 additions and 141 deletions.
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
@@ -12,8 +12,8 @@ namespace Lean.Elab.Deriving.BEq
 open Lean.Parser.Term
 open Meta
 
-def mkBEqHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  mkHeader `BEq 2 argNames nestedOcc
+def mkBEqHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  mkHeader `BEq 2 argNames indTypeFormer
 
 def mkMatch (ctx : Context) (header : Header) (e : Expr) (fvars : Array Expr) : TermElabM Term := do
   let f := e.getAppFn
@@ -100,11 +100,11 @@ where
     return alts
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ←  mkBEqHeader argNames nestedOcc
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ←  mkBEqHeader argNames indTypeFormer
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
   let type ← Term.elabTerm header.targetType none
   let mut body ← mkMatch ctx header type xs

diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
@@ -15,8 +15,8 @@ namespace Lean.Elab.Deriving.DecEq
 open Lean.Parser.Term
 open Meta
 
-def mkDecEqHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  mkHeader `DecidableEq 2 argNames nestedOcc
+def mkDecEqHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  mkHeader `DecidableEq 2 argNames indTypeFormer
 
 def mkMatch (ctx : Context) (header : Header) (e : Expr) (fvars : Array Expr) : TermElabM Term := do
   let f := e.getAppFn
@@ -93,12 +93,12 @@ where
           alts := alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
     return alts
 
-def mkAuxFunction (ctx : Context) (auxFunName : Name) (argNames : Array Name) (nestedOcc : NestedOccurence): TermElabM (TSyntax `command) := do
-  let header  ← mkDecEqHeader argNames nestedOcc
+def mkAuxFunction (ctx : Context) (auxFunName : Name) (argNames : Array Name) (indTypeFormer : IndTypeFormer): TermElabM (TSyntax `command) := do
+  let header  ← mkDecEqHeader argNames indTypeFormer
   let binders := header.binders
   let target₁ := mkIdent header.targetNames[0]!
   let target₂ := mkIdent header.targetNames[1]!
-  let termSuffix ← if ctx.auxFunNames.size > 1 || nestedOcc.getIndVal.isRec
+  let termSuffix ← if ctx.auxFunNames.size > 1 || indTypeFormer.getIndVal.isRec
     then `(Parser.Termination.suffix|termination_by structural $target₁)
     else `(Parser.Termination.suffix|)
   Term.elabBinders binders fun xs => do
@@ -112,9 +112,9 @@ def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do
   let mut res : Array (TSyntax `command) := #[]
   for i in [:ctx.auxFunNames.size] do
     let auxFunName    := ctx.auxFunNames[i]!
-    let nestedOcc     := ctx.typeInfos[i]!
+    let indTypeFormer := ctx.typeInfos[i]!
     let argNames      := ctx.typeArgNames[i]!
-    res := res.push (← mkAuxFunction ctx auxFunName argNames nestedOcc)
+    res := res.push (← mkAuxFunction ctx auxFunName argNames indTypeFormer)
   `(command| mutual $[$res:command]* end)
 
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do

diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -15,11 +15,11 @@ open Lean.Json
 open Lean.Parser.Term
 open Lean.Meta
 
-def mkToJsonHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  mkHeader ``ToJson 1 argNames nestedOcc
+def mkToJsonHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  mkHeader ``ToJson 1 argNames indTypeFormer
 
-def mkFromJsonHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  let header ← mkHeader ``FromJson 0 argNames nestedOcc
+def mkFromJsonHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  let header ← mkHeader ``FromJson 0 argNames indTypeFormer
   let jsonArg ← `(bracketedBinderF|(json : Json))
   return {header with
     binders := header.binders.push jsonArg}
@@ -175,11 +175,11 @@ def mkToJsonBody (ctx : Context) (header : Header) (e : Expr) (fvars : Array Exp
     mkToJsonBodyForInduct ctx header e fvars
 
 def mkToJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ←  mkToJsonHeader argNames nestedOcc
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ←  mkToJsonHeader argNames indTypeFormer
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
     let type       ← Term.elabTerm header.targetType none
     let mut body   ←  mkToJsonBody ctx header type xs
@@ -197,15 +197,15 @@ def mkFromJsonBody (ctx : Context) (header : Header) (e : Expr) (fvars : Array E
     mkFromJsonBodyForInduct ctx header e fvars
 
 def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ←  mkFromJsonHeader argNames nestedOcc --TODO fix header info
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ←  mkFromJsonHeader argNames indTypeFormer --TODO fix header info
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
     let type ← Term.elabTerm header.targetType none
     let mut body ← mkFromJsonBody ctx header type xs
-    if ctx.usePartial || nestedOcc.getIndVal.isRec then
+    if ctx.usePartial || indTypeFormer.getIndVal.isRec then
       let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
       body ← mkLet letDecls body
       `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← ctx.typeInfos[i]!.mkAppTerm header.argNames) := $body:term)

diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
@@ -13,8 +13,8 @@ open Command
 open Lean.Parser.Term
 open Meta
 
-def mkHashableHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  mkHeader `Hashable 1 argNames nestedOcc
+def mkHashableHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  mkHeader `Hashable 1 argNames indTypeFormer
 
 def mkMatch (ctx : Context) (header : Header) (e : Expr) (fvars : Array Expr) : TermElabM Term := do
   let f := e.getAppFn
@@ -60,11 +60,11 @@ where
     return alts
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ←  mkHashableHeader argNames nestedOcc
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ←  mkHashableHeader argNames indTypeFormer
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
   let type ← Term.elabTerm header.targetType none
   let mut body       ←  mkMatch ctx header type xs

diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
@@ -12,8 +12,8 @@ namespace Lean.Elab.Deriving.Ord
 open Lean.Parser.Term
 open Meta
 
-def mkOrdHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  mkHeader `Ord 2 argNames nestedOcc
+def mkOrdHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  mkHeader `Ord 2 argNames indTypeFormer
 
 def mkMatch (ctx : Context) (header : Header) (e : Expr) (fvars : Array Expr) : TermElabM Term := do
   let f := e.getAppFn
@@ -76,11 +76,11 @@ where
     return alts.pop.pop
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ← mkOrdHeader argNames nestedOcc
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ← mkOrdHeader argNames indTypeFormer
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
   let type ← Term.elabTerm header.targetType none
   let body ←  mkMatch ctx header type xs

diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
@@ -14,8 +14,8 @@ open Lean.Parser.Term
 open Meta
 open Std
 
-def mkReprHeader (argNames : Array Name) (nestedOcc : NestedOccurence) : TermElabM Header := do
-  let header ← mkHeader `Repr 1 argNames nestedOcc
+def mkReprHeader (argNames : Array Name) (indTypeFormer : IndTypeFormer) : TermElabM Header := do
+  let header ← mkHeader `Repr 1 argNames indTypeFormer
   return { header with
     binders := header.binders.push (← `(bracketedBinderF| (prec : Nat)))
   }
@@ -100,11 +100,11 @@ def mkBody (ctx : Context) (header : Header) (e : Expr) (fvars : Array Expr): Te
     mkBodyForInduct ctx header e fvars
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
-  let auxFunName := ctx.auxFunNames[i]!
-  let nestedOcc  := ctx.typeInfos[i]!
-  let argNames   := ctx.typeArgNames[i]!
-  let header     ←  mkReprHeader argNames nestedOcc
-  let binders    := header.binders
+  let auxFunName    := ctx.auxFunNames[i]!
+  let indTypeFormer := ctx.typeInfos[i]!
+  let argNames      := ctx.typeArgNames[i]!
+  let header        ←  mkReprHeader argNames indTypeFormer
+  let binders       := header.binders
   Term.elabBinders binders fun xs => do
   let type ← Term.elabTerm header.targetType none
   let mut body   ←  mkBody ctx header type xs