From 3bc82a7636e1f8606801adbcc8df409aa4864548 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Wed, 3 Aug 2022 18:32:47 -0400
Subject: [PATCH] feat: add include_str

---
 src/Lean/Elab.lean            |  1 +
 src/Lean/Elab/IncludeStr.lean | 30 ++++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 src/Lean/Elab/IncludeStr.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 62ab7fdcf9..06cd4d5439 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -43,3 +43,4 @@ import Lean.Elab.BuiltinCommand
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.Eval
 import Lean.Elab.Calc
+import Lean.Elab.IncludeStr
diff --git a/src/Lean/Elab/IncludeStr.lean b/src/Lean/Elab/IncludeStr.lean
new file mode 100644
index 0000000000..4a1e9190c9
--- /dev/null
+++ b/src/Lean/Elab/IncludeStr.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Xubai Wang, Wojciech Nawrocki
+-/
+
+import Lean.Elab.Term
+import Lean.Elab.Eval
+
+namespace Lean.Elab.Term
+
+private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=
+  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx
+
+@[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
+
+end Lean.Elab.Term