/* A Tvp program for exchanging left and right subtrees in a binary tree

*/

#define COMPLETE

/*
#define FULL
#define BLUR_ENTRY
#define BLUR_SUMMARY
#define ANCESTOR
*/

// **********************************************************************
// **********************************************************************
// SETS and PREDICATE DECLARATIONS
// **********************************************************************
// **********************************************************************
// ======================================================================


// ====================================================================== 
// Program variables and fields
// ====================================================================== 
%s ExchangeVarAll  	{ tree, bLeft, bRight }

%s MainVarAll		{ tree }

%s VarAll		ExchangeVarAll + MainVarAll

%s Fields { left, right }
%s Bools { }

%s FP { fp1 }
%s FR { }

// ====================================================================== 
// Standard predicates
// ====================================================================== 

#include "predicate.tvp" 

foreach (m in Mode){
  foreach (z in VarAllFPR){
    %r z(v_1) & r_down[m,z](v_2) & v_1!=v_2 & !cyc_down[m](v_1) 
       ==> !down[m](v_2,v_1)
#ifdef ANCESTOR
    %r z(v_2) & a_down[m,z](v_1) & v_1!=v_2 & !cyc_down[m](v_2) 
       ==> !down[m](v_2,v_1)
#endif
  }
  %r down[m](v_1,v_2) & !cyc_down[m](v_1) ==> !down[m](v_2,v_1)
  %r !cyc_down[m](v) & !sm(v) ==> !down[m](v,v)
}

#ifdef FULL
%s InstrumMode1 InstrumMode1 + { full_left, full_right }

foreach (m in Mode){
  %i full_left[m](v) = (E(v_1) left[m](v,v_1)) -> (E(v_1) right[m](v,v_1)) nonabs
  %i full_right[m](v) = (E(v_1) right[m](v,v_1)) -> (E(v_1) left[m](v,v_1)) nonabs
  %r (E(v_1) left[m](v,v_1)) & (A(v_2) !right[m](v,v_2)) ==> !full_left[m](v)
  %r (E(v_1) right[m](v,v_1)) & (A(v_2) !left[m](v,v_2)) ==> !full_right[m](v)
  %r (E(v_1) left[m](v,v_1)) & (E(v_1) right[m](v,v_1)) ==> full_left[m](v)
  %r (E(v_1) left[m](v,v_1)) & (E(v_1) right[m](v,v_1)) ==> full_right[m](v)
}
#endif

// ======================================================================
// specialized instrumentation predicates 
// ======================================================================


%s CrossInstrum1 CrossInstrum1 + { exch_right_succ, exch_left_succ }

foreach (m1 in Mode){
  foreach (m2 in Mode - { m1 }){
    %i exch_right_succ[m1,m2](v) = 
         A(v_1) ( right[m1](v,v_1) -> left[m2](v,v_1) ) abs
    %i exch_left_succ[m1,m2](v) = 
         A(v_1) ( left[m1](v,v_1) -> right[m2](v,v_1) ) abs
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode - { m1 }){
    %r right[m1](v_1,v_2) & left[m2](v_1,v_2) ==> exch_right_succ[m1,m2](v_1)
    %r left[m2](v_1,v_2) & right[m1](v_1,v_2) ==> exch_left_succ[m2,m1](v_1)
    %r right[m1](v_1,v_2) & !left[m2](v_1,v_2) ==> !exch_right_succ[m1,m2](v_1)
    %r left[m1](v_1,v_2) & !right[m2](v_1,v_2) ==> !exch_left_succ[m1,m2](v_1)

    %r exch_right_succ[m1,m2](v_1) & right[m1](v_1,v_2) ==> left[m2](v_1,v_2)
    %r exch_left_succ[m1,m2](v_1) & left[m1](v_1,v_2) ==> right[m2](v_1,v_2)

  }
}

foreach (m1 in Mode){
  foreach (m2 in Mode - {m1}){
    foreach (m3 in Mode - {m1,m2}){
      %r id_succ[right,m1,m2](v) & exch_right_succ[m2,m3](v)
         ==> exch_right_succ[m1,m3](v)
      %r id_succ[left,m1,m2](v) & exch_left_succ[m2,m3](v) 
         ==> exch_left_succ[m1,m3](v)
      %r exch_right_succ[m1,m2](v) & id_succ[left,m2,m3](v) 
         ==> exch_right_succ[m1,m3](v)
      %r exch_left_succ[m1,m2](v) & id_succ[right,m2,m3](v) 
         ==> exch_left_succ[m1,m3](v)

      %r exch_right_succ[m1,m2](v) & exch_left_succ[m2,m3](v) 
         ==> id_succ[right,m1,m3](v)
      %r exch_left_succ[m1,m2](v) & exch_right_succ[m2,m3](v) 
         ==> id_succ[left,m1,m3](v)
    }
  }
}

// Important: linking reachability in different modes

foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (z in VarAllFPR){
      %r r_down[m1,z](v) & (A(v_1) (r_down[m1,z](v) -> ((id_succ[right,m1,m2](v_1) & id_succ[left,m1,m2](v_1)) | (exch_right_succ[m1,m2](v_1) & exch_left_succ[m1,m2](v_1))))) ==> r_down[m2,z](v)

#ifdef ANCESTOR
      %r a_down[m1,z](v) & (A(v_1) ((a_down[m1,z](v) & !z(v_1))-> ((id_succ[right,m1,m2](v_1) & id_succ[left,m1,m2](v_1)) | (exch_right_succ[m1,m2](v_1) & exch_left_succ[m1,m2](v_1))))) ==> a_down[m2,z](v)
#endif

    }
  }
}

// Other important things
/* Idea:
foreach (m in Mode){
  %r r_down[m,bLeft](v) ==> !r_down[m,bRight](v)
  %r r_down[m,bRight](v) ==> !r_down[m,bLeft](v)
}
*/
// Real things: two subtrees of two "independent" variables are disjoint

// We specify it only for bRight and bLeft, but it could be generalized
foreach (m in Mode){
  %r r_down[m,bLeft](v) &
     (A(v) r_down[m,bLeft](v) -> !shared_down[m](v)) &
     (E(v_1,v_2)
      bLeft(v_1) & bRight(v_2) & v_1!=v_2 &
      !r_down[m,bLeft](v_2) & !r_down[m,bRight](v_1))
     ==> !r_down[m,bRight](v)
  %r r_down[m,bRight](v) &
     (A(v) r_down[m,bRight](v) -> !shared_down[m](v)) &
     (E(v_1,v_2)
      bLeft(v_1) & bRight(v_2) & v_1!=v_2 &
     !r_down[m,bLeft](v_2) & !r_down[m,bRight](v_1)) 
     ==> !r_down[m,bLeft](v)
}

%%

// **********************************************************************
// **********************************************************************
// FUNCTION DEFINITIONS
// **********************************************************************
// **********************************************************************

#include "function.tvp" 

%function BlurSummary[](X)
  %t "BlurSummary"
{
  begin
    focus(X, { r_down[out,fp1](v), cyc_down[out](v), cyc_down[ext](v) });
    let Y = transform(X,
                halt:E(v) cyc_down[out](v) | cyc_down[ext](v),
		update:{
#ifdef ANCESTOR
foreach (m in Mode){
  foreach(zz in VarAllFPR){
    a_down[m,zz](v) = (r_down[out,fp1](v) ? a_down[m,zz](v) : 1/2)
  }
}
#endif
foreach (m1 in Mode){
  foreach (m2 in Mode - {m1}){
    exch_right_succ[m1,m2](v) = (r_down[out,fp1](v) ? exch_right_succ[m1,m2](v) : 1/2)
    exch_left_succ[m1,m2](v) = (r_down[out,fp1](v) ? exch_left_succ[m1,m2](v) : 1/2)
  }
}
sm(v) = (r_down[out,fp1](v) ? sm(v) : 1/2)

// Cross-instrumentation
foreach(m in {out,ext}){
  foreach (f in Fields){
    foreach(p in CrossInstrumField1){
      p[f,inp,m](v) = 1/2
      p[f,m,inp](v) = 1/2
    }
    foreach(p in CrossInstrumField2){
      p[f,inp,m](v_1,v_2) = 1/2
      p[f,m,inp](v_1,v_2) = 1/2
    }
  }
  foreach(p in CrossInstrum1){
    p[inp,m](v) = 1/2
    p[m,inp](v) = 1/2
  }
  foreach(p in CrossInstrum2){
    p[inp,m](v_1,v_2) = 1/2
    p[m,inp](v_1,v_2) = 1/2
  }
}
})
    in 
    begin
      blur(Y);
      focus(Y, { cyc_down[out](v), cyc_down[ext](v) });
      let Z = transform(Y,
                halt:E(v) cyc_down[out](v) | cyc_down[ext](v),
	      )
      in
      Z
    end
  end
}

%function BlurEntry[](X)
     %t "BlurEntry"
{
  begin
    focus(X, { r_down[out,tree](v) });
    let Y = transform(X,
	update:{
#ifdef ANCESTOR
foreach (m in Mode){
  foreach(zz in VarAllFPR){
    a_down[m,zz](v) = 1/2
  }
}
#endif
foreach (m1 in Mode){
  foreach (m2 in Mode - {m1}){
    exch_right_succ[m1,m2](v) = (r_down[out,tree](v) ? exch_right_succ[m1,m2](v) : 1/2)
    exch_left_succ[m1,m2](v) = (r_down[out,tree](v) ? exch_left_succ[m1,m2](v) : 1/2)
  }
}
sm(v) = (r_down[out,tree](v) ? sm(v) : 1/2)
// Cross-instrumentation
foreach(m in {inp,out}){
  foreach (f in Fields){
    foreach(p in CrossInstrumField1){
      p[f,ext,m](v) = 1/2
      p[f,m,ext](v) = 1/2
    }
    foreach(p in CrossInstrumField2){
      p[f,ext,m](v_1,v_2) = 1/2
      p[f,m,ext](v_1,v_2) = 1/2
    }
  }
  foreach(p in CrossInstrum1){
    p[ext,m](v) = 1/2
    p[m,ext](v) = 1/2
  }
  foreach(p in CrossInstrum2){
    p[ext,m](v_1,v_2) = 1/2
    p[m,ext](v_1,v_2) = 1/2
  }
}
})
    in begin
      blur(Y);
      coerce(Y);
      Y
    end
  end
}

%function FocusReach[](X)
  %t "FocusReach"
{
  begin
    focus(X, { r_down[inp,bLeft](v), r_down[inp,bRight](v) });
    transform(X, halt: E(v) r_down[inp,bLeft](v) & r_down[inp,bRight](v))
  end
}

%function FocusRTree[](X)
  %t "FocusRTree"
{
  begin
    focus(X, { tree(v), r_down[out,tree](v) });
    X
  end
}
%%

// **********************************************************************
// **********************************************************************
// EQUATIONS
// **********************************************************************
// **********************************************************************

// ********************************************************************** 
// exchange */
// ********************************************************************** 

/* The function

function exchange(tree) : is
var bRight,bLeft;
begin
exchange_entry: y := tree;
exchange0:      if (tree!=null){
exchange1:         bRight = tree->right;
exchange2:         bLeft = tree->left;
exchange3:         tree->right = null;
exchange4:         tree->left = null;
exchange5:         tree->right = bLeft;
exchange6:         tree->left = bRight;
exchange7:         exchange(bRight);
exchange8:         exchange(bLeft);
exchange_end:
exchange_summary:
end
*/

exchange_entry = call_X_1[exchange, tree, tree](main_call)
exchange_entry = call_X_1[exchange, bRight, tree](exchange7)
exchange_entry = call_X_1[exchange, bLeft, tree](exchange8)
#ifdef BLUR_ENTRY
exchange_entry0  = BlurEntry[](exchange_entry)
exchange0      = IsVarNotNull[tree](exchange_entry0)
exchange_end   = IsVarNull[tree](exchange_entry0)
#else
exchange0      = IsVarNotNull[tree](exchange_entry)
exchange_end   = IsVarNull[tree](exchange_entry)
#endif
exchange2      = AssignVarNext[bRight,tree,right](exchange0)
exchange3      = AssignVarNext[bLeft,tree,left](exchange2)
exchange3a     = FocusReach[](exchange3)
exchange4      = AssignNextNull[tree,right](exchange3a)
exchange5      = AssignNextNull[tree,left](exchange4)
exchange6      = AssignNextVar[tree,right,bLeft](exchange5)
exchange7      = AssignNextVar[tree,left,bRight](exchange6)
exchange8      = ret_0_1[exchange, bRight](exchange7,exchange_summary)
exchange_end   = ret_0_1[exchange, bLeft](exchange8,exchange_summary)
#ifdef BLUR_SUMMARY
exchange_summary0 = summary_1_0[exchange,tree](exchange_end)
exchange_summary = BlurSummary[](exchange_summary0)
#else
exchange_summary = summary_1_0[exchange,tree](exchange_end)
#endif

// ********************************************************************** 
// Main
// ********************************************************************** 

main_call0 = Setup_1[tree](main_begin)
main_call = FocusRTree[](main_call0)
main_end = ret_0_1[exchange,tree](main_call,exchange_summary)

%%

exchange_entry
exchange0
exchange4
exchange7
exchange8
exchange_end
exchange_summary
main_begin
main_call
main_end

/*
main_begin
main_call0
main_call
exchange_entry
exchange0
exchange2
exchange3
exchange3a
exchange4
exchange5
exchange6
exchange7
exchange8
exchange_end
exchange_summary
main_end
*/