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_PROOF_TREE_COMPARISON_H 18 #define FRUIT_PROOF_TREE_COMPARISON_H 19 20 #if !FRUIT_EXTRA_DEBUG && !FRUIT_IN_META_TEST 21 #error "This file should only be included in debug mode or in tests." 22 #endif 23 24 namespace fruit { 25 namespace impl { 26 namespace meta { 27 28 // Checks whether Proof is entailed by Forest, i.e. whether there is a corresponding Proof1 in Forest with the same 29 // thesis 30 // and with the same hypotheses as Proof (or a subset). 31 struct IsProofEntailedByForest { 32 template <typename ProofTh, typename ProofHps, typename Forest> 33 struct apply { 34 using ForestHps = FindInMap(Forest, ProofTh); 35 using type = If(IsNone(ForestHps), Bool<false>, IsContained(ForestHps, ProofHps)); 36 }; 37 }; 38 39 struct IsForestEntailedByForest { 40 template <typename EntailedForest, typename Forest> 41 struct apply { 42 struct Helper { 43 template <typename CurrentResult, typename EntailedProof> 44 struct apply; 45 46 template <typename CurrentResult, typename EntailedProofTh, typename EntailedProofHps> 47 struct apply<CurrentResult, Pair<EntailedProofTh, EntailedProofHps>> { 48 using type = And(CurrentResult, IsProofEntailedByForest(EntailedProofTh, EntailedProofHps, Forest)); 49 }; 50 }; 51 52 using type = FoldVector(EntailedForest, Helper, Bool<true>); 53 }; 54 }; 55 56 // Given two proof trees, check if they are equal. 57 // Only for debugging. 58 struct IsProofTreeEqualTo { 59 template <typename Proof1, typename Proof2> 60 struct apply { 61 using type = And(IsSame(typename Proof1::First, typename Proof2::First), 62 IsSameSet(typename Proof1::Second, typename Proof2::Second)); 63 }; 64 }; 65 66 // Given two proofs forests, check if they are equal. 67 // This is not very efficient, consider re-implementing if it will be used often. 68 // Only for debugging. 69 struct IsForestEqualTo { 70 template <typename Forest1, typename Forest2> 71 struct apply { 72 using type = And(IsForestEntailedByForest(Forest1, Forest2), IsForestEntailedByForest(Forest2, Forest1)); 73 }; 74 }; 75 76 // Only for debugging, similar to checking IsProofEntailedByForest but gives a detailed error. 77 // Only for debugging. 78 struct CheckProofEntailedByForest { 79 template <typename ProofTh, typename ProofHps, typename Forest> 80 struct apply { 81 using ForestHps = FindInMap(Forest, ProofTh); 82 using type = If(IsNone(ForestHps), 83 ConstructError(ProofNotEntailedByForestBecauseThNotFoundErrorTag, ProofTh, GetMapKeys(Forest)), 84 If(IsContained(ForestHps, ProofHps), Bool<true>, 85 ConstructError(ProofNotEntailedByForestBecauseHpsNotASubsetErrorTag, ForestHps, ProofHps, 86 SetDifference(ForestHps, ProofHps)))); 87 }; 88 }; 89 90 // Only for debugging, similar to checking IsProofEntailedByForest but gives a detailed error. 91 // Only for debugging. 92 struct CheckForestEntailedByForest { 93 template <typename EntailedForest, typename Forest> 94 struct apply { 95 struct Helper { 96 template <typename CurrentResult, typename EntailedProof> 97 struct apply; 98 99 template <typename CurrentResult, typename EntailedProofTh, typename EntailedProofHps> 100 struct apply<CurrentResult, Pair<EntailedProofTh, EntailedProofHps>> { 101 using type = PropagateError(CurrentResult, 102 CheckProofEntailedByForest(EntailedProofTh, EntailedProofHps, Forest)); 103 }; 104 }; 105 106 using type = FoldVector(EntailedForest, Helper, Bool<true>); 107 }; 108 }; 109 110 // Given two proofs forests, check if they are equal. 111 // This is not very efficient, consider re-implementing if it will be used often. 112 // Only for debugging. 113 struct CheckForestEqualTo { 114 template <typename Forest1, typename Forest2> 115 struct apply { 116 using type = PropagateError(CheckForestEntailedByForest(Forest1, Forest2), 117 CheckForestEntailedByForest(Forest2, Forest1)); 118 }; 119 }; 120 121 } // namespace meta 122 } // namespace impl 123 } // namespace fruit 124 125 #endif // FRUIT_PROOF_TREE_COMPARISON_H 126