diff options
Diffstat (limited to 'tools/Scanner/Generator.lean')
| -rw-r--r-- | tools/Scanner/Generator.lean | 80 |
1 files changed, 43 insertions, 37 deletions
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean index 5884a0d..1f889d0 100644 --- a/tools/Scanner/Generator.lean +++ b/tools/Scanner/Generator.lean @@ -68,6 +68,21 @@ private def resolveEnum (enum : EnumRef) : Generator String := do let iface ← resolveInterface enum.toInterfaceRef return s!"{iface}.{enum.enum.pascalCase}" +private def typeToLean : ArgumentType → Generator String + | .int .none => do return "Int32" + | .int (.some enum) => resolveEnum enum + | .uint .none => do return "UInt32" + | .uint (.some enum) => resolveEnum enum + | .fixed => do return "Float32" + | .string .nullable => do return "Option String" + | .string .notNull => do return "String" + | .array => do return "ByteArray" + | .fd => do return "Fd" + | .object .nullable .none => do return "Option AnyObject" + | .object .nullable (.some iface) => do return s!"Option {← resolveInterface iface}" + | .object .notNull .none => do return s!"AnyObject" + | .object .notNull (.some iface) => resolveInterface iface + section Header private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do @@ -76,7 +91,7 @@ private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do private def emitObjectDefinitions (protocol : ProtocolDesc) : Generator Unit := do for iface in protocol.interfaces do - emitLine s!"def {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name" + emitLine s!"abbrev {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name" private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do for iface in protocol.interfaces do @@ -91,6 +106,15 @@ private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do for entry in enum.entries do emitLine s!" | {entry.name.camelCase}" +private def emitEnumMarshallable (protocol : ProtocolDesc) : Generator Unit := do + for iface in protocol.interfaces do + for enum in iface.enums do + emitLine s!"" + emitLine s!"instance : Marshallable {iface.name.pascalCase}.{enum.name.pascalCase} where" + emitLine s!" marshal := sorry" + emitLine s!" demarshal := sorry" + -- TODO + def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Header" do emitNamespace rootModule do @@ -99,6 +123,7 @@ def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String := emitLine "" emitObjectDefinitions protocol emitEnumDefinitions protocol + emitEnumMarshallable protocol end Header @@ -110,21 +135,7 @@ private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := d for event in iface.events do emitLine s!" | {event.name.camelCase}" for arg in event.arguments do - let argName := arg.name.camelCase - match arg.type with - | .int .none => emitLine s!" ({argName} : Int32)" - | .int (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})" - | .uint .none => emitLine s!" ({argName} : UInt32)" - | .uint (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})" - | .fixed => emitLine s!" ({argName} : Float)" - | .string .nullable => emitLine s!" ({argName} : Option String)" - | .string .notNull => emitLine s!" ({argName} : String)" - | .array => emitLine s!" ({argName} : ByteArray)" - | .fd => emitLine s!" ({argName} : Int32)" - | .object .nullable .none => emitLine s!" ({argName} : Option AnyObject)" - | .object .nullable (.some iface) => emitLine s!" ({argName} : Option {← resolveInterface iface})" - | .object .notNull .none => emitLine s!" ({argName} : AnyObject)" - | .object .notNull (.some iface) => emitLine s!" ({argName} : {← resolveInterface iface})" + emitLine s!" ({arg.name.camelCase} : {← typeToLean arg.type})" emitLine s!"" private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := do @@ -168,8 +179,13 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := for ev in iface.events do emitMessageDesc ev.toMessageDesc emitLine s!" ]" - emitLine s!" demarshalEvent := sorry" - -- TODO + emitLine s!" demarshalEvent" + for ev in iface.events do + emitLine s!" | {ev.opcode} => do" + emitLine s!" return .{ev.name.camelCase}" + for _ in ev.arguments do + emitLine s!" (← Marshallable.demarshal)" + emitLine " | _ => throw s!\"Received invalid opcode\"" def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Interface" do @@ -212,34 +228,24 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do emitLine s!" (ω : {iface.name.pascalCase})" -- TODO: Special wl_callback handling for arg in req.arguments do - let argName := arg.name.camelCase - match arg.type with - | .int .none => emitLine s!" ({argName} : Int32)" - | .int (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})" - | .uint .none => emitLine s!" ({argName} : UInt32)" - | .uint (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})" - | .fixed => emitLine s!" ({argName} : Float)" - | .string .nullable => emitLine s!" ({argName} : Option String)" - | .string .notNull => emitLine s!" ({argName} : String)" - | .array => emitLine s!" ({argName} : ByteArray)" - | .fd => emitLine s!" ({argName} : Int32)" - | .object .nullable .none => emitLine s!" ({argName} : Option AnyObject)" - | .object .nullable (.some iface) => emitLine s!" ({argName} : Option {← resolveInterface iface (suffix := ".Resolved")})" - | .object .notNull .none => emitLine s!" ({argName} : AnyObject)" - | .object .notNull (.some iface) => emitLine s!" ({argName} : {← resolveInterface iface (suffix := ".Resolved")})" + emitLine s!" ({arg.name.camelCase} : {← typeToLean arg.type})" match req.returnType with | .unit => emitLine s!" : DisplayM σ Unit :=" - | .object .none => emitLine s!" : DisplayM σ AnyObject :=" + | .object .none => emitLine s!" : DisplayM σ (Object ι) :=" | .object (.some iface) => emitLine s!" : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :=" - emitLine s!" sorry" - -- TODO + match req.returnType with + | .unit => emitLine s!" ω.send do" + | .object _ => emitLine s!" ω.sendConstructor do" + for arg in req.arguments do + emitLine s!" Marshallable.marshal {arg.name.camelCase}" + emitLine s!" return {req.opcode}" def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Requests" do emitNamespace rootModule do emitImport "Wayland.Display" emitLocalImport protocol.name ".Resolved" - emitLine "variable {σ : Type}" + emitLine "variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]" emitRequests protocol end Requests |