Duration grammar: definitions

This file contains only grammar-level definitions: the well-formedness predicates and the value relation. IsWfDuration states the syntax, value gives the denotation of already identified components, and IsDurationValue str v combines the same witnesses to say that str denotes v. The executable extraction machinery used to connect these definitions to Duration.parse lives in Cedar.Thm.Ext.Duration.Lemmas.

def Cedar.Thm.Duration.durationChunk (digits? : Option String) (suffix : String) : String

Render an optional duration component as its string representation. none produces "", some digits produces digits ++ suffix.

Equations

• Cedar.Thm.Duration.durationChunk none suffix = ""
• Cedar.Thm.Duration.durationChunk (some digits) suffix = digits ++ suffix

def Cedar.Thm.Duration.IsWfOptionalQuantity : Option String → Prop

Lift the Digit⁺ quantity-token predicate (IsDigits) to optional components: none is trivially valid.

Equations

• Cedar.Thm.Duration.IsWfOptionalQuantity none = True
• Cedar.Thm.Duration.IsWfOptionalQuantity (some digits) = digits.IsDigits

structure Cedar.Thm.Duration.Components : Type

The five optional digit-string components of a duration body, one per time unit. Each field holds none (unit absent) or some digits (unit present with that value).

• days : Option String
• hours : Option String
• minutes : Option String
• seconds : Option String
• milliseconds : Option String

def Cedar.Thm.Duration.Components.nonempty (components : Components) : Prop

At least one component must be present (the body cannot be empty).

Equations

• components.nonempty = (components.days ≠ none ∨ components.hours ≠ none ∨ components.minutes ≠ none ∨ components.seconds ≠ none ∨ components.milliseconds ≠ none)

def Cedar.Thm.Duration.Components.quantitiesWf (components : Components) : Prop

Every present component must be a valid duration quantity (nonempty, parseable digits).

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.Components.asString (components : Components) : String

Canonical string representation: concatenate present components in order d h m s ms. Absent components contribute "".

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.optionalNatOf : Option String → Nat

Natural-number value of an optional duration quantity. An absent component denotes zero; a present well-formed component is read by the shared grammar-level natOf.

Equations

• Cedar.Thm.Duration.optionalNatOf none = 0
• Cedar.Thm.Duration.optionalNatOf (some digits) = digits.natOf

def Cedar.Thm.Duration.Components.toMillis (components : Components) : Int

Unsigned millisecond value of already identified duration components.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.value (sign : String) (components : Components) : Int

The grammar's value function, applied to an already identified sign and component record.

Equations

• Cedar.Thm.Duration.value sign components = sign.signOf * components.toMillis

def Cedar.Thm.Duration.canonicalComponents (days hours minutes seconds ms : Nat) : Components

Canonical maximized components for a duration value split into days, hours, minutes, seconds, and milliseconds. All five fields are present, including zero-valued fields.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.canonicalBody (days hours minutes seconds ms : Nat) : String

Canonical maximized duration body: days d, hours h, minutes m, seconds s, and milliseconds ms, printed largest-to-smallest.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.IsWfBody (body : String) : Prop

A duration body string is well-formed iff it equals components.asString for some Components that is nonempty and has valid quantities.

Equations

• Cedar.Thm.Duration.IsWfBody body = ∃ (components : Cedar.Thm.Duration.Components), components.nonempty ∧ components.quantitiesWf ∧ body = components.asString

def Cedar.Thm.Duration.DurationProduction (str sign : String) (components : Components) : Prop

The grammar production witnessed by an optional sign and a nonempty component record.

Equations

• Cedar.Thm.Duration.DurationProduction str sign components = (str = sign ++ components.asString ∧ sign.IsWfSign ∧ components.nonempty ∧ components.quantitiesWf)

def Cedar.Thm.Duration.IsWfDuration (str : String) : Prop

A duration string is well-formed iff it has a valid grammar production.

Equations

• Cedar.Thm.Duration.IsWfDuration str = ∃ (sign : String), ∃ (components : Cedar.Thm.Duration.Components), Cedar.Thm.Duration.DurationProduction str sign components

def Cedar.Thm.Duration.IsDurationValue (str : String) (v : Int) : Prop

v is the value assigned to a valid duration production.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.Duration.normalize (str : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed or out-of-range inputs.

Equations

• Cedar.Thm.Duration.normalize str = Option.map Cedar.Spec.Ext.Datetime.Duration.toString (Cedar.Spec.Ext.Datetime.Duration.parse str)