diff options
Diffstat (limited to 'tools/Scanner/Generator.lean')
| -rw-r--r-- | tools/Scanner/Generator.lean | 70 |
1 files changed, 50 insertions, 20 deletions
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean index 1f889d0..76542e7 100644 --- a/tools/Scanner/Generator.lean +++ b/tools/Scanner/Generator.lean @@ -82,6 +82,8 @@ private def typeToLean : ArgumentType → Generator String | .object .nullable (.some iface) => do return s!"Option {← resolveInterface iface}" | .object .notNull .none => do return s!"AnyObject" | .object .notNull (.some iface) => resolveInterface iface + | .newID .none => do return s!"AnyObject" + | .newID (.some iface) => resolveInterface iface section Header @@ -142,23 +144,24 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := let emitMessageDesc (msg : MessageDesc) : Generator Unit := do emitLine " {" emitLine s!" name := {msg.name.quoted}" - let nullability (arg : Raw.ArgumentDesc) : String := - if arg.allowNull then ".nullable" else ".notNull" - let interfaceName (arg : Raw.ArgumentDesc) : String := - match arg.interface with - | .some iface => s!"(.some \"{iface}\")" - | .none => ".none" - let argumentDesc (arg : Raw.ArgumentDesc) : String := + let nullability : Nullability → String + | .nullable => ".nullable" + | .notNull => ".notNull" + let interfaceName : Option InterfaceRef → String + | .some iface => s!"(.some {iface.interface.quoted})" + | .none => ".none" + let argumentDesc (arg : ArgumentDesc) : String := match arg.type with - | .int => ".int" - | .uint => ".uint" - | .fixed => ".fixed" - | .string => s!".string {nullability arg}" - | .object => s!".object {nullability arg} {interfaceName arg}" - | .newID => s!".newID {interfaceName arg}" - | .array => ".array" - | .fd => ".fd" - let args := msg.rawArguments + | .int _ => ".int" + | .uint _ => ".uint" + | .fixed => ".fixed" + | .string null => s!".string {nullability null}" + | .object null iface => s!".object {nullability null} {interfaceName iface}" + | .newID (.some iface) => s!".newID (.some {iface.interface.quoted})" + | .newID .none => ".string .notNull, .uint, .newID .none" + | .array => ".array" + | .fd => ".fd" + let args := msg.arguments |>.map argumentDesc |>.toList |> String.intercalate ", " @@ -223,11 +226,15 @@ section Requests private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do for iface in protocol.interfaces do for req in iface.requests do + let baseName := s!"{iface.name.pascalCase}.{req.name.camelCase}" + let rawName := + if req.returnType.isWlCallback + then baseName ++ ".raw" + else baseName emitLine s!"" - emitLine s!"def {iface.name.pascalCase}.{req.name.camelCase}" + emitLine s!"def {rawName}" emitLine s!" (ω : {iface.name.pascalCase})" - -- TODO: Special wl_callback handling - for arg in req.arguments do + for arg in req.inputArguments do emitLine s!" ({arg.name.camelCase} : {← typeToLean arg.type})" match req.returnType with | .unit => emitLine s!" : DisplayM σ Unit :=" @@ -237,8 +244,31 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do | .unit => emitLine s!" ω.send do" | .object _ => emitLine s!" ω.sendConstructor do" for arg in req.arguments do - emitLine s!" Marshallable.marshal {arg.name.camelCase}" + match arg.type with + | .newID (.some _) => + emitLine s!" ArgumentMarshaller.marshalAnyObject .none" + | .newID .none => + emitLine s!" ArgumentMarshaller.marshalString (.some ι)" + emitLine s!" ArgumentMarshaller.marshalUInt (inferInstanceAs (Interface ι)).version" + emitLine s!" ArgumentMarshaller.marshalAnyObject .none" + | _ => + emitLine s!" Marshallable.marshal {arg.name.camelCase}" emitLine s!" return {req.opcode}" + -- Special case wl_callback handling + if req.returnType.isWlCallback then + emitLine s!"" + emitLine s!"def {baseName}" + emitLine s!" (ω : {iface.name.pascalCase})" + for arg in req.inputArguments do + emitLine s!" ({arg.name.camelCase} : {← typeToLean arg.type})" + emitLine s!" (γ : DisplayM σ Unit)" + emitLine s!" : DisplayM σ Unit := do" + let argNames := #["ω"] ++ (req.inputArguments.map fun arg ↦ arg.name.camelCase) + |>.toList + |> String.intercalate " " + emitLine s!" let ρ ← {rawName} {argNames}" + emitLine s!" ρ.listen fun" + emitLine s!" | .done _ => do ρ.keep; γ" def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Requests" do |