rely on impls more

cedar-lean/CedarProto/EntityDecl.lean

@@ -38,14 +38,6 @@ deriving Repr, Inhabited
 
 namespace EntityDecl
 
-@[inline]
-def mergeOption [Field α] (x1 x2 : Option α) : Option α :=
-  match x1, x2 with
-  | some s1, some s2 => some (Field.merge s1 s2)
-  | none, some x => some x
-  | some x, none => some x
-  | none, none => none
-
 @[inline]
 def mergeName (result : EntityDecl) (x : Spec.Name) : EntityDecl :=
   {result with
@@ -67,7 +59,7 @@ def mergeAttributes (result : EntityDecl) (x : Proto.Map String (Qualified Proto
 @[inline]
 def mergeTags (result : EntityDecl) (x : ProtoType) : EntityDecl :=
   {result with
-    tags := mergeOption result.tags (some x)
+    tags := Field.merge result.tags (some x)
   }
 
 @[inline]
@@ -82,7 +74,7 @@ def merge (x y : EntityDecl) : EntityDecl :=
     name := Field.merge x.name y.name
     descendants := y.descendants ++ x.descendants
     attrs := x.attrs ++ y.attrs
-    tags := mergeOption x.tags y.tags
+    tags := Field.merge x.tags y.tags
     enums := x.enums ++ y.enums
   }
 

cedar-lean/Protobuf/Field.lean

@@ -37,11 +37,6 @@ namespace Merge
 @[inline]
 def override (_ : α) (x : α) : α := x
 
-/-- Concatenation semantics, combines two arrays -/
-@[inline]
-def concatenate (x1 : Array α) (x2 : Array α) : Array α :=
-  x1.append x2
-
 end Merge
 
 @[inline]
@@ -58,6 +53,15 @@ def guardWireType {α : Type} [Field α] (wt : WireType) : BParsec Unit := do
   if foundWt ≠ wt then
     throw s!"WireType mismatch: found {repr foundWt}, expected {repr wt}"
 
+instance [Field α] : Field (Option α) where
+  parse := do
+    let a : α ← Field.parse
+    pure (some a)
+  merge
+  | some a1, some a2 => some (Field.merge a1 a2)
+  | _, a2 => a2
+  expectedWireType := Field.expectedWireType α
+
 @[inline]
 def fromInterField {α β : Type} [Inhabited α] [Field α] (convert : α → β) (merge : β → β → β) : Field β := {
   parse := do

cedar-lean/Protobuf/Map.lean

@@ -67,7 +67,7 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar
 instance {α β : Type} [Inhabited α] [Inhabited β] [Field α] [Field β] : Field (Map α β) := {
   parse := parse
   expectedWireType := WireType.LEN
-  merge := Field.Merge.concatenate
+  merge := (· ++ ·)
 }
 end Map
 end Proto

cedar-lean/Protobuf/Packed.lean

@@ -43,16 +43,22 @@ instance [Repr α] [Field α] : Repr (Repeated α) := by
   unfold Repeated
   apply inferInstance
 
+instance [Field α] : HAppend (Repeated α) (Repeated α) (Repeated α) where
+  hAppend a b :=
+    let a : Array α := a
+    let b : Array α := b
+    a ++ b
+
 /-- Parses one value from a record -/
 @[inline]
 def parse (α : Type) [Field α] : BParsec (Array α) := do
   let element ← Field.parse
   pure #[element]
 
 instance [Field α] : Field (Repeated α) := {
-  parse := (parse α)
+  parse := parse α
   expectedWireType := Field.expectedWireType α
-  merge := Field.Merge.concatenate
+  merge := (· ++ ·)
 }
 
 end Repeated
@@ -76,6 +82,12 @@ instance [Repr α] [Field α] : Repr (Packed α) := by
   unfold Packed
   apply inferInstance
 
+instance [Field α] : HAppend (Packed α) (Packed α) (Packed α) where
+  hAppend a b :=
+    let a : Array α := a
+    let b : Array α := b
+    a ++ b
+
 @[inline]
 def parse (α : Type) [Field α] : BParsec (Array α) := do
   let len_size ← Len.parseSize
@@ -86,9 +98,9 @@ def parse (α : Type) [Field α] : BParsec (Array α) := do
     #[]
 
 instance [Field α] : Field (Packed α) := {
-  parse := (parse α)
+  parse := parse α
   expectedWireType := WireType.LEN
-  merge := Field.Merge.concatenate
+  merge := (· ++ ·)
 }
 
 end Packed