1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 24 17:01:02 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Mar 25 09:17:05 2020 +0100
1.3 @@ -495,69 +495,60 @@
1.4 | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
1.5 | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
1.6
1.7 -
1.8 +
1.9 (*** locate an input formula within a program ***)
1.10
1.11 datatype input_term_result = Found_Step of Calc.T | Not_Derivable
1.12
1.13 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
1.14 -(*OLD*)let
1.15 - (*OLD*) val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
1.16 - (*OLD*) PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.17 - (*OLD*) | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
1.18 - (*OLD*) val {ppc, ...} = Specify.get_met mI;
1.19 - (*OLD*) val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
1.20 - (*OLD*) val itms = Specify.hack_until_review_Specify_1 mI itms
1.21 - (*OLD*) val thy = Celem.assoc_thy (get_obj g_domID pt p);
1.22 - (*OLD*) val srls = LItool.get_simplifier (pt, pos)
1.23 - (*OLD*) val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
1.24 - (*OLD*) (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
1.25 - (*OLD*) | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
1.26 - (*OLD*) val ini = LItool.init_form thy prog env;
1.27 - (*OLD*)in
1.28 - (*OLD*) case ini of
1.29 - (*OLD*) SOME t =>
1.30 - (*OLD*) let
1.31 - (*OLD*) val pos = start_new_level pos
1.32 - (*OLD*) val tac_ = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
1.33 - (*OLD*) val (pos, c, _, pt) = Generate.generate1 tac_ (is, ctxt) (pt, pos) (* implicit Take *)
1.34 - (*OLD*) in
1.35 - (*OLD*) ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))
1.36 - (*OLD*) end
1.37 - (*OLD*) | NONE =>
1.38 -(*OLD*) let
1.39 -(*NEW* ) val (tac', ist', ctxt') =
1.40 -(*NEW*) case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
1.41 -(*NEW*) Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
1.42 -(*NEW*) | _ => raise ERROR ("LI.by_tactic..Apply_Method " ^ strs2str' mI)
1.43 -(*NEW*) in
1.44 -(*NEW*) case tac' of
1.45 -(*NEW*) Tactic.Take' t =>
1.46 -(*NEW*) let
1.47 -(*NEW*) val pos = start_new_level pos
1.48 -(*NEW*) val tac_ = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
1.49 -(*NEW*) val (pos, c, _, pt) = Generate.generate1 tac_ (ist', ctxt') (pt, pos) (* explicit Take *)
1.50 -(*NEW*) in
1.51 -(*NEW*) ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))
1.52 -(*NEW*) end
1.53 -(*NEW*) | tac as Tactic.Subproblem' (_, _, headline, _, _, _) =>
1.54 -(*NEW*) let
1.55 -(*NEW*) val pos = start_new_level pos
1.56 -(*NEW*) val tac_ = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
1.57 -(*NEW*) val (pos, c, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, pos) (* Subproblem *)
1.58 -(*NEW*) (**)
1.59 -(*NEW*) in
1.60 -(*NEW*) ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (ist', ctxt')))], c, (pt, pos)))
1.61 -(*NEW*) end
1.62 -(*NEW*) | tac =>
1.63 -(*NEW*) raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
1.64 -(*NEW*) end
1.65 -( *OLD*) val pt = update_env pt (fst pos) (SOME (is, ctxt))
1.66 -(*OLD*) val (_, (tacis, c, ptp)) = do_next (pt, pos)
1.67 -(*OLD*) in ("ok", (tacis @ [(Tactic.Apply_Method mI,
1.68 -(*OLD*) Tactic.Apply_Method' (mI, NONE, e_istate, ctxt), (pos, (is, ctxt)))], c, ptp))
1.69 -(*OLD*) end
1.70 -(*OLD*)end
1.71 + let
1.72 + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
1.73 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.74 + | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
1.75 + val {ppc, ...} = Specify.get_met mI;
1.76 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
1.77 + val itms = Specify.hack_until_review_Specify_1 mI itms
1.78 + val srls = LItool.get_simplifier (pt, pos)
1.79 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
1.80 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
1.81 + | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
1.82 + val ini = LItool.init_form (Celem.assoc_thy (get_obj g_domID pt p)) prog env;
1.83 + val pos = start_new_level pos
1.84 + in
1.85 + case ini of
1.86 + SOME t =>
1.87 + let (* implicit Take *)
1.88 + val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
1.89 + val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos)
1.90 + in
1.91 + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
1.92 + end
1.93 + | NONE =>
1.94 + let
1.95 + val (tac', ist', ctxt') =
1.96 + case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
1.97 + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
1.98 + | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \<rightarrow> " ^ strs2str' mI)
1.99 + in
1.100 + case tac' of
1.101 + Tactic.Take' t =>
1.102 + let (* explicit Take *)
1.103 + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
1.104 + val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos)
1.105 + in
1.106 + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
1.107 + end
1.108 + | add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
1.109 + let (* Subproblem *)
1.110 + val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
1.111 + val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos)
1.112 + in
1.113 + ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
1.114 + end
1.115 + | tac =>
1.116 + raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
1.117 + end
1.118 + end
1.119 | by_tactic (Tactic.Check_Postcond' (pI, _)) _ (pt, pos as (p, _)) =
1.120 let
1.121 val (ist, ctxt) = get_loc pt pos
1.122 @@ -595,12 +586,12 @@
1.123 end
1.124 end
1.125 | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
1.126 - | by_tactic tac_ is (pt, pos) =
1.127 + | by_tactic tac_ ic (pt, pos) =
1.128 let
1.129 val pos = next_in_prog' pos
1.130 - val (pos', c, _, pt) = Generate.generate1 tac_ is (pt, pos);
1.131 + val (pos', c, _, pt) = Generate.generate1 tac_ ic (pt, pos);
1.132 in
1.133 - ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')))
1.134 + ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, ic))], c, (pt, pos')))
1.135 end
1.136 (*find_next_step from program, by_tactic will update Ctree*)
1.137 and do_next (ptp as (pt, pos as (p, p_))) =
2.1 --- a/src/Tools/isac/Interpret/step-solve.sml Tue Mar 24 17:01:02 2020 +0100
2.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Mar 25 09:17:05 2020 +0100
2.3 @@ -17,55 +17,10 @@
2.4 open Ctree;
2.5 open Pos
2.6
2.7 -(*NEW* )fun by_tactic (tac as Tactic.Apply_Method' _) (ptp as (pt, p)) =
2.8 -(*NEW*) LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
2.9 -( *OLD*)fun by_tactic (m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
2.10 -(*OLD*)let
2.11 - (*OLD*) val itms = case get_obj I pt p of
2.12 - (*OLD*) PblObj {meth=itms, ...} => itms
2.13 - (*OLD*) | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
2.14 - (*OLD*) val thy = Celem.assoc_thy (get_obj g_domID pt p);
2.15 - (*OLD*) val srls = LItool.get_simplifier (pt, pos)
2.16 - (*OLD*) val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
2.17 - (*OLD*) (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
2.18 - (*OLD*) | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
2.19 - (*OLD*) val ini = LItool.init_form thy sc env;
2.20 - (*OLD*)in
2.21 - (*OLD*) case ini of
2.22 - (*OLD*) SOME t =>
2.23 - (*OLD*) let
2.24 - (*OLD*) val pos = start_new_level pos
2.25 - (*OLD*) val tac_ = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
2.26 - (*OLD*) val (pos ,c, _, pt) = Generate.generate1 tac_ (is, ctxt) (pt, pos)(*implicit Take*);
2.27 - (*OLD*) in
2.28 - (*OLD*) ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))
2.29 - (*OLD*) end
2.30 - (*OLD*) | NONE =>
2.31 -(*OLD*) let
2.32 -(*OLD*) val (m', is', ctxt') =
2.33 -(*OLD*) case LI.find_next_step sc (pt, (lev_dn p, Res)) is ctxt of
2.34 -(*OLD*) LI.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
2.35 -(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Apply_Method " ^ strs2str' mI)
2.36 -(*OLD*) in
2.37 -(*OLD*) case LI.locate_input_tactic sc (pt, (lev_dn p, Res)) is' ctxt' m' of
2.38 -(*OLD*) LI.Safe_Step (istate, ctxt, tac) =>
2.39 -(*OLD*) let
2.40 -(*OLD*) val (p'', _, _,pt') =
2.41 -(*OLD*) Generate.generate1 tac (istate, ctxt) (pt, ((lev_on o lev_dn) p, Pbl));
2.42 -(*OLD*) in
2.43 -(*OLD*) ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
2.44 -(*OLD*) [(*ctree NOT cut*)], (pt', p'')))
2.45 -(*OLD*) end
2.46 -(*OLD*) | _ => (* NotLocatable, but applicable_in from the beginning *)
2.47 -(*OLD*) let
2.48 -(*OLD*) val (p, ps, _, pt) =
2.49 -(*OLD*) Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (lev_dn p, Frm) pt;
2.50 -(*OLD*) in
2.51 -(*OLD*) ("not-found-in-script",([(Tactic.input_from_T m, m, (pos, (is, ctxt)))], ps, (pt, p)))
2.52 -(*OLD*) end
2.53 -(*OLD*) end
2.54 -(*OLD*)end
2.55 -(*OLD*)
2.56 +fun by_tactic (tac as Tactic.Apply_Method' _) (ptp as (pt, p)) =
2.57 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
2.58 + | by_tactic (tac as Tactic.Check_Postcond' _) ptp =
2.59 + LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp
2.60 | by_tactic (Tactic.Free_Solve') (pt, po as (p, _)) =
2.61 let
2.62 val p' = lev_dn_ (p, Res);
2.63 @@ -73,8 +28,6 @@
2.64 in
2.65 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
2.66 end
2.67 - | by_tactic (tac as Tactic.Check_Postcond' _) ptp =
2.68 - LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp
2.69 | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))
2.70 | by_tactic (Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
2.71 let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
3.1 --- a/src/Tools/isac/MathEngBasic/tactic-def.sml Tue Mar 24 17:01:02 2020 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/tactic-def.sml Wed Mar 25 09:17:05 2020 +0100
3.3 @@ -12,14 +12,13 @@
3.4 datatype T =
3.5 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
3.6 | Add_Relation' of Rule.cterm' * Model.itm list
3.7 - | Apply_Assumption' of term list * term
3.8 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
3.9
3.10 | Begin_Sequ' | Begin_Trans' of term
3.11 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
3.12 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
3.13 | End_Sequ' | End_Trans' of Selem.result
3.14 - | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
3.15 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
3.16
3.17 | CAScmd' of term
3.18 | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
3.19 @@ -58,7 +57,7 @@
3.20 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
3.21 | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
3.22 | Tac_ of theory * string * string * string
3.23 - | Take' of term | Take_Inst' of term
3.24 + | Take' of term
3.25 val string_of : T -> string
3.26
3.27 datatype input =
3.28 @@ -243,18 +242,19 @@
3.29 datatype T =
3.30 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
3.31 | Add_Relation' of Rule.cterm' * Model.itm list
3.32 - | Apply_Assumption' of term list * term
3.33 - | Apply_Method' of
3.34 - Celem.metID * (* key for KEStore *)
3.35 - term option * (* the first formula of Calc.T *)
3.36 - Istate_Def.T * (* for the newly started program *)
3.37 - Proof.context (* for the newly started program *)
3.38 + | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
3.39 + * tactic Apply_Method metID
3.40 + * formula term *)
3.41 + Celem.metID * (* key for KEStore *)
3.42 + term option * (* the first formula of Calc.T. TODO: rm option *)
3.43 + Istate_Def.T * (* for the newly started program *)
3.44 + Proof.context (* for the newly started program *)
3.45 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
3.46 | Begin_Sequ' | Begin_Trans' of term
3.47 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
3.48 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
3.49 | End_Sequ' | End_Trans' of Selem.result
3.50 - | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
3.51 + | End_Ruleset' of term | End_Intersect' of term | End_Proof''
3.52 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
3.53 | CAScmd' of term
3.54 | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
3.55 @@ -275,15 +275,16 @@
3.56 | Free_Solve'
3.57
3.58 | Init_Proof' of Rule.cterm' list * Celem.spec
3.59 - | Model_Problem' of Celem.pblID *
3.60 + | Model_Problem' of (* first step in specifying *)
3.61 + Celem.pblID * (* key into KEStore *)
3.62 Model.itm list * (* the 'untouched' pbl *)
3.63 Model.itm list (* the casually completed met *)
3.64 | Or_to_List' of term * term
3.65 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
3.66 | Refine_Tacitly' of
3.67 - Celem.pblID * (* input*)
3.68 + Celem.pblID * (* input *)
3.69 Celem.pblID * (* the refined from applicable_in *)
3.70 - Rule.domID * (* from new pbt?! filled in specify *)
3.71 + Rule.domID * (* from new pbt?! filled in specify *)
3.72 Celem.metID * (* from new pbt?! filled in specify *)
3.73 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
3.74 | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
3.75 @@ -311,7 +312,7 @@
3.76 term * (* to be substituted into *)
3.77 term (* resulting from the substitution *)
3.78 | Tac_ of theory * string * string * string
3.79 - | Take' of term | Take_Inst' of term
3.80 + | Take' of term
3.81
3.82 fun string_of ma = case ma of
3.83 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
3.84 @@ -350,13 +351,10 @@
3.85 | Derive' rls => "Derive' " ^ Rule.id_rls rls
3.86 | Calculate' _ => "Calculate' "
3.87 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
3.88 - | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
3.89
3.90 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
3.91 - | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
3.92 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
3.93 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
3.94 - | End_Subproblem' _ => "End_Subproblem'"
3.95 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
3.96
3.97 | Empty_Tac_ => "Empty_Tac_"
4.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Tue Mar 24 17:01:02 2020 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Mar 25 09:17:05 2020 +0100
4.3 @@ -95,7 +95,7 @@
4.4
4.5 ML \<open>
4.6 if eq_set op = (Rule.terms2strs (Ctree.get_assumptions_ pt p),
4.7 - ["matches (?a = ?b) (-1 + x = 0)"])
4.8 + ["matches (?a = ?b) (-1 + x = 0)", "precond_rootmet x"])
4.9 then () else error "All_Ctx: asms after start interpretation of SubProblem";
4.10 \<close>
4.11
5.1 --- a/test/Tools/isac/Interpret/step-solve.sml Tue Mar 24 17:01:02 2020 +0100
5.2 +++ b/test/Tools/isac/Interpret/step-solve.sml Wed Mar 25 09:17:05 2020 +0100
5.3 @@ -7,29 +7,99 @@
5.4 "table of contents -----------------------------------------------------------------------------";
5.5 "-----------------------------------------------------------------------------------------------";
5.6 "-----------------------------------------------------------------------------------------------";
5.7 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
5.8 +"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
5.9 +"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
5.10 "-----------------------------------------------------------------------------------------------";
5.11 "-----------------------------------------------------------------------------------------------";
5.12 "-----------------------------------------------------------------------------------------------";
5.13
5.14 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
5.15 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
5.16 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
5.17 +"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
5.18 +"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
5.19 +"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
5.20 +(*cp fom..*)
5.21 +"----------- me method [diff,integration] ---------------";
5.22 val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"];
5.23 val spec = ("Integrate", ["integrate","function"], ["diff","integration"]);
5.24 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
5.25 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Given "functionTerm (x ^^^ 2 + 1)"*)
5.26 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Given "integrateBy x"*)
5.27 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Find "Integrate.antiDerivative FF"*)
5.28 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Theory "Integrate"*)
5.29 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Problem ["integrate", "function"]*)
5.30 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Method ["diff", "integration"]*)
5.31 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Apply_Method ["diff", "integration"]*)
5.32
5.33 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];
5.34 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
5.35 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Integrate"*)
5.36 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["integrate", "function"]*)
5.37 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Method ["diff", "integration"]*)
5.38 -(*[1], Frm*)val (_, (_(*[(tac1, _, _), (tac2, _, _)]*), _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["diff", "integration"]
5.39 - Take "Integral x ^^^ 2 + 1 D x"*)
5.40 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "integration")*)
5.41 -(*[], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Check_Postcond ["integrate", "function"]*)
5.42 -(*[], Und*)val (_, ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>*)
5.43 +(*+*)case nxt of (Apply_Method ["diff", "integration"]) => ()
5.44 +(*+*) | _ => error "integrate.sml -- me method [diff,integration] -- spec";
5.45 +
5.46 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "integration")*)
5.47 +(*/--------- step into Apply_Method ----------------------------------------------------------\*)
5.48 +(*\--------- step into Apply_Method ----------------------------------------------------------/*)
5.49 +
5.50 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_Postcond ["integrate", "function"]*)
5.51 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>End_Proof'*)
5.52
5.53 (*/--------- final test ----------------------------------------------------------------------\*)
5.54 val (res, asm) = (get_obj g_result pt (fst p));
5.55 if term2str res = "c + x + 1 / 3 * x ^^^ 3" then ()
5.56 -else error "Apply_Method with initial Take CHANGED";
5.57 +else error "Apply_Method with explicit Take CHANGED";
5.58 +
5.59 +
5.60 +"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
5.61 +"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
5.62 +"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
5.63 +(*cp from biegelinie-4..*)
5.64 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
5.65 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
5.66 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
5.67 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
5.68 + "AbleitungBiegelinie dy"];
5.69 +val spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
5.70 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
5.71 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
5.72 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
5.73 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
5.74 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
5.75 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
5.76 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
5.77 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
5.78 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.79 +(*----------- 10 -----------*)
5.80 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "GleichungsVariablen [[], c_2, c_3, c_4]"*)
5.81 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy*)
5.82 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
5.83 +
5.84 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*nxt = Model_Problem*)
5.85 +(*/--------- step into Apply_Method ----------------------------------------------------------\*)
5.86 +(*\--------- step into Apply_Method ----------------------------------------------------------/*)
5.87 +
5.88 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
5.89 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.90 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Find "Funktionen funs'''"*)
5.91 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
5.92 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
5.93 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
5.94 +(*----------- 20 -----------*)
5.95 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';
5.96 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Apply_Method ["Biegelinien", "ausBelastung"]*)
5.97 +(*/--------- step into Apply_Method of Subproblem --------------------------------------------\*)
5.98 +(*\--------- step into Apply_Method of Subproblem --------------------------------------------/*)
5.99 +
5.100 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.101 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.102 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.103 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.104 +(*----------- 30 -----------*)
5.105 +
5.106 +(*/--------- final test ----------------------------------------------------------------------\*)
5.107 +if p = ([1, 3], Pbl)
5.108 +then
5.109 + case f of PpcKF (Problem [],
5.110 + {Find = [Correct "antiDerivativeName Q"],
5.111 + Given = [Correct "functionTerm (- q_0)", Correct "integrateBy x"],
5.112 + Relate = [], Where = [], With = []}) => ()
5.113 + | _ =>
5.114 + (case nxt of
5.115 + Specify_Theory "Biegelinie" => ()
5.116 + | _ => error "CHANGED 1")
5.117 +else error "CHANGED 2"
6.1 --- a/test/Tools/isac/Test_Code/test-code.sml Tue Mar 24 17:01:02 2020 +0100
6.2 +++ b/test/Tools/isac/Test_Code/test-code.sml Wed Mar 25 09:17:05 2020 +0100
6.3 @@ -46,7 +46,7 @@
6.4 (*[], Res*)val ((pt, p), nxt, t) = me_trace (pt, p) nxt trace_ist_ctxt;(*End_Proof'*)
6.5
6.6 if p = ([], Res) andalso f2str t = "[x = 1]" andalso
6.7 -(get_ctxt pt p |> get_assumptions |> terms2str)
6.8 - = "[\"matches (?a = ?b) (-1 + x = 0)\",\"x = 1\",\"precond_rootmet x\"]"
6.9 + eq_set op = (get_ctxt pt p |> get_assumptions |> map term2str,
6.10 + ["precond_rootmet x", "matches (?a = ?b) (-1 + x = 0)", "x = 1"])
6.11 then case nxt of End_Proof' => () | _ => error "fun me_trace all Minisubpbl CHANGED 1"
6.12 else error "fun me_trace all Minisubpbl CHANGED 2";