proof/JSON_PrimitiveProof.bend
qasim-bend-kit@0.1.0.2 · 84 lines · 14 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
3
4def R() -> Type:
5 Result<&1, &1, J.Error, J.Value>
6
7def absurd(-A: Type, empty: Empty) -> A:
8 match empty:
9
10def false_type(b: Bool) -> Data:
11 match b:
12 case False{}: Unit
13 case True{}: Empty
14
15def false_true(e: {False{} == True{} : Bool}) -> Empty:
16 %e : false_type(_)
17 Unit{}
18
19def proof_valid(+valid: Bool, witness: J.NumberProofFrom(valid)) -> {valid == True{} : Bool}:
20 match valid:
21 case True{}: {==}
22 case False{}:
23 match witness:
24
25def 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
30def 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
40def 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
47def 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
61def 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
65def 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
70def 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
79def 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
83def 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))