Skip to content

Commit 0bc02c0

Browse files
ajreynolajreynol
committed
Format
1 parent fb2f7ab commit 0bc02c0

3 files changed

Lines changed: 35 additions & 32 deletions

File tree

‎src/cmd_parser.cpp‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -196,11 +196,11 @@ bool CmdParser::parseNextCommand()
196196
// explicit parameters are quote arrows
197197
std::map<ExprValue*, AttrMap>::iterator itp;
198198
AttrMap::iterator itpa;
199-
for (size_t i=0, nparams = params.size(); i<nparams; i++)
199+
for (size_t i = 0, nparams = params.size(); i < nparams; i++)
200200
{
201-
size_t ii = nparams-i-1;
201+
size_t ii = nparams - i - 1;
202202
Expr qt = d_state.mkQuoteType(params[ii]);
203-
itp = pattrMap.find(params[ii].getValue());
203+
itp = pattrMap.find(params[ii].getValue());
204204
if (itp != pattrMap.end())
205205
{
206206
itpa = itp->second.find(Attr::REQUIRES);
@@ -532,7 +532,7 @@ bool CmdParser::parseNextCommand()
532532
std::map<ExprValue*, AttrMap> pattrMap;
533533
std::vector<Expr> vars =
534534
d_eparser.parseAndBindSortedVarList(Kind::LAMBDA, pattrMap);
535-
if (vars.size()<pattrMap.size())
535+
if (vars.size() < pattrMap.size())
536536
{
537537
// If there were implicit variables, we go back and refine what is
538538
// bound in the body to only include the explicit arguments. This
@@ -726,7 +726,8 @@ bool CmdParser::parseNextCommand()
726726
}
727727
// push the scope
728728
d_state.pushScope();
729-
std::vector<Expr> vars = d_eparser.parseAndBindSortedVarList(Kind::PROGRAM);
729+
std::vector<Expr> vars =
730+
d_eparser.parseAndBindSortedVarList(Kind::PROGRAM);
730731
std::vector<Expr> argTypes = d_eparser.parseTypeList();
731732
Expr retType = d_eparser.parseType();
732733
Expr progType = retType;

‎src/expr_parser.cpp‎

Lines changed: 12 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,8 @@ Expr ExprParser::parseExpr()
212212
{
213213
nscopes = 1;
214214
d_state.pushScope();
215-
std::vector<Expr> vs = parseAndBindSortedVarList(Kind::NONE);
215+
std::vector<Expr> vs =
216+
parseAndBindSortedVarList(Kind::NONE);
216217
if (vs.empty())
217218
{
218219
d_lex.parseError("Expected non-empty sorted variable list");
@@ -769,7 +770,7 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(Kind k)
769770
}
770771

771772
std::vector<Expr> ExprParser::parseAndBindSortedVarList(
772-
Kind k, std::map<ExprValue*, AttrMap>& amap)
773+
Kind k, std::map<ExprValue*, AttrMap>& amap)
773774
{
774775
std::vector<Expr> varList;
775776
d_lex.eatToken(Token::LPAREN);
@@ -782,7 +783,7 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(
782783
t = parseType();
783784
Expr v;
784785
bool isImplicit = false;
785-
if (k==Kind::NONE)
786+
if (k == Kind::NONE)
786787
{
787788
// lookup and type check
788789
v = d_state.getBoundVar(name, t);
@@ -1114,7 +1115,8 @@ std::string ExprParser::parseStr(bool unescape)
11141115
return s;
11151116
}
11161117

1117-
void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope, Kind plk)
1118+
void ExprParser::parseAttributeList(
1119+
Kind k, Expr& e, AttrMap& attrs, bool& pushedScope, Kind plk)
11181120
{
11191121
std::map<std::string, Attr>::iterator its;
11201122
// while the next token is KEYWORD, exit if RPAREN
@@ -1156,7 +1158,7 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
11561158
// attributes on parameters
11571159
// parameter lists of define and declare-parameterized-const
11581160
// allow for several attributes
1159-
if (plk==Kind::CONST || plk==Kind::LAMBDA)
1161+
if (plk == Kind::CONST || plk == Kind::LAMBDA)
11601162
{
11611163
handled = true;
11621164
switch (a)
@@ -1166,18 +1168,14 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
11661168
case Attr::OPAQUE:
11671169
// requires no value
11681170
break;
1169-
case Attr::REQUIRES:
1170-
val = parseExprPair();
1171-
break;
1172-
default:
1173-
handled = false;
1174-
break;
1171+
case Attr::REQUIRES: val = parseExprPair(); break;
1172+
default: handled = false; break;
11751173
}
11761174
}
11771175
else
11781176
{
11791177
// all others only allow for :list
1180-
handled = (a==Attr::LIST);
1178+
handled = (a == Attr::LIST);
11811179
}
11821180
}
11831181
break;
@@ -1484,17 +1482,15 @@ void ExprParser::processAttributeMaps(const std::map<ExprValue*, AttrMap>& amap)
14841482
Attr ck = Attr::NONE;
14851483
Expr cons;
14861484
processAttributeMap(as.second, ck, cons);
1487-
if (ck!=Attr::NONE)
1485+
if (ck != Attr::NONE)
14881486
{
14891487
Expr v(as.first);
14901488
d_state.markConstructorKind(v, ck, cons);
14911489
}
14921490
}
14931491
}
14941492

