prepare test 4 for: push ctxt through LI
authorwneuper <Walther.Neuper@jku.at>
Sun, 21 Aug 2022 16:14:45 +0200
changeset 60531a25275e5bc73
parent 60530 edb91d2a28c1
child 60532 999794ca96b4
prepare test 4 for: push ctxt through LI
src/Tools/isac/Specify/step-specify.sml
test/Tools/isac/Knowledge/simplify.sml
test/Tools/isac/Specify/cas-command.sml
test/Tools/isac/Test_Some.thy
     1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Sun Aug 21 11:22:04 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Sun Aug 21 16:14:45 2022 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4        (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
     1.5      end;
     1.6  (* create a calc-tree with oris via an cas.refined pbl *)
     1.7 -(*  initialisePI <- nxt_specify_init_calc *)
     1.8 +(*  initialisePIDE <- nxt_specify_init_calc *)
     1.9  fun initialisePIDE (fmz, (dI, pI, mI)) = 
    1.10      let
    1.11  	    val thy = ThyC.get_theory dI
     2.1 --- a/test/Tools/isac/Knowledge/simplify.sml	Sun Aug 21 11:22:04 2022 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/simplify.sml	Sun Aug 21 16:14:45 2022 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  "--------------------------------------------------------";
     2.5  "table of contents --------------------------------------";
     2.6  "--------------------------------------------------------";
     2.7 -"----------- CAS-command Simplify -----------------------";
     2.8 +(*"----------- CAS-command Simplify -----------------------";*)
     2.9  "----------- append inform with final result ------------";
    2.10  "--------------------------------------------------------";
    2.11  "--------------------------------------------------------";
    2.12 @@ -15,20 +15,25 @@
    2.13  
    2.14  val thy = @{theory "Simplify"};
    2.15  
    2.16 -"----------- CAS-command Simplify -----------------------";
    2.17 -"----------- CAS-command Simplify -----------------------";
    2.18 -"----------- CAS-command Simplify -----------------------";
    2.19 -reset_states ();
    2.20 -CalcTree [([], References.empty)];
    2.21 -Iterator 1;
    2.22 -moveActiveRoot 1;
    2.23 -replaceFormula 1 "Simplify (2*a + 3*a)";
    2.24 -autoCalculate 1 (Steps 1);
    2.25 -autoCalculate 1 CompleteCalc;
    2.26 -val ((pt,p),_) = get_calc 1;
    2.27 -val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; UnparseC.term res;
    2.28 -if p = ([], Res) andalso UnparseC.term res = "5 * a" then ()
    2.29 -else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
    2.30 +(*
    2.31 +  This test is postponed, because respective user-requirements are not clarified.
    2.32 +  See test/../cas-command.sml --- start Calculation with CAS_Cmd ---
    2.33 +  and test/../Test_VSCode_Example.thy subsubsection \<open>Start Example with a CAS_Cmd\<close>
    2.34 +  "----------- CAS-command Simplify -----------------------";
    2.35 +  "----------- CAS-command Simplify -----------------------";
    2.36 +  "----------- CAS-command Simplify -----------------------";
    2.37 +  reset_states ();
    2.38 +  CalcTree [([], References.empty)];
    2.39 +  Iterator 1;
    2.40 +  moveActiveRoot 1;
    2.41 +  replaceFormula 1 "Simplify (2*a + 3*a)";
    2.42 +  autoCalculate 1 (Steps 1);
    2.43 +  autoCalculate 1 CompleteCalc;
    2.44 +  val ((pt,p),_) = get_calc 1;
    2.45 +  val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; UnparseC.term res;
    2.46 +  if p = ([], Res) andalso UnparseC.term res = "5 * a" then ()
    2.47 +  else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
    2.48 +*)
    2.49  
    2.50  "----------- append inform with final result ------------";
    2.51  "----------- append inform with final result ------------";
     3.1 --- a/test/Tools/isac/Specify/cas-command.sml	Sun Aug 21 11:22:04 2022 +0200
     3.2 +++ b/test/Tools/isac/Specify/cas-command.sml	Sun Aug 21 16:14:45 2022 +0200
     3.3 @@ -7,10 +7,11 @@
     3.4  "table of contents -----------------------------------------------------------------------------";
     3.5  "-----------------------------------------------------------------------------------------------";
     3.6  "----------- TODO ------------------------------------------------------------------------------";
     3.7 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
     3.8  "-----------------------------------------------------------------------------------------------";
     3.9  "-----------------------------------------------------------------------------------------------";
    3.10  "-----------------------------------------------------------------------------------------------";
    3.11  
    3.12 -"----------- TODO ------------------------------------------------------------------------------";
    3.13 -"----------- TODO ------------------------------------------------------------------------------";
    3.14 -"----------- TODO ------------------------------------------------------------------------------";
    3.15 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
    3.16 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
    3.17 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
     4.1 --- a/test/Tools/isac/Test_Some.thy	Sun Aug 21 11:22:04 2022 +0200
     4.2 +++ b/test/Tools/isac/Test_Some.thy	Sun Aug 21 16:14:45 2022 +0200
     4.3 @@ -108,7 +108,42 @@
     4.4  \<close> ML \<open>
     4.5  \<close>
     4.6  
     4.7 -section \<open>===================================================================================\<close>
     4.8 +section \<open>===== "Specify/cas-command.sml" ==================================================\<close>
     4.9 +ML \<open>
    4.10 +\<close> ML \<open>
    4.11 +\<close> ML \<open>
    4.12 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
    4.13 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
    4.14 +"----------- start Calculation with CAS_Cmd ----------------------------------------------------";
    4.15 +\<close> ML \<open>
    4.16 +val fmz = [];
    4.17 +val (dI',pI',mI') = References.empty;
    4.18 +\<close> ML \<open>
    4.19 +CalcTreeTEST [(fmz, (dI',pI',mI'))]
    4.20 +\<close> ML \<open>
    4.21 +"~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp): Formalise.T] = [(fmz, (dI',pI',mI'))];
    4.22 +"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : References.T) = (fmz, sp);
    4.23 +  val thy = ThyC.get_theory dI;
    4.24 +\<close> ML \<open>
    4.25 +  (*if*) mI = ["no_met"]; (*else*)
    4.26 +\<close> ML \<open>
    4.27 +dI = "empty_thy_id";
    4.28 +\<close> ML \<open>
    4.29 +pI = ["empty_probl_id"];
    4.30 +\<close> ML \<open>
    4.31 +mI = ["empty_meth_id"];
    4.32 +\<close> ML \<open>
    4.33 +\<close> ML \<open>
    4.34 +\<close> ML \<open>
    4.35 +\<close> ML \<open>
    4.36 +\<close> text \<open>
    4.37 +replaceFormula 1 "Simplify (2*a + 3*a)";
    4.38 +\<close> ML \<open>
    4.39 +\<close> ML \<open>
    4.40 +\<close> ML \<open>
    4.41 +\<close>
    4.42 +
    4.43 +section \<open>===== "Interpret/lucas-interpreter.sml" ==========================================\<close>
    4.44  ML \<open>
    4.45  \<close> ML \<open>
    4.46  \<close> ML \<open>