1module Std.Numeric.Profile
2
3import Std.Natural
4import Data.Bytes
5import Model.Word64
6
7-- Numeric profiles as Alpha VALUES, one owner (Language & Testing Evolution
8-- L13b; PRD 17 H2/H3, HW-005; PRD 08 N6). A profile declares what a float
9-- realization may assume: storage and accumulation formats, rounding,
10-- contraction, reduction order, subnormal handling, exceptional values and a
11-- per-operation approximation table. The two initial profiles are values in
12-- this module; docs/language/numeric-profiles/<name>.md is the prose each value
13-- is rendered against (debug/std-numeric-profile-check.py renders the values
14-- into docs/generated/ALPHA-NUMERIC-PROFILES.md from this module, never by hand).
15-- Nothing here is measured: a bound that has not been measured says so by
16-- name (StdApproximationUnmeasured), an operation a profile does not realize
17-- says so by name (StdApproximationUnsupported) -- a profile may narrow, it may
18-- never claim more than its lowering delivers.
19-- the identity a receipt carries for the profile
20family StdNumericProfileIdentity : Type 0
21constructor StdProfileIdentityX86SseScalarStrict
22constructor StdProfileIdentitySm86CooperativeM0
23constructor StdProfileIdentityNamed
24field unrestricted stdProfileIdentityName : Bytes
25
26end-family
27
28family StdNumericFormat : Type 0
29constructor StdFormatBinary32
30constructor StdFormatBinary64
31
32end-family
33
34-- only round-to-nearest-even is admitted; the family has one constructor so
35-- that a profile cannot declare another rounding by mistake
36family StdRounding : Type 0
37constructor StdRoundNearestEven
38
39end-family
40
41family StdContraction : Type 0
42constructor StdContractionForbidden
43constructor StdContractionPermittedWhereEmitted
44
45end-family
46
47family StdReductionOrder : Type 0
48constructor StdReductionStrictLeftFold
49constructor StdReductionDeclaredTree
50
51end-family
52
53-- SM86 flush-to-zero is a MEASURED fact (a pod probe, L26), never assumed
54family StdSubnormalHandling : Type 0
55constructor StdSubnormalsPreserved
56constructor StdSubnormalsFlushedToZero
57constructor StdSubnormalsUnmeasured
58
59end-family
60
61-- IEEE exceptional values: NaN propagates quieted, invalid operations give the
62-- target's default NaN, signed infinities and zeros; exceptions masked and never
63-- read back (the profile document spells the rules out)
64family StdExceptionalValues : Type 0
65constructor StdExceptionalIEEE
66-- Every arithmetic input/output is finite, or execution refuses by name.
67constructor StdExceptionalFiniteOrRefuse
68
69end-family
70
71family StdNumericOperation : Type 0
72constructor StdOpAdd
73constructor StdOpSubtract
74constructor StdOpMultiply
75constructor StdOpDivide
76constructor StdOpSquareRoot
77constructor StdOpReciprocal
78constructor StdOpReciprocalSquareRoot
79constructor StdOpExp2
80constructor StdOpTanh
81
82end-family
83
84-- a per-operation bound: exact = correctly rounded (at most half an ulp);
85-- a measured maximum ulp error; unmeasured (no bound may be relied on);
86-- unsupported (the profile does not realize the operation)
87family StdApproximation : Type 0
88constructor StdApproximationExact
89constructor StdApproximationMaxUlp
90field unrestricted stdApproximationUlp : Nat
91constructor StdApproximationUnmeasured
92constructor StdApproximationUnsupported
93
94end-family
95
96family StdApproximationEntry : Type 0
97constructor StdApproximationEntryOf
98field unrestricted stdApproximationEntryOperation : (family StdNumericOperation)
99field unrestricted stdApproximationEntryBound : (family StdApproximation)
100
101end-family
102
103family StdApproximationTable : Type 0
104constructor StdApproximationTableEmpty
105constructor StdApproximationTableCons
106field unrestricted stdApproximationTableHead : (family StdApproximationEntry)
107recursive unrestricted stdApproximationTableRest
108
109end-family
110
111family StdNumericProfile : Type 0
112constructor StdNumericProfileOf
113field unrestricted stdNumericProfileIdentity : (family StdNumericProfileIdentity)
114field unrestricted stdNumericProfileStorage : (family StdNumericFormat)
115field unrestricted stdNumericProfileAccumulation : (family StdNumericFormat)
116field unrestricted stdNumericProfileRounding : (family StdRounding)
117field unrestricted stdNumericProfileContraction : (family StdContraction)
118field unrestricted stdNumericProfileReductionOrder : (family StdReductionOrder)
119field unrestricted stdNumericProfileSubnormals : (family StdSubnormalHandling)
120field unrestricted stdNumericProfileExceptional : (family StdExceptionalValues)
121field unrestricted stdNumericProfileApproximations : (family StdApproximationTable)
122
123end-family
124
125-- H3: how a float case compares its observed value with the expected one; the
126-- runner refuses a float case that declares none. abs and rel are binary32 bit
127-- patterns (a Nat below 2^32), ulp a count.
128family StdNanPolicy : Type 0
129constructor StdNanNeverEqual
130constructor StdNanEqualByBits
131
132end-family
133
134family StdZeroPolicy : Type 0
135constructor StdZerosEqual
136constructor StdZerosDistinct
137
138end-family
139
140-- an aggregation that could hide a failure (a mean) is not a constructor
141family StdErrorAggregation : Type 0
142constructor StdAggregateEveryCase
143constructor StdAggregateMaximum
144
145end-family
146
147family StdTolerance : Type 0
148constructor StdToleranceOf
149field unrestricted stdToleranceAbsoluteBits : Nat
150field unrestricted stdToleranceRelativeBits : Nat
151field unrestricted stdToleranceUlp : Nat
152field unrestricted stdToleranceNanPolicy : (family StdNanPolicy)
153field unrestricted stdToleranceZeroPolicy : (family StdZeroPolicy)
154field unrestricted stdToleranceAggregation : (family StdErrorAggregation)
155
156end-family
157
158family StdNumericComparison : Type 0
159constructor StdCompareExactBits
160constructor StdCompareExactValue
161constructor StdCompareTolerance
162field unrestricted stdCompareTolerance : (family StdTolerance)
163
164end-family
165
166-- PRD 17 HW-004 / REG-019: whether a profile ADMITS a requested variant. A
167-- rejection names the capability that is missing (the device, the precision or
168-- the operation) with its diagnostic code; `alpha check` and `alpha build`
169-- refuse a root whose `admission` is rejected before anything is emitted.
170family StdNumericAdmission : Type 0
171constructor StdAdmissionAdmitted
172constructor StdAdmissionRejected
173field unrestricted stdAdmissionRejectedCode : Bytes
174field unrestricted stdAdmissionRejectedReason : Bytes
175
176end-family
177
178-- Conversion is an operation in the numerical program. These constructors
179-- fix both endpoints; an absent conversion cannot authorize a format change.
180-- Widening preserves finite binary32 values exactly. Narrowing is an explicit
181-- nearest-even rounding site, including overflow and subnormal outcomes; it is
182-- never inferred from a transport or admitted as an exact widening.
183family StdNumericConversion : Type 0
184constructor StdNumericKeepFormat
185field unrestricted stdNumericKeptFormat : (family StdNumericFormat)
186constructor StdNumericWidenBinary32
187constructor StdNumericRoundBinary64
188
189end-family
190
191-- operations as small codes, so two operations can be compared
192def stdOperationCode =
193 (lambda unrestricted operation : (family StdNumericOperation) .
194 (eliminate
195 StdNumericOperation
196 (lambda unrestricted current : (family StdNumericOperation) . Nat)
197 operation
198 (branch StdOpAdd . (byte-to-nat (byte 1)))
199 (branch StdOpSubtract . (byte-to-nat (byte 2)))
200 (branch StdOpMultiply . (byte-to-nat (byte 3)))
201 (branch StdOpDivide . (byte-to-nat (byte 4)))
202 (branch StdOpSquareRoot . (byte-to-nat (byte 5)))
203 (branch StdOpReciprocal . (byte-to-nat (byte 6)))
204 (branch StdOpReciprocalSquareRoot . (byte-to-nat (byte 7)))
205 (branch StdOpExp2 . (byte-to-nat (byte 8)))
206 (branch StdOpTanh . (byte-to-nat (byte 9)))))
207
208def stdOperationEqual =
209 (lambda unrestricted a : (family StdNumericOperation) .
210 (lambda unrestricted b : (family StdNumericOperation) .
211 (naturalEqual (stdOperationCode a) (stdOperationCode b))))
212
213def stdSelectApproximation =
214 (lambda unrestricted flag : Nat .
215 (lambda unrestricted whenTrue : (family StdApproximation) .
216 (lambda unrestricted whenFalse : (family StdApproximation) .
217 (nat-eliminate
218 (lambda unrestricted current : Nat . (family StdApproximation))
219 whenFalse
220 (lambda unrestricted predecessor : Nat .
221 (lambda unrestricted induction : (family StdApproximation) . whenTrue))
222 flag))))
223
224-- the bound a table declares for an operation; an operation the table does not
225-- name is Unsupported (never silently exact)
226def stdApproximationOf =
227 (lambda unrestricted operation : (family StdNumericOperation) .
228 (lambda unrestricted table : (family StdApproximationTable) .
229 (eliminate
230 StdApproximationTable
231 (lambda unrestricted current : (family StdApproximationTable) . (family StdApproximation))
232 table
233 (branch
234 StdApproximationTableEmpty
235 .
236 (constructor StdApproximation StdApproximationUnsupported))
237 (branch
238 StdApproximationTableCons
239 entry
240 rest
241 restBound
242 .
243 (eliminate
244 StdApproximationEntry
245 (lambda unrestricted current : (family StdApproximationEntry) .
246 (family StdApproximation))
247 entry
248 (branch
249 StdApproximationEntryOf
250 entryOperation
251 entryBound
252 .
253 (stdSelectApproximation
254 (stdOperationEqual entryOperation operation)
255 entryBound
256 restBound)))))))
257
258def stdApproximationIsExact =
259 (lambda unrestricted bound : (family StdApproximation) .
260 (eliminate
261 StdApproximation
262 (lambda unrestricted current : (family StdApproximation) . Nat)
263 bound
264 (branch StdApproximationExact . (succ zero))
265 (branch StdApproximationMaxUlp ulp . zero)
266 (branch StdApproximationUnmeasured . zero)
267 (branch StdApproximationUnsupported . zero)))
268
269-- projections
270def stdNumericProfileTable =
271 (lambda unrestricted profile : (family StdNumericProfile) .
272 (eliminate
273 StdNumericProfile
274 (lambda unrestricted current : (family StdNumericProfile) . (family StdApproximationTable))
275 profile
276 (branch
277 StdNumericProfileOf
278 identity
279 storage
280 accumulation
281 rounding
282 contraction
283 order
284 subnormals
285 exceptional
286 table
287 .
288 table)))
289
290def stdNumericProfileContractionOf =
291 (lambda unrestricted profile : (family StdNumericProfile) .
292 (eliminate
293 StdNumericProfile
294 (lambda unrestricted current : (family StdNumericProfile) . (family StdContraction))
295 profile
296 (branch
297 StdNumericProfileOf
298 identity
299 storage
300 accumulation
301 rounding
302 contraction
303 order
304 subnormals
305 exceptional
306 table
307 .
308 contraction)))
309
310def stdNumericProfileSubnormalsOf =
311 (lambda unrestricted profile : (family StdNumericProfile) .
312 (eliminate
313 StdNumericProfile
314 (lambda unrestricted current : (family StdNumericProfile) . (family StdSubnormalHandling))
315 profile
316 (branch
317 StdNumericProfileOf
318 identity
319 storage
320 accumulation
321 rounding
322 contraction
323 order
324 subnormals
325 exceptional
326 table
327 .
328 subnormals)))
329
330def stdNumericProfileReductionOrderOf =
331 (lambda unrestricted profile : (family StdNumericProfile) .
332 (eliminate
333 StdNumericProfile
334 (lambda unrestricted current : (family StdNumericProfile) . (family StdReductionOrder))
335 profile
336 (branch
337 StdNumericProfileOf
338 identity
339 storage
340 accumulation
341 rounding
342 contraction
343 order
344 subnormals
345 exceptional
346 table
347 .
348 order)))
349
350def stdNumericProfileIdentityOf =
351 (lambda unrestricted profile : (family StdNumericProfile) .
352 (eliminate
353 StdNumericProfile
354 (lambda unrestricted current : (family StdNumericProfile) .
355 (family StdNumericProfileIdentity))
356 profile
357 (branch
358 StdNumericProfileOf
359 identity
360 storage
361 accumulation
362 rounding
363 contraction
364 order
365 subnormals
366 exceptional
367 table
368 .
369 identity)))
370
371-- is the operation exact (correctly rounded) under the profile?
372def stdProfileExact =
373 (lambda unrestricted profile : (family StdNumericProfile) .
374 (lambda unrestricted operation : (family StdNumericOperation) .
375 (stdApproximationIsExact (stdApproximationOf operation (stdNumericProfileTable profile)))))
376
377-- the common subset of two profiles (PRD 19: the cross-target gate of System A):
378-- an operation both realize exactly
379def stdProfilesBothExact =
380 (lambda unrestricted a : (family StdNumericProfile) .
381 (lambda unrestricted b : (family StdNumericProfile) .
382 (lambda unrestricted operation : (family StdNumericOperation) .
383 (nat-eliminate
384 (lambda unrestricted current : Nat . Nat)
385 zero
386 (lambda unrestricted predecessor : Nat .
387 (lambda unrestricted induction : Nat . (stdProfileExact b operation)))
388 (stdProfileExact a operation)))))
389
390def stdNumericFormatCode =
391 (lambda unrestricted format : (family StdNumericFormat) .
392 (eliminate
393 StdNumericFormat
394 (lambda unrestricted current : (family StdNumericFormat) . Nat)
395 format
396 (branch StdFormatBinary32 . (succ zero))
397 (branch StdFormatBinary64 . (succ (succ zero)))))
398
399-- This is a constructor tag, not identity equality for named profiles.
400def stdNumericProfileIdentityCode =
401 (lambda unrestricted identity : (family StdNumericProfileIdentity) .
402 (eliminate
403 StdNumericProfileIdentity
404 (lambda unrestricted current : (family StdNumericProfileIdentity) . Nat)
405 identity
406 (branch StdProfileIdentityX86SseScalarStrict . (succ zero))
407 (branch StdProfileIdentitySm86CooperativeM0 . (succ (succ zero)))
408 (branch StdProfileIdentityNamed name . 3)))
409
410def stdNumericProfileStorageOf =
411 (lambda unrestricted profile : (family StdNumericProfile) .
412 (eliminate
413 StdNumericProfile
414 (lambda unrestricted current : (family StdNumericProfile) . (family StdNumericFormat))
415 profile
416 (branch
417 StdNumericProfileOf
418 identity
419 storage
420 accumulation
421 rounding
422 contraction
423 order
424 subnormals
425 exceptional
426 table
427 .
428 storage)))
429
430def stdApproximationIsUnsupported =
431 (lambda unrestricted bound : (family StdApproximation) .
432 (eliminate
433 StdApproximation
434 (lambda unrestricted current : (family StdApproximation) . Nat)
435 bound
436 (branch StdApproximationExact . zero)
437 (branch StdApproximationMaxUlp ulp . zero)
438 (branch StdApproximationUnmeasured . zero)
439 (branch StdApproximationUnsupported . (succ zero))))
440
441def stdAdmissionWhen =
442 (lambda unrestricted flag : Nat .
443 (lambda unrestricted whenTrue : (family StdNumericAdmission) .
444 (lambda unrestricted whenFalse : (family StdNumericAdmission) .
445 (nat-eliminate
446 (lambda unrestricted current : Nat . (family StdNumericAdmission))
447 whenFalse
448 (lambda unrestricted predecessor : Nat .
449 (lambda unrestricted induction : (family StdNumericAdmission) . whenTrue))
450 flag))))
451
452def stdAdmitted : (family StdNumericAdmission) =
453 (constructor StdNumericAdmission StdAdmissionAdmitted)
454
455-- does the profile admit an operation at a precision? The precision must be the
456-- profile's storage format, and the operation must not be Unsupported in its
457-- table (an Unmeasured bound is admitted: it is realized, only not yet measured)
458def stdProfileAdmits =
459 (lambda unrestricted profile : (family StdNumericProfile) .
460 (lambda unrestricted format : (family StdNumericFormat) .
461 (lambda unrestricted operation : (family StdNumericOperation) .
462 (stdAdmissionWhen
463 (naturalEqual
464 (stdNumericFormatCode format)
465 (stdNumericFormatCode (stdNumericProfileStorageOf profile)))
466 (stdAdmissionWhen
467 (stdApproximationIsUnsupported
468 (stdApproximationOf operation (stdNumericProfileTable profile)))
469 (constructor
470 StdNumericAdmission
471 StdAdmissionRejected
472 b"ALPHA-ADMISSION-UNSUPPORTED-OPERATION"
473 b"the profile declares the requested operation unsupported")
474 stdAdmitted)
475 (constructor
476 StdNumericAdmission
477 StdAdmissionRejected
478 b"ALPHA-ADMISSION-UNSUPPORTED-PRECISION"
479 b"the requested precision is not the profile's storage format")))))
480
481-- A semantic profile name is extensible; a device package supplies a name and
482-- its actual behavior record. Distinct names never compare equal merely because
483-- both use the extension constructor. Version changes must change the name.
484def stdNumericWord =
485 (lambda unrestricted value : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated value)))
486
487def stdNumericSizedBytes =
488 (lambda unrestricted value : Bytes . (bytes-append (stdNumericWord (bytes-length value)) value))
489
490def stdNumericProfileIdentityBytes =
491 (lambda unrestricted identity : (family StdNumericProfileIdentity) .
492 (eliminate
493 StdNumericProfileIdentity
494 (lambda unrestricted current : (family StdNumericProfileIdentity) . Bytes)
495 identity
496 (branch StdProfileIdentityX86SseScalarStrict . b"\x01")
497 (branch StdProfileIdentitySm86CooperativeM0 . b"\x02")
498 (branch StdProfileIdentityNamed name . (bytes-append b"\x03" (stdNumericSizedBytes name)))))
499
500-- the same on a device: a profile of another device is rejected first
501def stdProfileAdmitsOn =
502 (lambda unrestricted device : (family StdNumericProfileIdentity) .
503 (lambda unrestricted profile : (family StdNumericProfile) .
504 (lambda unrestricted format : (family StdNumericFormat) .
505 (lambda unrestricted operation : (family StdNumericOperation) .
506 (stdAdmissionWhen
507 (bytes-equal
508 (stdNumericProfileIdentityBytes device)
509 (stdNumericProfileIdentityBytes (stdNumericProfileIdentityOf profile)))
510 (stdProfileAdmits profile format operation)
511 (constructor
512 StdNumericAdmission
513 StdAdmissionRejected
514 b"ALPHA-ADMISSION-UNSUPPORTED-DEVICE"
515 b"the profile belongs to another device than the one requested"))))))
516
517def stdEntry =
518 (lambda unrestricted operation : (family StdNumericOperation) .
519 (lambda unrestricted bound : (family StdApproximation) .
520 (constructor StdApproximationEntry StdApproximationEntryOf operation bound)))
521
522def stdTableCons =
523 (lambda unrestricted entry : (family StdApproximationEntry) .
524 (lambda unrestricted rest : (family StdApproximationTable) .
525 (constructor StdApproximationTable StdApproximationTableCons entry rest)))
526
527def stdExact : (family StdApproximation) =
528 (constructor StdApproximation StdApproximationExact)
529
530def stdUnmeasured : (family StdApproximation) =
531 (constructor StdApproximation StdApproximationUnmeasured)
532
533def stdUnsupported : (family StdApproximation) =
534 (constructor StdApproximation StdApproximationUnsupported)
535
536def stdOpAdd : (family StdNumericOperation) =
537 (constructor StdNumericOperation StdOpAdd)
538
539def stdOpSubtract : (family StdNumericOperation) =
540 (constructor StdNumericOperation StdOpSubtract)
541
542def stdOpMultiply : (family StdNumericOperation) =
543 (constructor StdNumericOperation StdOpMultiply)
544
545def stdOpDivide : (family StdNumericOperation) =
546 (constructor StdNumericOperation StdOpDivide)
547
548def stdOpSquareRoot : (family StdNumericOperation) =
549 (constructor StdNumericOperation StdOpSquareRoot)
550
551def stdOpReciprocal : (family StdNumericOperation) =
552 (constructor StdNumericOperation StdOpReciprocal)
553
554def stdOpReciprocalSquareRoot : (family StdNumericOperation) =
555 (constructor StdNumericOperation StdOpReciprocalSquareRoot)
556
557def stdOpExp2 : (family StdNumericOperation) =
558 (constructor StdNumericOperation StdOpExp2)
559
560def stdOpTanh : (family StdNumericOperation) =
561 (constructor StdNumericOperation StdOpTanh)
562
563def stdTableEmpty : (family StdApproximationTable) =
564 (constructor StdApproximationTable StdApproximationTableEmpty)
565
566-- x86-64-sse-scalar-strict (PRD 08 N6): SSE scalar single precision, round to
567-- nearest even, no contraction, strict left-fold order, subnormals preserved
568-- (MXCSR FTZ/DAZ clear, asserted at entry), IEEE exceptional values with the
569-- x86 default NaN. add/subtract/multiply/divide are exact (correctly rounded
570-- by the hardware); the correctly-rounded square root is the declared
571-- extension AdamW needs and is NOT realized at HEAD (Unsupported until its
572-- lowering lands -- the value may narrow, never overstate); the MUFU-style
573-- operations have no x86 realization.
574def stdProfileX86SseScalarStrict : (family StdNumericProfile) =
575 (constructor
576 StdNumericProfile
577 StdNumericProfileOf
578 (constructor StdNumericProfileIdentity StdProfileIdentityX86SseScalarStrict)
579 (constructor StdNumericFormat StdFormatBinary32)
580 (constructor StdNumericFormat StdFormatBinary32)
581 (constructor StdRounding StdRoundNearestEven)
582 (constructor StdContraction StdContractionForbidden)
583 (constructor StdReductionOrder StdReductionStrictLeftFold)
584 (constructor StdSubnormalHandling StdSubnormalsPreserved)
585 (constructor StdExceptionalValues StdExceptionalIEEE)
586 (stdTableCons
587 (stdEntry stdOpAdd stdExact)
588 (stdTableCons
589 (stdEntry stdOpSubtract stdExact)
590 (stdTableCons
591 (stdEntry stdOpMultiply stdExact)
592 (stdTableCons
593 (stdEntry stdOpDivide stdExact)
594 (stdTableCons
595 (stdEntry stdOpSquareRoot stdUnsupported)
596 (stdTableCons
597 (stdEntry stdOpReciprocal stdUnsupported)
598 (stdTableCons
599 (stdEntry stdOpReciprocalSquareRoot stdUnsupported)
600 (stdTableCons
601 (stdEntry stdOpExp2 stdUnsupported)
602 (stdTableCons (stdEntry stdOpTanh stdUnsupported) stdTableEmpty))))))))))
603
604-- sm86-cooperative-m0: the profile the D-ladder actually ran. FFMA contraction
605-- is permitted where the lowering emits it; the reduction order is the
606-- D-ladder's declared tree; flush-to-zero and every MUFU bound are MEASURED
607-- facts (PRD 17 H2) and are Unmeasured until the L26 pod probe records them.
608-- add/subtract/multiply as emitted (FADD/FMUL, or the fused FFMA's own
609-- rounding) are exact; division on SM86 goes through a reciprocal
610-- approximation and is Unmeasured, not assumed exact.
611def stdProfileSm86CooperativeM0 : (family StdNumericProfile) =
612 (constructor
613 StdNumericProfile
614 StdNumericProfileOf
615 (constructor StdNumericProfileIdentity StdProfileIdentitySm86CooperativeM0)
616 (constructor StdNumericFormat StdFormatBinary32)
617 (constructor StdNumericFormat StdFormatBinary32)
618 (constructor StdRounding StdRoundNearestEven)
619 (constructor StdContraction StdContractionPermittedWhereEmitted)
620 (constructor StdReductionOrder StdReductionDeclaredTree)
621 (constructor StdSubnormalHandling StdSubnormalsUnmeasured)
622 (constructor StdExceptionalValues StdExceptionalIEEE)
623 (stdTableCons
624 (stdEntry stdOpAdd stdExact)
625 (stdTableCons
626 (stdEntry stdOpSubtract stdExact)
627 (stdTableCons
628 (stdEntry stdOpMultiply stdExact)
629 (stdTableCons
630 (stdEntry stdOpDivide stdUnmeasured)
631 (stdTableCons
632 (stdEntry stdOpSquareRoot stdUnmeasured)
633 (stdTableCons
634 (stdEntry stdOpReciprocal stdUnmeasured)
635 (stdTableCons
636 (stdEntry stdOpReciprocalSquareRoot stdUnmeasured)
637 (stdTableCons
638 (stdEntry stdOpExp2 stdUnmeasured)
639 (stdTableCons (stdEntry stdOpTanh stdUnmeasured) stdTableEmpty))))))))))
640
641-- the comparison every bit-exact float case declares (KAT rows, the model)
642def stdCompareExactBits : (family StdNumericComparison) =
643 (constructor StdNumericComparison StdCompareExactBits)
644
645def stdCompareExactValue : (family StdNumericComparison) =
646 (constructor StdNumericComparison StdCompareExactValue)
647
648def stdNumericProfileAccumulationOf =
649 (lambda unrestricted profile : (family StdNumericProfile) .
650 (eliminate
651 StdNumericProfile
652 (lambda unrestricted current : (family StdNumericProfile) . (family StdNumericFormat))
653 profile
654 (branch
655 StdNumericProfileOf
656 identity
657 storage
658 accumulation
659 rounding
660 contraction
661 order
662 subnormals
663 exceptional
664 table
665 .
666 accumulation)))
667
668def stdNumericProfileRoundingOf =
669 (lambda unrestricted profile : (family StdNumericProfile) .
670 (eliminate
671 StdNumericProfile
672 (lambda unrestricted current : (family StdNumericProfile) . (family StdRounding))
673 profile
674 (branch
675 StdNumericProfileOf
676 identity
677 storage
678 accumulation
679 rounding
680 contraction
681 order
682 subnormals
683 exceptional
684 table
685 .
686 rounding)))
687
688def stdNumericProfileExceptionalOf =
689 (lambda unrestricted profile : (family StdNumericProfile) .
690 (eliminate
691 StdNumericProfile
692 (lambda unrestricted current : (family StdNumericProfile) . (family StdExceptionalValues))
693 profile
694 (branch
695 StdNumericProfileOf
696 identity
697 storage
698 accumulation
699 rounding
700 contraction
701 order
702 subnormals
703 exceptional
704 table
705 .
706 exceptional)))
707
708def stdNumericConversionSource =
709 (lambda unrestricted conversion : (family StdNumericConversion) .
710 (eliminate
711 StdNumericConversion
712 (lambda unrestricted current : (family StdNumericConversion) . (family StdNumericFormat))
713 conversion
714 (branch StdNumericKeepFormat format . format)
715 (branch StdNumericWidenBinary32 . (constructor StdNumericFormat StdFormatBinary32))
716 (branch StdNumericRoundBinary64 . (constructor StdNumericFormat StdFormatBinary64))))
717
718def stdNumericConversionDestination =
719 (lambda unrestricted conversion : (family StdNumericConversion) .
720 (eliminate
721 StdNumericConversion
722 (lambda unrestricted current : (family StdNumericConversion) . (family StdNumericFormat))
723 conversion
724 (branch StdNumericKeepFormat format . format)
725 (branch StdNumericWidenBinary32 . (constructor StdNumericFormat StdFormatBinary64))
726 (branch StdNumericRoundBinary64 . (constructor StdNumericFormat StdFormatBinary32))))
727
728def stdNumericConversionCode =
729 (lambda unrestricted conversion : (family StdNumericConversion) .
730 (eliminate
731 StdNumericConversion
732 (lambda unrestricted current : (family StdNumericConversion) . Nat)
733 conversion
734 (branch StdNumericKeepFormat format . 0)
735 (branch StdNumericWidenBinary32 . 1)
736 (branch StdNumericRoundBinary64 . 2)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.