add river protocols

1 files changed, 35 insertions, 34 deletions

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")