leanexe/LeanExe/Examples/JsonTypedDecode.lean at main · jsmorph/leanexe · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
import LeanExe.Ascii.Json.Decode

namespace LeanExe
namespace Examples.JsonTypedDecode

open Ascii.Json

structure Request where
  values : Array UInt64
  multiplier : UInt64
  includeCount : Bool

def valuesFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "values".toUTF8

def multiplierFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "multiplier".toUTF8

def includeCountFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "includeCount".toUTF8

def sumFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "sum".toUTF8

def scaledFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "scaled".toUTF8

def countFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "count".toUTF8

def includedFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "included".toUTF8

def requestFieldNames : Array AsciiString :=
  #[valuesFieldName, multiplierFieldName, includeCountFieldName]

def checkedAdd (left right : UInt64) : Except ByteArray UInt64 :=
  let sum := left + right
  if sum < left then
    Except.error decodeError
  else
    Except.ok sum

def checkedMul (left right : UInt64) : Except ByteArray UInt64 :=
  let product := left * right
  if right == (0 : UInt64) then
    Except.ok product
  else if product / right == left then
    Except.ok product
  else
    Except.error decodeError

def sumValues (values : Array UInt64) : Except ByteArray UInt64 :=
  values.foldl
    (fun state value =>
      match state with
      | Except.error err => Except.error err
      | Except.ok sum => checkedAdd sum value)
    (Except.ok 0)

def decodeRequest (value : Value) : Except ByteArray Request := do
  let fields <- requireObject value
  let _ <- requireOnlyFields fields requestFieldNames
  let rawValues <- requireUniqueField fields valuesFieldName
  let values <- decodeUInt64Array rawValues
  let multiplier <- requireUInt64Field value multiplierFieldName
  let includeCount <- requireBoolField value includeCountFieldName
  pure { values := values, multiplier := multiplier, includeCount := includeCount }

def resultValue (sum scaled : UInt64) (count : Nat) (included : Bool) : Value :=
  Value.obj #[
    Field.mk sumFieldName (Value.num sum),
    Field.mk scaledFieldName (Value.num scaled),
    Field.mk countFieldName (Value.num (if included then UInt64.ofNat count else 0)),
    Field.mk includedFieldName (Value.bool included)
  ]

def runRequest (request : Request) : Except ByteArray ByteArray := do
  let sum <- sumValues request.values
  let scaled <- checkedMul sum request.multiplier
  renderExcept (resultValue sum scaled request.values.size request.includeCount)

def transform (input : ByteArray) : Except ByteArray ByteArray := do
  let value <- parseBytesExcept input
  let request <- decodeRequest value
  runRequest request

end Examples.JsonTypedDecode
end LeanExe