From 93d987461affc14412a0280277a37c201dc56718 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Dec 2019 19:17:45 -0800 Subject: [PATCH] chore: naming convention --- src/Init/Lean/Meta/Basic.lean | 12 +++++------- src/Init/Lean/Meta/Check.lean | 2 +- src/Init/Lean/Meta/DiscrTree.lean | 6 +++--- src/Init/Lean/Meta/ExprDefEq.lean | 8 ++++---- src/Init/Lean/Meta/FunInfo.lean | 2 +- src/Init/Lean/Meta/InferType.lean | 8 ++++---- src/Init/Lean/Meta/SynthInstance.lean | 2 +- 7 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean index c3e7b500ac..6b797f71f0 100644 --- a/src/Init/Lean/Meta/Basic.lean +++ b/src/Init/Lean/Meta/Basic.lean @@ -260,12 +260,12 @@ ctx ← read; pure ctx.config.opts env ← getEnv; pure $ isReducible env constName /-- While executing `x`, ensure the given transparency mode is used. -/ -@[inline] def usingTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α := +@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α := adaptReader (fun (ctx : Context) => { config := { transparency := mode, .. ctx.config }, .. ctx }) x -@[inline] def usingAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α := +@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α := adaptReader (fun (ctx : Context) => let oldMode := ctx.config.transparency; @@ -557,7 +557,7 @@ else k #[] type partial def isClassExpensive : Expr → MetaM (Option Name) -| type => usingTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants. +| type => withTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants. forallTelescopeReducingAux isClassExpensive type none $ fun xs type => do match type.getAppFn with | Expr.const c _ _ => do @@ -704,10 +704,8 @@ mvarId ← mkFreshId; modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s }; pure mvarId -def whnfUsingDefault : Expr → MetaM Expr := -fun e => usingTransparency TransparencyMode.default $ whnf e - -abbrev whnfD := whnfUsingDefault +def whnfD : Expr → MetaM Expr := +fun e => withTransparency TransparencyMode.default $ whnf e /-- Execute `x` using approximate unification. -/ @[inline] def approxDefEq {α} (x : MetaM α) : MetaM α := diff --git a/src/Init/Lean/Meta/Check.lean b/src/Init/Lean/Meta/Check.lean index 2e105a39e9..041a9d670c 100644 --- a/src/Init/Lean/Meta/Check.lean +++ b/src/Init/Lean/Meta/Check.lean @@ -79,7 +79,7 @@ private partial def checkAux : Expr → MetaM Unit def check (e : Expr) : MetaM Unit := traceCtx `Meta.check $ - usingTransparency TransparencyMode.all $ checkAux e + withTransparency TransparencyMode.all $ checkAux e def isTypeCorrect (e : Expr) : MetaM Bool := catch diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean index b7a30df40c..54d82ca987 100644 --- a/src/Init/Lean/Meta/DiscrTree.lean +++ b/src/Init/Lean/Meta/DiscrTree.lean @@ -182,7 +182,7 @@ partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key) private def initCapacity := 8 def mkPath (e : Expr) : MetaM (Array Key) := -usingTransparency TransparencyMode.reducible $ do +withTransparency TransparencyMode.reducible $ do let todo : Array Expr := Array.mkEmpty initCapacity; let keys : Array Key := Array.mkEmpty initCapacity; mkPathAux (todo.push e) keys @@ -309,7 +309,7 @@ match d.root.find Key.star with | some (Trie.node vs _) => result ++ vs def getMatch {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) := -usingTransparency TransparencyMode.reducible $ do +withTransparency TransparencyMode.reducible $ do let result := getStarResult d; (k, args) ← getMatchKeyArgs e; match k with @@ -341,7 +341,7 @@ private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array | some c => do result ← visitStarChild result; getUnifyAux 0 (todo ++ args) c.2 result def getUnify {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) := -usingTransparency TransparencyMode.reducible $ do +withTransparency TransparencyMode.reducible $ do (k, args) ← getUnifyKeyArgs e; match k with | Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[] diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index d3dd2956c0..00ddb6c718 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -27,7 +27,7 @@ namespace Meta private def isDefEqEta (a b : Expr) : MetaM Bool := if a.isLambda && !b.isLambda then do bType ← inferType b; - bType ← whnfUsingDefault bType; + bType ← whnfD bType; match bType with | Expr.forallE n d _ c => let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0)); @@ -128,7 +128,7 @@ if h : args₁.size = args₂.size then do synthPending a₂; pure () }; - usingAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂) + withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂) else pure false @@ -633,7 +633,7 @@ traceCtx `Meta.isDefEq.assign.checkTypes $ do -- must check whether types are definitionally equal or not, before assigning and returning true mvarType ← inferType mvar; vType ← inferType v; - condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType) + condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType) (do assignExprMVar mvar.mvarId! v; pure true) (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType; pure false) @@ -695,7 +695,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) -- must check whether types are definitionally equal or not, before assigning and returning true mvarType ← inferType mvar; vType ← inferType v; - condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType) + condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType) (do assignExprMVar mvarId v; pure true) (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType; pure false) diff --git a/src/Init/Lean/Meta/FunInfo.lean b/src/Init/Lean/Meta/FunInfo.lean index 4b6a9954f7..7dc1821fb7 100644 --- a/src/Init/Lean/Meta/FunInfo.lean +++ b/src/Init/Lean/Meta/FunInfo.lean @@ -56,7 +56,7 @@ else private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := checkFunInfoCache fn maxArgs? $ do fnType ← inferType fn; - usingTransparency TransparencyMode.default $ + withTransparency TransparencyMode.default $ forallBoundedTelescope fnType maxArgs? $ fun fvars type => do pinfo ← fvars.size.foldM (fun (i : Nat) (pinfo : Array ParamInfo) => do diff --git a/src/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean index 79ed3adc1d..6fe4692450 100644 --- a/src/Init/Lean/Meta/InferType.lean +++ b/src/Init/Lean/Meta/InferType.lean @@ -69,7 +69,7 @@ matchConst env structType.getAppFn failed $ fun structInfo structLvls => do def getLevel (type : Expr) : MetaM Level := do typeType ← inferType type; -typeType ← whnfUsingDefault typeType; +typeType ← whnfD typeType; match typeType with | Expr.sort lvl _ => pure lvl | Expr.mvar mvarId _ => @@ -141,7 +141,7 @@ private partial def inferTypeAux : Expr → MetaM Expr | Expr.localE _ _ _ _ => unreachable! def inferTypeImpl (e : Expr) : MetaM Expr := -usingTransparency TransparencyMode.default (inferTypeAux e) +withTransparency TransparencyMode.default (inferTypeAux e) @[init] def setInferTypeRef : IO Unit := inferTypeRef.set inferTypeImpl @@ -215,7 +215,7 @@ match r with | LBool.undef => do -- dbgTrace ("isPropQuick failed " ++ toString e); type ← inferType e; - type ← whnfUsingDefault type; + type ← whnfD type; match type with | Expr.sort u _ => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u | _ => pure false @@ -323,7 +323,7 @@ match r with | LBool.false => pure false | LBool.undef => do type ← inferType e; - type ← whnfUsingDefault type; + type ← whnfD type; match type with | Expr.sort _ _ => pure true | _ => pure false diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 56bb922923..98fbbe32e7 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -511,7 +511,7 @@ try $ r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e') def synthInstance? (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) := -usingTransparency TransparencyMode.reducible $ do +withTransparency TransparencyMode.reducible $ do type ← instantiateMVars type; type ← preprocess type; s ← get;