title: K Framework: Macros not recursively expanding
body: <p>I was looking at one of the tutorial exercises (the <a href="https://github.com/kframework/k/tree/master/k-distribution/tutorial/2_languages/4_logik/extended/exercises/logik-extended" rel="nofollow noreferrer">LOGIK extended</a> exercise), and for some reason one of the macro rules only expands once. I didn't change anything in <code>logik.k</code> other than adding the following lines to the <code>LOGIK</code> module so K would actually run the files:</p>
  
  <pre><code>syntax KResult ::= Val 
  configuration &lt;T&gt; &lt;k&gt; $PGM:Pgm &lt;/k&gt; &lt;/T&gt;
  </code></pre>
  
  <p>Then I ran:</p>
  
  <pre><code>kompile  --backend java  logik.k -d .
  krun tests/list-member-1.logik
  </code></pre>
  
  <p>And I got (I added some newlines for readability):</p>
  
  <pre><code>&lt;T&gt;
    &lt;k&gt;
      member ( X , [ X , .Terms | _ ] , .Terms ) . 
      member ( X , [ _ , .Terms | T ] , .Terms ) :- member ( X , T , .Terms ) , .Predicates . 
      ?- member ( 5 , [ 1 , .Terms | [ 2 , 3 , 4 , 5 , 6 , 5 , .Terms | [ .Terms ] ] ] , .Terms ) , .Predicates .
    &lt;/k&gt;
  &lt;/T&gt;
  </code></pre>
  
  <p>But I would expect the query to be</p>
  
  <pre><code>?- member ( 5 , [ 1 , .Terms | [ 2 , .Terms | [ 3 , .Terms | [4 , .Terms | [5 , .Terms | [6 , .Terms | [5 , .Terms | [ .Terms ] ] ] ] ] ] ] ] , .Terms ).
  </code></pre>
  
  <p>To be clear, the following rules seem to be the issue, as I would expect the rules to keep being used until they can't anymore, and I can't see why they would stop now.</p>
  
  <pre><code>  rule [T1:Term,T2:Term,Ts:Terms|T':Term] =&gt; [T1|[T2,Ts|T']]      [macro]
    rule [T:Term,Ts:Terms] =&gt; [T,Ts|[.Terms]]                      [macro]
  </code></pre>