prop-src/trs2.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This is the main partial evaluation routines.
   4 //
   5 ///////////////////////////////////////////////////////////////////////////////
   6 #include <iostream>
   7 #include <string.h>
   8 #include <stdlib.h>
   9 #include "trs.ph"
  10 #include "ir.ph"
  11 #include "ast.ph"
  12 #include "type.h"
  13 #include "list.h"
  14 #include "matchcom.h"
  15 #include "funmap.h"
  16 #include "rwgen.h"
  17
  18 ///////////////////////////////////////////////////////////////////////////////
  19 //
  20 //  Type definitions
  21 //
  22 ///////////////////////////////////////////////////////////////////////////////
  23 typedef TreeAutomaton::Functor Functor;
  24 typedef TreeAutomaton::State   State;
  25 typedef TreeAutomaton::Rule    Rule;
  26
  27 ///////////////////////////////////////////////////////////////////////////////
  28 //
  29 //  Method for partial evaluating the trs
  30 //
  31 ///////////////////////////////////////////////////////////////////////////////
  32 void TRS::mix()
  33 {  for (Rule r = 0; r < number_of_rules; r++)
  34    {  mix(r);
  35    }
  36 }
  37
  38 ///////////////////////////////////////////////////////////////////////////////
  39 //
  40 //  Method for partial evaluating one rule
  41 //
  42 ///////////////////////////////////////////////////////////////////////////////
  43 void TRS::mix(Rule r)
  44 {  mix_0(r);
  45    mix_1(r);
  46 }
  47
  48 ///////////////////////////////////////////////////////////////////////////////
  49 //
  50 //  Method for partial evaluting one rule, using 0-strategy.
  51 //
  52 ///////////////////////////////////////////////////////////////////////////////
  53 void TRS::mix_0(Rule r)
  54 {  int arity = num_var_map[r];
  55    for (int i = 0; i < arity; i++) states[i] = 0;
  56    // msg("0-Partial evaluating %r ", rule_map[r]) << rhs_map[r] << '\n';
  57    Term rhs = copy(rhs_map[r]);
  58    int reductions = 0;
  59    State new_state = normalize(rhs,reductions);
  60    if (reductions > 0)
  61    {  print_residue(r,rhs);
  62       make_rhs(r,optimized_map[r] = make_exp(rhs));
  63    }
  64 }
  65
  66 ///////////////////////////////////////////////////////////////////////////////
  67 //
  68 //  Method for partial evaluting one rule, using 1-strategy.
  69 //
  70 ///////////////////////////////////////////////////////////////////////////////
  71 void TRS::mix_1(Rule r)
  72 {  int arity            = num_var_map[r];
  73    int number_of_states = treeauto.number_of_states();
  74    // msg("1-Partial evaluating %r ", rule_map[r]) << rhs_map[r] << '\n';
  75    for (int i = 0; i < arity; i++)
  76    {  // If the variable does not have an index we can't do anything
  77       // with it.
  78       if (! compiler.has_index(var_pat_map[r][i]->ty)) continue;
  79       for (int j = 0; j < arity; j++) states[j] = 0;
  80       for (State s = 1; s < number_of_states; s++)
  81       {  // skip accept states
  82          states[i] = s;
  83          if (treeauto.is_accept_state(s)) continue;
  84          if (! is_relevant(r)) continue;
  85          int reductions = 0;
  86          Term rhs = copy(rhs_map[r]);
  87          State new_state = normalize(rhs,reductions);
  88          if (reductions > 0)
  89          {  generate_residue(r,i,s,rhs); }
  90       }
  91    }
  92 }
  93
  94 ///////////////////////////////////////////////////////////////////////////////
  95 //
  96 //  Method to check that a particular specialization is relevant
  97 //
  98 ///////////////////////////////////////////////////////////////////////////////
  99 Bool TRS::is_relevant(Rule r)
 100 {  int redex_count = 0;
 101    count_redex = true;
 102    State s = normalize(lhs_map[r],redex_count);
 103    count_redex = false;
 104    // cerr << lhs_map[r] << " has " << redex_count << " redexes\n";
 105    if (redex_count > 1) return false;
 106    if (treeauto.accept1_rule(s) != r) return false;
 107    return true;
 108 }
 109
 110 ///////////////////////////////////////////////////////////////////////////////
 111 //
 112 //  Method to normalize a rule
 113 //
 114 ///////////////////////////////////////////////////////////////////////////////
 115 TRS::State TRS::normalize(Term& term, int& reductions)
 116 {  Bool changed;
 117    State new_state;
 118    do {
 119       changed = false;
 120       match (term)
 121       {  CONSterm(f,_,n,args):
 122          {  int mu[MAX_VARS];
 123             for (int i = 0; i < n; i++)
 124             {  State s = normalize(args[i],reductions);
 125                mu[i]   = treeauto.index_map(f,i,s);
 126             }
 127             new_state = treeauto.get_delta(f,mu);
 128             // Check for redex
 129             if (treeauto.is_accept_state(new_state))
 130             {  if (count_redex) {
 131                   reductions++;
 132                   return new_state;
 133                }
 134                term = reduce(term,new_state,reductions,changed);
 135             }
 136          }
 137       |  VARterm(v,_,_): { return states[v]; }
 138       |  _:              { return 0; }
 139       }
 140    } while (changed);
 141    return new_state;
 142 }
 143
 144 ///////////////////////////////////////////////////////////////////////////////
 145 //
 146 //  Method to reduce a rule during accepting
 147 //
 148 ///////////////////////////////////////////////////////////////////////////////
 149 Term TRS::reduce(Term term, State state, int& reductions, Bool& changed)
 150 {
 151    // Test for conditional rules
 152    // For each rule that can accept, check the guard associated
 153    // with the rule.  Evaluate the guard if possible.
 154    // We'll not reduce if we are not guaranteed that the reduction
 155    // can be performed.
 156    const BitSet& accept = treeauto.accept_rules(state);
 157    for (Rule r = 0; r <= number_of_rules; r++)
 158    {  if (accept[r])
 159       {  Exp guard = guard_map[r];
 160          EvalResult result = SUCCESS;
 161          if (guard == NOexp) result = SUCCESS;
 162          else result = eval_guard(guard);
 163          switch (result)
 164          {  case SUCCESS:
 165             {  Term rule_rhs = rhs_map[r];
 166                Bool ok = true;
 167                Term new_rhs = subst(rule_rhs,term,ok);
 168                if (! ok) return term; // no reduction
 169                reductions++;
 170                changed = true;
 171                return new_rhs;
 172             } break;
 173             case UNKNOWN: return term; // no reduction
 174             case FAILURE:  break; // try next rule
 175          }
 176       }
 177    }
 178    return term;  // no reduction
 179 }
 180
 181 ///////////////////////////////////////////////////////////////////////////////
 182 //
 183 //  Apply a rule
 184 //
 185 ///////////////////////////////////////////////////////////////////////////////
 186 Term TRS::subst(Term rhs, Term redex, Bool& ok)
 187 {  match (rhs)
 188    {  CONSterm(f,c,n,args):
 189       {  return CONSterm(f,c,n,subst(n,args,redex,ok)); }
 190    |  VARterm(v,_,exp):
 191       {  return proj(exp,redex,ok); }
 192    |  CODEterm exp:
 193       {  return proj(exp,redex,ok); }
 194    |  _:  { bug("TRS::subst"); return redex; }
 195    }
 196 }
 197
 198 ///////////////////////////////////////////////////////////////////////////////
 199 //
 200 //  Apply a rule
 201 //
 202 ///////////////////////////////////////////////////////////////////////////////
 203 Term * TRS::subst(int n, Term * rhs, Term redex, Bool& ok)
 204 {  Term * args = (Term*)mem_pool.m_alloc(sizeof(Term) * n);
 205    for (int i = 0; i < n; i++)
 206       args[i] = subst(rhs[i],redex,ok);
 207    return args;
 208 }
 209
 210 ///////////////////////////////////////////////////////////////////////////////
 211 //
 212 //  Perform projection a rule
 213 //
 214 ///////////////////////////////////////////////////////////////////////////////
 215 Term TRS::proj(Exp exp, Term redex, Bool& ok)
 216 {  int nth;
 217    match (exp) and (redex)
 218    {  IDexp "redex", redex:  { return redex; }
 219    |  DOTexp(SELECTORexp(e,c1,ty),ith), redex:
 220       {  match (proj(e,redex,ok))
 221          {  CONSterm(_,c2,n,args) |
 222               c1 == c2 && ((nth = atol(ith+1)-1), nth < n):
 223             {  return args[nth]; }
 224          |  CODEterm(e): { return CODEterm(DOTexp(SELECTORexp(e,c1,ty),ith)); }
 225          |  VARterm(_,_,e):
 226                 { return CODEterm(DOTexp(SELECTORexp(e,c1,ty),ith)); }
 227          |  redex as CONSterm(_,c2,n,args):
 228             {  // msg("1 Can't project %e %i %i", exp,nth,n);
 229                // print(msg(""),redex); msg("\n");
 230                ok = false;
 231                return redex;
 232             }
 233          |  exp:
 234             {  // msg("1 Can't project %e", exp);
 235                // print(msg(""),redex); msg("\n");
 236                ok = false;
 237                return redex;
 238             }
 239          }
 240       }
 241    |  SELECTORexp(e,c1,ty), redex:
 242       {  match (proj(e,redex,ok))
 243          {  CONSterm(_,c2,n,args) | c1 == c2:
 244             {  return args[0]; }
 245          |  CODEterm(e): { return CODEterm(SELECTORexp(e,c1,ty)); }
 246          |  VARterm(_,_,e): { return CODEterm(SELECTORexp(e,c1,ty)); }
 247          |  redex:
 248             {  // msg("2 Can't project %e ", exp);
 249                // print(msg(""),redex); msg("\n");
 250                ok = false;
 251                return redex;
 252             }
 253          }
 254       }
 255    |  _, _:
 256       {  // msg("3 Can't project %e ", exp);
 257          // print(msg(""),redex); msg("\n");
 258          ok = false;
 259          return CODEterm(NOexp);
 260       }
 261    }
 262 }
 263
 264 ///////////////////////////////////////////////////////////////////////////////
 265 //
 266 //  Compose two projection expression
 267 //
 268 ///////////////////////////////////////////////////////////////////////////////
 269 Exp TRS::proj(Exp e1, Exp e2, Bool& ok)
 270 {  match (e1)
 271    {  IDexp "redex":       { return e2; }
 272    |  SELECTORexp(e,c,ty): { return SELECTORexp(proj(e,e2,ok),c,ty); }
 273    |  DOTexp(e,id):        { return DOTexp(proj(e,e2,ok),id); }
 274    |  _: { msg("Can't project %e %e\n", e1, e2);  return NOexp; }
 275    }
 276 }
 277
 278 ///////////////////////////////////////////////////////////////////////////////
 279 //
 280 //  Copying the rhs
 281 //
 282 ///////////////////////////////////////////////////////////////////////////////
 283 Term TRS::copy(Term rhs)
 284 {  match (rhs)
 285    {  CONSterm(f,c,n,args):
 286       {  return CONSterm(f,c,n,copy(n,args)); }
 287    |  _: { return rhs; }
 288    }
 289 }
 290
 291 ///////////////////////////////////////////////////////////////////////////////
 292 //
 293 //  Copying the rhs
 294 //
 295 ///////////////////////////////////////////////////////////////////////////////
 296 Term * TRS::copy(int n, Term rhs [])
 297 {  Term * args = (Term*)mem_pool.m_alloc(sizeof(Term) * n);
 298    for (int i = 0; i < n; i++)
 299       args[i] = copy(rhs[i]);
 300    return args;
 301 }
 302
 303 ///////////////////////////////////////////////////////////////////////////////
 304 //
 305 //  Method to evaluate a guard expression
 306 //
 307 ///////////////////////////////////////////////////////////////////////////////
 308 TRS::EvalResult TRS::eval_guard(Exp exp)
 309 {  return UNKNOWN;
 310 }
 311
 312 ///////////////////////////////////////////////////////////////////////////////
 313 //
 314 //  Method to print out the residue.
 315 //
 316 ///////////////////////////////////////////////////////////////////////////////
 317 void TRS::print_residue(Rule r, Term rhs_residue) const
 318 {  std::ostream& log = open_logfile();
 319    MatchRule rule = rule_map[r];
 320    log << "line " << rule->begin_line << ": "
 321        << rule_map[r] << ' ';
 322    print(log, rhs_map[r]); log << '\n';
 323    for (int i = 0; i < num_var_map[r]; i++)
 324    {  if (states[i] != 0)
 325       {  log << "\twhen " << var_pat_map[r][i] << " is in state:\n";
 326          treeauto.print_state(log,states[i]);
 327       }
 328    }
 329    log << "\toptimize rhs to ";
 330    print(log,rhs_residue);
 331    log << "\n\n";
 332 }