1.1 --- a/src/Tools/isac/Build_Isac.thy Thu Dec 08 10:16:40 2022 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Dec 08 10:33:27 2022 +0100
1.3 @@ -179,6 +179,7 @@
1.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
1.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
1.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
1.7 +(*ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"*)
1.8 ML \<open>
1.9 \<close> ML \<open>
1.10 \<close> ML \<open>
1.11 @@ -189,7 +190,6 @@
1.12 \<close> ML \<open>
1.13 \<close>
1.14 (*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
1.15 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
1.16 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
1.17 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
1.18 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml"
2.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Thu Dec 08 10:16:40 2022 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,45 +0,0 @@
2.4 -signature SUB_PROBLEM =
2.5 -sig
2.6 - val tac_from_prog: Ctree.ctree -> term -> Tactic.input * Tactic.T
2.7 -end
2.8 -
2.9 -(**)
2.10 -structure Sub_Problem(**): SUB_PROBLEM(**) =
2.11 -struct
2.12 -(**)
2.13 -
2.14 -fun tac_from_prog pt (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
2.15 - let
2.16 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
2.17 - val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);
2.18 - val ctxt = Proof_Context.init_global thy (*TODO: use ctxt from pt *)
2.19 - val ags = TermC.isalist2list ags';
2.20 - val (pI, pors, mI) =
2.21 - if mI = ["no_met"]
2.22 - then
2.23 - let
2.24 - val pors = (M_Match.arguments thy ((#model o (Problem.from_store ctxt)) pI) ags): O_Model.T
2.25 - handle ERROR "actual args do not match formal args"
2.26 - => (M_Match.arguments_msg ctxt pI stac ags (*raise exn*);[]);
2.27 - val pI' = Refine.refine_ori' ctxt pors pI;
2.28 - in (pI', pors (* refinement over models with diff.prec only *),
2.29 - (hd o #solve_mets o Problem.from_store ctxt) pI') end
2.30 - else (pI, (M_Match.arguments thy ((#model o Problem.from_store ctxt) pI) ags)
2.31 - handle ERROR "actual args do not match formal args"
2.32 - => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI);
2.33 - val (fmz_, vals) = O_Model.values' pors;
2.34 - val {cas, model, thy, ...} = Problem.from_store ctxt pI
2.35 - val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
2.36 - val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))
2.37 - val ctxt = ContextC.initialise dI vals
2.38 - val hdl =
2.39 - case cas of
2.40 - NONE => Auto_Prog.pblterm dI pI
2.41 - | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
2.42 - val f = Auto_Prog.subpbl (strip_thy dI) pI
2.43 - in
2.44 - (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
2.45 - end
2.46 - | tac_from_prog _ t = raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term t)
2.47 -
2.48 -(**)end(**)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/Specify/sub-problem.sml Thu Dec 08 10:33:27 2022 +0100
3.3 @@ -0,0 +1,52 @@
3.4 +signature SUB_PROBLEM =
3.5 +sig
3.6 + val tac_from_prog: Ctree.state -> term -> Tactic.input * Tactic.T
3.7 + val common_sub_thy: theory * theory -> theory
3.8 +end
3.9 +
3.10 +(**)
3.11 +structure Sub_Problem(**): SUB_PROBLEM(**) =
3.12 +struct
3.13 +(**)
3.14 +
3.15 +fun common_sub_thy (thy1, thy2) =
3.16 + if Context.subthy (thy1, thy2) then thy2
3.17 + else if Context.subthy (thy2, thy1) then thy1
3.18 + else Know_Store.get_ref_last_thy ()
3.19 +
3.20 +fun tac_from_prog (pt, p) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
3.21 + let
3.22 + val (dI, pI, mI) = Prog_Tac.dest_spec spec'
3.23 + val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
3.24 + val init_ctxt = Proof_Context.init_global thy
3.25 + val ags = TermC.isalist2list ags';
3.26 + val (pI, pors, mI) =
3.27 + if mI = ["no_met"]
3.28 + then
3.29 + let
3.30 + val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
3.31 + handle ERROR "actual args do not match formal args"
3.32 + => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
3.33 + val pI' = Refine.refine_ori' init_ctxt pors pI;
3.34 + in (pI', pors (* refinement over models with diff.prec only *),
3.35 + (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
3.36 + else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
3.37 + handle ERROR "actual args do not match formal args"
3.38 + => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
3.39 + val (fmz_, vals) = O_Model.values' init_ctxt pors;
3.40 + val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
3.41 + val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
3.42 + val dI = Context.theory_name
3.43 + (common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
3.44 + val ctxt = ContextC.initialise init_ctxt vals
3.45 + val hdl =
3.46 + case cas of
3.47 + NONE => Auto_Prog.pblterm dI pI
3.48 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
3.49 + val f = Auto_Prog.subpbl (strip_thy dI) pI
3.50 + in
3.51 + (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
3.52 + end
3.53 + | tac_from_prog _ t = raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term t)
3.54 +
3.55 +(**)end(**)
4.1 --- a/test/Tools/isac/Interpret/sub-problem.sml Thu Dec 08 10:16:40 2022 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,56 +0,0 @@
4.4 -(* Title: "Interpret/sub-problem.sml"
4.5 - Author: Walther Neuper
4.6 - (c) due to copyright terms
4.7 -*)
4.8 -
4.9 -"-----------------------------------------------------------------------------------------------";
4.10 -"table of contents -----------------------------------------------------------------------------";
4.11 -"-----------------------------------------------------------------------------------------------";
4.12 -"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.13 -"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.14 -"-----------------------------------------------------------------------------------------------";
4.15 -"-----------------------------------------------------------------------------------------------";
4.16 -"-----------------------------------------------------------------------------------------------";
4.17 -
4.18 -
4.19 -"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.20 -"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.21 -"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.22 -(* compare biegelinie-4.sml *)
4.23 -val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
4.24 -Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.25 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
4.26 - "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
4.27 -("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
4.28 -
4.29 - val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
4.30 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
4.31 - (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
4.32 - |> me';
4.33 -
4.34 -
4.35 -"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.36 -"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.37 -"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.38 -
4.39 -val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.40 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
4.41 - "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"];
4.42 -val refs =
4.43 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
4.44 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, refs)];
4.45 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
4.46 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Traegerlaenge L"*)
4.47 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
4.48 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Find "Biegelinie y"*)
4.49 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
4.50 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
4.51 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Biegelinie"*)
4.52 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["Biegelinien"]*)
4.53 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
4.54 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
4.55 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
4.56 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
4.57 -(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"]*)
4.58 - (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
4.59 -(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Tools/isac/Specify/sub-problem.sml Thu Dec 08 10:33:27 2022 +0100
5.3 @@ -0,0 +1,85 @@
5.4 +(* Title: "Interpret/sub-problem.sml"
5.5 + Author: Walther Neuper
5.6 + (c) due to copyright terms
5.7 +*)
5.8 +
5.9 +"-----------------------------------------------------------------------------------------------";
5.10 +"table of contents -----------------------------------------------------------------------------";
5.11 +"-----------------------------------------------------------------------------------------------";
5.12 +"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
5.13 +"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
5.14 +"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";
5.15 +"-----------------------------------------------------------------------------------------------";
5.16 +"-----------------------------------------------------------------------------------------------";
5.17 +"-----------------------------------------------------------------------------------------------";
5.18 +
5.19 +
5.20 +"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
5.21 +"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
5.22 +"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
5.23 +(* compare biegelinie-4.sml *)
5.24 +val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
5.25 +Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.26 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
5.27 + "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
5.28 +("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
5.29 +
5.30 + val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
5.31 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
5.32 + (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
5.33 + |> me';
5.34 +
5.35 +
5.36 +"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
5.37 +"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
5.38 +"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
5.39 +
5.40 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.41 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
5.42 + "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"];
5.43 +val refs =
5.44 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
5.45 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, refs)];
5.46 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
5.47 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Traegerlaenge L"*)
5.48 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
5.49 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Find "Biegelinie y"*)
5.50 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
5.51 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
5.52 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Biegelinie"*)
5.53 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["Biegelinien"]*)
5.54 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.55 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.56 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
5.57 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
5.58 +(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"]*)
5.59 + (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
5.60 +(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
5.61 +
5.62 +
5.63 +"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";
5.64 +"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";
5.65 +"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";
5.66 +val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Inverse_Z_Transform});
5.67 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Inverse_Z_Transform"
5.68 +then () else error "common_sub_thy 1";
5.69 +
5.70 +val (thy1, thy2) = (@{theory Inverse_Z_Transform}, @{theory Partial_Fractions});
5.71 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Inverse_Z_Transform"
5.72 +then () else error "common_sub_thy 2";
5.73 +
5.74 +val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq});
5.75 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = Context.theory_name @{theory}
5.76 +then () else error "common_sub_thy 3";
5.77 +
5.78 +val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge});
5.79 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Isac_Knowledge"
5.80 +then () else error "common_sub_thy 4";
5.81 +
5.82 +val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions});
5.83 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = Context.theory_name @{theory}
5.84 +then () else error "common_sub_thy 5";
5.85 +
5.86 +val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions});
5.87 +if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Isac_Knowledge"
5.88 +then () else error "common_sub_thy 6";
6.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Dec 08 10:16:40 2022 +0100
6.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Dec 08 10:33:27 2022 +0100
6.3 @@ -278,10 +278,10 @@
6.4 ML_file "Specify/cas-command.sml"
6.5 ML_file "Specify/p-spec.sml"
6.6 ML_file "Specify/specify.sml"
6.7 + ML_file "Specify/sub-problem.sml"
6.8 ML_file "Specify/step-specify.sml"
6.9
6.10 ML_file "Interpret/istate.sml"
6.11 - ML_file "Interpret/sub-problem.sml"
6.12 ML_file "Interpret/error-pattern.sml"
6.13 ML_file "Interpret/li-tool.sml"
6.14 ML_file "Interpret/lucas-interpreter.sml"