1	import Base
2	import ../libs/JSON.bend as J
3	import ./JSON_ListProof.bend as L
4	import ./JSON_PrimitiveProof.bend as P
5	import ./JSON_StringProof.bend as S
6	
7	def R() -> Type:
8	    Result<&1, &1, J.Error, J.Value>
9	
10	type Mode is Data:
11	    Whole{}
12	    Members{}
13	
14	def 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	
40	def 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	
48	def 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	
56	def 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	
64	def 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	
72	def 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	
96	def 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	
101	def 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	
107	def 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	
122	def 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	
137	def 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))