Lean: Add parsing for duration in the datetime extension

cedar-lean/Cedar/Spec/Ext/Datetime.lean

@@ -0,0 +1,119 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Data.Int64
+
+/-! This file defines Cedar datetime values and functions. -/
+
+namespace Cedar.Spec.Ext
+
+open Cedar.Data
+
+/--
+  A duration value is measured in milliseconds and constructed from a duration string.
+  A duration string is a concatenated sequence of quantity-unit pairs where the quantity
+  is a positive integer and unit is one of the following:
+    - `d` (for days)
+    - `h` (for hours)
+    - `m` (for minutes)
+    - `s` (for seconds)
+    - `ms` (for milliseconds)
+
+  Duration strings are required to be ordered from largest unit to smallest
+  unit, and contain one quantity per unit. Units with zero quantity may be
+  omitted.
+
+  A duration may be negative. Negative duration strings must begin with `-`.
+-/
+abbrev Duration := Int64
+
+namespace Datetime
+
+def MILLISECONDS_PER_SECOND: Int := 1000
+def MILLISECONDS_PER_MINUTE: Int := 60000
+def MILLISECONDS_PER_HOUR: Int := 360000
+def MILLISECONDS_PER_DAY: Int := 86400000
+
+----- Definitions -----
+
+def duration? (i : Int) : Option Duration :=
+  Int64.mk? i
+
+def durationUnits? (i: Int) (suffix: String) : Option Duration :=
+  match suffix with
+  | "ms" => duration? i
+  | "s" => duration? (i * MILLISECONDS_PER_SECOND)
+  | "m" => duration? (i * MILLISECONDS_PER_MINUTE)
+  | "h" => duration? (i * MILLISECONDS_PER_HOUR)
+  | "d" => duration? (i * MILLISECONDS_PER_DAY)
+  | _ => none
+
+def unitsToMilliseconds (days hours minutes second milliseconds: Int) : Int :=
+  days * MILLISECONDS_PER_DAY +
+  hours * MILLISECONDS_PER_HOUR +
+  minutes * MILLISECONDS_PER_MINUTE +
+  second * MILLISECONDS_PER_SECOND +
+  milliseconds
+
+def isNegativeDuration (str: String) : Bool × String :=
+  match str.front with
+  | '-' => (true, str.drop 1)
+  | _   => (false, str)
+
+def addOptionDurations (a b : Option Duration) : Option Duration :=
+  match a, b with
+  | some durationA, some durationB => some (Int64.add? durationA durationB).get!
+  | some duration, none => some duration
+  | none, some duration => some duration
+  | none, none => none
+
+def parseUnit? (str : String) (suffix: String) : Option Duration × String :=
+  if str.endsWith suffix
+  then
+    let new_str := str.dropRight suffix.length
+    let new_str_list := new_str.toList
+    let digits := ((new_str_list.reverse).takeWhile Char.isDigit).reverse
+    if digits.isEmpty
+    then (none, str)
+    else (durationUnits? (String.mk digits).toInt! suffix, new_str.dropRight digits.length)
+  else (none, str)
+
+def parseUnsignedDuration? (str : String) : Option Duration :=
+  let (milliseconds, rest) := parseUnit? str "ms"
+  let (seconds, rest) := parseUnit? rest "s"
+  let (minutes, rest) := parseUnit? rest "m"
+  let (hours, rest) := parseUnit? rest "h"
+  let (days, rest) := parseUnit? rest "d"
+  if rest.isEmpty
+  then
+    [days, hours, minutes, seconds, milliseconds].foldl (addOptionDurations · ·) none
+  else none
+
+def parse (str : String) : Option Duration :=
+  let (isNegative, rest) := isNegativeDuration str
+  match parseUnsignedDuration? rest with
+  | some duration =>
+    if isNegative then
+      Int64.neg? duration
+    else
+      some duration
+  | none => none
+
+deriving instance Repr for Duration
+
+abbrev duration := parse
+
+end Datetime

cedar-lean/UnitTest/Datetime.lean

