prop-src/indexing.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  Indexing optimizations for pattern matching.
   3 //
   4 //  The following indexing schemes is largely inspired by the work of
   5 //  Sekar, Ramesh and Ramakrishnan in ``Adaptive Pattern Matching.''
   6 //  Techreport, SUNY at Stony Brook (year 91+ but unknown).
   7 //
   8 //  Intuitively, an index is the next position of a pattern that must be
   9 //  inspected to determine a match(Levy and Huet).  Given a set of
  10 //  prioritized patterns, at least an index must exist at each position.
  11 //  The algorithm of SRR attempts to locate the index at each position
  12 //  when constructing the the DFA-like matching automata.
  13 //
  14 //  In the previous algorithm I've implemented, merging of matching trees at
  15 //  identical positions are performed and the resulting automaton guarantees
  16 //  that the same position is only examined once.  This is an improvement
  17 //  over Wadler's algorithm, which may examine the same position more than
  18 //  once in a match.  However, we may examine a position even if it is not
  19 //  needed.
  20 //
  21 //    For example, in
  22 //
  23 //       f(_,a,b):
  24 //       f(a,a,_):
  25 //       f(_,b,c):
  26 //
  27 //   We exam position 1, 2, 3 in sequence in term f even though it is
  28 // best to exam position 2 first.
  29 //
  30 //  I think my algorithm is similar to the one by Graf.  In any case,
  31 //  My, Graf's and Wadler's algorithms all use a fixed traversal order
  32 //  (usually left-to-right).  However, the intuition is that in many instances
  33 //  it is best if the traversal order *adapts* itself according to the
  34 //  pattern.  This is the essential idea of SRR's algorithm.
  35 //
  36 //  Sekar et al. have shown that constructing a DFA-like matching
  37 //  automata can be exponential in time and space.  They have
  38 //  developed a polynomial time algorithm for computing indices for untyped
  39 //  terms.  Unfortunately, in our typed case the time complexity of index
  40 //  computation is co-NP.
  41 //
  42 //  So we'll just use a few heuristics to compute something close to
  43 //  the notion of an index, and cross our fingers and hope for the best.
  44 ///////////////////////////////////////////////////////////////////////////////
  45 #include "ir.ph"
  46 #include "ast.ph"
  47 #include "matchcom.ph"
  48 #include "hashtab.h"
  49
  50 ///////////////////////////////////////////////////////////////////////////////
  51 //
  52 //  Hash function on position list
  53 //
  54 ///////////////////////////////////////////////////////////////////////////////
  55 unsigned int pos_hash (HashTable::Key p)
  56 {  Pos pos = (Pos)p;
  57    unsigned int h = 37;
  58    match while (pos)
  59    {  POSzero:            { return h; }
  60    |  POSinfinity:        { return h + 83; }
  61    |  POSint(i,p):        { h += i; pos = p; }
  62    |  POSlabel(l,p):      { h += (unsigned int)l; pos = p; }
  63    |  POSadaptive(i,_,p): { h += i + 437; pos = p; }
  64    }
  65 }
  66
  67 ///////////////////////////////////////////////////////////////////////////////
  68 //
  69 //  Checks if a pattern is refutable.
  70 //
  71 ///////////////////////////////////////////////////////////////////////////////
  72 Bool is_refutable(Pat pat)
  73 {  match while (pat)
  74    {  NOpat || WILDpat _ || IDpat(_,_,NOexp): { return false; }
  75    |  IDpat(_,_,! NOexp) || ASpat(_,_,_,! NOexp)
  76       || LITERALpat _ || LEXEMEpat _:    { return true; }
  77    |  ASpat(_,p,_,_):     { pat = p; }
  78    |  TYPEDpat(p,_):      { pat = p; }
  79    |  MARKEDpat(_,p):     { pat = p; }
  80    |  LOGICALpat (_,a,b): { return is_refutable(a) || is_refutable(b); }
  81    |  TUPLEpat ps:        { return is_refutable(ps); }
  82    |  ARRAYpat (ps,_):    { return is_refutable(ps); }
  83    |  VECTORpat { elements = ps, len = p ... }:
  84                           { return is_refutable(p) || is_refutable(ps); }
  85    |  RECORDpat (ps,_):   { return is_refutable(ps); }
  86    |  CONTEXTpat(_,p):    { return is_refutable(p); }
  87    |  CONSpat(ONEcons {
  88                 alg_ty =
  89                    TYCONty(DATATYPEtycon{ unit, arg, qualifiers ... },_)
  90                 ...
  91               }):
  92       {  return ((unit + arg > 1) || (qualifiers & QUALextensible)); }
  93    |  APPpat(a,b):       { return is_refutable(a) || is_refutable(b); }
  94    |  LISTpat{cons,nil,head=ps,tail=p}:
  95       {  if (is_refutable(ps)) return true;
  96          pat = p;
  97       }
  98    |  _: { bug("is_refutable()"); }
  99    }
 100 }
 101
 102 ///////////////////////////////////////////////////////////////////////////////
 103 //
 104 //  Is a pattern list refutable?
 105 //
 106 ///////////////////////////////////////////////////////////////////////////////
 107 Bool is_refutable(Pats pats)
 108 {  for_each (Pat, p, pats) if (is_refutable(p)) return true;
 109    return false;
 110 }
 111
 112 ///////////////////////////////////////////////////////////////////////////////
 113 //
 114 //  Is a labeled pattern list refutable?
 115 //
 116 ///////////////////////////////////////////////////////////////////////////////
 117 Bool is_refutable(LabPats pats)
 118 {  for_each (LabPat, p, pats) if (is_refutable(p.pat)) return true;
 119    return false;
 120 }
 121
 122 ///////////////////////////////////////////////////////////////////////////////
 123 //
 124 //  Method to compute the indices.
 125 //
 126 ///////////////////////////////////////////////////////////////////////////////
 127 void indexing(int priority, Pat pat, Pos pos, HashTable& index_map)
 128 {  match while (pat)
 129    {  ASpat(_,p,_,_):  { pat = p; }
 130    |  TYPEDpat(p,_):   { pat = p; }
 131    |  MARKEDpat(_,p):  { pat = p; }
 132    |  CONTEXTpat(_,p): { pat = p; }
 133    |  APPpat(CONSpat(ONEcons {
 134                 tag, alg_ty = TYCONty(DATATYPEtycon { unit ... }, _)
 135                 ... }),p as ! NOpat):
 136       {  indexing(priority, p, POSint(tag + unit, pos), index_map); return; }
 137    |  TUPLEpat ps:     { indexing(priority, ps, pos, index_map); return; }
 138    |  ARRAYpat (ps,_): { indexing(priority, ps, pos, index_map); return; }
 139    |  VECTORpat { elements = ps, len = p ...}:
 140       { indexing(priority, #[ p ... ps ], pos, index_map); return; }
 141    |  RECORDpat (ps,_):
 142       {  for_each(LabPat, p, ps)
 143             indexing(priority, p.pat, POSlabel(p.label,pos), index_map);
 144          return;
 145       }
 146    |  LOGICALpat(_,a,b): { indexing(priority,a,pos,index_map); pat = b; }
 147    }
 148 }
 149
 150 ///////////////////////////////////////////////////////////////////////////////
 151 //
 152 //  Method to compute the indices.
 153 //
 154 ///////////////////////////////////////////////////////////////////////////////
 155 void indexing(int priority, Pats pats, Pos pos, HashTable& index_map)
 156 {  int n;
 157    Pat Ps[32];
 158
 159    int i = 0;
 160    // initialize the pattern array
 161    {  for_each (Pat, p, pats) Ps[i++] = p; }
 162    n = i;
 163    if (n <= 0 || n > 32) return;
 164
 165    // compute the set of index positions for this pattern list
 166    unsigned long indices = 0;
 167    for (i = 0; i < n; i++)
 168       if (is_refutable(Ps[i])) indices |= 1 << i;
 169
 170    // Locate the position ranking
 171    HashTable::Entry * e = index_map.lookup(pos);
 172    int * ranks;
 173    if (e) {
 174       // Heuristic to update the ranks given new index and priority
 175       // informations.
 176       ranks = (int*)index_map.value(e);
 177
 178    } else {
 179       // Initialize the new ranking array.
 180       // Put all used positions in front and
 181       // the rest the the back.
 182       ranks = (int*)mem_pool[n * sizeof(int)];
 183       int j = 0;
 184       for (i = 0; i < n; i++) if (indices & (1 << i))     ranks[j++] = i;
 185       for (i = 0; i < n; i++) if (! (indices & (1 << i))) ranks[j++] = i;
 186       index_map.insert(pos, ranks);
 187    }
 188
 189    // Recursive on subcomponents, and insert an adaptive rank.
 190    for (i = 0; i < n; i++)
 191       indexing(priority, Ps[i], POSadaptive(i,ranks,pos), index_map);
 192 }
 193
 194 ///////////////////////////////////////////////////////////////////////////////
 195 //
 196 //  Method to compute the indices information for a set of pattern matching
 197 //  rules.
 198 //
 199 ///////////////////////////////////////////////////////////////////////////////
 200 void indexing (MatchRules rules, HashTable& index_map)
 201 {  int priority = 0;
 202    for_each (MatchRule, r, rules)
 203    {  match (r)
 204       {  MATCHrule(_, pat, _, _, _):
 205          {  indexing(priority, pat, POSzero, index_map);
 206             priority++;
 207          }
 208       }
 209    }
 210 }