Skip to content

Commit 99a9c77

Browse files
adpaco-awsadpaco-aws
authored
Lean: Add parsing for duration in the datetime extension (#471)
Signed-off-by: Adrian Palacios <[email protected]>
1 parent 473b5d0 commit 99a9c77

File tree

3 files changed

+220
-0
lines changed

3 files changed

+220
-0
lines changed

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

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
/-
2+
Copyright Cedar Contributors
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import Cedar.Data.Int64
18+
19+
/-! This file defines Cedar datetime values and functions. -/
20+
21+
namespace Cedar.Spec.Ext
22+
23+
open Cedar.Data
24+
25+
/--
26+
A duration value is measured in milliseconds and constructed from a duration string.
27+
A duration string is a concatenated sequence of quantity-unit pairs where the quantity
28+
is a natural number and unit is one of the following:
29+
- `d` (for days)
30+
- `h` (for hours)
31+
- `m` (for minutes)
32+
- `s` (for seconds)
33+
- `ms` (for milliseconds)
34+
35+
Duration strings are required to be ordered from largest unit to smallest
36+
unit, and contain one quantity per unit. Units with zero quantity may be
37+
omitted.
38+
39+
A duration may be negative. Negative duration strings must begin with `-`.
40+
-/
41+
abbrev Duration := Int64
42+
43+
namespace Datetime
44+
45+
def MILLISECONDS_PER_SECOND: Int := 1000
46+
def MILLISECONDS_PER_MINUTE: Int := 60000
47+
def MILLISECONDS_PER_HOUR: Int := 360000
48+
def MILLISECONDS_PER_DAY: Int := 86400000
49+
50+
----- Definitions -----
51+
52+
def duration? (i : Int) : Option Duration :=
53+
Int64.mk? i
54+
55+
def durationUnits? (n: Nat) (suffix: String) : Option Duration :=
56+
match Int64.mk? n with
57+
| none => none
58+
| some i =>
59+
match suffix with
60+
| "ms" => duration? i
61+
| "s" => duration? (i * MILLISECONDS_PER_SECOND)
62+
| "m" => duration? (i * MILLISECONDS_PER_MINUTE)
63+
| "h" => duration? (i * MILLISECONDS_PER_HOUR)
64+
| "d" => duration? (i * MILLISECONDS_PER_DAY)
65+
| _ => none
66+
67+
def unitsToMilliseconds (days hours minutes second milliseconds: Int) : Int :=
68+
days * MILLISECONDS_PER_DAY +
69+
hours * MILLISECONDS_PER_HOUR +
70+
minutes * MILLISECONDS_PER_MINUTE +
71+
second * MILLISECONDS_PER_SECOND +
72+
milliseconds
73+
74+
def isNegativeDuration (str: String) : Bool × String :=
75+
match str.front with
76+
| '-' => (true, str.drop 1)
77+
| _ => (false, str)
78+
79+
def parseUnit? (str : String) (suffix : String) : Option (Duration × String) :=
80+
if str.endsWith suffix
81+
then
82+
let newStr := str.dropRight suffix.length
83+
let newStrList := newStr.toList
84+
let digits := ((newStrList.reverse).takeWhile Char.isDigit).reverse
85+
if digits.isEmpty
86+
then none
87+
else do
88+
let units ← durationUnits? (← String.toNat? (String.mk digits)) suffix
89+
some (units, newStr.dropRight digits.length)
90+
else
91+
some (⟨0, (by decide)⟩, str)
92+
93+
def parseUnsignedDuration? (str : String) : Option Duration := do
94+
if str.isEmpty then failure
95+
let (milliseconds, restStr) ← parseUnit? str "ms"
96+
let (seconds, restStr) ← parseUnit? restStr "s"
97+
let (minutes, restStr) ← parseUnit? restStr "m"
98+
let (hours, restStr) ← parseUnit? restStr "h"
99+
let (days, restStr) ← parseUnit? restStr "d"
100+
if restStr.isEmpty
101+
then duration? (days + hours + minutes + seconds + milliseconds)
102+
else none
103+
104+
def Duration.parse (str : String) : Option Duration :=
105+
let (isNegative, restStr) := isNegativeDuration str
106+
match parseUnsignedDuration? restStr with
107+
| some duration =>
108+
if isNegative
109+
then Int64.neg? duration
110+
else some duration
111+
| none => none
112+
113+
deriving instance Repr for Duration
114+
115+
abbrev duration := Duration.parse
116+
117+
end Datetime

‎cedar-lean/UnitTest/Datetime.lean‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
/-
2+
Copyright Cedar Contributors
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import Cedar.Spec.Ext.Datetime
18+
import UnitTest.Run
19+
20+
/-! This file defines unit tests for Datetime functions. -/
21+
22+
namespace UnitTest.Datetime
23+
24+
open Cedar.Spec.Ext.Datetime
25+
26+
theorem test1 : toString ((Duration.parse "1ms").get!) = "1" := by native_decide
27+
theorem test2 : toString ((Duration.parse "1s").get!) = "1000" := by native_decide
28+
theorem test3 : toString ((Duration.parse "1m").get!) = "60000" := by native_decide
29+
theorem test4 : toString ((Duration.parse "1h").get!) = "360000" := by native_decide
30+
theorem test5 : toString ((Duration.parse "1d").get!) = "86400000" := by native_decide
31+
theorem test6 : toString ((Duration.parse "1d2h3m4s5ms").get!) = "87304005" := by native_decide
32+
theorem test7 : toString ((Duration.parse "2d12h").get!) = "177120000" := by native_decide
33+
theorem test8 : toString ((Duration.parse "3m30s").get!) = "210000" := by native_decide
34+
theorem test9 : toString ((Duration.parse "1h30m45s").get!) = "2205000" := by native_decide
35+
theorem test10 : toString ((Duration.parse "2d5h20m").get!) = "175800000" := by native_decide
36+
theorem test11 : toString ((Duration.parse "-1d12h").get!) = "-90720000" := by native_decide
37+
theorem test12 : toString ((Duration.parse "-3h45m").get!) = "-3780000" := by native_decide
38+
theorem test13 : toString ((Duration.parse "1d1ms").get!) = "86400001" := by native_decide
39+
theorem test14 : toString ((Duration.parse "59m59s999ms").get!) = "3599999" := by native_decide
40+
theorem test15 : toString ((Duration.parse "23h59m59s999ms").get!) = "11879999" := by native_decide
41+
theorem test16 : toString ((Duration.parse "0d0h0m0s0ms").get!) = "0" := by native_decide
42+
43+
private def testValid (str : String) (rep : Int) : TestCase IO :=
44+
test str ⟨λ _ => checkEq (Duration.parse str) (duration? rep)⟩
45+
46+
def testsForValidDurationStrings :=
47+
suite "Duration.parse for valid strings"
48+
[
49+
testValid "0ms" 0,
50+
testValid "0d0s" 0,
51+
testValid "1ms" 1,
52+
testValid "1s" 1000,
53+
testValid "1m" 60000,
54+
testValid "1h" 360000,
55+
testValid "1d" 86400000,
56+
testValid "12s340ms" 12340,
57+
testValid "1s234ms" 1234,
58+
testValid "-1s" (-1000),
59+
testValid "-4s200ms" (-4200),
60+
testValid "-9s876ms" (-9876),
61+
testValid "106751d23h47m16s854ms" 9223297516854,
62+
testValid "-106751d23h47m16s854ms" (-9223297516854),
63+
testValid "1d2h3m4s5ms" 87304005,
64+
testValid "2d12h" 177120000,
65+
testValid "3m30s" 210000,
66+
testValid "1h30m45s" 2205000,
67+
testValid "2d5h20m" 175800000,
68+
testValid "-1d12h" (-90720000),
69+
testValid "-3h45m" (-3780000),
70+
testValid "1d1ms" 86400001,
71+
testValid "59m59s999ms" 3599999,
72+
testValid "23h59m59s999ms" 11879999
73+
]
74+
75+
private def testInvalid (str : String) (msg : String) : TestCase IO :=
76+
test s!"{str} [{msg}]" ⟨λ _ => checkEq (Duration.parse str) .none⟩
77+
78+
def testsForInvalidDurationStrings :=
79+
suite "Duration.parse for invalid strings"
80+
[
81+
testInvalid "" "empty string",
82+
testInvalid "d" "unit but no amount",
83+
testInvalid "1d-1s" "invalid use of -",
84+
testInvalid "1d2h3m4s5ms6" "trailing amount",
85+
testInvalid "1x2m3s" "invalid unit",
86+
testInvalid "1.23s" "amounts must be integral",
87+
testInvalid "1s1d" "invalid order",
88+
testInvalid "1s1s" "repeated units",
89+
testInvalid "1d2h3m4s5ms " "trailing space",
90+
testInvalid " 1d2h3m4s5ms" "leading space",
91+
testInvalid "1d9223372036854775807ms" "overflow",
92+
testInvalid "1d92233720368547758071ms" "overflow ms",
93+
testInvalid "9223372036854776s1ms" "overflow s"
94+
]
95+
96+
def tests := [testsForValidDurationStrings, testsForInvalidDurationStrings]
97+
98+
-- Uncomment for interactive debugging
99+
-- #eval TestSuite.runAll tests
100+
101+
end UnitTest.Datetime

‎cedar-lean/UnitTest/Main.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
limitations under the License.
1515
-/
1616

17+
import UnitTest.Datetime
1718
import UnitTest.Decimal
1819
import UnitTest.IPAddr
1920
import UnitTest.Proto
@@ -22,6 +23,7 @@ import UnitTest.Wildcard
2223
open UnitTest
2324

2425
def tests :=
26+
Datetime.tests ++
2527
Decimal.tests ++
2628
IPAddr.tests ++
2729
Wildcard.tests ++

0 commit comments

Comments
 (0)