BusLang/proof.h 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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
#pragma once

#include <memory>
#include <vector>
#include <print>
#include <string_view>

#include "file_range.h"
#include "id.h"

using std::vector;
using std::string_view;
using std::shared_ptr;
using std::pair;

struct Statement;
struct Expression;


struct Proof : std::enable_shared_from_this<Proof> {
	FileRange fileRange;
	constexpr Proof(FileRange _fileRange): fileRange(_fileRange) { }
	virtual void print() const = 0;
	virtual ~Proof() = default;
};


struct Proof_Id final : Proof {
	Id id;
	constexpr Proof_Id(FileRange _fileRange, Id _id): Proof(_fileRange), id(_id) { }
	void print() const override;
	inline ~Proof_Id() override = default;
};


struct Proof_Block final : Proof {
	vector<shared_ptr<const Statement>> statements;
	shared_ptr<const Proof> finalProof;
	constexpr Proof_Block(FileRange _fileRange, vector<shared_ptr<const Statement>>&& _statements, shared_ptr<const Proof>&& _finalProof):
		Proof(_fileRange), statements(std::move(_statements)), finalProof(std::move(_finalProof)) { }
	void print() const override;
	inline ~Proof_Block() override = default;
};


struct Proof_Unwrap final : Proof {
	shared_ptr<const Proof> subProof;
	constexpr Proof_Unwrap(FileRange _fileRange, shared_ptr<const Proof>&& _subProof):
		Proof(_fileRange), subProof(std::move(_subProof))
	{
	}
	void print() const override;
	inline ~Proof_Unwrap() override = default;
};

struct Proof_RawUnwrap final : Proof {
	shared_ptr<const Proof> subProof;
	constexpr Proof_RawUnwrap(FileRange _fileRange, shared_ptr<const Proof>&& _subProof):
		Proof(_fileRange), subProof(std::move(_subProof))
	{
	}
	void print() const override;
	inline ~Proof_RawUnwrap() override = default;
};

struct Proof_Wrap final : Proof {
	Id defId;
	shared_ptr<const Proof> subProof;
	constexpr Proof_Wrap(FileRange _fileRange, Id _defId, shared_ptr<const Proof>&& _subProof):
		Proof(_fileRange), defId(_defId), subProof(std::move(_subProof))
	{
	}
	void print() const override;
	inline ~Proof_Wrap() override = default;
};

struct Proof_RawWrap final : Proof {
	Id defId;
	shared_ptr<const Proof> subProof;
	constexpr Proof_RawWrap(FileRange _fileRange, Id _defId, shared_ptr<const Proof>&& _subProof):
		Proof(_fileRange), defId(_defId), subProof(std::move(_subProof))
	{
	}
	void print() const override;
	inline ~Proof_RawWrap() override = default;
};

struct Proof_Shove final : Proof {
	shared_ptr<const Proof> left;
	shared_ptr<const Proof> right;
	constexpr Proof_Shove(FileRange _fileRange, shared_ptr<const Proof>&& _left, shared_ptr<const Proof>&& _right):
		Proof(_fileRange), left(std::move(_left)), right(std::move(_right))
	{
	}
	void print() const override;
	inline ~Proof_Shove() override = default;
};

struct Proof_RawShove final : Proof {
	shared_ptr<const Proof> left;
	shared_ptr<const Proof> right;
	constexpr Proof_RawShove(FileRange _fileRange, shared_ptr<const Proof>&& _left, shared_ptr<const Proof>&& _right):
		Proof(_fileRange), left(std::move(_left)), right(std::move(_right))
	{
	}
	void print() const override;
	inline ~Proof_RawShove() override = default;
};


struct Proof_Substitute final : Proof {
	vector<pair<string_view, shared_ptr<const Expression>>> vec;
	shared_ptr<const Proof> subProof;
	constexpr Proof_Substitute(FileRange _fileRange, vector<pair<string_view, shared_ptr<const Expression>>>&& _vec, shared_ptr<const Proof>&& _subProof):
		Proof(_fileRange), vec(std::move(_vec)), subProof(std::move(_subProof)) { }
	void print() const override;
	inline ~Proof_Substitute() override = default;
};