proof/JSON_AssemblyProof.bend
qasim-bend-kit@0.1.0.2 · 190 lines · 13 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
3import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as L
4import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as P
5import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
6
7def R() -> Type:
8 Result<&1, &1, J.Error, J.Value>
9
10type Mode is Data:
11 Whole{}
12 Members{}
13
14def tokens(value: J.Value, mode: Mode, tail: List<J.Token>) -> List<J.Token>:
15 match value:
16 case J.Arr{Nil{}}:
17 match mode:
18 case Whole{}: J.Delimiter{'['} <> J.Delimiter{']'} <> tail
19 case Members{}: J.Delimiter{']'} <> tail
20 case J.Arr{head <> rest}:
21 match mode:
22 case Whole{}: J.Delimiter{'['} <> tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail))
23 case Members{}: J.Delimiter{','} <> tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail))
24 case J.Obj{Nil{}}:
25 match mode:
26 case Whole{}: J.Delimiter{'{'} <> J.Delimiter{'}'} <> tail
27 case Members{}: J.Delimiter{'}'} <> tail
28 case J.Obj{(key, value) <> rest}:
29 match mode:
30 case Whole{}: J.Delimiter{'{'} <> J.Atom{Done{J.Str{key}}} <> J.Delimiter{':'} <> tokens(value, Whole{}, tokens(J.Obj{rest}, Members{}, tail))
31 case Members{}: J.Delimiter{','} <> J.Atom{Done{J.Str{key}}} <> J.Delimiter{':'} <> tokens(value, Whole{}, tokens(J.Obj{rest}, Members{}, tail))
32 case J.Null{}: J.Atom{J.decode_payload("null")} <> tail
33 case J.Bool{truth}:
34 match truth:
35 case True{}: J.Atom{J.decode_payload("true")} <> tail
36 case False{}: J.Atom{J.decode_payload("false")} <> tail
37 case J.Number{lexeme, certificate}: J.Atom{J.decode_payload(lexeme)} <> tail
38 case J.Str{text}: J.Atom{J.decode_payload("\"" ++ J.escape_string(text) ++ "\"")} <> tail
39
40def start_members(value: J.Value,
41 acc: List<&2, J.Value>,
42 fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, kont: J.ParserKont) -> J.Assembly:
43 match value:
44 case J.Arr{_}: J.ArrayComma{acc, kont}
45 case J.Obj{_}: J.ObjectComma{fields, kont}
46 case _: J.NeedValue{kont}
47
48def start(value: J.Value,
49 mode: Mode,
50 acc: List<&2, J.Value>,
51 fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, kont: J.ParserKont) -> J.Assembly:
52 match mode:
53 case Whole{}: J.NeedValue{kont}
54 case Members{}: start_members(value, acc, fields, kont)
55
56def completed_members(value: J.Value,
57 acc: List<&2, J.Value>,
58 fields: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> J.Value:
59 match value:
60 case J.Arr{xs}: J.Arr{List.reverse(&2, J.Value, List.reverse.go(&2, J.Value, xs, acc))}
61 case J.Obj{xs}: J.Obj{List.reverse(&2, Sigma<&2, &2, String, key => J.Value>, List.reverse.go(&2, Sigma<&2, &2, String, key => J.Value>, xs, fields))}
62 case _: value
63
64def completed(value: J.Value,
65 mode: Mode,
66 acc: List<&2, J.Value>,
67 fields: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> J.Value:
68 match mode:
69 case Whole{}: value
70 case Members{}: completed_members(value, acc, fields)
71
72def atom_roundtrip(+value: J.Value,
73 +mode: Mode,
74 -tail: List<J.Token>,
75 +acc: List<&2, J.Value>,
76 +fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, +kont: J.ParserKont, +text: String, started: {start(value, mode, acc, fields, kont) == J.NeedValue{kont} : J.Assembly}, completed_value: {completed(value, mode, acc, fields) == value : J.Value}, tokenized: {tokens(value, mode, tail) == J.Atom{J.decode_payload(text)} <> tail : List<J.Token>}, decoded: {J.decode_payload(text) == Done{value} : Result<&1, &1, J.Error, J.Value>}) -> {J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))) : R()}:
77 Equal.trans(R(),
78 J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
79 J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
80 J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))),
81 Equal.trans(R(),
82 J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
83 J.assemble(tokens(value, mode, tail), J.NeedValue{kont}),
84 J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
85 Equal.cong(J.Assembly, R(), state => J.assemble(tokens(value, mode, tail), state),
86 start(value, mode, acc, fields, kont), J.NeedValue{kont}, started),
87 Equal.cong(List<J.Token>, R(), stream => J.assemble(stream, J.NeedValue{kont}),
88 tokens(value, mode, tail), J.Atom{Done{value}} <> tail,
89 Equal.trans(List<J.Token>, tokens(value, mode, tail), J.Atom{J.decode_payload(text)} <> tail,
90 J.Atom{Done{value}} <> tail, tokenized,
91 Equal.cong(Result<&1, &1, J.Error, J.Value>, List<J.Token>, result => J.Atom{result} <> tail,
92 J.decode_payload(text), Done{value}, decoded)))),
93 Equal.cong(J.Value, R(), item => J.assemble(tail, J.assembly_resume(kont, item)),
94 value, completed(value, mode, acc, fields), Equal.sym(J.Value, completed(value, mode, acc, fields), value, completed_value)))
95
96def array_first_atom(result: Result<&1, &1, J.Error, J.Value>,
97 -tail: List<J.Token>,
98 +kont: J.ParserKont) -> {J.assemble(J.Atom{result} <> tail, J.ArrayFirst{kont}) == J.assemble(J.Atom{result} <> tail, J.NeedValue{J.InArray{Nil{}, kont}}) : R()}:
99 {==}
100
101def array_next_atom(result: Result<&1, &1, J.Error, J.Value>,
102 -tail: List<J.Token>,
103 +acc: List<&2, J.Value>,
104 +kont: J.ParserKont) -> {J.assemble(J.Atom{result} <> tail, J.ArrayNext{acc, kont}) == J.assemble(J.Atom{result} <> tail, J.NeedValue{J.InArray{acc, kont}}) : R()}:
105 {==}
106
107def array_first(+value: J.Value,
108 -tail: List<J.Token>,
109 +acc: List<&2, J.Value>,
110 +kont: J.ParserKont) -> {J.assemble(tokens(value, Whole{}, tail), J.ArrayFirst{kont}) == J.assemble(tokens(value, Whole{}, tail), J.NeedValue{J.InArray{Nil{}, kont}}) : R()}:
111 match value:
112 case J.Arr{Nil{}}: {==}
113 case J.Arr{head <> rest}: {==}
114 case J.Obj{Nil{}}: {==}
115 case J.Obj{(key, head) <> rest}: {==}
116 case J.Null{}: array_first_atom(J.decode_payload("null"), tail, kont)
117 case J.Bool{True{}}: array_first_atom(J.decode_payload("true"), tail, kont)
118 case J.Bool{False{}}: array_first_atom(J.decode_payload("false"), tail, kont)
119 case J.Number{s, cert}: array_first_atom(J.decode_payload(s), tail, kont)
120 case J.Str{s}: array_first_atom(J.decode_payload("\"" ++ J.escape_string(s) ++ "\""), tail, kont)
121
122def array_next(+value: J.Value,
123 -tail: List<J.Token>,
124 +acc: List<&2, J.Value>,
125 +kont: J.ParserKont) -> {J.assemble(tokens(value, Whole{}, tail), J.ArrayNext{acc, kont}) == J.assemble(tokens(value, Whole{}, tail), J.NeedValue{J.InArray{acc, kont}}) : R()}:
126 match value:
127 case J.Arr{Nil{}}: {==}
128 case J.Arr{head <> rest}: {==}
129 case J.Obj{Nil{}}: {==}
130 case J.Obj{(key, head) <> rest}: {==}
131 case J.Null{}: array_next_atom(J.decode_payload("null"), tail, acc, kont)
132 case J.Bool{True{}}: array_next_atom(J.decode_payload("true"), tail, acc, kont)
133 case J.Bool{False{}}: array_next_atom(J.decode_payload("false"), tail, acc, kont)
134 case J.Number{s, cert}: array_next_atom(J.decode_payload(s), tail, acc, kont)
135 case J.Str{s}: array_next_atom(J.decode_payload("\"" ++ J.escape_string(s) ++ "\""), tail, acc, kont)
136
137def roundtrip(+value: J.Value,
138 +mode: Mode,
139 -tail: List<J.Token>,
140 +acc: List<&2, J.Value>,
141 +fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, +kont: J.ParserKont) -> {J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))) : R()}:
142 match value:
143 case J.Arr{Nil{}}:
144 match mode:
145 case Whole{}: {==}
146 case Members{}: {==}
147 case J.Arr{head <> rest}:
148 match mode:
149 case Whole{}:
150 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.ArrayFirst{kont}), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{Nil{}, kont}}), array_first(head, tokens(J.Arr{rest}, Members{}, tail), Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
151 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{Nil{}, kont}}), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> Nil{}, kont}), roundtrip(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail), Nil{}, Nil{}, J.InArray{Nil{}, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
152 %Equal.sym(R(), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> Nil{}, kont}), J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{rest}, Members{}, head <> Nil{}, Nil{}))), roundtrip(J.Arr{rest}, Members{}, tail, head <> Nil{}, Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
153 Equal.cong(List<&2, J.Value>, R(), xs => J.assemble(tail, J.assembly_resume(kont, J.Arr{xs})), List.reverse(&2, J.Value, List.reverse(&2, J.Value, head <> rest)), head <> rest, L.reverse_twice(J.Value, head <> rest))
154 case Members{}:
155 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.ArrayNext{acc, kont}), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{acc, kont}}), array_next(head, tokens(J.Arr{rest}, Members{}, tail), acc, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Members{}, acc, fields))) : R()}
156 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{acc, kont}}), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> acc, kont}), roundtrip(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail), Nil{}, Nil{}, J.InArray{acc, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Members{}, acc, fields))) : R()}
157 roundtrip(J.Arr{rest}, Members{}, tail, head <> acc, Nil{}, kont)
158 case J.Obj{Nil{}}:
159 match mode:
160 case Whole{}: {==}
161 case Members{}: {==}
162 case J.Obj{(key, head) <> rest}:
163 match mode:
164 case Whole{}:
165 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail)), J.NeedValue{J.InObject{key, Nil{}, kont}}), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> Nil{}, kont}), roundtrip(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail), Nil{}, Nil{}, J.InObject{key, Nil{}, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Whole{}, acc, fields))) : R()}
166 %Equal.sym(R(), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> Nil{}, kont}), J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{rest}, Members{}, Nil{}, (key, head) <> Nil{}))), roundtrip(J.Obj{rest}, Members{}, tail, Nil{}, (key, head) <> Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Whole{}, acc, fields))) : R()}
167 Equal.cong(List<&2, Sigma<&2, &2, String, key => J.Value>>, R(), xs => J.assemble(tail, J.assembly_resume(kont, J.Obj{xs})), List.reverse(&2, Sigma<&2, &2, String, key => J.Value>, List.reverse(&2, Sigma<&2, &2, String, key => J.Value>, (key, head) <> rest)), (key, head) <> rest, L.reverse_twice(Sigma<&2, &2, String, key => J.Value>, (key, head) <> rest))
168 case Members{}:
169 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail)), J.NeedValue{J.InObject{key, fields, kont}}), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> fields, kont}), roundtrip(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail), Nil{}, Nil{}, J.InObject{key, fields, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Members{}, acc, fields))) : R()}
170 roundtrip(J.Obj{rest}, Members{}, tail, Nil{}, (key, head) <> fields, kont)
171 case J.Null{}:
172 match mode:
173 case Whole{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
174 case Members{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
175 case J.Bool{True{}}:
176 match mode:
177 case Whole{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
178 case Members{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
179 case J.Bool{False{}}:
180 match mode:
181 case Whole{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
182 case Members{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
183 case J.Number{s, cert}:
184 match mode:
185 case Whole{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
186 case Members{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
187 case J.Str{s}:
188 match mode:
189 case Whole{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))
190 case Members{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))