Repository navigation
Expand file tree
/
Copy pathproposition.cpp
More file actions
54 lines (48 loc) · 2.3 KB
/
Copy pathproposition.cpp
File metadata and controls
54 lines (48 loc) · 2.3 KB
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
#include "cppl/kernel/proposition.hpp"
#include "cppl/kernel/term.hpp"
#include "cppl/kernel/types.hpp"
#include <string>
#include <variant>
namespace cppl::kernel {
Proposition predicate(const Term& condition, bool positive) {
const Term* term = &condition;
while (const auto* primitive = std::get_if<Prim>(&term->node)) {
if (primitive->op != PrimOp::Not || primitive->arguments.size() != 1)
break;
positive = !positive;
term = &primitive->arguments[0];
}
if (const auto* primitive = std::get_if<Prim>(&term->node);
primitive != nullptr && primitive->arguments.size() == 2 &&
(primitive->op == PrimOp::Equal || primitive->op == PrimOp::NotEqual)) {
if (primitive->op == PrimOp::NotEqual)
positive = !positive;
if (positive) {
return Proposition::equality(Type{primitive->type}, primitive->arguments[0], primitive->arguments[1]);
}
return Proposition::equality(Type{kBoolean},
Term::primitive(PrimOp::Equal, primitive->type, primitive->arguments),
Term::literal(kBoolean, 0));
}
return Proposition::equality(Type{kBoolean}, *term, Term::literal(kBoolean, positive ? 1 : 0));
}
std::string describe(const Proposition& proposition) {
if (const auto* quantified = std::get_if<Forall>(&proposition.node)) {
return "forall " + describe(quantified->binder) + ". " + describe(*quantified->body);
}
if (const auto* implication = std::get_if<Implies>(&proposition.node)) {
return "(" + describe(*implication->premise) + " -> " + describe(*implication->conclusion) + ")";
}
if (const auto* conjunction = std::get_if<And>(&proposition.node)) {
return "(" + describe(*conjunction->left) + " && " + describe(*conjunction->right) + ")";
}
if (const auto* disjunction = std::get_if<Or>(&proposition.node)) {
return "(" + describe(*disjunction->left) + " || " + describe(*disjunction->right) + ")";
}
if (std::holds_alternative<Falsity>(proposition.node)) {
return "False";
}
const auto& equality = std::get<Eq>(proposition.node);
return "Eq<" + describe(equality.type) + ">(" + describe(equality.lhs) + ", " + describe(equality.rhs) + ")";
}
} // namespace cppl::kernel