From 9c78f6fa0e6ddb07b7601227d11a7e3c81de2dcd Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Thu, 4 Aug 2022 07:41:03 -0400
Subject: [PATCH] feat: make include_str a builtin

---
 src/Init/Notation.lean        |  5 +++++
 src/Lean/Elab/IncludeStr.lean | 21 ++++++++++-----------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 58bdef4538..ea4bf65dd3 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -316,3 +316,8 @@ instance : Coe Syntax (TSyntax `rawStx) where
 scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
 
 syntax (name := deprecated) "deprecated " (ident)? : attr
+
+/-- When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
+a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
+file cannot be read, elaboration fails. -/
+syntax (name := includeStr) "include_str" term : term
diff --git a/src/Lean/Elab/IncludeStr.lean b/src/Lean/Elab/IncludeStr.lean
index 4a1e9190c9..d9fc35a61c 100644
--- a/src/Lean/Elab/IncludeStr.lean
+++ b/src/Lean/Elab/IncludeStr.lean
@@ -15,16 +15,15 @@ private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath
 @[implementedBy evalFilePathUnsafe]
 private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
 
-/-- When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
-a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
-file cannot be read, elaboration fails. -/
-elab (name := includeStr) "include_str " path:term : term => do
-  let path ← evalFilePath path
-  let ctx ← readThe Lean.Core.Context
-  let srcPath := System.FilePath.mk ctx.fileName
-  let some srcDir := srcPath.parent
-    | throwError "cannot compute parent directory of '{srcPath}'"
-  let path := srcDir / path
-  Lean.mkStrLit <$> IO.FS.readFile path
+@[builtinTermElab includeStr] def elabIncludeStr : TermElab
+  | `(include_str $path:term), _ => do
+    let path ← evalFilePath path
+    let ctx ← readThe Lean.Core.Context
+    let srcPath := System.FilePath.mk ctx.fileName
+    let some srcDir := srcPath.parent
+      | throwError "cannot compute parent directory of '{srcPath}'"
+    let path := srcDir / path
+    mkStrLit <$> IO.FS.readFile path
+  | _, _ => throwUnsupportedSyntax
 
 end Lean.Elab.Term