blob: 17c30fdc42c40391a845a818a2414a9415f2492a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
import Scanner.Protocol
import Scanner.Parser
import Scanner.Processor
import Scanner.Generator
open WaylandScanner
def parseRawProtocol (path : System.FilePath) : IO Raw.ProtocolDesc := do
parse (← IO.FS.readFile path)
|>.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
|>.mapM parseRawProtocol
let clientProtocols ← processProtocols rawProtocols
|> IO.ofExcept
let rootModuleComponents := rootModule.split "."
|>.map String.Slice.toString
|>.toArray
let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
IO.FS.createDirAll rootModulePath
for protocol in clientProtocols do
writeProtocol protocol rootModule rootModulePath
writeIndex clientProtocols rootModule rootModulePath
return 0
def usage : IO UInt32 := do
IO.println "Usage:"
IO.println " lake exe WaylandScanner -- <rootModule> <outPath> <srcPath>"
IO.println ""
IO.println "Description:"
IO.println " Read all (XML) protocols from the <srcPath> directory and"
IO.println " generate bindings in the <rootModule> namespace, where the"
IO.println " root source path is located at <outPath>."
return 1
def main (args : List String) : IO UInt32 :=
match args with
| [rootModule, outPath, srcPath] => process rootModule outPath srcPath
| _ => usage
|
