From 5825eb394f1cc52feb677e577e70ed1602c1d5e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Mar 2022 06:25:57 -0800 Subject: [PATCH] refactor: move `isOutParam` to `Expr.lean`, rename `consumeAutoOptParam` => `consumeTypeAnnotations` --- src/Lean/Class.lean | 6 +----- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/MutualDef.lean | 2 +- src/Lean/Expr.lean | 10 ++++++++-- src/Lean/Meta/CongrTheorems.lean | 8 ++++---- src/Lean/Meta/SynthInstance.lean | 2 +- src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +- 7 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index d860361909..cac9818e80 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -50,10 +50,6 @@ def hasOutParams (env : Environment) (n : Name) : Bool := | some b => b | none => false -@[export lean_is_out_param] -def isOutParam (e : Expr) : Bool := - e.isAppOfArity `outParam 1 - /-- Auxiliary function for checking whether a class has `outParam`, and whether they are being correctly used. @@ -68,7 +64,7 @@ def isOutParam (e : Expr) : Bool := -/ private partial def checkOutParam : Nat → Array FVarId → Expr → Except String Bool | i, outParams, Expr.forallE _ d b _ => - if isOutParam d then + if d.isOutParam then let fvarId := { name := Name.mkNum `_fvar outParams.size } let outParams := outParams.push fvarId let fvar := mkFVar fvarId diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 9a127e4a51..d25823d627 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -163,7 +163,7 @@ private def addNewArg (argName : Name) (arg : Expr) : M Unit := do Recall that, `Arg` may be wrapping an already elaborated `Expr`. -/ private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do let s ← get - let expectedType := (← getArgExpectedType).consumeAutoOptParam + let expectedType := (← getArgExpectedType).consumeTypeAnnotations match arg with | Arg.expr val => let arg ← ensureArgType s.f val expectedType diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index dcae63332b..7449ac572b 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -675,7 +675,7 @@ private partial def mkInst? (className : Name) (type : Expr) : MetaM (Option MkI unless instTypeType.isForall do return none let d := instTypeType.bindingDomain! - if isOutParam d then + if d.isOutParam then let mvar ← mkFreshExprMVar d go? (mkApp instType mvar) (instTypeType.bindingBody!.instantiate1 mvar) (outParams.push mvar) else diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 6ccfeaab38..eefc08193a 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -931,15 +931,21 @@ def getAutoParamTactic? (e : Expr) : Option Expr := else none +@[export lean_is_out_param] +def isOutParam (e : Expr) : Bool := + e.isAppOfArity `outParam 1 + def isOptParam (e : Expr) : Bool := e.isAppOfArity `optParam 2 def isAutoParam (e : Expr) : Bool := e.isAppOfArity `autoParam 2 -partial def consumeAutoOptParam (e : Expr) : Expr := +partial def consumeTypeAnnotations (e : Expr) : Expr := if e.isOptParam || e.isAutoParam then - consumeAutoOptParam e.appFn!.appArg! + consumeTypeAnnotations e.appFn!.appArg! + else if e.isOutParam then + consumeTypeAnnotations e.appArg! else e diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 9bf1cb671b..6c5d55001e 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -64,8 +64,8 @@ partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := let mut hs := #[] for x in xs, y in ys, eq in eqs do hs := hs.push x |>.push y |>.push eq - let xType := xType.consumeAutoOptParam - let yType := yType.consumeAutoOptParam + let xType := xType.consumeTypeAnnotations + let yType := yType.consumeTypeAnnotations let resultType ← if xType == yType then mkEq xType yType else mkHEq xType yType let congrType ← mkForallFVars hs resultType return { @@ -79,8 +79,8 @@ where if i < xs.size then let x := xs[i] let y := ys[i] - let xType := (← inferType x).consumeAutoOptParam - let yType := (← inferType y).consumeAutoOptParam + let xType := (← inferType x).consumeTypeAnnotations + let yType := (← inferType y).consumeTypeAnnotations if xType == yType then withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h => loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq) diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 6181ea1a1b..3851ea9e45 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -633,7 +633,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) : match type with | Expr.forallE _ d b _ => do let arg := args.get ⟨i, h⟩ - let arg ← if isOutParam d then mkFreshExprMVar d else pure arg + let arg ← if d.isOutParam then mkFreshExprMVar d else pure arg let args := args.set ⟨i, h⟩ arg preprocessArgs (b.instantiate1 arg) (i+1) args | _ => diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 808638c6e3..936dcd5ef8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -295,7 +295,7 @@ where | Expr.forallE _ fd fb _, Expr.forallE _ md mb _ => do -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here? -- if so, I'll need to take a callback - if isOutParam fd then + if fd.isOutParam then tryUnify (args[i]) (mvars[i]) inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars | _, _ => return ()