Log.lean

import Lean.Elab.Term

deriving instance Lean.ToExpr for String.Pos
deriving instance Lean.ToExpr for Substring
deriving instance Lean.ToExpr for Lean.SourceInfo
deriving instance Lean.ToExpr for Lean.Syntax

syntax "log! " (interpolatedStr(term) <|> term:arg) : term

@[term_elab termLog!__]
def elabLog! : Lean.Elab.Term.TermElab
  | `(log!%$tk $m:interpolatedStr), expectedType? => do
    let tk ← Lean.Elab.Term.exprToSyntax (Lean.toExpr tk)
    Lean.Elab.Term.elabTerm (← ``(Lean.logInfoAt $tk m!$m)) expectedType?
  | `(log!%$tk $m:term), expectedType? => do
    let tk ← Lean.Elab.Term.exprToSyntax (Lean.toExpr tk)
    Lean.Elab.Term.elabTerm (← ``(Lean.logInfoAt $tk $m)) expectedType?
  | _, _ => Lean.Elab.throwUnsupportedSyntax