1.1 --- a/test/Tools/isac/BridgeJEdit/template.sml Tue Aug 15 12:22:49 2023 +0200
1.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Tue Aug 15 17:39:06 2023 +0200
1.3 @@ -61,8 +61,8 @@
1.4 (*+*) "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
1.5 (*+*)then () else error "final test of build I_Model.init_TEST FAILED";
1.6
1.7 - val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id; (*..MethodC ?*)
1.8 - val (_, preconds) = Pre_Conds.check ctxt where_rls where_ [(*TODO: I_Model.T_TEST*)] 0;
1.9 + val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id;
1.10 + val (_, preconds) = Pre_Conds.check_OLD ctxt where_rls where_ (model_patt, empty_i_model);
1.11
1.12 show ctxt preconds empty_i_model in_refs;
1.13 "~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =
2.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Aug 15 12:22:49 2023 +0200
2.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Aug 15 17:39:06 2023 +0200
2.3 @@ -542,18 +542,19 @@
2.4 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.5 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.6 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
2.7 +States.reset ();
2.8 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
2.9 ("Test", ["sqroot-test", "univariate", "equation", "test"],
2.10 ["Test", "squ-equ-test-subpbl1"]))];
2.11 Iterator 1;
2.12 moveActiveRoot 1;
2.13 - autoCalculate 1 CompleteCalcHead;
2.14 + autoCalculate 1 CompleteCalcHead;
2.15
2.16 val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
2.17 - meth, probl,
2.18 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
2.19 + meth, probl,
2.20 + spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
2.21 ["Test", "squ-equ-test-subpbl1"]),
2.22 - branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
2.23 + branch = TransitiveB, ostate = Ctree.Incomplete, ...}, []),
2.24 ([], Met)), []) = States.get_calc 1;
2.25 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
2.26 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
2.27 @@ -908,7 +909,7 @@
2.28 probl,
2.29 branch = TransitiveB,
2.30 origin,
2.31 - ostate = Incomplete,
2.32 + ostate = Ctree.Incomplete,
2.33 result},
2.34 []),
2.35 ([], Pbl)),
2.36 @@ -929,7 +930,7 @@
2.37 probl,
2.38 branch = TransitiveB,
2.39 origin,
2.40 - ostate = Incomplete,
2.41 + ostate = Ctree.Incomplete,
2.42 result},
2.43 []),
2.44 ([], Pbl)),
3.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Aug 15 12:22:49 2023 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Aug 15 17:39:06 2023 +0200
3.3 @@ -110,19 +110,19 @@
3.4 "----------- test matching problems --------------------------0---";
3.5 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
3.6 if M_Match.match_pbl fmz (Problem.from_store @{context} ["expanded", "univariate", "equation"]) =
3.7 - M_Match.Matches' {Find = [Correct "solutions L"],
3.8 + M_Match.Matches' {Find = [P_Model.Correct "solutions L"],
3.9 With = [],
3.10 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.11 - Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
3.12 - Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
3.13 + Given = [P_Model.Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", P_Model.Correct "solveFor x"],
3.14 + Where = [P_Model.Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
3.15 + P_Model.Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
3.16 Relate = []}
3.17 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
3.18
3.19 if M_Match.match_pbl fmz (Problem.from_store @{context} ["degree_2", "expanded", "univariate", "equation"]) =
3.20 - M_Match.Matches' {Find = [Correct "solutions L"],
3.21 + M_Match.Matches' {Find = [P_Model.Correct "solutions L"],
3.22 With = [],
3.23 - Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
3.24 - Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
3.25 + Given = [P_Model.Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", P_Model.Correct "solveFor x"],
3.26 + Where = [P_Model.Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
3.27 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
3.28 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
3.29
4.1 --- a/test/Tools/isac/Knowledge/simplify.sml Tue Aug 15 12:22:49 2023 +0200
4.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Tue Aug 15 17:39:06 2023 +0200
4.3 @@ -1,4 +1,4 @@
4.4 -(* Title: \<open>\<close>
4.5 +(* Title: Knowledge/simplify.sml
4.6 Author: Walther Neuper 061019
4.7 (c) due to copyright terms
4.8 *)
4.9 @@ -107,15 +107,12 @@
4.10 (** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) = ( *isa*)
4.11 (**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) = (*isa2*)
4.12 for_method ctxt oris (o_refs, refs) (pbl, met);
4.13 -"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
4.14 +"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met)) =
4.15 (oris, (o_refs, refs), (pbl, met));
4.16 val cmI = if mI = MethodC.id_empty then mI' else mI;
4.17 - val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
4.18 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
4.19
4.20 -(** ) val (preok as false, _) = Pre_Conds.check where_rls where_ pbl 0; ( *isa*)
4.21 -(**) val (preok as true, _) = Pre_Conds.check ctxt where_rls where_ pbl 0; (*isa2*)
4.22 - (*#### eval asms: "14 * x * y / (x * y) is_ratpolyexp = False" (*isa*)
4.23 - True ( *isa2*)
4.24 +(**) val (preok as true, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
4.25 (*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)
4.26 val ((pt,p),_) = States.get_calc 1;
4.27 Test_Tool.show_pt pt;
5.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Aug 15 12:22:49 2023 +0200
5.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Aug 15 17:39:06 2023 +0200
5.3 @@ -853,11 +853,11 @@
5.4 (*if*) p_ = Pos.Pbl (*else*);
5.5
5.6 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
5.7 -"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.8 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
5.9 = (ctxt, oris, (o_refs, refs), (pbl, met));
5.10 val cmI = if mI = MethodC.id_empty then mI' else mI;
5.11 - val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
5.12 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
5.13 + val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
5.14 + val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
5.15 val NONE =
5.16 (*case*) find_first (I_Model.is_error o #5) met (*of*);
5.17
6.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Aug 15 12:22:49 2023 +0200
6.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Aug 15 17:39:06 2023 +0200
6.3 @@ -72,6 +72,7 @@
6.4 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
6.5 SOME _ => false | NONE => true;
6.6 (*1*)val mis = (filter (notmem pbl)) pbt;
6.7 +
6.8 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
6.9 fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
6.10 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
6.11 @@ -80,16 +81,19 @@
6.12 val newitms = filter mem_vat news;
6.13 (*4*)val itms' = pbl @ newitms;
6.14
6.15 - val (pb, where_') =
6.16 - Pre_Conds.check ctxt where_rls where_ itms' mv;
6.17 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, pbl, (_)) =
6.18 - (ctxt, where_rls, where_, itms', mv);
6.19 - val env = Pre_Conds.environment pbl;
6.20 - val pres' = map (TermC.subst_atomic_all env) pres;
6.21 + val (pb, where_') = Pre_Conds.check_OLD ctxt where_rls where_
6.22 + (pbt, I_Model.OLD_to_TEST itms');
6.23 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
6.24 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms'));
6.25 + val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
6.26 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
6.27 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
6.28 + val full_subst = if env_eval = [] then pres_subst_other
6.29 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
6.30
6.31 -(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
6.32 +(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
6.33 (*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
6.34 -(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = pres'
6.35 +(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst
6.36
6.37 (*+*)val ctxt = Config.put rewrite_trace true ctxt;
6.38 val evals = map (
6.39 @@ -321,4 +325,4 @@
6.40 . . . . . . . . . . Rewrite_Set "Test_simplify",
6.41 ([2], Res), - 1 + x = 0
6.42 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
6.43 -*)
6.44 \ No newline at end of file
6.45 +*)
7.1 --- a/test/Tools/isac/Specify/refine.sml Tue Aug 15 12:22:49 2023 +0200
7.2 +++ b/test/Tools/isac/Specify/refine.sml Tue Aug 15 17:39:06 2023 +0200
7.3 @@ -368,7 +368,7 @@
7.4
7.5 (*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
7.6 (*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
7.7 -val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] = (**)
7.8 +val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =
7.9 refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
7.10 "~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
7.11 = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
7.12 @@ -408,7 +408,7 @@
7.13 val (_, env_model, (env_subst, env_eval)) =
7.14 of_max_variant model_patt i_model;
7.15 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
7.16 - val all_variants =
7.17 + val all_variants =
7.18 map (fn (_, variants, _, _, _) => variants) i_model
7.19 |> flat
7.20 |> distinct op =
7.21 @@ -452,7 +452,7 @@
7.22 (*+*)val false = all_lhs_atoms ts
7.23 (*-------------------- contine check_OLD -----------------------------------------------------*)
7.24
7.25 - val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
7.26 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
7.27
7.28 (*+*)if "[\"\n" ^
7.29 "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
7.30 @@ -471,7 +471,7 @@
7.31 (*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
7.32 (*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
7.33 val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =
7.34 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
7.35 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
7.36
7.37
7.38 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
8.1 --- a/test/Tools/isac/Specify/specify.sml Tue Aug 15 12:22:49 2023 +0200
8.2 +++ b/test/Tools/isac/Specify/specify.sml Tue Aug 15 17:39:06 2023 +0200
8.3 @@ -532,8 +532,8 @@
8.4 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
8.5 (oris, (o_refs, refs), (pbl, met));
8.6 val cmI = if mI = MethodC.id_empty then mI' else mI;
8.7 - val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
8.8 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
8.9 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
8.10 + val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
8.11 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
8.12 (*/------------------- check within find_next_step -----------------------------------------\*)
8.13 (*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
9.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Aug 15 12:22:49 2023 +0200
9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Aug 15 17:39:06 2023 +0200
9.3 @@ -289,14 +289,14 @@
9.4 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
9.5 ML_file "BridgeLibisabelle/interface.sml"
9.6
9.7 -(** ) (* evaluated in Build_Isac.thy already *)
9.8 +(**) (* evaluated in Build_Isac.thy already *)
9.9 ML_file "BridgeJEdit/e-collect.sml"
9.10 ML_file "BridgeJEdit/user-model.sml"
9.11 ML_file "BridgeJEdit/template.sml"
9.12 ML_file "BridgeJEdit/preliminary.sml"
9.13 ML_file "BridgeJEdit/calculation.sml"
9.14 ML_file "BridgeJEdit/vscode-example.sml"
9.15 -( **)
9.16 +(**)
9.17
9.18 ML_file "Knowledge/delete.sml"
9.19 ML_file "Knowledge/descript.sml"
10.1 --- a/test/Tools/isac/Test_Some.thy Tue Aug 15 12:22:49 2023 +0200
10.2 +++ b/test/Tools/isac/Test_Some.thy Tue Aug 15 17:39:06 2023 +0200
10.3 @@ -121,6 +121,15 @@
10.4 \<close>
10.5
10.6 section \<open>===================================================================================\<close>
10.7 +section \<open>===== simplify.sml ================================================================\<close>
10.8 +ML \<open>
10.9 +\<close> ML \<open>
10.10 +
10.11 +\<close> ML \<open>
10.12 +\<close> ML \<open>
10.13 +\<close>
10.14 +
10.15 +section \<open>===================================================================================\<close>
10.16 section \<open>===== Interpret/li-tool.sml =======================================================\<close>
10.17 ML \<open>
10.18 \<close> ML \<open>
11.1 --- a/test/Tools/isac/Test_Theory.thy Tue Aug 15 12:22:49 2023 +0200
11.2 +++ b/test/Tools/isac/Test_Theory.thy Tue Aug 15 17:39:06 2023 +0200
11.3 @@ -1349,20 +1349,26 @@
11.4 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
11.5 (*if*) p_ = Pos.Pbl (*else*);
11.6
11.7 +\<close> ML \<open>
11.8 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
11.9 -"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
11.10 +\<close> ML \<open>
11.11 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
11.12 = (ctxt, oris, (o_refs, refs), (pbl, met));
11.13 +\<close> ML \<open>
11.14 val cmI = if mI = MethodC.id_empty then mI' else mI;
11.15 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
11.16 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
11.17 + val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
11.18 val NONE =
11.19 (*case*) find_first (I_Model.is_error o #5) met (*of*);
11.20
11.21 +\<close> ML \<open>
11.22 (*case*)
11.23 Specify.item_to_add (ThyC.get_theory ctxt
11.24 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
11.25 +\<close> ML \<open>
11.26 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
11.27 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
11.28 +\<close> ML \<open>
11.29 (*\------------------- step into me Specify_Method -----------------------------------------//*)
11.30 val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
11.31
11.32 @@ -2250,11 +2256,11 @@
11.33 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
11.34 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
11.35 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
11.36 -(*overwrites NEW funs in Test_Theory ABOVE* )
11.37 +(*overwrites NEW funs in Test_Theory ABOVE*)
11.38 open Refine
11.39 open M_Match
11.40 open Pre_Conds
11.41 -( *overwrites NEW funs in Test_Theory ABOVE*)
11.42 +(*overwrites NEW funs in Test_Theory ABOVE*)
11.43 (*
11.44 refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;
11.45 this example was the demonstrator;
11.46 @@ -2275,31 +2281,22 @@
11.47 @{term "[c_3]::real list"},
11.48 @{term "[c_4]::real list"}] ),
11.49 (3, [1], "#Find", @{term "solution"}, [@{term "ss'''::bool list"}] )]
11.50 -\<close> ML \<open>
11.51 -(*ERROR exception Bind* )
11.52 -val ["normalise", "4x4", "LINEAR", "system"] =
11.53 - refine_ori' @{context} o_model ["LINEAR", "system"];
11.54 +;
11.55 val SOME ["normalise", "4x4", "LINEAR", "system"] =
11.56 -( *ERROR exception Bind*)
11.57 refine_ori @{context} o_model ["LINEAR", "system"];
11.58 \<close> ML \<open>
11.59 "~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =
11.60 (@{context}, o_model, ["LINEAR", "system"]);
11.61 -\<close> ML \<open>
11.62 -(*ERROR exception Bind* )
11.63 +
11.64 val opt as SOME ["system", "LINEAR", "4x4", "normalise"]
11.65 - =( *ERROR exception Bind*)
11.66 - app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
11.67 + = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
11.68 \<close> ML \<open>
11.69 (*
11.70 app_ptyp works strangely, parameter passing is awkward.
11.71 Present refin knows structure of Store.T, thus we bypass app_ptyp
11.72 -( **)
11.73 -\<close> ML \<open>
11.74 -
11.75 +*)
11.76 (*!*)val pblID = ["LINEAR", "system"];(**)
11.77 -(*isa* )val return_refin as SOME ["system", "LINEAR", "LINEAR"] = ( **)
11.78 -(*isa2*)val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
11.79 +val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
11.80 refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
11.81 \<close> ML \<open>
11.82 "~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
11.83 @@ -2307,84 +2304,57 @@
11.84 \<close> ML \<open>
11.85 val {where_rls, model, where_, ...} = py: Problem.T
11.86 val model = map (Model_Pattern.adapt_to_type ctxt) model
11.87 + val where_ = map (ParseC.adapt_term_to_type ctxt) where_;
11.88 +\<close> ML \<open>
11.89 + (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
11.90 +\<close> ML \<open>
11.91 +val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
11.92 +\<close> ML \<open>
11.93 +(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
11.94 +(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
11.95 +val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =
11.96 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
11.97 +\<close> ML \<open>
11.98 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
11.99 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
11.100 +\<close> ML \<open>
11.101 + val {where_rls, model, where_, ...} = py: Problem.T
11.102 + val model = map (Model_Pattern.adapt_to_type ctxt) model
11.103 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
11.104 \<close> ML \<open>
11.105 - (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
11.106 -\<close> ML \<open>
11.107 -val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
11.108 -\<close> ML \<open>
11.109 -(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
11.110 -(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
11.111 -(*isa* )val return_refin as NONE = ( **)
11.112 -(*isa2*)val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] = (**)
11.113 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
11.114 -\<close> ML \<open>
11.115 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
11.116 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
11.117 -\<close> ML \<open>
11.118 - val {where_rls, model, where_, ...} = py: Problem.T
11.119 - val model = map (Model_Pattern.adapt_to_type ctxt) model
11.120 - val where_ = map (ParseC.adapt_term_to_type ctxt) where_
11.121 -\<close> ML \<open>
11.122 -(*isa*) (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*else*);
11.123 -(*isa2*)(*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
11.124 -\<close> ML \<open>
11.125 -"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, oris, (pbt, where_)) =
11.126 - (ctxt, where_rls, ori, (model, where_));
11.127 -\<close> ML \<open>
11.128 -(*+*)val Rule_Def.Repeat
11.129 - {asm_rls = Rule_Set.Empty, calc = [], errpatts = [], id = "prls_4x4_linear_system", preconds = [], prog_rls = Rule_Set.Empty, program = Empty_Prog, rew_ord = ("dummy_ord", _), rules =
11.130 - [Thm ("LENGTH_CONS", _), Thm ("LENGTH_NIL", _), Eval ("Groups.plus_class.plus", _), Eval ("HOL.eq", _)]}
11.131 - = where_rls
11.132 +(*+*)val (**)true(** )false( **) = (*if*)
11.133 + M_Match.match_oris ctxt where_rls o_model (model, where_);
11.134 +"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
11.135 + (ctxt, where_rls, o_model, (model, where_));
11.136 + val i_model = (flat o (map (chk1_ model_pattern))) o_model;
11.137 +
11.138 (*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"
11.139 - = oris |> O_Model.to_string @{context}
11.140 -(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
11.141 - = pbt |> Model_Pattern.to_string @{context}
11.142 -(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
11.143 -\<close> ML \<open>
11.144 -\<close> ML \<open>
11.145 -(*old*)val itms = (flat o (map (M_Match.chk1_ pbt))) oris;
11.146 -(*+isa2*)val 3 = length itms
11.147 -\<close> ML \<open>
11.148 -(*old*)val mvat = I_Model.variables itms;
11.149 -(*+isa2*)val "[[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2], [c, c_2, c_3, c_4], ss''']"
11.150 - = mvat |> UnparseC.terms @{context}
11.151 -\<close> ML \<open>
11.152 -(*old*)val complete = M_Match.chk1_mis mvat itms pbt;
11.153 -(*+isa2*)val true = complete
11.154 -\<close> ML \<open>
11.155 -(*old*)val (pb as true, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;
11.156 -\<close> ML \<open>
11.157 -\<close> ML \<open>
11.158 -(*----------------------vvvvvvvvv---------------------------------------------------------------*)
11.159 -"~~~~~ fun match_oris , NEWNEWNEW args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
11.160 - (ctxt, where_rls, ori, (model, where_));
11.161 -\<close> ML \<open>
11.162 -(*new*)val i_model = (flat o (map (M_Match.chk1_ pbt))) o_model;
11.163 -\<close> ML \<open>
11.164 + = o_model |> O_Model.to_string @{context};
11.165 (*+*)if "[\n" ^
11.166 "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^
11.167 "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^
11.168 "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"
11.169 = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";
11.170 \<close> ML \<open>
11.171 -(*new*)val (pb as true, (** )_( **)where_'(**)) = Pre_Conds.check_OLD ctxt where_rls where_
11.172 - (model_pattern, I_Model.OLD_to_TEST i_model);
11.173 +(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
11.174 + = model_pattern |> Model_Pattern.to_string @{context}
11.175 +(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
11.176 +
11.177 + val mvat = I_Model.variables i_model;
11.178 + val complete = chk1_mis mvat i_model model_pattern;
11.179 +
11.180 + val (pb as true, (** )_( **)where_'(**)) =
11.181 + Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
11.182 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
11.183 + (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));
11.184 \<close> ML \<open>
11.185 (*+*)val [(true, xxx), (true, yyy)] = where_'
11.186 \<close> ML \<open>
11.187 (*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"
11.188 = where_' |> map #2 |> UnparseC.terms @{context}
11.189 -\<close> ML \<open>
11.190 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
11.191 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms));
11.192 -\<close> ML \<open>
11.193 +
11.194 val (_, env_model, (env_subst, env_eval)) =
11.195 - of_max_variant model_patt i_model
11.196 -\<close> ML \<open>
11.197 -(*eqsy*)val "[\"\n(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]" = env_model |> Subst.to_string @{context} (*should \<rightarrow> []*)
11.198 -(*eqsy*)val "[]" = env_subst |> Subst.to_string @{context} (* \<rightarrow> []*)
11.199 -\<close> ML \<open>
11.200 + of_max_variant model_patt i_model;
11.201 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
11.202 \<close> ML \<open>
11.203 val all_variants =
11.204 @@ -2404,7 +2374,7 @@
11.205 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
11.206 \<close> ML \<open>
11.207 val subst_eval_list =
11.208 - make_envs_preconds equal_givens
11.209 + make_envs_preconds equal_givens;
11.210 \<close> ML \<open>
11.211 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
11.212 \<close> ML \<open>
11.213 @@ -2421,12 +2391,21 @@
11.214 (*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"
11.215 = ts |> UnparseC.terms @{context}
11.216 \<close> ML \<open>
11.217 + val ts = if Model_Pattern.is_list_descr descr
11.218 + then if TermC.is_list (hd ts)
11.219 + then ts |> map TermC.isalist2list |> flat
11.220 + else ts
11.221 + else ts
11.222 +
11.223 +(*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
11.224 + = ts |> UnparseC.terms @{context};
11.225 +\<close> ML \<open>
11.226 (*if*) Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
11.227 \<close> ML \<open>
11.228 (*+*)val false = all_lhs_atoms ts
11.229 (*-------------------- contine check_OLD -----------------------------------------------------*)
11.230
11.231 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
11.232 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
11.233 \<close> ML \<open>
11.234 (*+*)if "[\"\n" ^
11.235 "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
11.236 @@ -2444,20 +2423,13 @@
11.237 \<close> ML \<open>
11.238 val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
11.239 \<close> ML \<open>
11.240 -\<close> ML \<open>
11.241 -\<close> ML \<open>
11.242 -\<close> ML \<open>
11.243 val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))
11.244 \<close> ML \<open>
11.245 (*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
11.246 (*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
11.247 -(*isa*)val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] = (**)
11.248 -(*isa2* )val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] = ( **)
11.249 +val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =
11.250 refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
11.251 \<close> ML \<open>
11.252 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
11.253 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
11.254 -\<close> ML \<open>
11.255 \<close> ML \<open>
11.256 \<close> ML \<open>
11.257 \<close>