diff options
| -rw-r--r-- | lib/Wayland.lean | 1 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 5 | ||||
| -rw-r--r-- | lib/Wayland/Helpers.lean | 15 | ||||
| -rw-r--r-- | server/server.c | 24 | ||||
| -rw-r--r-- | src/Waylean.lean | 36 | ||||
| -rw-r--r-- | tools/Scanner/Generator.lean | 70 | ||||
| -rw-r--r-- | tools/Scanner/Processor.lean | 13 | ||||
| -rw-r--r-- | tools/Scanner/Protocol.lean | 13 |
8 files changed, 129 insertions, 48 deletions
diff --git a/lib/Wayland.lean b/lib/Wayland.lean index c9a06fa..5f78211 100644 --- a/lib/Wayland.lean +++ b/lib/Wayland.lean @@ -4,3 +4,4 @@ import Wayland.Basic.PosixSignal import Wayland.Basic.Lens import Wayland.Display import Wayland.Protocols +import Wayland.Helpers diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 9ba60bc..70f5c67 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -101,7 +101,7 @@ class Interface (ι : InterfaceName) where version : UInt32 /-- Interface where all dependency interfaces can be resolvew. -/ -class ResolvedInterface (ι : InterfaceName) where +class ResolvedInterface (ι : InterfaceName) extends Interface ι where referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp -- TODO: Verify that dependencies of interfaces are in referencedInterfaces @@ -367,8 +367,7 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter events := iface'.events.map MessageDesc.toNative } (setComplete := if ι' == ι then 1 else 0) -/-- Get the `wl_display` instance within the display monad. -/ -def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do +def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do let proxy ← Native.Proxy.fromDisplay (← read).disp return ⟨proxy⟩ diff --git a/lib/Wayland/Helpers.lean b/lib/Wayland/Helpers.lean new file mode 100644 index 0000000..7230fc2 --- /dev/null +++ b/lib/Wayland/Helpers.lean @@ -0,0 +1,15 @@ +import Wayland.Display +import Wayland.Protocols + +-- Helpers that depend on the protocols and can thus not be included in `Display.lean`. + +namespace Wayland + +open Protocols + +variable {σ : Type} + +/-- Get the `wl_display` instance within the display monad. -/ +def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay' + +end Wayland diff --git a/server/server.c b/server/server.c index 3687865..1264513 100644 --- a/server/server.c +++ b/server/server.c @@ -8,6 +8,28 @@ static void die(char const* s) exit(EXIT_FAILURE); } +static void on_release_shm(struct wl_client* client, struct wl_resource* resource) +{ + fprintf(stderr, "Releasing shm %p\n", (void*)resource); + wl_resource_destroy(resource); +} + +static const struct wl_shm_interface shm_impl = { + .release = on_release_shm, +}; + +static void on_destroy_shm(struct wl_resource* resource) +{ + fprintf(stderr, "Destroyed shm %p\n", (void*)resource); +} + +static void on_bind_shm(struct wl_client *client, void *data, uint32_t version, uint32_t id) +{ + struct wl_resource* resource = wl_resource_create(client, &wl_shm_interface, wl_shm_interface.version, id); + fprintf(stderr, "Bound shm %p\n", (void*)resource); + wl_resource_set_implementation(resource, &shm_impl, NULL, on_destroy_shm); +} + int main(int argc, char** argv) { struct wl_display* disp = wl_display_create(); @@ -18,6 +40,8 @@ int main(int argc, char** argv) printf("Compositor running on %s\n", sock); + wl_global_create(disp, &wl_shm_interface, wl_shm_interface.version, NULL, on_bind_shm); + wl_display_run(disp); wl_display_destroy(disp); diff --git a/src/Waylean.lean b/src/Waylean.lean index f7eb668..953096a 100644 --- a/src/Waylean.lean +++ b/src/Waylean.lean @@ -1,32 +1,30 @@ import Wayland -open Wayland Protocols -def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do - let callback ← display.sync - callback.listen fun - | .done _ => do - callback.keep - handler +open Wayland Protocols structure State where - count : Int + shmName : Option UInt32 := .none -partial def nextTimer : DisplayM Int Unit := do - _ ← DisplayM.registerTimer 16ms do - let newCount := (← get) + 1 - set newCount - DisplayM.liftIO (IO.println s!"Timer tick {newCount}") - nextTimer +def requireGlobal (name : String) : Option UInt32 → DisplayM State UInt32 + | .some global => pure global + | .none => DisplayM.liftIO <| throw (.userError s!"Missing required global {name}") def launch : DisplayM State Unit := do _ ← DisplayM.registerSignal .SIGINT do DisplayM.liftIO (IO.println "Received SIGINT") DisplayM.requestQuit - DisplayM.zoom (mk_lens count) nextTimer - - let disp : WlDisplay ← DisplayM.getDisplay - disp.roundtrip do + let disp ← DisplayM.getDisplay + let registry ← disp.getRegistry + registry.listen fun + | .global name "wl_shm" _ => do + DisplayM.liftIO (IO.println s!"shm global registerd ({name})") + set ({ shmName := name } : State) + | _ => pure () + disp.sync do DisplayM.liftIO (IO.println "Roundtrip complete") + let shmName ← (← get).shmName |> requireGlobal "wl_shm" + let shm : WlShm ← registry.bind shmName + shm.release def main : IO Unit := - DisplayM.run launch { count := 0 } + DisplayM.run launch { } 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 diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean index a50767f..fd952a2 100644 --- a/tools/Scanner/Processor.lean +++ b/tools/Scanner/Processor.lean @@ -87,14 +87,13 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client. | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure | .array => Client.ArgumentType.array |> pure | .fd => Client.ArgumentType.fd |> pure - | .newID => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface + | .newID => Client.ArgumentType.newID <$> raw.interface.mapM resolveInterface | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface description := raw.description } private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.RequestDesc := do let newIDArgs := raw.arguments.filter fun arg ↦ arg.type == .newID - let otherArgs := raw.arguments.filter fun arg ↦ arg.type != .newID let returnType ← match newIDArgs with | #[] => Client.ReturnType.unit |> pure @@ -107,12 +106,17 @@ private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.Re isDestructor := raw.type == .destructor since := raw.since deprecatedSince := raw.deprecatedSince - rawArguments := raw.arguments - arguments := ← otherArgs.mapM processArgument + arguments := ← raw.arguments.mapM processArgument returnType := returnType } private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.EventDesc := do + let hasInvalidArg := raw.arguments.any fun arg ↦ + match arg.type, arg.interface with + | .newID, .none => true + | _, _ => false + if hasInvalidArg then + throw s!"Event arguments of type new_id must have an interface type specified (in {raw.name})" return { name := raw.name opcode := raw.opcode @@ -120,7 +124,6 @@ private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.Even isDestructor := raw.type == .destructor since := raw.since deprecatedSince := raw.deprecatedSince - rawArguments := raw.arguments arguments := ← raw.arguments.mapM processArgument } diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean index 183ef6a..7661f1e 100644 --- a/tools/Scanner/Protocol.lean +++ b/tools/Scanner/Protocol.lean @@ -155,8 +155,10 @@ inductive ArgumentType where | array | fd | object (nullability : Nullability) (interface : Option InterfaceRef) + | newID (interface : Option InterfaceRef) deriving Repr, BEq, Inhabited +/-- Logical argument (i.e., if there is a newID without an interface, this only includes the newID, not the string and uint). -/ structure ArgumentDesc where name : Identifier type : ArgumentType @@ -171,7 +173,6 @@ structure MessageDesc where since : Nat deprecatedSince : Option Nat arguments : Array ArgumentDesc - rawArguments : Array Raw.ArgumentDesc deriving Repr, BEq, Inhabited inductive ReturnType where @@ -179,10 +180,20 @@ inductive ReturnType where | object (type : Option InterfaceRef) deriving Repr, BEq, Inhabited +def ReturnType.isWlCallback : ReturnType → Bool + | .object (.some iface) => iface.interface == "wl_callback" + | _ => false + structure RequestDesc extends MessageDesc where returnType : ReturnType deriving Repr, BEq, Inhabited +def RequestDesc.inputArguments (req : RequestDesc) : Array ArgumentDesc := + req.arguments.filter fun arg ↦ + match arg.type with + | .newID _ => false + | _ => true + structure EventDesc extends MessageDesc deriving Repr, BEq, Inhabited |