From 9f319210728af7b023b63d7ae7db2c04307ba7fe Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 1 Oct 2024 15:22:49 -0700 Subject: [PATCH] Fix integration testing Signed-off-by: Shaobo He --- cedar-lean/DiffTest/Parser.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index b06fc3206..c14af6402 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -515,10 +515,11 @@ partial def jsonToEntityTypeEntry (json : Lean.Json) : ParseResult JsonEntitySch let descendants_json ← getJsonField json "descendants" >>= jsonToArray let descendants ← List.mapM jsonToName descendants_json.toList let attrs ← getJsonField json "attributes" >>= (getJsonField · "attrs") >>= jsonToRecordType - let tags ← -- the "tags" field may be absent + let tags ← -- the "tags" field must be present match getJsonField json "tags" with + | .ok .null => .ok .none | .ok jty => (jsonToCedarType jty).map .some - | .error _ => .ok .none + | _ => .error "`tags` field must exist" .ok { descendants := Set.make descendants, attrs := attrs,