1	import Base
2	import ../libs/JSON.bend as J
3	
4	def R() -> Type:
5	    Result<&1, &1, J.Error, J.Value>
6	
7	def absurd(-A: Type, empty: Empty) -> A:
8	    match empty:
9	
10	def false_type(b: Bool) -> Data:
11	    match b:
12	        case False{}: Unit
13	        case True{}: Empty
14	
15	def false_true(e: {False{} == True{} : Bool}) -> Empty:
16	    %e : false_type(_)
17	    Unit{}
18	
19	def proof_valid(+valid: Bool, witness: J.NumberProofFrom(valid)) -> {valid == True{} : Bool}:
20	    match valid:
21	        case True{}: {==}
22	        case False{}:
23	            match witness:
24	
25	def cert_valid(+text: String,
26	               certificate: J.NumberCert<text>) -> {J.number_valid(text) == True{} : Bool}:
27	    match certificate:
28	        case J.Certified{witness}: proof_valid(J.number_valid(text), witness)
29	
30	def proof_unique(+valid: Bool,
31	                 +a: J.NumberProofFrom(valid),
32	                 +b: J.NumberProofFrom(valid)) -> {a == b : J.NumberProofFrom(valid)}:
33	    match valid:
34	        case True{}:
35	            match a b:
36	                case Unit{} Unit{}: {==}
37	        case False{}:
38	            match a:
39	
40	def cert_unique(+text: String,
41	                +a: J.NumberCert<text>,
42	                +b: J.NumberCert<text>) -> {a == b : J.NumberCert<text>}:
43	    match a b:
44	        case J.Certified{x} J.Certified{y}:
45	            Equal.cong(J.NumberProof(text), J.NumberCert<text>, w => J.Certified{w}, x, y, proof_unique(J.number_valid(text), x, y))
46	
47	def number_route(+text: String,
48	                 +valid: Bool,
49	                 +certificate: J.NumberCert<text>,
50	                 evidence: {J.number_valid(text) == valid : Bool}) -> {J.payload_number(text, valid, evidence) == Done{J.Number{text, certificate}} : R()}:
51	    match valid:
52	        case True{}:
53	            Equal.cong(J.NumberCert<text>, R(), c => Done{J.Number{text, c}},
54	                J.Certified{J.number_proof(text, evidence)}, certificate,
55	                cert_unique(text, J.Certified{J.number_proof(text, evidence)}, certificate))
56	        case False{}:
57	            absurd({J.payload_number(text, False{}, evidence) == Done{J.Number{text, certificate}} : R()},
58	                false_true(Equal.trans(Bool, False{}, J.number_valid(text), True{},
59	                    Equal.sym(Bool, J.number_valid(text), False{}, evidence), cert_valid(text, certificate))))
60	
61	def number_roundtrip(+text: String,
62	                     +certificate: J.NumberCert<text>) -> {J.decode_payload(text) == Done{J.Number{text, certificate}} : R()}:
63	    number_route(text, J.number_valid(text), certificate, {==})
64	
65	def invalid_step(+text: String) -> {J.number_valid_step(text, J.NumberInvalid{}) == J.NumberInvalid{} : J.NumberState}:
66	    match text:
67	        case SNil{}: {==}
68	        case SCon{head, tail}: {==}
69	
70	def route_false(+text: String,
71	                +valid: Bool,
72	                evidence: {J.number_valid(text) == valid : Bool},
73	                no: {valid == False{} : Bool}) -> {J.payload_number(text, valid, evidence) == J.payload_other(text) : R()}:
74	    match valid:
75	        case False{}: {==}
76	        case True{}:
77	            absurd({J.payload_number(text, True{}, evidence) == J.payload_other(text) : R()}, false_true(Equal.sym(Bool, True{}, False{}, no)))
78	
79	def decode_false(+text: String,
80	                 no: {J.number_valid(text) == False{} : Bool}) -> {J.decode_payload(text) == J.payload_other(text) : R()}:
81	    route_false(text, J.number_valid(text), {==}, no)
82	
83	def invalid_end(+text: String) -> {J.number_valid_end(J.number_valid_step(text, J.NumberInvalid{})) == False{} : Bool}:
84	    Equal.cong(J.NumberState, Bool, J.number_valid_end, J.number_valid_step(text, J.NumberInvalid{}), J.NumberInvalid{}, invalid_step(text))