summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/expr.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/lfsc_checker/expr.cpp')
-rw-r--r--proofs/lfsc_checker/expr.cpp966
1 files changed, 966 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
new file mode 100644
index 000000000..7ffc6469a
--- /dev/null
+++ b/proofs/lfsc_checker/expr.cpp
@@ -0,0 +1,966 @@
+#include "expr.h"
+#include <stdlib.h>
+#include <sstream>
+#ifdef _MSC_VER
+#include <algorithm>
+#endif
+#include "check.h"
+
+using namespace std;
+
+int HoleExpr::next_id = 0;
+int Expr::markedCount = 0;
+
+C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768);
+
+//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768);
+
+#define USE_HOLE_PATH_COMPRESSION
+
+void Expr::debug() {
+ print(cout);
+ /*
+ cout << "\nAt " << this << "\n";
+ cout << "marked = " << getmark() << "\n";
+ */
+ cout << "\n";
+ cout.flush();
+}
+
+bool destroy_progs = false;
+
+#define destroydec(rr) \
+ do { \
+ Expr *r = rr; \
+ int ref = r->data >> 9; \
+ ref = ref - 1; \
+ r->debugrefcnt(ref,DEC); \
+ if (ref == 0) { \
+ _e = r; \
+ goto start_destroy; \
+ } \
+ else \
+ r->data = (ref << 9) | (r->data & 511); \
+ } while(0)
+
+
+void Expr::destroy(Expr *_e, bool dec_kids) {
+ start_destroy:
+ switch (_e->getclass()) {
+ case INT_EXPR:
+ delete (IntExpr *)_e;
+ break;
+ case SYMS_EXPR: {
+ SymSExpr *e = (SymSExpr *)_e;
+ if (e->val && e->val->getop() != PROG) {
+ Expr *tmp = e->val;
+ delete e;
+ destroydec(tmp);
+ }
+ else
+ delete e;
+ break;
+ }
+ case SYM_EXPR: {
+ SymExpr *e = (SymExpr *)_e;
+ if (e->val && e->val->getop() != PROG) {
+ Expr *tmp = e->val;
+ delete e;
+ destroydec(tmp);
+ }
+ else
+ delete e;
+ break;
+ }
+ case HOLE_EXPR: {
+ HoleExpr *e = (HoleExpr *)_e;
+ if (e->val) {
+ Expr *tmp = e->val;
+ delete e;
+ destroydec(tmp);
+ }
+ else
+ delete e;
+ break;
+ }
+ case CEXPR: {
+ CExpr *e = (CExpr *)_e;
+ if (dec_kids) {
+ Expr **cur = e->kids;
+ Expr *tmp;
+ while((tmp = *cur++)) {
+ if (*cur)
+ tmp->dec();
+ else {
+ delete e;
+ destroydec(tmp);
+ break;
+ }
+ }
+ }
+ else
+ delete e;
+ break;
+ }
+ }
+}
+
+Expr *Expr::clone() {
+ switch (getclass()) {
+ case INT_EXPR:
+ case RAT_EXPR:
+ inc();
+ return this;
+ case SYMS_EXPR:
+ case SYM_EXPR: {
+ SymExpr *e = (SymExpr *)this;
+ if (e->val)
+ if (e->val->getop() != PROG)
+ return e->val->clone();
+ e->inc();
+ return e;
+ }
+ case HOLE_EXPR: {
+ HoleExpr *e = (HoleExpr *)this;
+ if (e->val)
+ return e->val->clone();
+ e->inc();
+ return e;
+ }
+ case CEXPR: {
+ CExpr *e = (CExpr *)this;
+ int op = e->getop();
+ switch(op) {
+ case LAM: {
+#ifdef DEBUG_SYM_NAMES
+ SymSExpr *var = (SymSExpr *)e->kids[0];
+ SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
+#else
+ SymExpr *var = (SymExpr *)e->kids[0];
+ SymExpr *newvar = new SymExpr(*var);
+#endif
+ Expr *prev = var->val;
+ var->val = newvar;
+ Expr *bod = e->kids[1]->clone();
+ var->val = prev;
+ return new CExpr(LAM,newvar,bod);
+ }
+ case PI: {
+#ifdef DEBUG_SYM_NAMES
+ SymSExpr *var = (SymSExpr *)e->kids[0];
+ SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
+#else
+ SymExpr *var = (SymExpr *)e->kids[0];
+ SymExpr *newvar = new SymExpr(*var);
+#endif
+ Expr *tp = e->kids[1]->clone();
+ Expr *prev = var->val;
+ var->val = newvar;
+ Expr *bod = e->kids[2]->clone();
+ var->val = prev;
+ Expr* ret = new CExpr(PI,newvar,tp,bod);
+ if( data&256 )
+ ret->data |=256;
+ return ret;
+ }
+ default: {
+ Expr **cur = e->kids;
+ Expr *tmp;
+ int size = 0;
+ while((*cur++))
+ size++;
+ Expr **kids = new Expr*[size+1];
+ kids[size]=0;
+ cur = e->kids;
+ bool diff_kid = false;
+ int i = 0;
+ while((tmp = *cur++)) {
+ Expr *c = tmp->clone();
+ diff_kid |= (c != tmp);
+ kids[i++] = c;
+ }
+ if (diff_kid)
+ return new CExpr(op, true /* dummy */, kids);
+ for (int i = 0, iend = size; i != iend; i++)
+ kids[i]->dec();
+ delete[] kids;
+ e->inc();
+ return e;
+ }
+ }
+ }
+ }
+ return 0; // should never be reached
+}
+
+
+Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) {
+#ifndef USE_FLAT_APP
+ Expr *ret = hd;
+ for (int i = start, iend = args.size(); i < iend; i++)
+ ret = new CExpr(APP,ret,args[i]);
+ return ret;
+#else
+ if( start>=(int)args.size() )
+ return hd;
+ else
+ {
+ CExpr *ret = new CExpr( APP );
+ ret->kids = new Expr* [args.size()-start+2];
+ ret->kids[0] = hd;
+ for (int i = start, iend = args.size(); i < iend; i++)
+ ret->kids[i-start+1] = args[i];
+ ret->kids[args.size()-start+1] = NULL;
+ return ret;
+ }
+#endif
+}
+
+Expr* Expr::make_app(Expr* e1, Expr* e2 )
+{
+ //std::cout << "make app from ";
+ //e1->print( std::cout );
+ //std::cout << " ";
+ //e2->print( std::cout );
+ //std::cout << std::endl;
+ CExpr *ret;
+ if( e1->getclass()==CEXPR ){
+ int counter = 0;
+ while( ((CExpr*)e1)->kids[counter] ){
+ counter++;
+ }
+ ret = new CExpr( APP );
+ ret->kids = new Expr* [counter+2];
+ counter = 0;
+ while( ((CExpr*)e1)->kids[counter] ){
+ ret->kids[counter] = ((CExpr*)e1)->kids[counter];
+ counter++;
+ }
+ ret->kids[counter] = e2;
+ ret->kids[counter+1] = NULL;
+ }else{
+ ret = new CExpr( APP, e1, e2 );
+ }
+ //ret->print( std::cout );
+ //std::cout << std::endl;
+ return ret;
+}
+
+int Expr::cargCount = 0;
+
+Expr *Expr::collect_args(std::vector<Expr *> &args, bool follow_defs) {
+ //cargCount++;
+ //if( cargCount%1000==0)
+ //std::cout << cargCount << std::endl;
+#ifndef USE_FLAT_APP
+ CExpr *e = (CExpr *)this;
+ args.reserve(16);
+ while( e->getop() == APP ) {
+ args.push_back(e->kids[1]);
+ e = (CExpr *)e->kids[0];
+ if (follow_defs)
+ e = (CExpr *)e->followDefs();
+ }
+ std::reverse(args.begin(),args.end());
+ return e;
+#else
+ CExpr *e = (CExpr *)this;
+ args.reserve(16);
+ if( e->getop()==APP ){
+ int counter = 1;
+ while( e->kids[counter] ) {
+ args.push_back(e->kids[counter]);
+ counter++;
+ }
+ e = (CExpr*)e->kids[0];
+ }
+ if (follow_defs)
+ return e->followDefs();
+ else
+ return e;
+#endif
+}
+
+Expr *Expr::get_head(bool follow_defs) {
+ CExpr *e = (CExpr *)this;
+ while( e->getop() == APP ) {
+ e = (CExpr *)e->kids[0];
+ if (follow_defs)
+ e = (CExpr *)e->followDefs();
+ }
+ return e;
+}
+
+Expr *Expr::get_body(int op, bool follow_defs) {
+ CExpr *e = (CExpr *)this;
+ while( e->getop() == op ) {
+ e = (CExpr *)e->kids[2];
+ if (follow_defs)
+ e = (CExpr *)e->followDefs();
+ }
+ return e;
+}
+
+// if the return value is different from this, then it is a new reference
+Expr *CExpr::whr() {
+ vector<Expr *> args;
+ if (get_head()->getop() == LAM) {
+ CExpr *head = (CExpr *)collect_args(args, true);
+ Expr *cloned_head;
+ if (head->cloned()) {
+ // we must clone
+ head = (CExpr *)head->clone();
+ cloned_head = head;
+ }
+ else {
+ head->setcloned();
+ cloned_head = 0;
+ }
+ int i = 0;
+ int iend = args.size();
+
+ /* we will end up incrementing the ref count for all the args,
+ since each is either pointed to by a var (following a
+ beta-reduction), or else just an argument in the new
+ application we build below. */
+
+ do {
+ Expr *tmp = args[i++]->followDefs();
+ ((SymExpr *)head->kids[0])->val = tmp;
+ tmp->inc();
+ head = (CExpr *)head->kids[1];
+ } while(head->getop() == LAM && i < iend);
+ for (; i < iend; i++)
+ args[i]->inc();
+ head->inc();
+ if (cloned_head)
+ cloned_head->dec();
+ return build_app(head,args,i);
+ }
+ else
+ return this;
+}
+
+Expr* CExpr::convert_to_tree_app( Expr* e )
+{
+ if( e->getop()==APP )
+ {
+ std::vector< Expr* > kds;
+ int counter = 1;
+ while( ((CExpr*)e)->kids[counter] )
+ {
+ kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) );
+ counter++;
+ }
+ Expr* app = Expr::build_app( e->get_head(), kds );
+ //app->inc();
+ return app;
+ }
+ else
+ {
+ return e;
+ }
+}
+
+Expr* CExpr::convert_to_flat_app( Expr* e )
+{
+ if( e->getop()==APP )
+ {
+ std::vector< Expr* > args;
+ Expr* hd = ((CExpr*)e)->collect_args( args );
+ CExpr* nce = new CExpr( APP );
+ nce->kids = new Expr *[(int)args.size()+2];
+ nce->kids[0] = hd;
+ for( int a=0; a<(int)args.size(); a++ )
+ {
+ nce->kids[a+1] = convert_to_flat_app( args[a] );
+ }
+ nce->kids[(int)args.size()+1] = 0;
+ nce->inc();
+ return nce;
+ }
+ else
+ {
+ return e;
+ }
+}
+
+bool Expr::defeq(Expr *e) {
+
+ /* we handle a few special cases up front, where this Expr might
+ equal e, even though they have different opclass (i.e., different
+ structure). */
+
+ if (this == e)
+ return true;
+ int op1 = getop();
+ int op2 = e->getop();
+ switch (op1) {
+ case ASCRIBE:
+ return ((CExpr *)this)->kids[0]->defeq(e);
+ case APP: {
+ Expr *tmp = ((CExpr *)this)->whr();
+ if (tmp != this) {
+ bool b = tmp->defeq(e);
+ tmp->dec();
+ return b;
+ }
+ if (get_head()->getclass() == HOLE_EXPR) {
+ vector<Expr *> args;
+ Expr *head = collect_args(args, true);
+ Expr *t = e;
+ t->inc();
+ for (int i = 0, iend = args.size(); i < iend; i++) {
+ // don't worry about SYMS_EXPR's, since we should not be in code here.
+ if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark())
+ /* we cannot fill the hole in this case. Either this is not
+ a variable or we are using a variable again. */
+ return false;
+ SymExpr *v = (SymExpr *)args[i];
+
+ // we may have been mapping from expected var v to a computed var
+ Expr *tmp = (v->val ? v->val : v);
+
+ tmp->inc();
+ t = new CExpr(LAM, tmp, t);
+ args[i]->setexmark();
+ }
+ for (int i = 0, iend = args.size(); i < iend; i++)
+ args[i]->clearexmark();
+#ifdef DEBUG_HOLES
+ cout << "Filling hole ";
+ head->debug();
+ cout << "with ";
+ t->debug();
+#endif
+ ((HoleExpr *)head)->val = t;
+ return true;
+ }
+ break;
+ }
+ case NOT_CEXPR:
+ switch (getclass()) {
+ case HOLE_EXPR: {
+ HoleExpr *h = (HoleExpr *)this;
+ if (h->val)
+ return h->val->defeq(e);
+#ifdef DEBUG_HOLES
+ cout << "Filling hole ";
+ h->debug();
+ cout << "with ";
+ e->debug();
+#endif
+#ifdef USE_HOLE_PATH_COMPRESSION
+ Expr *tmp = e->followDefs();
+#else
+ Expr *tmp = e;
+#endif
+ h->val = tmp;
+ tmp->inc();
+ return true;
+ }
+ case SYMS_EXPR:
+ case SYM_EXPR: {
+ SymExpr *s = (SymExpr *)this;
+ if (s->val)
+ return s->val->defeq(e);
+ break;
+ }
+ }
+ break;
+ }
+
+ switch (op2) {
+ case ASCRIBE:
+ return defeq(((CExpr *)e)->kids[0]);
+ case APP: {
+ Expr *tmp = ((CExpr *)e)->whr();
+ if (tmp != e) {
+ bool b = defeq(tmp);
+ tmp->dec();
+ return b;
+ }
+ break;
+ }
+ case NOT_CEXPR:
+ switch (e->getclass()) {
+ case HOLE_EXPR: {
+ HoleExpr *h = (HoleExpr *)e;
+ if (h->val)
+ return defeq(h->val);
+
+#ifdef DEBUG_HOLES
+ cout << "Filling hole ";
+ h->debug();
+ cout << "with ";
+ debug();
+#endif
+#ifdef USE_HOLE_PATH_COMPRESSION
+ Expr *tmp = followDefs();
+#else
+ Expr *tmp = this;
+#endif
+ h->val = tmp;
+ tmp->inc();
+ return true;
+ }
+ case SYMS_EXPR:
+ case SYM_EXPR: {
+ SymExpr *s = (SymExpr *)e;
+ if (s->val)
+ return defeq(s->val);
+ break;
+ }
+ }
+ break;
+ }
+
+ /* at this point, e1 and e2 must have the same opclass if they are
+ to be equal. */
+
+ if (op1 != op2)
+ return false;
+
+ if (op1 == NOT_CEXPR) {
+ switch(getclass()) {
+ case INT_EXPR: {
+ IntExpr *i1 = (IntExpr *)this;
+ IntExpr *i2 = (IntExpr *)e;
+ return (mpz_cmp(i1->n,i2->n) == 0);
+ }
+ case RAT_EXPR: {
+ RatExpr *r1 = (RatExpr *)this;
+ RatExpr *r2 = (RatExpr *)e;
+ return (mpq_cmp(r1->n,r2->n) == 0);
+ }
+ case SYMS_EXPR:
+ case SYM_EXPR:
+ return (this == e);
+ }
+ }
+
+ /* Now op1 and op2 must both be CExprs, and must have the same op to be
+ equal. */
+
+ CExpr *e1 = (CExpr *)this;
+ CExpr *e2 = (CExpr *)e;
+
+ int last = 1;
+ switch (op1) {
+ case PI:
+ if (!e1->kids[1]->defeq(e2->kids[1]))
+ return false;
+ last++;
+ // fall through to LAM case
+ case LAM: {
+
+ /* It is critical that we point e1's var. (v1) back to e2's (call
+ it v2). The reason this is critical is that we assume any
+ holes are in e1. So we could end up with (_ v1) = t. We wish
+ to fill _ in this case with (\ v2 t). If v2 pointed to v1, we
+ could not return (\ v1 t), because the fact that v2 points to
+ v1 would then be lost.
+ */
+ SymExpr *v1 = (SymExpr *)e1->kids[0];
+ Expr *prev_v1_val = v1->val;
+ v1->val = e2->kids[0]->followDefs();
+ bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]);
+ v1->val = prev_v1_val;
+ return bodies_equal;
+ }
+ case APP:
+#ifndef USE_FLAT_APP
+ return (e1->kids[0]->defeq(e2->kids[0]) &&
+ e1->kids[1]->defeq(e2->kids[1]));
+#else
+ {
+ int counter = 0;
+ while( e1->kids[counter] ){
+ if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) )
+ return false;
+ counter++;
+ }
+ return e2->kids[counter]==NULL;
+ }
+#endif
+ case TYPE:
+ case KIND:
+ case MPZ:
+ // already checked that both exprs have the same opclass.
+ return true;
+ } // switch(op1)
+
+ return false; // never reached.
+}
+
+int Expr::fiCounter = 0;
+
+bool Expr::free_in(Expr *x) {
+ //fiCounter++;
+ //if( fiCounter%1==0 )
+ // std::cout << fiCounter << std::endl;
+ switch(getop()) {
+ case NOT_CEXPR:
+ switch (getclass()) {
+ case HOLE_EXPR: {
+ HoleExpr *h = (HoleExpr *)this;
+ if (h->val)
+ return h->val->free_in(x);
+ return (h == x);
+ }
+ case SYMS_EXPR:
+ case SYM_EXPR: {
+ SymExpr *s = (SymExpr *)this;
+ if (s->val && s->val->getclass() == HOLE_EXPR)
+ /* we do not need to follow the "val" pointer except in this
+ one case, when x is a hole (which we do not bother to check
+ here) */
+ return s->val->free_in(x);
+ return (s == x);
+ }
+ case INT_EXPR:
+ return false;
+ }
+ break;
+ case LAM:
+ case PI:
+ if (x == ((CExpr *)this)->kids[0])
+ return false;
+ // fall through
+ default: {
+ // must be a CExpr
+ CExpr *e = (CExpr *)this;
+ Expr *tmp;
+ Expr **cur = e->kids;
+ while ((tmp = *cur++))
+ if (tmp->free_in(x))
+ return true;
+ return false;
+ }
+ }
+ return false; // should not be reached
+}
+
+void Expr::calc_free_in(){
+ data &= ~256;
+ data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] );
+}
+
+string Expr::toString() {
+ ostringstream oss;
+ print(oss);
+ return oss.str();
+}
+
+static void print_kids(ostream &os, Expr **kids) {
+ Expr *tmp;
+ while ((tmp = *kids++)) {
+ os << " ";
+ tmp->print(os);
+ }
+}
+
+static void print_vector(ostream &os, const vector<Expr *> &v) {
+ for(int i = 0, iend = v.size(); i < iend; i++) {
+ os << " ";
+ v[i]->print(os);
+ }
+}
+
+void Expr::print(ostream &os) {
+ CExpr *e = (CExpr *)this; // for CEXPR cases
+
+ //std::cout << e->getop() << " ";
+ /*
+#ifdef DEBUG_REFCNT
+ os << "<";
+ char tmp[10];
+ sprintf(tmp,"%d",getrefcnt());
+ os << tmp << "> ";
+#endif
+*/
+
+ switch(getop()) {
+ case NOT_CEXPR: {
+ switch(getclass()) {
+ case INT_EXPR:
+ {
+ IntExpr *e = (IntExpr *)this;
+ if (mpz_sgn(e->n) < 0) {
+ os << "(~ ";
+ mpz_t tmp;
+ mpz_init(tmp);
+ mpz_neg(tmp,e->n);
+ char *s = mpz_get_str(0,10,tmp);
+ os << s;
+ free(s);
+ mpz_clear(tmp);
+ os << ")";
+ //os << "mpz";
+ }
+ else {
+ char *s = mpz_get_str(0,10,e->n);
+ os << s;
+ free(s);
+ //os << "mpz";
+ }
+ break;
+ }
+ case RAT_EXPR:
+ {
+ RatExpr *e = (RatExpr *)this;
+ char *s = mpq_get_str(0,10,e->n);
+ os << s;
+ if (mpq_sgn(e->n) < 0) {
+ os << "(~ ";
+ mpq_t tmp;
+ mpq_init(tmp);
+ mpq_neg(tmp,e->n);
+ char *s = mpq_get_str(0,10,tmp);
+ os << s;
+ free(s);
+ mpq_clear(tmp);
+ os << ")";
+ }
+ else {
+ char *s = mpq_get_str(0,10,e->n);
+ os << s;
+ free(s);
+ }
+ break;
+ }
+#ifndef DEBUG_SYM_NAMES
+ case SYM_EXPR:
+ {
+ SymExpr *e = (SymExpr *)this;
+ if (e->val) {
+ if (e->val->getop() == PROG) {
+ os << e;
+#ifdef DEBUG_SYMS
+ os << "[PROG]";
+#endif
+ }else{
+#ifdef DEBUG_SYMS
+ os << e;
+ os << "[SYM ";
+#endif
+ e->val->print(os);
+#ifdef DEBUG_SYMS
+ os << "]";
+#endif
+ }
+ }
+ else
+ os << e;
+ break;
+ }
+#else
+ case SYM_EXPR: /* if we are debugging sym names, then
+ SYM_EXPRs are really SymSExprs. */
+#endif
+ case SYMS_EXPR: {
+ SymSExpr *e = (SymSExpr *)this;
+ if (e->val) {
+ if (e->val->getop() == PROG) {
+ os << e->s;
+#ifdef DEBUG_SYMS
+ os << "[PROG]";
+#endif
+ }else{
+#ifdef DEBUG_SYMS
+ os << e->s;
+ os << "[SYM ";
+#endif
+ e->val->print(os);
+#ifdef DEBUG_SYMS
+ os << "]";
+#endif
+ }
+ }
+ else
+ os << e->s;
+ break;
+ }
+ case HOLE_EXPR:
+ {
+ HoleExpr *e = (HoleExpr *)this;
+ if (e->val) {
+#ifdef DEBUG_SYMS
+ os << "_" << "[HOLE ";
+#endif
+ e->val->print(os);
+#ifdef DEBUG_SYMS
+ os << "]";
+#endif
+ }else {
+ os << "_";
+#ifdef DEBUG_HOLE_NAMES
+ char tmp[100];
+ sprintf(tmp,"%d",e->id);
+ os << "[ " << tmp << "]";
+#else
+ os << "[ " << e << "]";
+#endif
+ }
+ break;
+ }
+ default:
+ os << "; unrecognized form of expr";
+ break;
+ }
+ break;
+ } // case NOT_CEXPR
+ case APP: {
+ os << "(";
+ vector<Expr *> args;
+ Expr *head = collect_args(args, false /* follow_defs */);
+ head->print(os);
+ print_vector(os, args);
+ os << ")";
+ break;
+ }
+ case LAM:
+ os << "(\\";
+ print_kids(os, e->kids);
+ os << ")";
+ break;
+ case PI:
+ os << "(!";
+ print_kids(os, e->kids);
+ os << ")";
+ break;
+ case TYPE:
+ os << "type";
+ break;
+ case KIND:
+ os << "kind";
+ break;
+ case MPZ:
+ os << "mpz";
+ break;
+ case MPQ:
+ os << "mpq";
+ break;
+ case ADD:
+ os << "(mp_add";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case MUL:
+ os << "(mp_mul";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case DIV:
+ os << "(mp_div";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case NEG:
+ os << "(mp_neg";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case IFNEG:
+ os << "(ifneg";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case IFZERO:
+ os << "(ifzero";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case RUN:
+ os << "(run";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case PROG:
+ os << "(prog";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case PROGVARS:
+ os << "(";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case MATCH:
+ os << "(match";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case CASE:
+ os << "(";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case LET:
+ os << "(let";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case DO:
+ os << "(do";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case IFMARKED:
+ os << "(ifmarked";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case COMPARE:
+ os << "(compare";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case MARKVAR:
+ os << "(markvar";
+ print_kids(os,e->kids);
+ os << ")";
+ break;
+ case FAIL:
+ os << "(fail ";
+ print_kids(os, e->kids);
+ os << ")";
+ break;
+ case ASCRIBE:
+ os << "(:";
+ print_kids(os, e->kids);
+ os << ")";
+ break;
+ default:
+ os << "; unrecognized form of expr(2) " << getop() << " " << getclass();
+ } // switch(getop())
+}
+
+bool Expr::isType( Expr* statType ){
+ Expr* typ = this;
+ while( typ!=statType ){
+ if( typ->getop()==PI ){
+ typ = ((CExpr*)typ)->kids[2];
+ }else{
+ return false;
+ }
+ }
+ return true;
+}
+
+int SymExpr::symmCount = 0;
+#ifdef MARKVAR_32
+int SymExpr::mark()
+{
+ if( mark_map.find( this )== mark_map.end() )
+ {
+ symmCount++;
+ mark_map[this] = 0;
+ }
+ return mark_map[this];
+}
+void SymExpr::smark( int m )
+{
+ mark_map[this] = m;
+}
+#endif \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback