Changeset a4a000d

Timestamp:

Sep 13, 2018, 4:37:26 PM (6 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, deferred_resn, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, no_list, persistent-indexer, pthread-emulation, qualifiedEnum

Children:

6e9ffd1

Parents:

4d59ff9

Message:

support assertions in RPDump

File:

• src/CodeTools/ResolvProtoDump.cc (modified) (20 diffs)

src/CodeTools/ResolvProtoDump.cc

@@ -39 +39 @@
         /// Visitor for dumping resolver prototype output
         class ProtoDump : public WithShortCircuiting, public WithVisitorRef<ProtoDump> {
-                std::set<std::string> decls;     ///< Declarations in this scope
-                std::vector<std::string> exprs;  ///< Expressions in this scope
-                std::vector<ProtoDump> subs;     ///< Sub-scopes
-                const ProtoDump* parent;         ///< Outer lexical scope
-                std::unique_ptr<Type> rtnType;   ///< Return type for this scope
+                std::set<std::string> decls;             ///< Declarations in this scope
+                std::vector<std::string> exprs;          ///< Expressions in this scope
+                std::vector<ProtoDump> subs;             ///< Sub-scopes
+                std::unordered_set<std::string> closed;  ///< Closed type variables
+                const ProtoDump* parent;                 ///< Outer lexical scope
+                std::unique_ptr<Type> rtnType;           ///< Return type for this scope
 
         public:
                 /// Default constructor for root ProtoDump
-                ProtoDump() : decls(), exprs(), subs(), parent(nullptr), rtnType(nullptr) {}
+                ProtoDump() : decls(), exprs(), subs(), closed(), parent(nullptr), rtnType(nullptr) {}
 
                 /// Child constructor
-                ProtoDump(const ProtoDump* p, Type* r) : decls(), exprs(), subs(), parent(p), rtnType(r) {}
+                ProtoDump(const ProtoDump* p, Type* r) 
+                        : decls(), exprs(), subs(), closed(p->closed), parent(p), rtnType(r) {}
 
                 // Fix copy issues
-                ProtoDump( const ProtoDump& o ) 
-                        : decls(o.decls), exprs(o.exprs), subs(o.subs), parent(o.parent), 
+                ProtoDump(const ProtoDump& o) 
+                        : decls(o.decls), exprs(o.exprs), subs(o.subs), closed(o.closed), parent(o.parent), 
                           rtnType(maybeClone(o.rtnType.get())) {}
                 ProtoDump( ProtoDump&& ) = default;
 
-                ProtoDump& operator= ( const ProtoDump& o ) {
+                ProtoDump& operator= (const ProtoDump& o) {
                         if ( this == &o ) return *this;
 
@@ -64 +66 @@
                         exprs = o.exprs;
                         subs = o.subs;
+                        closed = o.closed;
                         parent = o.parent;
                         rtnType.reset( maybeClone(o.rtnType.get()) );
@@ -69 +72 @@
                         return *this;
                 }
-                ProtoDump& operator= ( ProtoDump&& ) = default;
+                ProtoDump& operator= (ProtoDump&&) = default;
 
         private:
@@ -205 +208 @@
                 /// Visitor for printing types
                 struct TypePrinter : public WithShortCircuiting, WithVisitorRef<TypePrinter>, WithGuards {
-                        std::stringstream& ss;  ///< Output to print to
-                        unsigned depth;         ///< Depth of nesting from root type
-
-                        TypePrinter( std::stringstream& ss ) : ss(ss), depth(0) {}
+                        std::stringstream& ss;                          ///< Output to print to
+                        const std::unordered_set<std::string>& closed;  ///< Closed type variables
+                        unsigned depth;                                 ///< Depth of nesting from root type
+
+                        TypePrinter( const std::unordered_set<std::string>& closed, std::stringstream& ss ) 
+                                : ss(ss), closed(closed), depth(0) {}
 
                         // basic type represented as integer type
@@ -274 +279 @@
                         void previsit( EnumInstType* ) { ss << (int)BasicType::SignedInt; }
 
-                        // make sure first letter of TypeInstType is capitalized
                         void previsit( TypeInstType* vt ) {
-                                ti_name( vt->name, ss );
+                                // print closed variables as named types
+                                if ( closed.count( vt->name ) ) { ss << '#' << vt->name; }
+                                // otherwise make sure first letter is capitalized
+                                else { ti_name( vt->name, ss ); }
                         }
 
@@ -302 +309 @@
                 /// builds description of function
                 void build( const std::string& name, FunctionType* fnTy, std::stringstream& ss ) {
-                        PassVisitor<TypePrinter> printTy{ ss };
+                        PassVisitor<TypePrinter> printTy{ closed, ss };
+                        // print return values
                         build( printTy, from_decls( fnTy->returnVals ), ss, terminated );
+                        // print name
                         rp_name( name, ss );
+                        // print parameters
                         build( printTy, from_decls( fnTy->parameters ), ss, preceded );
-                        // TODO handle assertions
+                        // print assertions
+                        for ( TypeDecl* tyvar : fnTy->forall ) {
+                                for ( DeclarationWithType* assn : tyvar->assertions ) {
+                                        ss << " | "; 
+                                        build( assn->name, assn->get_type(), ss );
+                                }
+                        }
                 }
 
@@ -326 +342 @@
 
                         // print variable declaration as zero-arg function
-                        PassVisitor<TypePrinter> printTy{ ss };
+                        PassVisitor<TypePrinter> printTy{ closed, ss };
                         norefs->accept( printTy );
                         ss << ' ';
@@ -338 +354 @@
 
                         // print access as new field name
-                        PassVisitor<TypePrinter> printTy{ ss };
+                        PassVisitor<TypePrinter> printTy{ closed, ss };
                         norefs->accept( printTy );
                         ss << ' ';
@@ -359 +375 @@
                 struct ExprPrinter : WithShortCircuiting, WithVisitorRef<ExprPrinter> {
                         // TODO change interface to generate multiple expression candidates
-
-                        std::stringstream& ss;  ///< Output to print to
-
-                        ExprPrinter( std::stringstream& ss ) : ss(ss) {}
+                        const std::unordered_set<std::string>& closed;  ///< set of closed type vars
+                        std::stringstream& ss;                          ///< Output to print to
+
+                        ExprPrinter( const std::unordered_set<std::string>& closed, std::stringstream& ss ) 
+                                : closed(closed), ss(ss) {}
 
                         /// Names handled as nullary function calls
@@ -401 +418 @@
                         /// Address-of handled as operator
                         void previsit( AddressExpr* expr ) {
-                                // TODO global function to implement this
                                 ss << "$addr( ";
                                 expr->arg->accept( *visitor );
@@ -411 +427 @@
                         /// TODO put cast target functions in, and add second expression for target
                         void previsit( CastExpr* cast ) {
-                                PassVisitor<TypePrinter> tyPrinter{ ss };
+                                PassVisitor<TypePrinter> tyPrinter{ closed, ss };
                                 cast->result->accept( tyPrinter );
                                 visit_children = false;
@@ -438 +454 @@
                         /// Constant expression replaced by its type
                         void previsit( ConstantExpr* expr ) {
-                                PassVisitor<TypePrinter> tyPrinter{ ss };
+                                PassVisitor<TypePrinter> tyPrinter{ closed, ss };
                                 expr->constant.get_type()->accept( tyPrinter );
                                 visit_children = false;
@@ -460 +476 @@
                         /// Logical expressions represented as operators
                         void previsit( LogicalExpr* expr ) {
-                                // TODO global functions for these
                                 ss << '$' << ( expr->get_isAnd() ? "and" : "or" ) << "( ";
                                 expr->arg1->accept( *visitor );
@@ -471 +486 @@
                         /// Conditional expression represented as operator
                         void previsit( ConditionalExpr* expr ) {
-                                // TODO global function for this
                                 ss << "$if( ";
                                 expr->arg1->accept( *visitor );
@@ -484 +498 @@
                         /// Comma expression represented as operator
                         void previsit( CommaExpr* expr ) {
-                                // TODO global function for this
                                 ss << "$seq( ";
                                 expr->arg1->accept( *visitor );
@@ -498 +511 @@
                 void build( Initializer* init, std::stringstream& ss ) {
                         if ( SingleInit* si = dynamic_cast<SingleInit*>(init) ) {
-                                PassVisitor<ExprPrinter> exprPrinter{ ss };
+                                PassVisitor<ExprPrinter> exprPrinter{ closed, ss };
                                 si->value->accept( exprPrinter );
                                 ss << ' ';
@@ -521 +534 @@
                 void build( Type* rtnType, Expression* expr, std::stringstream& ss ) {
                         ss << "$constructor( ";
-                        PassVisitor<TypePrinter> tyPrinter{ ss };
+                        PassVisitor<TypePrinter> tyPrinter{ closed, ss };
                         rtnType->accept( tyPrinter );
                         ss << ' ';
-                        PassVisitor<ExprPrinter> exprPrinter{ ss };
+                        PassVisitor<ExprPrinter> exprPrinter{ closed, ss };
                         expr->accept( exprPrinter );
                         ss << " )";
@@ -587 +600 @@
                                 }
                                 PassVisitor<ProtoDump> body{ this, rtn };
+
+                                for ( TypeDecl* tyvar : decl->type->forall ) {
+                                        // add set of "closed" types to body so that it can print them as NamedType
+                                        body.pass.closed.insert( tyvar->name );
+
+                                        // add assertions to local scope as declarations as well
+                                        for ( DeclarationWithType* assn : tyvar->assertions ) {
+                                                assn->accept( body );
+                                        }
+                                }
                                 
                                 // add named parameters and returns to local scope
                                 body.pass.addAll( decl->type->returnVals );
                                 body.pass.addAll( decl->type->parameters );
-                                
-                                // TODO add assertions to local scope
-
-                                // TODO add set of "closed" types to body so that it can print them as NamedType
 
                                 // add contents of function to new scope
@@ -636 +655 @@
                 void previsit( Expression* expr ) {
                         std::stringstream ss;
-                        PassVisitor<ExprPrinter> exPrinter{ss};
+                        PassVisitor<ExprPrinter> exPrinter{ closed, ss };
                         expr->accept( exPrinter );
                         addExpr( ss.str() );
@@ -642 +661 @@
                 }
 
+                /// Print non-prelude global declarations for resolv proto
+                void printGlobals() const {
+                        std::cout << "#ptr<T> $addr T" << std::endl;  // &?
+                        int i = (int)BasicType::SignedInt;
+                        std::cout << i << " $and " << i << ' ' << i << std::endl;  // ?&&?
+                        std::cout << i << " $or " << i << ' ' << i << std::endl;  // ?||?
+                        std::cout << "T $if " << i << " T T" << std::endl; // ternary operator
+                        std::cout << "T $seq X T" << std::endl;  // ?,?
+                }
+
         public:
                 /// Prints this ProtoDump instance
                 void print(unsigned indent = 0) const {
+                        // print globals at root level
+                        if ( ! parent ) printGlobals();
+                        // print decls
                         std::string tab( indent, '\t' );
-                        // print decls
                         for ( const std::string& d : decls ) {
                                 std::cout << tab << d << std::endl;