cleanup 'deriving's

cedar-policy · Nov 15, 2023 · 650ed2a · 650ed2a
1 parent 2f32681
commit 650ed2a
Show file tree

Hide file tree

Showing 14 changed files with 36 additions and 86 deletions.
diff --git a/cedar-lean/Cedar/Data/Int64.lean b/cedar-lean/Cedar/Data/Int64.lean
@@ -73,8 +73,7 @@ if h : Int64.lt i₁ i₂ then isTrue h else isFalse h
 instance int64Le (i₁ i₂ : Int64) : Decidable (i₁ ≤ i₂) :=
 if h : Int64.le i₁ i₂ then isTrue h else isFalse h
 
-deriving instance Repr for Int64
-deriving instance DecidableEq for Int64
+deriving instance Repr, DecidableEq for Int64
 
 end Int64
 

diff --git a/cedar-lean/Cedar/Data/Map.lean b/cedar-lean/Cedar/Data/Map.lean
@@ -29,8 +29,7 @@ namespace Cedar.Data
 
 inductive Map (α : Type u) (β : Type v) where
 | mk : List (α × β) -> Map α β
-deriving Repr
-deriving instance DecidableEq, Repr, Inhabited for Map
+deriving Repr, DecidableEq, Repr, Inhabited
 
 namespace Map
 
@@ -111,4 +110,4 @@ theorem in_list_in_map {α : Type u} (k : α) (v : β) (m : Map α β) :
 
 end Map
 
-end Cedar.Data
+end Cedar.Data
diff --git a/cedar-lean/Cedar/Data/Set.lean b/cedar-lean/Cedar/Data/Set.lean
@@ -30,8 +30,7 @@ namespace Cedar.Data
 
 inductive Set (α : Type u) where
 | mk (l : List α)
-deriving Repr
-deriving instance DecidableEq, Repr, Inhabited, Lean.ToJson for Set
+deriving Repr, DecidableEq, Inhabited, Lean.ToJson
 
 namespace Set
 
@@ -106,6 +105,7 @@ def singleton {α} (a : α) : Set α :=
 
 def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α :=
   s.elts.foldl f init
+
 ----- Props and Theorems -----
 
 instance [LT α] : LT (Set α) where
@@ -157,4 +157,4 @@ theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α)
 
 end Set
 
-end Cedar.Data
+end Cedar.Data
diff --git a/cedar-lean/Cedar/Spec/Entities.lean b/cedar-lean/Cedar/Spec/Entities.lean
@@ -53,8 +53,6 @@ def Entities.attrsOrEmpty (es : Entities) (uid : EntityUID) : Map Attr Value :=
 
 ----- Derivations -----
 
-deriving instance Repr for EntityData
-deriving instance DecidableEq for EntityData
-deriving instance Inhabited for EntityData
+deriving instance Repr, DecidableEq, Inhabited for EntityData
 
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Expr.lean b/cedar-lean/Cedar/Spec/Expr.lean
@@ -66,16 +66,11 @@ inductive Expr where
 
 ----- Derivations -----
 
-deriving instance Repr for Var
-deriving instance Repr for UnaryOp
-deriving instance Repr for BinaryOp
-deriving instance Repr for Expr
+deriving instance Repr, DecidableEq for Var
+deriving instance Repr, DecidableEq for UnaryOp
+deriving instance Repr, DecidableEq for BinaryOp
+deriving instance Repr, Inhabited for Expr
 
-deriving instance Inhabited for Expr
-
-deriving instance DecidableEq for Var
-deriving instance DecidableEq for UnaryOp
-deriving instance DecidableEq for BinaryOp
 
 mutual
 

diff --git a/cedar-lean/Cedar/Spec/Ext.lean b/cedar-lean/Cedar/Spec/Ext.lean
@@ -39,8 +39,7 @@ def Ext.lt : Ext → Ext → Bool
 
 ----- Derivations -----
 
-deriving instance Repr for Ext
-deriving instance DecidableEq for Ext
+deriving instance Repr, DecidableEq for Ext
 
 instance : LT Ext where
 lt := fun x y => Ext.lt x y
@@ -54,4 +53,4 @@ instance : Coe Decimal Ext where
 instance : Coe IPAddr Ext where
   coe a := .ipaddr a
 
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Ext/IPAddr.lean b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean
@@ -256,8 +256,7 @@ def IPNet.lt : IPNet → IPNet → Bool
 
 ----- IPNet deriviations -----
 
-deriving instance Repr for IPNet
-deriving instance DecidableEq for IPNet
+deriving instance Repr, DecidableEq, Inhabited for IPNet
 
 instance : LT IPNet where
   lt := fun d₁ d₂ => IPNet.lt d₁ d₂

diff --git a/cedar-lean/Cedar/Spec/ExtFun.lean b/cedar-lean/Cedar/Spec/ExtFun.lean
@@ -64,7 +64,6 @@ def call : ExtFun → List Value → Result Value
 
 ----- Derivations -----
 
