| [99d4584] | 1 | // | 
|---|
|  | 2 | // Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo | 
|---|
|  | 3 | // | 
|---|
|  | 4 | // The contents of this file are covered under the licence agreement in the | 
|---|
|  | 5 | // file "LICENCE" distributed with Cforall. | 
|---|
|  | 6 | // | 
|---|
|  | 7 | // Candidate.hpp -- | 
|---|
|  | 8 | // | 
|---|
|  | 9 | // Author           : Aaron B. Moss | 
|---|
|  | 10 | // Created On       : Wed Jun 5 14:30:00 2019 | 
|---|
| [d76f32c] | 11 | // Last Modified By : Andrew Beach | 
|---|
|  | 12 | // Last Modified On : Wed Jun 12 14:15:00 2019 | 
|---|
|  | 13 | // Update Count     : 2 | 
|---|
| [99d4584] | 14 | // | 
|---|
|  | 15 |  | 
|---|
|  | 16 | #pragma once | 
|---|
|  | 17 |  | 
|---|
|  | 18 | #include <iosfwd> | 
|---|
|  | 19 | #include <memory>        // for shared_ptr | 
|---|
|  | 20 | #include <vector> | 
|---|
|  | 21 |  | 
|---|
|  | 22 | #include "Cost.h" | 
|---|
|  | 23 | #include "AST/Node.hpp" | 
|---|
|  | 24 | #include "AST/TypeEnvironment.hpp" | 
|---|
|  | 25 | #include "Common/Indenter.h" | 
|---|
|  | 26 |  | 
|---|
|  | 27 | namespace ast { | 
|---|
|  | 28 | class Expr; | 
|---|
|  | 29 |  | 
|---|
|  | 30 | /// A list of unresolved assertions | 
|---|
|  | 31 | using AssertionList = std::vector<AssertionSet::value_type>; | 
|---|
| [4b7cce6] | 32 |  | 
|---|
|  | 33 | /// Convenience to merge AssertionList into AssertionSet | 
|---|
|  | 34 | static inline void mergeAssertionSet( AssertionSet & dst, const AssertionList & src ) { | 
|---|
|  | 35 | for ( const auto & s : src ) { dst.emplace( s ); } | 
|---|
|  | 36 | } | 
|---|
| [99d4584] | 37 | } | 
|---|
|  | 38 |  | 
|---|
|  | 39 | namespace ResolvExpr { | 
|---|
|  | 40 |  | 
|---|
|  | 41 | /// One option for resolution of an expression | 
|---|
|  | 42 | struct Candidate { | 
|---|
|  | 43 | ast::ptr<ast::Expr> expr;  ///< Satisfying expression | 
|---|
|  | 44 | Cost cost;                 ///< Cost of the whole expression | 
|---|
|  | 45 | Cost cvtCost;              ///< Cost of conversions to satisfying expression | 
|---|
|  | 46 | ast::TypeEnvironment env;  ///< Containing type environment | 
|---|
|  | 47 | ast::OpenVarSet open;      ///< Open variables for environment | 
|---|
|  | 48 | ast::AssertionList need;   ///< Assertions which need to be resolved | 
|---|
| [d57e349] | 49 |  | 
|---|
| [4b7cce6] | 50 | Candidate() : expr(), cost( Cost::zero ), cvtCost( Cost::zero ), env(), open(), need() {} | 
|---|
| [d76f32c] | 51 |  | 
|---|
| [4b7cce6] | 52 | Candidate( const ast::Expr * x, const ast::TypeEnvironment & e ) | 
|---|
|  | 53 | : expr( x ), cost( Cost::zero ), cvtCost( Cost::zero ), env( e ), open(), need() {} | 
|---|
|  | 54 |  | 
|---|
| [c8e4d2f8] | 55 | Candidate( const Candidate & o, const ast::Expr * x, const Cost & addedCost = Cost::zero ) | 
|---|
|  | 56 | : expr( x ), cost( o.cost + addedCost ), cvtCost( Cost::zero ), env( o.env ), open( o.open ), | 
|---|
| [4b7cce6] | 57 | need( o.need ) {} | 
|---|
| [d76f32c] | 58 |  | 
|---|
| [9d5089e] | 59 | Candidate( | 
|---|
|  | 60 | const ast::Expr * x, const ast::TypeEnvironment & e, const ast::OpenVarSet & o, | 
|---|
|  | 61 | const ast::AssertionSet & n, const Cost & c, const Cost & cvt = Cost::zero ) | 
|---|
|  | 62 | : expr( x ), cost( c ), cvtCost( cvt ), env( e ), open( o ), need( n.begin(), n.end() ) {} | 
|---|
|  | 63 |  | 
|---|
| [d76f32c] | 64 | Candidate( | 
|---|
|  | 65 | const ast::Expr * x, ast::TypeEnvironment && e, ast::OpenVarSet && o, | 
|---|
|  | 66 | ast::AssertionSet && n, const Cost & c, const Cost & cvt = Cost::zero ) | 
|---|
|  | 67 | : expr( x ), cost( c ), cvtCost( cvt ), env( std::move( e ) ), open( std::move( o ) ), | 
|---|
| [4b7cce6] | 68 | need( n.begin(), n.end() ) {} | 
|---|
| [99d4584] | 69 | }; | 
|---|
|  | 70 |  | 
|---|
|  | 71 | /// Shared reference to a candidate | 
|---|
|  | 72 | using CandidateRef = std::shared_ptr< Candidate >; | 
|---|
|  | 73 |  | 
|---|
|  | 74 | /// List of candidates | 
|---|
|  | 75 | using CandidateList = std::vector< CandidateRef >; | 
|---|
|  | 76 |  | 
|---|
| [4b7cce6] | 77 | /// Sum the cost of a list of candidates | 
|---|
|  | 78 | static inline Cost sumCost( const CandidateList & candidates ) { | 
|---|
|  | 79 | Cost total = Cost::zero; | 
|---|
|  | 80 | for ( const CandidateRef & r : candidates ) { total += r->cost; } | 
|---|
|  | 81 | return total; | 
|---|
|  | 82 | } | 
|---|
|  | 83 |  | 
|---|
| [d57e349] | 84 | /// Holdover behaviour from old `findMinCost` -- xxx -- can maybe be eliminated? | 
|---|
|  | 85 | static inline void promoteCvtCost( CandidateList & candidates ) { | 
|---|
|  | 86 | for ( CandidateRef & r : candidates ) { | 
|---|
|  | 87 | r->cost = r->cvtCost; | 
|---|
|  | 88 | } | 
|---|
|  | 89 | } | 
|---|
|  | 90 |  | 
|---|
| [99d4584] | 91 | void print( std::ostream & os, const Candidate & cand, Indenter indent = {} ); | 
|---|
|  | 92 |  | 
|---|
|  | 93 | void print( std::ostream & os, const CandidateList & cands, Indenter indent = {} ); | 
|---|
|  | 94 |  | 
|---|
|  | 95 | } // namespace ResolvExpr | 
|---|
|  | 96 |  | 
|---|
|  | 97 | // Local Variables: // | 
|---|
|  | 98 | // tab-width: 4 // | 
|---|
|  | 99 | // mode: c++ // | 
|---|
|  | 100 | // compile-command: "make install" // | 
|---|
|  | 101 | // End: // | 
|---|