blob: d6962c756563537d34a257ddb421f052cb516084 (
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
|
import Scanner.Protocol
import Scanner.Parser
open WaylandScanner
def parseProtocol (path : System.FilePath) : IO ProtocolDesc := do
parse (← IO.FS.readFile path)
|>.mapError (fun ε ↦ s!"{path}: {ε}")
|> IO.ofExcept
def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do
let protocols ← (← srcPath.readDir)
|>.map IO.FS.DirEntry.path
|>.mapM parseProtocol
let rootModuleComponents := rootModule.split "."
|>.map String.Slice.toString
|>.toArray
let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
IO.println (reprStr protocols)
IO.FS.createDirAll rootModulePath
let indexPath := rootModulePath.addExtension "lean"
IO.FS.writeFile indexPath ""
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
|
