[ optimise ] Union double matching on one variable

Author: spcfox

src/Core/Case/Optimise.idr

@@ -114,6 +114,9 @@ optimiseTree ps (Case idx el ty alts)
            Right p => case mapFst catMaybes $ optimiseAlts ps var p alts of
                            ([], def) => def
                            (alts, Nothing) => Just $ Case idx el ty alts
+                           (alts, Just def@(Case idx' _ _ alts')) =>
+                               Just $ Case idx el ty $ alts ++
+                                 if idx == idx' then alts' else [DefaultCase def]
                            (alts, Just def) =>
                                Just $ Case idx el ty $ alts ++ [DefaultCase def]
 optimiseTree _ tm = Just tm

tests/idris2/casetree/casetree006/expected

@@ -10,19 +10,17 @@ Compile time tree: case {arg:1} of
             First {e:25} {e:26} {e:27} => 1
           True => case {arg:5} of
             First {e:28} {e:29} {e:30} => 2
-      _ => case {arg:3} of
-        (::) {e:1} {e:2} {e:3} => case {arg:5} of
-          First {e:4} {e:5} {e:6} => 5
+      (::) {e:1} {e:2} {e:3} => case {arg:5} of
+        First {e:4} {e:5} {e:6} => 5
     S {e:19} => case {arg:3} of
       Nil {e:31} => case {arg:4} of
         (::) {e:32} {e:33} {e:34} {e:35} => case {e:34} of
           False => case {arg:5} of
             Later {e:36} {e:37} {e:38} {e:39} {e:40} {e:41} => 3
           True => case {arg:5} of
             Later {e:42} {e:43} {e:44} {e:45} {e:46} {e:47} => 4
-      _ => case {arg:3} of
-        (::) {e:7} {e:8} {e:9} => case {arg:5} of
-          Later {e:10} {e:11} {e:12} {e:13} {e:14} {e:15} => 6
+      (::) {e:7} {e:8} {e:9} => case {arg:5} of
+        Later {e:10} {e:11} {e:12} {e:13} {e:14} {e:15} => 6
   _ => case {arg:2} of
     Z => case {arg:3} of
       (::) {e:1} {e:2} {e:3} => case {arg:5} of
@@ -34,7 +32,7 @@ Erasable args: [0, 5]
 Detaggable arg types: [4, 5]
 Inferrable args: [0, 2]
 Compiled: \ {arg:1}, {arg:2}, {arg:3}, {arg:4} => case {arg:1} of
-  { _builtin.CONS {tag = 1} [cons] {e:8} {e:9} => case {arg:2} of  { 0 => case {arg:3} of  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.CONS {tag = 1} [cons] {e:14} {e:15} => case {e:14} of  { 0 => 1; 1 => 2}}; _ => case {arg:3} of  { _builtin.CONS {tag = 1} [cons] {e:2} {e:3} => 5}}; _ => case {arg:3} of  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.CONS {tag = 1} [cons] {e:19} {e:20} => case {e:19} of  { 0 => 3; 1 => 4}}; _ => case {arg:3} of  { _builtin.CONS {tag = 1} [cons] {e:5} {e:6} => 6}}}
+  { _builtin.CONS {tag = 1} [cons] {e:8} {e:9} => case {arg:2} of  { 0 => case {arg:3} of  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.CONS {tag = 1} [cons] {e:14} {e:15} => case {e:14} of  { 0 => 1; 1 => 2}}; _builtin.CONS {tag = 1} [cons] {e:2} {e:3} => 5}; _ => case {arg:3} of  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.CONS {tag = 1} [cons] {e:19} {e:20} => case {e:19} of  { 0 => 3; 1 => 4}}; _builtin.CONS {tag = 1} [cons] {e:5} {e:6} => 6}}
   ; _ => case {arg:2} of
            { 0 => case {arg:3} of
                     { _builtin.CONS {tag = 1} [cons] {e:2} {e:3} => 5

tests/idris2/total/total022/expected

@@ -4,20 +4,18 @@ Arguments [{arg:1}, {arg:2}, {arg:3}, {arg:4}]
 Compile time tree: case {arg:1} of
   Nil {e:1} => case {arg:4} of
     Nothing {e:2} => ()
-    _ => case {arg:4} of
-      Just {e:3} {e:4} => case {e:4} of
-        Refl {e:5} {e:6} => f {arg:3} {arg:2} {arg:3} Nothing
+    Just {e:3} {e:4} => case {e:4} of
+      Refl {e:5} {e:6} => f {arg:3} {arg:2} {arg:3} Nothing
   (::) {e:7} {e:8} {e:9} => case {arg:4} of
     Nothing {e:10} => f {e:9} {arg:2} {arg:3} Nothing
-    _ => case {arg:4} of
-      Just {e:3} {e:4} => case {e:4} of
-        Refl {e:5} {e:6} => f {arg:3} {arg:2} {arg:3} Nothing
+    Just {e:3} {e:4} => case {e:4} of
+      Refl {e:5} {e:6} => f {arg:3} {arg:2} {arg:3} Nothing
   _ => case {arg:4} of
     Just {e:3} {e:4} => case {e:4} of
       Refl {e:5} {e:6} => f {arg:3} {arg:2} {arg:3} Nothing
 Compiled: \ {arg:1}, {arg:2}, {arg:3}, {arg:4} => case {arg:1} of
-  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.NOTHING {tag = 0} [nothing] => ___; _ => case {arg:4} of  { _builtin.JUST {tag = 1} [just] {e:4} => Main.f {arg:3} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing])}}
-  ; _builtin.CONS {tag = 1} [cons] {e:8} {e:9} => case {arg:4} of  { _builtin.NOTHING {tag = 0} [nothing] => Main.f {e:9} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing]); _ => case {arg:4} of  { _builtin.JUST {tag = 1} [just] {e:4} => Main.f {arg:3} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing])}}
+  { _builtin.NIL {tag = 0} [nil] => case {arg:4} of  { _builtin.NOTHING {tag = 0} [nothing] => ___; _builtin.JUST {tag = 1} [just] {e:4} => Main.f {arg:3} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing])}
+  ; _builtin.CONS {tag = 1} [cons] {e:8} {e:9} => case {arg:4} of  { _builtin.NOTHING {tag = 0} [nothing] => Main.f {e:9} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing]); _builtin.JUST {tag = 1} [just] {e:4} => Main.f {arg:3} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing])}
   ; _ => case {arg:4} of
            { _builtin.JUST {tag = 1} [just] {e:4} => Main.f {arg:3} {arg:2} {arg:3} (_builtin.NOTHING {tag = 0} [nothing])
            }