simple.cc - generated code example
[prop.git] / prop-src / setl-ast.ph
blob2090c5b344deef9ad9cf0c0183b16b53fe260b3a
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
10 #include "basics.ph"
11 #include "ir.ph"
13 ///////////////////////////////////////////////////////////////////////////////
15 //  Forward AST declarations.
17 ///////////////////////////////////////////////////////////////////////////////
18 datatype Exp    // expressions
19      and Decl   // prop declarations
20      and Time   // time complexity
21      and Space  // space complexity
24 ///////////////////////////////////////////////////////////////////////////////
26 //  AST for definitions, signatures, statements and bindings
28 ///////////////////////////////////////////////////////////////////////////////
30 ///////////////////////////////////////////////////////////////////////////////
32 //  Type 'Def' represents definitions. 
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
59 ///////////////////////////////////////////////////////////////////////////////
61 //  Type 'Sig' represents signatures. 
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
72 ///////////////////////////////////////////////////////////////////////////////
74 //  Type 'Stmt' represents statements. 
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
89 ///////////////////////////////////////////////////////////////////////////////
91 //  Miscellaneous type abbreviations
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
102 ///////////////////////////////////////////////////////////////////////////////
104 //  Pretty printing routines for definitions, statements and generators
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);
118 #endif