-deriving instance Repr for ExtFun
-deriving instance DecidableEq for ExtFun
+deriving instance Repr, DecidableEq for ExtFun
 
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Policy.lean b/cedar-lean/Cedar/Spec/Policy.lean
@@ -116,27 +116,13 @@ def Scope.bound : Scope → Option EntityUID
 
 ----- Derivations -----
 
-deriving instance Repr for Effect
-deriving instance Repr for Scope
-deriving instance Repr for PrincipalScope
-deriving instance Repr for ResourceScope
-deriving instance Repr for ActionScope
-deriving instance Repr for Policy
-
-deriving instance DecidableEq for Effect
-deriving instance DecidableEq for Scope
-deriving instance DecidableEq for PrincipalScope
-deriving instance DecidableEq for ResourceScope
-deriving instance DecidableEq for ActionScope
-deriving instance DecidableEq for Policy
-
-deriving instance Inhabited for Effect
-deriving instance Inhabited for Scope
-deriving instance Inhabited for PrincipalScope
-deriving instance Inhabited for ResourceScope
-deriving instance Inhabited for ActionScope
-deriving instance Inhabited for Policy
+deriving instance Repr, DecidableEq, Inhabited for Effect
+deriving instance Repr, DecidableEq, Inhabited for Scope
+deriving instance Repr, DecidableEq, Inhabited for PrincipalScope
+deriving instance Repr, DecidableEq, Inhabited for ResourceScope
+deriving instance Repr, DecidableEq, Inhabited for ActionScope
+deriving instance Repr, DecidableEq, Inhabited for Policy
 
 deriving instance Lean.ToJson for PolicyID
 
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Request.lean b/cedar-lean/Cedar/Spec/Request.lean
@@ -31,8 +31,6 @@ structure Request where
   resource : EntityUID
   context : Map Attr Value
 
-deriving instance Repr for Request
-deriving instance DecidableEq for Request
-deriving instance Inhabited for Request
+deriving instance Repr, DecidableEq, Inhabited for Request
 
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Response.lean b/cedar-lean/Cedar/Spec/Response.lean
@@ -36,12 +36,7 @@ structure Response where
 
 ----- Derivations -----
 
-deriving instance Repr for Decision, Response
+deriving instance Repr, DecidableEq, Lean.ToJson for Decision
+deriving instance Repr, DecidableEq, Lean.ToJson for Response
 
-deriving instance DecidableEq for Decision
-deriving instance DecidableEq for Response
-
-deriving instance Lean.ToJson for Decision
-deriving instance Lean.ToJson for Response
-
-end Cedar.Spec
+end Cedar.Spec
diff --git a/cedar-lean/Cedar/Spec/Value.lean b/cedar-lean/Cedar/Spec/Value.lean
@@ -129,27 +129,14 @@ instance : Coe Value (Result (Data.Set Value)) where
 
 ----- Derivations -----
 
-deriving instance Repr for Except
-deriving instance Repr for Error
-deriving instance Repr for Name
-deriving instance Repr for EntityType
-deriving instance Repr for EntityUID
-deriving instance Repr for Prim
+deriving instance Repr, DecidableEq, BEq for Except
+deriving instance Repr, DecidableEq for Error
+deriving instance Repr, DecidableEq, Inhabited for Name
+deriving instance Repr, DecidableEq, Inhabited for EntityType
+deriving instance Repr, DecidableEq, Inhabited for EntityUID
+deriving instance Repr, DecidableEq, Inhabited for Prim
 deriving instance Repr for Value
 
-deriving instance DecidableEq for Except
-deriving instance DecidableEq for Error
-deriving instance DecidableEq for Name
-deriving instance DecidableEq for EntityType
-deriving instance DecidableEq for EntityUID
-deriving instance DecidableEq for Prim
-
-deriving instance Inhabited for Name
-deriving instance Inhabited for EntityType
-deriving instance Inhabited for EntityUID
-deriving instance Inhabited for Prim
-
-deriving instance BEq for Except
 
 mutual
 

diff --git a/cedar-lean/Cedar/Spec/Wildcard.lean b/cedar-lean/Cedar/Spec/Wildcard.lean
@@ -19,9 +19,7 @@ namespace Cedar.Spec
 inductive PatElem where
   | star
   | justChar (c : Char)
-deriving Repr
-deriving instance DecidableEq for PatElem
-deriving instance Inhabited for PatElem
+deriving Repr, DecidableEq, Inhabited
 
 abbrev Pattern := List PatElem
 

diff --git a/cedar-lean/UnitTest/IPAddr.lean b/cedar-lean/UnitTest/IPAddr.lean
@@ -72,8 +72,6 @@ def testsForInvalidStrings :=
     testInvalid "F:AE::F:5:F:F:0/01" "no leading zeros"
   ]
 
-deriving instance Inhabited for IPNet
-
 private def parse! (str : String) : IPNet :=
   match parse str with
   | .some ip => ip