1495-
void ExprParser::processAttributeMap(const AttrMap& attrs,
1496-
Attr& ck,
1497-
Expr& cons)
1493+
void ExprParser::processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons)
14981494
{
14991495
ck = Attr::NONE;
15001496
for (const std::pair<const Attr, std::vector<Expr>>& a : attrs)

‎src/expr_parser.h‎

Lines changed: 17 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ class ExprParser
4848
* ((<symbol> <sort>)*) All variables marked
4949
* :implicit that were parsed and not added to the return value of this
5050
* method.
51-
*
51+
*
5252
* @param k The category of the parameter list:
5353
* - CONST if this is a parameter list of declare-paramaterized-const
5454
* - LAMBDA if this is the parameter list of a define command.
@@ -61,8 +61,8 @@ class ExprParser
6161
/**
6262
* Same as above, but tracks attributes.
6363
*/
64-
std::vector<Expr> parseAndBindSortedVarList(Kind k,
65-
std::map<ExprValue*, AttrMap>& amap);
64+
std::vector<Expr> parseAndBindSortedVarList(
65+
Kind k, std::map<ExprValue*, AttrMap>& amap);
6666
/**
6767
* Parse and bind a let list, i.e. ((x1 t1) ... (xn tn)), where x1...xn are
6868
* symbols to bind to terms t1...tn.
@@ -115,11 +115,11 @@ class ExprParser
115115
* string when `unescape` is set to true.
116116
*/
117117
std::string parseStr(bool unescape);
118-
118+
119119
/**
120120
* Parse attribute list
121121
* <attr_1> ... <attr_n>
122-
*
122+
*
123123
* @param k The category of expression we are applying attributes to which is:
124124
* - PARAM if applied to a parameter,
125125
* - PROOF_RULE if applied to the symbol introduced by a declare-rule command,
@@ -134,10 +134,17 @@ class ExprParser
134134
* @param plk If k is PARAM, this is the category of the parameter list
135135
* which that parameter belongs to
136136
*/
137-
void parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope, Kind plk = Kind::NONE);
137+
void parseAttributeList(Kind k,
138+
Expr& e,
139+
AttrMap& attrs,
140+
bool& pushedScope,
141+
Kind plk = Kind::NONE);
138142
/** Same as above, but ensures we pop the scope */
139-
void parseAttributeList(Kind k, Expr& e, AttrMap& attrs, Kind plk = Kind::NONE);
140-
143+
void parseAttributeList(Kind k,
144+
Expr& e,
145+
AttrMap& attrs,
146+
Kind plk = Kind::NONE);
147+
141148
/**
142149
* Parse literal kind.
143150
*/
@@ -178,9 +185,8 @@ class ExprParser
178185
* @param ck The constructor kind contained in attrs.
179186
* @param cons The corresponding constructor with ck.
180187
*/
181-
void processAttributeMap(const AttrMap& attrs,
182-
Attr& ck,
183-
Expr& cons);
188+
void processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons);
189+
184190
protected:
185191
/**
186192
* Parse constructor definition list, add to declaration type. The expected

0 commit comments

Comments
 (0)