Skip to content

Commit 88a2bc8

Browse files
ajreynolajreynol
committed
Add eo::eq and eo::is_ok
1 parent c5ea014 commit 88a2bc8

3 files changed

Lines changed: 58 additions & 68 deletions

File tree

‎src/kind.cpp‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
5151
case Kind::BINARY: o << "BINARY"; break;
5252
case Kind::STRING: o << "STRING"; break;
5353
// operations on literals
54+
case Kind::EVAL_IS_OK: o << "EVAL_IS_OK"; break;
5455
case Kind::EVAL_IS_EQ: o << "EVAL_IS_EQ"; break;
5556
case Kind::EVAL_IF_THEN_ELSE: o << "EVAL_IF_THEN_ELSE"; break;
5657
case Kind::EVAL_REQUIRES: o << "EVAL_REQUIRES"; break;
@@ -65,6 +66,8 @@ std::ostream& operator<<(std::ostream& o, Kind k)
6566
case Kind::EVAL_IS_STR: o << "EVAL_IS_STR"; break;
6667
case Kind::EVAL_IS_BOOL: o << "EVAL_IS_BOOL"; break;
6768
case Kind::EVAL_IS_VAR: o << "EVAL_IS_VAR"; break;
69+
// equality
70+
case Kind::EVAL_EQ: o << "EVAL_EQ";break;
6871
// lists
6972
case Kind::EVAL_NIL: o << "EVAL_NIL";break;
7073
case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
@@ -134,6 +137,7 @@ std::string kindToTerm(Kind k)
134137
ss << "eo::";
135138
switch (k)
136139
{
140+
case Kind::EVAL_IS_OK: ss << "is_ok"; break;
137141
case Kind::EVAL_IS_EQ: ss << "is_eq"; break;
138142
case Kind::EVAL_IF_THEN_ELSE: ss << "ite"; break;
139143
case Kind::EVAL_REQUIRES: ss << "requires"; break;
@@ -148,6 +152,8 @@ std::string kindToTerm(Kind k)
148152
case Kind::EVAL_IS_STR: ss << "is_str"; break;
149153
case Kind::EVAL_IS_BOOL: ss << "is_bool"; break;
150154
case Kind::EVAL_IS_VAR: ss << "is_var"; break;
155+
// equality
156+
case Kind::EVAL_EQ: ss << "eq"; break;
151157
// lists
152158
case Kind::EVAL_NIL: ss << "nil"; break;
153159
case Kind::EVAL_CONS: ss << "cons"; break;
@@ -227,6 +233,7 @@ bool isLiteralOp(Kind k)
227233
{
228234
switch(k)
229235
{
236+
case Kind::EVAL_IS_OK:
230237
case Kind::EVAL_IS_EQ:
231238
case Kind::EVAL_IF_THEN_ELSE:
232239
case Kind::EVAL_REQUIRES:
@@ -241,6 +248,8 @@ bool isLiteralOp(Kind k)
241248
case Kind::EVAL_IS_STR:
242249
case Kind::EVAL_IS_BOOL:
243250
case Kind::EVAL_IS_VAR:
251+
// equality
252+
case Kind::EVAL_EQ:
244253
// lists
245254
case Kind::EVAL_NIL:
246255
case Kind::EVAL_CONS:

‎src/kind.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ enum class Kind
6262

6363
// operations on literals
6464
// core
65+
EVAL_IS_OK,
6566
EVAL_IS_EQ,
6667
EVAL_IF_THEN_ELSE,
6768
EVAL_REQUIRES,
@@ -70,12 +71,15 @@ enum class Kind
7071
EVAL_TYPE_OF,
7172
EVAL_NAME_OF,
7273
EVAL_COMPARE,
74+
// testers
7375
EVAL_IS_Z,
7476
EVAL_IS_Q,
7577
EVAL_IS_BIN,
7678
EVAL_IS_STR,
7779
EVAL_IS_BOOL,
7880
EVAL_IS_VAR,
81+
// equality
82+
EVAL_EQ,
7983
// lists
8084
EVAL_NIL,
8185
EVAL_CONS,

‎src/type_checker.cpp‎

Lines changed: 45 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
141141
{
142142
case Kind::EVAL_IS_EQ:
143143
case Kind::EVAL_VAR:
144+
case Kind::EVAL_EQ:
144145
case Kind::EVAL_INT_DIV:
145146
case Kind::EVAL_INT_MOD:
146147
case Kind::EVAL_RAT_DIV:
@@ -163,6 +164,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
163164
ret = (nargs>=3);
164165
break;
165166
case Kind::PROOF_TYPE:
167+
case Kind::EVAL_IS_OK:
166168
case Kind::EVAL_TYPE_OF:
167169
case Kind::EVAL_NAME_OF:
168170
case Kind::EVAL_HASH:
@@ -1067,37 +1069,35 @@ Expr TypeChecker::evaluateLiteralOpInternal(
10671069
{
10681070
Assert (!args.empty());
10691071
Trace("type_checker") << "EVALUATE-LIT " << k << " " << args << std::endl;
1072+
if (k==Kind::EVAL_IF_THEN_ELSE)
1073+
{
1074+
Assert (args.size()==3);
1075+
if (args[0]->getKind()==Kind::BOOLEAN)
1076+
{
1077+
const Literal* l = args[0]->asLiteral();
1078+
// eagerly evaluate even if branches are non-ground
1079+
return Expr(args[l->d_bool ? 1 : 2]);
1080+
}
1081+
// note that we do not simplify based on the branches being equal
1082+
return d_null;
1083+
}
1084+
if (!isGround(args))
1085+
{
1086+
Trace("type_checker") << "...does not evaluate (non-ground)" << std::endl;
1087+
return d_null;
1088+
}
10701089
switch (k)
10711090
{
1072-
case Kind::EVAL_IS_EQ:
1091+
case Kind::EVAL_IS_OK:
10731092
{
1074-
Assert (args.size()==2);
1075-
bool ret = args[0]==args[1];
1076-
if (ret)
1077-
{
1078-
// eagerly evaluate if sides are equal, even if non-ground
1079-
return d_state.mkTrue();
1080-
}
1081-
else if (isGround(args))
1082-
{
1083-
// otherwise, if both sides are ground, we evaluate to false.
1084-
// note this is independent of whether they are values.
1085-
return d_state.mkFalse();
1086-
}
1087-
return d_null;
1093+
Assert (args.size()==1);
1094+
return args[0]->isEvaluatable() ? d_state.mkTrue() : d_state.mkFalse();
10881095
}
10891096
break;
1090-
case Kind::EVAL_IF_THEN_ELSE:
1097+
case Kind::EVAL_IS_EQ:
10911098
{
1092-
Assert (args.size()==3);
1093-
if (args[0]->getKind()==Kind::BOOLEAN)
1094-
{
1095-
const Literal* l = args[0]->asLiteral();
1096-
// eagerly evaluate even if branches are non-ground
1097-
return Expr(args[l->d_bool ? 1 : 2]);
1098-
}
1099-
// note that we do not simplify based on the branches being equal
1100-
return d_null;
1099+
Assert (args.size()==2);
1100+
return !args[0]->isEvaluatable() && !args[1]->isEvaluatable()() && args[0]==args[1];
11011101
}
11021102
break;
11031103
case Kind::EVAL_REQUIRES:
@@ -1120,25 +1120,18 @@ Expr TypeChecker::evaluateLiteralOpInternal(
11201120
break;
11211121
case Kind::EVAL_HASH:
11221122
{
1123-
if (args[0]->isGround())
1124-
{
1125-
size_t h = d_state.getHash(args[0]);
1126-
Literal lh(Integer(static_cast<unsigned int>(h)));
1127-
return Expr(d_state.mkLiteralInternal(lh));
1128-
}
1129-
return d_null;
1123+
Assert (args.size()==1);
1124+
size_t h = d_state.getHash(args[0]);
1125+
Literal lh(Integer(static_cast<unsigned int>(h)));
1126+
return Expr(d_state.mkLiteralInternal(lh));
11301127
}
11311128
break;
11321129
case Kind::EVAL_COMPARE:
11331130
{
1134-
if (args[0]->isGround() && args[1]->isGround())
1135-
{
1136-
size_t h1 = d_state.getHash(args[0]);
1137-
size_t h2 = d_state.getHash(args[1]);
1138-
Literal lb(h1>h2);
1139-
return Expr(d_state.mkLiteralInternal(lb));
1140-
}
1141-
return d_null;
1131+
size_t h1 = d_state.getHash(args[0]);
1132+
size_t h2 = d_state.getHash(args[1]);
1133+
Literal lb(h1>h2);
1134+
return Expr(d_state.mkLiteralInternal(lb));
11421135
}
11431136
break;
11441137
case Kind::EVAL_IS_Z:
@@ -1148,10 +1141,7 @@ Expr TypeChecker::evaluateLiteralOpInternal(
11481141
case Kind::EVAL_IS_BOOL:
11491142
case Kind::EVAL_IS_VAR:
11501143
{
1151-
if (!args[0]->isGround())
1152-
{
1153-
return d_null;
1154-
}
1144+
Assert (args.size()==1);
11551145
Kind kk;
11561146
switch (k)
11571147
{
@@ -1171,39 +1161,31 @@ Expr TypeChecker::evaluateLiteralOpInternal(
11711161
case Kind::EVAL_TYPE_OF:
11721162
{
11731163
// get the type if ground
1174-
if (isGround(args))
1164+
Expr e(args[0]);
1165+
Expr et = getType(e);
1166+
if (et.isGround())
11751167
{
1176-
Expr e(args[0]);
1177-
Expr et = getType(e);
1178-
if (et.isGround())
1179-
{
1180-
// don't permit ground evaluatable types
1181-
Assert (!et.isEvaluatable());
1182-
return et;
1183-
}
1168+
// don't permit ground evaluatable types
1169+
Assert (!et.isEvaluatable());
1170+
return et;
11841171
}
11851172
return d_null;
11861173
}
11871174
break;
11881175
case Kind::EVAL_NAME_OF:
11891176
{
1190-
// get the type if ground
1191-
if (isGround(args))
1177+
Kind k = args[0]->getKind();
1178+
if (k==Kind::CONST || k==Kind::VARIABLE)
11921179
{
1193-
Kind k = args[0]->getKind();
1194-
if (k==Kind::CONST || k==Kind::VARIABLE)
1195-
{
1196-
Literal sym(String(Expr(args[0]).getSymbol()));
1197-
return Expr(d_state.mkLiteralInternal(sym));
1198-
}
1180+
Literal sym(String(Expr(args[0]).getSymbol()));
1181+
return Expr(d_state.mkLiteralInternal(sym));
11991182
}
1200-
return d_null;
12011183
}
12021184
break;
12031185
case Kind::EVAL_VAR:
12041186
{
12051187
// if arguments are ground and the first argument is a string
1206-
if (args[0]->getKind()==Kind::STRING && args[1]->isGround())
1188+
if (args[0]->getKind()==Kind::STRING)
12071189
{
12081190
Expr type(args[1]);
12091191
Expr tt = getType(type);
@@ -1282,11 +1264,6 @@ Expr TypeChecker::evaluateLiteralOpInternal(
12821264
default:
12831265
break;
12841266
}
1285-
if (!isGround(args))
1286-
{
1287-
Trace("type_checker") << "...does not evaluate (non-ground)" << std::endl;
1288-
return d_null;
1289-
}
12901267
// convert argument expressions to literals
12911268
std::vector<const Literal*> lits;
12921269
bool allValues = true;

0 commit comments

Comments
 (0)