leanexe/LeanExe/Examples/JsonDouble.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
import LeanExe.Ascii.Json

namespace LeanExe
namespace Examples.JsonDouble

def inputFieldName : ByteArray :=
  "n".toUTF8

def resultFieldName : ByteArray :=
  "result".toUTF8

def parseInput (text : AsciiString) : Option UInt64 :=
  Ascii.Json.getUInt64Field text inputFieldName

def resultJson (n : UInt64) : ByteArray :=
  Ascii.Json.object1UInt64 resultFieldName n

def doubleFits (n : UInt64) : Bool :=
  !(n > (9223372036854775807 : UInt64))

def transformAscii (text : AsciiString) : ByteArray :=
  match parseInput text with
  | some n =>
      if doubleFits n then
        resultJson (n * 2)
      else
        Ascii.Json.errorJson
  | none => Ascii.Json.errorJson

def transform (input : ByteArray) : ByteArray :=
  match AsciiString.ofByteArray? input with
  | some text => transformAscii text
  | none => Ascii.Json.errorJson

end Examples.JsonDouble
end LeanExe