chore: rename LitValue.natVal/strVal to .nat/str (#8394)

Author: zwarich

src/Lean/Compiler/IR/ToIR.lean

@@ -65,8 +65,8 @@ def addDecl (d : Decl) : M Unit :=
 
 def lowerLitValue (v : LCNF.LitValue) : LitVal :=
   match v with
-  | .natVal n => .num n
-  | .strVal s => .str s
+  | .nat n => .num n
+  | .str s => .str s
 
 -- TODO: This should be cached.
 def lowerEnumToScalarType (name : Name) : M (Option IRType) := do

src/Lean/Compiler/LCNF/Basic.lean

@@ -34,14 +34,14 @@ def Param.toExpr (p : Param) : Expr :=
   .fvar p.fvarId
 
 inductive LitValue where
-  | natVal (val : Nat)
-  | strVal (val : String)
+  | nat (val : Nat)
+  | str (val : String)
   -- TODO: add constructors for `Int`, `Float`, `UInt` ...
   deriving Inhabited, BEq, Hashable
 
 def LitValue.toExpr : LitValue → Expr
-  | .natVal v => .lit (.natVal v)
-  | .strVal v => .lit (.strVal v)
+  | .nat v => .lit (.natVal v)
+  | .str v => .lit (.strVal v)
 
 inductive Arg where
   | erased
@@ -117,8 +117,8 @@ private unsafe def LetValue.updateArgsImp (e : LetValue) (args' : Array Arg) : L
 
 def LetValue.toExpr (e : LetValue) : Expr :=
   match e with
-  | .lit (.natVal val) => .lit (.natVal val)
-  | .lit (.strVal val) => .lit (.strVal val)
+  | .lit (.nat val) => .lit (.natVal val)
+  | .lit (.str val) => .lit (.strVal val)
   | .erased => erasedExpr
   | .proj n i s => .proj n i (.fvar s)
   | .const n us as => mkAppN (.const n us) (as.map Arg.toExpr)

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -171,9 +171,9 @@ where
   | n + 1 => .ctor ``Nat.succ #[goSmall n]
 
 def ofLCNFLit : LCNF.LitValue → Value
-| .natVal n => ofNat n
+| .nat n => ofNat n
 -- TODO: We could make this much more precise but the payoff is questionable
-| .strVal .. => .top
+| .str .. => .top
 
 partial def proj : Value → Nat → Value
 | .ctor _ vs , i => vs.getD i bot
@@ -206,11 +206,11 @@ partial def getLiteral (v : Value) : CompilerM (Option ((Array CodeDecl) × FVar
 where
   go : Value → CompilerM ((Array CodeDecl) × FVarId)
   | .ctor `Nat.zero #[] .. => do
-    let decl ← mkAuxLetDecl <| .lit <| .natVal <| 0
+    let decl ← mkAuxLetDecl <| .lit <| .nat <| 0
     return (#[.let decl], decl.fvarId)
   | .ctor `Nat.succ #[val] .. => do
     let val := getNatConstant val + 1
-    let decl ← mkAuxLetDecl <| .lit <| .natVal <| val
+    let decl ← mkAuxLetDecl <| .lit <| .nat <| val
     return (#[.let decl], decl.fvarId)
   | .ctor i vs => do
     let args ← vs.mapM go

src/Lean/Compiler/LCNF/InferType.lean

@@ -103,8 +103,8 @@ def inferConstType (declName : Name) (us : List Level) : CompilerM Expr := do
 
 def inferLitValueType (value : LitValue) : Expr :=
   match value with
-  | .natVal .. => mkConst ``Nat
-  | .strVal .. => mkConst ``String
+  | .nat .. => mkConst ``Nat
+  | .str .. => mkConst ``String
 
 mutual
   partial def inferArgType (arg : Arg) : InferTypeM Expr :=

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -64,22 +64,22 @@ def mkAuxLit [Literal α] (x : α) (prefixName := `_x) : FolderM FVarId := do
   mkAuxLetDecl lit prefixName
 
 partial def getNatLit (fvarId : FVarId) : CompilerM (Option Nat) := do
-  let some (.lit (.natVal n)) ← findLetValue? fvarId | return none
+  let some (.lit (.nat n)) ← findLetValue? fvarId | return none
   return n
 
 def mkNatLit (n : Nat) : FolderM LetValue :=
-  return .lit (.natVal n)
+  return .lit (.nat n)
 
 instance : Literal Nat where
   getLit := getNatLit
   mkLit := mkNatLit
 
 def getStringLit (fvarId : FVarId) : CompilerM (Option String) := do
-  let some (.lit (.strVal s)) ← findLetValue? fvarId | return none
+  let some (.lit (.str s)) ← findLetValue? fvarId | return none
   return s
 
 def mkStringLit (n : String) : FolderM LetValue :=
-  return .lit (.strVal n)
+  return .lit (.str n)
 
 instance : Literal String where
   getLit := getStringLit

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -54,7 +54,7 @@ Remark: We use this method when simplifying projections and cases-constructor.
 -/
 def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
   match (← findLetDecl? fvarId) with
-  | some { value := .lit (.natVal n), .. } =>
+  | some { value := .lit (.nat n), .. } =>
     return some <| .natVal n
   | some { value := .const declName _ args, .. } =>
     let some (.ctorInfo val) := (← getEnv).find? declName | return none

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -290,7 +290,7 @@ where
         let argsNew := mkJmpNewArgs args info.paramIdx #[] jpAlt.dependsOnDiscr
         return some <| .jmp jpAlt.decl.fvarId argsNew
       | .natVal (n+1) =>
-        let auxDecl ← mkAuxLetDecl (.lit (.natVal n))
+        let auxDecl ← mkAuxLetDecl (.lit (.nat n))
         let argsNew := mkJmpNewArgs args info.paramIdx #[.fvar auxDecl.fvarId] jpAlt.dependsOnDiscr
         return some <| .let auxDecl (.jmp jpAlt.decl.fvarId argsNew)
 

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -207,7 +207,7 @@ partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
         return k
       | .natVal 0 => simp k
       | .natVal (n+1) =>
-        let auxDecl ← mkAuxLetDecl (.lit (.natVal n))
+        let auxDecl ← mkAuxLetDecl (.lit (.nat n))
         addFVarSubst params[0]!.fvarId auxDecl.fvarId
         let k ← simp k
         eraseParams params

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -407,8 +407,8 @@ partial def etaReduceImplicit (e : Expr) : Expr :=
 
 def litToValue (lit : Literal) : LitValue :=
   match lit with
-  | .natVal val => .natVal val
-  | .strVal val => .strVal val
+  | .natVal val => .nat val
+  | .strVal val => .str val
 
 /--
 Put the given expression in `LCNF`.

src/Lean/Compiler/LCNF/ToMono.lean

@@ -105,7 +105,7 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
 partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
   let resultType ← toMonoType c.resultType
   let natType := mkConst ``Nat
-  let zeroDecl ← mkLetDecl `zero natType (.lit (.natVal 0))
+  let zeroDecl ← mkLetDecl `zero natType (.lit (.nat 0))
   let isZeroDecl ← mkLetDecl `isZero (mkConst ``Bool) (.const ``Nat.decEq [] #[.fvar c.discr, .fvar zeroDecl.fvarId])
   let alts ← c.alts.mapM fun alt => do
     match alt with
@@ -114,7 +114,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
       eraseParams ps
       if ctorName == ``Nat.succ then
         let p := ps[0]!
-        let oneDecl ← mkLetDecl `one natType (.lit (.natVal 1))
+        let oneDecl ← mkLetDecl `one natType (.lit (.nat 1))
         let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar c.discr, .fvar oneDecl.fvarId] }
         modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
         return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl (← k.toMono)))
@@ -126,7 +126,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
 partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
   let resultType ← toMonoType c.resultType
   let natType := mkConst ``Nat
-  let zeroNatDecl ← mkLetDecl `natZero natType (.lit (.natVal 0))
+  let zeroNatDecl ← mkLetDecl `natZero natType (.lit (.nat 0))
   let zeroIntDecl ← mkLetDecl `intZero (mkConst ``Int) (.const ``Int.ofNat [] #[.fvar zeroNatDecl.fvarId])
   let isNegDecl ← mkLetDecl `isNeg (mkConst ``Bool) (.const ``Int.decLt [] #[.fvar c.discr, .fvar zeroIntDecl.fvarId])
   let alts ← c.alts.mapM fun alt => do
@@ -137,7 +137,7 @@ partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code :
       let p := ps[0]!
       if ctorName == ``Int.negSucc then
         let absDecl ← mkLetDecl `abs natType (.const ``Int.natAbs [] #[.fvar c.discr])
-        let oneDecl ← mkLetDecl `one natType (.lit (.natVal 1))
+        let oneDecl ← mkLetDecl `one natType (.lit (.nat 1))
         let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar absDecl.fvarId, .fvar oneDecl.fvarId] }
         modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
         return .alt ``Bool.true #[] (.let absDecl (.let oneDecl (.let subOneDecl (← k.toMono))))