summaryrefslogtreecommitdiff
path: root/tools/Scanner.lean
diff options
context:
space:
mode:
authorHannes Schulze <haschu0103@outlook.de>2026-04-05 16:15:03 +0200
committerHannes Schulze <haschu0103@outlook.de>2026-04-05 16:15:03 +0200
commit1f5491a5af7bd0f1ec4046994d6344886465cba5 (patch)
tree9ca3af2221cdbc302b932b67965791a8065699a9 /tools/Scanner.lean
parentad4d34bba7671fdf75850a312c7eeeaeb990a9d3 (diff)
initial codegen
Diffstat (limited to 'tools/Scanner.lean')
-rw-r--r--tools/Scanner.lean25
1 files changed, 22 insertions, 3 deletions
diff --git a/tools/Scanner.lean b/tools/Scanner.lean
index 81b4181..1daed2a 100644
--- a/tools/Scanner.lean
+++ b/tools/Scanner.lean
@@ -1,6 +1,7 @@
import Scanner.Protocol
import Scanner.Parser
import Scanner.Processor
+import Scanner.Generator
open WaylandScanner
@@ -9,6 +10,24 @@ def parseRawProtocol (path : System.FilePath) : IO Raw.ProtocolDesc := do
|>.mapError (fun ε ↦ s!"{path}: {ε}")
|> IO.ofExcept
+def writeProtocol (protocol : Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+ let protocolPath := rootModulePath / protocol.name.pascalCase
+ IO.FS.createDirAll protocolPath
+ let umbrellaPath := protocolPath.addExtension "lean"
+ IO.FS.writeFile umbrellaPath <| generateUmbrella rootModule protocol
+ let headerPath := protocolPath / "Header.lean"
+ IO.FS.writeFile headerPath <| generateHeader rootModule protocol
+ let interfacePath := protocolPath / "Interface.lean"
+ IO.FS.writeFile interfacePath <| generateInterface rootModule protocol
+ let resolvedPath := protocolPath / "Resolved.lean"
+ IO.FS.writeFile resolvedPath <| generateResolved rootModule protocol
+ let requestsPath := protocolPath / "Requests.lean"
+ IO.FS.writeFile requestsPath <| generateRequests rootModule protocol
+
+def writeIndex (protocols : Array Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+ let indexPath := rootModulePath.addExtension "lean"
+ IO.FS.writeFile indexPath <| generateIndex rootModule protocols
+
def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do
let rawProtocols ← (← srcPath.readDir)
|>.map IO.FS.DirEntry.path
@@ -19,10 +38,10 @@ def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.
|>.map String.Slice.toString
|>.toArray
let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
- IO.println (reprStr clientProtocols)
IO.FS.createDirAll rootModulePath
- let indexPath := rootModulePath.addExtension "lean"
- IO.FS.writeFile indexPath ""
+ for protocol in clientProtocols do
+ writeProtocol protocol rootModule rootModulePath
+ writeIndex clientProtocols rootModule rootModulePath
return 0
def usage : IO UInt32 := do