prop-src/pat.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file implements the analysis routines for patterns and match
   4 //  decision trees.  These are used for mode analysis and determinism
   5 //  analysis for logic clauses compilation.
   6 //
   7 ///////////////////////////////////////////////////////////////////////////////
   8 #include "ir.ph"
   9 #include "matchcom.ph"
  10 #include "pat.ph"
  11
  12 ///////////////////////////////////////////////////////////////////////////////
  13 //
  14 //  Convert a pattern into an unifier if the constructor is part of
  15 //  an unifiable type.
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 Pat mkunifier (Cons cons, Pat pat, Pat transformed_pat)
  19 {  match (cons)
  20    {  ONEcons { alg_ty = DATATYPEty({ qualifiers, terms, unit ... },_) ... }
  21           | qualifiers & QUALunifiable:
  22       {  Cons unifier_cons = terms[unit];
  23          Bool mode_save = write_mode;
  24          write_mode = true;
  25          Pat new_p = LOGICALpat(ORpat,transformed_pat,
  26                         UNIFYpat(APPpat(CONSpat(unifier_cons),WILDpat()),
  27                                  pat2unifier(pat)));
  28          write_mode = mode_save;
  29          return new_p;
  30       }
  31    |  _:  { return pat; }
  32    }
  33 }
  34
  35 ///////////////////////////////////////////////////////////////////////////////
  36 //
  37 //  Convert a simple pattern into an unifier.
  38 //
  39 ///////////////////////////////////////////////////////////////////////////////
  40 Pat unifier_of (Pat pat)
  41 {  Pat new_p = pat;
  42    match (pat)
  43    { NOpat || WILDpat _ || IDpat _ ||
  44      LITERALpat _ || CONTEXTpat _ || LEXEMEpat _: // skip
  45    | CONSpat cons:    { new_p = mkunifier(cons,pat,pat); }
  46    | APPpat(a as CONSpat c,b):
  47                       { new_p = mkunifier(c,pat,APPpat(a,unifier_of(b))); }
  48    | TYPEDpat(p, t):  { new_p = TYPEDpat(unifier_of(p),t); }
  49    | ASpat(id,p,t,e): { new_p = ASpat(id,unifier_of(p),t,e); }
  50    | ARRAYpat(ps,f):  { new_p = ARRAYpat(unifier_of(ps),f); }
  51    | TUPLEpat ps:     { new_p = TUPLEpat(unifier_of(ps)); }
  52    | EXTUPLEpat ps:   { new_p = EXTUPLEpat(unifier_of(ps)); }
  53    | RECORDpat(ps,f): { new_p = RECORDpat(unifier_of(ps),f); }
  54    | GUARDpat(p, e):  { new_p = GUARDpat(unifier_of(p),e); }
  55    | LISTpat { cons, nil, head, tail }:
  56                       { new_p = LISTpat'{cons = cons, nil = nil,
  57                                          head = unifier_of(head),
  58                                          tail = unifier_of(tail)};
  59                       }
  60    | VECTORpat { cons, len, array, elements, head_flex, tail_flex }:
  61                       { new_p = VECTORpat'{ cons     = cons,
  62                                             len      = unifier_of(len),
  63                                             array    = unifier_of(array),
  64                                             elements = unifier_of(elements),
  65                                             head_flex = head_flex,
  66                                             tail_flex = tail_flex
  67                                           };
  68                       }
  69    | LOGICALpat (cont, a, b):
  70                   { new_p = LOGICALpat(cont,unifier_of(a),unifier_of(b)); }
  71    | MARKEDpat  (l, p): { new_p = MARKEDpat(l, unifier_of(p)); }
  72    | _:                 { bug ("%Lunsupported unifier: %p", pat); }
  73    }
  74    if (new_p != pat && boxed(pat) && boxed(new_p))
  75    {  new_p->selector = pat->selector;
  76       new_p->ty       = pat->ty;
  77    }
  78    return new_p;
  79 }
  80
  81 ///////////////////////////////////////////////////////////////////////////////
  82 //
  83 //  Convert a simple pattern list into an unifier list.
  84 //
  85 ///////////////////////////////////////////////////////////////////////////////
  86 Pats unifier_of (Pats pats)
  87 {  match (pats)
  88    { #[]:        { return #[]; }
  89    | #[h ... t]: { return #[unifier_of(h) ... unifier_of(t)]; }
  90    }
  91 }
  92
  93 ///////////////////////////////////////////////////////////////////////////////
  94 //
  95 //  Convert a simple labeled pattern list into an labeled unifier list.
  96 //
  97 ///////////////////////////////////////////////////////////////////////////////
  98 LabPats unifier_of (LabPats pats)
  99 {  match (pats)
 100    { #[]:        { return #[]; }
 101    | #[h ... t]: { LabPat lab_pat;
 102                    lab_pat.label = h.label;
 103                    lab_pat.pat   = unifier_of(h.pat);
 104                    return #[ lab_pat ... unifier_of(t) ];
 105                  }
 106    }
 107 }
 108 ///////////////////////////////////////////////////////////////////////////////
 109 //
 110 //  Check whether pattern a subsumes b, i.e. more general.
 111 //
 112 ///////////////////////////////////////////////////////////////////////////////
 113 Bool subsumes (Pat a, Pat b, Bool v)
 114 {  match (a) and (b)
 115    {  WILDpat _ || IDpat _, _:     { return true; }
 116    |  BACKEDGEpat(_,_,a), _:       { return subsumes(a,b,v); }
 117    |  LITERALpat i, LITERALpat j:  { return literal_equal(i,j); }
 118    |  TUPLEpat a,   TUPLEpat b:    { return subsumes(a,b,v); }
 119    |  EXTUPLEpat a, EXTUPLEpat b:  { return subsumes(a,b,v); }
 120    |  ASpat(_,a,_,_), _:           { return subsumes(a,b,v); }
 121    |  _,           ASpat(_,b,_,_): { return subsumes(a,b,v); }
 122    |  TYPEDpat(a,_),  _:           { return subsumes(a,b,v); }
 123    |  _,           TYPEDpat(b,_):  { return subsumes(a,b,v); }
 124    |  CONSpat c,   CONSpat d:      { return c == d; }
 125    |  APPpat(a,b), APPpat(c,d): { return subsumes(a,c,v) && subsumes(b,d,v); }
 126    |  GUARDpat(a,b), GUARDpat(c,d): { return subsumes(a,c,v) && equal(b,d); }
 127    |  LOGICALpat(ORpat,x,y), b:  { return subsumes(x,b,v) && subsumes(y,b,v); }
 128    |  _,           _:              { return false; }
 129    }
 130 }
 131
 132 ///////////////////////////////////////////////////////////////////////////////
 133 //
 134 //  Checks whether list a subsumes list b.  Subsumption is computed
 135 //  componentwise.
 136 //
 137 ///////////////////////////////////////////////////////////////////////////////
 138 Bool subsumes (Pats a, Pats b, Bool v)
 139 {  match (a) and (b)
 140    {  #[],        #[]:        { return true; }
 141    |  #[m ... n], #[o ... p]: { return subsumes(m,o,v) && subsumes(n,p,v); }
 142    |  _,          _:          { return false; }
 143    }
 144 }
 145
 146 ///////////////////////////////////////////////////////////////////////////////
 147 //
 148 //  Computes the subsumption info for two labeled pat lists.
 149 //
 150 ///////////////////////////////////////////////////////////////////////////////
 151 Bool subsumes (LabPats, LabPats, Bool verbose)
 152 {  return false;
 153 }