1.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Thu May 30 12:39:13 2019 +0200
1.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Sat Jun 01 11:09:19 2019 +0200
1.3 @@ -6,70 +6,21 @@
1.4 "-----------------------------------------------------------------";
1.5 "table of contents -----------------------------------------------";
1.6 "-----------------------------------------------------------------";
1.7 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.8 "-------- test the same called by interSteps norm_Poly -----------";
1.9 "-------- test the same called by interSteps norm_Rational -------";
1.10 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
1.11 -"-------- how to stepwise construct Scripts -------";(*TODO remove -- partial_function is easier*)
1.12 "-------- distinguish input to Model -----------------------------------------";
1.13 "-------- fun subpbl, fun pblterm --------------------------------------------";
1.14 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
1.15 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
1.16 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
1.17 "-------- fun op @@ ----------------------------------------------------------";
1.18 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
1.19 -"-------- Handle Var from parsing by partial_function ------------------------";
1.20 -"-------- Compare program terms: from old parsing | from partial_function ----";
1.21 "-------- fun get_fun_id -----------------------------------------------------";
1.22 "-------- fun rules2scr_Rls --------------------------------------------------";
1.23 "-----------------------------------------------------------------------------";
1.24 "-----------------------------------------------------------------------------";
1.25 "-----------------------------------------------------------------------------";
1.26
1.27 -
1.28 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.29 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.30 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
1.31 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
1.32 -writeln(term2str auto_script);
1.33 -atomty auto_script;
1.34 -
1.35 -show_mets();
1.36 -val {scr = Prog parsed_script,...} = get_met ["Test","test_interSteps_1"];
1.37 -writeln(term2str parsed_script);
1.38 -atomty parsed_script;
1.39 -
1.40 -(*the structure of the auto-gen. script is interpreted correctly*)
1.41 -reset_states ();
1.42 -CalcTree
1.43 -[(["Term (b + a - b)",(*this is Schalk 299b*)
1.44 - "normalform N"],
1.45 - ("Poly",["polynomial","simplification"],
1.46 - ["Test","test_interSteps_1"]))];
1.47 -Iterator 1;
1.48 -moveActiveRoot 1;
1.49 -autoCalculate 1 CompleteCalcHead;
1.50 -
1.51 -fetchProposedTactic 1 (*..Apply_Method*);
1.52 -autoCalculate 1 (Step 1);
1.53 -getTactic 1 ([1], Frm) (*still empty*);
1.54 -
1.55 -fetchProposedTactic 1 (*discard_minus_*);
1.56 -autoCalculate 1 (Step 1);
1.57 -
1.58 -fetchProposedTactic 1 (*order_add_rls_*);
1.59 -autoCalculate 1 (Step 1);
1.60 -
1.61 -fetchProposedTactic 1 (*collect_numerals_*);
1.62 -autoCalculate 1 (Step 1);
1.63 -
1.64 -autoCalculate 1 CompleteCalc;
1.65 -
1.66 -val ((pt,p),_) = get_calc 1; show_pt pt;
1.67 -if existpt' ([1], Frm) pt then ()
1.68 -else error "scrtools.sml: test-script test_interSteps_1 doesnt work";
1.69 -
1.70 -
1.71 "-------- test the same called by interSteps norm_Poly -----------";
1.72 "-------- test the same called by interSteps norm_Poly -----------";
1.73 "-------- test the same called by interSteps norm_Poly -----------";
1.74 @@ -225,57 +176,11 @@
1.75 if contain_bdv (get_rules rls) then ()
1.76 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
1.77
1.78 -two_scr_arg auto_script;
1.79 +if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
1.80 +then () else error "formal_args of auto-gen.script changed";
1.81 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
1.82 (str2term "someTermWithBdv");
1.83
1.84 -"-------- how to stepwise construct Scripts ----------------------";
1.85 -"-------- how to stepwise construct Scripts ----------------------";
1.86 -"-------- how to stepwise construct Scripts ----------------------";
1.87 -val thy = @{theory "Rational"};
1.88 -(*no trailing _*)
1.89 -val p1 = parse thy (
1.90 -"Script SimplifyScript (t_t::real) = " ^
1.91 -" (Rewrite_Set discard_minus False " ^
1.92 -" t_t)");
1.93 -
1.94 -(*required (): (Rewrite_Set discard_minus False)*)
1.95 -val p2 = parse thy (
1.96 -"Script SimplifyScript (t_t::real) = " ^
1.97 -" (Rewrite_Set discard_minus False " ^
1.98 -" t_t)");
1.99 -
1.100 -val p3 = parse thy (
1.101 -"Script SimplifyScript (t_t::real) = " ^
1.102 -" ((Rewrite_Set discard_minus False) " ^
1.103 -" t_t)");
1.104 -
1.105 -val p4 = parse thy (
1.106 -"Script SimplifyScript (t_t::real) = " ^
1.107 -" ((Rewrite_Set discard_minus False) " ^
1.108 -" t_t)");
1.109 -
1.110 -val p5 = parse thy (
1.111 -"Script SimplifyScript (t_t::real) = " ^
1.112 -" ((Try (Rewrite_Set discard_minus False) " ^
1.113 -" Try (Rewrite_Set discard_parentheses False)) " ^
1.114 -" t_t)");
1.115 -
1.116 -val p6 = parse thy (
1.117 -"Script SimplifyScript (t_t::real) = " ^
1.118 -" ((Try (Rewrite_Set discard_minus False) @@ " ^
1.119 -" Try (Rewrite_Set rat_mult_poly False) @@ " ^
1.120 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
1.121 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
1.122 -" (Repeat " ^
1.123 -" ((Try (Rewrite_Set add_fractions_p_rls False) @@ " ^
1.124 -" Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
1.125 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
1.126 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
1.127 -" Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
1.128 -" Try (Rewrite_Set discard_parentheses False)) " ^
1.129 -" t_t)"
1.130 -);
1.131
1.132 "-------- distinguish input to Model -----------------------------------------";
1.133 "-------- distinguish input to Model -----------------------------------------";
1.134 @@ -420,189 +325,12 @@
1.135 "Try (Repeat (Rewrite ''risolate_root_div'' False))"
1.136 then () else error "fun @@ changed"
1.137
1.138 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
1.139 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
1.140 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
1.141 -(* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)
1.142 -val prog_str_'''' = (* string constants: the intermediate version before partial_function *)
1.143 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.144 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
1.145 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
1.146 - " (L_L::bool list) = " ^
1.147 - " (SubProblem (''TestX'', " ^
1.148 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
1.149 - " [''Test'', ''solve_linear'']) " ^
1.150 - " [BOOL e_e, REAL v_v]) " ^
1.151 - " in Check_elementwise L_L {(v_v::real). Assumptions}) ";
1.152 -val prog_str_Free = (* Free varibles: the version up to now *)
1.153 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.154 - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.155 - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.156 - " (L_L::bool list) = " ^
1.157 - " (SubProblem (TestX, " ^
1.158 - " [LINEAR, univariate, equation, test], " ^
1.159 - " [Test, solve_linear]) " ^
1.160 - " [BOOL e_e, REAL v_v]) " ^
1.161 - " in Check_elementwise L_L {(v_v::real). Assumptions}) "
1.162 -
1.163 -(* term with string constants *)
1.164 -val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
1.165 -val Const ("Test.Solve'_root'_equation", _) $
1.166 - Free ("e_e", _) $ Free ("v_v", _) $
1.167 - (Const ("HOL.Let", _) $
1.168 - (Const ("Script.Seq", _) $
1.169 - (Const ("Script.Try", _) $
1.170 - (Const ("Script.Rewrite'_Set", _) $
1.171 - norm_equation_'''' $ Const ("HOL.False", _))) $
1.172 - (Const ("Script.Try", _) $
1.173 - (Const ("Script.Rewrite'_Set", _) $
1.174 - Test_simplify_'''' $ Const ("HOL.False", _))) $
1.175 - Free ("e_e", _)) $
1.176 - Abs ("e_e", _,
1.177 - Const ("HOL.Let", _) $
1.178 - (Const ("Script.SubProblem", _) $
1.179 - (Const ("Product_Type.Pair", _) $ TestX_'''' $
1.180 - (Const ("Product_Type.Pair", _) $
1.181 - pblkey_'''' $ metkey_'''')) $
1.182 - args) $
1.183 - Abs ("L_L", _,
1.184 - Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_''''
1.185 -;
1.186 -(* term with Free varibles *)
1.187 -val prog_Free = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_Free
1.188 -val Const ("Test.Solve'_root'_equation", _) $
1.189 - Free ("e_e", _) $ Free ("v_v", _) $
1.190 - (Const ("HOL.Let", _) $
1.191 - (Const ("Script.Seq", _) $
1.192 - (Const ("Script.Try", _) $
1.193 - (Const ("Script.Rewrite'_Set", _) $
1.194 - norm_equation_Free $ Const ("HOL.False", _))) $
1.195 - (Const ("Script.Try", _) $
1.196 - (Const ("Script.Rewrite'_Set", _) $
1.197 - Test_simplify_Free $ Const ("HOL.False", _))) $
1.198 - Free ("e_e", _)) $
1.199 - Abs ("e_e", _,
1.200 - Const ("HOL.Let", _) $
1.201 - (Const ("Script.SubProblem", _) $
1.202 - (Const ("Product_Type.Pair", _) $ TestX_Free $
1.203 - (Const ("Product_Type.Pair", _) $
1.204 - pblkey_Free $ metkey_Free)) $
1.205 - args) $
1.206 - Abs ("L_L", _,
1.207 - Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_Free
1.208 -;
1.209 -(* compare term with string constants and term with Free varibles *)
1.210 -if HOLogic.dest_string norm_equation_'''' = "norm_equation" then () else error "dest_string 1";
1.211 -(* --------------------- string constants = Free varibles *)
1.212 -if HOLogic.dest_string norm_equation_'''' = Term.term_name norm_equation_Free then () else error "";
1.213 -if HOLogic.dest_string Test_simplify_'''' = Term.term_name Test_simplify_Free then () else error "";
1.214 -if HOLogic.dest_string TestX_'''' = Term.term_name TestX_Free then () else error "dest_string 2";
1.215 -
1.216 -if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
1.217 - ["LINEAR", "univariate", "equation", "test"] then () else error "dest_string 3";
1.218 -(* --------------------- string constants = Free varibles *)
1.219 -if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
1.220 - (pblkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 4";
1.221 -if (metkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
1.222 - (metkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 5";
1.223 -
1.224 -"-------- Handle Var from parsing by partial_function ------------------------";
1.225 -"-------- Handle Var from parsing by partial_function ------------------------";
1.226 -"-------- Handle Var from parsing by partial_function ------------------------";
1.227 -(* (1) parsing proprietary as used up to now *)
1.228 -val prog_str_'''' =
1.229 - "xxx e_e = (let e_e = (Rewrite_Set ''yyy'' False) e_e in [e_e])"
1.230 -val prog_'''' = ((*TermC.inst_abs o*) Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
1.231 -(*Output: val prog_'''' = ... $ (Const ("HOL.Let", "bool... )... $ Free ("e_e", "bool")) $ ...*)
1.232 -
1.233 -(* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)
1.234 -val prog_part = (HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps}
1.235 -(*Output: val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
1.236 -;
1.237 -Logic.unvarify_global: term -> term
1.238 -;
1.239 -val prog_part = (Logic.unvarify_global o HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps};
1.240 -(*val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
1.241 -
1.242 -(* (3) compare (1)..(2) *)
1.243 -if prog_'''' = prog_part then () else error "appl of Logic.unvarify_global changed"
1.244 -
1.245 -"-------- Compare program terms: from old parsing | from partial_function ----";
1.246 -"-------- Compare program terms: from old parsing | from partial_function ----";
1.247 -"-------- Compare program terms: from old parsing | from partial_function ----";
1.248 -(* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)
1.249 -
1.250 -(* (1) parsing proprietary as used up to now *)
1.251 -val prog_str_'''' = (* string constants: the intermediate version before partial_function *)
1.252 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.253 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
1.254 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
1.255 - " (L_L::bool list) = " ^
1.256 - " (SubProblem (''TestX'', " ^
1.257 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
1.258 - " [''Test'', ''solve_linear'']) " ^
1.259 - " [BOOL e_e, REAL v_v]) " ^
1.260 - " in Check_elementwise L_L {(v_v::real). Assumptions}) ";
1.261 -val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
1.262 -
1.263 -(* body_of ---> src/../scrtools.sml for test with old parsing *)
1.264 -fun body_of_'''' (_ $ body) = body
1.265 - | body_of_'''' t = raise TERM ("body_of", [t])
1.266 -
1.267 -val body_'''' = body_of_'''' prog_'''';
1.268 -term2str body_''''; (* with TermC.inst_abs:
1.269 - "let e_ea =\n (Try (Rewrite_Set ''norm_equation'' False) @@\n Try (Rewrite_Set ''Test_simplify'' False))\n e_e;\n L_La =\n SubProblem\n (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}":
1.270 -------------------------> e_e; Free ("e_e", "bool"))
1.271 -*)
1.272 -
1.273 -(* formal_args in src/../scrtools.sml*)
1.274 -fun formal_args_'''' scr = (fst o split_last o snd o strip_comb) scr;
1.275 -
1.276 -val args_'''' = formal_args_'''' prog_'''';
1.277 -case args_'''' of [Free ("e_e", _), Free ("v_v", _)] => ()
1.278 -| _ => error "formal_args";
1.279 -
1.280 -(* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)
1.281 -val prog_part = Thm.prop_of @{thm minisubpbl.simps}
1.282 -
1.283 -(* body_of ---> src/../scrtools.sml BEFORE above, new body_of *)
1.284 -fun body_of_part t = (t
1.285 - |> HOLogic.dest_Trueprop
1.286 - |> HOLogic.dest_eq
1.287 - |> snd
1.288 - |> Logic.unvarify_global
1.289 - |> TermC.inst_abs)
1.290 -handle TERM _ => raise TERM ("body_of", [t])
1.291 -
1.292 -val body_part = body_of_part prog_part;
1.293 -term2str body_part; (* with TermC.inst_abs, without:
1.294 - "let e_ea =\n (Try (Rewrite_Set ''norm_equation'' False) @@\n Try (Rewrite_Set ''Test_simplify'' False))\n ?e_e;\n L_La =\n SubProblem\n (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL ?v_v]\nin Check_elementwise L_L {v_v. Assumptions}":
1.295 -------------------------> ?e_e; Var (("e_e", 0), "bool"))
1.296 -*)
1.297 -
1.298 -(* formal_args ---> src/../scrtools.sml BEFORE old formal_args *)
1.299 -fun formal_args_part prog = (prog
1.300 - |> HOLogic.dest_Trueprop
1.301 - |> HOLogic.dest_eq
1.302 - |> fst
1.303 - |> Logic.unvarify_global
1.304 - |> strip_comb
1.305 - |> snd
1.306 -)
1.307 -handle TERM _ => raise TERM ("formal_args", [t])
1.308 -
1.309 -val args_part = formal_args_part prog_part;
1.310 -
1.311 -(* (3) compare (1)..(2) *)
1.312 -if body_'''' = body_part then () else error "body_of changed";
1.313 -if args_'''' = args_part then () else error "formal_args changed"
1.314 -
1.315 "-------- fun get_fun_id -----------------------------------------------------";
1.316 "-------- fun get_fun_id -----------------------------------------------------";
1.317 "-------- fun get_fun_id -----------------------------------------------------";
1.318 (* fun_id is nested into arguments, compare ... *)
1.319 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
1.320 - (((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) =
1.321 + (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
1.322 Thm.prop_of @{thm biegelinie.simps};
1.323 (* ... to: *)
1.324 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
1.325 @@ -613,12 +341,14 @@
1.326 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
1.327 nested $ _) =
1.328 Thm.prop_of @{thm biegelinie.simps};
1.329 -val (((((Const ("Biegelinie.biegelinie", _) $
1.330 - Var (("l", 0), _)) $
1.331 - Var (("q", 0), _)) $
1.332 - Var (("v", 0), _)) $
1.333 - Var (("b", 0), _)) $
1.334 - Var (("s", 0), _)) = nested;
1.335 +val (Const ("Biegelinie.biegelinie", _) $
1.336 + Var (("l", 0), _) $
1.337 + Var (("q", 0), _) $
1.338 + Var (("v", 0), _) $
1.339 + Var (("b", 0), _) $
1.340 + Var (("s", 0), _) $
1.341 + Var (("vs", 0), _) $
1.342 + Var (("id_abl", 0), _)) = nested;
1.343 strip_comb nested;
1.344 (*val it =
1.345 (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
1.346 @@ -627,10 +357,10 @@
1.347 Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
1.348 term * term list*)
1.349
1.350 -case get_fun_id (Thm.prop_of @{thm biegelinie.simps}) of
1.351 +case get_fun_id (prep_program @{thm biegelinie.simps}) of
1.352 ("Biegelinie.biegelinie", _) => ()
1.353 | _ => error "get_fun_id changed";
1.354 -case get_fun_id (Thm.prop_of @{thm simplify.simps}) of
1.355 +case get_fun_id (prep_program @{thm simplify.simps}) of
1.356 ("PolyMinus.simplify", _) => ()
1.357 | _ => error "get_fun_id changed";
1.358