1module Observe.Metric
2
3import Data.JSON
4import Observe.Declaration
5import Observe.Interchange
6import Observe.Value
7import Std.Natural
8
9-- Numeric storage alone does not establish an objective. Schema binding,
10-- value type, meaning, coordinate/state scope and origin must all be admitted.
11def aosMetricAdmission =
12 (lambda unrestricted schema : Nat .
13 (lambda unrestricted numeric : Nat .
14 (lambda unrestricted meaning : Nat .
15 (lambda unrestricted scope : Nat .
16 (lambda unrestricted origin : Nat .
17 (naturalAnd
18 (naturalEqual schema 1)
19 (naturalAnd
20 (naturalEqual numeric 1)
21 (naturalAnd
22 (naturalEqual meaning 1)
23 (naturalAnd (naturalEqual scope 1) (naturalEqual origin 1))))))))))
24
25def aosMetricReductionAdmission =
26 (lambda unrestricted meaning : Nat .
27 (lambda unrestricted sums : Nat .
28 (lambda unrestricted counts : Nat .
29 (lambda unrestricted identities : Nat .
30 (lambda unrestricted state : Nat .
31 (naturalAnd
32 (naturalEqual meaning 1)
33 (naturalAnd
34 (naturalEqual sums 1)
35 (naturalAnd
36 (naturalEqual counts 1)
37 (naturalAnd (naturalEqual identities 1) (naturalEqual state 1))))))))))
38
39-- Missing source schemas are pending rather than guessed from another run.
40-- Existing invalid/unsupported/truncated input has precedence over pending.
41def aosMetricAgreement =
42 (lambda unrestricted variants : Nat .
43 (lambda unrestricted invalid : Nat .
44 (lambda unrestricted unsupported : Nat .
45 (lambda unrestricted truncated : Nat .
46 (lambda unrestricted pending : Nat .
47 (let unrestricted agreement =
48 (aosDeclarationAgreement variants invalid unsupported truncated)
49 in
50 (aosChoose
51 Nat
52 (naturalAnd (naturalNonzero pending) (naturalLessOrEqual agreement 2))
53 6
54 agreement)))))))
55
56def aosCountedMeanNumerator =
57 (lambda unrestricted firstSum : Nat .
58 (lambda unrestricted secondSum : Nat . (naturalAdd firstSum secondSum)))
59
60def aosCountedMeanDenominator =
61 (lambda unrestricted firstCount : Nat .
62 (lambda unrestricted secondCount : Nat . (naturalAdd firstCount secondCount)))
63
64-- This models exact nonnegative counted sums, not floating-point rounding.
65-- Cross multiplication compares a hand-stated rational without division;
66-- each contributor and the asserted denominator must have positive count.
67def aosCountedMeanAgreement =
68 (lambda unrestricted firstSum : Nat .
69 (lambda unrestricted firstCount : Nat .
70 (lambda unrestricted secondSum : Nat .
71 (lambda unrestricted secondCount : Nat .
72 (lambda unrestricted numerator : Nat .
73 (lambda unrestricted denominator : Nat .
74 (naturalAnd
75 (naturalNonzero firstCount)
76 (naturalAnd
77 (naturalNonzero secondCount)
78 (naturalAnd
79 (naturalNonzero denominator)
80 (naturalEqual
81 (naturalMultiply (aosCountedMeanNumerator firstSum secondSum) denominator)
82 (naturalMultiply numerator (aosCountedMeanDenominator firstCount secondCount))))))))))))
83
84-- Disjoint bucket counts merge by addition; worker percentiles cannot supply
85-- these sufficient statistics. The recorded total must equal the bucket sum.
86def aosHistogramMergeCount =
87 (lambda unrestricted first : Nat . (lambda unrestricted second : Nat . (naturalAdd first second)))
88
89def aosHistogramCountAgreement =
90 (lambda unrestricted total : Nat .
91 (lambda unrestricted buckets : Nat . (naturalEqual total buckets)))
92
93-- A sampled row is explicitly diagnostic. Its exact value and source
94-- coordinate do not establish a full objective or an identified model state.
95-- Callers retain the sampling index and stage in the schema-bound payload.
96def aosSampledRowMetric =
97 (lambda unrestricted identity : Bytes .
98 (lambda unrestricted schema : Bytes .
99 (lambda unrestricted name : Bytes .
100 (lambda unrestricted unit : Bytes .
101 (lambda unrestricted equation : Bytes .
102 (lambda unrestricted phase : Bytes .
103 (aosDescriptorRecord
104 b"metric"
105 identity
106 (constructor
107 JSON
108 JSONObject
109 (aosField
110 b"format"
111 (aosJSONText b"AOS-METRIC/1")
112 (aosField
113 b"schema_id"
114 (aosJSONText schema)
115 (aosField
116 b"field"
117 (aosJSONText b"row_loss")
118 (aosField
119 b"name"
120 (aosJSONText name)
121 (aosField
122 b"value_type"
123 (aosJSONText b"f32")
124 (aosField
125 b"unit"
126 (aosJSONText unit)
127 (aosField
128 b"equation"
129 (aosJSONText equation)
130 (aosField
131 b"role"
132 (aosJSONText b"diagnostic")
133 (aosField
134 b"population"
135 (constructor
136 JSON
137 JSONObject
138 (aosField
139 b"kind"
140 (aosJSONText b"sample")
141 (aosField
142 b"reference"
143 (constructor
144 JSON
145 JSONObject
146 (aosField
147 b"state"
148 (aosJSONText b"not_recorded")
149 (aosField
150 b"reason"
151 (constructor
152 JSON
153 JSONObject
154 (aosField
155 b"code"
156 (aosJSONText b"native-sample-has-no-population-identity")
157 aosObjectEnd))
158 aosObjectEnd)))
159 aosObjectEnd)))
160 (aosField
161 b"reduction"
162 (constructor
163 JSON
164 JSONObject
165 (aosField
166 b"kind"
167 (aosJSONText b"none")
168 (aosField
169 b"sum_field"
170 (constructor JSON JSONNull)
171 (aosField
172 b"count_field"
173 (constructor JSON JSONNull)
174 (aosField
175 b"population_count_field"
176 (constructor JSON JSONNull)
177 aosObjectEnd)))))
178 (aosField
179 b"state_phase"
180 (aosJSONText phase)
181 (aosField
182 b"state_field"
183 (constructor JSON JSONNull)
184 (aosField
185 b"contribution_field"
186 (constructor JSON JSONNull)
187 (aosField
188 b"source_precision"
189 (aosJSONText b"binary32 original bits")
190 (aosField
191 b"coordinates"
192 (constructor
193 JSON
194 JSONArray
195 (constructor
196 JSON
197 JSONArrayNext
198 (constructor
199 JSON
200 JSONObject
201 (aosField
202 b"field"
203 (aosJSONText b"completed_submissions")
204 (aosField
205 b"meaning"
206 (aosJSONText b"custom")
207 (aosField
208 b"scope"
209 (aosJSONText b"producer-epoch")
210 aosObjectEnd))))
211 (constructor JSON JSONArrayEnd)))
212 (aosField
213 b"origin"
214 (constructor
215 JSON
216 JSONObject
217 (aosField
218 b"kind"
219 (aosJSONText b"derived")
220 (aosField
221 b"method"
222 (aosJSONText
223 b"source-declared interpretation of one native binary32 row; not a population aggregate")
224 aosObjectEnd)))
225 aosObjectEnd))))))))))))))))))))))))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.