Add C++ Concepts TS support.

gcc/c-family/
	* c-common.c (c_common_reswords): Add __is_same_as, concept, requires.
	* c-common.h (enum rid): Add RID_IS_SAME_AS, RID_CONCEPT, RID_REQUIRES.
	(D_CXX_CONCEPTS, D_CXX_CONCEPTS_FLAGS): New.
	* c-cppbuiltin.c (c_cpp_builtins): Define __cpp_concepts.
	* c-opts.c (set_std_cxx1z): Set flag_concepts.
	* c.opt (fconcepts): New.
gcc/cp/
	* constraint.cc, logic.cc: New files.
	* Make-lang.in (CXX_AND_OBJCXX_OBJS): Add constraint.o and logic.o.
	(c++.tags): Also process .cc files.
	* call.c (enum rejection_reason_code): Add rr_constraint_failure.
	(print_z_candidate): Handle it.
	(constraint_failure): New.
	(add_function_candidate): Check constraints.
	(build_new_function_call): Handle evaluating concepts.
	(joust): Check more_constrained.
	* class.c (add_method): Check equivalently_constrained.
	(build_clone): Copy constraints.
	(currently_open_class): Return tree.
	(resolve_address_of_overloaded_function): Check constraints.
	* constexpr.c (cxx_eval_constant_expression): Handle REQUIRES_EXPR.
	(potential_constant_expression_1): Likewise.
	* cp-objcp-common.c (cp_tree_size): Handle CONSTRAINT_INFO.
	(cp_common_init_ts): Handle WILDCARD_DECL and REQUIRES_EXPR.
	* cp-tree.def: Add CONSTRAINT_INFO, WILDCARD_DECL, REQUIRES_EXPR,
	SIMPLE_REQ, TYPE_REQ, COMPOUND_REQ, NESTED_REQ, PRED_CONSTR,
	EXPR_CONSTR, TYPE_CONSTR, ICONV_CONSTR, DEDUCT_CONSTR,
	EXCEPT_CONSTR, PARM_CONSTR, CONJ_CONSTR, DISJ_CONSTR.
	* cp-tree.h (struct tree_constraint_info, check_nonnull)
	(check_constraint_info, CI_TEMPLATE_REQS, CI_DECLARATOR_REQS)
	(CI_ASSOCIATED_CONSTRAINTS, CI_NORMALIZED_CONSTRAINTS)
	(CI_ASSUMPTIONS, TEMPLATE_PARMS_CONSTRAINTS)
	(TEMPLATE_PARM_CONSTRAINTS, COMPOUND_REQ_NOEXCEPT_P)
	(PLACEHOLDER_TYPE_CONSTRAINTS, PRED_CONSTR_EXPR, EXPR_CONSTR_EXPR)
	(TYPE_CONSTR_TYPE, ICONV_CONSTR_EXPR, ICONV_CONSTR_TYPE)
	(DEDUCT_CONSTR_EXPR, DEDUCT_CONSTR_PATTERN)
	(DEDUCT_CONSTR_PLACEHOLDER, EXCEPT_CONSTR_EXPR, PARM_CONSTR_PARMS)
	(PARM_CONSTR_OPERAND, CONSTRAINT_VAR_P, CONSTRAINED_PARM_CONCEPT)
	(CONSTRAINED_PARM_EXTRA_ARGS, CONSTRAINED_PARM_PROTOTYPE)
	(DECL_DECLARED_CONCEPT_P, WILDCARD_PACK_P, struct cp_unevaluated)
	(struct local_specialization_stack, enum auto_deduction_context)
	(variable_concept_p, concept_template_p)
	(struct deferring_access_check_sentinel): New.
	(enum cp_tree_node_structure_enum): Add TS_CP_CONSTRAINT_INFO.
	(union lang_tree_node): Add constraint_info field.
	(struct lang_decl_base): Add concept_p flag.
	(enum cp_decl_spec): Add ds_concept.
	(struct cp_declarator): Add requires_clause.
	* cxx-pretty-print.c (cxx_pretty_printer::primary_expression)
	(cxx_pretty_printer::expression): Handle REQUIRES_EXPR,
	TRAIT_EXPR, *_CONSTR.
	(pp_cxx_parameter_declaration_clause): Accept a chain of
	PARM_DECLs.
	(cxx_pretty_printer::declarator): Print requires-clause.
	(pp_cxx_template_declaration): Likewise.
	(pp_cxx_trait_expression): Handle CPTK_IS_SAME_AS.
	(pp_cxx_requires_clause, pp_cxx_requirement)
	(pp_cxx_requirement_list, pp_cxx_requirement_body)
	(pp_cxx_requires_expr, pp_cxx_simple_requirement)
	(pp_cxx_type_requirement, pp_cxx_compound_requirement)
	(pp_cxx_nested_requirement, pp_cxx_predicate_constraint)
	(pp_cxx_expression_constraint, pp_cxx_type_constraint)
	(pp_cxx_implicit_conversion_constraint)
	(pp_cxx_argument_deduction_constraint)
	(pp_cxx_exception_constraint, pp_cxx_parameterized_constraint)
	(pp_cxx_conjunction, pp_cxx_disjunction, pp_cxx_constraint): New.
	* cxx-pretty-print.h: Declare them.
	* decl.c (decls_match): Compare constraints.
	(duplicate_decls): Likewise.  Remove constraints before freeing.
	(cxx_init_decl_processing): Call init_constraint_processing.
	(cp_finish_decl): Diagnose concept without initializer.
	(grokfndecl, grokvardecl): Handle concepts and constraints.
	(grokdeclarator): Handle concept, requires-clause.
	(grokparms): No longer static.
	(xref_tag_1): Check constraints.
	(finish_function): Call check_function_concept.
	(cp_tree_node_structure): Handle CONSTRAINT_INFO.
	(check_concept_refinement, is_concept_var, check_concept_fn): New.
	* decl2.c (check_classfn): Compare constraints.
	(mark_used): Don't instantiate concepts.
	* error.c (dump_template_decl): Print constraints.
	(dump_function_decl): Likewise.
	(dump_expr): Handle REQUIRES_EXPR, *_REQ, *_CONSTR.
	* lex.c (init_reswords): Set D_CXX_CONCEPTS.
	* method.c (implicitly_declare_fn): Copy constraints from
	inherited ctor.
	* parser.h (struct cp_parser): Add in_result_type_constraint_p and
	prevent_constrained_type_specifiers fields.
	* parser.c (make_call_declarator): Add requires_clause parm.
	(cp_parser_new): Clear prevent_constrained_type_specifiers.
	(cp_parser_primary_expression): Handle RID_IS_SAME_AS, RID_REQUIRES.
	(cp_parser_postfix_expression): Set prevent_constrained_type_specifiers.
	(cp_parser_trait_expr): Handle RID_IS_SAME_AS.
	(cp_parser_declaration): Handle concept introduction.
	(cp_parser_member_declaration): Likewise.
	(cp_parser_template_parameter): Handle constrained parameter.
	(cp_parser_type_parameter): Handle constraints.
	(cp_parser_decl_specifier_seq): Handle RID_CONCEPT.
	(cp_parser_template_id): Handle partial concept id.
	(cp_parser_type_name): Add overload that takes typename_keyword_p.
	Handle constrained parameter.
	(cp_parser_nonclass_name): Handle concept names.
	(cp_parser_alias_declaration): Handle constraints.
	(cp_parser_late_return_type_opt): Also handle requires-clause.
	(cp_parser_type_id_1): Handle deduction constraint.
	(cp_parser_parameter_declaration): Handle constrained parameters.
	(cp_parser_class_specifier_1): Handle constraints.
	(cp_parser_template_declaration_after_parameters): Split out from
	cp_parser_template_declaration_after_export.
	(cp_parser_single_declaration): Handle constraints.
	(synthesize_implicit_template_parm): Handle constraints.
	(cp_parser_maybe_concept_name, cp_parser_maybe_partial_concept_id)
	(cp_parser_introduction_list, get_id_declarator)
	(get_unqualified_id, is_constrained_parameter)
	(cp_parser_check_constrained_type_parm)
	(cp_parser_constrained_type_template_parm)
	(cp_parser_constrained_template_template_parm)
	(constrained_non_type_template_parm, finish_constrained_parameter)
	(declares_constrained_type_template_parameter)
	(declares_constrained_template_template_parameter)
	(check_type_concept, cp_parser_maybe_constrained_type_specifier)
	(cp_parser_maybe_concept_name, cp_parser_maybe_partial_concept_id)
	(cp_parser_requires_clause, cp_parser_requires_clause_opt)
	(cp_parser_requires_expression)
	(cp_parser_requirement_parameter_list, cp_parser_requirement_body)
	(cp_parser_requirement_list, cp_parser_requirement)
	(cp_parser_simple_requirement, cp_parser_type_requirement)
	(cp_parser_compound_requirement, cp_parser_nested_requirement)
	(cp_parser_template_introduction)
	(cp_parser_explicit_template_declaration)
	(get_concept_from_constraint): New.
	* pt.c (local_specialization_stack): Implement.
	(maybe_new_partial_specialization): New.
	(maybe_process_partial_specialization): Use it.
	(retrieve_local_specialization, register_local_specialization)
	(template_parm_to_arg, build_template_decl, extract_fnparm_pack)
	(tsubst_expr): No longer static.
	(spec_hasher::equal): Compare constraints.
	(determine_specialization): Handle constraints.
	(check_explicit_specialization): Handle concepts.
	(process_template_parm): Handle constraints.
	(end_template_parm_list): Add overload taking no arguments.
	(process_partial_specialization): Handle concepts and constraints.
	Register partial specializations of variable templates.
	(redeclare_class_template): Handle constraints.
	(convert_template_argument): Handle WILDCARD_DECL.  Check
	is_compatible_template_arg.
	(coerce_template_parameter_pack): Handle wildcard packs.
	(coerce_template_parms): DR 1430 also applies to concepts.  Add
	overloads taking fewer parameters.
	(lookup_template_class_1): Handle constraints.
	(lookup_template_variable): Concepts are always bool.
	(finish_template_variable): Handle concepts and constraints.
	(tsubst_friend_class): Handle constraints.
	(gen_elem_of_pack_expansion_instantiation): Handle constraints.
	(tsubst_pack_expansion): Handle local parameters.
	(tsubst_decl) [FUNCTION_DECL]: Handle constraints.
	(tsubst) [TEMPLATE_TYPE_PARM]: Handle deduction constraints.
	(tsubst_copy_and_build): Handle REQUIRES_EXPR.
	(more_specialized_fn, more_specialized_partial_spec): Check constraints.
	(more_specialized_inst): Split out from most_specialized_instantiation.
	(most_specialized_partial_spec): Check constraints.
	(instantiate_decl): Never instantiate a concept.
	(value_dependent_expression_p): Handle REQUIRES_EXPR, TYPE_REQ,
	variable concepts.
	(type_dependent_expression_p): Handle WILDCARD_DECL, REQUIRES_EXPR.
	(instantiation_dependent_r): Handle REQUIRES_EXPR and concepts.
	(do_auto_deduction): Add overload taking tsubst flags and context enum.
	Handle constraints.
	(get_template_for_ordering, most_constrained_function)
	(is_compatible_template_arg, convert_wildcard_argument)
	(struct	constr_entry, struct constr_hasher, decl_constraints)
	(valid_constraints_p, get_constraints, set_constraints)
	(remove_constraints, init_constraint_processing): New.
	* ptree.c (cxx_print_xnode): Handle CONSTRAINT_INFO.
	* search.c (lookup_member): Do lookup in the open partial
	instantiation.
	* semantics.c (finish_template_template_parm): Handle constraints.
	(fixup_template_type): New.
	(finish_template_type): Call it.
	(trait_expr_value, finish_trait_expr): Handle CPTK_IS_SAME_AS.
	* tree.c (cp_tree_equal): Handle local parameters, CONSTRAINT_INFO.
	(cp_walk_subtrees): Handle REQUIRES_EXPR.
	* typeck.c (cp_build_function_call_vec): Check constraints.

