Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.ReadableSExpr

set_option doc.verso true

File I/O for readable S-expressions

Read and write the readable rose syntax using Geb.Rsexp.parse and Geb.Rsexp.print. Syntax errors and labels outside Fin k return none; filesystem errors remain IO.Error exceptions.

Main definitions

Geb.Rsexp.readFile: read a readable rose expression.
Geb.Rsexp.writeFile: write its normalized readable spelling.

Implementation notes

IO.FS.readBinFile supplies bytes, mapped individually to characters. The grammar uses ASCII labels, delimiters and whitespace; other bytes are rejected by the parser. Reads hold the complete file in memory. IO.FS.writeFile creates or truncates the output, without adding a newline. Compose a read with Option.map Geb.Ast.ofRose to obtain a binary tree; compose Geb.Ast.toRose with the writer to serialize one.

Tags

readable S-expression, file I/O, binary tree, rose tree

public sectionnamespace Geb.Rsexp

Read a readable expression, accepting the parser's leading and trailing whitespace.

def readFile (k : Nat) (path : System.FilePath) : IO (Option (Rose k)) := do
  return parse k ((← IO.FS.readBinFile path).data.toList.map fun b ↦ Char.ofNat b.toNat)

Write a readable expression, without a trailing newline.

def writeFile {k : Nat} (path : System.FilePath) (r : Rose k) : IO Unit :=
  IO.FS.writeFile path (String.ofList (print r))

end Geb.Rsexp