From 52aef7611a7d914f953072e1cf137200c3580685 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Sep 2020 08:38:37 -0700 Subject: [PATCH] chore: fix `val` vs `value` naming convention --- src/Lean/Elab/Definition.lean | 20 +++++++-------- src/Lean/Elab/MutualDef.lean | 46 +++++++++++++++++------------------ 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean index 1682f975a5..d4db073b9f 100644 --- a/src/Lean/Elab/Definition.lean +++ b/src/Lean/Elab/Definition.lean @@ -39,7 +39,7 @@ structure DefView := (declId : Syntax) (binders : Syntax) (type? : Option Syntax) -(val : Syntax) +(value : Syntax) namespace Command @@ -51,19 +51,19 @@ let (binders, type) := expandOptDeclSig (stx.getArg 2); let modifiers := modifiers.addAttribute { name := `inline }; let modifiers := modifiers.addAttribute { name := `reducible }; { ref := stx, kind := DefKind.abbrev, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := type, val := stx.getArg 3 } + declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView := -- parser! "def " >> declId >> optDeclSig >> declVal let (binders, type) := expandOptDeclSig (stx.getArg 2); { ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := type, val := stx.getArg 3 } + declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView := -- parser! "theorem " >> declId >> declSig >> declVal let (binders, type) := expandDeclSig (stx.getArg 2); { ref := stx, kind := DefKind.theorem, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := some type, val := stx.getArg 3 } + declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 } def mkFreshInstanceName : CommandElabM Name := do s ← get; @@ -82,7 +82,7 @@ val ← match (stx.getArg 3).getOptional? with }; pure { ref := stx, kind := DefKind.opaque, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := some type, val := val + declId := stx.getArg 1, binders := binders, type? := some type, value := val } def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do @@ -97,7 +97,7 @@ declId ← match (stx.getArg 1).getOptional? with }; pure { ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := declId, binders := binders, type? := type, val := stx.getArg 3 + declId := declId, binders := binders, type? := type, value := stx.getArg 3 } def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := @@ -106,7 +106,7 @@ let (binders, type) := expandDeclSig (stx.getArg 1); let id := mkIdentFrom stx `_example; let declId := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode]; { ref := stx, kind := DefKind.example, modifiers := modifiers, - declId := declId, binders := binders, type? := some type, val := stx.getArg 2 } + declId := declId, binders := binders, type? := some type, value := stx.getArg 2 } def isDefLike (stx : Syntax) : Bool := let declKind := stx.getKind; @@ -159,7 +159,7 @@ def mkDef? (view : DefView) (declName : Name) (scopeLevelNames allUserLevelNames : TermElabM (Option Declaration) := do withRef view.ref do Term.synthesizeSyntheticMVars; -val ← withRef view.val $ Term.ensureHasType type val; +val ← withRef view.value $ Term.ensureHasType type val; Term.synthesizeSyntheticMVarsNoPostponing; type ← instantiateMVars type; val ← instantiateMVars val; @@ -226,11 +226,11 @@ runTermElabM declName $ fun vars => Term.withLevelNames allUserLevelNames $ Term Term.synthesizeSyntheticMVarsNoPostponing; type ← instantiateMVars type; withUsedWhen' vars xs type view.kind.isTheorem $ fun vars => do - val ← elabDefVal view.val type; + val ← elabDefVal view.value type; mkDef? view declName scopeLevelNames allUserLevelNames vars xs type val | none => do { type ← withRef view.binders $ mkFreshTypeMVar; - val ← elabDefVal view.val type; + val ← elabDefVal view.value type; mkDef? view declName scopeLevelNames allUserLevelNames vars xs type val }; match decl? with diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 066dcd79c8..4df189521d 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -21,7 +21,7 @@ structure DefViewElabHeader := (levelNames : List Name) (numParams : Nat) (type : Expr) -- including the parameters -(declVal : Syntax) +(valueStx : Syntax) instance DefViewElabHeader.inhabited : Inhabited DefViewElabHeader := ⟨⟨arbitrary _, {}, DefKind.«def», arbitrary _, arbitrary _, [], 0, arbitrary _, arbitrary _⟩⟩ @@ -92,7 +92,7 @@ views.foldlM levelNames := levelNames, numParams := xs.size, type := type, - declVal := view.val + valueStx := view.value }; check headers newHeader; pure $ headers.push newHeader) @@ -131,7 +131,7 @@ else private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) := headers.mapM fun header => withDeclName header.declName $ withLevelNames header.levelNames do - valStx ← liftMacroM $ declValToTerm header.declVal; + valStx ← liftMacroM $ declValToTerm header.valueStx; forallBoundedTelescope header.type header.numParams fun xs type => do val ← elabTermEnsuringType valStx type; mkLambdaFVars xs val @@ -210,7 +210,7 @@ structure PreDeclaration := (modifiers : Modifiers) (declName : Name) (type : Expr) -(val : Expr) +(value : Expr) namespace MutualClosure @@ -498,7 +498,7 @@ mainHeaders.size.foldM lparams := [], -- we set it later modifiers := header.modifiers, type := type, - val := val + value := val }) preDecls @@ -513,7 +513,7 @@ letRecClosures.foldl lparams := [], -- we set it later modifiers := { modifiers with attrs := c.toLift.attrs }, type := type, - val := val + value := val }) preDecls @@ -571,9 +571,9 @@ else private def instantiateMVarsAtPreDecls (preDecls : Array PreDeclaration) : TermElabM (Array PreDeclaration) := preDecls.mapM fun preDecl => do - type ← instantiateMVars preDecl.type; - val ← instantiateMVars preDecl.val; - pure { preDecl with type := type, val := val } + type ← instantiateMVars preDecl.type; + value ← instantiateMVars preDecl.value; + pure { preDecl with type := type, value := value } private def levelMVarToParamExpr (e : Expr) : StateRefT Nat TermElabM Expr := do nextIdx ← get; @@ -583,9 +583,9 @@ pure e private def levelMVarToParamPreDeclsAux (preDecls : Array PreDeclaration) : StateRefT Nat TermElabM (Array PreDeclaration) := preDecls.mapM fun preDecl => do - type ← levelMVarToParamExpr preDecl.type; - val ← levelMVarToParamExpr preDecl.val; - pure { preDecl with type := type, val := val } + type ← levelMVarToParamExpr preDecl.type; + value ← levelMVarToParamExpr preDecl.value; + pure { preDecl with type := type, value := value } private def levelMVarToParamPreDecls (preDecls : Array PreDeclaration) : TermElabM (Array PreDeclaration) := (levelMVarToParamPreDeclsAux preDecls).run' 1 @@ -597,7 +597,7 @@ private def getLevelParamsPreDecls (preDecls : Array PreDeclaration) (scopeLevel let (_, s) := StateT.run (preDecls.forM fun preDecl => do { collectLevelParamsExpr preDecl.type; - collectLevelParamsExpr preDecl.val }) + collectLevelParamsExpr preDecl.value }) {}; match sortDeclLevelParams scopeLevelNames allUserLevelNames s.params with | Except.error msg => throwError msg @@ -606,9 +606,9 @@ match sortDeclLevelParams scopeLevelNames allUserLevelNames s.params with private def shareCommon (preDecls : Array PreDeclaration) : Array PreDeclaration := let result : Std.ShareCommonM (Array PreDeclaration) := preDecls.mapM fun preDecl => do { - type ← Std.withShareCommon preDecl.type; - val ← Std.withShareCommon preDecl.val; - pure { preDecl with type := type, val := val } + type ← Std.withShareCommon preDecl.type; + value ← Std.withShareCommon preDecl.value; + pure { preDecl with type := type, value := value } }; result.run @@ -623,7 +623,7 @@ let fixExpr (e : Expr) : Expr := pure $ preDecls.map fun preDecl => { preDecl with type := fixExpr preDecl.type, - val := fixExpr preDecl.val, + value := fixExpr preDecl.value, lparams := lparams } private def applyAttributesOf (preDecls : Array PreDeclaration) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do @@ -635,16 +635,16 @@ let decl := match preDecl.kind with | DefKind.«example» => unreachable! | DefKind.«theorem» => - Declaration.thmDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.val } + Declaration.thmDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.value } | DefKind.«opaque» => - Declaration.opaqueDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.val, + Declaration.opaqueDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.value, isUnsafe := preDecl.modifiers.isUnsafe } | DefKind.«abbrev» => - Declaration.defnDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.val, + Declaration.defnDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.value, hints := ReducibilityHints.«abbrev», isUnsafe := preDecl.modifiers.isUnsafe } | DefKind.«def» => - Declaration.defnDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.val, - hints := ReducibilityHints.regular (getMaxHeight env preDecl.val + 1), + Declaration.defnDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.value, + hints := ReducibilityHints.regular (getMaxHeight env preDecl.value + 1), isUnsafe := preDecl.modifiers.isUnsafe }; addDecl decl; applyAttributesOf #[preDecl] AttributeApplicationTime.afterTypeChecking; @@ -657,7 +657,7 @@ let decl := Declaration.mutualDefnDecl $ preDecls.toList.map fun preDecl => { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, - value := preDecl.val, + value := preDecl.value, isUnsafe := true, hints := ReducibilityHints.opaque };