wneuper/isa: test/Tools/isac/OLDTESTS/script.sml@0d22a6bf1fc6

     1 (* tests for ME/script.sml

     2    WN.13.3.00

     4    WN050908 OLD FILE, MERGE WITH smltest/ME/script.sml

     6 use"systest/script.sml";

     7 use"script.sml";

     8 *)

    11 "         scripts: Variante 'funktional'               ";

    12 "############## Make_fun_by_new_variable ##############";

    13 "############## Make_fun_by_explicit ##############";

    14 "################ Solve_root_equation #################";

    15 "------- Notlocatable: Free_Solve -------";

    17 "  --- test100:  nxt_tac order------------------------------------ ";

    18 "  --- test100:  order 1 3 1 2 ----------------------------------- ";

    19 " --- test200: nxt_tac order ------------------------------------- ";

    20 " --- test200: order 3 1 1 2 --------------------------------- ";

    22 "  --- root-equation:  nxt_tac order------------------------------ ";

    23 "  --- root-equation:  1.norm_equation ------------------------------ ";

    24 (* --- test200: calculate -----------------------------------------*)

    25 "  --- check_elementwise ------------------------------ ";

    27 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    28 "  --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";

    30 "--------- from_prog ---------------------------------------------";

    31 "-----------------------------------------------------------------";

    37 " ################################################# 6.5.03";

    38 "         scripts: Variante 'funktional'            6.5.03";

    39 " ################################################# 6.5.03 ";

    41 val c = (the o (TermC.parse DiffApp.thy))

    42   "Program Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\

    43    \      (v_::real) (itv_::real set) (err_::bool) =          \

    44    \ (let e_e = (hd o (filterVar m_)) rs_;              \

    45    \      t_ = (if 1 < length_ rs_                            \

    46    \           then (SubProblem (Reals_s,[make,function],[no_met])\

    47    \                     [REAL m_, REAL v_v, BOOL_LIST rs_])\

    48    \           else (hd rs_));                                \

    49    \      (mx_::real) = SubProblem (Reals_s,[on_interval,max_of,function], \

    50    \                                [Isac,maximum_on_interval])\

    51    \                               [BOOL t_, REAL v_v, REAL_SET itv_]\

    52    \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values])   \

    53    \      [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_,     \

    54    \       BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";

    57 "################################################### 6.5.03";

    58 "############## Make_fun_by_new_variable ########### 6.5.03";

    59 "################################################### 6.5.03";

    61 val sc = (the o (TermC.parse DiffApp.thy)) (*start interpretieren*)

    62   "Program Make_fun_by_new_variable (f_::real) (v_::real)     \

    63    \      (eqs_::bool list) =                                 \

    64    \(let h_ = (hd o (filterVar f_)) eqs_;             \

    65    \     es_ = dropWhile (ident h_) eqs_;                    \

    66    \     vs_ = dropWhile (ident f_) (Vars h_);                \

    67    \     v_1 = nth_ 1 vs_;                                   \

    68    \     v_2 = nth_ 2 vs_;                                   \

    69    \     e_1 = (hd o (filterVar v_1)) es_;            \

    70    \     e_2 = (hd o (filterVar v_2)) es_;            \

    71    \  (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\

    72    \                    [BOOL e_1, REAL v_1]);\

    73    \  (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\

    74    \                    [BOOL e_2, REAL v_2])\

    75    \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";

    77 val ags = map (Thm.term_of o the o (TermC.parse DiffApp.thy))

    78   ["A::real", "alpha::real",

    79    "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"];

    80 val ll = [](*:loc_*);

    81 (* problem with exn PTREE + eval_to -------------------------

    82 "-------------- subproblem with empty formalizaton -------";

    83 val (mI1,m1) =

    84   ("Subproblem", tac2tac_ pt p

    85    (Subproblem (("Reals",["univar", "equation", "test"],

    86 		(""(*"ANDERN !!!!!!!*),"no_met")),[])));

    87 val (mI2,m2) = (mI1,m1);

    88 val (mI3,m3) =

    89   ("Substitute", tac2tac_ pt p

    90    (Substitute [("a", "#2*r*sin alpha"),("b", "#2*r*cos alpha")]));

    91 "------- same_tacpbl + eval_to -------";

    92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);

    93 loc_2str l1;

    94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)

    95 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1;

    96 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)

    98 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);

    99 loc_2str l2;

   100 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)

   101 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t2;

   102 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)

   104 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);

   105 loc_2str l3;

   106 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)

   107 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t3;

   108 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)

   111 "------- eq_tacIDs + eq_consts + eval_args -------";

   112 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];

   113 val eq_cons = filter (eq_consts m) eq_ids;

   114 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;

   115 "------- locate -------";

   118 "-------------- subproblem with formalizaton -------";

   119 val (mI,m) =

   120   ("Subproblem", tac2tac_ pt []

   121    (Subproblem (("Reals",["univar", "equation", "test"],

   122 		(""(*"ANDERN !!!!!!!*),"no_met")),

   123 	       ["a//#2=r*sin alpha", "a"])));

   124 "------- same_tacpbl + eval_to -------";

   127 "------- eq_tacIDs + eq_consts + eval_args -------";

   128 val eq_ids = eq_tacIDs [] sc (mI,m) [];

   129 val eq_cons = filter (eq_consts m) eq_ids;

   130 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;

   133 "------- locate -------";

   134 -------------------------------------------------------*)

   135 (* use"ME/script.sml";

   136    use"test-script.sml";

   137    *)

   141 "############## Make_fun_by_explicit ############## 6.5.03";

   142 "############## Make_fun_by_explicit ############## 6.5.03";

   143 "############## Make_fun_by_explicit ############## 6.5.03";

   144 val c = (the o (TermC.parse DiffApp.thy))

   145    "Program Make_fun_by_explicit (f_::real) (v_::real)         \

   146    \      (eqs_::bool list) =                                 \

   147    \ (let h_  = (hd o (filterVar f_)) eqs_;                   \

   148    \      e_1 = hd (dropWhile (ident h_) eqs_);               \

   149    \      vs_ = dropWhile (ident f_) (Vars h_);                \

   150    \      v_1 = hd (dropWhile (ident v_v) vs_);                \

   151    \      (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\

   152    \                          [BOOL e_1, REAL v_1])\

   153    \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";

   156 (*#####################################################--------11.5.02

   157 "################ Solve_root_equation #################";

   158 (*#####################################################*)

   159 val sc = (Thm.term_of o the o (TermC.parse Test.thy))

   160   "Program Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\

   161    \ (let e_e = Rewrite square_equation_left True eq_;     \

   162    \      e_e = Rewrite_Set Test_simplify False e_;          \

   163    \      e_e = Rewrite_Set rearrange_assoc False e_;          \

   164    \      e_e = Rewrite_Set isolate_root False e_;             \

   165    \      e_e = Rewrite_Set Test_simplify False e_;          \

   167    \      e_e = Rewrite square_equation_left True e_;        \

   168    \      e_e = Rewrite_Set Test_simplify False e_;          \

   170    \      e_e = Rewrite_Set norm_equation False e_;        \

   171    \      e_e = Rewrite_Set Test_simplify False e_;      \

   172    \      e_e = Rewrite_Set_Inst [(''bdv'',v_)] isolate_bdv False e_;\

   173    \      e_e = Rewrite_Set Test_simplify False e_e       \

   174    \ in [e_::bool])";

   175 val ags = map (Thm.term_of o the o (TermC.parse Test.thy))

   176   ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real", "#0"];

   177 val fmz =

   178   ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",

   179    "solveFor x", "errorBound (eps = #0)", "solutions v_i_"];

   180 ----------------------------------------------------------------11.5.02...*)

   183 (*################################# me raises exception with not-locatable

   184 "--------------------- Notlocatable: Free_Solve ---------------------";

   185 "--------------------- Notlocatable: Free_Solve ---------------------";

   186 "--------------------- Notlocatable: Free_Solve ---------------------";

   187 val fmz = [];

   188 val (dI',pI',mI') =

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

   190    ["Test", "sqrt-equ-test"]);

   191 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   192 val nxt = ("Model_Problem",

   193 	   Model_Problem ["sqroot-test", "univariate", "equation", "test"]);

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

   195 val nxt =

   196   ("Add_Given",

   197    Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");

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

   199 val nxt = ("Add_Given",Add_Given "solveFor x");

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

   201 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");

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

   203 val nxt = ("Add_Find",Add_Find "solutions v_i_");

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

   205 val nxt = ("Specify_Theory",Specify_Theory "Test");

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

   207 val nxt =

   208   ("Specify_Problem",Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);

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

   210 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]);

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

   213 "--- -1 ---";

   214 val nxt = ("Free_Solve",Free_Solve);

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

   217 "--- 0 ---";

   218 val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");

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

   220 (*me ("Begin_Trans" ////*)

   222 "--- 1 ---";

   223 val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", ""));

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

   226 "--- 2 ---";

   227 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

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

   230 "--- 3 ---";

   231 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

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

   233 if f = Form'

   234     (Test_Out.FormKF

   235        (~1,EdUndef,1,Nundef,

   236         "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"))

   237 then () else error "behaviour in root-expl. Free_Solve changed";

   238 writeln (pr_ctree pr_short pt);

   239 ---------------------------------me raises exception with not-locatable*)

   242 val d = Rule_Set.empty;

   244 "  --- test100:  nxt_tac order------------------------------------ ";

   245 "  --- test100:  nxt_tac order------------------------------------ ";

   247 val scr as (Prog sc) = Prog (((inst_abs Test.thy)

   248 				  o Thm.term_of o the o (TermC.parse thy))

   249  "Program Testeq (e_e::bool) =                                        \

   250    \(While (contains_root e_e) Do                                     \

   251    \((Try (Repeat (Rewrite rroot_square_inv))) #>    \

   252    \  (Try (Repeat (Rewrite square_equation_left))) #> \

   253    \  (Try (Repeat (Rewrite radd_0)))))\

   254    \ e_e            ");

   255 TermC.atomty sc;

   256 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],

   257 		     ["Test", "sqrt-equ-test"]);

   258 val c = [];

   259 val (p,_,_,_,_,pt) = CalcTreeTEST [([], (dI',pI',mI')))];

   260 val nxt = ("Specify_Theory",Specify_Theory "Test");

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

   262 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]); (*for asm in square_equation_left*)

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

   264 val p = ([1],Res):pos';

   265 val eq_ = (Thm.term_of o the o (TermC.parse thy))"e_::bool";

   267 val ct =   "0+(sqrt(sqrt(sqrt a)) \<up> 2) \<up> 2=0";

   268 val ve0_= TermC.parseNEW'' thy ct;

   269 val ets0=[([],(Tac_(Program.thy,"BS", "", ""),[(eq_,ve0_)],[(eq_,ve0_)],

   270 	       TermC.empty,TermC.empty,Safe)),

   271 	  ([],(User', [],                [],        TermC.empty, TermC.empty,Sundef))]:ets;

   272 val l0 = [];

   273 " --------------- 1. ---------------------------------------------";

   274 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test", ""))(TermC.str2term ct,[])Complete;

   275 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv"

   276 val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv", "")) (pt, p);

   277 *)

   280 val scr as (Prog sc) =

   281     Prog (((inst_abs Test.thy)  o Thm.term_of o the o (TermC.parse thy))

   282  "Program Testterm (g_::real) = (Calculate cancel g_)");

   283 (*

   284 val scr as (Prog sc) =

   285     Prog (((inst_abs Test.thy)  o Thm.term_of o the o (TermC.parse thy))

   286  "Program Testterm (g_::real) = (Calculate power g_)");

   287 val scr as (Prog sc) =

   288     Prog (((inst_abs Test.thy)  o Thm.term_of o the o (TermC.parse thy))

   289  "Program Testterm (g_::real) = (Calculate pow g_)");

   290 ..............................................................*)

   291 writeln

   292 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\

   293 \     (Repeat (Calculate cancel g_)) Or                     \n\

   294 \     (Repeat (Calculate power g_)) Or                        \n\

   295 \%%%%%%%%%%%%%%%%%%%%%--- \<up>  \<up> --- conflicts with Isa-types \n\

   296 \%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";

   299 "--------- from_prog ---------------------------------------------";

   300 "--------- from_prog ---------------------------------------------";

   301 "--------- from_prog ---------------------------------------------";

   302 (* mv test/../script.sml: -----> *)

   303 "----------- fun from_prog ---------------------------------------"

author	wneuper <walther.neuper@jku.at>
	Tue, 20 Jul 2021 14:37:56 +0200
changeset 60339	0d22a6bf1fc6
parent 60242	73ee61385493
child 60340	0ee698b0a703
permissions	-rw-r--r--