Source/Packages

Data.UTF8

packages/foundation/standard/src/Data/UTF8.alpha

1,298 lines193 declarations53.6 KiBSHA-256 4bef3dfd330d

def · lines 1217–1251

decodeUTF8WithTelemetry

Full file
1217def decodeUTF8WithTelemetry =
1218  (lambda unrestricted input : Bytes .
1219    (eliminate
1220      UTF8DecodeResult
1221      (lambda unrestricted current : (family UTF8DecodeResult) . (family UTF8DecodeExecutionResult))
1222      (decodeUTF8 input)
1223      (branch
1224        UTF8DecodeSucceeded
1225        codepoints
1226        .
1227        (constructor
1228          UTF8DecodeExecutionResult
1229          UTF8DecodeExecutionSucceeded
1230          codepoints
1231          (utf8DecodeTelemetryFor input (bytes-length input) codepoints zero zero)))
1232      (branch
1233        UTF8DecodeFailed
1234        code
1235        offset
1236        .
1237        (app
1238          (lambda unrestricted exactOffset : Nat .
1239            (constructor
1240              UTF8DecodeExecutionResult
1241              UTF8DecodeExecutionFailed
1242              code
1243              offset
1244              (utf8ErrorStableCode code)
1245              (utf8DecodeTelemetryFor
1246                input
1247                exactOffset
1248                (constructor UTF8Codepoints UTF8CodepointsEnd)
1249                (succ zero)
1250                exactOffset)))
1251          (modelWord32ToNatural offset)))))

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.