178 lines
7.5 KiB
Text
178 lines
7.5 KiB
Text
/-
|
||
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Lean.Elab.App
|
||
|
||
public section
|
||
|
||
namespace Lean.Elab.Term
|
||
open Meta
|
||
|
||
/--
|
||
Decompose `e` into `(r, a, b)`.
|
||
|
||
Remark: it assumes the last two arguments are explicit.
|
||
-/
|
||
def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
|
||
if e.getAppNumArgs < 2 then
|
||
return none
|
||
else
|
||
return some (e.appFn!.appFn!, e.appFn!.appArg!, e.appArg!)
|
||
|
||
private def getRelUniv (r : Expr) : MetaM Level := do
|
||
let rType ← inferType r
|
||
forallTelescopeReducing rType fun _ sort => do
|
||
let .sort u ← whnf sort | throwError "unexpected relation type{indentExpr rType}"
|
||
return u
|
||
|
||
def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr) := do
|
||
let some (r, a, b) ← getCalcRelation? resultType | unreachable!
|
||
let some (s, _, c) ← getCalcRelation? (← instantiateMVars stepType) | unreachable!
|
||
let u ← getRelUniv r
|
||
let v ← getRelUniv s
|
||
let (α, β, γ) := (← inferType a, ← inferType b, ← inferType c)
|
||
let (u_1, u_2, u_3) := (← getLevel α, ← getLevel β, ← getLevel γ)
|
||
let w ← mkFreshLevelMVar
|
||
let t ← mkFreshExprMVar (← mkArrow α (← mkArrow γ (mkSort w)))
|
||
let selfType := mkAppN (Lean.mkConst ``Trans [u, v, w, u_1, u_2, u_3]) #[α, β, γ, r, s, t]
|
||
match (← trySynthInstance selfType) with
|
||
| .some self =>
|
||
let result := mkAppN (Lean.mkConst ``Trans.trans [u, v, w, u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, step]
|
||
let resultType := (← instantiateMVars (← inferType result)).headBeta
|
||
unless (← getCalcRelation? resultType).isSome do
|
||
throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
|
||
return (result, resultType)
|
||
| _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
|
||
|
||
/--
|
||
Adds a type annotation to a hole that occurs immediately at the beginning of the term.
|
||
This is so that coercions can trigger when elaborating the term.
|
||
See https://github.com/leanprover/lean4/issues/2040 for further rationale.
|
||
|
||
- `_ < 3` is annotated
|
||
- `(_) < 3` is not, because it occurs after an atom
|
||
- in `_ < _` only the first one is annotated
|
||
- `_ + 2 < 3` is annotated (not the best heuristic, ideally we'd like to annotate `_ + 2`)
|
||
- `lt _ 3` is not, because it occurs after an identifier
|
||
-/
|
||
partial def annotateFirstHoleWithType (t : Term) (type : Expr) : TermElabM Term :=
|
||
-- The state is true if we should annotate the immediately next hole with the type.
|
||
return ⟨← StateT.run' (go t) true⟩
|
||
where
|
||
go (t : Syntax) := do
|
||
unless ← get do return t
|
||
match t with
|
||
| .node _ ``Lean.Parser.Term.hole _ =>
|
||
set false
|
||
`(($(⟨t⟩) : $(← exprToSyntax type)))
|
||
| .node i k as => return .node i k (← as.mapM go)
|
||
| _ => set false; return t
|
||
|
||
/-- View of a `calcStep`. -/
|
||
structure CalcStepView where
|
||
ref : Syntax
|
||
/-- A relation term like `a ≤ b` -/
|
||
term : Term
|
||
/-- A proof of `term` -/
|
||
proof : Term
|
||
deriving Inhabited
|
||
|
||
def mkCalcFirstStepView (step0 : TSyntax ``calcFirstStep) : TermElabM CalcStepView :=
|
||
withRef step0 do
|
||
match step0 with
|
||
| `(calcFirstStep| $term:term) => return { ref := step0, term := ← `($term = _), proof := ← ``(rfl)}
|
||
| `(calcFirstStep| $term := $proof) => return { ref := step0, term, proof}
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
def mkCalcStepViews (steps : TSyntax ``calcSteps) : TermElabM (Array CalcStepView) :=
|
||
match steps with
|
||
| `(calcSteps|
|
||
$step0:calcFirstStep
|
||
$rest*) => do
|
||
let mut steps := #[← mkCalcFirstStepView step0]
|
||
for step in rest do
|
||
let `(calcStep| $term := $proof) := step | throwUnsupportedSyntax
|
||
steps := steps.push { ref := step, term, proof }
|
||
return steps
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
def elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr) := do
|
||
let mut result? := none
|
||
let mut prevRhs? := none
|
||
for step in steps do
|
||
let type ← elabType <| ← do
|
||
if let some prevRhs := prevRhs? then
|
||
annotateFirstHoleWithType step.term (← inferType prevRhs)
|
||
else
|
||
pure step.term
|
||
let some (_, lhs, rhs) ← getCalcRelation? type |
|
||
throwErrorAt step.term "invalid 'calc' step, relation expected{indentExpr type}"
|
||
if let some prevRhs := prevRhs? then
|
||
unless (← isDefEqGuarded lhs prevRhs) do
|
||
throwErrorAt step.term "\
|
||
invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
|
||
but previous right-hand side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
|
||
let proof ← withFreshMacroScope do elabTermEnsuringType step.proof type
|
||
result? := some <| ← do
|
||
if let some (result, resultType) := result? then
|
||
synthesizeSyntheticMVarsUsingDefault
|
||
withRef step.term do mkCalcTrans result resultType proof type
|
||
else
|
||
pure (proof, type)
|
||
prevRhs? := rhs
|
||
synthesizeSyntheticMVarsUsingDefault
|
||
return result?.get!
|
||
|
||
def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) : MetaM α := do
|
||
let resultType := (← instantiateMVars (← inferType result)).headBeta
|
||
let some (r, lhs, rhs) ← getCalcRelation? resultType | unreachable!
|
||
if let some (er, elhs, erhs) ← getCalcRelation? expectedType then
|
||
if ← isDefEqGuarded r er then
|
||
let mut failed := false
|
||
unless ← isDefEqGuarded lhs elhs do
|
||
let (lhs, elhs) ← addPPExplicitToExposeDiff lhs elhs
|
||
let (lhsTy, elhsTy) ← addPPExplicitToExposeDiff (← inferType lhs) (← inferType elhs)
|
||
logErrorAt steps[0]!.term m!"\
|
||
invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
|
||
but is expected to be{indentD m!"{elhs} : {elhsTy}"}"
|
||
failed := true
|
||
unless ← isDefEqGuarded rhs erhs do
|
||
let (rhs, erhs) ← addPPExplicitToExposeDiff rhs erhs
|
||
let (rhsTy, erhsTy) ← addPPExplicitToExposeDiff (← inferType rhs) (← inferType erhs)
|
||
logErrorAt steps.back!.term m!"\
|
||
invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
|
||
but is expected to be{indentD m!"{erhs} : {erhsTy}"}"
|
||
failed := true
|
||
if failed then
|
||
throwAbortTerm
|
||
throwTypeMismatchError "'calc' expression" expectedType resultType result
|
||
|
||
/-!
|
||
Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
|
||
to unify with the LHS and RHS.
|
||
Two people have already re-implemented `elabCalcSteps` trying to do so and then reverted the changes,
|
||
not being aware of examples like https://github.com/leanprover/lean4/issues/2073
|
||
|
||
The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS.
|
||
(Consider `≤` vs `≥`. Users expect to be able to use `calc` to prove `≥` using chained `≤`!)
|
||
Furthermore, the types of the LHS and RHS do not need to be the same (consider `x ∈ S` as a relation),
|
||
so we also cannot use the expected LHS and RHS as type hints.
|
||
-/
|
||
|
||
/-- Elaborator for the `calc` term mode variant. -/
|
||
@[builtin_term_elab Lean.calc]
|
||
def elabCalc : TermElab
|
||
| `(calc%$tk $steps:calcSteps), expectedType? => withRef tk do
|
||
let steps ← mkCalcStepViews steps
|
||
let (result, _) ← elabCalcSteps steps
|
||
ensureHasTypeWithErrorMsgs expectedType? result
|
||
(mkImmedErrorMsg := fun _ => throwCalcFailure steps)
|
||
(mkErrorMsg := fun _ => throwCalcFailure steps)
|
||
| _, _ => throwUnsupportedSyntax
|
||
|
||
end Lean.Elab.Term
|