| [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 ) | 
|---|
| [4e13e2a] | 53 | : expr( x ), cost( Cost::zero ), cvtCost( Cost::zero ), env( e ), open(), need() { | 
|---|
|  | 54 | assert(x->result); | 
|---|
|  | 55 | } | 
|---|
| [4b7cce6] | 56 |  | 
|---|
| [c8e4d2f8] | 57 | Candidate( const Candidate & o, const ast::Expr * x, const Cost & addedCost = Cost::zero ) | 
|---|
|  | 58 | : expr( x ), cost( o.cost + addedCost ), cvtCost( Cost::zero ), env( o.env ), open( o.open ), | 
|---|
| [4e13e2a] | 59 | need( o.need ) { | 
|---|
|  | 60 | assert(x->result); | 
|---|
|  | 61 | } | 
|---|
| [d76f32c] | 62 |  | 
|---|
| [9d5089e] | 63 | Candidate( | 
|---|
| [4e13e2a] | 64 | const ast::Expr * x, const ast::TypeEnvironment & e, const ast::OpenVarSet & o, | 
|---|
| [9d5089e] | 65 | const ast::AssertionSet & n, const Cost & c, const Cost & cvt = Cost::zero ) | 
|---|
| [4e13e2a] | 66 | : expr( x ), cost( c ), cvtCost( cvt ), env( e ), open( o ), need( n.begin(), n.end() ) { | 
|---|
|  | 67 | assert(x->result); | 
|---|
|  | 68 | } | 
|---|
| [9d5089e] | 69 |  | 
|---|
| [d76f32c] | 70 | Candidate( | 
|---|
|  | 71 | const ast::Expr * x, ast::TypeEnvironment && e, ast::OpenVarSet && o, | 
|---|
|  | 72 | ast::AssertionSet && n, const Cost & c, const Cost & cvt = Cost::zero ) | 
|---|
|  | 73 | : expr( x ), cost( c ), cvtCost( cvt ), env( std::move( e ) ), open( std::move( o ) ), | 
|---|
| [4e13e2a] | 74 | need( n.begin(), n.end() ) { | 
|---|
|  | 75 | assert(x->result); | 
|---|
|  | 76 | } | 
|---|
| [99d4584] | 77 | }; | 
|---|
|  | 78 |  | 
|---|
|  | 79 | /// Shared reference to a candidate | 
|---|
|  | 80 | using CandidateRef = std::shared_ptr< Candidate >; | 
|---|
|  | 81 |  | 
|---|
|  | 82 | /// List of candidates | 
|---|
|  | 83 | using CandidateList = std::vector< CandidateRef >; | 
|---|
|  | 84 |  | 
|---|
| [4b7cce6] | 85 | /// Sum the cost of a list of candidates | 
|---|
|  | 86 | static inline Cost sumCost( const CandidateList & candidates ) { | 
|---|
|  | 87 | Cost total = Cost::zero; | 
|---|
|  | 88 | for ( const CandidateRef & r : candidates ) { total += r->cost; } | 
|---|
|  | 89 | return total; | 
|---|
|  | 90 | } | 
|---|
|  | 91 |  | 
|---|
| [d57e349] | 92 | /// Holdover behaviour from old `findMinCost` -- xxx -- can maybe be eliminated? | 
|---|
| [46da46b] | 93 | /* | 
|---|
| [d57e349] | 94 | static inline void promoteCvtCost( CandidateList & candidates ) { | 
|---|
|  | 95 | for ( CandidateRef & r : candidates ) { | 
|---|
|  | 96 | r->cost = r->cvtCost; | 
|---|
|  | 97 | } | 
|---|
|  | 98 | } | 
|---|
| [46da46b] | 99 | */ | 
|---|
| [d57e349] | 100 |  | 
|---|
| [99d4584] | 101 | void print( std::ostream & os, const Candidate & cand, Indenter indent = {} ); | 
|---|
|  | 102 |  | 
|---|
|  | 103 | void print( std::ostream & os, const CandidateList & cands, Indenter indent = {} ); | 
|---|
|  | 104 |  | 
|---|
|  | 105 | } // namespace ResolvExpr | 
|---|
|  | 106 |  | 
|---|
|  | 107 | // Local Variables: // | 
|---|
|  | 108 | // tab-width: 4 // | 
|---|
|  | 109 | // mode: c++ // | 
|---|
|  | 110 | // compile-command: "make install" // | 
|---|
|  | 111 | // End: // | 
|---|