Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor Protobufs code #561

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Refactor Protobufs code #561

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
cc599b8
Refactor Protobufs code
shaobo-he-aws Mar 2, 2025
368a8d6
minor update
shaobo-he-aws Mar 2, 2025
aedda8d
no lambda
shaobo-he-aws Mar 2, 2025
dc0f458
Update cedar-lean/CedarProto/PolicySet.lean
shaobo-he-aws Mar 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 32 additions & 30 deletions cedar-lean/CedarProto/ActionConstraint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ instance : Inhabited ActionScope.In where
@[inline]
def mergeEuids (result : ActionScope.In) (e2 : Array EntityUID) : ActionScope.In :=
match result with
| .actionInAny e1 => .actionInAny (e1 ++ e2.toList)
| _ => panic!("ActionScope.In expected ActionScope constructor to be set to .actionInAny")
| .actionInAny e1 => .actionInAny (e1 ++ e2.toList)
| _ => panic!("ActionScope.In expected ActionScope constructor to be set to .actionInAny")

@[inline]
def merge (x1 x2 : ActionScope.In) : ActionScope.In :=
Expand All @@ -71,12 +71,12 @@ def merge (x1 x2 : ActionScope.In) : ActionScope.In :=
@[inline]
def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.In) := do
match t.fieldNum with
| 1 =>
let x : Repeated EntityUID ← Field.guardedParse t
pure (pure $ mergeEuids · x)
| _ =>
t.wireType.skip
pure ignore
| 1 =>
let x : Repeated EntityUID ← Field.guardedParse t
pureMergeFn (mergeEuids · x)
| _ =>
t.wireType.skip
pure ignore

instance : Message ActionScope.In := {
parseField := parseField
Expand Down Expand Up @@ -105,7 +105,7 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.Eq) := do
match t.fieldNum with
| 1 =>
let x : EntityUID ← Field.guardedParse t
pure (pure $ mergeEuid · x)
pureMergeFn (mergeEuid · x)
| _ =>
t.wireType.skip
pure ignore
Expand All @@ -121,25 +121,27 @@ namespace ActionScope
@[inline]
def mergeAny (_ : ActionScope) (x : Proto.ActionScope.Any) : ActionScope :=
match x with
| .any => .actionScope (Scope.any)
| .any => .actionScope (Scope.any)

@[inline]
def mergeIn (result : ActionScope) (x : Proto.ActionScope.In) : ActionScope :=
have e2 := match x with
have e2 :=
match x with
| .actionInAny e => e
| _ => panic!("Proto.ActionScope.In expected to have constructor .actionInAny")
| _ => panic!("Proto.ActionScope.In expected to have constructor .actionInAny")
match result with
| .actionInAny e1 => .actionInAny (e1 ++ e2)
| _ => .actionInAny e2
| .actionInAny e1 => .actionInAny (e1 ++ e2)
| _ => .actionInAny e2

@[inline]
def mergeEq (result : ActionScope) (x : Proto.ActionScope.Eq) : ActionScope :=
have e2 := match x with
have e2 :=
match x with
| .actionScope (.eq e) => e
| _ => panic!("Proto.ActionScope.Eq expected to have constructor .actionScope .eq")
| _ => panic!("Proto.ActionScope.Eq expected to have constructor .actionScope .eq")
match result with
| .actionScope (.eq e1) => .actionScope (.eq (Field.merge e1 e2))
| _ => .actionScope (.eq e2)
| .actionScope (.eq e1) => .actionScope (.eq (Field.merge e1 e2))
| _ => .actionScope (.eq e2)

@[inline]
def merge (x1 x2 : ActionScope) : ActionScope :=
Expand All @@ -155,18 +157,18 @@ def merge (x1 x2 : ActionScope) : ActionScope :=
@[inline]
def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope) := do
match t.fieldNum with
| 1 =>
let x : Proto.ActionScope.Any ← Field.guardedParse t
pure (pure $ mergeAny · x)
| 2 =>
let x : Proto.ActionScope.In ← Field.guardedParse t
pure (pure $ mergeIn · x)
| 3 =>
let x : Proto.ActionScope.Eq ← Field.guardedParse t
pure (pure $ mergeEq · x)
| _ =>
t.wireType.skip
pure ignore
| 1 =>
let x : Proto.ActionScope.Any ← Field.guardedParse t
pureMergeFn (mergeAny · x)
| 2 =>
let x : Proto.ActionScope.In ← Field.guardedParse t
pureMergeFn (mergeIn · x)
| 3 =>
let x : Proto.ActionScope.Eq ← Field.guardedParse t
pureMergeFn (mergeEq · x)
| _ =>
t.wireType.skip
pure ignore

instance : Message ActionScope := {
parseField := parseField
Expand Down
42 changes: 22 additions & 20 deletions cedar-lean/CedarProto/EntityReference.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,36 +48,38 @@ def mergeSlot (result : EntityUIDOrSlot) (x : Proto.EntityReferenceSlot) : Entit
-- For enums, if result is already of the same type, then we don't do anything
-- otherwise, we construct a default object of the new type.
match x with
| .slot => match result with
| .slot _ => result
| .entityUID _ => .slot default
| .slot =>
match result with
| .slot _ => result
| .entityUID _ => .slot default

@[inline]
def mergeEuid (result : EntityUIDOrSlot) (x : EntityUID) : EntityUIDOrSlot :=
match result with
| .entityUID e => .entityUID (Field.merge e x)
| .slot _ => .entityUID x
| .entityUID e => .entityUID (Field.merge e x)
| .slot _ => .entityUID x

@[inline]
def merge (x : EntityUIDOrSlot) (y : EntityUIDOrSlot) : EntityUIDOrSlot :=
match y with
| .entityUID e2 => mergeEuid x e2
| .slot s2 => match x with
| .entityUID _ => y
| .slot s1 => .slot (Field.merge s1 s2)
| .entityUID e2 => mergeEuid x e2
| .slot s2 =>
match x with
| .entityUID _ => y
| .slot s1 => .slot (Field.merge s1 s2)

@[inline]
def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUIDOrSlot) := do
match t.fieldNum with
| 1 =>
let x : Proto.EntityReferenceSlot ← Field.guardedParse t
pure (pure $ mergeSlot · x)
| 2 =>
let x : EntityUID ← Field.guardedParse t
pure (pure $ mergeEuid · x)
| _ =>
t.wireType.skip
pure ignore
| 1 =>
let x : Proto.EntityReferenceSlot ← Field.guardedParse t
pureMergeFn (mergeSlot · x)
| 2 =>
let x : EntityUID ← Field.guardedParse t
pureMergeFn (mergeEuid · x)
| _ =>
t.wireType.skip
pure ignore

instance : Message EntityUIDOrSlot := {
parseField := parseField
Expand All @@ -87,8 +89,8 @@ instance : Message EntityUIDOrSlot := {
@[inline]
def withSlot (x : EntityUIDOrSlot) (s : SlotID) : EntityUIDOrSlot :=
match x with
| .entityUID x => .entityUID x
| .slot _ => .slot s
| .entityUID x => .entityUID x
| .slot _ => .slot s

end EntityUIDOrSlot

Expand Down
Loading