wneuper/isa: test/Tools/isac/Interpret/rewtools.sml@89b3eaa34de6

     1 (* Title: test for rewtools.sml

     2    authors: Walther Neuper 2000, 2006

     4 theory Test_Some imports Isac.Build_Thydata begin

     5 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"

     6 ML {* KEStore_Elems.set_ref_thy @{theory};

     7   fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}

     8 ML_file "Interpret/rewtools.sml"

     9 *)

    11 "--------------------------------------------------------";

    12 "--------------------------------------------------------";

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

    14 "--------------------------------------------------------";

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

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

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

    18 "----------- initContext Thy_ Integration-demo ----------";

    19 "----------- initContext..Thy_, fun context_thm ---------";

    20 "----------- initContext..Thy_, fun context_rls ---------";

    21 "----------- checkContext..Thy_, fun context_thy --------";

    22 "----------- checkContext..Thy_, fun context_rls --------";

    23 "----------- checkContext..Thy_ on last formula ---------";

    24 "----------- fun guh2theID ------------------------------";

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

    26 "--------------------------------------------------------";

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

    28 "--------------------------------------------------------";

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

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

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

    32 "----------- build fun get_bdv_subst --------------------------------";

    33 "--------------------------------------------------------";

    34 "--------------------------------------------------------";

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

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

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

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

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

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

    42 ;

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

    44     val thy = Thy_Info_get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)

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

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

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

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

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

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

    51 ;

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

    53 Thy_Info_get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)

    54 ;

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

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

    57 knowthys ()

    58 ;

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

    60         val allthys = filter_out (member Context.eq_thy

    61           [(*Thy_Info_get_theory "ProgLang",*) Thy_Info_get_theory "Interpret",

    62             Thy_Info_get_theory "MathEngine", Thy_Info_get_theory "BridgeLibisabelle"])

    63           (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"));

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

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

    66 Thy_Info_get_theory "Complex_Main";*)

    67 Thy_Info.get_theory "Complex_Main";;

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

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

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

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

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

    74 ;

    75 if thy_containing_rls "Biegelinie" "e_rls" = ("IsacScripts", "KEStore") then ()

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

    77 ;

    78 if thy_containing_rls "Build_Thydata" "list_rls" = (*FIXME: handle redifinition in several thys*)

    79   ("IsacKnowledge", "Base_Tools") then ()

    80 else error ("thy_containing_rls changed for 'Biegelinie', 'list_rls'")

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

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

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

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

    86 if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Atools")

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

    89 "----------- initContext Thy_ Integration-demo ----------";

    90 "----------- initContext Thy_ Integration-demo ----------";

    91 "----------- initContext Thy_ Integration-demo ----------";

    92 reset_states ();

    93 CalcTree

    94 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],

    95   ("Integrate",["integrate","function"],

    96   ["diff","integration"]))];

    97 Iterator 1;

    98 moveActiveRoot 1;

    99 autoCalculate 1 CompleteCalc;

   100 interSteps 1 ([1],Res);

   101 interSteps 1 ([1,1],Res);

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

   103 if existpt' ([1,1,1], Frm) pt then ()

   104 else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";

   105 initContext  1 Thy_ ([1,1,1], Frm);

   107 "----------- initContext..Thy_, fun context_thm ---------";

   108 "----------- initContext..Thy_, fun context_thm ---------";

   109 "----------- initContext..Thy_, fun context_thm ---------";

   110 reset_states (); (*start of calculation, return No.1*)

   111 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   112   ("Test", ["sqroot-test","univariate","equation","test"],

   113    ["Test","squ-equ-test-subpbl1"]))];

   114 Iterator 1; moveActiveRoot 1;

   115 autoCalculate 1 CompleteCalc;

   117 "----- no thy-context at result -----";

   118 val p = ([], Res);

   119 initContext 1 Thy_ p;

   120 val ((pt,_),_) = get_calc 1; show_pt pt; (* 11 lines with subpbl *)

   122 interSteps 1 ([2], Res);

   123 val ((pt,_),_) = get_calc 1; show_pt pt; (* added [2,1]..[2,6] *)

   124 interSteps 1 ([3,1], Res);

   125 val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *)

   127 val p = ([2,4], Res);

   128 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);

   129   member op = [Pbl,Met] p_ = false;

   130   pos = ([],Res) = false;

   131   val cs as (ptp as (pt,_),_) = get_calc cI;

   132   exist_lev_on' pt pos = true;

   133               val pos' = lev_on' pt pos

   134               val tac = get_tac_checked pt pos';

   135   is_rewtac tac = true;

   136 "~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =

   137   ((pt, pos), tac);

   138     val Appl (Rewrite' (thy', ord', erls, _, (thmID,thm), f, (res,asm))) = applicable_in pos pt tac

   139             val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

   140             val thm_deriv = Thm.get_name_hint thm;

   142 if thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv)

   143    = "thy_isac_Test-thm-radd_left_commute" then ()

   144 else error "context_thy mini-subpbl ([2,4], Res) changed";

   145 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*

   146 -rw-rw-r-- 1 wneuper wneuper 638 Aug  8 16:04 thy_isac_Test-thm-radd_left_commute.html*)

   149 val p = ([3,1,1], Frm);

   150 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);

   151   member op = [Pbl,Met] p_ = false;

   152   pos = ([],Res) = false;

   153   val cs as (ptp as (pt,_),_) = get_calc cI;

   154   exist_lev_on' pt pos = true;

   155               val pos' = lev_on' pt pos

   156               val tac = get_tac_checked pt pos';

   157   is_rewtac tac = true;

   158 "~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=

   159   ((pt, pos), tac);

   160 val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =

   161   applicable_in pos pt tac

   162              val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

   163              val thm_deriv = Thm.get_name_hint thm;

   164 if thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv) =

   165   "thy_isac_Test-thm-risolate_bdv_add" then ()

   166 else error "context_thy mini-subpbl ([3,1,1], Frm) changed";

   167 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*

   168 -rw-rw-r-- 1 wneuper wneuper 646 Aug  8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)

   171 val p = ([2,5], Res);

   172 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);

   173   member op = [Pbl,Met] p_ = false;

   174   pos = ([],Res) = false;

   175   val cs as (ptp as (pt,_),_) = get_calc cI;

   176  exist_lev_on' pt pos = true;

   177               val pos' = lev_on' pt pos

   178               val tac = get_tac_checked pt pos';

   179 if is_rewtac tac = false then ()

   180 else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"

   182 "----------- initContext..Thy_, fun context_rls ---------";

   183 "----------- initContext..Thy_, fun context_rls ---------";

   184 "----------- initContext..Thy_, fun context_rls ---------";

   185 (*using pt from above*)

   186 val p = ([1], Res);

   187 val tac = Rewrite_Set "Test_simplify";

   188 initContext 1 Thy_ p;

   189 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

   190   --- in initContext..Thy_ ---*)

   191 val ContRls {rls,result,...} = context_thy (pt,p) tac;

   192 if rls = "thy_isac_Test-rls-Test_simplify"

   193    andalso term2str result = "-1 + x = 0" then ()

   194 else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";

   196 val p = ([3,1], Frm);

   197 val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");

   198 initContext 1 Thy_ p;

   199 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 ->  x = 0 + -1 * -1

   200   --- in initContext..Thy_ ---*)

   201 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

   202 if rls =  "thy_isac_Test-rls-isolate_bdv"

   203    andalso term2str result = "x = 0 + -1 * -1" then ()

   204 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

   206 "----------- checkContext..Thy_, fun context_thy --------";

   207 "----------- checkContext..Thy_, fun context_thy --------";

   208 "----------- checkContext..Thy_, fun context_thy --------";

   209 (*using pt from above*)

   210 val p = ([2,4], Res);

   211 val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});

   212 checkContext 1 p "thy_Test-thm-radd_left_commute";

   213 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0

   214   --- in checkContext..Thy_ ---*)

   215 val ContThm {thm,result,...} = context_thy (pt,p) tac;

   216 if thm =  "thy_isac_Test-thm-radd_left_commute"

   217    andalso term2str result = "-2 + (1 + x) = 0" then ()

   218 else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";

   220 val p = ([3,1,1], Frm);

   221 val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));

   222 checkContext 1 p "thy_Test-thm-risolate_bdv_add";

   223 (* risolate_bdv_add:  -1 + x = 0 -> x = 0 + -1 * -1

   224   --- in checkContext..Thy_ ---*)

   225 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;

   226 if thm =  "thy_isac_Test-thm-risolate_bdv_add"

   227    andalso term2str result = "x = 0 + - 1 * -1" then ()

   228 else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";

   230 val p = ([2,5], Res);

   231 val tac = Calculate "plus";

   232 (*checkContext..Thy_ 1 ([2,5], Res);*)

   233 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)

   234 checkContext 1 p ;

   235 (* Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0

   236   --- in checkContext..Thy_ ---*)

   238 "----------- checkContext..Thy_, fun context_rls --------";

   239 "----------- checkContext..Thy_, fun context_rls --------";

   240 "----------- checkContext..Thy_, fun context_rls --------";

   241 (*using pt from above*)

   242 val p = ([1], Res);

   243 val tac = Rewrite_Set "Test_simplify";

   244 checkContext 1 p "thy_isac_Test-rls-Test_simplify";

   245 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

   246   --- in checkContext..Thy_ ---*)

   247 val ContRls {rls,result,...} = context_thy (pt,p) tac;

   248 if rls = "thy_isac_Test-rls-Test_simplify"

   249    andalso term2str result = "-1 + x = 0" then ()

   250 else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";

   252 val p = ([3,1], Frm);

   253 val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");

   254 checkContext 1 p "thy_Test-rls-isolate_bdv";

   255 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

   256 if rls = "thy_isac_Test-rls-isolate_bdv"

   257    andalso term2str result = "x = 0 + -1 * -1" then ()

   258 else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";

   260 "----------- checkContext..Thy_ on last formula ---------";

   261 "----------- checkContext..Thy_ on last formula ---------";

   262 "----------- checkContext..Thy_ on last formula ---------";

   263 reset_states (); (*start of calculation, return No.1*)

   264 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   265   ("Test", ["sqroot-test","univariate","equation","test"],

   266    ["Test","squ-equ-test-subpbl1"]))];

   267 Iterator 1; moveActiveRoot 1;

   269 autoCalculate 1 CompleteCalcHead;

   270 autoCalculate 1 (Step 1);

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

   272 initContext 1 Thy_ ([1], Frm);

   273 checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";

   275 autoCalculate 1 (Step 1);

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

   277 initContext 1 Thy_ ([1], Res);

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

   280 "----------- fun guh2theID ------------------------------";

   281 "----------- fun guh2theID ------------------------------";

   282 "----------- fun guh2theID ------------------------------";

   283 val guh = "thy_scri_ListG-thm-zip_Nil";

   284 (*default_print_depth 3; 999*)

   285 take_fromto 1 4 (Symbol.explode guh);

   286 take_fromto 5 9 (Symbol.explode guh);

   287 val rest = takerest (9,(Symbol.explode guh));

   289 separate "-" rest;

   290 space_implode "-" rest;

   291 commas rest;

   293 val delim = "-";

   294 val thyID = takewhile [] (not o (curry op= delim)) rest;

   295 val rest' = dropuntil (curry op= delim) rest;

   296 val setc = take_fromto 1 5 rest';

   297 val xstr = takerest (5, rest');

   299 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()

   300 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";

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

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

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

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

   307 reset_states ();

   308 CalcTree

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

   310       ("Test",

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

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

   313 Iterator 1; moveActiveRoot 1;

   314 autoCalculate 1 CompleteCalcHead;

   316 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

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

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

   320 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

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

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

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

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

   327 initContext 1 Thy_ ([1],Res);

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

   330 reset_states ();

   331 CalcTree

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

   333       ("Test",

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

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

   336 Iterator 1; moveActiveRoot 1;

   337 autoCalculate 1 CompleteCalc;

   338 interSteps 1 ([1],Res);

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

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

   343 interSteps 1 ([2],Res);

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

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

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

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

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

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

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

   353 if contains_rule r1 Test_simplify then ()

   354 else error "rewtools.sml contains_rule Thm";

   356 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");

   357 if contains_rule r1 Test_simplify then ()

   358 else error "rewtools.sml contains_rule Calc";

   360 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");

   361 if not (contains_rule r1 Test_simplify) then ()

   362 else error "rewtools.sml contains_rule Calc";

   364 "----------- build fun get_bdv_subst --------------------------------";

   365 "----------- build fun get_bdv_subst --------------------------------";

   366 "----------- build fun get_bdv_subst --------------------------------";

   367 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];

   368 val env = [(str2term "v_v", str2term "x")];

   369 subst2str env = "[\"\n(v_v, x)\"]";

   371 "~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);

   372     fun scan (Const _) = NONE

   373       | scan (Free _) = NONE

   374       | scan (Var _) = NONE

   375       | scan (Bound _) = NONE

   376       | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =

   377         if TermC.is_bdv_subst t then SOME t else NONE

   378       | scan (Abs (_, _, body)) = scan body

   379       | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

   381 val SOME tm = scan prog;

   382 val subst = tm |> subst_atomic env;

   383 if term2str tm = "[(''bdv'', v_v)]" then () else error "get_bdv_subst changed 1";

   385 if subst'_to_sube subst = ["(''bdv'', x)"] then () else error "get_bdv_subst changed 2";

   387 case get_bdv_subst prog env of

   388   (SOME ["(''bdv'', x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()

   389 | _ => error "get_bdv_subst changed 3";

   391 val (SOME subs, _) = get_bdv_subst prog env;

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 29 Aug 2019 13:52:47 +0200
changeset 59602	89b3eaa34de6
parent 59600	0914ffedb4c5
child 59603	30cd47104ad7
permissions	-rw-r--r--