2.2. Formal Specification🔗

We formalize the validity of an input string by the predicate IsWfDuration (well-formed syntax of the grammar) and the function computeValue (value function). All three numeric grammars phrase well-formedness the same way — the string is the rendering of well-formed components — but where the decimal grammar has a fixed sequence of fields, the duration grammar describes an ordered concatenation of optional components, so the specification is phrased over an explicit record of those components.

The building block is again IsDigits, the shared Digit⁺ predicate introduced in the Decimal Parsing chapter.

Each of the five components is optional. IsWfOptionalQuantity lifts IsDigits to optional strings — an absent component (none) is trivially valid, and a present one must be a non-empty digit string:

public def IsWfOptionalQuantity : Option String → Prop
  | none => True
  | some digits => IsDigits digits

A Components record holds the five optional digit strings, one per time unit:

public structure Components where
  days : Option String
  hours : Option String
  minutes : Option String
  seconds : Option String
  milliseconds : Option String

Two predicates constrain a record. nonempty enforces that at least one component is present — the body cannot be empty:

public def Components.nonempty (components : Components) : Prop :=
  components.days ≠ none ∨
  components.hours ≠ none ∨
  components.minutes ≠ none ∨
  components.seconds ≠ none ∨
  components.milliseconds ≠ none

quantitiesWf enforces that every present component is a valid digit quantity:

public def Components.quantitiesWf
    (components : Components) : Prop :=
  IsWfOptionalQuantity components.days ∧
  IsWfOptionalQuantity components.hours ∧
  IsWfOptionalQuantity components.minutes ∧
  IsWfOptionalQuantity components.seconds ∧
  IsWfOptionalQuantity components.milliseconds

asString renders a record back to a string by concatenating the present components in order d h m s ms, each absent component contributing "". This is what ties the abstract record to the concrete grammar's largest-to-smallest ordering:

public def Components.asString (components : Components) : String :=
  durationChunk components.days "d" ++
  durationChunk components.hours "h" ++
  durationChunk components.minutes "m" ++
  durationChunk components.seconds "s" ++
  durationChunk components.milliseconds "ms"

A body is well-formed exactly when it is the rendering of some record that is both nonempty and has valid quantities. Phrasing well-formedness existentially over asString bakes the ordering constraint in for free: a string is well-formed only if it can be produced by concatenating components in the canonical order, so out-of-order strings have no witnessing record:

public def IsWfBody (body : String) : Prop :=
  ∃ components : Components,
    components.nonempty ∧
    components.quantitiesWf ∧
    body = components.asString

Well-formedness of the whole string then adds the optional leading '-'. That sign is its own production, Sign ::= ['-'], and reuses the shared IsWfSign predicate from the Decimal Parsing chapter. A duration string is well-formed exactly when it is the rendering of such a sign followed by a well-formed body — the same rendering-existential shape used for the body itself, and for the decimal and datetime grammars:

public def IsWfDuration (str : String) : Prop :=
  ∃ sign body,
    str = sign ++ body ∧
    IsWfSign sign ∧
    IsWfBody body

The value function is defined independently of the parser. extractTrailingQuantity peels the natural-number token immediately preceding a given suffix. When the suffix is absent the component is simply not present, so it yields some (0, s); when the suffix is present but its digits are missing or unparseable the string is malformed, so it yields none — the same failure structure as the parser's parseUnit? (shown in the next section):

public def extractTrailingQuantity (s : String) (suffix : String) : Option (Nat × String) :=
  if s.endsWith suffix then
    let rest := (s.dropEnd suffix.length).toString
    let digits := rest.toList.reverse.takeWhile Char.isDigit |>.reverse
    match toNat?' (String.ofList digits) with
    | some n => some (n, (rest.dropEnd digits.length).toString)
    | none => none
  else
    some (0, s)

computeBodyValue extracts each component right-to-left (ms, s, m, h, d) and combines them into an unsigned millisecond total, failing (none) if any present component is unparseable:

public def computeBodyValue (body : String) : Option Int := do
  let (ms, body) ← extractTrailingQuantity body "ms"
  let (sec, body) ← extractTrailingQuantity body "s"
  let (min, body) ← extractTrailingQuantity body "m"
  let (hr, body) ← extractTrailingQuantity body "h"
  let (day, _) ← extractTrailingQuantity body "d"
  some (↑day * MILLISECONDS_PER_DAY +
    ↑hr * MILLISECONDS_PER_HOUR +
    ↑min * MILLISECONDS_PER_MINUTE +
    ↑sec * MILLISECONDS_PER_SECOND +
    ↑ms)

Finally computeValue splits off the sign and applies it to the body's value, propagating none when the body is structurally unparseable:

public def computeValue (str : String) : Option Int :=
  let (isNegative, body) := isNegativeDuration str
  computeSignedBodyValue isNegative body