prop-src/trs.h

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.6),
   3 //  last updated on Nov 2, 1999.
   4 //  The original source file is "trs.ph".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_TUPLE2_USED
   8 #include <propdefs.h>
   9 #line 1 "trs.ph"
  10 ///////////////////////////////////////////////////////////////////////////////
  11 //
  12 //  Data structure for partial evaluting a TRS
  13 //
  14 ///////////////////////////////////////////////////////////////////////////////
  15
  16 #ifndef term_rewrite_system_h
  17 #define term_rewrite_system_h
  18
  19 #include <AD/automata/treeauto.h>
  20 #include "basics.h"
  21 #include "ir.h"
  22 #include "ast.h"
  23 #include <iostream>
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 //  Forward declarations
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 class FunctorMap;
  31 class RewritingCompiler;
  32 class CodeGen;
  33
  34 ///////////////////////////////////////////////////////////////////////////////
  35 //
  36 //  This class represents a rewriting term
  37 //
  38 ///////////////////////////////////////////////////////////////////////////////
  39 #line 30 "trs.ph"
  40 #line 36 "trs.ph"
  41 ///////////////////////////////////////////////////////////////////////////////
  42 //
  43 // Forward class definition for Term
  44 //
  45 ///////////////////////////////////////////////////////////////////////////////
  46 #ifndef datatype_Term_defined
  47 #define datatype_Term_defined
  48    class a_Term;
  49    typedef a_Term * Term;
  50 #endif
  51
  52 ///////////////////////////////////////////////////////////////////////////////
  53 //
  54 // Base class for datatype Term
  55 //
  56 ///////////////////////////////////////////////////////////////////////////////
  57 class a_Term : public MEM {
  58 public:
  59    enum Tag_Term {
  60       tag_CONSterm = 0, tag_VARterm = 1, tag_CODEterm = 2,
  61       tag_OPAQUEterm = 3, tag_PATterm = 4
  62    };
  63
  64 public:
  65    const Tag_Term tag__; // variant tag
  66 protected:
  67    inline a_Term(Tag_Term t__) : tag__(t__) {}
  68 public:
  69 };
  70 inline int boxed(const a_Term *) { return 1; }
  71 inline int untag(const a_Term * x) { return x->tag__; }
  72 ///////////////////////////////////////////////////////////////////////////////
  73 //
  74 // Class for datatype constructor Term::CONSterm
  75 //
  76 ///////////////////////////////////////////////////////////////////////////////
  77 class Term_CONSterm : public a_Term {
  78 public:
  79 #line 30 "trs.ph"
  80    TreeAutomaton::Functor _1; Cons _2; int _3; Term * _4;
  81    Term_CONSterm (TreeAutomaton::Functor x_1, Cons x_2, int x_3, Term * x_4);
  82 };
  83
  84 ///////////////////////////////////////////////////////////////////////////////
  85 //
  86 // Class for datatype constructor Term::VARterm
  87 //
  88 ///////////////////////////////////////////////////////////////////////////////
  89 class Term_VARterm : public a_Term {
  90 public:
  91 #line 32 "trs.ph"
  92    int _1; Pat _2; Exp _3;
  93    Term_VARterm (int x_1, Pat x_2, Exp x_3);
  94 };
  95
  96 ///////////////////////////////////////////////////////////////////////////////
  97 //
  98 // Class for datatype constructor Term::CODEterm
  99 //
 100 ///////////////////////////////////////////////////////////////////////////////
 101 class Term_CODEterm : public a_Term {
 102 public:
 103 #line 33 "trs.ph"
 104    Exp CODEterm;
 105    Term_CODEterm (Exp x_CODEterm);
 106 };
 107
 108 ///////////////////////////////////////////////////////////////////////////////
 109 //
 110 // Class for datatype constructor Term::OPAQUEterm
 111 //
 112 ///////////////////////////////////////////////////////////////////////////////
 113 class Term_OPAQUEterm : public a_Term {
 114 public:
 115 #line 34 "trs.ph"
 116    Decls OPAQUEterm;
 117    Term_OPAQUEterm (Decls x_OPAQUEterm);
 118 };
 119
 120 ///////////////////////////////////////////////////////////////////////////////
 121 //
 122 // Class for datatype constructor Term::PATterm
 123 //
 124 ///////////////////////////////////////////////////////////////////////////////
 125 class Term_PATterm : public a_Term {
 126 public:
 127 #line 35 "trs.ph"
 128    Pat PATterm;
 129    Term_PATterm (Pat x_PATterm);
 130 };
 131
 132 ///////////////////////////////////////////////////////////////////////////////
 133 //
 134 // Datatype constructor functions for Term
 135 //
 136 ///////////////////////////////////////////////////////////////////////////////
 137 extern a_Term * CONSterm (TreeAutomaton::Functor x_1, Cons x_2, int x_3, Term * x_4);
 138 extern a_Term * VARterm (int x_1, Pat x_2, Exp x_3);
 139 extern a_Term * CODEterm (Exp x_CODEterm);
 140 extern a_Term * OPAQUEterm (Decls x_OPAQUEterm);
 141 extern a_Term * PATterm (Pat x_PATterm);
 142
 143 #line 36 "trs.ph"
 144 #line 36 "trs.ph"
 145
 146
 147
 148 ///////////////////////////////////////////////////////////////////////////////
 149 //
 150 //  This class represent a term rewriting system.
 151 //
 152 ///////////////////////////////////////////////////////////////////////////////
 153 class TRS {
 154    TRS();                         // no default constructor
 155    TRS(const TRS&);               // no copy constructor
 156    void operator = (const TRS&);  // no assignment
 157 public:
 158    typedef TreeAutomaton::Functor Functor;
 159    typedef TreeAutomaton::State   State;
 160    typedef TreeAutomaton::Rule    Rule;
 161    enum EvalResult { SUCCESS, FAILURE, UNKNOWN };
 162
 163    typedef
 164 #line 54 "trs.ph"
 165 Tuple2<State, Term>
 166 #line 54 "trs.ph"
 167  Residue;
 168    typedef a_List<Residue> *
 169 #line 55 "trs.ph"
 170  Residues;
 171
 172 private:
 173    ////////////////////////////////////////////////////////////////////////////
 174    //
 175    //  Data to implement the tree automaton and the rules
 176    //
 177    ////////////////////////////////////////////////////////////////////////////
 178    enum { MAX_VARS = 256 };
 179    RewritingCompiler&   compiler; // the rewriting compiler
 180    const FunctorMap&    Fmap;     // the functor map
 181    const TreeAutomaton& treeauto; // the tree automata
 182    int         number_of_rules;   // number of rules
 183    MatchRule * rule_map;          // mapping from rule_no to rule
 184    Exp *       guard_map;         // mapping from rule_no to guard
 185    Term *      lhs_map;           // mapping from rule_no to lhs
 186    Term *      rhs_map;           // mapping from rule_no to rhs
 187    int *       num_var_map;       // mapping from rule_no to number of vars
 188    Exp **      var_map;           // mapping from rule_no to variable bindings
 189    Pat **      var_pat_map;       // mapping from rule_no to variable patterns
 190    Residues ** residue_map;       // mapping from rule_no x variable -> residue
 191    Literal *   literal_map;       // mapping from functor -> literal
 192    Exp *      optimized_map;     // mapping from rule_no -> optimized expr
 193    int         states[MAX_VARS];  // state table
 194    int         mus[MAX_VARS];     // mu table
 195    Bool        count_redex;       // count redex mode/don't normalize
 196
 197    ////////////////////////////////////////////////////////////////////////////
 198    //
 199    //  The local variable environment.
 200    //
 201    ////////////////////////////////////////////////////////////////////////////
 202    int         num_vars;           // number of variables in environment
 203    Exp         vars[MAX_VARS];     // variable bindings
 204    Pat         var_pats[MAX_VARS]; // variable pattern names
 205
 206    ////////////////////////////////////////////////////////////////////////////
 207    //
 208    //  Partial evaluation statistics
 209    //
 210    ////////////////////////////////////////////////////////////////////////////
 211    int         number_of_specializations;
 212    void        clear_statistics();
 213
 214 public:
 215    TRS(RewritingCompiler&);
 216   ~TRS();
 217
 218    ////////////////////////////////////////////////////////////////////////////
 219    //
 220    //  Pretty printing
 221    //
 222    ////////////////////////////////////////////////////////////////////////////
 223    void print (std::ostream&) const;
 224    void print (std::ostream&,Term) const;
 225    void print_report(std::ostream&) const;
 226    void print_specializations(std::ostream&) const;
 227
 228    ////////////////////////////////////////////////////////////////////////////
 229    //
 230    //  Partial evaluation and code generation methods
 231    //
 232    ////////////////////////////////////////////////////////////////////////////
 233    void mix();
 234    Bool gen_replacement(CodeGen&, Rule, Exp);
 235
 236 private:
 237
 238    ////////////////////////////////////////////////////////////////////////////
 239    //
 240    //  Methods to construct the term representation.
 241    //
 242    ////////////////////////////////////////////////////////////////////////////
 243    void   make_lhs(Rule r, Pat);
 244    void   make_rhs(Rule r, Term);
 245    void   make_rhs(Rule r, Exp);
 246
 247    Term   make_term(Pat);
 248    Term   make_term(Pat, Cons, Pats);
 249    Term * make_term(Pats);
 250
 251    Term   make_term(Exp);
 252    Term   make_term(Exp, Id, Exps);
 253    Term * make_term(Exps);
 254
 255    Term   make_term_var(Pat, Exp);
 256
 257    ////////////////////////////////////////////////////////////////////////////
 258    //
 259    //  Methods for partial evaluation
 260    //
 261    ////////////////////////////////////////////////////////////////////////////
 262    void mix(Rule);
 263    void mix_0(Rule);
 264    void mix_1(Rule);
 265
 266    ////////////////////////////////////////////////////////////////////////////
 267    //
 268    //  Methods for normalization and reduction
 269    //
 270    ////////////////////////////////////////////////////////////////////////////
 271    State normalize (Term& term, int& reductions);
 272    Bool  is_relevant(Rule);
 273    Term  reduce    (Term term, State, int& reductions, Bool& changed);
 274    EvalResult eval_guard(Exp);
 275    Term  subst     (Term, Term, Bool&);
 276    Term* subst     (int, Term[], Term, Bool&);
 277    Term  proj      (Exp, Term, Bool&);
 278    Exp   proj      (Exp, Exp, Bool&);
 279    Term  copy      (Term);
 280    Term* copy      (int, Term[]);
 281
 282    ////////////////////////////////////////////////////////////////////////////
 283    //
 284    //  Methods for generating residue code
 285    //
 286    ////////////////////////////////////////////////////////////////////////////
 287    void generate_residue(Rule, int, State, Term);
 288    Exp  make_exp(Term) const;
 289    Exps make_exp(int n, Term []) const;
 290
 291    ////////////////////////////////////////////////////////////////////////////
 292    //
 293    //  Methods for error reporting
 294    //
 295    ////////////////////////////////////////////////////////////////////////////
 296    void print_residue(Rule, Term) const;
 297 };
 298
 299 #endif
 300 /*
 301 ------------------------------- Statistics -------------------------------
 302 Merge matching rules         = yes
 303 Number of DFA nodes merged   = 0
 304 Number of ifs generated      = 0
 305 Number of switches generated = 0
 306 Number of labels             = 0
 307 Number of gotos              = 0
 308 Adaptive matching            = enabled
 309 Fast string matching         = disabled
 310 Inline downcasts             = enabled
 311 --------------------------------------------------------------------------
 312 */