-
Notifications
You must be signed in to change notification settings - Fork 0
/
dictionary.h
72 lines (59 loc) · 2.96 KB
/
dictionary.h
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
/*******************************************************************************
* *
* FunnyProof - Easy for use proof assistant. *
* Copyright (C) 2015 Nedeljko Stefanovic *
* *
* This program is free software: you can redistribute it and/or modify *
* it under the terms of version 3 of the GNU General Public License as *
* published by the Free Software Foundation. *
* *
* This program is distributed in the hope that it will be useful, *
* but WITHOUT ANY WARRANTY; without even the implied warranty of *
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *
* GNU General Public License for more details. *
* *
* You should have received a copy of the GNU General Public License *
* along with this program. If not, see <http://www.gnu.org/licenses/>. *
* *
*******************************************************************************/
#ifndef DICTIONARY_H
#define DICTIONARY_H
#include "language.h"
class Dictionary
{
public:
class Environment
{
std::map<std::wstring, Symbol> symbols;
std::map<Symbol, std::wstring> names;
public:
DECLARE Environment();
DECLARE Environment(const Environment &other);
DECLARE Environment(Environment &&other);
DECLARE bool insert(const std::wstring &name, const Symbol &symbol);
DECLARE bool insert(const Symbol &symbol, const std::wstring &name);
DECLARE const Symbol& operator ()(const std::wstring &name) const;
DECLARE std::wstring operator ()(const Symbol &symbol) const;
DECLARE const std::map<std::wstring, Symbol>& getSymbols() const;
DECLARE const std::map<Symbol, std::wstring>& getNames() const;
};
private:
std::vector<Environment> environents;
public:
DECLARE Dictionary();
DECLARE void push();
DECLARE bool pop();
DECLARE bool mergeTop2Environments();
DECLARE size_t size() const;
DECLARE Symbol operator ()(const std::wstring &name) const;
DECLARE std::wstring operator ()(const Symbol &symbol) const;
DECLARE const Environment& getCurrentEnvironment() const;
DECLARE const std::vector<Environment>& getEnvironments() const;
DECLARE bool insert(const std::wstring &name, const Symbol &symbol);
DECLARE std::wstring operator ()(const Term &term) const;
DECLARE std::wstring operator ()(const Formula &formula) const;
};
#ifdef INLINE
#include "dictionary_imp.h"
#endif
#endif // DICTIONARY_H