max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make include_str a builtin

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-08-04 07:41:03 -04:00 • committed by Leonardo de Moura
parent 3bc82a7636
commit 9c78f6fa0e
2 changed files with 15 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Notation.lean
View file

@ -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

21
src/Lean/Elab/IncludeStr.lean
View file

@ -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