cprover
lispexpr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "lispexpr.h"
10 
11 #include <iostream>
12 
13 std::string lispexprt::expr2string() const
14 {
15  std::string result;
16 
17  switch(type)
18  {
19  case Number:
20  case Symbol:
21  result=value;
22  break;
23 
24  case List:
25  result="(";
26  for(unsigned j=0; j<size(); j++)
27  {
28  if((j+1)==size() && size()!=1)
29  {
30  if((*this)[j].is_nil())
31  break;
32  result+=" . ";
33  }
34  else if(j!=0)
35  result+=' ';
36 
37  result+=(*this)[j].expr2string();
38  }
39  result+=')';
40  break;
41 
42  case String:
43  result="\"";
44  result+=escape(value);
45  result+="\"";
46  break;
47  }
48 
49  return result;
50 }
51 
52 bool lispexprt::parse(const std::string &s)
53 {
55  return parse(s, ptr);
56 }
57 
59  const std::string &s,
61 {
62  clear();
63  value="";
64 
65  if(ptr==std::string::npos || ptr>=s.size())
66  return true;
67 
68  // we ignore whitespace
69  ptr=s.find_first_not_of(" \t", ptr);
70  if(ptr==std::string::npos)
71  return true;
72 
73  if(s[ptr]=='(') // LispCons
74  {
75  type=List;
76  lispexprt expr;
77 
78  for(ptr++; ptr<s.size();)
79  {
80  bool dot=false;
81 
82  if(ptr<s.size() && s[ptr]=='.')
83  {
84  dot=true;
85  ptr++;
86  }
87 
88  if(expr.parse(s, ptr))
89  return true;
90  push_back(expr);
91 
92  if(ptr<s.size() && s[ptr]==')')
93  {
94  if(!dot && size()>1)
95  {
96  expr.parse("nil");
97  push_back(expr);
98  }
99 
100  ptr++;
101  break;
102  }
103  }
104  }
105  else if(s[ptr]=='"') // LispString
106  {
107  type=String;
108  bool quoted=false;
109 
110  value.reserve(50); // guessing - will be adjusted automatically
111 
112  for(ptr++; ptr<s.size() && (s[ptr]!='"' && !quoted); ptr++)
113  {
114  if(!quoted && s[ptr]=='\\')
115  quoted=true;
116  else
117  {
118  quoted=false;
119  value+=s[ptr];
120  }
121  }
122 
123  if(ptr<s.size())
124  ptr++;
125  }
126  else if(isdigit(s[ptr])) // LispNumber
127  {
128  value.reserve(10); // guessing - will be adjusted automatically
129 
130  type=Number;
131  for(; ptr<s.size() && (isdigit(s[ptr]) || s[ptr]=='.'); ptr++)
132  value+=s[ptr];
133  }
134  else // must be LispSymbol
135  {
136  value.reserve(20); // guessing - will be adjusted automatically
137 
138  type=Symbol;
139  for(; ptr<s.size() && s[ptr]!=' ' && s[ptr]!='\t' &&
140  s[ptr]!=')' && s[ptr]!='.'; ptr++)
141  value+=s[ptr];
142  }
143 
144  // we ignore whitespace
145  ptr=s.find_first_not_of(" \t", ptr);
146 
147  return false;
148 }
149 
150 std::string escape(const std::string &s)
151 {
152  std::string result;
153 
154  for(unsigned i=0; i<s.size(); i++)
155  {
156  if(s[i]=='\\' || s[i]=='"')
157  result+='\\';
158 
159  result+=s[i];
160  }
161 
162  return result;
163 }
164 
166 {
167  std::string line;
168  char ch;
169 
170  while(true)
171  {
172  line="";
173 
174  while(true)
175  {
176  if(!std::cin.read(&ch, 1))
177  return 0;
178 
179  if(ch=='\n')
180  {
181  lispexprt expr;
182  if(expr.parse(line))
183  std::cout << "Parsing error\n";
184  else
185  std::cout << expr << "\n";
186 
187  break;
188  }
189 
190  line+=ch;
191  }
192  }
193 
194  return 0;
195 }
std::string expr2string() const
Definition: lispexpr.cpp:13
bool parse(const std::string &s)
Definition: lispexpr.cpp:52
unsignedbv_typet size_type()
Definition: c_types.cpp:57
int test_lispexpr()
Definition: lispexpr.cpp:165
lispsymbolt value
Definition: lispexpr.h:78
std::string escape(const std::string &s)
Definition: lispexpr.cpp:150
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
Definition: dot.cpp:353
enum lispexprt::@19 type