Add types and methods from datetime extension to parsers

Signed-off-by: Adrian Palacios <accorell@amazon.com>
cedar-policy · Mar 4, 2025 · 0b03d0b · 0b03d0b
1 parent 434f09f
commit 0b03d0b
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 0 deletions.
diff --git a/cedar-lean/CedarProto/Expr.lean b/cedar-lean/CedarProto/Expr.lean
@@ -491,6 +491,12 @@ def mergeName (result : ExprKind.ExtensionFunctionApp) (xfn : Spec.Name) : BPars
     | "isLoopback" => pure $ .call .isLoopback es
     | "isMulticast" => pure $ .call .isMulticast es
     | "isInRange" => pure $ .call .isInRange es
+    | "datetime" => pure $ .call .datetime es
+    | "duration" => pure $ .call .duration es
+    | "offset" => pure $ .call .offset es
+    | "durationSince" => pure $ .call .durationSince es
+    | "toDate" => pure $ .call .toDate es
+    | "toTime" => pure $ .call .toTime es
     | xfn => throw s!"mergeName: unknown extension function {xfn}"
   | _ => panic!("Expected ExprKind.ExtensionFunctionApp to have constructor .call")
 

diff --git a/cedar-lean/CedarProto/Type.lean b/cedar-lean/CedarProto/Type.lean
@@ -162,6 +162,8 @@ partial def toCedarType : ProtoType → Except String CedarType
   | .ext n => match n.id with -- ignoring n.path because currently no extension types have nonempty namespaces
     | "ipaddr" => .ok (.ext .ipAddr)
     | "decimal" => .ok (.ext .decimal)
+    | "datetime" => .ok (.ext .datetime)
+    | "duration" => .ok (.ext .duration)
     | _ => .error s!"unknown extension type name: {n.toName}"
 
 end ProtoType

diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean
@@ -133,6 +133,12 @@ def jsonToExtFun (json : Lean.Json) : ParseResult ExtFun := do
   | "isLoopback" => .ok .isLoopback
   | "isMulticast" => .ok .isMulticast
   | "isInRange" => .ok .isInRange
+  | "datetime" => .ok .datetime
+  | "duration" => .ok .duration
+  | "offset" => .ok .offset
+  | "durationSince" => .ok .durationSince
+  | "toDate" => .ok .toDate
+  | "toTime" => .ok .toTime
   | xfn => .error s!"jsonToExtFun: unknown extension function {xfn}"
 
 /- mapM functions for lists of key-value pairs -/
@@ -410,6 +416,8 @@ def jsonToExtType (json : Lean.Json) : ParseResult ExtType := do
   match xty.id with
   | "ipaddr" => .ok .ipAddr
   | "decimal" => .ok .decimal
+  | "datetime" => .ok .datetime
+  | "duration" => .ok .duration
   | xty => .error s!"jsonToExtType: unknown extension type {xty}"
 
 /-