leanexe/LeanExe/Examples/JsonMergeTreeCommand.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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
import LeanExe.Examples.JsonTreeCommand
import LeanExe.Runtime

namespace LeanExe
namespace Examples.JsonMergeTreeCommand

open Ascii.Json
open Examples.JsonTreeCommand

def treeFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "tree".toUTF8

def gcFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "gc".toUTF8

def allocsFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "allocs".toUTF8

def releasesBeforeFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "releasesBefore".toUTF8

def freesBeforeFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "freesBefore".toUTF8

def freesAfterFirstFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "freesAfterFirst".toUTF8

def freesAfterSecondFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "freesAfterSecond".toUTF8

def releasesAfterSecondFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "releasesAfterSecond".toUTF8

def firstNodesFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "firstNodes".toUTF8

def secondNodesFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "secondNodes".toUTF8

def releasesFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "releases".toUTF8

def freesFieldName : AsciiString :=
  AsciiString.ofTrustedByteArray "frees".toUTF8

def mergeInto : Tree -> Tree -> Tree
  | Tree.empty, acc => acc
  | Tree.node value left right, acc =>
      let withLeft := mergeInto left acc
      let withValue := insertOwned withLeft value
      mergeInto right withValue

def mergeTrees (first second : Tree) : Tree :=
  let withFirst := mergeInto first Tree.empty
  mergeInto second withFirst

def gcValue
    (allocs releasesBefore freesBefore freesAfterFirst freesAfterSecond
      releasesAfterSecond firstNodes secondNodes : UInt64) :
    Value :=
  Value.obj #[
    Field.mk allocsFieldName (Value.num allocs),
    Field.mk releasesBeforeFieldName (Value.num releasesBefore),
    Field.mk freesBeforeFieldName (Value.num freesBefore),
    Field.mk freesAfterFirstFieldName (Value.num freesAfterFirst),
    Field.mk freesAfterSecondFieldName (Value.num freesAfterSecond),
    Field.mk releasesAfterSecondFieldName (Value.num releasesAfterSecond),
    Field.mk firstNodesFieldName (Value.num firstNodes),
    Field.mk secondNodesFieldName (Value.num secondNodes)
  ]

def mergedTreeValue
    (tree : Tree)
    (allocs releasesBefore freesBefore freesAfterFirst freesAfterSecond
      releasesAfterSecond firstNodes secondNodes : UInt64) :
    Value :=
  Value.obj #[
    Field.mk treeFieldName (treeValue tree),
    Field.mk gcFieldName
      (gcValue allocs releasesBefore freesBefore freesAfterFirst freesAfterSecond
        releasesAfterSecond firstNodes secondNodes)
  ]

def makeMergedTreeValue : Value -> Except ByteArray ByteArray
  | Value.arr items =>
      if items.size == 2 then
        match buildTree items[0]! with
        | some first =>
            match buildTree items[1]! with
            | some second =>
                let merged := mergeTrees first second
                let firstNodes := nodeCount first
                let secondNodes := nodeCount second
                let allocs := Runtime.allocCount
                let releasesBefore := Runtime.releaseCount
                let freesBefore := Runtime.freeCount
                let freesAfterFirst := Runtime.release first
                let freesAfterSecond := Runtime.release second
                let releasesAfterSecond := Runtime.releaseCount
                match render?
                    (mergedTreeValue merged allocs releasesBefore freesBefore freesAfterFirst
                      freesAfterSecond releasesAfterSecond firstNodes secondNodes) with
                | some bytes => Except.ok bytes
                | none => Except.error errorJson
            | none => Except.error errorJson
        | none => Except.error errorJson
      else
        Except.error errorJson
  | Value.null => Except.error errorJson
  | Value.bool _ => Except.error errorJson
  | Value.num _ => Except.error errorJson
  | Value.str _ => Except.error errorJson
  | Value.obj _ => Except.error errorJson

def makeMergedTree (input : ByteArray) : Except ByteArray ByteArray :=
  match parseBytes input with
  | some value => makeMergedTreeValue value
  | none => Except.error errorJson

def decodeMergedTreeInput (value : Value) : Option Tree :=
  match get? value treeFieldName with
  | some treeJson => decodeTree treeJson
  | none => none

def searchResultValue (found : Bool) : Value :=
  Value.obj #[
    Field.mk foundFieldName (Value.bool found),
    Field.mk allocsFieldName (Value.num Runtime.allocCount),
    Field.mk releasesFieldName (Value.num Runtime.releaseCount),
    Field.mk freesFieldName (Value.num Runtime.freeCount)
  ]

def searchMergedTreeValue (tree : Tree) (args : Array ByteArray) : Except ByteArray ByteArray :=
  match parseNeedle args with
  | none => Except.error errorJson
  | some needle =>
      match render? (searchResultValue (contains tree needle)) with
      | some bytes => Except.ok bytes
      | none => Except.error errorJson

def searchMergedTree (input : ByteArray) (args : Array ByteArray) : Except ByteArray ByteArray :=
  match parseBytes input with
  | some value =>
      match decodeMergedTreeInput value with
      | some tree => searchMergedTreeValue tree args
      | none => Except.error errorJson
  | none => Except.error errorJson

end Examples.JsonMergeTreeCommand
end LeanExe