@@ -0,0 +1,98 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Spec.Ext.Datetime
+import UnitTest.Run
+
+/-! This file defines unit tests for Datetime functions. -/
+
+namespace UnitTest.Datetime
+
+open Cedar.Spec.Ext.Datetime
+
+theorem test1 : toString ((parse "1ms").get!) = "1" := by native_decide
+theorem test2 : toString ((parse "1s").get!) = "1000" := by native_decide
+theorem test3 : toString ((parse "1m").get!) = "60000" := by native_decide
+theorem test4 : toString ((parse "1h").get!) = "360000" := by native_decide
+theorem test5 : toString ((parse "1d").get!) = "86400000" := by native_decide
+theorem test6 : toString ((parse "1d2h3m4s5ms").get!) = "87304005" := by native_decide
+theorem test7 : toString ((parse "2d12h").get!) = "177120000" := by native_decide
+theorem test8 : toString ((parse "3m30s").get!) = "210000" := by native_decide
+theorem test9 : toString ((parse "1h30m45s").get!) = "2205000" := by native_decide
+theorem test10 : toString ((parse "2d5h20m").get!) = "175800000" := by native_decide
+theorem test11 : toString ((parse "-1d12h").get!) = "-90720000" := by native_decide
+theorem test12 : toString ((parse "-3h45m").get!) = "-3780000" := by native_decide
+theorem test13 : toString ((parse "1d1ms").get!) = "86400001" := by native_decide
+theorem test14 : toString ((parse "59m59s999ms").get!) = "3599999" := by native_decide
+theorem test15 : toString ((parse "23h59m59s999ms").get!) = "11879999" := by native_decide
+theorem test16 : toString ((parse "0d0h0m0s0ms").get!) = "0" := by native_decide
+
+private def testValid (str : String) (rep : Int) : TestCase IO :=
+  test str ⟨λ _ => checkEq (parse str) (duration? rep)⟩
+
+def testsForValidDurationStrings :=
+  suite "Duration.parse for valid strings"
+  [
+    testValid "0ms" 0,
+    testValid "0d0s" 0,
+    testValid "1ms" 1,
+    testValid "1s" 1000,
+    testValid "1m" 60000,
+    testValid "1h" 360000,
+    testValid "1d" 86400000,
+    testValid "12s340ms" 12340,
+    testValid "1s234ms" 1234,
+    testValid "-1s" (-1000),
+    testValid "-4s200ms" (-4200),
+    testValid "-9s876ms" (-9876),
+    testValid "106751d23h47m16s854ms" 9223297516854,
+    testValid "-106751d23h47m16s854ms" (-9223297516854),
+    testValid "1d2h3m4s5ms" 87304005,
+    testValid "2d12h" 177120000,
+    testValid "3m30s" 210000,
+    testValid "1h30m45s" 2205000,
+    testValid "2d5h20m" 175800000,
+    testValid "-1d12h" (-90720000),
+    testValid "-3h45m" (-3780000),
+    testValid "1d1ms" 86400001,
+    testValid "59m59s999ms" 3599999,
+    testValid "23h59m59s999ms" 11879999
+  ]
+
+private def testInvalid (str : String) (msg : String) : TestCase IO :=
+  test s!"{str} [{msg}]" ⟨λ _ => checkEq (parse str) .none⟩
+
+def testsForInvalidDurationStrings :=
+  suite "Duration.parse for invalid strings"
+  [
+    testInvalid "" "empty string",
+    testInvalid "d" "unit but no amount",
+    testInvalid "1d-1s" "invalid use of -",
+    testInvalid "1d2h3m4s5ms6" "trailing amount",
+    testInvalid "1x2m3s" "invalid unit",
+    testInvalid "1.23s" "amounts must be integral",
+    testInvalid "1s1d" "invalid order",
+    testInvalid "1s1s" "repeated units",
+    testInvalid "1d2h3m4s5ms " "trailing space",
+    testInvalid " 1d2h3m4s5ms" "leading space"
+  ]
+
+def tests := [testsForValidDurationStrings, testsForInvalidDurationStrings]
+
+-- Uncomment for interactive debugging
+-- #eval TestSuite.runAll tests
+
+end UnitTest.Datetime

cedar-lean/UnitTest/Main.lean

@@ -14,13 +14,15 @@
  limitations under the License.
 -/
 
+import UnitTest.Datetime
 import UnitTest.Decimal
 import UnitTest.IPAddr
 import UnitTest.Wildcard
 
 open UnitTest
 
 def tests :=
+  Datetime.tests ++
   Decimal.tests ++
   IPAddr.tests ++
   Wildcard.tests