prop-src/trs.ph

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  Data structure for partial evaluting a TRS
   4 //
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #ifndef term_rewrite_system_h
   8 #define term_rewrite_system_h
   9
  10 #include <AD/automata/treeauto.h>
  11 #include "basics.ph"
  12 #include "ir.h"
  13 #include "ast.h"
  14
  15 ///////////////////////////////////////////////////////////////////////////////
  16 //
  17 //  Forward declarations
  18 //
  19 ///////////////////////////////////////////////////////////////////////////////
  20 class FunctorMap;
  21 class RewritingCompiler;
  22 class CodeGen;
  23 class std::ostream;
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 //  This class represents a rewriting term
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 datatype Term : public MEM =
  31    CONSterm   (TreeAutomaton::Functor, Cons, int, Term [])
  32 |  VARterm    (int, Pat, Exp)
  33 |  CODEterm   (Exp)
  34 |  OPAQUEterm (Decls)
  35 |  PATterm    (Pat)
  36 ;
  37
  38
  39 ///////////////////////////////////////////////////////////////////////////////
  40 //
  41 //  This class represent a term rewriting system.
  42 //
  43 ///////////////////////////////////////////////////////////////////////////////
  44 class TRS {
  45    TRS();                         // no default constructor
  46    TRS(const TRS&);               // no copy constructor
  47    void operator = (const TRS&);  // no assignment
  48 public:
  49    typedef TreeAutomaton::Functor Functor;
  50    typedef TreeAutomaton::State   State;
  51    typedef TreeAutomaton::Rule    Rule;
  52    enum EvalResult { SUCCESS, FAILURE, UNKNOWN };
  53
  54    typedef .[State, Term] Residue;
  55    typedef List<Residue> Residues;
  56
  57 private:
  58    ////////////////////////////////////////////////////////////////////////////
  59    //
  60    //  Data to implement the tree automaton and the rules
  61    //
  62    ////////////////////////////////////////////////////////////////////////////
  63    enum { MAX_VARS = 256 };
  64    RewritingCompiler&   compiler; // the rewriting compiler
  65    const FunctorMap&    Fmap;     // the functor map
  66    const TreeAutomaton& treeauto; // the tree automata
  67    int         number_of_rules;   // number of rules
  68    MatchRule * rule_map;          // mapping from rule_no to rule
  69    Exp *       guard_map;         // mapping from rule_no to guard
  70    Term *      lhs_map;           // mapping from rule_no to lhs
  71    Term *      rhs_map;           // mapping from rule_no to rhs
  72    int *       num_var_map;       // mapping from rule_no to number of vars
  73    Exp **      var_map;           // mapping from rule_no to variable bindings
  74    Pat **      var_pat_map;       // mapping from rule_no to variable patterns
  75    Residues ** residue_map;       // mapping from rule_no x variable -> residue
  76    Literal *   literal_map;       // mapping from functor -> literal
  77    Exp *      optimized_map;     // mapping from rule_no -> optimized expr
  78    int         states[MAX_VARS];  // state table
  79    int         mus[MAX_VARS];     // mu table
  80    Bool        count_redex;       // count redex mode/don't normalize
  81
  82    ////////////////////////////////////////////////////////////////////////////
  83    //
  84    //  The local variable environment.
  85    //
  86    ////////////////////////////////////////////////////////////////////////////
  87    int         num_vars;           // number of variables in environment
  88    Exp         vars[MAX_VARS];     // variable bindings
  89    Pat         var_pats[MAX_VARS]; // variable pattern names
  90
  91    ////////////////////////////////////////////////////////////////////////////
  92    //
  93    //  Partial evaluation statistics
  94    //
  95    ////////////////////////////////////////////////////////////////////////////
  96    int         number_of_specializations;
  97    void        clear_statistics();
  98
  99 public:
 100    TRS(RewritingCompiler&);
 101   ~TRS();
 102
 103    ////////////////////////////////////////////////////////////////////////////
 104    //
 105    //  Pretty printing
 106    //
 107    ////////////////////////////////////////////////////////////////////////////
 108    void print (std::ostream&) const;
 109    void print (std::ostream&,Term) const;
 110    void print_report(std::ostream&) const;
 111    void print_specializations(std::ostream&) const;
 112
 113    ////////////////////////////////////////////////////////////////////////////
 114    //
 115    //  Partial evaluation and code generation methods
 116    //
 117    ////////////////////////////////////////////////////////////////////////////
 118    void mix();
 119    Bool gen_replacement(CodeGen&, Rule, Exp);
 120
 121 private:
 122
 123    ////////////////////////////////////////////////////////////////////////////
 124    //
 125    //  Methods to construct the term representation.
 126    //
 127    ////////////////////////////////////////////////////////////////////////////
 128    void   make_lhs(Rule r, Pat);
 129    void   make_rhs(Rule r, Term);
 130    void   make_rhs(Rule r, Exp);
 131
 132    Term   make_term(Pat);
 133    Term   make_term(Pat, Cons, Pats);
 134    Term * make_term(Pats);
 135
 136    Term   make_term(Exp);
 137    Term   make_term(Exp, Id, Exps);
 138    Term * make_term(Exps);
 139
 140    Term   make_term_var(Pat, Exp);
 141
 142    ////////////////////////////////////////////////////////////////////////////
 143    //
 144    //  Methods for partial evaluation
 145    //
 146    ////////////////////////////////////////////////////////////////////////////
 147    void mix(Rule);
 148    void mix_0(Rule);
 149    void mix_1(Rule);
 150
 151    ////////////////////////////////////////////////////////////////////////////
 152    //
 153    //  Methods for normalization and reduction
 154    //
 155    ////////////////////////////////////////////////////////////////////////////
 156    State normalize (Term& term, int& reductions);
 157    Bool  is_relevant(Rule);
 158    Term  reduce    (Term term, State, int& reductions, Bool& changed);
 159    EvalResult eval_guard(Exp);
 160    Term  subst     (Term, Term, Bool&);
 161    Term* subst     (int, Term[], Term, Bool&);
 162    Term  proj      (Exp, Term, Bool&);
 163    Exp   proj      (Exp, Exp, Bool&);
 164    Term  copy      (Term);
 165    Term* copy      (int, Term[]);
 166
 167    ////////////////////////////////////////////////////////////////////////////
 168    //
 169    //  Methods for generating residue code
 170    //
 171    ////////////////////////////////////////////////////////////////////////////
 172    void generate_residue(Rule, int, State, Term);
 173    Exp  make_exp(Term) const;
 174    Exps make_exp(int n, Term []) const;
 175
 176    ////////////////////////////////////////////////////////////////////////////
 177    //
 178    //  Methods for error reporting
 179    //
 180    ////////////////////////////////////////////////////////////////////////////
 181    void print_residue(Rule, Term) const;
 182 };
 183
 184 #endif