BusLang/proof.cpp at master · JesseBusman/BusLang · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
#include "proof.h"
#include "id.h"
#include "expression.h"
#include "statement.h"


void Proof_Id::print() const {
	std::print("{}:{}", id.name, id.id);
}


void Proof_Block::print() const {
	std::print("{{\n");
	for (auto& s : statements) {
		s->print(1);
		std::println();
	}
	std::print("    ");
	finalProof->print();
	std::print("\n}}");
}


void Proof_Unwrap::print() const {
	std::print("unwrap (");
	subProof->print();
	std::print(")");
}


void Proof_RawUnwrap::print() const {
	std::print("rawunwrap (");
	subProof->print();
	std::print(")");
}


void Proof_Wrap::print() const {
	std::print("wrap {}:{} (", defId.name, defId.id);
	subProof->print();
	std::print(")");
}

void Proof_RawWrap::print() const {
	std::print("rawwrap {}:{} (", defId.name, defId.id);
	subProof->print();
	std::print(")");
}


void Proof_Shove::print() const {
	std::print("(");
	left->print();
	std::print(") > (");
	right->print();
	std::print(")");
}

void Proof_RawShove::print() const {
	std::print("(");
	left->print();
	std::print(") >> (");
	right->print();
	std::print(")");
}


void Proof_Substitute::print() const {
	std::print("substitute ");
	for (unsigned int i=0; i<vec.size(); i++) {
		if (i != 0) std::print(", ");
		std::print("{}=(", vec[i].first);
		vec[i].second->print();
		std::print(")");
	}
	std::print(" in ");
	subProof->print();
}