def balance

qasim-bend-kit@0.1.0.2 · proof/JSON_ParallelProof.bend:32

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

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))