From 1f967dad6fb973b028034985b9635513e3a8391f Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Wed, 15 May 2019 21:34:16 -0700 Subject: [PATCH 1/8] Add a match exhaustion check --- include/tvm/relay/pass.h | 18 +++ src/relay/ir/alpha_equal.cc | 21 ++- src/relay/pass/match_exhaustion.cc | 230 +++++++++++++++++++++++++++++ src/relay/pass/match_exhaustion.h | 47 ++++++ 4 files changed, 312 insertions(+), 4 deletions(-) create mode 100644 src/relay/pass/match_exhaustion.cc create mode 100644 src/relay/pass/match_exhaustion.h diff --git a/include/tvm/relay/pass.h b/include/tvm/relay/pass.h index 67cc5df82407..896687ba0524 100644 --- a/include/tvm/relay/pass.h +++ b/include/tvm/relay/pass.h @@ -122,6 +122,24 @@ TVM_DLL bool AlphaEqual(const Expr& e1, const Expr& e2); */ TVM_DLL bool AlphaEqual(const Type& t1, const Type& t2); +/*! + * \brief Compare two patterns for structural equivalence. + * + * This comparison operator respects scoping and compares + * patterns without regard to variable choice. + * + * For example: `A(x, _, y)` is equal to `A(z, _, a)`. + * + * See https://en.wikipedia.org/wiki/Lambda_calculus#Alpha_equivalence + * for more details. + * + * \param t1 The left hand pattern. + * \param t2 The right hand pattern. + * + * \return true if equal, otherwise false + */ +TVM_DLL bool AlphaEqual(const Pattern& t1, const Pattern& t2); + /*! * \brief Add abstraction over a function * diff --git a/src/relay/ir/alpha_equal.cc b/src/relay/ir/alpha_equal.cc index 81017d4fddfa..f7a5646a81ec 100644 --- a/src/relay/ir/alpha_equal.cc +++ b/src/relay/ir/alpha_equal.cc @@ -60,6 +60,10 @@ class AlphaEqualHandler: if (!rhs->derived_from()) return false; return ExprEqual(Downcast(lhs), Downcast(rhs)); } + if (lhs->derived_from()) { + if (!rhs->derived_from()) return false; + return PatternEqual(Downcast(lhs), Downcast(rhs)); + } return AttrEqual(lhs, rhs); } @@ -110,6 +114,15 @@ class AlphaEqualHandler: } } + /*! + * Check equality of two patterns. + */ + bool PatternEqual(const Pattern& lhs, const Pattern& rhs) { + if (lhs.same_as(rhs)) return true; + if (!lhs.defined() || !rhs.defined()) return false; + return VisitPattern(lhs, rhs); + } + protected: /*! * \brief Check if data type equals each other. @@ -440,10 +453,6 @@ class AlphaEqualHandler: return PatternEqual(lhs->lhs, rhs->lhs) && ExprEqual(lhs->rhs, rhs->rhs); } - bool PatternEqual(const Pattern& lhs, const Pattern& rhs) { - return VisitPattern(lhs, rhs); - } - bool VisitPattern_(const PatternWildcardNode* lhs, const Pattern& other) final { return other.as(); } @@ -495,6 +504,10 @@ class AlphaEqualHandler: std::unordered_map equal_map_; }; +bool AlphaEqual(const Pattern& lhs, const Pattern& rhs) { + return AlphaEqualHandler(false).PatternEqual(lhs, rhs); +} + bool AlphaEqual(const Type& lhs, const Type& rhs) { return AlphaEqualHandler(false).TypeEqual(lhs, rhs); } diff --git a/src/relay/pass/match_exhaustion.cc b/src/relay/pass/match_exhaustion.cc new file mode 100644 index 000000000000..7dcd47a9f333 --- /dev/null +++ b/src/relay/pass/match_exhaustion.cc @@ -0,0 +1,230 @@ +/* + * Licensed to the Apache Software Foundation (ASF) under one + * or more contributor license agreements. See the NOTICE file + * distributed with this work for additional information + * regarding copyright ownership. The ASF licenses this file + * to you under the Apache License, Version 2.0 (the + * "License"); you may not use this file except in compliance + * with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, + * software distributed under the License is distributed on an + * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY + * KIND, either express or implied. See the License for the + * specific language governing permissions and limitations + * under the License. + */ + +/*! + * Copyright (c) 2019 by Contributors + * \file match_exhaustion.cc + * \brief Checking Relay match expression exhaustiveness. + * + * This file implements a function that checks whether a match + * expression is exhaustive, that is, whether a given match clause + * matches every possible case. This is important for ensuring + * code correctness, since hitting an unmatched case results in a + * dynamic error unless exhaustiveness is checked in advance. + */ +#include "match_exhaustion.h" +#include +#include +#include +#include +#include +#include +#include + +namespace tvm { +namespace relay { + +class CandidateChecker : public PatternFunctor { + public: + explicit CandidateChecker() {} + + bool Check(const Pattern& pat, const Pattern& candidate) { + return this->VisitPattern(pat, candidate); + } + + // for a constructor pattern, we must ensure that the candidate is + // a ConstructorPattern, that it has the same constructor, and + // that its fields match the subpatterns. + bool VisitPattern_(const PatternConstructorNode* op, const Pattern& cand) override { + auto* ctor_cand = cand.as(); + if (ctor_cand == nullptr) { + return false; + } + + // check that constructors match + if (!op->constructor.same_as(ctor_cand->constructor)) { + return false; + } + + // now check that subpatterns match + for (size_t i = 0; i < op->patterns.size(); i++) { + if (!this->Check(op->patterns[i], ctor_cand->patterns[i])) { + return false; + } + } + return true; + } + + // wildcard and var patterns always come up true + bool VisitPattern_(const PatternWildcardNode*, const Pattern&) override { + return true; + } + + bool VisitPattern_(const PatternVarNode*, const Pattern&) override { + return true; + } +}; + +std::deque> CartesianProduct(std::deque>* fields) { + CHECK(!fields->empty()); + Array field_vals = fields->back(); + fields->pop_back(); + std::deque> ret; + + // base case: this is the last field left + if (fields->empty()) { + for (auto val : field_vals) { + ret.push_back(Array{val}); + } + return ret; + } + + // if we have more fields left, get the sub-candidates by getting + // their cartesian product and appending the elements here onto those + std::deque> candidates = CartesianProduct(fields); + for (auto val : field_vals) { + for (auto candidate : candidates) { + // make a copy because we will mutate + Array new_candidate = Array(candidate); + new_candidate.push_back(val); + ret.push_back(candidate); + } + } + return ret; +} + +Array ExpandWildcards(const Pattern& cand, + const GlobalTypeVar& gtv, + const Module& mod) { + auto ctor_cand = cand.as(); + + // for a wildcard node, create constructor nodes with wildcards + // for all args + if (!ctor_cand) { + TypeData td = mod->LookupDef(gtv); + // for each constructor add a candidate + Array ret; + for (auto constructor : td->constructors) { + Array args; + for (auto inp : constructor->inputs) { + args.push_back(PatternWildcardNode::make()); + } + ret.push_back(PatternConstructorNode::make(constructor, args)); + } + return ret; + } + + // for constructors, we will expand the wildcards in any field + // that is an ADT + std::deque> values_by_field; + for (size_t i = 0; i < ctor_cand->constructor->inputs.size(); i++) { + auto type_call = ctor_cand->constructor->inputs[i].as(); + // for non-ADT fields, we can only have a wildcard for the value + if (!type_call) { + values_by_field.push_back(Array{PatternWildcardNode::make()}); + } + // otherwise, recursively expand + auto nested_gtv = Downcast(type_call->func); + values_by_field.push_back(ExpandWildcards(ctor_cand->patterns[i], nested_gtv, mod)); + } + + // generate new candidates using a cartesian product + auto all_subfields = CartesianProduct(&values_by_field); + Array ret; + for (auto subfields : all_subfields) { + ret.push_back(PatternConstructorNode::make(ctor_cand->constructor, subfields)); + } + return ret; +} + +/*! + * \brief Tests whether all match expressions in the given program + * are exhaustive. + * \return Returns a list of cases that are not handled by the match + * expression. + */ +Array CheckMatchExhaustion(const Match& match, const Module& mod) { + // algorithm: + // candidates = { Wildcard } + // while candidates not empty { + // cand = candidates.pop() + // for clause in clauses { + // if clause matches candidate: continue + // } + // candidates += expand_possible_wildcards(cand) + // if no new candidates produced: + // return cand + // } + // return null + std::stack candidates; + candidates.push(PatternWildcardNode::make()); + CandidateChecker checker; + + Array failures; + + while (!candidates.empty()) { + Pattern cand = candidates.top(); + candidates.pop(); + GlobalTypeVar gtv = GlobalTypeVar(nullptr); + for (auto clause : match->clauses) { + // if the check succeeds, then this candidate can be eliminated + if (checker.Check(clause->lhs, cand)) { + continue; + } else { + // only a constructor pattern can fail so this will give + // us a global type var to use + auto ctor_pat = Downcast(clause->lhs); + gtv = ctor_pat->constructor->belong_to; + } + } + + // no pattern matched so attempt to generate new candidates + if (!gtv.defined()) { + // must be a weird case like zero clauses + failures.push_back(cand); + continue; + } + + auto new_candidates = ExpandWildcards(cand, gtv, mod); + // if we cannot expand wildcards, we are left with only the same + // candidate, thus we fail + if (new_candidates.size() == 1 && AlphaEqual(new_candidates[0], cand)) { + failures.push_back(cand); + continue; + } + + // otherwise add new candidates (discard old one) and continue + for (auto candidate : new_candidates) { + candidates.push(candidate); + } + } + + // the pattern is exhaustive + return failures; +} + +TVM_REGISTER_API("relay._ir_pass.infer_type") +.set_body_typed< + Array(const Match&, + const Module&)>([](const Match& match, + const Module& mod_ref) { + return CheckMatchExhaustion(match, mod_ref); + }); +} // namespace relay +} // namespace tvm diff --git a/src/relay/pass/match_exhaustion.h b/src/relay/pass/match_exhaustion.h new file mode 100644 index 000000000000..26bbeceade65 --- /dev/null +++ b/src/relay/pass/match_exhaustion.h @@ -0,0 +1,47 @@ +/* + * Licensed to the Apache Software Foundation (ASF) under one + * or more contributor license agreements. See the NOTICE file + * distributed with this work for additional information + * regarding copyright ownership. The ASF licenses this file + * to you under the Apache License, Version 2.0 (the + * "License"); you may not use this file except in compliance + * with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, + * software distributed under the License is distributed on an + * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY + * KIND, either express or implied. See the License for the + * specific language governing permissions and limitations + * under the License. + */ + +/*! + * Copyright (c) 2018 by Contributors + * \file tvm/relay/pass/match_exhaustion.h + * \brief Header of definitions for match exhaustion. + */ + +#ifndef TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ +#define TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ + +#include +#include +#include +#include + +namespace tvm { +namespace relay { + +/*! + * \brief Tests whether all match expressions in the given program + * are exhaustive. + * \return Returns a list of cases that are not handled by the match + * expression. + */ +Array CheckMatchExhaustion(const Match& match, const Module& mod); + +} // namespace relay +} // namespace tvm +#endif // TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ From d3b7739d2af4de5c09bd6132bf2eab6bc8122861 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 16 May 2019 14:04:27 -0700 Subject: [PATCH 2/8] Matches are a trichotomy --- src/relay/ir/alpha_equal.cc | 21 +----- src/relay/pass/match_exhaustion.cc | 114 +++++++++++++++-------------- 2 files changed, 64 insertions(+), 71 deletions(-) diff --git a/src/relay/ir/alpha_equal.cc b/src/relay/ir/alpha_equal.cc index f7a5646a81ec..81017d4fddfa 100644 --- a/src/relay/ir/alpha_equal.cc +++ b/src/relay/ir/alpha_equal.cc @@ -60,10 +60,6 @@ class AlphaEqualHandler: if (!rhs->derived_from()) return false; return ExprEqual(Downcast(lhs), Downcast(rhs)); } - if (lhs->derived_from()) { - if (!rhs->derived_from()) return false; - return PatternEqual(Downcast(lhs), Downcast(rhs)); - } return AttrEqual(lhs, rhs); } @@ -114,15 +110,6 @@ class AlphaEqualHandler: } } - /*! - * Check equality of two patterns. - */ - bool PatternEqual(const Pattern& lhs, const Pattern& rhs) { - if (lhs.same_as(rhs)) return true; - if (!lhs.defined() || !rhs.defined()) return false; - return VisitPattern(lhs, rhs); - } - protected: /*! * \brief Check if data type equals each other. @@ -453,6 +440,10 @@ class AlphaEqualHandler: return PatternEqual(lhs->lhs, rhs->lhs) && ExprEqual(lhs->rhs, rhs->rhs); } + bool PatternEqual(const Pattern& lhs, const Pattern& rhs) { + return VisitPattern(lhs, rhs); + } + bool VisitPattern_(const PatternWildcardNode* lhs, const Pattern& other) final { return other.as(); } @@ -504,10 +495,6 @@ class AlphaEqualHandler: std::unordered_map equal_map_; }; -bool AlphaEqual(const Pattern& lhs, const Pattern& rhs) { - return AlphaEqualHandler(false).PatternEqual(lhs, rhs); -} - bool AlphaEqual(const Type& lhs, const Type& rhs) { return AlphaEqualHandler(false).TypeEqual(lhs, rhs); } diff --git a/src/relay/pass/match_exhaustion.cc b/src/relay/pass/match_exhaustion.cc index 7dcd47a9f333..4bc030547a5b 100644 --- a/src/relay/pass/match_exhaustion.cc +++ b/src/relay/pass/match_exhaustion.cc @@ -40,47 +40,57 @@ namespace tvm { namespace relay { -class CandidateChecker : public PatternFunctor { +/*! \brief Possible pattern match results */ +enum MatchResult : int { + kMatch = 0, // pattern matches + kClash = 1, // pattern conflicts + kUnspecified = 2, // ambiguous: candidate needs more constructors specified +}; + +class CandidateChecker : public PatternFunctor { public: explicit CandidateChecker() {} - bool Check(const Pattern& pat, const Pattern& candidate) { + MatchResult Check(const Pattern& pat, const Pattern& candidate) { return this->VisitPattern(pat, candidate); } // for a constructor pattern, we must ensure that the candidate is // a ConstructorPattern, that it has the same constructor, and // that its fields match the subpatterns. - bool VisitPattern_(const PatternConstructorNode* op, const Pattern& cand) override { + MatchResult VisitPattern_(const PatternConstructorNode* op, const Pattern& cand) override { auto* ctor_cand = cand.as(); + // attempting to match non-constructor to constructor pattern: need to specify if (ctor_cand == nullptr) { - return false; + return MatchResult::kUnspecified; } // check that constructors match if (!op->constructor.same_as(ctor_cand->constructor)) { - return false; + return MatchResult::kClash; } // now check that subpatterns match for (size_t i = 0; i < op->patterns.size(); i++) { - if (!this->Check(op->patterns[i], ctor_cand->patterns[i])) { - return false; + MatchResult submatch = this->Check(op->patterns[i], ctor_cand->patterns[i]); + if (submatch != MatchResult::kMatch) { + return submatch; } } - return true; + return MatchResult::kMatch; } - // wildcard and var patterns always come up true - bool VisitPattern_(const PatternWildcardNode*, const Pattern&) override { - return true; + // wildcard and var patterns always match + MatchResult VisitPattern_(const PatternWildcardNode*, const Pattern&) override { + return MatchResult::kMatch; } - bool VisitPattern_(const PatternVarNode*, const Pattern&) override { - return true; + MatchResult VisitPattern_(const PatternVarNode*, const Pattern&) override { + return MatchResult::kMatch; } }; +// Returns list of arrays corresponding to Cartesian product of input list std::deque> CartesianProduct(std::deque>* fields) { CHECK(!fields->empty()); Array field_vals = fields->back(); @@ -109,9 +119,9 @@ std::deque> CartesianProduct(std::deque>* fields) return ret; } -Array ExpandWildcards(const Pattern& cand, - const GlobalTypeVar& gtv, - const Module& mod) { +// Expands all wildcards in the candidate pattern once, using the global type var +// to decide which constructors to insert. Returns a list of all possible expansions. +Array ExpandWildcards(const Pattern& cand, const GlobalTypeVar& gtv, const Module& mod) { auto ctor_cand = cand.as(); // for a wildcard node, create constructor nodes with wildcards @@ -160,18 +170,20 @@ Array ExpandWildcards(const Pattern& cand, * expression. */ Array CheckMatchExhaustion(const Match& match, const Module& mod) { - // algorithm: - // candidates = { Wildcard } - // while candidates not empty { - // cand = candidates.pop() - // for clause in clauses { - // if clause matches candidate: continue - // } - // candidates += expand_possible_wildcards(cand) - // if no new candidates produced: - // return cand - // } - // return null + /* algorithm: + * candidates = { Wildcard } + * while candidates not empty { + * cand = candidates.pop() + * for clause in clauses { + * if clause matches candidate: next candidate + * if candidate is not specific enough: + * candidates += expand_possible_wildcards(cand) + * continue + * } + * failed_candidates += { cand } + * } + * return failed_candidates + */ std::stack candidates; candidates.push(PatternWildcardNode::make()); CandidateChecker checker; @@ -182,48 +194,42 @@ Array CheckMatchExhaustion(const Match& match, const Module& mod) { Pattern cand = candidates.top(); candidates.pop(); GlobalTypeVar gtv = GlobalTypeVar(nullptr); + bool failure = true; for (auto clause : match->clauses) { // if the check succeeds, then this candidate can be eliminated - if (checker.Check(clause->lhs, cand)) { + MatchResult check = checker.Check(clause->lhs, cand); + if (check == MatchResult::kClash) { continue; - } else { - // only a constructor pattern can fail so this will give + } + + failure = false; + + // match was not specific enough: need to expand wildcards + if (check == MatchResult::kUnspecified) { + // only a constructor pattern can fail to match so this will give // us a global type var to use auto ctor_pat = Downcast(clause->lhs); gtv = ctor_pat->constructor->belong_to; + auto new_candidates = ExpandWildcards(cand, gtv, mod); + for (auto candidate : new_candidates) { + candidates.push(candidate); + } } + break; } - // no pattern matched so attempt to generate new candidates - if (!gtv.defined()) { - // must be a weird case like zero clauses + if (failure) { failures.push_back(cand); - continue; - } - - auto new_candidates = ExpandWildcards(cand, gtv, mod); - // if we cannot expand wildcards, we are left with only the same - // candidate, thus we fail - if (new_candidates.size() == 1 && AlphaEqual(new_candidates[0], cand)) { - failures.push_back(cand); - continue; - } - - // otherwise add new candidates (discard old one) and continue - for (auto candidate : new_candidates) { - candidates.push(candidate); } } - // the pattern is exhaustive return failures; } -TVM_REGISTER_API("relay._ir_pass.infer_type") -.set_body_typed< - Array(const Match&, - const Module&)>([](const Match& match, - const Module& mod_ref) { +TVM_REGISTER_API("relay._ir_pass.check_match_exhaustion") +.set_body_typed(const Match&, const Module&)> +([] + (const Match& match, const Module& mod_ref) { return CheckMatchExhaustion(match, mod_ref); }); } // namespace relay From e112492fbb1a80261a5ae081edf258905759082f Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 16 May 2019 16:41:40 -0700 Subject: [PATCH 3/8] Add tests for case matching, add match completeness check to type checking, fix prelude functions and broken tests --- include/tvm/relay/pass.h | 13 +- python/tvm/relay/ir_pass.py | 18 ++ python/tvm/relay/prelude.py | 29 ++- src/relay/pass/match_exhaustion.cc | 76 +++--- src/relay/pass/match_exhaustion.h | 47 ---- src/relay/pass/type_infer.cc | 10 + tests/python/relay/test_adt.py | 18 +- tests/python/relay/test_pass_partial_eval.py | 21 +- .../python/relay/test_pass_unmatched_cases.py | 229 ++++++++++++++++++ 9 files changed, 361 insertions(+), 100 deletions(-) delete mode 100644 src/relay/pass/match_exhaustion.h create mode 100644 tests/python/relay/test_pass_unmatched_cases.py diff --git a/include/tvm/relay/pass.h b/include/tvm/relay/pass.h index 896687ba0524..4dcf2e6f76da 100644 --- a/include/tvm/relay/pass.h +++ b/include/tvm/relay/pass.h @@ -409,8 +409,19 @@ TVM_DLL Expr ToANormalForm(const Expr& e, const Module& mod); TVM_DLL Expr ToGraphNormalForm(const Expr& e); /*! - * \brief Aggressive constant propagation/constant folding/inlining. + * \brief Finds cases that the given match expression does not catch, if any. + * + * \param match the match expression to test * + * \param mod The module used for accessing global type var definitions, can be None. + * + * \return Returns a list of cases (as patterns) that are not handled by the match + * expression. + */ +TVM_DLL Array UnmatchedCases(const Match& match, const Module& mod); + +/*! + * \brief Aggressive constant propagation/constant folding/inlining. * It will do as much computation in compile time as possible. * It has two benefit: remove runtime overhead, and allow more optimization (typically fusion). * As a side effect, code size will explode. diff --git a/python/tvm/relay/ir_pass.py b/python/tvm/relay/ir_pass.py index ea34c6b1958b..8f1ceded76dd 100644 --- a/python/tvm/relay/ir_pass.py +++ b/python/tvm/relay/ir_pass.py @@ -652,3 +652,21 @@ def partial_evaluate(expr): The output expression. """ return _ir_pass.partial_evaluate(expr) + +def unmatched_cases(match, mod=None): + """ + Finds cases that the match expression does not catch, if any. + + Parameters + ---------- + match : tvm.relay.Match + The match expression + mod : Optional[tvm.relay.Module] + The module (defaults to an empty module) + + Returns + ------- + missing_patterns : [tvm.relay.Pattern] + Patterns that the match expression does not catch. + """ + return _ir_pass.unmatched_cases(match, mod) diff --git a/python/tvm/relay/prelude.py b/python/tvm/relay/prelude.py index 92647e5b14b4..6f2936bf2f8e 100644 --- a/python/tvm/relay/prelude.py +++ b/python/tvm/relay/prelude.py @@ -83,7 +83,8 @@ def define_list_nth(self): def define_list_update(self): - """Defines a function to update the nth element of a list and return the updated list. + """Defines a function to update the nth element of a list if it exists and return + the updated list (does nothing if the list has fewer than n elements). update(l, i, v) : list[a] -> Tensor[(), int32] -> a -> list[a] """ @@ -172,7 +173,7 @@ def define_list_foldr(self): def define_list_foldr1(self): """Defines a right-way fold over a nonempty list. - foldr1(f, l) : fn(fn(a, a) -> a, list[a]) -> a + foldr1(f, l) : fn(fn(a, a) -> a, list[a]) -> optional[a] foldr1(f, cons(a1, cons(a2, cons(..., cons(an, nil))))) evalutes to f(a1, f(a2, f(..., f(an-1, an)))...) @@ -184,13 +185,21 @@ def define_list_foldr1(self): x = Var("x") y = Var("y") z = Var("z") + r = Var("r") one_case = Clause(PatternConstructor(self.cons, - [PatternVar(x), PatternConstructor(self.nil)]), x) + [PatternVar(x), PatternConstructor(self.nil)]), + self.some(x)) cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), - f(y, self.foldr1(f, z))) + Match(self.foldr1(f, z), [ + Clause(PatternConstructor(self.some, [PatternVar(r)]), + self.some(f(y, r))), + # should never happen + Clause(PatternConstructor(self.none, []), self.none()) + ])) + empty_case = Clause(PatternConstructor(self.nil, []), self.none()) self.mod[self.foldr1] = Function([f, av], - Match(av, [one_case, cons_case]), a, [a]) - + Match(av, [one_case, cons_case, empty_case]), + self.optional(a), [a]) def define_list_concat(self): """Defines a function that concatenates two lists. @@ -327,7 +336,6 @@ def define_list_map_accuml(self): TupleType([a, self.l(c)]), [a, b, c]) - def define_optional_adt(self): """Defines an optional ADT, which can either contain some other type or nothing at all.""" @@ -504,12 +512,9 @@ def define_iterate(self): def __init__(self, mod): self.mod = mod self.define_list_adt() - self.define_list_hd() - self.define_list_tl() self.define_list_map() self.define_list_foldl() self.define_list_foldr() - self.define_list_foldr1() self.define_list_concat() self.define_list_filter() self.define_list_zip() @@ -518,6 +523,10 @@ def __init__(self, mod): self.define_list_map_accuml() self.define_optional_adt() + self.define_list_hd() + self.define_list_tl() + self.define_list_foldr1() + self.define_list_unfoldr() self.define_list_unfoldl() diff --git a/src/relay/pass/match_exhaustion.cc b/src/relay/pass/match_exhaustion.cc index 4bc030547a5b..0f05280ea8cc 100644 --- a/src/relay/pass/match_exhaustion.cc +++ b/src/relay/pass/match_exhaustion.cc @@ -28,13 +28,11 @@ * code correctness, since hitting an unmatched case results in a * dynamic error unless exhaustiveness is checked in advance. */ -#include "match_exhaustion.h" #include #include #include #include #include -#include #include namespace tvm { @@ -71,6 +69,7 @@ class CandidateChecker : public PatternFunctorpatterns.size() == ctor_cand->patterns.size()); for (size_t i = 0; i < op->patterns.size(); i++) { MatchResult submatch = this->Check(op->patterns[i], ctor_cand->patterns[i]); if (submatch != MatchResult::kMatch) { @@ -91,14 +90,13 @@ class CandidateChecker : public PatternFunctor> CartesianProduct(std::deque>* fields) { - CHECK(!fields->empty()); - Array field_vals = fields->back(); - fields->pop_back(); - std::deque> ret; +Array> CartesianProduct(Array> fields) { + CHECK_NE(fields.size(), 0); + Array field_vals = fields[fields.size() - 1]; + Array> ret; // base case: this is the last field left - if (fields->empty()) { + if (fields.size() == 1) { for (auto val : field_vals) { ret.push_back(Array{val}); } @@ -107,12 +105,14 @@ std::deque> CartesianProduct(std::deque>* fields) // if we have more fields left, get the sub-candidates by getting // their cartesian product and appending the elements here onto those - std::deque> candidates = CartesianProduct(fields); + Array> remaining_fields; + for (size_t i = 0; i < fields.size() - 1; i++) { + remaining_fields.push_back(fields[i]); + } + Array> candidates = CartesianProduct(remaining_fields); for (auto val : field_vals) { for (auto candidate : candidates) { - // make a copy because we will mutate - Array new_candidate = Array(candidate); - new_candidate.push_back(val); + candidate.push_back(val); ret.push_back(candidate); } } @@ -121,11 +121,11 @@ std::deque> CartesianProduct(std::deque>* fields) // Expands all wildcards in the candidate pattern once, using the global type var // to decide which constructors to insert. Returns a list of all possible expansions. -Array ExpandWildcards(const Pattern& cand, const GlobalTypeVar& gtv, const Module& mod) { +Array ExpandWildcards(const Pattern& clause_pat, const Pattern& cand, + const GlobalTypeVar& gtv, const Module& mod) { auto ctor_cand = cand.as(); - // for a wildcard node, create constructor nodes with wildcards - // for all args + // for a wildcard node, create constructor nodes with wildcards for all args if (!ctor_cand) { TypeData td = mod->LookupDef(gtv); // for each constructor add a candidate @@ -142,20 +142,25 @@ Array ExpandWildcards(const Pattern& cand, const GlobalTypeVar& gtv, co // for constructors, we will expand the wildcards in any field // that is an ADT - std::deque> values_by_field; + PatternConstructor clause_ctor = Downcast(clause_pat); + Array> values_by_field; for (size_t i = 0; i < ctor_cand->constructor->inputs.size(); i++) { - auto type_call = ctor_cand->constructor->inputs[i].as(); + auto* subpattern = clause_ctor->patterns[i].as(); // for non-ADT fields, we can only have a wildcard for the value - if (!type_call) { - values_by_field.push_back(Array{PatternWildcardNode::make()}); + if (!subpattern) { + values_by_field.push_back({PatternWildcardNode::make()}); + continue; } + // otherwise, recursively expand - auto nested_gtv = Downcast(type_call->func); - values_by_field.push_back(ExpandWildcards(ctor_cand->patterns[i], nested_gtv, mod)); + auto nested_gtv = Downcast(subpattern->constructor->belong_to); + values_by_field.push_back(ExpandWildcards(GetRef(subpattern), + ctor_cand->patterns[i], + nested_gtv, mod)); } // generate new candidates using a cartesian product - auto all_subfields = CartesianProduct(&values_by_field); + auto all_subfields = CartesianProduct(values_by_field); Array ret; for (auto subfields : all_subfields) { ret.push_back(PatternConstructorNode::make(ctor_cand->constructor, subfields)); @@ -164,21 +169,21 @@ Array ExpandWildcards(const Pattern& cand, const GlobalTypeVar& gtv, co } /*! - * \brief Tests whether all match expressions in the given program - * are exhaustive. + * \brief Finds cases that the match expression does not catch, if any. * \return Returns a list of cases that are not handled by the match * expression. */ -Array CheckMatchExhaustion(const Match& match, const Module& mod) { +Array UnmatchedCases(const Match& match, const Module& mod) { /* algorithm: * candidates = { Wildcard } * while candidates not empty { * cand = candidates.pop() * for clause in clauses { + * if clause fails: next clause * if clause matches candidate: next candidate * if candidate is not specific enough: * candidates += expand_possible_wildcards(cand) - * continue + * next candidate * } * failed_candidates += { cand } * } @@ -210,7 +215,7 @@ Array CheckMatchExhaustion(const Match& match, const Module& mod) { // us a global type var to use auto ctor_pat = Downcast(clause->lhs); gtv = ctor_pat->constructor->belong_to; - auto new_candidates = ExpandWildcards(cand, gtv, mod); + auto new_candidates = ExpandWildcards(clause->lhs, cand, gtv, mod); for (auto candidate : new_candidates) { candidates.push(candidate); } @@ -226,11 +231,16 @@ Array CheckMatchExhaustion(const Match& match, const Module& mod) { return failures; } -TVM_REGISTER_API("relay._ir_pass.check_match_exhaustion") -.set_body_typed(const Match&, const Module&)> -([] - (const Match& match, const Module& mod_ref) { - return CheckMatchExhaustion(match, mod_ref); - }); +// expose for testing only +TVM_REGISTER_API("relay._ir_pass.unmatched_cases") +.set_body_typed(const Match&, + const Module&)>([](const Match& match, + const Module& mod_ref) { + Module call_mod = mod_ref; + if (!call_mod.defined()) { + call_mod = ModuleNode::make({}, {}); + } + return UnmatchedCases(match, call_mod); + }); } // namespace relay } // namespace tvm diff --git a/src/relay/pass/match_exhaustion.h b/src/relay/pass/match_exhaustion.h deleted file mode 100644 index 26bbeceade65..000000000000 --- a/src/relay/pass/match_exhaustion.h +++ /dev/null @@ -1,47 +0,0 @@ -/* - * Licensed to the Apache Software Foundation (ASF) under one - * or more contributor license agreements. See the NOTICE file - * distributed with this work for additional information - * regarding copyright ownership. The ASF licenses this file - * to you under the Apache License, Version 2.0 (the - * "License"); you may not use this file except in compliance - * with the License. You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, - * software distributed under the License is distributed on an - * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY - * KIND, either express or implied. See the License for the - * specific language governing permissions and limitations - * under the License. - */ - -/*! - * Copyright (c) 2018 by Contributors - * \file tvm/relay/pass/match_exhaustion.h - * \brief Header of definitions for match exhaustion. - */ - -#ifndef TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ -#define TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ - -#include -#include -#include -#include - -namespace tvm { -namespace relay { - -/*! - * \brief Tests whether all match expressions in the given program - * are exhaustive. - * \return Returns a list of cases that are not handled by the match - * expression. - */ -Array CheckMatchExhaustion(const Match& match, const Module& mod); - -} // namespace relay -} // namespace tvm -#endif // TVM_RELAY_PASS_MATCH_EXHAUSTION_H_ diff --git a/src/relay/pass/type_infer.cc b/src/relay/pass/type_infer.cc index 482cef3b2c2d..94179ad7c505 100644 --- a/src/relay/pass/type_infer.cc +++ b/src/relay/pass/type_infer.cc @@ -292,6 +292,16 @@ class TypeInferencer : private ExprFunctor, GetType(c->rhs), op->span); } + + // check completness + Match match = GetRef(op); + Array unmatched_cases = UnmatchedCases(match, this->mod_); + if (unmatched_cases.size() != 0) { + this->ReportFatalError(match, + RELAY_ERROR("Match clause does not handle the following cases: " + << unmatched_cases)); + } + return rtype; } diff --git a/tests/python/relay/test_adt.py b/tests/python/relay/test_adt.py index 77f4ab1f16a0..5f6016475ce2 100644 --- a/tests/python/relay/test_adt.py +++ b/tests/python/relay/test_adt.py @@ -99,6 +99,12 @@ def to_list(l): break return ret +def get_optional(opt): + assert isinstance(opt, ConstructorValue) + assert opt.constructor.name_hint == 'some' + assert len(opt.fields) == 1 + return opt.fields[0] + def tree_to_dict(t): assert isinstance(t, ConstructorValue) ret = {} @@ -150,8 +156,12 @@ def test_hd_tl(): got = [] for i in range(len(expected)): - got.append(count(intrp.evaluate(hd(l)))) - l = tl(l) + got.append(count(get_optional(intrp.evaluate(hd(l))))) + t = relay.Var('t') + l = relay.Match(tl(l), [ + relay.Clause(relay.PatternConstructor(p.some, [relay.PatternVar(t)]), t), + relay.Clause(relay.PatternConstructor(p.none, []), p.nil()) + ]) assert got == expected @@ -248,7 +258,7 @@ def test_foldr(): def test_foldr1(): a = relay.TypeVar("a") lhs = mod[p.foldr1].checked_type - rhs = relay.FuncType([relay.FuncType([a, a], a), l(a)], a, [a]) + rhs = relay.FuncType([relay.FuncType([a, a], a), l(a)], p.optional(a), [a]) assert lhs == rhs x = relay.Var("x") @@ -259,7 +269,7 @@ def test_foldr1(): cons(make_nat_expr(2), cons(make_nat_expr(3), nil()))))) - assert count(res) == 6 + assert count(get_optional(res)) == 6 def test_sum(): diff --git a/tests/python/relay/test_pass_partial_eval.py b/tests/python/relay/test_pass_partial_eval.py index 78fa63b5231d..780977646ed2 100644 --- a/tests/python/relay/test_pass_partial_eval.py +++ b/tests/python/relay/test_pass_partial_eval.py @@ -138,16 +138,27 @@ def hd_impl(): cons_case = relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternVar(y), relay.PatternVar(z)]), - y) - return relay.Function([x], relay.Match(x, [cons_case]), a, [a]) + p.some(y)) + nil_case = relay.Clause(relay.PatternConstructor(p.nil, []), p.none()) + return relay.Function([x], relay.Match(x, [cons_case, nil_case]), + p.optional(a), [a]) t = relay.TypeVar("t") x = relay.Var("x", t) + y = relay.Var("y", t) + s = relay.Var("s") hd = relay.Var("hd") - body = relay.Let(hd, hd_impl(), hd(p.cons(x, p.nil()))) - f = relay.Function([x], body, None, [t]) + body = relay.Let( + hd, hd_impl(), + relay.Match( + hd(p.cons(x, p.nil())), + [ + relay.Clause(relay.PatternConstructor(p.some, [relay.PatternVar(s)]), s), + relay.Clause(relay.PatternWildcard(), y) + ])) + f = relay.Function([x, y], body, None, [t]) f = infer_type(f, mod=mod) res = dcpe(f) - assert alpha_equal(res, relay.Function([x], x, t, [t])) + assert alpha_equal(res, relay.Function([x, y], x, t, [t])) if __name__ == '__main__': diff --git a/tests/python/relay/test_pass_unmatched_cases.py b/tests/python/relay/test_pass_unmatched_cases.py new file mode 100644 index 000000000000..eb26f08e2305 --- /dev/null +++ b/tests/python/relay/test_pass_unmatched_cases.py @@ -0,0 +1,229 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +import tvm +from tvm import relay +from tvm.relay.prelude import Prelude +from tvm.relay.ir_pass import unmatched_cases + +def test_empty_match_block(): + # empty match block will not match anything, so it should return a wildcard pattern + v = relay.Var('v') + match = relay.Match(v, []) + + unmatched = unmatched_cases(match) + assert len(unmatched) == 1 + assert isinstance(unmatched[0], relay.PatternWildcard) + + +def test_trivial_matches(): + # a match clause with a wildcard will match anything + v = relay.Var('v') + match = relay.Match(v, [ + relay.Clause(relay.PatternWildcard(), v) + ]) + assert len(unmatched_cases(match)) == 0 + + # same with a pattern var + w = relay.Var('w') + match = relay.Match(v, [ + relay.Clause(relay.PatternVar(w), w) + ]) + assert len(unmatched_cases(match)) == 0 + + +def test_single_constructor_adt(): + mod = relay.Module() + box = relay.GlobalTypeVar('box') + a = relay.TypeVar('a') + box_ctor = relay.Constructor('box', [a], box) + box_data = relay.TypeData(box, [a], [box_ctor]) + mod[box] = box_data + + v = relay.Var('v') + match = relay.Match(v, [ + relay.Clause(relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), v) + ]) + + # with one constructor, having one pattern constructor case is exhaustive + assert len(unmatched_cases(match, mod)) == 0 + + # this will be so if we nest the constructors too + nested_pattern = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + box_ctor, + [relay.PatternConstructor(box_ctor, + [relay.PatternConstructor( + box_ctor, + [relay.PatternWildcard()])])]), v) + ]) + assert len(unmatched_cases(nested_pattern, mod)) == 0 + + +def test_too_specific_match(): + mod = relay.Module() + p = Prelude(mod) + + v = relay.Var('v') + match = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternWildcard()])]), v) + ]) + + unmatched = unmatched_cases(match, mod) + + # will not match nil or a list of length 1 + nil_found = False + single_length_found = False + assert len(unmatched) == 2 + for case in unmatched: + assert isinstance(case, relay.PatternConstructor) + if case.constructor == p.nil: + nil_found = True + if case.constructor == p.cons: + assert isinstance(case.patterns[1], relay.PatternConstructor) + assert case.patterns[1].constructor == p.nil + single_length_found = True + assert nil_found and single_length_found + + # if we add a wildcard, this should work + new_match = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternWildcard()])]), v), + relay.Clause(relay.PatternWildcard(), v) + ]) + assert len(unmatched_cases(new_match, mod)) == 0 + + +def test_multiple_constructor_clauses(): + mod = relay.Module() + p = Prelude(mod) + + v = relay.Var('v') + match = relay.Match(v, [ + # list of length exactly 1 + relay.Clause( + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.nil, [])]), v), + # list of length exactly 2 + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.nil, []) + ])]), v), + # empty list + relay.Clause( + relay.PatternConstructor(p.nil, []), v), + # list of length 2 or more + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternWildcard()])]), v) + ]) + assert len(unmatched_cases(match, mod)) == 0 + + +def test_mixed_adt_constructors(): + mod = relay.Module() + box = relay.GlobalTypeVar('box') + a = relay.TypeVar('a') + box_ctor = relay.Constructor('box', [a], box) + box_data = relay.TypeData(box, [a], [box_ctor]) + mod[box] = box_data + + p = Prelude(mod) + + v = relay.Var('v') + box_of_lists_inc = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + box_ctor, + [relay.PatternConstructor(p.cons, [ + relay.PatternWildcard(), relay.PatternWildcard()])]), v) + ]) + + # will fail to match a box containing an empty list + unmatched = unmatched_cases(box_of_lists_inc, mod) + assert len(unmatched) == 1 + assert isinstance(unmatched[0], relay.PatternConstructor) + assert unmatched[0].constructor == box_ctor + assert len(unmatched[0].patterns) == 1 and unmatched[0].patterns[0].constructor == p.nil + + box_of_lists_comp = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + box_ctor, [relay.PatternConstructor(p.nil, [])]), v), + relay.Clause( + relay.PatternConstructor( + box_ctor, [relay.PatternConstructor(p.cons, [ + relay.PatternWildcard(), relay.PatternWildcard()])]), v) + ]) + assert len(unmatched_cases(box_of_lists_comp, mod)) == 0 + + list_of_boxes_inc = relay.Match(v, [ + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternWildcard()]), v) + ]) + + # fails to match empty list of boxes + unmatched = unmatched_cases(list_of_boxes_inc, mod) + assert len(unmatched) == 1 + assert isinstance(unmatched[0], relay.PatternConstructor) + assert unmatched[0].constructor == p.nil + + list_of_boxes_comp = relay.Match(v, [ + # exactly one box + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.nil, [])]), v), + # exactly two boxes + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.cons, [ + relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.nil, []) + ])]), v), + # exactly three boxes + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.cons, [ + relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.cons, [ + relay.PatternConstructor(box_ctor, [relay.PatternWildcard()]), + relay.PatternConstructor(p.nil, []) + ])])]), v), + # one or more boxes + relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternWildcard()]), v), + # no boxes + relay.Clause(relay.PatternConstructor(p.nil, []), v) + ]) + assert len(unmatched_cases(list_of_boxes_comp, mod)) == 0 From a2f2fce595f0777fdaf3d69d2c088180a21c5ca8 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 16 May 2019 17:56:27 -0700 Subject: [PATCH 4/8] Make missing cases only a warning, not an error for now --- python/tvm/relay/prelude.py | 70 ++++++++++++++------ src/relay/pass/type_infer.cc | 5 +- tests/python/relay/test_adt.py | 18 ++--- tests/python/relay/test_pass_partial_eval.py | 21 ++---- 4 files changed, 62 insertions(+), 52 deletions(-) diff --git a/python/tvm/relay/prelude.py b/python/tvm/relay/prelude.py index 6f2936bf2f8e..0aef01ef4acf 100644 --- a/python/tvm/relay/prelude.py +++ b/python/tvm/relay/prelude.py @@ -35,6 +35,47 @@ def define_list_adt(self): self.cons = Constructor("cons", [a, self.l(a)], self.l) self.mod[self.l] = TypeData(self.l, [a], [self.nil, self.cons]) + def define_list_hd(self): + """Defines a function to get the head of a list. Assume the list has at least one + element. + + hd(l) : list[a] -> a + """ + self.hd = GlobalVar("hd") + a = TypeVar("a") + x = Var("x", self.l(a)) + y = Var("y") + z = Var("z") + cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), y) + self.mod[self.hd] = Function([x], Match(x, [cons_case]), a, [a]) + + def define_list_tl(self): + """Defines a function to get the tail of a list. + + tl(l) : list[a] -> list[a] + """ + self.tl = GlobalVar("tl") + a = TypeVar("a") + x = Var("x", self.l(a)) + y = Var("y") + z = Var("z") + cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), z) + self.mod[self.tl] = Function([x], Match(x, [cons_case]), self.l(a), [a]) + + def define_list_nth(self): + """Defines a function to get the nth element of a list. + + nth(l) : list[a] -> a + """ + self.nth = GlobalVar("nth") + a = TypeVar("a") + x = Var("x", self.l(a)) + n = Var("n", self.nat()) + + y = Var("y") + z_case = Clause(PatternConstructor(self.z), self.hd(x)) + s_case = Clause(PatternConstructor(self.s, [PatternVar(y)]), self.nth(self.tl(x), y)) + self.mod[self.nth] = Function([x, n], Match(n, [z_case, s_case]), a, [a]) def define_list_hd(self): """Defines a function to get the head of a list. Assume the list has at least one @@ -83,8 +124,7 @@ def define_list_nth(self): def define_list_update(self): - """Defines a function to update the nth element of a list if it exists and return - the updated list (does nothing if the list has fewer than n elements). + """Defines a function to update the nth element of a list and return the updated list. update(l, i, v) : list[a] -> Tensor[(), int32] -> a -> list[a] """ @@ -173,7 +213,7 @@ def define_list_foldr(self): def define_list_foldr1(self): """Defines a right-way fold over a nonempty list. - foldr1(f, l) : fn(fn(a, a) -> a, list[a]) -> optional[a] + foldr1(f, l) : fn(fn(a, a) -> a, list[a]) -> a foldr1(f, cons(a1, cons(a2, cons(..., cons(an, nil))))) evalutes to f(a1, f(a2, f(..., f(an-1, an)))...) @@ -185,21 +225,13 @@ def define_list_foldr1(self): x = Var("x") y = Var("y") z = Var("z") - r = Var("r") one_case = Clause(PatternConstructor(self.cons, - [PatternVar(x), PatternConstructor(self.nil)]), - self.some(x)) + [PatternVar(x), PatternConstructor(self.nil)]), x) cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), - Match(self.foldr1(f, z), [ - Clause(PatternConstructor(self.some, [PatternVar(r)]), - self.some(f(y, r))), - # should never happen - Clause(PatternConstructor(self.none, []), self.none()) - ])) - empty_case = Clause(PatternConstructor(self.nil, []), self.none()) + f(y, self.foldr1(f, z))) self.mod[self.foldr1] = Function([f, av], - Match(av, [one_case, cons_case, empty_case]), - self.optional(a), [a]) + Match(av, [one_case, cons_case]), a, [a]) + def define_list_concat(self): """Defines a function that concatenates two lists. @@ -336,6 +368,7 @@ def define_list_map_accuml(self): TupleType([a, self.l(c)]), [a, b, c]) + def define_optional_adt(self): """Defines an optional ADT, which can either contain some other type or nothing at all.""" @@ -512,9 +545,12 @@ def define_iterate(self): def __init__(self, mod): self.mod = mod self.define_list_adt() + self.define_list_hd() + self.define_list_tl() self.define_list_map() self.define_list_foldl() self.define_list_foldr() + self.define_list_foldr1() self.define_list_concat() self.define_list_filter() self.define_list_zip() @@ -523,10 +559,6 @@ def __init__(self, mod): self.define_list_map_accuml() self.define_optional_adt() - self.define_list_hd() - self.define_list_tl() - self.define_list_foldr1() - self.define_list_unfoldr() self.define_list_unfoldl() diff --git a/src/relay/pass/type_infer.cc b/src/relay/pass/type_infer.cc index 94179ad7c505..27904379ca6f 100644 --- a/src/relay/pass/type_infer.cc +++ b/src/relay/pass/type_infer.cc @@ -297,9 +297,8 @@ class TypeInferencer : private ExprFunctor, Match match = GetRef(op); Array unmatched_cases = UnmatchedCases(match, this->mod_); if (unmatched_cases.size() != 0) { - this->ReportFatalError(match, - RELAY_ERROR("Match clause does not handle the following cases: " - << unmatched_cases)); + LOG(WARNING) << "Match clause " << match << " does not handle the following cases: " + << unmatched_cases; } return rtype; diff --git a/tests/python/relay/test_adt.py b/tests/python/relay/test_adt.py index 5f6016475ce2..77f4ab1f16a0 100644 --- a/tests/python/relay/test_adt.py +++ b/tests/python/relay/test_adt.py @@ -99,12 +99,6 @@ def to_list(l): break return ret -def get_optional(opt): - assert isinstance(opt, ConstructorValue) - assert opt.constructor.name_hint == 'some' - assert len(opt.fields) == 1 - return opt.fields[0] - def tree_to_dict(t): assert isinstance(t, ConstructorValue) ret = {} @@ -156,12 +150,8 @@ def test_hd_tl(): got = [] for i in range(len(expected)): - got.append(count(get_optional(intrp.evaluate(hd(l))))) - t = relay.Var('t') - l = relay.Match(tl(l), [ - relay.Clause(relay.PatternConstructor(p.some, [relay.PatternVar(t)]), t), - relay.Clause(relay.PatternConstructor(p.none, []), p.nil()) - ]) + got.append(count(intrp.evaluate(hd(l)))) + l = tl(l) assert got == expected @@ -258,7 +248,7 @@ def test_foldr(): def test_foldr1(): a = relay.TypeVar("a") lhs = mod[p.foldr1].checked_type - rhs = relay.FuncType([relay.FuncType([a, a], a), l(a)], p.optional(a), [a]) + rhs = relay.FuncType([relay.FuncType([a, a], a), l(a)], a, [a]) assert lhs == rhs x = relay.Var("x") @@ -269,7 +259,7 @@ def test_foldr1(): cons(make_nat_expr(2), cons(make_nat_expr(3), nil()))))) - assert count(get_optional(res)) == 6 + assert count(res) == 6 def test_sum(): diff --git a/tests/python/relay/test_pass_partial_eval.py b/tests/python/relay/test_pass_partial_eval.py index 780977646ed2..78fa63b5231d 100644 --- a/tests/python/relay/test_pass_partial_eval.py +++ b/tests/python/relay/test_pass_partial_eval.py @@ -138,27 +138,16 @@ def hd_impl(): cons_case = relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternVar(y), relay.PatternVar(z)]), - p.some(y)) - nil_case = relay.Clause(relay.PatternConstructor(p.nil, []), p.none()) - return relay.Function([x], relay.Match(x, [cons_case, nil_case]), - p.optional(a), [a]) + y) + return relay.Function([x], relay.Match(x, [cons_case]), a, [a]) t = relay.TypeVar("t") x = relay.Var("x", t) - y = relay.Var("y", t) - s = relay.Var("s") hd = relay.Var("hd") - body = relay.Let( - hd, hd_impl(), - relay.Match( - hd(p.cons(x, p.nil())), - [ - relay.Clause(relay.PatternConstructor(p.some, [relay.PatternVar(s)]), s), - relay.Clause(relay.PatternWildcard(), y) - ])) - f = relay.Function([x, y], body, None, [t]) + body = relay.Let(hd, hd_impl(), hd(p.cons(x, p.nil()))) + f = relay.Function([x], body, None, [t]) f = infer_type(f, mod=mod) res = dcpe(f) - assert alpha_equal(res, relay.Function([x, y], x, t, [t])) + assert alpha_equal(res, relay.Function([x], x, t, [t])) if __name__ == '__main__': From 31902f6a4c2ea68933130f9cbabb18c0f9f4b73d Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 16 May 2019 18:14:08 -0700 Subject: [PATCH 5/8] Trim some poorly written logic --- src/relay/pass/match_exhaustion.cc | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/src/relay/pass/match_exhaustion.cc b/src/relay/pass/match_exhaustion.cc index 0f05280ea8cc..0b87925ea1c8 100644 --- a/src/relay/pass/match_exhaustion.cc +++ b/src/relay/pass/match_exhaustion.cc @@ -119,11 +119,13 @@ Array> CartesianProduct(Array> fields) { return ret; } -// Expands all wildcards in the candidate pattern once, using the global type var +// Expands all wildcards in the candidate pattern once, using the pattern // to decide which constructors to insert. Returns a list of all possible expansions. Array ExpandWildcards(const Pattern& clause_pat, const Pattern& cand, - const GlobalTypeVar& gtv, const Module& mod) { + const Module& mod) { auto ctor_cand = cand.as(); + PatternConstructor clause_ctor = Downcast(clause_pat); + auto gtv = Downcast(clause_ctor->constructor->belong_to); // for a wildcard node, create constructor nodes with wildcards for all args if (!ctor_cand) { @@ -142,7 +144,6 @@ Array ExpandWildcards(const Pattern& clause_pat, const Pattern& cand, // for constructors, we will expand the wildcards in any field // that is an ADT - PatternConstructor clause_ctor = Downcast(clause_pat); Array> values_by_field; for (size_t i = 0; i < ctor_cand->constructor->inputs.size(); i++) { auto* subpattern = clause_ctor->patterns[i].as(); @@ -153,10 +154,8 @@ Array ExpandWildcards(const Pattern& clause_pat, const Pattern& cand, } // otherwise, recursively expand - auto nested_gtv = Downcast(subpattern->constructor->belong_to); values_by_field.push_back(ExpandWildcards(GetRef(subpattern), - ctor_cand->patterns[i], - nested_gtv, mod)); + ctor_cand->patterns[i], mod)); } // generate new candidates using a cartesian product @@ -198,24 +197,20 @@ Array UnmatchedCases(const Match& match, const Module& mod) { while (!candidates.empty()) { Pattern cand = candidates.top(); candidates.pop(); - GlobalTypeVar gtv = GlobalTypeVar(nullptr); + bool failure = true; for (auto clause : match->clauses) { - // if the check succeeds, then this candidate can be eliminated + // if the check fails, we move on to the next MatchResult check = checker.Check(clause->lhs, cand); if (check == MatchResult::kClash) { continue; } + // either success or we need to generate more candidates; + // either way, we're done with this candidate failure = false; - - // match was not specific enough: need to expand wildcards if (check == MatchResult::kUnspecified) { - // only a constructor pattern can fail to match so this will give - // us a global type var to use - auto ctor_pat = Downcast(clause->lhs); - gtv = ctor_pat->constructor->belong_to; - auto new_candidates = ExpandWildcards(clause->lhs, cand, gtv, mod); + auto new_candidates = ExpandWildcards(clause->lhs, cand, mod); for (auto candidate : new_candidates) { candidates.push(candidate); } From fad18da87174f6d2f6f430d381bcccf459757d3c Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Fri, 24 May 2019 12:30:20 -0700 Subject: [PATCH 6/8] Make partial matching more aggressively search for clash --- src/relay/pass/match_exhaustion.cc | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/relay/pass/match_exhaustion.cc b/src/relay/pass/match_exhaustion.cc index 0b87925ea1c8..173d6eacf528 100644 --- a/src/relay/pass/match_exhaustion.cc +++ b/src/relay/pass/match_exhaustion.cc @@ -70,11 +70,20 @@ class CandidateChecker : public PatternFunctorpatterns.size() == ctor_cand->patterns.size()); + bool unspecified = false; for (size_t i = 0; i < op->patterns.size(); i++) { MatchResult submatch = this->Check(op->patterns[i], ctor_cand->patterns[i]); - if (submatch != MatchResult::kMatch) { - return submatch; + // if we have a clash anywhere, then we can return clash + if (submatch == MatchResult::kClash) { + return MatchResult::kClash; } + if (submatch == MatchResult::kUnspecified) { + unspecified = true; + } + } + // only return unspecified if we have ruled out a clash + if (unspecified) { + return MatchResult::kUnspecified; } return MatchResult::kMatch; } From b782c03d196cc7456f69aa14d08355706fa4ff16 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Fri, 24 May 2019 12:30:27 -0700 Subject: [PATCH 7/8] Add trickier test case --- .../python/relay/test_pass_unmatched_cases.py | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/tests/python/relay/test_pass_unmatched_cases.py b/tests/python/relay/test_pass_unmatched_cases.py index eb26f08e2305..4f2bb20ad7d6 100644 --- a/tests/python/relay/test_pass_unmatched_cases.py +++ b/tests/python/relay/test_pass_unmatched_cases.py @@ -146,6 +146,44 @@ def test_multiple_constructor_clauses(): assert len(unmatched_cases(match, mod)) == 0 +def test_missing_in_the_middle(): + mod = relay.Module() + p = Prelude(mod) + + v = relay.Var('v') + match = relay.Match(v, [ + # list of length exactly 1 + relay.Clause( + relay.PatternConstructor(p.cons, [relay.PatternWildcard(), + relay.PatternConstructor(p.nil, [])]), v), + # empty list + relay.Clause( + relay.PatternConstructor(p.nil, []), v), + # list of length 3 or more + relay.Clause( + relay.PatternConstructor( + p.cons, [relay.PatternWildcard(), + relay.PatternConstructor( + p.cons, + [relay.PatternWildcard(), + relay.PatternConstructor( + p.cons, + [relay.PatternWildcard(), + relay.PatternWildcard()])])]), + v) + ]) + + # fails to match a list of length exactly two + unmatched = unmatched_cases(match, mod) + assert len(unmatched) == 1 + assert isinstance(unmatched[0], relay.PatternConstructor) + assert unmatched[0].constructor == p.cons + assert isinstance(unmatched[0].patterns[1], relay.PatternConstructor) + assert unmatched[0].patterns[1].constructor == p.cons + assert isinstance(unmatched[0].patterns[1].patterns[1], relay.PatternConstructor) + assert unmatched[0].patterns[1].patterns[1].constructor == p.nil + + def test_mixed_adt_constructors(): mod = relay.Module() box = relay.GlobalTypeVar('box') From 32f13b02dcf862ab94521c1ae50289e0f3d15789 Mon Sep 17 00:00:00 2001 From: "Steven S. Lyubomirsky" Date: Thu, 30 May 2019 16:36:43 -0700 Subject: [PATCH 8/8] Fix rebase artifacts --- python/tvm/relay/prelude.py | 43 ------------------------------------- 1 file changed, 43 deletions(-) diff --git a/python/tvm/relay/prelude.py b/python/tvm/relay/prelude.py index 0aef01ef4acf..4e7d52c4bdc2 100644 --- a/python/tvm/relay/prelude.py +++ b/python/tvm/relay/prelude.py @@ -49,49 +49,6 @@ def define_list_hd(self): cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), y) self.mod[self.hd] = Function([x], Match(x, [cons_case]), a, [a]) - def define_list_tl(self): - """Defines a function to get the tail of a list. - - tl(l) : list[a] -> list[a] - """ - self.tl = GlobalVar("tl") - a = TypeVar("a") - x = Var("x", self.l(a)) - y = Var("y") - z = Var("z") - cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), z) - self.mod[self.tl] = Function([x], Match(x, [cons_case]), self.l(a), [a]) - - def define_list_nth(self): - """Defines a function to get the nth element of a list. - - nth(l) : list[a] -> a - """ - self.nth = GlobalVar("nth") - a = TypeVar("a") - x = Var("x", self.l(a)) - n = Var("n", self.nat()) - - y = Var("y") - z_case = Clause(PatternConstructor(self.z), self.hd(x)) - s_case = Clause(PatternConstructor(self.s, [PatternVar(y)]), self.nth(self.tl(x), y)) - self.mod[self.nth] = Function([x, n], Match(n, [z_case, s_case]), a, [a]) - - def define_list_hd(self): - """Defines a function to get the head of a list. Assume the list has at least one - element. - - hd(l) : list[a] -> a - """ - self.hd = GlobalVar("hd") - a = TypeVar("a") - x = Var("x", self.l(a)) - y = Var("y") - z = Var("z") - cons_case = Clause(PatternConstructor(self.cons, [PatternVar(y), PatternVar(z)]), y) - self.mod[self.hd] = Function([x], Match(x, [cons_case]), a, [a]) - - def define_list_tl(self): """Defines a function to get the tail of a list.