(* tests on Atools.thy and Atools.ML

   author: Walther Neuper

   050814, 08:51

   (c) due to copyright terms

use"../smltest/IsacKnowledge/atools.sml";

use"atools.sml";

*)

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

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

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

"----------- occurs_in -------------------------------------------";

"----------- argument_of -----------------------------------------";

"----------- sameFunId -------------------------------------------";

"----------- filter_sameFunId ------------------------------------";

"----------- boollist2sum ----------------------------------------";

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

val thy = Atools.thy;

"----------- occurs_in -------------------------------------------";

"----------- occurs_in -------------------------------------------";

"----------- occurs_in -------------------------------------------";

fun str2term str = (term_of o the o (parse thy )) str;

fun term2s t = Syntax.string_of_term (thy2ctxt thy) t;

val t = str2term "x";

if occurs_in t t then "OK" else error "atools.sml: occurs_in x x -> f";

val t = str2term "x occurs_in x";

val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;

if (term2s t') = "x occurs_in x = True" then ()

else error "atools.sml: x occurs_in x = True ???";

"------- some_occur_in";

some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");

val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \

		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;

if term2str t' =

   "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()

else error "atools.sml: some_occur_in true";

val t = str2term "some_of [c_3, c_4] occur_in \

		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;

if term2str t' =

   "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()

else error "atools.sml: some_occur_in false";

"----------- argument_of -----------------------------------------";

"----------- argument_of -----------------------------------------";

"----------- argument_of -----------------------------------------";

val t = str2term "argument_in (M_b x)";

val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;

if term2s t' = "(argument_in M_b x) = x" then ()

else error "atools.sml:(argument_in M_b x) = x  ???";

"----------- sameFunId -------------------------------------------";

"----------- sameFunId -------------------------------------------";

"----------- sameFunId -------------------------------------------";

val t = str2term "M_b L"; atomty t;

val t as f1 $ _ = str2term "M_b L";

val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";

f1 = f2 (*true*);

val (p as Const ("Atools.sameFunId",_) $ 

			(f1 $ _) $ 

			(Const ("op =", _) $ (f2 $ _) $ _)) = 

    str2term "sameFunId (M_b L) (M_b x = c + L*x)";

f1 = f2 (*true*);

eval_sameFunId "" "Atools.sameFunId" 

		 (str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);

eval_sameFunId "" "Atools.sameFunId" 

		 (str2term "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);

eval_sameFunId "" "Atools.sameFunId" 

		 (str2term "sameFunId (M_b L) (  y x = c + L*x)")""(*false*);

eval_sameFunId "" "Atools.sameFunId" 

		 (str2term "sameFunId (  y L) (M_b x = c + L*x)")""(*false*);

eval_sameFunId "" "Atools.sameFunId" 

		 (str2term "sameFunId (  y L) (  y x = c + L*x)")""(*true*);

"----------- filter_sameFunId ------------------------------------";

"----------- filter_sameFunId ------------------------------------";

"----------- filter_sameFunId ------------------------------------";

val flhs as (fid $ _) = str2term "y' L";

val fs = str2term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) = 

    str2term "filter_sameFunId (y' L) \

	     \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";

if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()

else error "atools.slm diff.behav. in filter_sameFunId";

"----------- boollist2sum ----------------------------------------";

"----------- boollist2sum ----------------------------------------";

"----------- boollist2sum ----------------------------------------";

val u_ = str2term "[]";

val u_ = str2term "[b1 = k - 2*q]";

val u_ = str2term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

val ut_ = isalist2list u_;

val sum_ = map lhs ut_;

val t = list2sum sum_;

term2str t;

val t = str2term 

       "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

val p as Const ("Atools.boollist2sum", _) $ (Const ("List.list.Cons", _) $

						   _ $ _) = t;

val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";

if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 

else error "atools.sml diff.behav. in eval_boollist2sum";

trace_rewrite:=true;

val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls 

		      [Calc ("Atools.boollist2sum", eval_boollist2sum "")];

val t = str2term 

       "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

case rewrite_set_ thy false srls_ t of SOME _ => ()

| _ => error "atools.sml diff.rewrite boollist2sum";

trace_rewrite:=false;

(* use"IsacKnowledge/Atools.ML";

   use"../smltest/IsacKnowledge/atools.sml";

   *)