2.1. The format
A Cedar decimal is a signed fixed-point number with up to four fraction digits:
"1.5", "-12.34", or "922337203685477.5807". Cedar stores the
value times 10^4 in an Int64, so "1.5" denotes 15000.
Three concerns, one per DSL clause:
-
Shape — an optional minus sign, one or more natural digits, a dot, one to four fraction digits. This is the grammar.
-
Meaning — sign times (natural part scaled by 10⁴ plus fraction part scaled to fill four places). This is the value clause.
-
Bounds — the value must fit in
Int64. This is the constraint clause.
The authored block is in cedar-examples/Inputs/Decimal.lean:
triptych Decimal where
grammar
Decimal ::= Sign Natural "." Fraction
Sign ::= sign
Natural ::= digit+
Fraction ::= digit{1,4}
value
Sign * (nat Natural * 10 ^ 4 + nat Fraction * 10 ^ (4 - len Fraction))
ofSpec Int64.ofInt
toSpec Int64.toInt
constraints
value ∈ [Int64.MIN, Int64.MAX]
parser Cedar.Spec.Ext.Decimal.parse
printer decimalToStr
to "Outputs/Decimal"Two details worth pausing on before we look at the output:
Named sign capture. Triptych does not allow sign anonymously inside another production.
It must have its own named rule, such as Sign ::= sign, so the value expression can read it.
The conversion pair. The surface value is an Int. ofSpec Int64.ofInt
converts that value to the generated parser's domain type, while
toSpec Int64.toInt maps a domain value back to the specification. These conversions
belong to the value boundary; the parser clause only names the external parser. The
range constraint makes Int64.ofInt faithful on every accepted value.