1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Implementation for class StringSymbol.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 #include "NA_Theory.hh"
35
36 // interface class definitions
37 #include "symbol.hh"
38 #include "dagNode.hh"
39 #include "term.hh"
40
41 // built in class definitions
42 #include "stringSymbol.hh"
43 #include "stringTerm.hh"
44 #include "stringDagNode.hh"
45
StringSymbol(int id)46 StringSymbol::StringSymbol(int id)
47 : NA_Symbol(id)
48 {
49 sort = 0;
50 charSort = 0;
51 }
52
53 void
fillInSortInfo(Term * subject)54 StringSymbol::fillInSortInfo(Term* subject)
55 {
56 Sort* s = (static_cast<StringTerm*>(subject)->getValue().length() == 1) ? charSort : sort;
57 subject->setSortInfo(s->component(), s->index());
58 }
59
60 void
computeBaseSort(DagNode * subject)61 StringSymbol::computeBaseSort(DagNode* subject)
62 {
63 Sort* s = (static_cast<StringDagNode*>(subject)->getValue().length() == 1) ? charSort : sort;
64 subject->setSortIndex(s->index());
65 }
66
67 bool
isConstructor(DagNode *)68 StringSymbol::isConstructor(DagNode* /* subject */)
69 {
70 return true;
71 }
72
73 void
compileOpDeclarations()74 StringSymbol::compileOpDeclarations()
75 {
76 const Vector<OpDeclaration>& opDecls = getOpDeclarations();
77 int nrOpDecls = opDecls.length();
78 for (int i = 0; i < nrOpDecls; i++)
79 {
80 Sort* s = opDecls[i].getDomainAndRange()[0];
81 if (sort == 0 || s->index() < sort->index())
82 sort = s; // set sort to largest (smallest index) declared sort
83 if (charSort == 0 || s->index() > charSort->index())
84 charSort = s; // set charSort to smallest (largest index) declared sort
85 }
86 }
87
88 Term*
termify(DagNode * dagNode)89 StringSymbol::termify(DagNode* dagNode)
90 {
91 return new StringTerm(this, safeCast(StringDagNode*, dagNode)->getValue());
92 }
93