prop-src/setl-ast.ph

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file contains the abstract syntax tree definitions for the
   4 //  SETL-like extension language of Prop.
   5 //
   6 ///////////////////////////////////////////////////////////////////////////////
   7 #ifndef setl_extension_abstract_syntax_tree_h
   8 #define setl_extension_abstract_syntax_tree_h
   9
  10 #include "basics.ph"
  11 #include "ir.ph"
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  Forward AST declarations.
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 datatype Exp    // expressions
  19      and Decl   // prop declarations
  20      and Time   // time complexity
  21      and Space  // space complexity
  22 ;
  23
  24 ///////////////////////////////////////////////////////////////////////////////
  25 //
  26 //  AST for definitions, signatures, statements and bindings
  27 //
  28 ///////////////////////////////////////////////////////////////////////////////
  29
  30 ///////////////////////////////////////////////////////////////////////////////
  31 //
  32 //  Type 'Def' represents definitions.
  33 //
  34 ///////////////////////////////////////////////////////////////////////////////
  35 datatype Def : public Loc =
  36        NOdef
  37     |  VARdef       { id       : Id,         // variable name
  38                       ty       : Ty,         // type of variable
  39                       init_exp : Exp = NOexp // initial value
  40                     }
  41     |  FUNCTIONdef  { id         : Id,       // name of function
  42                       args       : LabTys,   // arguments
  43                       return_ty  : Ty,       // return type
  44                       local_defs : Defs,     // local defintions
  45                       body       : Stmts     // body of function
  46                     }
  47     |  MODULEdef    { id         : Id,       // name of module
  48                       args       : LabSigs,  // arguments
  49                       sig        : Sig,      // signature constraint
  50                       body       : Defs      // body of module
  51                     }
  52     |  SIGNATUREdef { id         : Id,       // name of signature
  53                       args       : LabSigs,  // arguments
  54                       sig        : Sig       // body of signature
  55                     }
  56     |  TYPEdef      (Decl)                   // datatype/type definition
  57     |  LAMBDAdef    (LabTys, Defs)           // module abstraction
  58
  59 ///////////////////////////////////////////////////////////////////////////////
  60 //
  61 //  Type 'Sig' represents signatures.
  62 //
  63 ///////////////////////////////////////////////////////////////////////////////
  64 and Sig : public Loc =
  65        NOsig                        // no signature
  66     |  IDsig  (Id)                  // signature name
  67     |  DOTsig (Sig, Id)             // signature selection
  68     |  APPsig (Sig, Sigs)           // signature application
  69     |  DEFsig (Defs)                // definitions
  70     |  LAMBDAsig (LabSigs, Sig)     // signature abstraction
  71
  72 ///////////////////////////////////////////////////////////////////////////////
  73 //
  74 //  Type 'Stmt' represents statements.
  75 //
  76 ///////////////////////////////////////////////////////////////////////////////
  77 and Stmt : public Loc =
  78        NOstmt                                  // empty statement
  79     |  ASSIGNstmt      (Exp, Exp)              // assignment
  80     |  BLOCKstmt       (Defs, Stmts)           // statement block
  81     |  WHILEstmt       (Exp, Stmt)             // while loop
  82     |  IFstmt          (Exp, Stmt, Stmt)       // if/then/else
  83     |  MATCHstmt       (Decl)                  // match statement
  84     |  REWRITEstmt     (Decl)                  // rewriting statement
  85     |  REPLACEMENTstmt (Decl)                  // replacement statement
  86     |  FORALLstmt      (Generators, Stmt)      // iteration
  87     |  RETURNstmt      (Exp)                   // return statement
  88
  89 ///////////////////////////////////////////////////////////////////////////////
  90 //
  91 //  Miscellaneous type abbreviations
  92 //
  93 ///////////////////////////////////////////////////////////////////////////////
  94 where type LabSig     = { id : Id, sig : Sig } // labeled signature
  95        and LabSigs    = List<LabSig>           // labeled signature list
  96        and Defs       = List<Def>              // list of definitions
  97        and Sigs       = List<Sig>              // list of signatures
  98        and Stmts      = List<Stmt>             // list of statements
  99        and Generators = List<Generator>        // list of generators
 100 ;
 101
 102 ///////////////////////////////////////////////////////////////////////////////
 103 //
 104 //  Pretty printing routines for definitions, statements and generators
 105 //
 106 ///////////////////////////////////////////////////////////////////////////////
 107 extern std::ostream& operator << (std::ostream&, Def);
 108 extern std::ostream& operator << (std::ostream&, Defs);
 109 extern std::ostream& operator << (std::ostream&, Sig);
 110 extern std::ostream& operator << (std::ostream&, Sigs);
 111 extern std::ostream& operator << (std::ostream&, Stmt);
 112 extern std::ostream& operator << (std::ostream&, Stmts);
 113 extern std::ostream& operator << (std::ostream&, LabSig);
 114 extern std::ostream& operator << (std::ostream&, LabSigs);
 115 extern std::ostream& operator << (std::ostream&, Generator);
 116 extern std::ostream& operator << (std::ostream&, Generators);
 117
 118 #endif