prop-src/trs.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  These are the routines for building the data structure
   4 //  for partial evaluting a TRS
   5 //
   6 ///////////////////////////////////////////////////////////////////////////////
   7 #include <iostream>
   8 #include <string.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 "datagen.h"
  16 #include "rwgen.h"
  17 #include "funmap.h"
  18 #include "setlgen.h"
  19
  20 ///////////////////////////////////////////////////////////////////////////////
  21 //
  22 //  Constructors for represents a term
  23 //
  24 ///////////////////////////////////////////////////////////////////////////////
  25 instantiate datatype Term;
  26
  27 ///////////////////////////////////////////////////////////////////////////////
  28 //
  29 //  Constructor for TRS
  30 //
  31 ///////////////////////////////////////////////////////////////////////////////
  32 TRS::TRS(RewritingCompiler& C)
  33    : compiler(C), Fmap(*C.Fmap), treeauto(*C.Fmap->tree_gen),
  34      count_redex(false)
  35 {
  36    MatchRules rules = Fmap.bottomup_rules;
  37    number_of_rules  = length(rules);
  38    rule_map    = new MatchRule [number_of_rules];
  39    guard_map   = new Exp       [number_of_rules];
  40    lhs_map     = new Term      [number_of_rules];
  41    rhs_map     = new Term      [number_of_rules];
  42    num_var_map = new int       [number_of_rules];
  43    var_map     = new Exp *     [number_of_rules];
  44    var_pat_map = new Pat *     [number_of_rules];
  45    residue_map = new Residues *[number_of_rules];
  46    literal_map = new Literal   [Fmap.G.functors()];
  47    optimized_map = new Exp     [number_of_rules];
  48
  49    clear_statistics();
  50
  51    int i = 0;
  52    for_each(MatchRule, r, rules)
  53    {  match (r)
  54       {  MATCHrule(_,pat,guard,exp,action):
  55          {  if (r->rule_number != i) bug("%LTRS::TRS()");
  56             rule_map[i]  = r;
  57             guard_map[i] = guard;
  58             make_lhs(i,pat);
  59             match (action)
  60             {  #[MARKEDdecl(_,REPLACEMENTdecl(exp,_))]: { make_rhs(i,exp); }
  61             |  _: { rhs_map[i] = OPAQUEterm(action); }
  62             }
  63          }
  64       }
  65       i++;
  66    }
  67 }
  68
  69 ///////////////////////////////////////////////////////////////////////////////
  70 //
  71 //  Destructor for TRS
  72 //
  73 ///////////////////////////////////////////////////////////////////////////////
  74 TRS::~TRS()
  75 {  delete [] rule_map;
  76    delete [] guard_map;
  77    delete [] lhs_map;
  78    delete [] rhs_map;
  79    delete [] num_var_map;
  80    delete [] var_map;
  81    delete [] var_pat_map;
  82    delete [] residue_map;
  83    delete [] literal_map;
  84    delete [] optimized_map;
  85 }
  86
  87 ///////////////////////////////////////////////////////////////////////////////
  88 //
  89 //  Method to determine if any expression is a pattern variable.
  90 //
  91 ///////////////////////////////////////////////////////////////////////////////
  92 Bool is_pattern_var(Exp exp)
  93 {  match while (exp)
  94    {  SELECTORexp(IDexp "redex",_,_):           { return true; }
  95    |  DOTexp(SELECTORexp(IDexp "redex",_,_),_): { return true; }
  96    |  DOTexp(SELECTORexp(e,_,_),_):             { exp = e; }
  97    |  SELECTORexp(e,_,_):                       { exp = e; }
  98    |  _:                                        { return false; }
  99    }
 100 }
 101
 102 ///////////////////////////////////////////////////////////////////////////////
 103 //
 104 //  Method to create the lhs
 105 //
 106 ///////////////////////////////////////////////////////////////////////////////
 107 void TRS::make_lhs(Rule r, Pat pat)
 108 {  num_vars = 0;
 109    lhs_map[r] = make_term(pat);
 110
 111    num_var_map[r] = num_vars;
 112    var_map[r]     = (Exp*)mem_pool.m_alloc(sizeof(Exp)*num_vars);
 113    var_pat_map[r] = (Pat*)mem_pool.m_alloc(sizeof(Pat)*num_vars);
 114    residue_map[r] = (Residues*)mem_pool.c_alloc(sizeof(Residues)*num_vars);
 115    optimized_map[r] = NOexp;
 116
 117    memcpy(var_map[r],    vars,    sizeof(Exp)*num_vars);
 118    memcpy(var_pat_map[r],var_pats,sizeof(Pat)*num_vars);
 119 }
 120
 121 ///////////////////////////////////////////////////////////////////////////////
 122 //
 123 //  Method to create the lhs for rule r
 124 //
 125 ///////////////////////////////////////////////////////////////////////////////
 126 Term TRS::make_term(Pat pat)
 127 {  match while (pat)
 128    {  MARKEDpat(_,p): { pat = p; }
 129    |  ASpat(_,p,_,_): { pat = p; }
 130    |  IDpat _:        { return make_term_var(pat,pat->selector); }
 131    |  APPpat(CONSpat C, TUPLEpat ps): { return make_term(pat,C,ps); }
 132    |  APPpat(CONSpat C, p):           { return make_term(pat,C,#[p]); }
 133    |  CONSpat C:                      { return make_term(pat,C,#[]); }
 134    |  LISTpat { cons, nil, head = #[], tail = NOpat }:
 135       {  return make_term(pat,nil,#[]); }
 136    |  LISTpat { cons, nil, head = #[], tail }:
 137       {  pat = tail; }
 138    |  LISTpat { cons, nil, head = #[h ... t], tail }:
 139       {  Pat tl_pat = LISTpat'{cons = cons, nil = nil, head = t, tail = tail};
 140          tl_pat->ty = pat->ty;
 141          return make_term(pat,cons,#[h,tl_pat]);
 142       }
 143    |  LITERALpat l | Fmap.literal_map.contains(l):
 144       {  Functor f = Fmap.literal_map[l];
 145          literal_map[f] = l;
 146          return CONSterm(f,NOcons,0,0);
 147       }
 148    |  pat:                            { return PATterm(pat); }
 149    }
 150 }
 151
 152 ///////////////////////////////////////////////////////////////////////////////
 153 //
 154 //  Method to create the lhs for rule r
 155 //
 156 ///////////////////////////////////////////////////////////////////////////////
 157 Term TRS::make_term(Pat pat, Cons cons, Pats pats)
 158 {  int n       = length(pats);
 159    FunctorTable::Entry * E = Fmap.type_map.lookup(pat->ty);
 160    if (E == 0) { return PATterm(pat); }
 161    match (cons->alg_ty)
 162    {  DATATYPEty ({ unit ... }, _):
 163       {  Functor f = Fmap.type_map.value(E) + cons->tag +
 164                        (cons->ty == NOty ? 0 : unit);
 165          return CONSterm(f,cons,n,make_term(pats));
 166       }
 167    |  _: { bug("TRS::make_term"); return PATterm(pat); }
 168    }
 169 }
 170
 171 ///////////////////////////////////////////////////////////////////////////////
 172 //
 173 //  Method to create the lhs for rule r
 174 //
 175 ///////////////////////////////////////////////////////////////////////////////
 176 Term * TRS::make_term(Pats pats)
 177 {  int n = length(pats);
 178    Term * args = (Term *)mem_pool.m_alloc(sizeof(Term) * n);
 179    int i = 0;
 180    for_each(Pat, p, pats) args[i++] = make_term(p);
 181    return args;
 182 }
 183
 184 ///////////////////////////////////////////////////////////////////////////////
 185 //
 186 //  Return the type of an expression
 187 //
 188 ///////////////////////////////////////////////////////////////////////////////
 189 Ty type_of(Exp e) { return type_of(e,Env()); }
 190
 191 ///////////////////////////////////////////////////////////////////////////////
 192 //
 193 //  Method to create the rhs for rule r
 194 //
 195 ///////////////////////////////////////////////////////////////////////////////
 196 void TRS::make_rhs(Rule r, Exp exp)
 197 {  type_of(exp);
 198    rhs_map[r] = make_term(exp);
 199 }
 200
 201 ///////////////////////////////////////////////////////////////////////////////
 202 //
 203 //  Method to create the rhs
 204 //
 205 ///////////////////////////////////////////////////////////////////////////////
 206 Term TRS::make_term(Exp exp)
 207 {  Exp law_exp;
 208    match while (exp)
 209    {  MARKEDexp(_,e):  { exp = e; }
 210    |  IDexp id:        { return make_term(exp,id,#[]); }
 211    |  CONSexp(cons,#[],NOexp):
 212       { return make_term(exp,cons->name,#[]); }
 213    |  CONSexp(cons,#[],TUPLEexp es):
 214       { return make_term(exp,cons->name,es); }
 215    |  CONSexp(cons,#[],e):
 216       { return make_term(exp,cons->name,#[e]); }
 217    |  LISTexp(cons, nil, #[h], t):
 218       { Exp nil_exp = t == NOexp ? CONSexp(nil,#[],NOexp) : t;
 219         nil_exp->ty = exp->ty;
 220         return make_term(exp,cons->name,#[h,nil_exp]);
 221       }
 222    |  LISTexp(cons, nil, #[h ... t], tail):
 223       { Exp e2 = LISTexp(cons, nil, t, tail);
 224         e2->ty = exp->ty;
 225         return make_term(exp,cons->name,#[h,e2]);
 226       }
 227    |  APPexp(IDexp id,TUPLEexp es):
 228       { law_exp = DatatypeCompiler::lookup_law(id,es);
 229         if (law_exp == NOexp) return make_term(exp,id,es);
 230         type_of(law_exp);
 231         exp = law_exp;
 232       }
 233    |  APPexp(IDexp id,e):
 234       { law_exp = DatatypeCompiler::lookup_law(id,#[e]);
 235         if (law_exp == NOexp) return make_term(exp,id,#[e]);
 236         type_of(law_exp);
 237         exp = law_exp;
 238       }
 239    |  LITERALexp l | Fmap.literal_map.contains(l):
 240       { return CONSterm(Fmap.literal_map[l],0,0,0); }
 241    |  exp | is_pattern_var(exp): { return make_term_var(NOpat,exp); }
 242    |  exp:                       { return CODEterm(exp); }
 243    }
 244 }
 245
 246 ///////////////////////////////////////////////////////////////////////////////
 247 //
 248 //  Method to create the rhs
 249 //
 250 ///////////////////////////////////////////////////////////////////////////////
 251 Term TRS::make_term(Exp exp, Id id, Exps exps)
 252 {  int n = length(exps);
 253    Cons cons = find_cons(id);
 254    if (cons == NOcons) { return CODEterm(exp); }
 255    FunctorTable::Entry * E = Fmap.type_map.lookup(exp->ty);
 256    if (E == 0) { return CODEterm(exp); }
 257    match (cons->alg_ty)
 258    {  DATATYPEty({ unit ... },_):
 259       {  Functor f = Fmap.type_map.value(E) + cons->tag +
 260                          (cons->ty == NOty ? 0 : unit);
 261          return CONSterm(f,cons,n,make_term(exps));
 262       }
 263    |  _:  { bug("TRS::make_term"); return CODEterm(exp); }
 264    }
 265 }
 266
 267 ///////////////////////////////////////////////////////////////////////////////
 268 //
 269 //  Method to create the term variable
 270 //
 271 ///////////////////////////////////////////////////////////////////////////////
 272 Term TRS::make_term_var(Pat pat, Exp exp)
 273 {  for (int i = 0; i < num_vars; i++)
 274    {  if (equal(exp,vars[i])) return VARterm(i,var_pats[i],vars[i]); }
 275    if (pat == NOpat) { return CODEterm(exp); }
 276    if (num_vars == MAX_VARS)
 277       bug("%LTRS::make_term_var() too many variables");
 278    vars[num_vars] = exp;
 279    var_pats[num_vars] = pat;
 280    return VARterm(num_vars++,pat,exp);
 281 }
 282
 283 ///////////////////////////////////////////////////////////////////////////////
 284 //
 285 //  Method to create the term from a list of expressions
 286 //
 287 ///////////////////////////////////////////////////////////////////////////////
 288 Term * TRS::make_term(Exps exps)
 289 {  int n = length(exps);
 290    Term * args = (Term *)mem_pool.m_alloc(sizeof(Term) * n);
 291    int i = 0;
 292    for_each(Exp, e, exps) args[i++] = make_term(e);
 293    return args;
 294 }
 295
 296 /////////////////////////////////////////////////////////////////////////////// //
 297 //
 298 //  Method to print a term
 299 //
 300 ///////////////////////////////////////////////////////////////////////////////
 301 void TRS::print (std::ostream& s, Term term) const
 302 {  match (term)
 303    {  CONSterm(f,cons,2,args) | is_list_constructor(cons):
 304       {  s << '#' << cons->name[1];
 305          Term t = term;
 306          Id comma = "";
 307          match while (t)
 308          {  CONSterm(g,cons2,2,args) | g == f:
 309             {  s << comma; print(s,args[0]); t = args[1]; comma = ", "; }
 310          }
 311          match (t)
 312          {  CONSterm(g,nil,0,args)
 313               | cons && is_list_constructor(nil): // skip
 314          |  _:   { s << comma; print(s,t); }
 315          }
 316          s << cons->name[5];
 317       }
 318    |  CONSterm(f,cons,arity,args):
 319       {  s << (cons != NOcons ? cons->name : Fmap.G.functor_name(f));
 320          if (arity > 0)
 321          {  s << '(';
 322             for (int i = 0; i < arity; i++)
 323             {  print(s,args[i]);
 324                if (i < arity - 1) s << ", ";
 325             }
 326             s << ')';
 327          }
 328       }
 329    |  VARterm(v,pat,_): { s << pat; }
 330    |  CODEterm(exp):    { Bool save = pretty_print_exp;
 331                           pretty_print_exp = true;
 332                           s << "[[" << exp << "]]";
 333                           pretty_print_exp = save;
 334                         }
 335    |  OPAQUEterm _:     { s << "..."; }
 336    |  PATterm pat:      { s << "[[" << pat << "]]"; }
 337    }
 338 }
 339
 340 ///////////////////////////////////////////////////////////////////////////////
 341 //
 342 //  Method to print a TRS
 343 //
 344 ///////////////////////////////////////////////////////////////////////////////
 345 void TRS::print (std::ostream& s) const
 346 {  s << "\n\nBottom-up term rewriting system:\n";
 347    Bool save = pretty_print_exp;
 348    pretty_print_exp = true;
 349    for (Rule r = 0; r < number_of_rules; r++)
 350    {  MatchRule rule = rule_map[r];
 351       s << "line " << rule->begin_line << ": ";
 352       print(s,lhs_map[r]);
 353       if (guard_map[r] != NOexp) s << " | " << guard_map[r];
 354       s << ":\n\t"; print(s,rhs_map[r]); s << '\n';
 355       for (int i = 0; i < num_var_map[r]; i++)
 356       {  Pat pat_var = var_pat_map[r][i];
 357          Ty pat_ty   = pat_var->ty;
 358          s << "\tvariable " << pat_var << " : " << pat_ty;
 359          if (! compiler.has_index(pat_ty)) s << " has no index";
 360          s << '\n';
 361       }
 362       s << '\n';
 363    }
 364    s << '\n';
 365    pretty_print_exp = save;
 366 }