1	import Base
2	import ../libs/JSON.bend as J
3	
4	# Semantic token sequence for a forest, independent of its scheduling shape.
5	def 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	
10	def 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	
15	def 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	
23	def 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	
32	def 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	
46	def 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	
54	def 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))