Complete duration, add tests and docs

Signed-off-by: Adrian Palacios <[email protected]>

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

@@ -23,7 +23,20 @@ namespace Cedar.Spec.Ext
 open Cedar.Data
 
 /--
-  DESCRIBE DATETIME AND DURATION HERE
+  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
 
@@ -34,6 +47,8 @@ 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
 
@@ -46,12 +61,18 @@ def durationUnits? (i: Int) (suffix: String) : Option Duration :=
   | "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!
@@ -81,7 +102,6 @@ def parseUnsignedDuration? (str : String) : Option Duration :=
     [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
@@ -94,12 +114,6 @@ def parse (str : String) : Option Duration :=
 
 deriving instance Repr for Duration
 
-#eval parse "-1d1s"
-#eval Int64.mk? 500
-#eval parseUnit? "12m" "m"
-#eval parseUnit? "12s" "s"
-#eval parseUnit? "12ms" "ms"
-
--- abbrev duration := parse
+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