module Observe.Metric

import Data.JSON
import Observe.Declaration
import Observe.Interchange
import Observe.Value
import Std.Natural

-- Numeric storage alone does not establish an objective. Schema binding,
-- value type, meaning, coordinate/state scope and origin must all be admitted.
def aosMetricAdmission =
  (lambda unrestricted schema : Nat .
    (lambda unrestricted numeric : Nat .
      (lambda unrestricted meaning : Nat .
        (lambda unrestricted scope : Nat .
          (lambda unrestricted origin : Nat .
            (naturalAnd
              (naturalEqual schema 1)
              (naturalAnd
                (naturalEqual numeric 1)
                (naturalAnd
                  (naturalEqual meaning 1)
                  (naturalAnd (naturalEqual scope 1) (naturalEqual origin 1))))))))))

def aosMetricReductionAdmission =
  (lambda unrestricted meaning : Nat .
    (lambda unrestricted sums : Nat .
      (lambda unrestricted counts : Nat .
        (lambda unrestricted identities : Nat .
          (lambda unrestricted state : Nat .
            (naturalAnd
              (naturalEqual meaning 1)
              (naturalAnd
                (naturalEqual sums 1)
                (naturalAnd
                  (naturalEqual counts 1)
                  (naturalAnd (naturalEqual identities 1) (naturalEqual state 1))))))))))

-- Missing source schemas are pending rather than guessed from another run.
-- Existing invalid/unsupported/truncated input has precedence over pending.
def aosMetricAgreement =
  (lambda unrestricted variants : Nat .
    (lambda unrestricted invalid : Nat .
      (lambda unrestricted unsupported : Nat .
        (lambda unrestricted truncated : Nat .
          (lambda unrestricted pending : Nat .
            (let unrestricted agreement =
              (aosDeclarationAgreement variants invalid unsupported truncated)
              in
              (aosChoose
                Nat
                (naturalAnd (naturalNonzero pending) (naturalLessOrEqual agreement 2))
                6
                agreement)))))))

def aosCountedMeanNumerator =
  (lambda unrestricted firstSum : Nat .
    (lambda unrestricted secondSum : Nat . (naturalAdd firstSum secondSum)))

def aosCountedMeanDenominator =
  (lambda unrestricted firstCount : Nat .
    (lambda unrestricted secondCount : Nat . (naturalAdd firstCount secondCount)))

-- This models exact nonnegative counted sums, not floating-point rounding.
-- Cross multiplication compares a hand-stated rational without division;
-- each contributor and the asserted denominator must have positive count.
def aosCountedMeanAgreement =
  (lambda unrestricted firstSum : Nat .
    (lambda unrestricted firstCount : Nat .
      (lambda unrestricted secondSum : Nat .
        (lambda unrestricted secondCount : Nat .
          (lambda unrestricted numerator : Nat .
            (lambda unrestricted denominator : Nat .
              (naturalAnd
                (naturalNonzero firstCount)
                (naturalAnd
                  (naturalNonzero secondCount)
                  (naturalAnd
                    (naturalNonzero denominator)
                    (naturalEqual
                      (naturalMultiply (aosCountedMeanNumerator firstSum secondSum) denominator)
                      (naturalMultiply numerator (aosCountedMeanDenominator firstCount secondCount))))))))))))

-- Disjoint bucket counts merge by addition; worker percentiles cannot supply
-- these sufficient statistics. The recorded total must equal the bucket sum.
def aosHistogramMergeCount =
  (lambda unrestricted first : Nat . (lambda unrestricted second : Nat . (naturalAdd first second)))

def aosHistogramCountAgreement =
  (lambda unrestricted total : Nat .
    (lambda unrestricted buckets : Nat . (naturalEqual total buckets)))

-- A sampled row is explicitly diagnostic. Its exact value and source
-- coordinate do not establish a full objective or an identified model state.
-- Callers retain the sampling index and stage in the schema-bound payload.
def aosSampledRowMetric =
  (lambda unrestricted identity : Bytes .
    (lambda unrestricted schema : Bytes .
      (lambda unrestricted name : Bytes .
        (lambda unrestricted unit : Bytes .
          (lambda unrestricted equation : Bytes .
            (lambda unrestricted phase : Bytes .
              (aosDescriptorRecord
                b"metric"
                identity
                (constructor
                  JSON
                  JSONObject
                  (aosField
                    b"format"
                    (aosJSONText b"AOS-METRIC/1")
                    (aosField
                      b"schema_id"
                      (aosJSONText schema)
                      (aosField
                        b"field"
                        (aosJSONText b"row_loss")
                        (aosField
                          b"name"
                          (aosJSONText name)
                          (aosField
                            b"value_type"
                            (aosJSONText b"f32")
                            (aosField
                              b"unit"
                              (aosJSONText unit)
                              (aosField
                                b"equation"
                                (aosJSONText equation)
                                (aosField
                                  b"role"
                                  (aosJSONText b"diagnostic")
                                  (aosField
                                    b"population"
                                    (constructor
                                      JSON
                                      JSONObject
                                      (aosField
                                        b"kind"
                                        (aosJSONText b"sample")
                                        (aosField
                                        b"reference"
                                        (constructor
                                        JSON
                                        JSONObject
                                        (aosField
                                        b"state"
                                        (aosJSONText b"not_recorded")
                                        (aosField
                                        b"reason"
                                        (constructor
                                        JSON
                                        JSONObject
                                        (aosField
                                        b"code"
                                        (aosJSONText b"native-sample-has-no-population-identity")
                                        aosObjectEnd))
                                        aosObjectEnd)))
                                        aosObjectEnd)))
                                    (aosField
                                      b"reduction"
                                      (constructor
                                        JSON
                                        JSONObject
                                        (aosField
                                        b"kind"
                                        (aosJSONText b"none")
                                        (aosField
                                        b"sum_field"
                                        (constructor JSON JSONNull)
                                        (aosField
                                        b"count_field"
                                        (constructor JSON JSONNull)
                                        (aosField
                                        b"population_count_field"
                                        (constructor JSON JSONNull)
                                        aosObjectEnd)))))
                                      (aosField
                                        b"state_phase"
                                        (aosJSONText phase)
                                        (aosField
                                        b"state_field"
                                        (constructor JSON JSONNull)
                                        (aosField
                                        b"contribution_field"
                                        (constructor JSON JSONNull)
                                        (aosField
                                        b"source_precision"
                                        (aosJSONText b"binary32 original bits")
                                        (aosField
                                        b"coordinates"
                                        (constructor
                                        JSON
                                        JSONArray
                                        (constructor
                                        JSON
                                        JSONArrayNext
                                        (constructor
                                        JSON
                                        JSONObject
                                        (aosField
                                        b"field"
                                        (aosJSONText b"completed_submissions")
                                        (aosField
                                        b"meaning"
                                        (aosJSONText b"custom")
                                        (aosField
                                        b"scope"
                                        (aosJSONText b"producer-epoch")
                                        aosObjectEnd))))
                                        (constructor JSON JSONArrayEnd)))
                                        (aosField
                                        b"origin"
                                        (constructor
                                        JSON
                                        JSONObject
                                        (aosField
                                        b"kind"
                                        (aosJSONText b"derived")
                                        (aosField
                                        b"method"
                                        (aosJSONText
                                        b"source-declared interpretation of one native binary32 row; not a population aggregate")
                                        aosObjectEnd)))
                                        aosObjectEnd))))))))))))))))))))))))