source: src/ResolvExpr/TypeEnvironment.h @ 8633f060

//
// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
//
// The contents of this file are covered under the licence agreement in the
// file "LICENCE" distributed with Cforall.
//
// TypeEnvironment.h --
//
// Author           : Richard C. Bilson
// Created On       : Sun May 17 12:24:58 2015
// Last Modified By : Peter A. Buhr
// Last Modified On : Sat Jul 22 09:35:45 2017
// Update Count     : 3
//

#pragma once

#include <iostream>                    // for ostream
#include <list>                        // for list, list<>::iterator, list<>...
#include <map>                         // for map, map<>::value_compare
#include <set>                         // for set
#include <string>                      // for string

#include "SynTree/Declaration.h"       // for TypeDecl::Data, DeclarationWit...
#include "SynTree/SynTree.h"           // for UniqueId
#include "SynTree/Type.h"              // for Type, Type::ForallList
#include "SynTree/TypeSubstitution.h"  // for TypeSubstitution

namespace ResolvExpr {
        // adding this comparison operator significantly improves assertion resolution run time for
        // some cases. The current resolution algorithm's speed partially depends on the order of
        // assertions. Assertions which have fewer possible matches should appear before
        // assertions which have more possible matches. This seems to imply that this could
        // be further improved by providing an indexer as an additional argument and ordering based
        // on the number of matches of the same kind (object, function) for the names of the
        // declarations.
        //
        // I've seen a TU go from 54 minutes to 1 minute 34 seconds with the addition of this comparator.
        struct AssertCompare {
                bool operator()( DeclarationWithType * d1, DeclarationWithType * d2 ) const {
                        int cmp = d1->get_name().compare( d2->get_name() );
                        return cmp < 0 ||
                                ( cmp == 0 && d1->get_type() < d2->get_type() );
                }
        };
        struct AssertionSetValue {
                bool isUsed;
                // chain of Unique IDs of the assertion declarations. The first ID in the chain is the ID of an assertion on the current type,
                // with each successive ID being the ID of an assertion pulled in by the previous ID. The last ID in the chain is
                // the ID of the assertion that pulled in the current assertion.
                std::list< UniqueId > idChain;
        };
        typedef std::map< DeclarationWithType*, AssertionSetValue, AssertCompare > AssertionSet;
        typedef std::map< std::string, TypeDecl::Data > OpenVarSet;

        void printAssertionSet( const AssertionSet &, std::ostream &, int indent = 0 );
        void printOpenVarSet( const OpenVarSet &, std::ostream &, int indent = 0 );

        struct EqvClass {
                std::set< std::string > vars;
                Type *type;
                bool allowWidening;
                TypeDecl::Data data;

                void initialize( const EqvClass &src, EqvClass &dest );
                EqvClass();
                EqvClass( const EqvClass &other );
                EqvClass &operator=( const EqvClass &other );
                ~EqvClass();
                void print( std::ostream &os, Indenter indent = {} ) const;
        };

        class TypeEnvironment {
          public:
                bool lookup( const std::string &var, EqvClass &eqvClass ) const;
                void add( const EqvClass &eqvClass );
                void add( const Type::ForallList &tyDecls );
                void add( const TypeSubstitution & sub );
                template< typename SynTreeClass > int apply( SynTreeClass *&type ) const;
                template< typename SynTreeClass > int applyFree( SynTreeClass *&type ) const;
                void makeSubstitution( TypeSubstitution &result ) const;
                bool isEmpty() const { return env.empty(); }
                void print( std::ostream &os, Indenter indent = {} ) const;
                void combine( const TypeEnvironment &second, Type *(*combineFunc)( Type*, Type* ) );
                void simpleCombine( const TypeEnvironment &second );
                void extractOpenVars( OpenVarSet &openVars ) const;
                TypeEnvironment *clone() const { return new TypeEnvironment( *this ); }

                /// Iteratively adds the environment of a new actual (with allowWidening = false),
                /// and extracts open variables.
                void addActual( const TypeEnvironment& actualEnv, OpenVarSet& openVars );

                typedef std::list< EqvClass >::iterator iterator;
                iterator begin() { return env.begin(); }
                iterator end() { return env.end(); }
                typedef std::list< EqvClass >::const_iterator const_iterator;
                const_iterator begin() const { return env.begin(); }
                const_iterator end() const { return env.end(); }
          private:
                std::list< EqvClass > env;
                std::list< EqvClass >::iterator internal_lookup( const std::string &var );
        };

        template< typename SynTreeClass >
        int TypeEnvironment::apply( SynTreeClass *&type ) const {
                TypeSubstitution sub;
                makeSubstitution( sub );
                return sub.apply( type );
        }

        template< typename SynTreeClass >
        int TypeEnvironment::applyFree( SynTreeClass *&type ) const {
                TypeSubstitution sub;
                makeSubstitution( sub );
                return sub.applyFree( type );
        }

        std::ostream & operator<<( std::ostream & out, const TypeEnvironment & env );
} // namespace ResolvExpr

// Local Variables: //
// tab-width: 4 //
// mode: c++ //
// compile-command: "make install" //
// End: //