(* Title:  BridgeLibisabelle/thy-present.sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

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

"----------- fun thy_containing_rls ---------------------";

"----------- apply thy_containing_rls -------------------";

"----------- fun thy_containing_cal ---------------------";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

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

(*============ inhibit exn WN120321 ==============================================

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

"----------- fun filter_appl_rews -----------------------";

============ inhibit exn WN120321 ==============================================*)

"----------- fun is_contained_in ------------------------";

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

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

"----------- fun thy_containing_rls ---------------------";

"----------- fun thy_containing_rls ---------------------";

"----------- fun thy_containing_rls ---------------------";

(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)

if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()

else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")  

;

"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");

    val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)

val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';

val SOME (thy'', _) = xxx;

val SOME ("Poly", _) = xxx;

if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";

(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)

if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"

;

"~~~~~ fun partID', args:"; val (thy') = (thy');

ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)

;

"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');

(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)

Thy_Read.knowthys () 

;

"~~~~~ fun knowthys , args:"; val () = ();

        val allthys = filter_out (member Context.eq_thy

          [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret", 

            ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) 

          (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));

length allthys = 152; (*in Isabelle2015/Isac*)

(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"

ThyC.get_theory "Complex_Main";*)

Thy_Info.get_theory "Complex_Main";;

"----------- apply thy_containing_rls -------------------";

"----------- apply thy_containing_rls -------------------";

"----------- apply thy_containing_rls -------------------";

if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()

else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")

;

if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()

else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'")

;

if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)

(**)("IsacKnowledge", "Base_Tools")(**)

(** )("IsacScripts", "Prog_Expr")( **)

then () else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")

"----------- fun thy_containing_cal ---------------------";

"----------- fun thy_containing_cal ---------------------";

"----------- fun thy_containing_cal ---------------------";

(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)

if Thy_Read.thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")

then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----------- debugging on Tests/solve_linear_as_rootpbl -";

"----- initContext -----";

reset_states ();

CalcTree 

    [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],

      ("Test",

       ["LINEAR", "univariate", "equation", "test"],

       ["Test", "solve_linear"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

if is_curr_endof_calc pt ([1],Frm) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Frm)";

autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

if not (is_curr_endof_calc pt ([1],Frm)) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";

if is_curr_endof_calc pt ([1],Res) then ()

else error "rewtools.sml is_curr_endof_calc ([1],Res)";

(*//----------------- dropped with "purge code for theory-hierarchy" * )

initContext 1 Ptool.Thy_ ([1],Res);

"----- checkContext -----";

reset_states ();

CalcTree 

    [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],

      ("Test",

       ["LINEAR", "univariate", "equation", "test"],

       ["Test", "solve_linear"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([1],Res);

val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";

interSteps 1 ([2],Res);

val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;

checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";

checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";

( *//----------------- dropped with "purge code for theory-hierarchy" *)

"----------- fun is_contained_in ------------------------";

"----------- fun is_contained_in ------------------------";

"----------- fun is_contained_in ------------------------";

val r1 = Thm ("real_diff_minus", @{thm real_diff_minus});

if Rule_Set.contains r1 Test_simplify then ()

else error "rewtools.sml Rule_Set.contains Thm";

val r1 = Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_");

if Rule_Set.contains r1 Test_simplify then ()

else error "rewtools.sml Rule_Set.contains Eval";

val r1 = Eval (\<^const_name>\<open>minus\<close>, eval_binop "#add_");

if not (Rule_Set.contains r1 Test_simplify) then ()

else error "rewtools.sml Rule_Set.contains Eval";