2.3. Parser
Duration.parse returns some d when the input string is valid, and none otherwise. It first splits off an optional leading '-' with isNegativeDuration, then hands the remaining body to parseDuration? (shown here directly from its source in Cedar.Spec.Ext.Datetime):
public def Duration.parse (str : String) : Option Duration :=
let (isNegative, restStr) := isNegativeDuration str
parseDuration? isNegative restStr
parseDuration? consumes each unit suffix in largest-to-smallest order (d, h, m, s, ms are peeled from the right), accumulates the signed millisecond total, and requires that the body be fully consumed. Because the units are matched in a fixed order, out-of-order strings like 1h30m1d are rejected:
def parseDuration? (isNegative : Bool) (str : String) : Option Duration := do
if str.isEmpty then failure
let (milliseconds, restStr) ← parseUnit? isNegative str "ms"
let (seconds, restStr) ← parseUnit? isNegative restStr "s"
let (minutes, restStr) ← parseUnit? isNegative restStr "m"
let (hours, restStr) ← parseUnit? isNegative restStr "h"
let (days, restStr) ← parseUnit? isNegative restStr "d"
if restStr.isEmpty
then duration? (days + hours + minutes + seconds + milliseconds)
else noneFor example:
#eval (Duration.parse "1d2h30m").map Duration.toString -- valid
#eval (Duration.parse "-1h30m").map Duration.toString -- negative
#eval Duration.parse "1h30m1d" -- out of order
#eval Duration.parse "" -- empty