CBMC
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 "string_utils.h"
12 
13 #include <iostream>
14 
15 std::string lispexprt::expr2string() const
16 {
17  std::string result;
18 
19  switch(type)
20  {
21  case Number:
22  case Symbol:
23  result=value;
24  break;
25 
26  case List:
27  result="(";
28  for(std::size_t j=0; j<size(); j++)
29  {
30  if((j+1)==size() && size()!=1)
31  {
32  if((*this)[j].is_nil())
33  break;
34  result+=" . ";
35  }
36  else if(j!=0)
37  result+=' ';
38 
39  result+=(*this)[j].expr2string();
40  }
41  result+=')';
42  break;
43 
44  case String:
45  result="\"";
46  result+=escape(value);
47  result+="\"";
48  break;
49  }
50 
51  return result;
52 }
53 
54 bool lispexprt::parse(const std::string &s)
55 {
57  return parse(s, ptr);
58 }
59 
61  const std::string &s,
63 {
64  clear();
65  value.clear();
66 
67  if(ptr==std::string::npos || ptr>=s.size())
68  return true;
69 
70  // we ignore whitespace
71  ptr=s.find_first_not_of(" \t", ptr);
72  if(ptr==std::string::npos)
73  return true;
74 
75  if(s[ptr]=='(') // LispCons
76  {
77  type=List;
78  lispexprt expr;
79 
80  for(ptr++; ptr<s.size();)
81  {
82  bool dot=false;
83 
84  if(ptr<s.size() && s[ptr]=='.')
85  {
86  dot=true;
87  ptr++;
88  }
89 
90  if(expr.parse(s, ptr))
91  return true;
92  push_back(expr);
93 
94  if(ptr<s.size() && s[ptr]==')')
95  {
96  if(!dot && size()>1)
97  {
98  expr.parse("nil");
99  push_back(expr);
100  }
101 
102  ptr++;
103  break;
104  }
105  }
106  }
107  else if(s[ptr]=='"') // LispString
108  {
109  type=String;
110  bool quoted=false;
111 
112  value.reserve(50); // guessing - will be adjusted automatically
113 
114  for(ptr++; ptr<s.size() && (s[ptr]!='"' && !quoted); ptr++)
115  {
116  if(!quoted && s[ptr]=='\\')
117  quoted=true;
118  else
119  {
120  quoted=false;
121  value+=s[ptr];
122  }
123  }
124 
125  if(ptr<s.size())
126  ptr++;
127  }
128  else if(isdigit(s[ptr])) // LispNumber
129  {
130  value.reserve(10); // guessing - will be adjusted automatically
131 
132  type=Number;
133  for(; ptr<s.size() && (isdigit(s[ptr]) || s[ptr]=='.'); ptr++)
134  value+=s[ptr];
135  }
136  else // must be LispSymbol
137  {
138  value.reserve(20); // guessing - will be adjusted automatically
139 
140  type=Symbol;
141  for(; ptr<s.size() && s[ptr]!=' ' && s[ptr]!='\t' &&
142  s[ptr]!=')' && s[ptr]!='.'; ptr++)
143  value+=s[ptr];
144  }
145 
146  // we ignore whitespace
147  ptr=s.find_first_not_of(" \t", ptr);
148 
149  return false;
150 }
151 
153 {
154  std::string line;
155  char ch;
156 
157  while(true)
158  {
159  line.clear();
160 
161  while(true)
162  {
163  if(!std::cin.read(&ch, 1))
164  return 0;
165 
166  if(ch=='\n')
167  {
168  lispexprt expr;
169  if(expr.parse(line))
170  std::cout << "Parsing error\n";
171  else
172  std::cout << expr << "\n";
173 
174  break;
175  }
176 
177  line+=ch;
178  }
179  }
180 
181  return 0;
182 }
@ Number
Definition: lispexpr.h:76
@ String
Definition: lispexpr.h:76
@ Symbol
Definition: lispexpr.h:76
lispsymbolt value
Definition: lispexpr.h:77
enum lispexprt::@7 type
std::string expr2string() const
Definition: lispexpr.cpp:15
bool parse(const std::string &s)
Definition: lispexpr.cpp:54
int isdigit(int c)
Definition: ctype.c:24
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:359
int __CPROVER_ID java::java io InputStream read
Definition: java.io.c:5
int test_lispexpr()
Definition: lispexpr.cpp:152
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
#define size_type
Definition: unistd.c:347