You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@tvm.apache.org by GitBox <gi...@apache.org> on 2020/06/21 23:26:00 UTC

[GitHub] [incubator-tvm] hypercubestart opened a new pull request #5881: [WIP][Relay] Mutual Recursion Support

hypercubestart opened a new pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881


   Working on adding mutual recursion to as a relay pass. 
   
   cc for help and advice: @MarisaKirisame @jroesch 


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] wweic commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
wweic commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475262656



##########
File path: include/tvm/relay/transform.h
##########
@@ -210,6 +210,16 @@ TVM_DLL Pass FastMath();
  */
 TVM_DLL Pass InferType();
 
+/*!
+ * \brief Infer the type of all functions in a module.
+ *
+ * This pass should be used when typechecking modules
+ * with mutually recursive functions.
+ *
+ * \return The pass.
+ */
+TVM_DLL Pass InferTypeAll();

Review comment:
       once this is stabilized, we should deprecate `InferType`.




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] jroesch commented on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
jroesch commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-680276865


   Can we hold off on merging this until #6274 lands? This heavily changes the way the type inferencer works. 


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475823330



##########
File path: tests/python/relay/test_type_infer.py
##########
@@ -362,6 +365,147 @@ def test_let_polymorphism():
     int32 = relay.TensorType((), "int32")
     tvm.ir.assert_structural_equal(body.checked_type, relay.TupleType([int32, relay.TupleType([])]))
 
+def test_mutual_recursion():
+    # f(x) = if x > 0 then g(x - 1) else 0
+    # g(y) = if y > 0 then f(y - 1) else 0
+    tensortype = relay.TensorType((), 'float32')
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    zero = relay.Constant(tvm.nd.array(np.array(0, dtype='float32')))
+    one = relay.Constant(tvm.nd.array(np.array(1, dtype='float32')))
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func):
+        subtract_one = relay.op.subtract(var, one)
+        cond = relay.If(relay.op.greater(var, zero),
+                        relay.Call(call_func, [subtract_one]),
+                        zero)
+        func = relay.Function([var], cond)
+        return func
+
+    f = body(x, g_gv)
+    g = body(y, f_gv)
+
+    mod = tvm.IRModule()
+    # p = Prelude(mod)
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    expected = relay.FuncType([tensortype], tensortype)
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_adt():
+    # f[A](x: A) = match x {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => g(b)
+    # }
+    # g[B](y: B) = match y {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => f(b)
+    # }
+    p = Prelude()
+    l = p.l
+
+    A = relay.TypeVar("A")
+    B = relay.TypeVar("B")
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func, type_param):
+        a = relay.Var("a", type_param)
+        b = relay.Var("b")
+        body = relay.Match(
+            var, 
+            [
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternVar(a), relay.PatternConstructor(p.nil)]), a),
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternWildcard(), relay.PatternVar(b)]), relay.Call(call_func, [b]))
+            ],
+            complete=False
+        )
+        func = relay.Function([var], body, type_params=[type_param])
+        return func
+
+    f = body(x, g_gv, A)
+    g = body(y, f_gv, B)
+
+    mod = p.mod
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    tv = relay.TypeVar("test")
+    expected = relay.FuncType([l(tv)], tv, [tv])
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_peano():
+    # even and odd function for peano function
+    # even(x) = match x {
+    #   z => true
+    #   s(a: nat) => odd(a)
+    # }
+    # odd(x) = match x {
+    #   z => false
+    #   s(a: nat) => even(a)
+    # }
+    p = Prelude()
+    add_nat_definitions(p)
+    z = p.z

