Skip to content

Commit

Permalink
Cases for datetime types in extExprToValue (#568)
Browse files Browse the repository at this point in the history
Signed-off-by: Adrian Palacios <accorell@amazon.com>
  • Loading branch information
adpaco-aws authored Mar 5, 2025
1 parent ee3715f commit 582a8cb
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions cedar-lean/CedarProto/Value.lean
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,12 @@ private def extExprToValue (xfn : ExtFun) (args : List Expr) : Except String Val
| .ip, [.lit (.string s)] => match Spec.Ext.IPAddr.ip s with
| .some v => .ok $ .ext (.ipaddr v)
| .none => .error s!"exprToValue: failed to parse ip {s}"
| .datetime, [.lit (.string s)] => match Spec.Ext.Datetime.parse s with
| .some v => .ok $ .ext (.datetime v)
| .none => .error s!"exprToValue: failed to parse datetime {s}"
| .duration, [.lit (.string s)] => match Spec.Ext.Datetime.Duration.parse s with
| .some v => .ok $ .ext (.duration v)
| .none => .error s!"exprToValue: failed to parse duration {s}"
| _, _ => .error s!"exprToValue: unexpected extension value\n{repr (Expr.call xfn args)}"

partial def exprToValue : Expr → Except String Value
Expand Down

0 comments on commit 582a8cb

Please sign in to comment.