1 /* Derivation and subsumption rules for constraints.
2 Copyright (C) 2013 Free Software Foundation, Inc.
3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
5 This file is part of GCC.
7 GCC is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 3, or (at your option)
12 GCC is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
17 You should have received a copy of the GNU General Public License
18 along with GCC; see the file COPYING3. If not see
19 <http://www.gnu.org/licenses/>. */
25 #include "coretypes.h"
29 #include "c-family/c-common.h"
30 #include "c-family/c-objc.h"
31 #include "tree-inline.h"
36 #include "diagnostic.h"
38 #include "tree-iterator.h"
49 // Increment iter distance(first, last) times.
50 template<typename I1
, typename I2
, typename I3
>
51 I1
next_by_distance (I1 iter
, I2 first
, I3 last
)
53 for ( ; first
!= last
; ++first
, ++iter
)
59 // -------------------------------------------------------------------------- //
62 // A term list is a list of propositions in the constraint language. It is
63 // used to maintain the lists of assumptions and conclusions in a proof goal.
65 // Each term list maintains an iterator that refers to the current term. This
66 // can be used by various tactics to support iteration and stateful
67 // manipulation of the list.
68 struct term_list
: std::list
<tree
>
71 term_list (const term_list
&x
);
72 term_list
& operator= (const term_list
&x
);
74 tree
current_term () { return *current
; }
75 const_tree
current_term () const { return *current
; }
89 term_list::term_list ()
90 : std::list
<tree
> (), current (end ())
94 term_list::term_list (const term_list
&x
)
96 , current (next_by_distance (begin (), x
.begin (), x
.current
))
100 term_list::operator= (const term_list
&x
)
102 std::list
<tree
>::operator=(x
);
103 current
= next_by_distance (begin (), x
.begin (), x
.current
);
107 // Insert the term T into the list before the current position, making
108 // this term current.
110 term_list::insert (tree t
)
112 current
= std::list
<tree
>::insert (current
, t
);
115 // Remove the current term form the list, repositioning to the term
116 // following the removed term. Note that the new position could be past
117 // the end of the list.
119 // The removed term is returned.
124 current
= std::list
<tree
>::erase (current
);
128 // Initialize the current term to the first in the list.
135 // Advance to the next term in the list.
142 // Returns true when the current position is past the end.
144 term_list::done () const
146 return current
== end ();
150 // -------------------------------------------------------------------------- //
153 // A goal (or subgoal) models a sequent of the form 'A |- C' where A and C are
154 // lists of assumptions and conclusions written as propositions in the
155 // constraint language (i.e., lists of trees).
158 term_list assumptions
;
159 term_list conclusions
;
163 // -------------------------------------------------------------------------- //
166 // A proof state owns a list of goals and tracks the current sub-goal.
167 // The class also provides facilities for managing subgoals and constructing
169 struct proof_state
: std::list
<proof_goal
>
173 iterator
branch (iterator i
);
176 // An alias for proof state iterators.
177 typedef proof_state::iterator goal_iterator
;
179 // Initialize the state with a single empty goal, and set that goal as the
182 proof_state::proof_state ()
183 : std::list
<proof_goal
> (1)
187 // Branch the current goal by creating a new subgoal, returning a reference to
188 // the new object. This does not update the current goal.
189 inline proof_state::iterator
190 proof_state::branch (iterator i
)
192 return insert (++i
, *i
);
196 // -------------------------------------------------------------------------- //
199 // These functions modify the current state and goal by decomposing
200 // logical expressions using the logical rules of sequent calculus for
201 // first order logic.
203 // Note that in each decomposition rule, the term T has been erased
204 // from term list before the specific rule is applied.
206 // Left-and logical rule.
208 // Gamma, P, Q |- Delta
209 // -------------------------
210 // Gamma, P and Q |- Delta
212 left_and (proof_state
&, goal_iterator i
, tree t
)
214 gcc_assert (TREE_CODE (t
) == TRUTH_ANDIF_EXPR
);
216 // Insert the operands into the current branch. Note that the
217 // final order of insertion is left-to-right.
218 term_list
&l
= i
->assumptions
;
219 l
.insert (TREE_OPERAND (t
, 1));
220 l
.insert (TREE_OPERAND (t
, 0));
223 // Left-or logical rule.
225 // Gamma, P |- Delta Gamma, Q |- Delta
226 // -----------------------------------------
227 // Gamma, P or Q |- Delta
229 left_or (proof_state
&s
, goal_iterator i
, tree t
)
231 gcc_assert (TREE_CODE (t
) == TRUTH_ORIF_EXPR
);
233 // Branch the current subgoal.
234 goal_iterator j
= s
.branch (i
);
235 term_list
&l1
= i
->assumptions
;
236 term_list
&l2
= j
->assumptions
;
238 // Insert operands into the different branches.
239 l1
.insert (TREE_OPERAND (t
, 0));
240 l2
.insert (TREE_OPERAND (t
, 1));
243 // Left-requires logical rule
244 // A requirement is effectively a conjunction of syntactic requirements.
245 // The arguments are discarded.
247 // Gamma, P1, P2, ..., Pn |- Delta
248 // --------------------------------------------------
249 // Gamma, requires(args) { P1, P2, ..., Pn } |- Delta
251 left_requires (proof_state
&, goal_iterator i
, tree t
)
253 gcc_assert (TREE_CODE (t
) == REQUIRES_EXPR
);
255 // Insert the sub-expressions into the curent term list.
256 term_list
&l
= i
->assumptions
;
257 for (tree p
= TREE_OPERAND (t
, 1); p
; p
= TREE_CHAIN (p
))
258 l
.insert (TREE_VALUE (p
));
261 // Right-and logical rule.
263 // Gamma |- P, Delta Gamma |- Q, Delta
264 // -----------------------------------------
265 // Gamma |- P and Q, Delta
267 right_and (proof_state
&s
, goal_iterator i
, tree t
)
269 gcc_assert (TREE_CODE (t
) == TRUTH_ORIF_EXPR
);
271 // Branch the current subgoal.
272 goal_iterator j
= s
.branch (i
);
273 term_list
&l1
= i
->conclusions
;
274 term_list
&l2
= j
->conclusions
;
276 // Insert operands into the different branches.
277 l1
.insert (TREE_OPERAND (t
, 0));
278 l2
.insert (TREE_OPERAND (t
, 1));
281 // Right-or logical rule.
283 // Gamma |- P, Q, Delta
284 // ------------------------
285 // Gamma |- P or Q, Delta
287 right_or (proof_state
&, goal_iterator i
, tree t
)
289 gcc_assert (TREE_CODE (t
) == TRUTH_ANDIF_EXPR
);
291 // Insert the operands into the current branch. Note that the
292 // final order of insertion is left-to-right.
293 term_list
&l
= i
->conclusions
;
294 l
.insert (TREE_OPERAND (t
, 1));
295 l
.insert (TREE_OPERAND (t
, 0));
299 // -------------------------------------------------------------------------- //
302 // The following algorithms decompose expressions into sets of atomic
305 // These decomposition strategies do not branch conclusions so that
306 // only a single term exists on the right side. These algorithms decompose
307 // expressions until we have a set of atomic sequent that contain no
308 // more logical expressions.
310 // Left decomposition.
311 // Continually decompose assumptions until there are no terms in any
312 // subgoal that can be further decomposed.
315 decompose_left_term (proof_state
&s
, goal_iterator i
)
317 term_list
&l
= i
->assumptions
;
318 tree t
= l
.current_term ();
319 switch (TREE_CODE (t
))
321 case TRUTH_ANDIF_EXPR
:
322 left_and (s
, i
, l
.erase ());
324 case TRUTH_ORIF_EXPR
:
325 left_or (s
, i
, l
.erase ());
328 left_requires (s
, i
, l
.erase ());
337 decompose_left_goal (proof_state
&s
, goal_iterator i
)
339 term_list
& l
= i
->assumptions
;
342 decompose_left_term (s
, i
);
346 decompose_left (proof_state
& s
)
348 goal_iterator iter
= s
.begin ();
349 goal_iterator end
= s
.end ();
350 for ( ; iter
!= end
; ++iter
)
351 decompose_left_goal (s
, iter
);
355 // -------------------------------------------------------------------------- //
358 // Extract a list of term lists from a proof state, and return it as a
359 // a tree (a vector of vectors).
361 // Returns a vector of terms from the given term list.
363 extract_terms (term_list
& l
)
365 tree result
= make_tree_vec (l
.size());
366 term_list::iterator iter
= l
.begin();
367 term_list::iterator end
= l
.end();
368 for (int n
= 0; iter
!= end
; ++iter
, ++n
)
369 TREE_VEC_ELT (result
, n
) = *iter
;
373 // Extract the assumption vector from the proof state s.
375 extract_assumptions (proof_state
& s
)
377 tree result
= make_tree_vec (s
.size ());
378 goal_iterator iter
= s
.begin ();
379 goal_iterator end
= s
.end ();
380 for (int n
= 0; iter
!= end
; ++iter
, ++n
)
381 TREE_VEC_ELT (result
, n
) = extract_terms (iter
->assumptions
);
388 // Decompose the required expression T into a constraint set: a
389 // vector of vectors containing only atomic propositions.
391 decompose_assumptions (tree t
)
393 // Create a proof state, and insert T as the sole assumption.
395 term_list
&l
= s
.begin ()->assumptions
;
398 // Decompose the expression into a constraint set, and then
399 // extract the terms for the AST.
401 return extract_assumptions (s
);
405 // -------------------------------------------------------------------------- //
406 // Subsumption and Entailment
408 // The following framework implements the subsumption and entailment
409 // logic used for overload resolution and lookup.
413 bool subsumes_prop(tree
, tree
);
414 bool subsumes_atom(tree
, tree
);
415 bool subsumes_and(tree
, tree
);
416 bool subsumes_or(tree
, tree
);
418 // Returns true if the assumption A matches the conclusion C. This
419 // is generally the case when A and C have the same syntax.
421 // TODO: Implement special cases for:
422 // * __is_same_as |- __is_convertible_to
423 // * __is_same_as |- __is_derived_from
424 // * Any other built-in predicates?
426 match_terms (tree a
, tree c
)
428 return cp_tree_equal (a
, c
);
431 // Returns true if the list of assumptions AS subsume the atomic
432 // proposition C. This is the case when we can find a proposition in
433 // AS that entails the conclusion C.
435 subsumes_atom (tree as
, tree c
)
437 for (int i
= 0; i
< TREE_VEC_LENGTH (as
); ++i
)
438 if (match_terms (TREE_VEC_ELT (as
, i
), c
))
443 // Returns true when both operands of C are subsumed by the assumptions AS.
445 subsumes_and (tree as
, tree c
)
447 tree l
= TREE_OPERAND (c
, 0);
448 tree r
= TREE_OPERAND (c
, 1);
449 return subsumes_prop (as
, l
) && subsumes_prop (as
, r
);
452 // Returns true when either operand of C is subsumed by the assumptions AS.
454 subsumes_or (tree as
, tree c
)
456 tree l
= TREE_OPERAND (c
, 0);
457 tree r
= TREE_OPERAND (c
, 1);
458 return subsumes_prop (as
, l
) || subsumes_prop (as
, r
);
461 // Returns true when the sub-requirements of C are subsumed by the
462 // assumptions in AS.
464 subsumes_requires (tree as
, tree c
)
466 tree t
= TREE_OPERAND (c
, 1);
467 while (t
&& subsumes_prop (as
, TREE_VALUE (t
)))
472 // Returns true when the list of assumptions AS subsumes the
473 // concluded proposition C.
475 // This is a simple recursive descent on C, matching against
476 // propositions in the assumption list AS.
478 subsumes_prop (tree as
, tree c
)
480 switch (TREE_CODE (c
))
482 case TRUTH_ANDIF_EXPR
:
483 return subsumes_and (as
, c
);
484 case TRUTH_ORIF_EXPR
:
485 return subsumes_or (as
, c
);
487 return subsumes_requires (as
, c
);
489 return subsumes_atom (as
, c
);
493 // Returns true the LEFT constraints subsume the RIGHT constraints.
494 // This is done by checking that the RIGHT requirements follow from
495 // each of the LEFT subgoals.
497 subsumes_constraints (tree left
, tree right
)
499 gcc_assert (check_constraint_info (left
));
500 gcc_assert (check_constraint_info (right
));
502 // Check that the required expression in RIGHT is subsumed by each
503 // subgoal in the assumptions of LEFT.
504 tree as
= CI_ASSUMPTIONS (left
);
505 tree c
= reduce_requirements (CI_REQUIREMENTS (right
));
506 for (int i
= 0; i
< TREE_VEC_LENGTH (as
); ++i
)
507 if (!subsumes_prop (TREE_VEC_ELT (as
, i
), c
))
515 // Returns true the LEFT constraints subsume the RIGHT constraints. Note
516 // that subsumption is a reflexive relation (e.g., <=)
518 subsumes (tree left
, tree right
)
526 return subsumes_constraints (left
, right
);