proof/JSON_ParallelProof.bend
qasim-bend-kit@0.1.0.2 · 57 lines · 7 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
3
4
5def forest(trees: List<&2, J.LexTree>, tail: List<J.Token>) -> List<J.Token>:
6 match trees:
7 case Nil{}: tail
8 case head <> rest: J.token_list(J.decode_tree(head), forest(rest, tail))
9
10def flat(items: List<&2, J.Lexeme>, tail: List<J.Token>) -> List<J.Token>:
11 match items:
12 case Nil{}: tail
13 case head <> rest: J.decode_lexeme(head) <> flat(rest, tail)
14
15def join(+trees: List<&2, J.LexTree>,
16 -tail: List<J.Token>) -> {J.token_list(J.decode_tree(J.lex_join(trees)), tail) == forest(trees, tail) : List<J.Token>}:
17 match trees:
18 case Nil{}: {==}
19 case head <> rest:
20 Equal.cong(List<J.Token>, List<J.Token>, xs => J.token_list(J.decode_tree(head), xs),
21 J.token_list(J.decode_tree(J.lex_join(rest)), tail), forest(rest, tail), join(rest, tail))
22
23def pairs(+trees: List<&2, J.LexTree>,
24 -tail: List<J.Token>) -> {forest(J.lex_pairs(trees), tail) == forest(trees, tail) : List<J.Token>}:
25 match trees:
26 case Nil{}: {==}
27 case head <> Nil{}: {==}
28 case left <> right <> rest:
29 Equal.cong(List<J.Token>, List<J.Token>, xs => J.token_list(J.decode_tree(left), J.token_list(J.decode_tree(right), xs)),
30 forest(J.lex_pairs(rest), tail), forest(rest, tail), pairs(rest, tail))
31
32def balance(+fuel: Nat,
33 +trees: List<&2, J.LexTree>,
34 -tail: List<J.Token>) -> {J.token_list(J.decode_tree(J.lex_balance(fuel, trees)), tail) == forest(trees, tail) : List<J.Token>}:
35 match fuel:
36 case 0n: join(trees, tail)
37 case 1n+p:
38 match trees:
39 case Nil{}: {==}
40 case head <> Nil{}: {==}
41 case left <> right <> rest:
42 Equal.trans(List<J.Token>, J.token_list(J.decode_tree(J.lex_balance(p, J.lex_pairs(left <> right <> rest))), tail),
43 forest(J.lex_pairs(left <> right <> rest), tail), forest(left <> right <> rest, tail),
44 balance(p, J.lex_pairs(left <> right <> rest), tail), pairs(left <> right <> rest, tail))
45
46def leaves(+items: List<&2, J.Lexeme>,
47 -tail: List<J.Token>) -> {forest(J.lex_leaves(items), tail) == flat(items, tail) : List<J.Token>}:
48 match items:
49 case Nil{}: {==}
50 case head <> rest:
51 Equal.cong(List<J.Token>, List<J.Token>, xs => J.decode_lexeme(head) <> xs,
52 forest(J.lex_leaves(rest), tail), flat(rest, tail), leaves(rest, tail))
53
54def decode(+items: List<&2, J.Lexeme>,
55 -tail: List<J.Token>) -> {J.token_list(J.decode_tree(J.lex_tree(items)), tail) == flat(items, tail) : List<J.Token>}:
56 Equal.trans(List<J.Token>, J.token_list(J.decode_tree(J.lex_tree(items)), tail), forest(J.lex_leaves(items), tail), flat(items, tail),
57 balance(1n+List.length(&2, J.Lexeme, items), J.lex_leaves(items), tail), leaves(items, tail))