app/willard/proj.pcc

   1 #include <AD/pretty/postream.h>
   2 #include "proj.ph"
   3 #include "list.ph"
   4
   5 ///////////////////////////////////////////////////////////////////////////////
   6 //
   7 //  Constructor and destructor for projection recognition
   8 //
   9 ///////////////////////////////////////////////////////////////////////////////
  10 Projection::Projection() {}
  11 Projection::~Projection() {}
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  Method to invoke projection recognition
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 Exp Projection::projection_recognition(Exp e)
  19 { message("Projection recognition phase", e); (*this)(e); return e;
  20 }
  21
  22 ///////////////////////////////////////////////////////////////////////////////
  23 //
  24 //  Method to create a projection
  25 //
  26 ///////////////////////////////////////////////////////////////////////////////
  27 Exp Projection::make_projection
  28    (const IdSet& Invisible, Ids xs, Exps As, Exp P, Exp exp)
  29 {  Ids  visible_xs = #[];
  30    Exps visible_As = #[];
  31    match while (xs) and (As) of
  32       #[a ... b], #[c ... d]:
  33       {  if (Invisible.contains(a))
  34          {  P = EXISTS(a,c,P); }
  35          else
  36          {  visible_xs = #[a ... visible_xs];
  37             visible_As = #[c ... visible_As];
  38          }
  39          xs = b; As = d;
  40       }
  41    end match;
  42    changed = true;
  43    Exp body = P == True ? exp : GUARD(P,exp);
  44    return GENERATOR(rev(visible_xs),rev(visible_As),body);
  45 }
  46
  47 ///////////////////////////////////////////////////////////////////////////////
  48 //
  49 //  Transformation to recongize projections and transform them into
  50 //  existential queries.  Assume the set comprehensions are in flatten form.
  51 //
  52 ///////////////////////////////////////////////////////////////////////////////
  53 rewrite Projection
  54 {
  55 //
  56 // Locate all set comprehension quantifiers.
  57 //
  58 // { es : xs in As | p }  where FV(xs) - FV(es) > 0
  59 //
  60    GENERATOR(xs,As,GUARD(p,e)) | length(xs) == length(As):
  61    {  IdSet S1;
  62       IdSet S2;
  63       free_vars(xs,S1);
  64       free_vars(e,S2);
  65       remove_vars(S1,S2);
  66       if (S1.size() > 0) rewrite(make_projection(S1,xs,As,p,e));
  67    }
  68 |  GENERATOR(xs,As,e) | length(xs) == length(As):
  69    {  IdSet S1;
  70       IdSet S2;
  71       free_vars(xs,S1);
  72       free_vars(e,S2);
  73       remove_vars(S1,S2);
  74       if (S1.size() > 0) rewrite(make_projection(S1,xs,As,True,e));
  75    }
  76 };