fix: move cdot and calc parsers to Lean namespace

closes #3168

src/Init/NotationExtra.lean

@@ -87,6 +87,7 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBi
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
 end
 
+namespace Lean
 -- first step of a `calc` block
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
@@ -136,6 +137,7 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
 @[inherit_doc «calc»]
 macro tk:"calc" steps:calcSteps : conv =>
   `(conv| tactic => calc%$tk $steps)
+end Lean
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
@@ -361,19 +363,19 @@ macro_rules
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
 
+namespace Lean
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
+syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
-namespace Lean
 /-! # `repeat` and `while` notation -/
 
 inductive Loop where
@@ -436,20 +438,3 @@ def insertUnexpander : Lean.PrettyPrinter.Unexpander
   | _ => throw ()
 
 end Lean
-
--- TODO: delete bootstrapping workaround
-
-namespace Lean
-
-syntax (name := cdot) "mycdot" : tactic
-
-syntax (name := «calc») "mycalc" : term
-
-syntax (name := calcTactic) "mycalc" : tactic
-
-syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
--- enforce indentation of calc steps so we know when to stop parsing them
-syntax calcStep := ppIndent(colGe term " := " term)
-syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine linebreak calcStep)*)
-
-end Lean

src/Lean/Elab/Calc.lean

@@ -121,121 +121,3 @@ def elabCalc : TermElab := fun stx expectedType? => do
   return result
 
 end Lean.Elab.Term
-
-
--- TODO: delete
-namespace Old
-open Lean Elab Term 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)) :=
-  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}\n{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
-
-def getCalcFirstStep (step0 : TSyntax ``_root_.calcFirstStep) : TermElabM (TSyntax ``_root_.calcStep) :=
-  withRef step0 do
-  match step0  with
-  | `(_root_.calcFirstStep| $term:term) =>
-    `(_root_.calcStep| $term = _ := rfl)
-  | `(_root_.calcFirstStep| $term := $proof) =>
-    `(_root_.calcStep| $term := $proof)
-  | _ => throwUnsupportedSyntax
-
-def getCalcSteps (steps : TSyntax ``_root_.calcSteps) : TermElabM (Array (TSyntax ``_root_.calcStep)) :=
-  match steps with
-  | `(_root_.calcSteps|
-        $step0:calcFirstStep
-        $rest*) => do
-    let step0 ← getCalcFirstStep step0
-    pure (#[step0] ++ rest)
-  | _ => unreachable!
-
-def elabCalcSteps (steps : TSyntax ``_root_.calcSteps) : TermElabM Expr := do
-  let mut result? := none
-  let mut prevRhs? := none
-  for step in ← getCalcSteps steps do
-    let `(_root_.calcStep| $pred := $proofTerm) := step | unreachable!
-    let type ← elabType <| ← do
-      if let some prevRhs := prevRhs? then
-        annotateFirstHoleWithType pred (← inferType prevRhs)
-      else
-        pure pred
-    let some (_, lhs, rhs) ← getCalcRelation? type |
-      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
-    if let some prevRhs := prevRhs? then
-      unless (← isDefEqGuarded lhs prevRhs) do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}" -- "
-    let proof ← withFreshMacroScope do elabTermEnsuringType proofTerm type
-    result? := some <| ← do
-      if let some (result, resultType) := result? then
-        synthesizeSyntheticMVarsUsingDefault
-        withRef pred do mkCalcTrans result resultType proof type
-      else
-        pure (proof, type)
-    prevRhs? := rhs
-  return result?.get!.1
-
-/-- Elaborator for the `calc` term mode variant. -/
-@[builtin_term_elab «calc»]
-def elabCalc : TermElab := fun stx expectedType? => do
-  let steps : TSyntax ``_root_.calcSteps := ⟨stx[1]⟩
-  let result ← elabCalcSteps steps
-  synthesizeSyntheticMVarsUsingDefault
-  let result ← ensureHasType expectedType? result
-  return result
-
-end Old

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -134,9 +134,6 @@ def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
     withInfoContext (pure ()) initInfo
     evalSepByIndentTactic stx[1]
 
--- TODO: delete after stage0
-@[builtin_tactic cdot] def evalTacticCDotOld : Tactic := evalTacticCDot
-
 @[builtin_tactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
   let mkInfo ← mkInitialTacticInfo stx[0]
   focus do

src/Lean/Elab/Tactic/Calc.lean

@@ -33,8 +33,4 @@ def evalCalc : Tactic := fun stx => withMainContext do
   (← getMainGoal).assign val
   replaceMainGoal mvarIds
 
--- TODO: delete
-@[builtin_tactic calcTactic]
-def evalCalcOld : Tactic := evalCalc
-
 end Lean.Elab.Tactic