app/willard/paige-aux.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.5),
   3 //  last updated on Jun 18, 1997.
   4 //  The original source file is "paige-aux.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_STRCMP_USED
   9 #define PROP_QUARK_USED
  10 #define PROP_TUPLE2_USED
  11 #include <propdefs.h>
  12 #line 1 "paige-aux.pcc"
  13 #include "paige.h"
  14 #include "willard-ast.h"
  15 #include <AD/strings/quark.h>
  16
  17 //
  18 //  Auxiliary routines to generate new variable names
  19 //
  20 Id PaigeGoyal::gensym() { return gensym("Q"); }
  21 Id PaigeGoyal::gensym(Id prefix)
  22    { return Quark(Quark(prefix,"_"),++new_name); }
  23
  24 //
  25 //  Auxiliary routines to check whether a variable is free in an expression
  26 //
  27 Bool PaigeGoyal::is_free(Id x, Exp e) const
  28 {  IdSet S;
  29    free_vars(e,S);
  30    return ! S.contains(x);
  31 }
  32
  33 Bool PaigeGoyal::is_free(Ids xs, Exp e) const
  34 {  IdSet S;
  35    free_vars(e,S);
  36
  37 #line 24 "paige-aux.pcc"
  38 #line 24 "paige-aux.pcc"
  39 {
  40    for (;;) {
  41       if (xs) {
  42 #line 24 "paige-aux.pcc"
  43         if (S.contains(xs->_1)) return false; xs = xs->_2;
  44 #line 24 "paige-aux.pcc"
  45       } else { goto L1; }
  46    }
  47    L1:;
  48 }
  49 #line 25 "paige-aux.pcc"
  50 #line 25 "paige-aux.pcc"
  51
  52    return true;
  53 }
  54
  55 void PaigeGoyal::remove_vars(IdSet& S, Ids ids) const
  56 {
  57
  58 #line 31 "paige-aux.pcc"
  59 #line 31 "paige-aux.pcc"
  60 {
  61    for (;;) {
  62       if (ids) {
  63 #line 31 "paige-aux.pcc"
  64         S.remove(ids->_1); ids = ids->_2;
  65 #line 31 "paige-aux.pcc"
  66       } else { goto L2; }
  67    }
  68    L2:;
  69 }
  70 #line 31 "paige-aux.pcc"
  71 #line 31 "paige-aux.pcc"
  72
  73 }
  74
  75 void PaigeGoyal::remove_vars(IdSet& S, const IdSet& T) const
  76 {  foreach(i,T) S.remove(T.key(i));
  77 }
  78
  79 //
  80 //  Methods to collect free variables in a term
  81 //
  82 void PaigeGoyal::free_vars(Exp e, IdSet& S) const
  83 {
  84 #line 42 "paige-aux.pcc"
  85 #line 52 "paige-aux.pcc"
  86 {
  87    switch (e->tag__) {
  88       case a_Exp::tag_OP: {
  89 #line 43 "paige-aux.pcc"
  90         free_vars(_OP(e)->_2,S);
  91 #line 43 "paige-aux.pcc"
  92          } break;
  93       case a_Exp::tag_APP: {
  94 #line 44 "paige-aux.pcc"
  95         free_vars(_APP(e)->_2,S);
  96 #line 44 "paige-aux.pcc"
  97          } break;
  98       case a_Exp::tag_LIT: {
  99 #line 45 "paige-aux.pcc"
 100         return;
 101 #line 45 "paige-aux.pcc"
 102          } break;
 103       case a_Exp::tag_ID: {
 104 #line 46 "paige-aux.pcc"
 105         S.insert(_ID(e)->ID);
 106 #line 46 "paige-aux.pcc"
 107          } break;
 108       case a_Exp::tag_TUPLE: {
 109 #line 47 "paige-aux.pcc"
 110         free_vars(_TUPLE(e)->TUPLE,S);
 111 #line 47 "paige-aux.pcc"
 112          } break;
 113       case a_Exp::tag_FORALL: {
 114 #line 48 "paige-aux.pcc"
 115         free_vars(_FORALL(e)->_2,S); free_vars(_FORALL(e)->_3,S); S.remove(_FORALL(e)->_1);
 116 #line 48 "paige-aux.pcc"
 117          } break;
 118       case a_Exp::tag_EXISTS: {
 119 #line 49 "paige-aux.pcc"
 120         free_vars(_EXISTS(e)->_2,S); free_vars(_EXISTS(e)->_3,S); S.remove(_EXISTS(e)->_1);
 121 #line 49 "paige-aux.pcc"
 122          } break;
 123       case a_Exp::tag_GUARD: {
 124 #line 51 "paige-aux.pcc"
 125         free_vars(_GUARD(e)->_1,S); free_vars(_GUARD(e)->_2,S);
 126 #line 51 "paige-aux.pcc"
 127          } break;
 128       case a_Exp::tag_GENERATOR: {
 129 #line 52 "paige-aux.pcc"
 130         free_vars(_GENERATOR(e)->_2,S); free_vars(_GENERATOR(e)->_3,S); remove_vars(S,_GENERATOR(e)->_1);
 131 #line 52 "paige-aux.pcc"
 132          } break;
 133       default: {
 134 #line 50 "paige-aux.pcc"
 135         free_vars(_LET(e)->_2,S); free_vars(_LET(e)->_3,S); S.remove(_LET(e)->_1);
 136 #line 50 "paige-aux.pcc"
 137          } break;
 138    }
 139 }
 140 #line 54 "paige-aux.pcc"
 141 #line 54 "paige-aux.pcc"
 142
 143 }
 144
 145 void PaigeGoyal::free_vars(Exps es, IdSet& S) const
 146 {
 147 #line 58 "paige-aux.pcc"
 148 #line 59 "paige-aux.pcc"
 149 {
 150    for (;;) {
 151       if (es) {
 152 #line 59 "paige-aux.pcc"
 153         free_vars(es->_1,S); es = es->_2;
 154 #line 59 "paige-aux.pcc"
 155       } else { goto L3; }
 156    }
 157    L3:;
 158 }
 159 #line 59 "paige-aux.pcc"
 160 #line 59 "paige-aux.pcc"
 161
 162 }
 163
 164 void PaigeGoyal::free_vars(Ids xs, IdSet& S) const
 165 {
 166 #line 63 "paige-aux.pcc"
 167 #line 64 "paige-aux.pcc"
 168 {
 169    for (;;) {
 170       if (xs) {
 171 #line 64 "paige-aux.pcc"
 172         S.insert(xs->_1); xs = xs->_2;
 173 #line 64 "paige-aux.pcc"
 174       } else { goto L4; }
 175    }
 176    L4:;
 177 }
 178 #line 64 "paige-aux.pcc"
 179 #line 64 "paige-aux.pcc"
 180
 181 }
 182 #line 66 "paige-aux.pcc"
 183 /*
 184 ------------------------------- Statistics -------------------------------
 185 Merge matching rules         = yes
 186 Number of DFA nodes merged   = 4
 187 Number of ifs generated      = 4
 188 Number of switches generated = 1
 189 Number of labels             = 0
 190 Number of gotos              = 0
 191 Adaptive matching            = disabled
 192 Fast string matching         = disabled
 193 Inline downcasts             = disabled
 194 --------------------------------------------------------------------------
 195 */