From 924241fd20f582fe0935db960ed3f06a65920f6d Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 6 Apr 2026 09:26:02 +0200 Subject: add river protocols --- tools/Scanner/Generator.lean | 69 ++++++++++++++++++++++---------------------- 1 file changed, 35 insertions(+), 34 deletions(-) (limited to 'tools/Scanner') diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean index f2514f4..36c1212 100644 --- a/tools/Scanner/Generator.lean +++ b/tools/Scanner/Generator.lean @@ -122,39 +122,40 @@ private def emitEnumMarshallable (protocol : ProtocolDesc) : Generator Unit := d 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" - if enum.bitfield then - emitLine s!" marshal" - emitLine s!" | .uint, μ => ArgumentMarshaller.marshalUInt <|" - emitLine s!" 0" - for entry in enum.entries do - emitLine s!" ||| (if μ.{entry.name.camelCase} then {entry.value} else 0)" - emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected uint.\"" - emitLine s!" demarshal" - emitLine s!" | .uint => do" - emitLine s!" let μ ← ArgumentDemarshaller.demarshalUInt" - emitLine " return {" - for entry in enum.entries do - emitLine s!" {entry.name.camelCase} := (μ &&& {entry.value}) == {entry.value}" - emitLine " }" - emitLine s!" | _ => throw \"Demarshalling unexpected type, expected uint.\"" - else - emitLine s!" marshal" - for entry in enum.entries do - emitLine s!" | .int, .{entry.name.camelCase} => ArgumentMarshaller.marshalInt {entry.value}" - emitLine s!" | .uint, .{entry.name.camelCase} => ArgumentMarshaller.marshalUInt {entry.value}" - emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected int or uint.\"" - emitLine s!" demarshal" - let emitMatch (demarshal : String) : Generator Unit := do - emitLine s!" match (← ArgumentDemarshaller.{demarshal}) with" + emitNamespace s!"{iface.name.pascalCase}.{enum.name.pascalCase}" do + emitLine s!"instance : Marshallable {iface.name.pascalCase}.{enum.name.pascalCase} where" + if enum.bitfield then + emitLine s!" marshal" + emitLine s!" | .uint, μ => ArgumentMarshaller.marshalUInt <|" + emitLine s!" 0" + for entry in enum.entries do + emitLine s!" ||| (if μ.{entry.name.camelCase} then {entry.value} else 0)" + emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected uint.\"" + emitLine s!" demarshal" + emitLine s!" | .uint => do" + emitLine s!" let μ ← ArgumentDemarshaller.demarshalUInt" + emitLine " return {" + for entry in enum.entries do + emitLine s!" {entry.name.camelCase} := (μ &&& {entry.value}) == {entry.value}" + emitLine " }" + emitLine s!" | _ => throw \"Demarshalling unexpected type, expected uint.\"" + else + emitLine s!" marshal" for entry in enum.entries do - emitLine s!" | {entry.value} => pure .{entry.name.camelCase}" - emitLine s!" | _ => throw \"Invalid enum value.\"" - emitLine s!" | .int => do" - emitMatch "demarshalInt" - emitLine s!" | .uint => do" - emitMatch "demarshalUInt" - emitLine s!" | _ => throw \"Demarshalling unexpected type, expected int or uint.\"" + emitLine s!" | .int, .{entry.name.camelCase} => ArgumentMarshaller.marshalInt {entry.value}" + emitLine s!" | .uint, .{entry.name.camelCase} => ArgumentMarshaller.marshalUInt {entry.value}" + emitLine s!" | _, _ => throw \"Marshalling unexpected type, expected int or uint.\"" + emitLine s!" demarshal" + let emitMatch (demarshal : String) : Generator Unit := do + emitLine s!" match (← ArgumentDemarshaller.{demarshal}) with" + for entry in enum.entries do + emitLine s!" | {entry.value} => pure .{entry.name.camelCase}" + emitLine s!" | _ => throw \"Invalid enum value.\"" + emitLine s!" | .int => do" + emitMatch "demarshalInt" + emitLine s!" | .uint => do" + emitMatch "demarshalUInt" + emitLine s!" | _ => throw \"Demarshalling unexpected type, expected int or uint.\"" def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String := Generator.runProtocol rootModule protocol ".Header" do @@ -210,7 +211,7 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := emitLine " }," for iface in protocol.interfaces do emitLine s!"" - emitLine s!"instance : Interface {iface.name.pascalCase}.name where" + emitLine s!"instance instInterface{iface.name.pascalCase} : Interface {iface.name.pascalCase}.name where" emitLine s!" event := {iface.name.pascalCase}.Event" emitLine s!" version := {iface.version}" emitLine s!" requests := #[" @@ -243,7 +244,7 @@ section Resolved private def emitResolvedInterfaces (protocol : ProtocolDesc) : Generator Unit := do for iface in protocol.interfaces do - emitLine s!"instance : ResolvedInterface {iface.name.pascalCase}.name where" + emitLine s!"instance instResolvedInterface{iface.name.pascalCase} : ResolvedInterface {iface.name.pascalCase}.name where" emitLine s!" referencedInterfaces := #[" for ref in iface.referencedInterfaces do let name ← resolveInterface ref (suffix := ".Interface") -- cgit v1.3.1