prop-src/datagen.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file implements the datatype compiler of Prop.
   4 //
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #include <iostream.h>
   8 #include <AD/strings/quark.h>
   9 #include "ir.ph"
  10 #include "ast.ph"
  11 #include "type.h"
  12 #include "datagen.h"
  13 #include "options.h"
  14 #include "datatype.ph"
  15 #include "list.h"
  16
  17 ///////////////////////////////////////////////////////////////////////////////
  18 //
  19 //  Constructor and destructors for datatype compiler
  20 //
  21 ///////////////////////////////////////////////////////////////////////////////
  22 int DatatypeCompiler::max_embedded_tags = 0;
  23 int DatatypeCompiler::max_embedded_bits = 0;
  24 LabelGen DatatypeCompiler::temp_vars("_T");
  25
  26 DatatypeCompiler:: DatatypeCompiler(TyOpt opt, int embedded_tags)
  27    : optimizations(opt)
  28      {  max_embedded_tags = embedded_tags;
  29         max_embedded_bits = 0;
  30         for (int i = embedded_tags - 1; i > 0; i >>= 1)
  31            max_embedded_bits++;
  32      }
  33 DatatypeCompiler::~DatatypeCompiler() {}
  34
  35 ///////////////////////////////////////////////////////////////////////////////
  36 //
  37 //  Method to create a datatype hierarchy
  38 //
  39 ///////////////////////////////////////////////////////////////////////////////
  40 static DatatypeHierarchy * create_datatype_hierarchy
  41    (Id name, TyVars parameters, Inherits inhs, TyQual qual,
  42     TermDefs terms, Decls body)
  43 {
  44    match (lookup_ty(name))
  45    {  DATATYPEty({ hierarchy ... }, _): { return hierarchy; }
  46    |  _:
  47       { return new DatatypeHierarchy(name,parameters,inhs,qual,terms,body); }
  48    }
  49 }
  50
  51 ///////////////////////////////////////////////////////////////////////////////
  52 //
  53 //  Top level method to map datatype and type definitions into
  54 //  a C++ class hierarchy.
  55 //
  56 ///////////////////////////////////////////////////////////////////////////////
  57 void DatatypeCompiler::gen_datatype
  58    ( DatatypeDefs data_defs,   // datatype definitions
  59      ViewDefs     view_defs,   // view definitions
  60      LawDefs      law_defs,    // law definitions
  61      TyDefs       ty_defs      // type definitions
  62    )
  63 {
  64    // Build the classes hierarchies
  65    int N = length(data_defs);
  66    DatatypeHierarchy ** H = new DatatypeHierarchy * [N];
  67    {  int i = 0;
  68       for_each (DatatypeDef, d, data_defs)
  69       {  match (d)
  70          {  DATATYPEdef(name,tvs,inh,q,terms,body):
  71             {  H[i] = create_datatype_hierarchy(name,tvs,inh,q,terms,body);
  72                i++;
  73             }
  74          }
  75       }
  76    }
  77
  78    // Generate forward datatype definitions
  79    {  for (int i = 0; i < N; i++)
  80          if (H[i]) H[i]->generate_forward_declarations(*this);
  81    }
  82
  83    //  Generate type definitions
  84    {  for_each (TyDef, t, ty_defs) gen_type_def(t); }
  85
  86    //  Generate the class hierarchies
  87    {  for (int i = 0; i < N; i++)
  88          if (H[i]) H[i]->generate_datatype_definitions(*this);
  89    }
  90
  91    //  Compile the pattern laws
  92    gen_law_defs(law_defs);
  93 }
  94
  95 ///////////////////////////////////////////////////////////////////////////////
  96 //
  97 //  Method to generate a type definition
  98 //
  99 ///////////////////////////////////////////////////////////////////////////////
 100 void DatatypeCompiler::gen_type_def (TyDef ty_def)
 101 {  match (ty_def)
 102    {  TYdef(id,tyvars,ty,generative) | generative:
 103       {  pr ("%^%/%^// Definition of type %s%V%^%/"
 104              "%#"
 105              "%^%^typedef %t;\n\n",
 106              id, tyvars, ty_def->begin_line, ty_def->file_name, ty, id);
 107       }
 108    |  _: /* skip */
 109    }
 110 }
 111
 112 ///////////////////////////////////////////////////////////////////////////////
 113 //
 114 //  Method to preprocess a datatype (for constraints)
 115 //
 116 ///////////////////////////////////////////////////////////////////////////////
 117 void DatatypeCompiler::preprocess_def (DatatypeDef def)
 118 {  match (def) of
 119       DATATYPEdef (id,tyvars,_,qual,terms,_) | qual & QUALunifiable:
 120       {  Id      var_term_name = Quark(id,"_var");
 121          TermDef var_term = TERMdef'{ id   = var_term_name,
 122                                       ty   = mkidvarty(id,tyvars),
 123                                       qual = QUALvariable
 124                                     };
 125          terms = #[ var_term ... terms ];
 126          // msg("[Unifiable datatype %s]\n", id);
 127       }
 128    |  _: // skip otherwise
 129    end match;
 130 }