Co-Authored-By: Braden Obrzut <admin@maniacsvault.net>
Co-Authored-By: Jason Merrill <jason@redhat.com>

From-SVN: r226713

1 files changed, 497 insertions, 0 deletions

diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
new file mode 100644
index 0000000..7e01640
--- /dev/null
+++ b/gcc/cp/logic.cc
@@ -0,0 +1,497 @@
+/* Derivation and subsumption rules for constraints.
+   Copyright (C) 2013-2015 Free Software Foundation, Inc.
+   Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 3, or (at your option)
+any later version.
+
+GCC is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "tm.h"
+#include "hash-set.h"
+#include "machmode.h"
+#include "vec.h"
+#include "double-int.h"
+#include "input.h"
+#include "alias.h"
+#include "symtab.h"
+#include "wide-int.h"
+#include "inchash.h"
+#include "tree.h"
+#include "stringpool.h"
+#include "attribs.h"
+#include "intl.h"
+#include "flags.h"
+#include "cp-tree.h"
+#include "c-family/c-common.h"
+#include "c-family/c-objc.h"
+#include "cp-objcp-common.h"
+#include "tree-inline.h"
+#include "decl.h"
+#include "toplev.h"
+#include "type-utils.h"
+
+#include <list>
+
+namespace {
+
+// Helper algorithms
+
+// Increment iter distance(first, last) times.
+template<typename I1, typename I2, typename I3>
+  I1 next_by_distance (I1 iter, I2 first, I3 last)
+  {
+    for ( ; first != last; ++first, ++iter)
+      ;
+    return iter;
+  }
+
+/*---------------------------------------------------------------------------
+                           Proof state
+---------------------------------------------------------------------------*/
+
+/* A term list is a list of atomic constraints. It is used
+   to maintain the lists of assumptions and conclusions in a
+   proof goal.
+
+   Each term list maintains an iterator that refers to the current
+   term. This can be used by various tactics to support iteration
+   and stateful manipulation of the list. */
+struct term_list : std::list<tree>
+{
+  term_list ();
+  term_list (const term_list &x);
+  term_list& operator= (const term_list &x);
+
+  tree       current_term ()       { return *current; }
+  const_tree current_term () const { return *current; }
+
+
+  void insert (tree t);
+  tree erase ();
+
+  void start ();
+  void next ();
+  bool done() const;
+
+  iterator current;
+};
+
+inline
+term_list::term_list ()
+  : std::list<tree> (), current (end ())
+{ }
+
+inline
+term_list::term_list (const term_list &x)
+  : std::list<tree> (x)
+  , current (next_by_distance (begin (), x.begin (), x.current))
+{ }
+
+inline term_list&
+term_list::operator= (const term_list &x)
+{
+  std::list<tree>::operator=(x);
+  current = next_by_distance (begin (), x.begin (), x.current);
+  return *this;
+}
+
+/* Try saving the term T into the list of terms. If
+   T is already in the list of terms, then no action is
+   performed. Otherwise, insert T before the current
+   position, making this term current.
+
+   Note that not inserting terms is an optimization
+   that corresponds to the structural rule of
+   contraction.
+
+   NOTE: With the contraction rule, this data structure
+   would be more efficiently represented as an ordered set
+   or hash set.  */
+void
+term_list::insert (tree t)
+{
+  /* Search the current term list. If there is already
+     a matching term, do not add the new one.  */
+  for (iterator i = begin(); i != end(); ++i)
+    if (cp_tree_equal (*i, t))
+      return;
+
+  current = std::list<tree>::insert (current, t);
+}
+
+/* Remove the current term from the list, repositioning to
+   the term following the removed term. Note that the new
+   position could be past the end of the list.
+
+   The removed term is returned. */
+inline tree
+term_list::erase ()
+{
+  tree t = *current;
+  current = std::list<tree>::erase (current);
+  return t;
+}
+
+/* Initialize the current term to the first in the list. */
+inline void
+term_list::start ()
+{
+  current = begin ();
+}
+
+/* Advance to the next term in the list. */
+inline void
+term_list::next ()
+{
+  ++current;
+}
+
+/* Returns true when the current position is past the end. */
+inline bool
+term_list::done () const
+{
+  return current == end ();
+}
+
+
+/* A goal (or subgoal) models a sequent of the form
+   'A |- C' where A and C are lists of assumptions and
+   conclusions written as propositions in the constraint
+   language (i.e., lists of trees).
+*/
+struct proof_goal
+{
+  term_list assumptions;
+  term_list conclusions;
+};
+
+/* A proof state owns a list of goals and tracks the
+   current sub-goal. The class also provides facilities
+   for managing subgoals and constructing term lists. */
+struct proof_state : std::list<proof_goal>
+{
+  proof_state ();
+
+  iterator branch (iterator i);
+};
+
+/* An alias for proof state iterators. */
+typedef proof_state::iterator goal_iterator;
+
+/* Initialize the state with a single empty goal,
+   and set that goal as the current subgoal. */
+inline
+proof_state::proof_state ()
+  : std::list<proof_goal> (1)
+{ }
+
+
+/* Branch the current goal by creating a new subgoal,
+   returning a reference to // the new object. This does
+   not update the current goal. */
+inline proof_state::iterator
+proof_state::branch (iterator i)
+{
+  gcc_assert (i != end());
+  proof_goal& g = *i;
+  return insert (++i, g);
+}
+
+/*---------------------------------------------------------------------------
+                           Logical rules
+---------------------------------------------------------------------------*/
+
+/*These functions modify the current state and goal by decomposing
+  logical expressions using the logical rules of sequent calculus for
+  first order logic.
+
+  Note that in each decomposition rule, the term T has been erased
+  from term list before the specific rule is applied. */
+
+/* The left logical rule for conjunction adds both operands
+   to the current set of constraints. */
+void
+left_conjunction (proof_state &, goal_iterator i, tree t)
+{
+  gcc_assert (TREE_CODE (t) == CONJ_CONSTR);
+
+  /* Insert the operands into the current branch. Note that the
+     final order of insertion is left-to-right. */
+  term_list &l = i->assumptions;
+  l.insert (TREE_OPERAND (t, 1));
+  l.insert (TREE_OPERAND (t, 0));
+}
+
+/* The left logical rule for disjunction creates a new goal,
+   adding the first operand to the original set of
+   constraints and the second operand to the new set
+   of constraints. */
+void
+left_disjunction (proof_state &s, goal_iterator i, tree t)
+{
+  gcc_assert (TREE_CODE (t) == DISJ_CONSTR);
+
+  /* Branch the current subgoal. */
+  goal_iterator j = s.branch (i);
+  term_list &l1 = i->assumptions;
+  term_list &l2 = j->assumptions;
+
+  /* Insert operands into the different branches. */
+  l1.insert (TREE_OPERAND (t, 0));
+  l2.insert (TREE_OPERAND (t, 1));
+}
+
+/* The left logical rules for parameterized constraints
+   adds its operand to the current goal. The list of
+   parameters are effectively discarded. */
+void
+left_parameterized_constraint (proof_state &, goal_iterator i, tree t)
+{
+  gcc_assert (TREE_CODE (t) == PARM_CONSTR);
+  term_list &l = i->assumptions;
+  l.insert (PARM_CONSTR_OPERAND (t));
+}
+
+/*---------------------------------------------------------------------------
+                           Decomposition
+---------------------------------------------------------------------------*/
+
+/* The following algorithms decompose expressions into sets of
+   atomic propositions. In terms of the sequent calculus, these
+   functions exercise the logical rules only.
+
+   This is equivalent, for the purpose of determining subsumption,
+   to rewriting a constraint in disjunctive normal form. It also
+   allows the resulting assumptions to be used as declarations
+   for the purpose of separate checking. */
+
+/* Apply the left logical rules to the proof state. */
+void
+decompose_left_term (proof_state &s, goal_iterator i)
+{
+  term_list &l = i->assumptions;
+  tree t = l.current_term ();
+  switch (TREE_CODE (t))
+    {
+    case CONJ_CONSTR:
+      left_conjunction (s, i, l.erase ());
+      break;
+    case DISJ_CONSTR:
+      left_disjunction (s, i, l.erase ());
+      break;
+    case PARM_CONSTR:
+      left_parameterized_constraint (s, i, l.erase ());
+      break;
+    default:
+      l.next ();
+      break;
+    }
+}
+
+/* Apply the left logical rules of the sequent calculus
+   until the current goal is fully decomposed into atomic
+   constraints. */
+void
+decompose_left_goal (proof_state &s, goal_iterator i)
+{
+  term_list& l = i->assumptions;
+  l.start ();
+  while (!l.done ())
+    decompose_left_term (s, i);
+}
+
+/* Apply the left logical rules of the sequent calculus
+   until the antecedents are fully decomposed into atomic
+   constraints. */
+void
+decompose_left (proof_state& s)
+{
+  goal_iterator iter = s.begin ();
+  goal_iterator end = s.end ();
+  for ( ; iter != end; ++iter)
+    decompose_left_goal (s, iter);
+}
+
+/* Returns a vector of terms from the term list L. */
+tree
+extract_terms (term_list& l)
+{
+  tree result = make_tree_vec (l.size());
+  term_list::iterator iter = l.begin();
+  term_list::iterator end = l.end();
+  for (int n = 0; iter != end; ++iter, ++n)
+    TREE_VEC_ELT (result, n) = *iter;
+  return result;
+}
+
+/* Extract the assumptions from the proof state S
+   as a vector of vectors of atomic constraints. */
+inline tree
+extract_assumptions (proof_state& s)
+{
+  tree result = make_tree_vec (s.size ());
+  goal_iterator iter = s.begin ();
+  goal_iterator end = s.end ();
+  for (int n = 0; iter != end; ++iter, ++n)
+    TREE_VEC_ELT (result, n) = extract_terms (iter->assumptions);
+  return result;
+}
+
+} // namespace
+
+/* Decompose the required expression T into a constraint set: a
+   vector of vectors containing only atomic propositions. If T is
+   invalid, return an error. */
+tree
+decompose_assumptions (tree t)
+{
+  if (!t || t == error_mark_node)
+    return t;
+
+  /* Create a proof state, and insert T as the sole assumption. */
+  proof_state s;
+  term_list &l = s.begin ()->assumptions;
+  l.insert (t);
+
+  /* Decompose the expression into a constraint set, and then
+     extract the terms for the AST. */
+  decompose_left (s);
+  return extract_assumptions (s);
+}
+
+
+/*---------------------------------------------------------------------------
+                           Subsumption Rules
+---------------------------------------------------------------------------*/
+
+namespace {
+
+bool subsumes_constraint (tree, tree);
+bool subsumes_conjunction (tree, tree);
+bool subsumes_disjunction (tree, tree);
+bool subsumes_parameterized_constraint (tree, tree);
+bool subsumes_atomic_constraint (tree, tree);
+
+/* Returns true if the assumption A matches the conclusion C. This
+   is generally the case when A and C have the same syntax.
+
+   NOTE: There will be specialized matching rules to accommodate
+   type equivalence, conversion, inheritance, etc. But this is not
+   in the current concepts draft. */
+inline bool
+match_terms (tree a, tree c)
+{
+  return cp_tree_equal (a, c);
+}
+
+/* Returns true if the list of assumptions AS subsumes the atomic
+   proposition C. This is the case when we can find a proposition
+  in AS that entails the conclusion C. */
+bool
+subsumes_atomic_constraint (tree as, tree c)
+{
+  for (int i = 0; i < TREE_VEC_LENGTH (as); ++i)
+    if (match_terms (TREE_VEC_ELT (as, i), c))
+      return true;
+  return false;
+}
+
+/* Returns true when both operands of C are subsumed by the
+   assumptions AS. */
+inline bool
+subsumes_conjunction (tree as, tree c)
+{
+  tree l = TREE_OPERAND (c, 0);
+  tree r = TREE_OPERAND (c, 1);
+  return subsumes_constraint (as, l) && subsumes_constraint (as, r);
+}
+
+/* Returns true when either operand of C is subsumed by the
+   assumptions AS. */
+inline bool
+subsumes_disjunction (tree as, tree c)
+{
+  tree l = TREE_OPERAND (c, 0);
+  tree r = TREE_OPERAND (c, 1);
+  return subsumes_constraint (as, l) || subsumes_constraint (as, r);
+}
+
+/* Returns true when the operand of C is subsumed by the
+   assumptions in AS. The parameters are not considered in
+   the subsumption rules. */
+bool
+subsumes_parameterized_constraint (tree as, tree c)
+{
+  tree t = PARM_CONSTR_OPERAND (c);
+  return subsumes_constraint (as, t);
+}
+
+
+/* Returns true when the list of assumptions AS subsumes the
+   concluded proposition C. This is a simple recursive descent
+   on C, matching against propositions in the assumption list AS. */
+bool
+subsumes_constraint (tree as, tree c)
+{
+  switch (TREE_CODE (c))
+    {
+    case CONJ_CONSTR:
+      return subsumes_conjunction (as, c);
+    case DISJ_CONSTR:
+      return subsumes_disjunction (as, c);
+    case PARM_CONSTR:
+      return subsumes_parameterized_constraint (as, c);
+    default:
+      return subsumes_atomic_constraint (as, c);
+    }
+}
+
+/* Returns true if the LEFT constraints subsume the RIGHT constraints.
+   This is done by checking that the RIGHT requirements follow from
+   each of the LEFT subgoals. */
+bool
+subsumes_constraints_nonnull (tree left, tree right)
+{
+  gcc_assert (check_constraint_info (left));
+  gcc_assert (check_constraint_info (right));
+
+  /* Check that the required expression in RIGHT is subsumed by each
+     subgoal in the assumptions of LEFT. */
+  tree as = CI_ASSUMPTIONS (left);
+  tree c = CI_NORMALIZED_CONSTRAINTS (right);
+  for (int i = 0; i < TREE_VEC_LENGTH (as); ++i)
+    if (!subsumes_constraint (TREE_VEC_ELT (as, i), c))
+      return false;
+  return true;
+}
+
+} /* namespace */
+
+/* Returns true if the LEFT constraints subsume the RIGHT
+   constraints. */
+bool
+subsumes (tree left, tree right)
+{
+  if (left == right)
+    return true;
+  if (!left)
+    return false;
+  if (!right)
+    return true;
+  return subsumes_constraints_nonnull (left, right);
+}