From 2e34b1b6d7c084474dc10a7aad70e8a0125c223f Mon Sep 17 00:00:00 2001
From: Craig Disselkoen <cdiss@amazon.com>
Date: Tue, 26 Nov 2024 15:33:30 -0500
Subject: [PATCH] small refactor in Protobuf/Map.lean

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
---
 cedar-lean/Protobuf/Map.lean | 26 ++++++--------------------
 1 file changed, 6 insertions(+), 20 deletions(-)

diff --git a/cedar-lean/Protobuf/Map.lean b/cedar-lean/Protobuf/Map.lean
index 0de0ecf6..07d35c7c 100644
--- a/cedar-lean/Protobuf/Map.lean
+++ b/cedar-lean/Protobuf/Map.lean
@@ -46,11 +46,7 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar
      let tag1 ← Tag.parse
      let result ← match tag1.fieldNum with
           | 1 =>
-               let foundWt1 := Field.expectedWireType KeyT
-               if foundWt1 ≠ tag1.wireType then
-                    throw s!"WireType mismatch: found {repr foundWt1}, expected {repr tag1.wireType}"
-               else
-               let key : KeyT ← Field.parse
+               let key : KeyT ← Field.guardedParse tag1
 
                -- Since the fields are optional, check to see if we're done parsing now
                let curPos ← BParsec.pos
@@ -59,21 +55,14 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar
                else
 
                let tag2 ← Tag.parse
-               let foundWt2 := Field.expectedWireType ValueT
-               if foundWt2 ≠ tag2.wireType then
-                    throw s!"WireType mismatch: found {repr foundWt2}, expected {repr tag2.wireType}"
-               else
                if tag2.fieldNum != 2 then
                     throw s!"Expected Field Number 2 within map, not {tag2.fieldNum}"
                else
-               let value : ValueT ← Field.parse
+
+               let value : ValueT ← Field.guardedParse tag2
                pure #[(Prod.mk key value)]
           | 2 =>
-               let foundWt1 := Field.expectedWireType ValueT
-               if foundWt1 ≠ tag1.wireType then
-                    throw s!"WireType mismatch: found {repr foundWt1}, expected {repr tag1.wireType}"
-               else
-               let value : ValueT ← Field.parse
+               let value : ValueT ← Field.guardedParse tag1
 
                -- Since the fields are optional, check to see if we're done parsing now
                let curPos ← BParsec.pos
@@ -82,14 +71,11 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar
                else
 
                let tag2 ← Tag.parse
-               let foundWt2 := Field.expectedWireType KeyT
-               if foundWt2 ≠ tag2.wireType then
-                    throw s!"WireType mismatch: found {repr foundWt2}, expected {repr tag2.wireType}"
-               else
                if tag2.fieldNum != 1 then
                     throw s!"Expected Field Number 1 within map, not {tag2.fieldNum}"
                else
-               let key : KeyT ← Field.parse
+
+               let key : KeyT ← Field.guardedParse tag2
                pure #[(Prod.mk key value)]
 
           | _ => throw "Unexpected Field Number within Map Element"