1 /* 2 * Copyright 2014 Google Inc. All rights reserved. 3 * 4 * Licensed under the Apache License, Version 2.0 (the "License"); 5 * you may not use this file except in compliance with the License. 6 * You may obtain a copy of the License at 7 * 8 * http://www.apache.org/licenses/LICENSE-2.0 9 * 10 * Unless required by applicable law or agreed to in writing, software 11 * distributed under the License is distributed on an "AS IS" BASIS, 12 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 13 * See the License for the specific language governing permissions and 14 * limitations under the License. 15 */ 16 17 #ifndef FRUIT_META_PROOF_TREES_H 18 #define FRUIT_META_PROOF_TREES_H 19 20 #include <fruit/impl/fruit_assert.h> 21 #include <fruit/impl/injection_debug_errors.h> 22 #include <fruit/impl/meta/errors.h> 23 #include <fruit/impl/meta/graph.h> 24 #include <fruit/impl/meta/set.h> 25 26 namespace fruit { 27 namespace impl { 28 namespace meta { 29 30 // Given a set of formulas Hps=Set<Hp1, ... Hp(n)> and a formula Th, Pair<Th, Hps> represents the 31 // following proof tree: 32 // 33 // Hp1 ... Hp(n) 34 // ------------- 35 // Th 36 // 37 // Hp1, ... Hp(n) must be distinct. 38 // Formulas are atomic, any type can be used as formula (except None). 39 // 40 // A proof forest is a map (i.e. a Set of Pair(s)) from each Th to the corresponding set of Hps. 41 // Note that a proof forest doesn't need to have any additional property (for example, a proof tree 42 // might contain the thesis as hypotheses, or there might be a longer loop e.g A=>B, B=>A. 43 using EmptyProofForest = EmptySet; 44 45 #if !FRUIT_NO_LOOP_CHECK 46 47 using ProofForestFindHps = GraphFindNeighbors; 48 49 // ProofForestFindLoop(F) returns a loop in the given forest as a Vector<Th1, ..., Thk> such that: 50 // IsInSet(Th1, ProofForestFindHps(Th2)), IsInSet(Th2, ProofForestFindHps(Th3)), ..., 51 // IsInSet(Th{k-1}, ProofForestFindHps(Thk)), IsInSet(Thk, ProofForestFindHps(Th1)) 52 // if there is no such loop, returns None. 53 using ProofForestFindLoop = GraphFindLoop; 54 55 #else // FRUIT_NO_LOOP_CHECK 56 57 struct ProofForestFindLoop { 58 template <typename F> 59 struct apply { 60 using type = None; 61 }; 62 }; 63 64 struct AddProofTreeToForest { 65 template <typename Forest, typename Proof> 66 struct apply { 67 using type = Vector<>; 68 }; 69 }; 70 71 struct AddProofTreeSetToForest { 72 template <typename Proofs, typename Forest> 73 struct apply { 74 using type = Vector<>; 75 }; 76 }; 77 78 #endif // FRUIT_NO_LOOP_CHECK 79 80 } // namespace meta 81 } // namespace impl 82 } // namespace fruit 83 84 #endif // FRUIT_META_PROOF_TREES_H 85