prop-src/ast.ph

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file contains the abstract syntax tree definitions for the
   4 //  Prop language.  For simplicity, C++ statements are currently not
   5 //  handled directly in the AST.
   6 //
   7 ///////////////////////////////////////////////////////////////////////////////
   8 #ifndef abstract_syntax_tree_h
   9 #define abstract_syntax_tree_h
  10
  11 #include "basics.ph"
  12 #include "ir.h"
  13
  14 ///////////////////////////////////////////////////////////////////////////////
  15 //
  16 //  Options to the pattern matching compiler.
  17 //
  18 ///////////////////////////////////////////////////////////////////////////////
  19 enum { MATCHnone            = 0,     // no option (select first matching rule)
  20        MATCHall             = 1<<0,  // select all matching rules
  21        MATCHwhile           = 1<<1,  // loop back
  22        MATCHnocheck         = 1<<2,  // no checking
  23        MATCHwithcost        = 1<<3,  // with cost minimization
  24        MATCHwithintcost     = 1<<4,  // with integer costs
  25        MATCHwithexpcost     = 1<<5,  // with expression costs
  26        MATCHwithtreecost    = 1<<6,  // use cumulative cost
  27        MATCHrefutable       = 1<<7,  // pattern is refutable
  28        MATCHscanner         = 1<<8,  // lexical scanner
  29        MATCHcaseinsensitive = 1<<9,  // insensitive case during string matching
  30        MATCHlexemepat       = 1<<10, // with lexeme pattern
  31        MATCHnotrace         = 1<<11, // no tracing
  32        MATCHunification     = 1<<12  // unification mode
  33      };
  34
  35 ///////////////////////////////////////////////////////////////////////////////
  36 //
  37 //  Forward type declarations.
  38 //  These are defined in other places.
  39 //
  40 ///////////////////////////////////////////////////////////////////////////////
  41 datatype Ty                  // type expression
  42      and Pat                 // patterns
  43      and Cons                // constructor info
  44      and Literal             // literals
  45      and GramExp             // grammar expressions
  46      and FieldDef            // bitfield definition
  47      and FieldLaw            // bitfield law
  48      and Stmt                // statements
  49      and Def                 // definitions
  50      and Cost                // cost expression
  51      and ConstraintSet       // logical constraint rule set
  52      and GraphRewritingRule  // a graph rewriting rule
  53 ;
  54
  55 class ClassDefinition;
  56 class RewriteIndexing;
  57
  58 ///////////////////////////////////////////////////////////////////////////////
  59 //
  60 //  Information on a match rule.
  61 //
  62 ///////////////////////////////////////////////////////////////////////////////
  63 class MatchRuleInfo : public Loc
  64 {  MatchRuleInfo   (const MatchRuleInfo&);  // no copy constructor
  65    void operator = (const MatchRuleInfo&);  // no assignment
  66 public:
  67    Bool used;           // is the rule being used?
  68    Ty   ty;             // type of pattern
  69    int  rule_number;    // rule number
  70    Bool negated;        // negation in inference?
  71    Bool rewriting;      // A rewriting pattern?
  72    Bool is_chain_rule;  // Chain rule?
  73    enum RewritingMode
  74    {  BEFORE, PREORDER, POSTORDER, TOPDOWN, BOTTOMUP, LAST_REWRITING_MODE
  75    } mode;              // rewriting mode
  76    enum
  77    {  NO_OPTIONS = 0, CUTREWRITE = 1, REPLACEMENT = 2, FAILREWRITE = 4 };
  78    typedef int RewritingOption;
  79    RewritingOption option;
  80
  81    MatchRuleInfo();
  82 };
  83
  84 ///////////////////////////////////////////////////////////////////////////////
  85 //
  86 //  Expressions.
  87 //
  88 ///////////////////////////////////////////////////////////////////////////////
  89 datatype Exp : public MEM =
  90    ////////////////////////////////////////////////////////////////////////////
  91    //
  92    //  Basic expressions.  These are mostly generated by the parser.
  93    //
  94    ////////////////////////////////////////////////////////////////////////////
  95      NOexp                       // no expression.
  96    | LITERALexp (Literal)        // literal expression.
  97    | IDexp      (Id)             // identifier
  98    | RELexp     int              // nth relation during inference
  99    | DOTexp     (Exp, Id)        // e . l
 100    | SELECTORexp(Exp, Cons, Ty)  // selector from a constructor
 101    | DEREFexp   (Exp)            // * e
 102    | ARROWexp   (Exp, Id)        // e -> l
 103    | INDEXexp   (Exp, Exp)       // e1 [ e2 ]
 104    | BINOPexp   (Id, Exp, Exp)   // e1 op e2
 105    | PREFIXexp  (Id, Exp)        // op e
 106    | POSTFIXexp (Id, Exp)        // e op
 107    | APPexp     (Exp, Exp)       // e1(e2)
 108    | ASSIGNexp  (Exp, Exp)       // e1 := e2
 109    | IFexp      (Exp, Exp, Exp)  // e1 ? e2 : e3
 110    | TUPLEexp   (List<Exp>)      // (e,...,e)
 111    | EXTUPLEexp (List<Exp>)      // .(e,...,e)
 112    | RECORDexp  (List<LabExp>)   // { x = e1, y = e2, ... z = en }
 113    | LISTexp    (Cons, Cons, List<Exp>, Exp) // #[1,2,3,4,5]
 114    | VECTORexp  (Cons, List<Exp>)            // [| 1, 2, 3, 4, 5 |]
 115    | CONSexp    (Cons, List<Exp>, Exp)       // cons(e)
 116    | CASTexp    (Ty,Exp)                     // casts
 117    | QUALexp    (Ty, Id)                     // qualified expression ty :: id
 118
 119    ////////////////////////////////////////////////////////////////////////////
 120    //
 121    //  Extensions to deal with pattern matching, rewriting and inference.
 122    //  Most of these are generated internally.
 123    //
 124    ////////////////////////////////////////////////////////////////////////////
 125    | EQexp      (Ty, Exp, Exp)       // equality expression
 126    | UNIFYexp   (Ty, Exp, Exp)       // unification expression
 127    | LTexp      (Ty, Exp, Exp)       // less than expression
 128    | HASHexp    (Ty, Exp)            // hashing expression
 129    | THISCOSTexp()                   // current cost
 130    | COSTexp    (ChildNo)            // cost attribute of child
 131    | THISSYNexp (RuleNo,Ty,Bool)     // current synthesized attribue
 132    | SYNexp     (ChildNo, RuleNo,Ty,Bool) // synthesized attribute of child
 133    | SENDexp    (Id, List<Exp>)      // [| email sendTo: recipient |]
 134
 135    ////////////////////////////////////////////////////////////////////////////
 136    //
 137    //  Extensions to deal with the SETL-like sublanguage.
 138    //
 139    ////////////////////////////////////////////////////////////////////////////
 140    | SETLexp    (SETLOp, Exps)        // SETL-like operator expression.
 141    | LISTCOMPexp { exp        : Exp,  // list comprehension
 142                    generators : List<Generator>,
 143                    guard      : Exp
 144                  }
 145    | FORALLexp  (Id, Exp)             // universal quantifier
 146    | EXISTSexp  (Id, Exp)             // existential quantifier
 147
 148    ////////////////////////////////////////////////////////////////////////////
 149    //
 150    //  Miscellaneous expressions.
 151    //
 152    ////////////////////////////////////////////////////////////////////////////
 153    | MARKEDexp  (Loc, Exp) // expressions marked with the location.
 154    public:
 155    {
 156       Ty ty;
 157    }
 158
 159 ///////////////////////////////////////////////////////////////////////////////
 160 //
 161 //  SETL-like operators
 162 //
 163 ///////////////////////////////////////////////////////////////////////////////
 164 and SETLOp =
 165       ARBop         // extract arbitrary element
 166    |  DOMop         // domain
 167    |  RANop         // range
 168    |  CARDop        // cardinality
 169    |  WITHop        // with
 170    |  WITHASSIGNop  // with :=
 171    |  LESSop        // less
 172    |  LESSASSIGNop  // less :=
 173
 174 ///////////////////////////////////////////////////////////////////////////////
 175 //
 176 //  A generator expression:  pat | guard <- exp
 177 //
 178 ///////////////////////////////////////////////////////////////////////////////
 179 and Generator : public Loc =
 180       GENERATOR { pat   : Pat, // bindings
 181                   guard : Exp, // guard expression, if any
 182                   exp   : Exp  // a collection object
 183                 }
 184
 185 ///////////////////////////////////////////////////////////////////////////////
 186 //
 187 //  Pattern matching expressions.
 188 //
 189 ///////////////////////////////////////////////////////////////////////////////
 190 and MatchExp : public Loc = MATCHexp  (Exp, Id)
 191
 192 ///////////////////////////////////////////////////////////////////////////////
 193 //
 194 //  Pattern matching rules.
 195 //
 196 ///////////////////////////////////////////////////////////////////////////////
 197 and MatchRule : public MatchRuleInfo =
 198        MATCHrule (Id, Pat, Exp, Cost, List<Decl>)
 199        // nonterminal -> pat | guard: action
 200
 201 ///////////////////////////////////////////////////////////////////////////////
 202 //
 203 //  Prop declarations/specifications
 204 //
 205 ///////////////////////////////////////////////////////////////////////////////
 206 and Decl : public MEM =
 207      NOdecl
 208    | OPAQUEdecl          (const char *)
 209
 210      // datatype and instantiation declarations
 211    | DATATYPEdecl        (DatatypeDefs, ViewDefs, LawDefs, TyDefs)
 212    | INSTANTIATEdecl     (Bool, Tys)
 213
 214      // special class definition
 215    | CLASSDEFdecl        (ClassDefinition *)
 216
 217      // inference rules declarations
 218    | INFERENCEdecl       (Id, InferenceRules)
 219
 220      // rewriting rule declarations
 221    | REWRITEdecl         (Id, RewriteIndexings, MatchRules)
 222    | REWRITINGdecl       (Protocols, Exp, Exp, RewriteIndexings,
 223                           MatchRules, TyQual)
 224    | REPLACEMENTdecl     (Exp, MatchRuleInfo::RewritingMode)
 225    | CUTREWRITEdecl      (Exp, MatchRuleInfo::RewritingMode)
 226    | FAILREWRITEdecl     (MatchRuleInfo::RewritingMode)
 227    | INJECTdecl          { node_number : int,
 228                            direction   : EntryDirection
 229                          }
 230    | GOTOdecl            Id
 231    | SETSTATEdecl        int
 232
 233      // constraint class and constraint declarations
 234    | CONSTRAINTdecl      (Id, ConstraintSet)
 235
 236      // syntax class and grammar declarations
 237    | SYNTAXdecl          (Id, GramExp)
 238    | ATTRIBUTEGRAMMARdecl(Id, GramExp)
 239
 240      // functions and pattern matching definitions
 241    | FUNdecl             (FunDefs)
 242    | MATCHdecl           (MatchExps, MatchRules, MatchOptions, Ty)
 243
 244      // bitfield declarations
 245    | BITFIELDdecl        { name        : Id,
 246                            width       : int,
 247                            field_names : FieldDefs,
 248                            laws        : FieldLaws
 249                          }
 250
 251      // SETL-style statements and definitions
 252    | SETLSTMTdecl        (Stmt)
 253    | SETLDEFdecl         (Def)
 254
 255      // graphrewrite declarations
 256    | GRAPHREWRITEdecl       { name  : Id,
 257                               args  : LabTys,
 258                               rules : GraphRewritingRules
 259                             }
 260
 261      // dataflow declarations
 262    | DATAFLOWdecl           { name : Id
 263                             }
 264      // misc expressions.
 265    | CLASSOFdecl         (Id)
 266    | TYPEEXPdecl         (Ty)
 267    | EXPdecl             { exp    : Exp,
 268                            prefix : const char * = 0,
 269                            suffix : const char * = 0
 270                          }
 271
 272      // location marker
 273    | MARKEDdecl          (Loc, Decl)
 274
 275 ///////////////////////////////////////////////////////////////////////////////
 276 //
 277 //  Direction of entry into the RETE network
 278 //
 279 ///////////////////////////////////////////////////////////////////////////////
 280 and EntryDirection = LEFTdirection | RIGHTdirection
 281
 282 ///////////////////////////////////////////////////////////////////////////////
 283 //
 284 //  Protocol of a rewrite type defines the set inherited and synthesized
 285 //  attributes for a rewrite type.
 286 //
 287 ///////////////////////////////////////////////////////////////////////////////
 288 and  Protocol : public Loc = PROTOCOL { ty : Ty, inh : Ty, syn : Ty }
 289
 290 ///////////////////////////////////////////////////////////////////////////////
 291 //
 292 //  Datatype definitions.
 293 //
 294 ///////////////////////////////////////////////////////////////////////////////
 295 and  DatatypeDef : public Loc =
 296         DATATYPEdef (Id, TyVars, Inherits, TyQual, TermDefs, Decls)
 297
 298 ///////////////////////////////////////////////////////////////////////////////
 299 //
 300 //  Definition of a constructor term.
 301 //
 302 ///////////////////////////////////////////////////////////////////////////////
 303 and     TermDef : public Loc =
 304                         TERMdef { id             : Id,
 305                                   ty             : Ty,
 306                                   decls          : Decls        = #[],
 307                                   inherits       : Inherits     = #[],
 308                                   pat            : Pat          = NOpat,
 309                                   print_formats  : PrintFormats = #[],
 310                                   opt            : TyOpt        = OPTnone,
 311                                   qual           : TyQual       = QUALnone,
 312                                   view_predicate : Exp          = NOexp
 313                                 }
 314
 315 ///////////////////////////////////////////////////////////////////////////////
 316 //
 317 //  Definition of a datatype view
 318 //
 319 ///////////////////////////////////////////////////////////////////////////////
 320 and    ViewDef : public Loc = VIEWdef(Pat, Exp, List<LabExp>)
 321
 322 ///////////////////////////////////////////////////////////////////////////////
 323 //
 324 //  Definition of a pattern law.
 325 //
 326 ///////////////////////////////////////////////////////////////////////////////
 327 and    LawDef : public Loc =
 328                       LAWdef{ id     : Id,
 329                               args   : Ids,
 330                               guard  : Exp,
 331                               pat    : Pat,
 332                               invert : Bool,
 333                               ty     : Ty = NOty
 334                             }
 335
 336 ///////////////////////////////////////////////////////////////////////////////
 337 //
 338 //  Type definitions.
 339 //
 340 ///////////////////////////////////////////////////////////////////////////////
 341 and     TyDef : public Loc = TYdef  (Id, TyVars, Ty, Bool)
 342
 343 ///////////////////////////////////////////////////////////////////////////////
 344 //
 345 //  Function definitions.
 346 //
 347 ///////////////////////////////////////////////////////////////////////////////
 348 and     FunDef : public Loc = FUNdef (QualId, Ty, Ty, MatchRules)
 349
 350 ///////////////////////////////////////////////////////////////////////////////
 351 //
 352 //  A qualified name
 353 //
 354 ///////////////////////////////////////////////////////////////////////////////
 355 and    QualId : public MEM = NESTEDid (Ty, QualId)
 356                            | SIMPLEid (Id)
 357
 358 ///////////////////////////////////////////////////////////////////////////////
 359 //
 360 //  Inference rule
 361 //
 362 ///////////////////////////////////////////////////////////////////////////////
 363 and    InferenceRule : public Loc =
 364            INFERENCErule(MatchRules, Exp, Conclusions)
 365
 366 and    Conclusion : public Loc = ASSERTaction (Exp)
 367                                | RETRACTaction (Exp)
 368                                | STMTaction (Decls)
 369
 370 ///////////////////////////////////////////////////////////////////////////////
 371 //
 372 //  Miscellaneous.
 373 //
 374 ///////////////////////////////////////////////////////////////////////////////
 375 where type MatchExps      = List<MatchExp>
 376 and        MatchRules     = List<MatchRule>
 377 and        Decls          = List<Decl>
 378 and        DatatypeDefs   = List<DatatypeDef>
 379 and        ViewDefs       = List<ViewDef>
 380 and        LawDefs        = List<LawDef>
 381 and        TyDefs         = List<TyDef>
 382 and        TermDefs       = List<TermDef>
 383 and        FunDefs        = List<FunDef>
 384 and        Protocols      = List<Protocol>
 385 and        LabExp         = { label : Id, exp : Exp }
 386 and        LabMatchRule   = { id : QualId, rule : MatchRule, return_ty : Ty }
 387 and        LabMatchRules  = { id : QualId, rules : MatchRules, return_ty : Ty }
 388 and        Exps           = List<Exp>
 389 and        LabExps        = List<LabExp>
 390 and        InferenceRules = List<InferenceRule>
 391 and        Conclusions    = List<Conclusion>
 392 and        GraphRewritingRules = List<GraphRewritingRule>
 393 and        FieldDefs      = List<FieldDef>
 394 and        FieldLaws      = List<FieldLaw>
 395 and        ChildNo        = int
 396 and        RuleNo         = int
 397 and        MatchOptions   = int
 398 and        RewriteIndexings = List<RewriteIndexing *>
 399 ;
 400
 401 ///////////////////////////////////////////////////////////////////////////////
 402 //
 403 //  AST manipulation methods.
 404 //
 405 ///////////////////////////////////////////////////////////////////////////////
 406 extern Exp component_exp(Exps, int);
 407 extern Exp component_exp(Exps, Id);
 408 extern Exp component_exp(LabExps, Id);
 409
 410 ///////////////////////////////////////////////////////////////////////////////
 411 //
 412 //  Pretty printing methods.
 413 //
 414 ///////////////////////////////////////////////////////////////////////////////
 415 extern ostream& operator << (ostream&, Exp);
 416 extern ostream& operator << (ostream&, List<Exp>);
 417 extern ostream& operator << (ostream&, LabExp);
 418 extern ostream& operator << (ostream&, List<LabExp>);
 419 extern ostream& operator << (ostream&, Cost);
 420 extern ostream& operator << (ostream&, MatchRule);
 421 extern ostream& operator << (ostream&, QualId);
 422
 423 #endif