summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/lfsc_checker/check.cpp124
-rw-r--r--proofs/lfsc_checker/code.cpp154
-rw-r--r--proofs/lfsc_checker/expr.cpp7
-rwxr-xr-xproofs/signatures/ex-mem.plf68
4 files changed, 217 insertions, 136 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 8ef114115..b550c58a1 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -101,7 +101,7 @@ void eat_rparen() {
}
void eat_excess(int prev) {
- while(open_parens > prev)
+ while(open_parens > prev)
eat_rparen();
}
@@ -110,8 +110,8 @@ void eat_excess(int prev) {
1. expected=0, create is false: check() sets computed to be the classifier of
the checked term.
-2. expected=0, create is true: check() returns
- the checked expression and sets computed to be its classifier.
+2. expected=0, create is true: check() returns
+ the checked expression and sets computed to be its classifier.
3. expected is non-null, create is false: check returns NULL.
@@ -119,14 +119,14 @@ void eat_excess(int prev) {
was checked.
We consume the reference for expected, to enable tail calls in the
-application case.
+application case.
If is_hole is NULL, then the expression parsed may not be a hole.
Otherwise, it may be, and we will set *is_hole to true if it is
(but leave *is_hole alone if it is not).
*/
-
+
bool allow_run = false;
int app_rec_level = 0;
@@ -143,7 +143,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
open_parens++;
- char c = non_ws();
+ char c = non_ws();
switch (c) {
case EOF:
report_error("Unexpected end of file.");
@@ -190,7 +190,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
+string("is neither \"type\" nor \"kind\".\n")
+string("1. the expected classifier: ")
+expected->toString());
- if (create){
+ if (create){
CExpr* ret = new CExpr(PI, sym, domain, range);
ret->calc_free_in();
return ret;
@@ -198,7 +198,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
return 0;
}
else {
- if (create){
+ if (create){
CExpr* ret = new CExpr(PI, sym, domain, range);
ret->calc_free_in();
return ret;
@@ -235,7 +235,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
symbols[id] = sym;
symbol_types[id] = expected_domain;
#else
- pair<Expr *, Expr *> prevpr =
+ pair<Expr *, Expr *> prevpr =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
Expr *prev = prevpr.first;
Expr *prevtp = prevpr.second;
@@ -244,7 +244,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
//will clean up local sym name eventually
local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
- if (prev)
+ if (prev)
prev->dec();
if (prevtp)
prevtp->dec();
@@ -288,21 +288,21 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
+string(" a kind, not a type.\n")
+string("1. The expected classifier: ")
+expected->toString());
-
+
/* we need to map the pivar to the new sym, because in our
higher-order matching we may have (_ x) to unify with t.
The x must be something from an expected type, since only these
can have holes. We want to map expected vars x to computed vars y,
so that we can set the hole to be \ y t, where t contains ys but
not xs. */
-
+
#ifdef USE_HASH_MAPS
Expr *prev = symbols[id];
Expr *prevtp = symbol_types[id];
symbols[id] = sym;
symbol_types[id] = expected_domain;
#else
- pair<Expr *, Expr *> prevpr =
+ pair<Expr *, Expr *> prevpr =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
Expr *prev = prevpr.first;
Expr *prevtp = prevpr.second;
@@ -319,7 +319,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
if (prev_pivar_val)
prev_pivar_val->dec();
- if (prev)
+ if (prev)
prev->dec();
if (prevtp)
prevtp->dec();
@@ -351,7 +351,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
orig_expected->dec();
sym->dec(); // the pivar->val reference
- if (create)
+ if (create)
return new CExpr(LAM, sym, range);
sym->dec(); // the symbol table reference, otherwise in the new LAM
return 0;
@@ -364,24 +364,24 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
Expr *code = read_code();
//string errstr = (string("The first argument in a run expression must be")
- // +string(" a call to a program.\n1. the argument: ")
+ // +string(" a call to a program.\n1. the argument: ")
// +code->toString());
/* determine expected type of the result term, and make sure
the code term is an allowed one. */
#if 0
Expr *progret;
- if (code->isArithTerm())
+ if (code->isArithTerm())
progret = statMpz;
else {
if (code->getop() != APP)
report_error(errstr);
CExpr *call = (CExpr *)code;
-
+
// prog is not known to be a SymExpr yet
CExpr *prog = (CExpr *)call->get_head();
-
+
if (prog->getop() != PROG)
report_error(errstr);
@@ -389,16 +389,16 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
}
#else
Expr *progret = NULL;
- if (code->isArithTerm())
+ if (code->isArithTerm())
progret = statMpz;
else {
if (code->getop() == APP)
{
CExpr *call = (CExpr *)code;
-
+
// prog is not known to be a SymExpr yet
CExpr *prog = (CExpr *)call->get_head();
-
+
if (prog->getop() == PROG)
progret = prog->kids[0]->get_body();
}
@@ -433,7 +433,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
if (!expected)
tp->inc();
-
+
Expr *trm = check(create, tp, NULL, NULL, return_pos);
eat_excess(prev);
eat_rparen();
@@ -478,14 +478,14 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
symbols[id] = sym;
symbol_types[id] = tp_of_trm;
#else
- pair<Expr *, Expr *> prevpr =
+ pair<Expr *, Expr *> prevpr =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,tp_of_trm));
Expr *prev = prevpr.first;
Expr *prevtp = prevpr.second;
#endif
if (tail_calls && big_check && return_pos && !create) {
- if (prev)
+ if (prev)
prev->dec();
if (prevtp)
prevtp->dec();
@@ -506,7 +506,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
#endif
tp_of_trm->dec(); // because removed from the symbol table now
- sym->dec();
+ sym->dec();
return body;
}
}
@@ -545,7 +545,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
report_error("Negative sign with expr that is not an int. literal.");
}
}
- else
+ else
return 0;
}
default: { // the application case
@@ -562,7 +562,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
// we must clone
Expr *orig_headtp = headtp;
headtp = (CExpr *)headtp->clone();
- orig_headtp->dec();
+ orig_headtp->dec();
}
else
headtp->setcloned();
@@ -578,11 +578,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
while ((c = non_ws()) != ')') {
our_ungetc(c);
if (headtp->getop() != PI)
- report_error(string("The type of an applied term is not ")
+ report_error(string("The type of an applied term is not ")
+ string("a pi-type.\n")
+ string("\n1. the type of the term: ")
+ headtp->toString()
- + (headtrm ? (string("\n2. the term: ")
+ + (headtrm ? (string("\n2. the term: ")
+ headtrm->toString())
: string("")));
SymExpr *headtp_var = (SymExpr *)headtp->kids[0];
@@ -627,7 +627,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
+ expected->toString()
+ string("\n2. The computed type: ")
+ headtp_range->toString()
- + (headtrm ? (string("\n3. the application: ")
+ + (headtrm ? (string("\n3. the application: ")
+ headtrm->toString())
: string("")));
expected->dec();
@@ -670,7 +670,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
#ifndef USE_FLAT_APP
headtrm = new CExpr(APP, headtrm, arg);
#else
+ Expr* orig_headtrm = headtrm;
headtrm = Expr::make_app( headtrm, arg );
+ if( orig_headtrm->getclass()==CEXPR ){
+ orig_headtrm->dec();
+ }
#endif
consumed_arg = true;
}
@@ -739,7 +743,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
+ expected->toString()
+ string("\n2. The computed type: ")
+ headtp->toString()
- + (headtrm ? (string("\n3. the application: ")
+ + (headtrm ? (string("\n3. the application: ")
+ headtrm->toString())
: string("")));
@@ -755,7 +759,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
ret = headtrm;
}
- /* do this check here to give the defeq() call above a
+ /* do this check here to give the defeq() call above a
chance to fill in some holes */
for (int i = 0, iend = holes.size(); i < iend; i++) {
if (!holes[i]->val){
@@ -783,7 +787,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
report_error("Unexpected end of file.");
break;
- case '_':
+ case '_':
if (!is_hole)
report_error("A hole is being used in a disallowed position.");
*is_hole = true;
@@ -803,7 +807,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
our_ungetc(d);
string v;
char c;
- while (isdigit(c = our_getc()))
+ while (isdigit(c = our_getc()))
v.push_back(c);
bool parseMpq = false;
string v2;
@@ -811,7 +815,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
{
parseMpq = true;
v.push_back( c );
- while(isdigit(c = our_getc()))
+ while(isdigit(c = our_getc()))
v.push_back(c);
}
our_ungetc(c);
@@ -916,7 +920,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
#ifdef USE_HASH_MAPS
void discard_old_symbol(const string &id) {
Expr *tmp = symbols[id];
- if (tmp)
+ if (tmp)
tmp->dec();
tmp = symbol_types[id];
if (tmp)
@@ -940,7 +944,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
char *f;
if (strcmp(_filename,"stdin") == 0) {
- curfile = stdin;
+ curfile = stdin;
f = strdup(_filename);
}
else {
@@ -967,7 +971,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
else
f = strdup(_filename);
curfile = fopen(f,"r");
- if (!curfile)
+ if (!curfile)
report_error(string("Could not open file \"")
+ string(f)
+ string("\" for reading.\n"));
@@ -985,15 +989,15 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
switch ((d = non_ws())) {
case 'd':
char b;
- if ((b = our_getc()) != 'e')
+ if ((b = our_getc()) != 'e')
report_error(string("Unexpected start of command."));
switch ((b = our_getc())) {
case 'f': {// expecting "define"
-
+
if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e')
report_error(string("Unexpected start of command."));
-
+
string id(prefix_id());
Expr *ttp;
int prevo = open_parens;
@@ -1010,7 +1014,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
symbols[id] = s;
symbol_types[id] = ttp;
#else
- pair<Expr *, Expr *> prev =
+ pair<Expr *, Expr *> prev =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
if (prev.first)
prev.first->dec();
@@ -1020,7 +1024,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
break;
}
case 'c': {// expecting "declare"
- if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r'
+ if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r'
|| our_getc() != 'e')
report_error(string("Unexpected start of command."));
@@ -1045,7 +1049,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
symbols[id] = s;
symbol_types[id] = t;
#else
- pair<Expr *, Expr *> prev =
+ pair<Expr *, Expr *> prev =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,t));
if( lw )
lw->add_symbol( s, t );
@@ -1056,7 +1060,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
#endif
break;
}
- default:
+ default:
report_error(string("Unexpected start of command."));
} // switch((b = our_getc())) following "de"
break;
@@ -1105,7 +1109,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q'
|| our_getc() != 'u' || our_getc() != 'e')
report_error(string("Unexpected start of command."));
-
+
string id(prefix_id());
Expr *ttp;
int prevo = open_parens;
@@ -1121,7 +1125,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
symbols[id] = s;
symbol_types[id] = ttp;
#else
- pair<Expr *, Expr *> prev =
+ pair<Expr *, Expr *> prev =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
if (prev.first)
prev.first->dec();
@@ -1150,7 +1154,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
break;
}
case 'p': { // program case
- if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g'
+ if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g'
|| our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm')
report_error(string("Unexpected start of command."));
@@ -1209,10 +1213,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
symbols->insert(varstr.c_str(), pair<Expr *, Expr *>(var,tp));
#endif
}
-
+
if (!vars.size())
report_error("A program lacks input variables.");
-
+
statType->inc();
int prev = open_parens;
Expr *progtp = check(true,statType,&tmp,0, true);
@@ -1221,7 +1225,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
if (!progtp->isDatatype())
report_error(string("Return type for a program is not a")
+string(" datatype.\n1. the type: ")+progtp->toString());
-
+
Expr *progcode = read_code();
for (int i = vars.size() - 1, iend = 0; i >= iend; i--) {
@@ -1231,10 +1235,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
}
// just put the type here for type checking. Make sure progtp is kid 0.
- prog->val = new CExpr(PROG, progtp);
-
+ prog->val = new CExpr(PROG, progtp);
+
check_code(progcode);
-
+
progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode);
//if compiling side condition code, give this code to the side condition code writer
if( a.compile_scc ){
@@ -1242,7 +1246,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
scw->add_scc( progstr, (CExpr*)progcode );
}
}
-
+
// remove the variables from the symbol table.
for (int i = 0, iend = vars.size(); i < iend; i++) {
string &s = ((SymSExpr *)vars[i])->s;
@@ -1263,10 +1267,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
break;
}
- default:
+ default:
report_error(string("Unexpected start of command."));
} // switch((d = non_ws())
-
+
eat_char(')');
} // while
else
@@ -1350,7 +1354,7 @@ void cleanup() {
delete symbols;
#endif
- // clean up programs
+ // clean up programs
symmap2::iterator j, jend;
for (j = progs.begin(), jend = progs.end(); j != jend; j++) {
@@ -1378,6 +1382,6 @@ void init() {
symbols->insert("type", pair<Expr *, Expr *>(statType, statKind));
statType->inc();
symbols->insert("mpz", pair<Expr *, Expr *>(statMpz, statType));
- symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType));
+ symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType));
#endif
}
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 225700580..34c6c133b 100644
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -23,7 +23,7 @@ string *eat_str(const char *str, bool check_end = true) {
our_ungetc(d);
return s;
}
-
+
delete s;
return 0;
}
@@ -76,13 +76,17 @@ Expr *read_case() {
prevs.push_back(symbols[varstr]);
symbols[varstr] = var;
#else
- prevs.push_back(symbols->insert(varstr.c_str(),
+ prevs.push_back(symbols->insert(varstr.c_str(),
pair<Expr *, Expr *>(var,NULL)));
#endif
#ifndef USE_FLAT_APP
pat = new CExpr(APP,pat,var);
#else
+ Expr* orig_pat = pat;
pat = Expr::make_app(pat,var);
+ if( orig_pat->getclass()==CEXPR ){
+ orig_pat->dec();
+ }
#endif
}
break;
@@ -101,7 +105,7 @@ Expr *read_case() {
pat = read_ctor();
break;
}
-
+
Expr *ret = read_code();
if( pat )
ret = new CExpr(CASE, pat, ret);
@@ -124,16 +128,16 @@ Expr *read_code() {
string *pref = NULL;
char d = non_ws();
switch(d) {
- case '(':
+ case '(':
{
- char c = non_ws();
- switch (c)
+ char c = non_ws();
+ switch (c)
{
- case 'd':
+ case 'd':
{
our_ungetc('d');
pref = eat_str("do");
- if (pref)
+ if (pref)
break;
Expr *ret = read_code();
while ((c = non_ws()) != ')') {
@@ -142,11 +146,11 @@ Expr *read_code() {
}
return ret;
}
- case 'f':
+ case 'f':
{
our_ungetc('f');
pref = eat_str("fail");
- if (pref)
+ if (pref)
break;
Expr *c = read_code();
@@ -156,14 +160,14 @@ Expr *read_code() {
//if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val)
// report_error(string("\"fail\" must be used with a (undefined) base ")
// +string("type.\n1. the expression used: "+c->toString()));
-
+
return new CExpr(FAIL, c);
}
- case 'l':
+ case 'l':
{
our_ungetc('l');
pref = eat_str("let");
- if (pref)
+ if (pref)
break;
string id(prefix_id());
@@ -175,12 +179,12 @@ Expr *read_code() {
Expr *prev = symbols[id];
symbols[id] = var;
#else
- pair<Expr *, Expr *> prev =
+ pair<Expr *, Expr *> prev =
symbols->insert(id.c_str(), pair<Expr *, Expr *>(var,NULL));
#endif
Expr *t2 = read_code();
-
+
#ifdef USE_HASH_MAPS
symbols[id] = prev;
#else
@@ -189,11 +193,11 @@ Expr *read_code() {
eat_char(')');
return new CExpr(LET, var, t1, t2);
}
- case 'i':
+ case 'i':
{
our_ungetc('i');
pref = eat_str("ifmarked",false);
- if (pref)
+ if (pref)
break;
#ifndef MARKVAR_32
Expr *e1 = read_code();
@@ -220,16 +224,16 @@ Expr *read_code() {
eat_char(')');
return ret;
}
- case 'm':
+ case 'm':
{
char c;
- switch ((c = our_getc()))
+ switch ((c = our_getc()))
{
- case 'a':
+ case 'a':
{
char cc;
switch ((cc = our_getc())) {
- case 't':
+ case 't':
{
our_ungetc('t');
pref = eat_str("tch");
@@ -253,7 +257,7 @@ Expr *read_code() {
}
return new CExpr(MATCH,cases);
}
- case 'r':
+ case 'r':
{
our_ungetc('r');
pref = eat_str("rkvar", false);
@@ -268,7 +272,7 @@ Expr *read_code() {
CExpr* ret = NULL;
if( index>=1 && index<=32 )
{
- ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() );
+ ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() );
}
else
{
@@ -287,7 +291,7 @@ Expr *read_code() {
break;
}
}
- case 'p':
+ case 'p':
{
our_ungetc('p');
pref = eat_str("p_",false);
@@ -297,7 +301,7 @@ Expr *read_code() {
}
char c = our_getc();
switch(c) {
- case 'a':
+ case 'a':
{
our_ungetc('a');
pref = eat_str("add");
@@ -311,7 +315,7 @@ Expr *read_code() {
eat_char(')');
return ret;
}
- case 'n':
+ case 'n':
{
our_ungetc('n');
pref = eat_str("neg");
@@ -319,12 +323,12 @@ Expr *read_code() {
pref->insert(0,"mp_");
break;
}
-
+
Expr *ret = new CExpr(NEG, read_code());
eat_char(')');
return ret;
}
- case 'i':
+ case 'i':
{ // mpz_if_neg
char c = our_getc();
if( c=='f' )
@@ -439,7 +443,7 @@ Expr *read_code() {
{
our_ungetc('c');
pref = eat_str("compare");
- if (pref)
+ if (pref)
break;
Expr *e1 = read_code();
Expr *e2 = read_code();
@@ -452,21 +456,21 @@ Expr *read_code() {
case EOF:
report_error("Unexpected end of file.");
break;
- default:
+ default:
{ // the application case
our_ungetc(c);
break;
}
}
// parse application
- if (pref)
+ if (pref)
// we have eaten part of the name of an applied identifier
pref->append(prefix_id());
else
pref = new string(prefix_id());
Expr *ret = progs[*pref];
- if (!ret)
+ if (!ret)
#ifdef USE_HASH_TABLES
ret = symbols[*pref];
#else
@@ -486,7 +490,11 @@ Expr *read_code() {
ret = new CExpr(APP,ret,read_code());
#else
Expr* ke = read_code();
+ Expr* orig_ret = ret;
ret = Expr::make_app(ret,ke);
+ if( orig_ret->getclass()==CEXPR ){
+ orig_ret->dec();
+ }
#endif
}
return ret;
@@ -494,7 +502,7 @@ Expr *read_code() {
case EOF:
report_error("Unexpected end of file.");
break;
- case '_':
+ case '_':
report_error("Holes may not be used in code.");
return NULL;
case '0':
@@ -506,19 +514,19 @@ Expr *read_code() {
case '6':
case '7':
case '8':
- case '9':
+ case '9':
{
our_ungetc(d);
string v;
char c;
- while (isdigit(c = our_getc()))
+ while (isdigit(c = our_getc()))
v.push_back(c);
bool parseMpq = false;
if( c=='/' )
{
parseMpq = true;
v.push_back(c);
- while(isdigit(c = our_getc()))
+ while(isdigit(c = our_getc()))
v.push_back(c);
}
our_ungetc(c);
@@ -540,7 +548,7 @@ Expr *read_code() {
return new IntExpr(num);
}
}
- default:
+ default:
{
our_ungetc(d);
string id(prefix_id());
@@ -550,7 +558,7 @@ Expr *read_code() {
pair<Expr *, Expr *> p = symbols->get(id.c_str());
Expr *ret = p.first;
#endif
- if (!ret)
+ if (!ret)
ret = progs[id];
if (!ret)
report_error(string("Undeclared identifier: ")+id);
@@ -609,7 +617,7 @@ Expr *check_code(Expr *_e) {
int iend = args.size();
vector<Expr *> argtps(iend);
- for (int i = 0; i < iend; i++)
+ for (int i = 0; i < iend; i++)
argtps[i] = check_code(args[i]);
#endif
@@ -623,18 +631,18 @@ Expr *check_code(Expr *_e) {
tp = symbols->get(((SymSExpr *)h)->s.c_str()).second;
#endif
}
-
+
if (!tp)
report_error(string("The head of an application is missing a type in ")
+string("code.\n1. the application: ")+e->toString());
-
+
tp = tp->followDefs();
if (tp->getop() != PI)
report_error(string("The head of an application does not have ")
+string("functional type in code.")
+string("\n1. the application: ")+e->toString());
-
+
CExpr *cur = (CExpr *)tp;
int i = 0;
while (cur->getop() == PI) {
@@ -661,7 +669,7 @@ Expr *check_code(Expr *_e) {
+ string("\n5. expected type: ")
+cur->kids[1]->toString());
}
-
+
//if (cur->kids[2]->free_in((SymExpr *)cur->kids[0]))
if( cur->get_free_in() ){
cur->calc_free_in();
@@ -682,8 +690,8 @@ Expr *check_code(Expr *_e) {
+string("arguments in code.\n")
+string("1. the application: ")+e->toString()
+string("\n2. the head's type: ")+tp->toString());
-
-
+
+
return cur;
}
//is this right?
@@ -693,7 +701,7 @@ Expr *check_code(Expr *_e) {
case MPQ:
return statType;
break;
- case DO:
+ case DO:
check_code(e->kids[0]);
return check_code(e->kids[1]);
@@ -706,22 +714,22 @@ Expr *check_code(Expr *_e) {
Expr *prevtp = symbol_types[var->s];
symbol_types[var->s] = tp1;
#else
- pair<Expr *, Expr *> prev =
+ pair<Expr *, Expr *> prev =
symbols->insert(var->s.c_str(), pair<Expr *, Expr *>(NULL,tp1));
#endif
Expr *tp2 = check_code(e->kids[2]);
-
+
#ifdef USE_HASH_MAPS
symbol_types[var->s] = prevtp;
#else
symbols->insert(var->s.c_str(), prev);
#endif
-
+
return tp2;
}
- case ADD:
+ case ADD:
case MUL:
case DIV:
{
@@ -732,14 +740,14 @@ Expr *check_code(Expr *_e) {
report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n")
+string("1. the argument: ")+e->kids[0]->toString()
+string("\n1. its type: ")+tp0->toString());
-
+
if (tp0 != tp1)
report_error(string("Arguments to mp_[arith] have differing types.\n")
+string("1. argument 1: ")+e->kids[0]->toString()
+string("\n1. its type: ")+tp0->toString()
+string("2. argument 2: ")+e->kids[1]->toString()
+string("\n2. its type: ")+tp1->toString());
-
+
return tp0;
}
@@ -749,18 +757,18 @@ Expr *check_code(Expr *_e) {
report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n")
+string("1. the argument: ")+e->kids[0]->toString()
+string("\n1. its type: ")+tp0->toString());
-
+
return tp0;
}
- case IFNEG:
+ case IFNEG:
case IFZERO: {
Expr *tp0 = check_code(e->kids[0]);
if (tp0 != statMpz && tp0 != statMpq)
report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n")
+string("1. the argument: ")+e->kids[0]->toString()
+string("\n1. its type: ")+tp0->toString());
-
+
SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]);
SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]);
if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2)
@@ -785,7 +793,7 @@ Expr *check_code(Expr *_e) {
}
case MARKVAR: {
SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
-
+
Expr* tptp = NULL;
if (tp->getclass() == SYMS_EXPR && !tp->val){
@@ -808,12 +816,12 @@ Expr *check_code(Expr *_e) {
return tp;
}
- case IFMARKED:
+ case IFMARKED:
{
SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
Expr* tptp = NULL;
-
+
if (tp->getclass() == SYMS_EXPR && !tp->val){
#ifdef USE_HASH_MAPS
tptp = symbol_types[tp->s];
@@ -821,7 +829,7 @@ Expr *check_code(Expr *_e) {
tptp = symbols->get(tp->s.c_str()).second;
#endif
}
-
+
if (!tptp->isType( statType ) ){
string errstr = (string("\"ifmarked\" is used with an expression which ")
+string("cannot be a lambda-bound variable.\n")
@@ -877,7 +885,7 @@ Expr *check_code(Expr *_e) {
+string("\n4. second expression's type: ")+tp3->toString());
return tp2;
}
- case MATCH:
+ case MATCH:
{
SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]);
Expr *tptp = NULL;
@@ -905,14 +913,14 @@ Expr *check_code(Expr *_e) {
while ((c_or_default = *cur++)) {
Expr *tp = NULL;
CExpr *pat = NULL;
- if (c_or_default->getop() != CASE)
+ if (c_or_default->getop() != CASE)
// this is the default of the MATCH
tp = check_code(c_or_default);
else {
// this is a CASE of the MATCH
c = (CExpr *)c_or_default;
pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR
- if (pat->getclass() == SYMS_EXPR)
+ if (pat->getclass() == SYMS_EXPR)
tp = check_code(c->kids[1]);
else {
// extend type context and then check the body of the case
@@ -941,7 +949,7 @@ Expr *check_code(Expr *_e) {
symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1];
#else
prevs.push_back
- (symbols->insert(((SymSExpr *)vars[i])->s.c_str(),
+ (symbols->insert(((SymSExpr *)vars[i])->s.c_str(),
pair<Expr *, Expr *>(NULL,
((CExpr *)(curtp->followDefs()))->kids[1])));
#endif
@@ -949,7 +957,7 @@ Expr *check_code(Expr *_e) {
}
tp = check_code(c->kids[1]);
-
+
for (int i = 0, iend = prevs.size(); i < iend; i++) {
#ifdef USE_HASH_MAPS
symbol_types[((SymSExpr *)vars[i])->s] = prevs[i];
@@ -974,13 +982,13 @@ Expr *check_code(Expr *_e) {
: (string("\n2. type for the body of case for ")
+pat->toString()))
+string(": ")+tp->toString());
-
+
}
return mtp;
}
} // end switch
-
+
report_error("Type checking an unrecognized form of code (internal error).");
return NULL;
}
@@ -1013,12 +1021,12 @@ Expr *run_code(Expr *_e) {
return e;
case HOLE_EXPR: {
Expr *tmp = e->followDefs();
- if (tmp == e)
+ if (tmp == e)
report_error("Encountered an unfilled hole running code.");
tmp->inc();
return tmp;
}
- case SYMS_EXPR:
+ case SYMS_EXPR:
case SYM_EXPR: {
Expr *tmp = e->followDefs();
//std::cout << "follow def = ";
@@ -1054,7 +1062,7 @@ Expr *run_code(Expr *_e) {
r0->dec();
return r1;
}
- case ADD:
+ case ADD:
case MUL:
case DIV:
{
@@ -1127,7 +1135,7 @@ Expr *run_code(Expr *_e) {
return NULL;
}
}
- case IFNEG:
+ case IFNEG:
case IFZERO:{
Expr *r1 = run_code(e->kids[0]);
if (!r1)
@@ -1142,7 +1150,7 @@ Expr *run_code(Expr *_e) {
}else if( r1->getclass() == RAT_EXPR ){
if( e->getop() == IFNEG )
cond = mpq_sgn( ((RatExpr *)r1)->n )<0;
- else if( e->getop() == IFZERO )
+ else if( e->getop() == IFZERO )
cond = mpq_sgn( ((RatExpr *)r1)->n )==0;
}
else
@@ -1203,7 +1211,7 @@ Expr *run_code(Expr *_e) {
_e = e->kids[2];
goto start_run_code;
}
- //else
+ //else
r2->dec();
_e = e->kids[3];
goto start_run_code;
@@ -1283,7 +1291,7 @@ Expr *run_code(Expr *_e) {
vector<Expr *> args;
Expr *hd = e->collect_args(args);
- for (int i = 0, iend = args.size(); i < iend; i++)
+ for (int i = 0, iend = args.size(); i < iend; i++)
if (!(args[i] = run_code(args[i]))) {
for (int j = 0; j < i; j++)
args[j]->dec();
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 7ffc6469a..ae0e49531 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -234,6 +234,7 @@ Expr* Expr::make_app(Expr* e1, Expr* e2 )
counter = 0;
while( ((CExpr*)e1)->kids[counter] ){
ret->kids[counter] = ((CExpr*)e1)->kids[counter];
+ ret->kids[counter]->inc();
counter++;
}
ret->kids[counter] = e2;
@@ -346,8 +347,8 @@ Expr* CExpr::convert_to_tree_app( Expr* e )
if( e->getop()==APP )
{
std::vector< Expr* > kds;
- int counter = 1;
- while( ((CExpr*)e)->kids[counter] )
+ int counter = 1;
+ while( ((CExpr*)e)->kids[counter] )
{
kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) );
counter++;
@@ -963,4 +964,4 @@ void SymExpr::smark( int m )
{
mark_map[this] = m;
}
-#endif \ No newline at end of file
+#endif
diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf
new file mode 100755
index 000000000..12c4c3e16
--- /dev/null
+++ b/proofs/signatures/ex-mem.plf
@@ -0,0 +1,68 @@
+; AJR : proof used for testing memory use of theory lemmas
+
+(check
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b a))
+(% A3 (th_holds (not (= s a a)))
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b a) (\ v2 (\ a2
+(decl_atom (= s a a) (\ v3 (\ a3
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT2
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT3
+;...add copies here...
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+ (contra _ A1 l1)
+))) (\ C1
+; C1 is the clause ( v1 )
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+ (contra _ A2 l2)
+))) (\ C2
+; C2 is the clause ( v2 )
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(clausify_false
+ (contra _ l3 A3)
+))) (\ C3
+; C3 is the clause ( ~v3 )
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _
+(R _ _ C2
+(R _ _ C1 CT1 v1) v2) C3 v3)
+
+(\ x x))
+
+)))))))))))))))))))))))))))))
+))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback