(* Title: tests for ListC

   Author: Walther Neuper 17.6.00

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------";

"-----------------------------------------------------------------------------";

"----------- inssort in SML --------------------------------------------------";

"----------- insertion sort by rewrite stepwise ------------------------------";

"----------- insertion sort with ruleset -------------------------------------";

"----------- insertion sort with MathEngine ----------------------------------";

"----------- insertion sort: CAS-command -------------------------------------";

"----------- insertion sort: met_Prog_sort_ins_steps -------------------------";

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"----------- inssort in SML --------------------------------------------------";

"----------- inssort in SML --------------------------------------------------";

"----------- inssort in SML --------------------------------------------------";

fun foldr _ [] a = a

  | foldr f (x :: xs) a = foldr f xs (f a x);

(*val foldr = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)

fun ins [] a = [a]

  | ins (x :: xs) a = if x < a then x :: (ins xs a) else a :: (x :: xs);

(*val ins = fn : int list -> int -> int list*)

fun sort xs = foldr ins xs [];

(*val sort = fn : int list -> int list*)

"----------- insertion sort by rewrite stepwise ------------------------------";

"----------- insertion sort by rewrite stepwise ------------------------------";

"----------- insertion sort by rewrite stepwise ------------------------------";

val ctxt = Proof_Context.init_global @{theory};

val SOME t = parseNEW ctxt "sort {|| 1, 3, 2 ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm sort_deff} t;

term2str t' = "xfoldr ins {|| 1, 3, 2 ||} {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';

term2str t' = "(ins 1 o xfoldr ins {|| 3, 2 ||}) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';

term2str t' = "(ins 1 o (ins 3 o xfoldr ins {|| 2 ||})) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';

term2str t' = "(ins 1 o (ins 3 o (ins 2 o xfoldr ins {|| ||}))) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Nil} t';

term2str t' = "(ins 1 o (ins 3 o (ins 2 o id))) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_id} t';

term2str t' = "(ins 1 o (ins 3 o ins 2)) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_assoc} t';

term2str t' = "(ins 1 o ins 3 o ins 2) {|| ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';

term2str t' = "(ins 1 o ins 3) (ins 2 {|| ||})";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';

term2str t' = "ins 1 (ins 3 (ins 2 {|| ||}))";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';

term2str t' = "ins 1 (ins 3 {|| 2 ||})";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';

term2str t' = "ins 1 (if 3 < 2 then {|| 3, 2 ||} else 2 @# ins 3 {|| ||})";

val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_")  t';

term2str t' = "ins 1 (if False then {|| 3, 2 ||} else 2 @# ins 3 {|| ||})";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_False} t';

term2str t' = "ins 1 (2 @# ins 3 {|| ||})";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';

term2str t' = "ins 1 {|| 2, 3 ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';

term2str t' = "if 1 < 2 then {|| 1, 2, 3 ||} else 2 @# ins 1 {|| 3 ||}";

val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_")  t';

term2str t' = "if True then {|| 1, 2, 3 ||} else 2 @# ins 1 {|| 3 ||}";

val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_True} t';

if term2str t' = "{|| 1, 2, 3 ||}" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";

"----------- insertion sort with ruleset -------------------------------------";

"----------- insertion sort with ruleset -------------------------------------";

"----------- insertion sort with ruleset -------------------------------------";

if term2str t = "InsSort.sort {|| 1, 3, 2 ||}" then () else error "CHANGED START FOR sort with ruleset";

val SOME (t', _) = rewrite_set_ @{theory} false ins_sort t;

if term2str t' = "{|| 1, 2, 3 ||}" then () else error "CHANGED RESULT FOR sort with ruleset";

"----------- insertion sort with MathEngine ----------------------------------";

"----------- insertion sort with MathEngine ----------------------------------";

"----------- insertion sort with MathEngine ----------------------------------";

val fmz = ["unsorted {||1, 3, 2||}", "sorted s_s"];

val (dI',pI',mI') = ("InsSort", ["insertion","SORT","Programming"], 

  ["Programming","SORT","insertion"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem",..*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Specify_Problem",..*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

if f2str f = "{|| 1, 2, 3 ||}"

then case nxt of ("End_Proof'", End_Proof') => ()

  | _ => error "--- insertion sort with MathEngine CHANGED 1"

else error "--- insertion sort with MathEngine CHANGED 2";

"----------- insertion sort: CAS-command -------------------------------------";

"----------- insertion sort: CAS-command -------------------------------------";

"----------- insertion sort: CAS-command -------------------------------------";

val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort {||1, 3, 2||}";

show_pt pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("Check_Postcond",..*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("End_Proof'",..*)

if f2str f = "{|| 1, 2, 3 ||}"

then case nxt of ("End_Proof'", End_Proof') => ()

  | _ => error "--- insertion sort: CAS-command CHANGED 1"

else error "--- insertion sort: CAS-command CHANGED 2";

"----------- insertion sort: met_Prog_sort_ins_steps -------------------------";

"----------- insertion sort: met_Prog_sort_ins_steps -------------------------";

"----------- insertion sort: met_Prog_sort_ins_steps -------------------------";

reset_states ();

CalcTree

[(["unsorted {||1, 3, 2||}", "sorted s_s"], 

  ("InsSort", ["insertion","SORT","Programming"], 

  ["Programming","SORT","insertion_steps"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([],Res);

val ((pt,p),_) = get_calc 1; show_pt pt;

if p = ([], Res)andalso term2str (get_obj g_res pt (fst p)) = "{|| 1, 2, 3 ||}"

andalso length (get_interval ([], Pbl) ([], Res) 1 pt) = 23 then ()

else error "met_Prog_sort_ins_steps CHANGED"