feat: expand helper macros

lean4-mode/lean4-syntax.el

@@ -19,7 +19,7 @@
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "attributes" "raw" "replacing" "generalizing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "rec" "forall" "Pi" "fun"
-    "exists" "if" "then" "else" "assume" "from" "init_quot"
+    "exists" "if" "then" "else" "assume" "from" "init_quot" "return"
     "mutual" "def" "run_cmd")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean4-keywords1-regexp
@@ -42,6 +42,9 @@
 (defconst lean4-warnings '("sorry" "exit") "lean warnings")
 (defconst lean4-warnings-regexp
   (eval `(rx word-start (or ,@lean4-warnings) word-end)))
+(defconst lean4-debugging '("unreachable" "panic" "assert" "dbgTrace") "lean debugging")
+(defconst lean4-debugging-regexp
+  (eval `(rx word-start (or ,@lean4-debugging))))
 
 
 (defconst lean4-syntax-table
@@ -168,6 +171,7 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; warnings
      (,lean4-warnings-regexp . 'font-lock-warning-face)
+     (,lean4-debugging-regexp . 'font-lock-warning-face)
      ;; escaped identifiers
      (,(rx (and (group "«") (group (one-or-more (not (any "»")))) (group "»")))
       (1 font-lock-comment-face t)

src/Init/Util.lean

@@ -38,6 +38,12 @@ constant panic {α : Type u} [Inhabited α] (msg : String) : α := arbitrary _
 @[neverExtract, inline] def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
 panic (mkPanicMessage modName line col msg)
 
+@[noinline] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
+"PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
+
+@[neverExtract, inline] def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
+panic (mkPanicMessageWithDecl modName declName line col msg)
+
 -- TODO: should be a macro
 @[neverExtract, noinline, nospecialize] def unreachable! {α : Type u} [Inhabited α] : α :=
 panic! "unreachable"

src/Lean/Elab/BuiltinNotation.lean

@@ -250,6 +250,40 @@ fun stx => do
 @[builtinMacro Lean.Parser.Term.not] def expandNot : Macro := expandPrefixOp `Not
 @[builtinMacro Lean.Parser.Term.bnot] def expandBNot : Macro := expandPrefixOp `not
 
+@[builtinTermElab panic] def elabPanic : TermElab :=
+fun stx expectedType? => do
+  let arg := stx.getArg 1;
+  pos ← getRefPosition;
+  env ← getEnv;
+  declName? ← getDeclName?;
+  stxNew ← match declName? with
+  | some declName => `(panicWithPosWithDecl $(quote (toString env.mainModule)) $(quote (toString declName)) $(quote pos.line) $(quote pos.column) $arg)
+  | none => `(panicWithPos $(quote (toString env.mainModule)) $(quote pos.line) $(quote pos.column) $arg);
+  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+
+@[builtinMacro Lean.Parser.Term.unreachable]  def expandUnreachable : Macro :=
+fun stx => `(panic! "unreachable code has been reached")
+
+@[builtinMacro Lean.Parser.Term.assert]  def expandAssert : Macro :=
+fun stx =>
+  -- TODO: support for disabling runtime assertions
+  let cond := stx.getArg 1;
+  let body := stx.getArg 3;
+  match cond.reprint with
+  | some code => `(if $cond then $body else panic! ("assertion violation: " ++ $(quote code)))
+  | none => `(if $cond then $body else panic! ("assertion violation"))
+
+@[builtinMacro Lean.Parser.Term.dbgTrace]  def expandDbgTrace : Macro :=
+fun stx =>
+  let arg  := stx.getArg 1;
+  let body := stx.getArg 3;
+  `(dbgTrace $arg fun _ => $body)
+
+@[builtinMacro Lean.Parser.Term.return]  def expandReturn : Macro :=
+fun stx =>
+  let arg := stx.getArg 1;
+  `(pure $arg)
+
 /-
 TODO
 @[builtinTermElab] def elabsubst : TermElab := expandInfixOp infixR " ▸ " 75

src/Lean/Parser/Term.lean

@@ -246,7 +246,7 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
-@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable! " >> termParser
+@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
 @[builtinTermParser] def dbgTrace    := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
 @[builtinTermParser] def assert      := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
 @[builtinTermParser] def «return»    := parser!:leadPrec "return " >> termParser

tests/lean/dbgMacros.lean

@@ -0,0 +1,34 @@
+new_frontend
+
+def f (x : Nat) :=
+if x = 0 then panic! "unexpected zero"
+else x - 1
+
+#eval f 0
+
+#eval f 10
+
+def g (x : Nat) :=
+if x = 0 then unreachable!
+else x - 1
+
+#eval g 0
+
+def h (x : Nat) :=
+assert! x != 0;
+x - 1
+
+#eval h 1
+#eval h 0
+
+def f2 (x : Nat) :=
+dbgTrace! "f2, x: " ++ toString x;
+x + 1
+
+#eval f2 10
+
+def g2 (x : Nat) : IO Nat := do
+IO.println "g2 started";
+return x + 1
+
+#eval g2 10

tests/lean/dbgMacros.lean.expected.out

@@ -0,0 +1,12 @@
+PANIC at f dbgMacros:4:14: unexpected zero
+PANIC at g dbgMacros:12:14: unreachable code has been reached
+PANIC at h dbgMacros:18:0: assertion violation: x != 0
+f2, x: 10
+0
+9
+0
+0
+0
+11
+g2 started
+11