prop-src/lawgen.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  Module to generate law abbreviations.
   4 //
   5 ///////////////////////////////////////////////////////////////////////////////
   6 #include "ir.ph"
   7 #include "ast.ph"
   8 #include "datagen.h"
   9 #include "type.h"
  10 #include "hashtab.h"
  11 #include "list.h"
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  Law environment.
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 HashTable DatatypeCompiler::law_env(string_hash,string_equal);
  19
  20 ///////////////////////////////////////////////////////////////////////////////
  21 //
  22 //  Method to lookup a pattern law.
  23 //
  24 ///////////////////////////////////////////////////////////////////////////////
  25 Pat DatatypeCompiler::lookup_pat (Id id)
  26 {  HashTable::Entry * e = law_env.lookup(id);
  27    return e ? (Pat)e->v : NOpat;
  28 }
  29
  30 ///////////////////////////////////////////////////////////////////////////////
  31 //
  32 //  Method to enter a new pattern
  33 //
  34 ///////////////////////////////////////////////////////////////////////////////
  35 void DatatypeCompiler::add_law(LawDef law_def)
  36 {  match (law_def)
  37    {  LAWdef { id, args, pat, guard, invert ... }:
  38       {  if (lookup_pat(id) != NOpat) {
  39             error ("%Lduplicated definition of pattern constructor '%s'\n",id);
  40          } else {
  41             // type check pattern
  42             Pat p = guard != NOexp ? GUARDpat(p,guard) : pat;
  43             law_env.insert(id, POLYpat(id, length(args), args, p, guard,
  44                            invert));
  45          }
  46       }
  47    }
  48 }
  49
  50 ///////////////////////////////////////////////////////////////////////////////
  51 //
  52 //  Function 'invertible' checks whether a pattern is invertible into
  53 //  a pseudo constructor.
  54 //
  55 ///////////////////////////////////////////////////////////////////////////////
  56 fun invertible NOpat || IDpat _ || LITERALpat _ || INDpat _
  57             || CONSpat _ : Bool:       { return true; }
  58   | invertible WILDpat _ || APPENDpat _ || LOGICALpat _ || ARRAYpat _:
  59                                        { return false; }
  60   | invertible APPpat(CONSpat _,p):    { return invertible(p); }
  61   | invertible TYPEDpat(p,_):          { return invertible(p); }
  62   | invertible ASpat(_,p,_,_):         { return invertible(p); }
  63   | invertible CONTEXTpat(_,p):        { return invertible(p); }
  64   | invertible TUPLEpat ps:            { return invertible(ps); }
  65   | invertible EXTUPLEpat ps:          { return invertible(ps); }
  66   | invertible RECORDpat(ps,flex):     { return ! flex && invertible(ps); }
  67   | invertible GUARDpat(p,_):          { return invertible(p); }
  68   | invertible MARKEDpat(_,p):         { return invertible(p); }
  69   | invertible LISTpat { head, tail ... }:
  70      { return invertible(head) && invertible(tail); }
  71   | invertible VECTORpat { len, array, elements, head_flex, tail_flex ... }:
  72      { return ! head_flex && ! tail_flex &&
  73                 invertible(len) && invertible(array) && invertible(elements);
  74      }
  75   | invertible p: { bug("invertible: %p", p); return false; }
  76
  77 and invertible (#[] : Pats): Bool: { return true; }
  78   | invertible #[a ... b]:         { return invertible(a) && invertible(b); }
  79
  80 and invertible (#[] : LabPats): Bool: { return true; }
  81   | invertible #[a ... b]:   { return invertible(a.pat) && invertible(b); }
  82 ;
  83
  84 ///////////////////////////////////////////////////////////////////////////////
  85 //
  86 //  Function to convert a pattern into a variable creation expression.
  87 //
  88 ///////////////////////////////////////////////////////////////////////////////
  89 Exp mkvariable (Pat p)
  90 {  match (deref_all(p->ty))
  91    {  DATATYPEty({ qualifiers, terms, unit ... },_)
  92        | qualifiers & QUALunifiable:
  93       {  return APPexp(IDexp(terms[unit]->name),TUPLEexp(#[])); }
  94    |  _: { error("%L%p with type %T is not unifiable\n", p, p->ty);
  95            return NOexp;
  96          }
  97    }
  98 }
  99
 100 ///////////////////////////////////////////////////////////////////////////////
 101 //
 102 //  Function 'pat2exp' converts an invertible pattern into a
 103 //  constructor expression.  Also extracts the bound variable bindings
 104 //  at the same time.
 105 //
 106 ///////////////////////////////////////////////////////////////////////////////
 107 static List<.[Id,Ty]> boundvars = #[];
 108 static Exps           actual_args = #[];
 109 static Bool           application_error = false;
 110 Bool   write_mode = false;
 111
 112 fun pat2exp NOpat: Exp:          { return NOexp; }
 113   | pat2exp p as IDpat(id,_,_):
 114        { return write_mode ? mkvariable(p) : IDexp(id); }
 115   | pat2exp INDpat(id,i,_) | actual_args != #[]:
 116        {  int k = 0;
 117           for_each(Exp, e, actual_args)
 118           {  if (k == i) return e;
 119              k++;
 120           }
 121           error("%LMissing argument %i in law variable %s\n",i,id);
 122           application_error = true;
 123           return NOexp;
 124        }
 125   | pat2exp INDpat(id,_,ty):
 126        { boundvars = #[.(id,ty) ... boundvars];
 127          return IDexp(id);
 128        }
 129   | pat2exp LITERALpat l:        { return LITERALexp(l); }
 130   | pat2exp TYPEDpat(p,_):       { return pat2exp(p); }
 131   | pat2exp ASpat(_,p,_,_):      { return pat2exp(p); }
 132   | pat2exp CONTEXTpat(_,p):     { return pat2exp(p); }
 133   | pat2exp TUPLEpat ps:         { return TUPLEexp(pat2exp(ps)); }
 134   | pat2exp EXTUPLEpat ps:       { return EXTUPLEexp(pat2exp(ps)); }
 135   | pat2exp RECORDpat(ps,_):     { return RECORDexp(pat2exp(ps)); }
 136   | pat2exp GUARDpat(p,e):       { return pat2exp(p); }
 137   | pat2exp MARKEDpat(_,p):      { return pat2exp(p); }
 138   | pat2exp CONSpat(ONEcons{name...}): { return IDexp(name); }
 139   | pat2exp APPpat(CONSpat c,e): { return CONSexp(c,#[],pat2exp(e)); }
 140   | pat2exp LISTpat { cons, nil, head, tail ... }:
 141       { return LISTexp(cons,nil,pat2exp(head),pat2exp(tail)); }
 142   | pat2exp VECTORpat { cons, elements ... }:
 143       { return VECTORexp(cons,pat2exp(elements)); }
 144   | pat2exp p as WILDpat _ | write_mode:
 145       { return mkvariable(p); }
 146   | pat2exp p: { bug("pat2exp: %p", p); return NOexp; }
 147
 148 and pat2exp (#[]: Pats): Exps: { return #[]; }
 149   | pat2exp #[a ... b]:        { return #[pat2exp(a) ... pat2exp(b)]; }
 150
 151 and pat2exp (#[] : LabPats): LabExps: { return #[]; }
 152   | pat2exp #[a ... b]:               { LabExp labexp;
 153                                         labexp.label = a.label;
 154                                         labexp.exp   = pat2exp(a.pat);
 155                                         return #[ labexp ... pat2exp(b) ];
 156                                       }
 157
 158 and pat2constructor (p : Pat) : Exp:
 159     {  Bool mode_save = write_mode;
 160        write_mode = false;
 161        Exp  e = pat2exp(p);
 162        write_mode = mode_save;
 163        return e;
 164     }
 165
 166 and pat2unifier (p : Pat) : Exp:
 167     {  Bool mode_save = write_mode;
 168        write_mode = true;
 169        Exp  e = pat2exp(p);
 170        write_mode = mode_save;
 171        return e;
 172     }
 173 ;
 174
 175 ///////////////////////////////////////////////////////////////////////////////
 176 //
 177 //  Method to lookup a pattern law.
 178 //
 179 ///////////////////////////////////////////////////////////////////////////////
 180 Exp DatatypeCompiler::lookup_law (Id id, Exps args)
 181 {  Pat pat = lookup_pat(id);
 182    match (pat)
 183    {  POLYpat(id,arity,_,pat,guard,invert) | invert == true:
 184       {  {  if (invertible(pat) && guard == NOexp)
 185             {  actual_args = args;
 186                application_error = false;
 187                if (arity != length(args))
 188                {  error("%Larity mismatch between law %p and arguments %f\n",
 189                         pat, TUPLEexp(args));
 190                   return NOexp;
 191                }
 192                Exp exp = pat2exp(pat);
 193                actual_args = #[];
 194                if (application_error)
 195                   error("%Lcannot apply law %p with arguments %f\n",
 196                         pat, TUPLEexp(args));
 197                return exp;
 198             } else
 199             {  error ("%Llaw %s(...) = %p is not invertible\n",id,pat);
 200             }
 201          }
 202       }
 203    |  _: // skip
 204    }
 205    return NOexp;
 206 }
 207
 208 ///////////////////////////////////////////////////////////////////////////////
 209 //
 210 //  Method to generate pattern law definitions
 211 //
 212 ///////////////////////////////////////////////////////////////////////////////
 213 void DatatypeCompiler::gen_law_defs (LawDefs law_defs)
 214 {
 215    for_each (LawDef, l, law_defs)
 216    {  match (l)
 217       {  LAWdef{id,args,guard,pat,ty,invert}:
 218          {  l->set_loc();
 219
 220             // infer the type of the pattern.
 221             ty = type_of(pat);
 222
 223             // If the law is invertible, generate
 224             // code for the laws
 225             if (invert)
 226             {  if (invertible(pat) && guard == NOexp)
 227                {  boundvars = #[];
 228                   gen_law_inverse(l->loc(),id,args,pat2constructor(pat),ty);
 229                   boundvars = #[];
 230                } else
 231                {  error ("%Llaw %s(...) = %p is not invertible\n",id,pat);
 232                }
 233             }
 234          }
 235       }
 236    }
 237 }
 238
 239 ///////////////////////////////////////////////////////////////////////////////
 240 //
 241 //  Check if type can be a C++ parameter
 242 //
 243 ///////////////////////////////////////////////////////////////////////////////
 244 Bool is_parameter_type (Ty ty)
 245 {  match (deref ty)
 246    {  TYCONty(RECORDtycon _ || TUPLEtycon || ARRAYtycon _,_): return false;
 247    |  _: return true;
 248    }
 249 }
 250
 251
 252 ///////////////////////////////////////////////////////////////////////////////
 253 //
 254 //  Method to generate an inverse for a law definition
 255 //
 256 ///////////////////////////////////////////////////////////////////////////////
 257 void DatatypeCompiler::gen_law_inverse
 258    (const Loc * location, Id id, Ids args, Exp exp, Ty ty)
 259 {   // Generate the header name
 260     pr("%^%/"
 261        "%^// Definition of law %s"
 262        "%^%/"
 263        "%#"
 264        "%^inline %t(",
 265        id, location->begin_line, location->file_name, ty, id);
 266
 267     // Generate the parameters
 268     Bool comma = false;
 269     match while (args)
 270     {  #[ arg ... rest ]:
 271        {  if (comma) pr(", ");
 272           List<.[Id,Ty]> bvs = boundvars;
 273           Bool found = false;
 274           Bool mode_save = write_mode;
 275           write_mode = false;
 276           match while (bvs)
 277           {  #[.(v,ty) ... others]:
 278              {  if (v == arg)
 279                 {  if (! is_parameter_type(ty))
 280                    { error("%Llaw '%s': type %T cannot be used in parameter %s\n",
 281                            id, ty,v);
 282                    }
 283                    found = true; pr("%t",ty,v);
 284                    bvs = #[];
 285                 }
 286                 else bvs = others;
 287              }
 288           }
 289           if (! found)
 290              error("%Llaw '%s': bound variable '%s' is absent in body %e\n",
 291                    id, arg, exp);
 292           args  = rest;
 293           comma = true;
 294           write_mode = mode_save;
 295        }
 296     }
 297
 298     // Generate the body
 299    pr(")%^{ return %e; }\n\n", exp);
 300 }