diff options
Diffstat (limited to 'proofs/lfsc_checker/check.cpp')
| -rw-r--r-- | proofs/lfsc_checker/check.cpp | 1383 |
1 files changed, 1383 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp new file mode 100644 index 000000000..8ef114115 --- /dev/null +++ b/proofs/lfsc_checker/check.cpp @@ -0,0 +1,1383 @@ +#include "position.h" +#include "check.h" +#include "code.h" +#include "expr.h" +#include "trie.h" +#include "sccwriter.h" +#include "libwriter.h" +#ifndef _MSC_VER +#include <libgen.h> +#endif +#include <stack> +#include <string.h> +#include <time.h> +#include "scccode.h" +#include "print_smt2.h" + +using namespace std; +#ifndef _MSC_VER +using namespace __gnu_cxx; +#endif + +int linenum = 1; +int colnum = 1; +const char *filename = 0; +FILE *curfile = 0; + +//#define USE_HASH_MAPS + +symmap2 progs; +std::vector< Expr* > ascHoles; + +#ifdef USE_HASH_MAPS +hash_map<string, Expr *> symbols; +hash_map<string, Expr *> symbol_types; +#else +Trie<pair<Expr *, Expr *> > *symbols = new Trie<pair<Expr *, Expr *> >; +#endif + +hash_map<string, bool > imports; +std::map<SymExpr*, int > mark_map; +std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > local_sym_names; + +Expr *not_defeq1 = 0; +Expr *not_defeq2 = 0; + +bool tail_calls = true; +bool big_check = true; + +void report_error(const string &msg) { + if (filename) { + Position p(filename,linenum,colnum); + p.print(cout); + } + cout << "\n"; + cout << msg; + cout << "\n"; + if (not_defeq1 && not_defeq2) { + cout << "The following terms are not definitionally equal:\n1. "; + not_defeq1->print(cout); + cout << "\n2. "; + not_defeq2->print(cout); + } + cout.flush(); + _exit(1); +} + +Expr *call_run_code(Expr *code) { + if (dbg_prog) { + cout << "[Running "; + code->print(cout); + cout << "\n"; + } + Expr *computed_result = run_code(code); + if (dbg_prog) { + cout << "] returning "; + if (computed_result) + computed_result->print(cout); + else + cout << "fail"; + cout << "\n"; + } + return computed_result; +} + +char our_getc_c = 0; + +int IDBUF_LEN = 2048; +char idbuf[2048]; + +Expr *statType = new CExpr(TYPE, 0); +Expr *statKind = new CExpr(KIND, 0); +Expr *statMpz = new CExpr(MPZ,0); +Expr *statMpq = new CExpr(MPQ,0); + +int open_parens = 0; + +// only call in check() +void eat_rparen() { + eat_char(')'); + open_parens--; +} + +void eat_excess(int prev) { + while(open_parens > prev) + eat_rparen(); +} + +/* There are four cases for check(): + +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. + +3. expected is non-null, create is false: check returns NULL. + +4. expected is non-null, create is true: check returns the term that + was checked. + +We consume the reference for expected, to enable tail calls in the +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; + +Expr *check(bool create, Expr *expected, Expr **computed = NULL, + bool *is_hole = 0, bool return_pos = false, bool inAsc = false ) { + start_check: + //std::cout << "check code "; + //if( expected ) + // expected->print( std::cout ); + //std::cout << std::endl; + char d = non_ws(); + switch(d) { + case '(': { + + open_parens++; + + char c = non_ws(); + switch (c) { + case EOF: + report_error("Unexpected end of file."); + break; + case '!': { // the pi case + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + Expr *sym = new SymSExpr(id,SYMS_EXPR); +#else + Expr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + allow_run = true; + int prevo = open_parens; + Expr *domain = check(true, statType); + eat_excess(prevo); + allow_run = false; +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = domain; +#else + pair<Expr *,Expr *>prev = + symbols->insert(id.c_str(),pair<Expr *,Expr *>(sym,domain)); +#endif + if (expected) + expected->inc(); + Expr *range = check(create, expected, computed, NULL, return_pos); + eat_excess(prevo); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(),prev); +#endif + if (expected) { + int o = expected->followDefs()->getop(); + expected->dec(); + if (o != TYPE && o != KIND) + report_error(string("The expected classifier for a pi abstraction") + +string("is neither \"type\" nor \"kind\".\n") + +string("1. the expected classifier: ") + +expected->toString()); + if (create){ + CExpr* ret = new CExpr(PI, sym, domain, range); + ret->calc_free_in(); + return ret; + } + return 0; + } + else { + if (create){ + CExpr* ret = new CExpr(PI, sym, domain, range); + ret->calc_free_in(); + return ret; + } + int o = (*computed)->followDefs()->getop(); + if (o != TYPE && o != KIND) + report_error(string("The classifier for the range of a pi") + +string("abstraction is neither \"type\" nor ") + +string("\"kind\".\n1. the computed classifier: ") + +range->toString()); + return 0; + } + } + case '%': { // the case for big lambda + if (expected || create || !return_pos || !big_check) + report_error(string("Big lambda abstractions can only be used") + +string("in the return position of a \"bigcheck\"\n") + +string("command.")); + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + + int prevo = open_parens; + Expr *expected_domain = check(true, statType); + eat_excess(prevo); + +#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 = + symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain)); + Expr *prev = prevpr.first; + Expr *prevtp = prevpr.second; +#endif + expected_domain->inc(); // because we have stored it in the symbol table + + //will clean up local sym name eventually + local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) ); + if (prev) + prev->dec(); + if (prevtp) + prevtp->dec(); + create = false; + expected = NULL; + // computed unchanged + is_hole = NULL; + // return_pos unchanged + + // note we will not store the proper return type in computed. + + goto start_check; + } + + case '\\': { // the lambda case + if (!expected) + report_error(string("We are computing a type for a lambda ") + +string("abstraction, but we can only check\n") + +string("such against a type. Try inserting an ") + +string("ascription (using ':').\n")); + Expr *orig_expected = expected; + expected = expected->followDefs(); + if (expected->getop() != PI) + report_error(string("We are type-checking a lambda abstraction, but\n") + +string("the expected type is not a pi abstraction.\n") + +string("1. The expected type: ") + expected->toString()); + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + + CExpr *pitp = (CExpr *)expected; + Expr *expected_domain = pitp->kids[1]; + Expr *expected_range = pitp->kids[2]; + SymExpr *pivar = (SymExpr *)pitp->kids[0]; + if (expected_range->followDefs()->getop() == TYPE) + report_error(string("The expected classifier for a lambda abstraction") + +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 = + symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain)); + Expr *prev = prevpr.first; + Expr *prevtp = prevpr.second; +#endif + Expr *prev_pivar_val = pivar->val; + sym->inc(); + pivar->val = sym; + + expected_domain->inc(); // because we have stored it in the symbol table + expected_range->inc(); // because we will pass it to a recursive call + + if (tail_calls && big_check && return_pos && !create) { + //will clean up local sym name eventually + 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) + prev->dec(); + if (prevtp) + prevtp->dec(); + orig_expected->dec(); + create = false; + expected = expected_range; + computed = NULL; + is_hole = NULL; + // return_pos unchanged + goto start_check; + } + else { + + int prev = open_parens; + Expr *range = check(create, expected_range, NULL, NULL, return_pos); + eat_excess(prev); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(), prevpr); +#endif + expected_domain->dec(); // because removed from the symbol table now + + pivar->val = prev_pivar_val; + + orig_expected->dec(); + + sym->dec(); // the pivar->val reference + if (create) + return new CExpr(LAM, sym, range); + sym->dec(); // the symbol table reference, otherwise in the new LAM + return 0; + } + } + case '^': { // the run case + if (!allow_run || !create || !expected) + report_error(string("A run expression (operator \"^\") appears in") + +string(" a disallowed position.")); + + 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: ") + // +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()) + 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); + + progret = prog->kids[0]->get_body(); + } +#else + Expr *progret = NULL; + 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(); + } + } +#endif + /* determine expected type of the result term, and make sure + the code term is an allowed one. */ + //Expr* progret = check_code( code ); + + /* the next term cannot be a hole where run expressions are introduced. + When they are checked in applications, it can be. */ + int prev = open_parens; + if( progret ) + progret->inc(); + Expr *trm = check(true, progret); + eat_excess(prev); + eat_rparen(); + + if (expected->getop() != TYPE) + report_error(string("The expected type for a run expression is not ") + +string("\"type\".\n") + +string("1. The expected type: ")+expected->toString()); + expected->dec(); + return new CExpr(RUN, code, trm); + } + + case ':': { // the ascription case + statType->inc(); + int prev = open_parens; + Expr *tp = check(true, statType, NULL, NULL, false, true ); + eat_excess(prev); + + if (!expected) + tp->inc(); + + Expr *trm = check(create, tp, NULL, NULL, return_pos); + eat_excess(prev); + eat_rparen(); + if (expected) { + if (!expected->defeq(tp)) + report_error(string("The expected type does not match the ") + +string("ascribed type in an ascription.\n") + +string("1. The expected type: ")+expected->toString() + +string("\n2. The ascribed type: ")+tp->toString()); + + // no need to dec tp, since it was consumed by the call to check + expected->dec(); + if (create) + return trm; + trm->dec(); + return 0; + } + else { + *computed = tp; + if (create) + return trm; + return 0; + } + } + case '@': { // the local definition case + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); +#endif + int prev_open = open_parens; + Expr *tp_of_trm; + Expr *trm = check(true, NULL, &tp_of_trm); + eat_excess(prev_open); + + sym->val = trm; + +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = tp_of_trm; +#else + 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) + prev->dec(); + if (prevtp) + prevtp->dec(); + // all parameters to check() unchanged here + goto start_check; + } + else { + int prev_open = open_parens; + Expr *body = check(create, expected, computed, is_hole, return_pos); + eat_excess(prev_open); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(), prevpr); +#endif + tp_of_trm->dec(); // because removed from the symbol table now + + sym->dec(); + return body; + } + } + case '~': { + int prev = open_parens; + Expr *e = check(create, expected, computed, is_hole, return_pos); + eat_excess(prev); + eat_rparen(); + + // this has been only very lightly tested -- ads. + + if (expected) { + if (expected != statMpz && expected != statMpq) + report_error("Negative sign where an numeric expression is expected."); + } + else { + if ((*computed) != statMpz && (*computed) != statMpq) + report_error("Negative sign where an numeric expression is expected."); + } + + if (create) { + if (e->getclass() == INT_EXPR) + { + IntExpr *ee = (IntExpr *)e; + mpz_neg(ee->n, ee->n); + return ee; + } + else if( e->getclass() == RAT_EXPR ) + { + RatExpr *ee = (RatExpr *)e; + mpq_neg(ee->n, ee->n); + return ee; + } + else + { + report_error("Negative sign with expr that is not an int. literal."); + } + } + else + return 0; + } + default: { // the application case + our_ungetc(c); + Expr *head_computed; + int prev = open_parens; + Expr *headtrm = check(create,0,&head_computed); + eat_excess(prev); + + CExpr *headtp = (CExpr *)head_computed->followDefs(); + headtp->inc(); + head_computed->dec(); + if ( headtp->cloned()) { + // we must clone + Expr *orig_headtp = headtp; + headtp = (CExpr *)headtp->clone(); + orig_headtp->dec(); + } + else + headtp->setcloned(); +#ifdef DEBUG_APPS + char tmp[100]; + sprintf(tmp,"(%d) ", app_rec_level++); + cout << tmp << "{ headtp = "; + headtp->debug(); +#endif + char c; + vector<HoleExpr *> holes; + vector<bool> free_holes; + while ((c = non_ws()) != ')') { + our_ungetc(c); + if (headtp->getop() != PI) + 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->toString()) + : string(""))); + SymExpr *headtp_var = (SymExpr *)headtp->kids[0]; + Expr *headtp_domain = headtp->kids[1]; + Expr *headtp_range = headtp->kids[2]; + if (headtp_domain->getop() == RUN) { + CExpr *run = (CExpr *)headtp_domain; + Expr *code = run->kids[0]; + Expr *expected_result = run->kids[1]; + Expr *computed_result = call_run_code(code); + if (!computed_result) + report_error(string("A side condition failed.\n") + +string("1. the side condition: ") + +code->toString()); + if (!expected_result->defeq(computed_result)) + report_error(string("The expected result of a side condition ") + +string("does not match the computed result.\n") + +string("1. expected result: ") + +expected_result->toString() + +string("\n2. computed result: ") + +computed_result->toString()); + computed_result->dec(); + } + else { + // check an argument + bool var_in_range = headtp->get_free_in();//headtp_range->free_in(headtp_var); + bool arg_is_hole = false; + bool consumed_arg = false; + + bool create_arg = (create || var_in_range); + + headtp_domain->inc(); + + if (tail_calls && !create_arg && headtp_range->getop() != PI) { + // we can make a tail call to check() here. + + if (expected) { + if (!expected->defeq(headtp_range)) + report_error(string("The type expected for an application ") + + string("does not match the computed type.\n") + + string("1. The expected type: ") + + expected->toString() + + string("\n2. The computed type: ") + + headtp_range->toString() + + (headtrm ? (string("\n3. the application: ") + + headtrm->toString()) + : string(""))); + expected->dec(); + } + else { + headtp_range->inc(); + *computed = headtp_range; + } + + headtp->dec(); + + // same as below + for (int i = 0, iend = holes.size(); i < iend; i++) { + if (!holes[i]->val) + /* if the hole is free in the domain, we will be filling + it in when we make our tail call, since the domain + is the expected type for the argument */ + if (!headtp_domain->free_in(holes[i])) + report_error(string("A hole was left unfilled after ") + +string("checking an application.\n")); + holes[i]->dec(); + } + + create = false; + expected = headtp_domain; + computed = NULL; + is_hole = NULL; // the argument cannot be a hole + // return_pos is unchanged + +#ifdef DEBUG_APPS + cout << "Making tail call.\n"; +#endif + + goto start_check; + } + + Expr *arg = check(create_arg, headtp_domain, NULL, &arg_is_hole); + eat_excess(prev); + if (create) { +#ifndef USE_FLAT_APP + headtrm = new CExpr(APP, headtrm, arg); +#else + headtrm = Expr::make_app( headtrm, arg ); +#endif + consumed_arg = true; + } + if (var_in_range) { + Expr *tmp = arg->followDefs(); + tmp->inc(); + headtp_var->val = tmp; + } + if (arg_is_hole) { + if (consumed_arg) + arg->inc(); + else + consumed_arg = true; // not used currently +#ifdef DEBUG_HOLES + cout << "An argument is a hole: "; + arg->debug(); +#endif + holes.push_back((HoleExpr *)arg); + } + } + headtp_range->inc(); + headtp->dec(); + headtp = (CExpr *)headtp_range; + } + open_parens--; + + // check for remaining RUN in the head's type after all the arguments + + if (headtp->getop() == PI && headtp->kids[1]->getop() == RUN) { + CExpr *run = (CExpr *)headtp->kids[1]; + Expr *code = run->kids[0]->followDefs(); + Expr *expected_result = run->kids[1]; + Expr *computed_result = call_run_code(code); + if (!computed_result) + report_error(string("A side condition failed.\n") + +string("1. the side condition: ")+code->toString()); + if (!expected_result->defeq(computed_result)) + report_error(string("The expected result of a side condition ") + +string("does not match the computed result.\n") + +string("1. expected result: ") + +expected_result->toString() + +string("\n2. computed result: ") + +computed_result->toString()); + Expr *tmp = headtp->kids[2]; + tmp->inc(); + headtp->dec(); + headtp = (CExpr *)tmp; + computed_result->dec(); + } + +#ifdef DEBUG_APPS + for (int i = 0, iend = holes.size(); i < iend; i++) { + cout << tmp << "hole "; + holes[i]->debug(); + } + cout << "}"; + app_rec_level--; +#endif + + Expr *ret = 0; + if (expected) { + if (!expected->defeq(headtp)){ + report_error(string("The type expected for an application does not") + + string(" match the computed type.(2) \n") + + string("1. The expected type: ") + + expected->toString() + + string("\n2. The computed type: ") + + headtp->toString() + + (headtrm ? (string("\n3. the application: ") + + headtrm->toString()) + : string(""))); + + } + expected->dec(); + headtp->dec(); + if (create) + ret = headtrm; + } + else { + *computed = headtp; + if (create) + ret = headtrm; + } + + /* 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){ + if( inAsc ){ +#ifdef DEBUG_HOLES + std::cout << "Ascription Hole: "; + holes[i]->print( std::cout ); + std::cout << std::endl; +#endif + ascHoles.push_back( holes[i] ); + }else{ + report_error(string("A hole was left unfilled after checking") + +string(" an application (2).\n")); + } + } + holes[i]->dec(); + } + + return ret; + + } // end application case + } + } + case EOF: + report_error("Unexpected end of file."); + break; + + case '_': + if (!is_hole) + report_error("A hole is being used in a disallowed position."); + *is_hole = true; + if (expected) + expected->dec(); + return new HoleExpr(); + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': { + our_ungetc(d); + string v; + char c; + while (isdigit(c = our_getc())) + v.push_back(c); + bool parseMpq = false; + string v2; + if( c=='/' ) + { + parseMpq = true; + v.push_back( c ); + while(isdigit(c = our_getc())) + v.push_back(c); + } + our_ungetc(c); + + + Expr *i = 0; + if (create) { + if( parseMpq ) + { + mpq_t num; + mpq_init(num); + if (mpq_set_str(num,v.c_str(),10) == -1) + report_error("Error reading a numeral."); + i = new RatExpr(num); + } + else + { + mpz_t num; + if (mpz_init_set_str(num,v.c_str(),10) == -1) + report_error("Error reading a numeral."); + i = new IntExpr(num); + } + } + + if (expected) { + if( ( !parseMpq && expected != statMpz ) || ( parseMpq && expected != statMpq ) ) + report_error(string("We parsed a numeric literal, but were ") + +string("expecting a term of a different type.\n") + +string("1. the expected type: ")+expected->toString()); + expected->dec(); + if (create) + return i; + return 0; + } + else { + if( parseMpq ) + { + statMpq->inc(); + *computed = statMpq; + if (create) + return i; + return statMpq; + } + else + { + statMpz->inc(); + *computed = statMpz; + if (create) + return i; + return statMpz; + } + } + } + default: { + our_ungetc(d); + string id(prefix_id()); +#ifdef USE_HASH_MAPS + Expr *ret = symbols[id]; + Expr *rettp = symbol_types[id]; +#else + pair<Expr *, Expr *> p = symbols->get(id.c_str()); + Expr *ret = p.first; + Expr *rettp = p.second; +#endif + if (!ret) + report_error(string("Undeclared identifier: ")+id); + if (expected) { + if (!expected->defeq(rettp)) + report_error(string("The type expected for a symbol does not") + + string(" match the symbol's type.\n") + + string("1. The symbol: ") + + id + + string("\n2. The expected type: ") + + expected->toString() + + string("\n3. The symbol's type: ") + + rettp->toString()); + expected->dec(); + if (create) { + ret->inc(); + return ret; + } + return 0; + } + else { + if( computed ){ + *computed = rettp; + (*computed)->inc(); + } + if (create) { + ret->inc(); + return ret; + } + return 0; + } + } + } + + report_error("Unexpected operator at the start of a term."); + return 0; +} + +#ifdef USE_HASH_MAPS +void discard_old_symbol(const string &id) { + Expr *tmp = symbols[id]; + if (tmp) + tmp->dec(); + tmp = symbol_types[id]; + if (tmp) + tmp->dec(); +} +#endif + +int check_time; + +void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { + int prev_linenum = linenum; + int prev_colnum = colnum; + const char *prev_filename = filename; + FILE * prev_curfile = curfile; + + // from code.h + dbg_prog = a.show_runs; + run_scc = a.run_scc; + tail_calls = !a.no_tail_calls; + + + char *f; + if (strcmp(_filename,"stdin") == 0) { + curfile = stdin; + f = strdup(_filename); + } + else { + if (prev_curfile) { + f = strdup(prev_filename); +#ifdef _MSC_VER + std::string str( f ); + for( int n=str.length(); n>=0; n-- ){ + if( str[n]=='\\' || str[n]=='/' ){ + str = str.erase( n, str.length()-n ); + break; + } + } + char *tmp = (char*)str.c_str(); +#else + char *tmp = dirname(f); +#endif + delete f; + f = new char[strlen(tmp) + 10 + strlen(_filename)]; + strcpy(f,tmp); + strcat(f,"/"); + strcat(f,_filename); + } + else + f = strdup(_filename); + curfile = fopen(f,"r"); + if (!curfile) + report_error(string("Could not open file \"") + + string(f) + + string("\" for reading.\n")); + } + + linenum = 1; + colnum = 1; + filename = f; + + char c; + while ((c = non_ws()) && c!=EOF ) { + if( c == '(' ) + { + char d; + switch ((d = non_ws())) { + case 'd': + char b; + 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; + Expr *t = check(true, 0, &ttp, NULL, true); + eat_excess(prevo); + + int o = ttp->followDefs()->getop(); + if (o == KIND) + report_error(string("Kind-level definitions are not supported.\n")); + SymSExpr *s = new SymSExpr(id); + s->val = t; +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = ttp; +#else + pair<Expr *, Expr *> prev = + symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp)); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + case 'c': {// expecting "declare" + if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' + || our_getc() != 'e') + report_error(string("Unexpected start of command.")); + + string id(prefix_id()); + Expr *ttp; + int prevo = open_parens; + Expr *t = check(true, 0, &ttp, NULL, true); + eat_excess(prevo); + + ttp = ttp->followDefs(); + if (ttp->getop() != TYPE && ttp->getop() != KIND) + report_error(string("The expression declared for \"") + +id+string("\" is neither\na type nor a kind.\n") + +string("1. The expression: ") + +t->toString() + +string("\n2. Its classifier (should be \"type\" ") + +string("or \"kind\"): ")+ttp->toString()); + ttp->dec(); + SymSExpr *s = new SymSExpr(id); +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = t; +#else + pair<Expr *, Expr *> prev = + symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,t)); + if( lw ) + lw->add_symbol( s, t ); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + default: + report_error(string("Unexpected start of command.")); + } // switch((b = our_getc())) following "de" + break; + case 'c': { + if (our_getc() != 'h' || our_getc() != 'e' || our_getc() != 'c' || our_getc() != 'k') + report_error(string("Unexpected start of command.")); + if( run_scc ){ + init_compiled_scc(); + } + Expr *computed; + big_check = true; + int prev = open_parens; + (void)check(false, 0, &computed, NULL, true); + + //print out ascription holes + for( int a=0; a<(int)ascHoles.size(); a++ ){ +#ifdef PRINT_SMT2 + print_smt2( ascHoles[a], std::cout ); +#else + ascHoles[a]->print( std::cout ); +#endif + std::cout << std::endl; + } + if( !ascHoles.empty() ) + std::cout << std::endl; + ascHoles.clear(); + + //clean up local symbols + for( int a=0; a<(int)local_sym_names.size(); a++ ){ +#ifdef USE_HASH_MAPS +#else + symbols->insert( local_sym_names[a].first.c_str(), local_sym_names[a].second ); +#endif + } + local_sym_names.clear(); + mark_map.clear(); + + eat_excess(prev); + + computed->dec(); + //cleanup(); + //exit(0); + break; + } + case 'o': { // opaque case + 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; + (void)check(false, 0, &ttp, NULL, true); + eat_excess(prevo); + + int o = ttp->followDefs()->getop(); + if (o == KIND) + report_error(string("Kind-level definitions are not supported.\n")); + SymSExpr *s = new SymSExpr(id); +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = ttp; +#else + pair<Expr *, Expr *> prev = + symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp)); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + case 'r': { // run case + if (our_getc() != 'u' || our_getc() != 'n') + report_error(string("Unexpected start of command.")); + Expr *code = read_code(); + check_code(code); + cout << "[Running-sc "; + code->print(cout); + Expr *tmp = run_code(code); + cout << "] = \n"; + if (tmp) { + tmp->print(cout); + tmp->dec(); + } + else + cout << "fail"; + cout << "\n"; + code->dec(); + break; + } + case 'p': { // program case + 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.")); + + string progstr(prefix_id()); + SymSExpr *prog = new SymSExpr(progstr); + if (progs.find(progstr) != progs.end()) + report_error(string("Redeclaring program ")+progstr+string(".")); + progs[progstr] = prog; + eat_char('('); + char d; + vector<Expr *> vars; + vector<Expr *> tps; + Expr *tmp; + while ((d = non_ws()) != ')') { + our_ungetc(d); + eat_char('('); + string varstr = prefix_id(); +#ifdef USE_HASH_MAPS + if (symbols.find(varstr) != symbols.end()) +#else + if (symbols->get(varstr.c_str()).first != NULL) +#endif + report_error(string("A program variable is already declared") + +string(" (as a constant).\n1. The variable: ") + +varstr); + Expr *var = new SymSExpr(varstr); + vars.push_back(var); + statType->inc(); + int prev = open_parens; + Expr *tp = check(true, NULL, &tmp, 0, true); + if( tp->getclass()==SYMS_EXPR ){ +#ifdef USE_HASH_MAPS + Expr *tptp = symbol_types[((SymSExpr*)tp)->s]; +#else + pair<Expr *, Expr *> p = symbols->get(((SymSExpr*)tp)->s.c_str()); + Expr *tptp = p.second; +#endif + if( !tptp->isType( statType ) ){ + report_error(string("Bad argument for side condition")); + } + }else{ + if (!tp->isDatatype()){ + report_error(string("Type for a program variable is not a ") + +string("datatype.\n1. the type: ")+tp->toString()); + } + } + eat_excess(prev); + + tps.push_back(tp); + eat_char(')'); + +#ifdef USE_HASH_MAPS + symbols[varstr] = var; + symbol_types[varstr] = tp; +#else + 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); + eat_excess(prev); + + 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--) { + vars[i]->inc(); // used below for the program code (progcode) + progtp = new CExpr(PI, vars[i], tps[i], progtp); + progtp->calc_free_in(); + } + + // just put the type here for type checking. Make sure progtp is kid 0. + 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 ){ + if( scw ){ + 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; + +#ifdef USE_HASH_MAPS + symbols[s] = NULL; + symbol_types[s] = NULL; +#else + symbols->insert(s.c_str(), pair<Expr*,Expr*>(NULL,NULL)); +#endif + } + + progtp->inc(); + prog->val->dec(); + + prog->val = progcode; + + break; + } + + default: + report_error(string("Unexpected start of command.")); + } // switch((d = non_ws()) + + eat_char(')'); + } // while + else + { + if( c != ')' ) + { + char c2[2]; + c2[1] = 0; + c2[0] = c; + string syn = string("Bad syntax (mismatched parentheses?): "); + syn.append(string(c2)); + report_error(syn); + } + } + } + free(f); + if (curfile != stdin) + fclose(curfile); + linenum = prev_linenum; + colnum = prev_colnum; + filename = prev_filename; + curfile = prev_curfile; + +} + +class Deref : public Trie<pair<Expr *, Expr *> >::Cleaner { +public: + ~Deref() {} + void clean(pair<Expr *, Expr *> p) { + Expr *tmp = p.first; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up "; + tmp->debug(); +#endif + tmp->dec(); + } + tmp = p.second; + if (tmp) { +#ifdef DEBUG + cout << " : "; + tmp->debug(); +#endif + tmp->dec(); + } +#ifdef DEBUG + cout << "\n"; +#endif + } +}; + +template <> +Trie<pair<Expr *, Expr *> >::Cleaner * +Trie<pair<Expr *, Expr *> >::cleaner = new Deref; + +void cleanup() { + symmap::iterator i, iend; +#ifdef USE_HASH_MAPS + Expr *tmp; + for (i = symbols.begin(), iend = symbols.end(); i != iend; i++) { + tmp = i->second; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up " << i->first << " : "; + tmp->debug(); +#endif + tmp->dec(); + } + } + for (i = symbol_types.begin(), iend = symbol_types.end(); i != iend; i++) { + tmp = i->second; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up " << i->first << " : "; + tmp->debug(); +#endif + tmp->dec(); + } + } +#else + delete symbols; +#endif + + // clean up programs + + symmap2::iterator j, jend; + for (j = progs.begin(), jend = progs.end(); j != jend; j++) { + SymExpr *p = j->second; + if (p) { + Expr *progcode = p->val; + p->val = NULL; + progcode->dec(); + p->dec(); + } + } +} + +void init() { +#ifdef USE_HASH_MAPS + string tp("type"); + symbols[tp] = statType; + symbol_types[tp] = statKind; + string mpz("mpz"); + symbols[mpz] = statMpz; + symbol_types[mpz] = statType; + statType->inc(); + sym +#else + 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)); +#endif +} |