def assemble_source

qasim-bend-kit@0.1.0.2 · PROOF.bend:44

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as Json
import qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend as ParallelProof
import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as AssemblyProof
import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as SourceProof

44def assemble_source(+value: Json.Value) -> {Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}) == Done{value} : ResultValue()}:
45    Equal.trans(ResultValue(),
46        Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
47        Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
48        Done{value},
49        Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
50            Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
51            AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
52            Equal.trans(List<Json.Token>,
53                Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
54                SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
55                AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
56                Equal.trans(List<Json.Token>,
57                    Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
58                    ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
59                    SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
60                    ParallelProof.decode(Json.source(value, False{}, Nil{}), Nil{}),
61                    Equal.sym(List<Json.Token>, SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
62                        ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
63                        SourceProof.token_source_flat(Json.source(value, False{}, Nil{}), Nil{}))),
64                SourceProof.source_tokens(value, AssemblyProof.Whole{}, Nil{}, Nil{}))),
65        Equal.trans(ResultValue(),
66            Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
67            Json.assemble(Nil{}, Json.assembly_resume(Json.Top{}, value)),
68            Done{value},
69            AssemblyProof.roundtrip(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Nil{}, Json.Top{}), {==}))