Review comment:
       the parser isn't set up to handle mutual recursive functions, we would have to make changes to the parser which feels out of the scope of this PR




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] MarisaKirisame commented on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
MarisaKirisame commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-680278434


   @hypercubestart sorry to put this on hold, but IMHO 6274 is an essential PR and we should focus on it with stronger priority. everything is good and we will merge this after 6274.


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on pull request #5881: [WIP][Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-678063156


   ready for review @MarisaKirisame @jroesch @slyubomirsky @joshpoll @tqchen @wweic @weberlo 


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] MarisaKirisame commented on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
MarisaKirisame commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-679084125


   Please rebase.


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475802507



##########
File path: src/relay/transforms/type_infer.cc
##########
@@ -109,6 +134,44 @@ class TypeInferencer : private ExprFunctor<Type(const Expr&)>,
   // inference the type of expr.
   Expr Infer(Expr expr);
 
+  void SetCurrentFunc(GlobalVar current_func) {
+    this->current_func_ = current_func;
+    this->solver_.SetCurrentFunc(current_func);
+  }
+
+  void Solve();
+  Expr ResolveType(Expr expr);
+
+  // Lazily get type for expr
+  // expression, we will populate it now, and return the result.
+  Type GetType(const Expr& expr) {
+    auto it = type_map_.find(expr);
+    if (it != type_map_.end() && it->second.checked_type.defined()) {
+      if (expr.as<GlobalVarNode>() != nullptr) {
+        // if we don't dedup GlobalVarNode, two functions that use the same GlobalVar
+        // may resolve to the same type incorrectly
+        return DeDupType().VisitType(it->second.checked_type);

Review comment:
       if we DeDup a TypeVar, this will always be incorrect because there is no subst taking place.
   
   i.e.
   ```
   In `id`: 
     fn [A](%x: A) -> A {
     %x
   } unable to unify: `A` and `A`;
   ```
   %x is DeDup into a different typevar which is incorrect




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475825103



##########
File path: src/relay/op/type_relations.cc
##########
@@ -126,6 +126,7 @@ bool BroadcastCompRel(const Array<Type>& types, int num_inputs, const Attrs& att
       return true;
     }
   }
+  reporter->Assign(types[0], types[1]);

Review comment:
       ```
       # f(x) = if x > 0 then g(x - 1) else 0
       # g(y) = if y > 0 then f(y - 1) else 0
   ```
   this test doesn't typecheck otherwise




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] wweic commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
wweic commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475262844



##########
File path: python/tvm/ir/module.py
##########
@@ -87,6 +87,10 @@ def _add(self, var, val, update=False):
                 var = _ty.GlobalTypeVar(var)
             _ffi_api.Module_AddDef(self, var, val, update)
 
+    def add_unchecked(self, var, val):

Review comment:
       add a doc string

##########
File path: src/relay/analysis/type_solver.h
##########
@@ -65,6 +65,9 @@ class TypeSolver {
  public:
   TypeSolver(const GlobalVar& current_func, const IRModule& _mod, ErrorReporter* err_reporter);
   ~TypeSolver();
+
+  void SetCurrentFunc(GlobalVar current_func) { this->current_func = current_func; }

Review comment:
       add a comment

##########
File path: python/tvm/relay/transform/transform.py
##########
@@ -98,6 +98,8 @@ def InferType():
     """
     return _ffi_api.InferType()
 
+def InferTypeAll():

Review comment:
       Add a doc string

##########
File path: src/relay/transforms/type_infer.cc
##########
@@ -109,6 +134,44 @@ class TypeInferencer : private ExprFunctor<Type(const Expr&)>,
   // inference the type of expr.
   Expr Infer(Expr expr);
 
+  void SetCurrentFunc(GlobalVar current_func) {
+    this->current_func_ = current_func;
+    this->solver_.SetCurrentFunc(current_func);
+  }
+
+  void Solve();
+  Expr ResolveType(Expr expr);

Review comment:
       add a comment.




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] MarisaKirisame commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
MarisaKirisame commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475869124



##########
File path: src/relay/op/type_relations.cc
##########
@@ -126,6 +126,7 @@ bool BroadcastCompRel(const Array<Type>& types, int num_inputs, const Attrs& att
       return true;
     }
   }
+  reporter->Assign(types[0], types[1]);

Review comment:
       even if you add explicit type? not doing anything is the correct thing, and i dont think you should do this (look unsound to me) to make the type checker stronger - probably too strong.




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475911255



##########
File path: src/relay/op/type_relations.cc
##########
@@ -126,6 +126,7 @@ bool BroadcastCompRel(const Array<Type>& types, int num_inputs, const Attrs& att
       return true;
     }
   }
+  reporter->Assign(types[0], types[1]);

Review comment:
       removed, added type annotation to test. thanks!




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart edited a comment on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart edited a comment on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-678063156


   ready for review cc: @MarisaKirisame @jroesch @slyubomirsky @joshpoll @tqchen @wweic @weberlo 


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] tqchen closed pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
tqchen closed pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881


   


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475823726



##########
File path: src/relay/analysis/type_solver.h
##########
@@ -65,6 +65,9 @@ class TypeSolver {
  public:
   TypeSolver(const GlobalVar& current_func, const IRModule& _mod, ErrorReporter* err_reporter);
   ~TypeSolver();
+
+  void SetCurrentFunc(GlobalVar current_func) { this->current_func = current_func; }

Review comment:
       done thanks!




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] jroesch commented on pull request #5881: [WIP][Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
jroesch commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-672641857


   Sorry I meant to review this a long time ago and just got sidetracked by lots of things. I'm currently working on refactoring the type inferencer to use the new diagnostics. I should have a branch out by next week, could you potentially rebase on top of that and land these tests? 


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-679820639


   @wweic @jroesch could you review?


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] wweic commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
wweic commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475262656



##########
File path: include/tvm/relay/transform.h
##########
@@ -210,6 +210,16 @@ TVM_DLL Pass FastMath();
  */
 TVM_DLL Pass InferType();
 
+/*!
+ * \brief Infer the type of all functions in a module.
+ *
+ * This pass should be used when typechecking modules
+ * with mutually recursive functions.
+ *
+ * \return The pass.
+ */
+TVM_DLL Pass InferTypeAll();

Review comment:
       once this is stabilized, we should deprecate `InferType`.




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475823330



##########
File path: tests/python/relay/test_type_infer.py
##########
@@ -362,6 +365,147 @@ def test_let_polymorphism():
     int32 = relay.TensorType((), "int32")
     tvm.ir.assert_structural_equal(body.checked_type, relay.TupleType([int32, relay.TupleType([])]))
 
+def test_mutual_recursion():
+    # f(x) = if x > 0 then g(x - 1) else 0
+    # g(y) = if y > 0 then f(y - 1) else 0
+    tensortype = relay.TensorType((), 'float32')
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    zero = relay.Constant(tvm.nd.array(np.array(0, dtype='float32')))
+    one = relay.Constant(tvm.nd.array(np.array(1, dtype='float32')))
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func):
+        subtract_one = relay.op.subtract(var, one)
+        cond = relay.If(relay.op.greater(var, zero),
+                        relay.Call(call_func, [subtract_one]),
+                        zero)
+        func = relay.Function([var], cond)
+        return func
+
+    f = body(x, g_gv)
+    g = body(y, f_gv)
+
+    mod = tvm.IRModule()
+    # p = Prelude(mod)
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    expected = relay.FuncType([tensortype], tensortype)
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_adt():
+    # f[A](x: A) = match x {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => g(b)
+    # }
+    # g[B](y: B) = match y {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => f(b)
+    # }
+    p = Prelude()
+    l = p.l
+
+    A = relay.TypeVar("A")
+    B = relay.TypeVar("B")
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func, type_param):
+        a = relay.Var("a", type_param)
+        b = relay.Var("b")
+        body = relay.Match(
+            var, 
+            [
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternVar(a), relay.PatternConstructor(p.nil)]), a),
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternWildcard(), relay.PatternVar(b)]), relay.Call(call_func, [b]))
+            ],
+            complete=False
+        )
+        func = relay.Function([var], body, type_params=[type_param])
+        return func
+
+    f = body(x, g_gv, A)
+    g = body(y, f_gv, B)
+
+    mod = p.mod
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    tv = relay.TypeVar("test")
+    expected = relay.FuncType([l(tv)], tv, [tv])
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_peano():
+    # even and odd function for peano function
+    # even(x) = match x {
+    #   z => true
+    #   s(a: nat) => odd(a)
+    # }
+    # odd(x) = match x {
+    #   z => false
+    #   s(a: nat) => even(a)
+    # }
+    p = Prelude()
+    add_nat_definitions(p)
+    z = p.z

Review comment:
       parser fails to handle a module with mutually recursive functions, we would have to make changes to the parser which feels out of the scope of this PR.




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart edited a comment on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart edited a comment on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-679820639


   @wweic @jroesch could you review please?


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] hypercubestart commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
hypercubestart commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475824761



##########
File path: src/relay/transforms/type_infer.cc
##########
@@ -86,6 +86,31 @@ struct ResolvedTypeInfo {
   Array<Type> type_args = Array<Type>(ObjectPtr<Object>(nullptr));
 };
 
+// helper class to dedup typevars of a type
+// - types do not have to be already typechecked
+//
+// This is used to Dedup GlobalVar type to avoid
+// incorrect type resolving across different usages
+class DeDupType : public TypeMutator, public ExprMutator, public PatternMutator {

Review comment:
       moved to `de_deplicate.cc` thanks!




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] wweic commented on pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
wweic commented on pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#issuecomment-678824179


   I'll try to take a pass today


----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org



[GitHub] [incubator-tvm] MarisaKirisame commented on a change in pull request #5881: [Relay] Mutual Recursion Support

Posted by GitBox <gi...@apache.org>.
MarisaKirisame commented on a change in pull request #5881:
URL: https://github.com/apache/incubator-tvm/pull/5881#discussion_r475539746



##########
File path: src/relay/analysis/type_solver.h
##########
@@ -65,6 +65,9 @@ class TypeSolver {
  public:
   TypeSolver(const GlobalVar& current_func, const IRModule& _mod, ErrorReporter* err_reporter);
   ~TypeSolver();
+
+  void SetCurrentFunc(GlobalVar current_func) { this->current_func = current_func; }

Review comment:
       ```suggestion
     void SetCurrentFunc(const GlobalVar& current_func) { this->current_func = current_func; }
   ```

##########
File path: src/relay/transforms/type_infer.cc
##########
@@ -86,6 +86,31 @@ struct ResolvedTypeInfo {
   Array<Type> type_args = Array<Type>(ObjectPtr<Object>(nullptr));
 };
 
+// helper class to dedup typevars of a type
+// - types do not have to be already typechecked
+//
+// This is used to Dedup GlobalVar type to avoid
+// incorrect type resolving across different usages
+class DeDupType : public TypeMutator, public ExprMutator, public PatternMutator {

Review comment:
       move to common file

##########
File path: tests/python/relay/test_type_infer.py
##########
@@ -362,6 +365,147 @@ def test_let_polymorphism():
     int32 = relay.TensorType((), "int32")
     tvm.ir.assert_structural_equal(body.checked_type, relay.TupleType([int32, relay.TupleType([])]))
 
+def test_mutual_recursion():
+    # f(x) = if x > 0 then g(x - 1) else 0
+    # g(y) = if y > 0 then f(y - 1) else 0
+    tensortype = relay.TensorType((), 'float32')
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    zero = relay.Constant(tvm.nd.array(np.array(0, dtype='float32')))
+    one = relay.Constant(tvm.nd.array(np.array(1, dtype='float32')))
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func):
+        subtract_one = relay.op.subtract(var, one)
+        cond = relay.If(relay.op.greater(var, zero),
+                        relay.Call(call_func, [subtract_one]),
+                        zero)
+        func = relay.Function([var], cond)
+        return func
+
+    f = body(x, g_gv)
+    g = body(y, f_gv)
+
+    mod = tvm.IRModule()
+    # p = Prelude(mod)
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    expected = relay.FuncType([tensortype], tensortype)
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_adt():
+    # f[A](x: A) = match x {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => g(b)
+    # }
+    # g[B](y: B) = match y {
+    #   Cons(a, Nil) => a
+    #   Cons(_, b) => f(b)
+    # }
+    p = Prelude()
+    l = p.l
+
+    A = relay.TypeVar("A")
+    B = relay.TypeVar("B")
+
+    x = relay.Var("x")
+    y = relay.Var("y")
+
+    f_gv = relay.GlobalVar('f')
+    g_gv = relay.GlobalVar('g')
+
+    def body(var, call_func, type_param):
+        a = relay.Var("a", type_param)
+        b = relay.Var("b")
+        body = relay.Match(
+            var, 
+            [
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternVar(a), relay.PatternConstructor(p.nil)]), a),
+                relay.Clause(relay.PatternConstructor(p.cons, [relay.PatternWildcard(), relay.PatternVar(b)]), relay.Call(call_func, [b]))
+            ],
+            complete=False
+        )
+        func = relay.Function([var], body, type_params=[type_param])
+        return func
+
+    f = body(x, g_gv, A)
+    g = body(y, f_gv, B)
+
+    mod = p.mod
+    mod.add_unchecked(f_gv, f)
+    mod.add_unchecked(g_gv, g)
+    mod = transform.InferTypeAll()(mod)
+
+    tv = relay.TypeVar("test")
+    expected = relay.FuncType([l(tv)], tv, [tv])
+    tvm.ir.assert_structural_equal(mod[f_gv].checked_type, expected)
+    tvm.ir.assert_structural_equal(mod[g_gv].checked_type, expected)
+
+def test_mutual_recursion_peano():
+    # even and odd function for peano function
+    # even(x) = match x {
+    #   z => true
+    #   s(a: nat) => odd(a)
+    # }
+    # odd(x) = match x {
+    #   z => false
+    #   s(a: nat) => even(a)
+    # }
+    p = Prelude()
+    add_nat_definitions(p)
+    z = p.z

Review comment:
       can you try using the parser?

##########
File path: src/relay/op/type_relations.cc
##########
@@ -126,6 +126,7 @@ bool BroadcastCompRel(const Array<Type>& types, int num_inputs, const Attrs& att
       return true;
     }
   }
+  reporter->Assign(types[0], types[1]);

Review comment:
       why?

##########
File path: src/relay/transforms/type_infer.cc
##########
@@ -109,6 +134,44 @@ class TypeInferencer : private ExprFunctor<Type(const Expr&)>,
   // inference the type of expr.
   Expr Infer(Expr expr);
 
+  void SetCurrentFunc(GlobalVar current_func) {
+    this->current_func_ = current_func;
+    this->solver_.SetCurrentFunc(current_func);
+  }
+
+  void Solve();
+  Expr ResolveType(Expr expr);
+
+  // Lazily get type for expr
+  // expression, we will populate it now, and return the result.
+  Type GetType(const Expr& expr) {
+    auto it = type_map_.find(expr);
+    if (it != type_map_.end() && it->second.checked_type.defined()) {
+      if (expr.as<GlobalVarNode>() != nullptr) {
+        // if we don't dedup GlobalVarNode, two functions that use the same GlobalVar
+        // may resolve to the same type incorrectly
+        return DeDupType().VisitType(it->second.checked_type);

Review comment:
       what if you always dedup?




----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

For queries about this service, please contact Infrastructure at:
users@infra.apache.org