1.1 --- a/src/Tools/isac/CalcElements/contextC.sml Wed Nov 27 18:47:26 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Fri Nov 29 15:22:29 2019 +0100
1.3 @@ -180,9 +180,9 @@
1.4 structure ContextC(**) : CONTEXT_C(**) =
1.5 struct
1.6
1.7 -val e_ctxt = Proof_Context.init_global @{theory "HOL"};
1.8 +val e_ctxt = Proof_Context.init_global @{theory "Pure"};
1.9 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
1.10 -fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "HOL"});
1.11 +fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
1.12 fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx)
1.13
1.14 (* in Subproblem take respective actual arguments from program *)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 27 18:47:26 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Nov 29 15:22:29 2019 +0100
2.3 @@ -29,9 +29,7 @@
2.4 datatype next_tactic_result =
2.5 NStep of Ctree.state * Istate.T * Proof.context * tactic
2.6 | Helpless | End_Program
2.7 -(*val determine_next_tactic :
2.8 - Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *)
2.9 - val determine_next_tactic: Ctree.state -> Rule.program -> Istate.T * Proof.context
2.10 + val determine_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
2.11 -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe)
2.12
2.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.14 @@ -474,7 +472,7 @@
2.15 | scan_to_tactic2 _ _ = raise ERROR "scan_to_tactic2: uncovered pattern";
2.16
2.17 (*decide for the next applicable Prog_Tac*)
2.18 -fun determine_next_tactic (ptp as(pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, ctxt) =
2.19 +fun determine_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt =
2.20 (case scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) of
2.21 Term_Val2 v => (* program finished *)
2.22 (case par_pbl_det pt p of
2.23 @@ -491,7 +489,7 @@
2.24 (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
2.25 | Accept_Tac2 (m', (ist as {act_arg, ...})) =>
2.26 (m', (Pstate ist, ctxt), (act_arg, Telem.Safe))) (* found next tac *)
2.27 - | determine_next_tactic _ _ (is, _) =
2.28 + | determine_next_tactic _ _ is _ =
2.29 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
2.30
2.31
2.32 @@ -503,7 +501,7 @@
2.33
2.34 (* FIXME.WN050821 compare fun solve ... fun begin_end_prog
2.35 begin_end_prog (Apply_Method' vvv FIXME: get args in applicable_in *)
2.36 -fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) (ist, ctxt) (pt, pos as (p, _)) =
2.37 +fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
2.38 let
2.39 val {ppc, ...} = Specify.get_met mI;
2.40 val (itms, oris, probl) = case get_obj I pt p of
2.41 @@ -556,13 +554,12 @@
2.42 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
2.43 | _ => get_assumptions_ pt (p, p_))
2.44 val metID = get_obj g_metID pt pp;
2.45 - val {srls = srls, scr = sc, ...} = Specify.get_met metID;
2.46 - val (loc, pst, ctxt) = case get_loc pt (p, p_) of
2.47 - loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
2.48 + val {scr = sc, ...} = Specify.get_met metID;
2.49 + val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
2.50 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
2.51 val thy' = get_obj g_domID pt pp;
2.52 val thy = Celem.assoc_thy thy';
2.53 - val (_, _, (scval, _)) = determine_next_tactic (pt, (p, p_)) sc loc;
2.54 + val (_, _, (scval, _)) = determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt;
2.55 in
2.56 if pp = []
2.57 then
2.58 @@ -605,8 +602,8 @@
2.59 else
2.60 let
2.61 val thy' = get_obj g_domID pt (par_pblobj pt p);
2.62 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
2.63 - val (tac_, is, (t, _)) = determine_next_tactic (pt, pos) sc is;
2.64 + val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
2.65 + val (tac_, is, (t, _)) = determine_next_tactic sc (pt, pos) ist ctxt;
2.66 (* TODO here ^^^ return finished/helpless/ok ?*)
2.67 in case tac_ of
2.68 Tactic.End_Detail' _ =>
3.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Nov 27 18:47:26 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Fri Nov 29 15:22:29 2019 +0100
3.3 @@ -147,12 +147,13 @@
3.4 fun path_down_form (p, fa) {env, path, eval, act_arg, or, finish, assoc, ...} =
3.5 {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
3.6 or = or, finish = finish, assoc = assoc}
3.7 -fun path_up' path = drop_last path
3.8 +fun path_up' [] = raise ERROR "path_up' []"
3.9 + | path_up' path = drop_last path
3.10 fun path_up {env, path, eval, form_arg, act_arg, or, finish, assoc} =
3.11 - {env = env, path = drop_last path, eval = eval, form_arg = form_arg, act_arg = act_arg,
3.12 + {env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
3.13 or = or, finish = finish, assoc = assoc}
3.14 fun path_up_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
3.15 - {env = env, path = (drop_last path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
3.16 + {env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
3.17 or = or, finish = finish, assoc = assoc}
3.18
3.19 fun set_form f {env, path, eval, act_arg, or, finish, assoc, ...} =
4.1 --- a/src/Tools/isac/MathEngine/solve.sml Wed Nov 27 18:47:26 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngine/solve.sml Fri Nov 29 15:22:29 2019 +0100
4.3 @@ -138,7 +138,7 @@
4.4 | NONE =>
4.5 let
4.6 val (m', (is', ctxt'), _) = (* re-design: should not be necessary *)
4.7 - LucinNEW.determine_next_tactic (pt, (p, Res)) sc (is, ctxt);
4.8 + LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt;
4.9 in
4.10 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
4.11 LucinNEW.Safe_Step (istate, ctxt, tac) =>
4.12 @@ -177,14 +177,13 @@
4.13 | _ => get_assumptions_ pt (p,p_))
4.14 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
4.15 val metID = get_obj g_metID pt pp;
4.16 - val {srls = srls, scr = sc, ...} = Specify.get_met metID;
4.17 - val (loc, pst, ctxt) = case get_loc pt (p, p_) of
4.18 - loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
4.19 + val {scr = sc, ...} = Specify.get_met metID;
4.20 + val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
4.21 | _ => error "solve Check_Postcond: uncovered case get_loc"
4.22
4.23 val thy' = get_obj g_domID pt pp;
4.24 val thy = Celem.assoc_thy thy';
4.25 - val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (pt, (p, p_)) sc loc;
4.26 + val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt;
4.27 (* Telem.safe should go on to Check_Postcond' vvvvv *)
4.28 in
4.29 if pp = []
5.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 27 18:47:26 2019 +0100
5.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Nov 29 15:22:29 2019 +0100
5.3 @@ -59,7 +59,7 @@
5.4
5.5 val NONE = (*case*) ini (*of*);
5.6 val (m', (is', ctxt'), _) =
5.7 - LucinNEW.determine_next_tactic (pt, (p, Res)) sc (is, ctxt);
5.8 + LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt;
5.9 (*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, false)";
5.10 val Safe_Step (_, _, Take' _) = (*case*)
5.11 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
6.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Nov 27 18:47:26 2019 +0100
6.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Fri Nov 29 15:22:29 2019 +0100
6.3 @@ -166,7 +166,7 @@
6.4 val ini = Lucin.init_form thy sc env;
6.5 val p = lev_dn p;
6.6 val NONE = (*case*) ini (*of*);
6.7 - val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
6.8 + val (m', (is', ctxt'), _) = determine_next_tactic sc (pt, (p, Res)) is ctxt;
6.9 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
6.10 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
6.11 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
7.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Nov 27 18:47:26 2019 +0100
7.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri Nov 29 15:22:29 2019 +0100
7.3 @@ -316,7 +316,7 @@
7.4 go_scan_up2 thy ptp scr E l ay a v;
7.5 scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
7.6 go_scan_up2 thy ptp sc E l Skip_ a v;
7.7 -determine_next_tactic (thy',srls) (pt,pos) sc is;
7.8 +determine_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
7.9 do_solve_step (pt,ip);
7.10 step p ((pt, e_pos'),[]);
7.11 *)
8.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 27 18:47:26 2019 +0100
8.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri Nov 29 15:22:29 2019 +0100
8.3 @@ -381,8 +381,8 @@
8.4 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
8.5 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
8.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
8.7 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
8.8 -val (tac_,is,(t,_)) = determine_next_tactic (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
8.9 +val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
8.10 +val (tac_,is,(t,_)) = determine_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
8.11 case tac_ of Or_to_List' _ => ()
8.12 | _ => error "Or_to_List broken ?"
8.13
8.14 @@ -485,8 +485,8 @@
8.15 "~~~~~ fun do_solve_step , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
8.16 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
8.17 val thy' = get_obj g_domID pt (par_pblobj pt p);
8.18 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
8.19 - val (tac_,is,(t,_)) = determine_next_tactic (pt,pos) sc is;
8.20 + val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
8.21 + val (tac_,is,(t,_)) = determine_next_tactic sc (pt,pos) ist ctxt;
8.22 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
8.23
8.24 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
9.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Nov 27 18:47:26 2019 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Nov 29 15:22:29 2019 +0100
9.3 @@ -101,12 +101,12 @@
9.4 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
9.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);
9.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.7 - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
9.8 + val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
9.9
9.10 val (_, _, _) =
9.11 - determine_next_tactic (pt, pos) sc is;
9.12 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
9.13 - = ((pt, pos), sc, is);
9.14 + determine_next_tactic sc (pt, pos) ist ctxt;
9.15 +"~~~~~ fun determine_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
9.16 + = (sc, (pt, pos), ist, ctxt);
9.17
9.18 val Accept_Tac2 (Rewrite_Set' _, _) = (*case*)
9.19 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
9.20 @@ -155,12 +155,12 @@
9.21 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
9.22 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
9.23 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.24 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
9.25 + val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
9.26
9.27 val (_, _, _) =
9.28 - determine_next_tactic (pt, pos) (Rule.Prog prog) is;
9.29 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as (pt, p)), sc, (Istate.Pstate ist, _))
9.30 - = ((pt, pos), prog, is);
9.31 + determine_next_tactic sc (pt, pos) ist ctxt;
9.32 +"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
9.33 + = (sc, (pt, pos), ist, ctxt);
9.34
9.35 val Accept_Tac2 (_, _) = (*case*)
9.36 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
9.37 @@ -168,43 +168,43 @@
9.38 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
9.39 (*if*) 0 = length path (*else*);
9.40
9.41 - go_scan_up2 (sc, cct) (trans_scan_up2 ist |> set_appy Skip_);
9.42 -"~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.43 + go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_);
9.44 +"~~~~~ fun go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.45 = ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
9.46 (*if*) 1 < length path (*then*);
9.47
9.48 scan_up2 yyy (ist |> path_up) (go_up path prog);
9.49 -"~~~~~ fun scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ ))
9.50 +"~~~~~ and scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ ))
9.51 = (yyy, (ist |> path_up), (go_up path prog));
9.52
9.53 go_scan_up2 yyy (ist |> set_appy Skip_);
9.54 -"~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.55 +"~~~~~ fun go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.56 = (yyy, (ist |> set_appy Skip_));
9.57 (*if*) 1 < length path (*then*);
9.58
9.59 - scan_up2 yyy (ist |> path_up) (go_up path sc);
9.60 -"~~~~~ fun scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
9.61 - = (yyy, (ist |> path_up), (go_up path sc));
9.62 + scan_up2 yyy (ist |> path_up) (go_up path prog);
9.63 +"~~~~~ and scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
9.64 + = (yyy, (ist |> path_up), (go_up path prog));
9.65
9.66 go_scan_up2 yyy ist;
9.67 "~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.68 = (yyy, ist);
9.69 (*if*) 1 < length path (*then*);
9.70
9.71 - scan_up2 yyy (ist |> path_up) (go_up path sc);
9.72 + scan_up2 yyy (ist |> path_up) (go_up path prog);
9.73 "~~~~~ fun scan_up2 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
9.74 - = (yyy, (ist |> path_up), (go_up path sc));
9.75 + = (yyy, (ist |> path_up), (go_up path prog));
9.76
9.77 go_scan_up2 yyy ist;
9.78 "~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
9.79 = (yyy, ist);
9.80 (*if*) 1 < length path (*then*);
9.81
9.82 - scan_up2 yyy (ist |> path_up) (go_up path sc);
9.83 + scan_up2 yyy (ist |> path_up) (go_up path prog);
9.84 "~~~~~ fun scan_up2 , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
9.85 - = (yyy, (ist |> path_up), (go_up path sc));
9.86 + = (yyy, (ist |> path_up), (go_up path prog));
9.87 (*if*) finish = Napp_ (*else*);
9.88 - val (i, body) = check_Let_up ist sc;
9.89 + val (i, body) = check_Let_up ist prog;
9.90
9.91 (*case*) scan_dn2 xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
9.92 "~~~~~ fun scan_dn2 , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))
9.93 @@ -241,4 +241,4 @@
9.94 | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
9.95 else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
9.96
9.97 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
9.98 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
9.99 \ No newline at end of file
10.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Nov 27 18:47:26 2019 +0100
10.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Fri Nov 29 15:22:29 2019 +0100
10.3 @@ -54,11 +54,11 @@
10.4 "~~~~~ and do_solve_step , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
10.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
10.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.7 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
10.8 + val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
10.9
10.10 - determine_next_tactic (pt, pos) sc is;
10.11 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
10.12 - = ((pt, pos), sc, is);
10.13 + determine_next_tactic sc (pt, pos) ist ctxt;
10.14 +"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
10.15 + = (sc, (pt, pos), ist, ctxt);
10.16
10.17 (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
10.18 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
10.19 @@ -95,4 +95,4 @@
10.20 (*+*)val (res, asm) = (get_obj g_result pt (fst p));
10.21 (*+*)if p = ([], Res) andalso
10.22 (*+*) term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
10.23 -(*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";
10.24 +(*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";
10.25 \ No newline at end of file
11.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Nov 27 18:47:26 2019 +0100
11.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Fri Nov 29 15:22:29 2019 +0100
11.3 @@ -46,8 +46,8 @@
11.4 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
11.5 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
11.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
11.7 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
11.8 -val (tac_,is, (t,_)) = determine_next_tactic (pt,pos) sc is;
11.9 +val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
11.10 +val (tac_,(ist, ctxt), (t,_)) = determine_next_tactic sc (pt,pos) ist ctxt;
11.11
11.12 (*+*);tac_; (* = Check_Postcond' *)
11.13
11.14 @@ -59,12 +59,11 @@
11.15 | _ => get_assumptions_ pt (p, p_))
11.16 val metID = get_obj g_metID pt pp;
11.17 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
11.18 - val (loc, pst, ctxt) = case get_loc pt (p, p_) of
11.19 - loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
11.20 + val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
11.21 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
11.22 val thy' = get_obj g_domID pt pp;
11.23 val thy = Celem.assoc_thy thy';
11.24 - val (_, _, (scval, _)) = determine_next_tactic (pt, (p, p_)) sc loc;
11.25 + val (_, _, (scval, _)) = determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt;
11.26
11.27 (*if*) pp = []; (*false*)
11.28
12.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Nov 27 18:47:26 2019 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Fri Nov 29 15:22:29 2019 +0100
12.3 @@ -55,12 +55,12 @@
12.4 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
12.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
12.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.7 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
12.8 + val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
12.9
12.10 val (Check_elementwise' _, (Pstate _, _), _) =
12.11 - determine_next_tactic (pt, pos) sc is;
12.12 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as (pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
12.13 - = ((pt, pos), sc, is);
12.14 + determine_next_tactic sc (pt, pos) ist ctxt;
12.15 +"~~~~~ fun determine_next_tactic , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
12.16 + = (sc, (pt, pos), ist, ctxt);
12.17
12.18 (*case*)
12.19 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
13.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Nov 27 18:47:26 2019 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Fri Nov 29 15:22:29 2019 +0100
13.3 @@ -48,7 +48,6 @@
13.4 else error "calculation not finished correctly 2";
13.5 show_pt pt; (* 11 lines with subpbl *)
13.6 ;
13.7 -
13.8 "----- no thy-context at result -----";
13.9 (** val p = ([], Res);
13.10 ** initContext 1 Thy_ p
13.11 @@ -61,8 +60,8 @@
13.12 (** val ((pt, p), tacis) = get_calc cI;*)
13.13 val ip' = lev_pred' pt ip;
13.14 val ("detailrls", pt, _(*lastpos*)) = (*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);
13.15 +;
13.16 show_pt pt; (* added [2,1]..[2,6] *)
13.17 -
13.18 (**
13.19 ** interSteps 1 ([3,1], Res); (* added [3,1,1] Frm + Res *)
13.20 ** val ((pt,_),_) = get_calc 1;
13.21 @@ -100,8 +99,17 @@
13.22 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *);
13.23
13.24 show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)
13.25 +val (_, _, (pt''''', p''''')) =
13.26 + complete_solve CompleteSubpbl [] (pt', pos');
13.27 +show_pt pt''''';(*ok in comparison to desired functionality?
13.28 +:
13.29 +(([3], Pbl), solve (-1 + x = 0, x)),
13.30 +(([3,1], Frm), -1 + x = 0),
13.31 +(([3,1,1], Frm), -1 + x = 0),
13.32 +(([3,1,1], Res), x = 0 + -1 * -1)]
13.33 +----------------------------------- but the previously existing end ..([], Res) is missing*)
13.34
13.35 - complete_solve CompleteSubpbl [] (pt', pos');
13.36 +(*//---- oucommented after multiple renaming in lucin, which created cascaeds of error ------ \\* )
13.37 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));
13.38 (*if*) p = ([], Res) (* = false*);
13.39 (*if*) member op = [Pbl,Met] p_ (* = false*);
13.40 @@ -118,19 +126,26 @@
13.41 (*if*) member op = [Pbl, Met] p_ (*else*);
13.42 val (pbl, p', rls') = par_pbl_det pt p;
13.43 (*if*) pbl (*else*);
13.44 - val scr = (*case*) rls' (*of*);
13.45 - (Rule.e_rls(*!!!*), get_loc pt (p, p_), scr) (*return value*);
13.46 + val Rls {scr = Rule.Prog prog,...} = (*case*) rls' (*of*);
13.47 + val t = get_last_formula (pt, (p, p_))
13.48 + val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
13.49 +(*+*)id_rls rls' = "isolate_bdv";
13.50
13.51 -(*+*)id_rls rls' = "isolate_bdv";
13.52 -"~~~~~ from from_pblobj_or_detail' to do_solve_step return val:"; val () = ();
13.53 + (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') (*return value*);
13.54 +"~~~~~ from fun from_pblobj_or_detail'\<longrightarrow>and do_solve_step return val:"; val (_, (ist, ctxt), sc)
13.55 + = (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog');
13.56
13.57 val (Rewrite_Inst' (_, _, _, _, _, ("risolate_bdv_add", _), _, _), is, (t, _)) =
13.58 - determine_next_tactic (pt, pos) sc is;
13.59 -"~~~~~ fun determine_next_tactic , args:"; val ((ptp as (pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, _(*ctxt*)))
13.60 - = ((pt, pos), sc, is);
13.61 + determine_next_tactic sc (pt, pos) ist ctxt;
13.62
13.63 - (*case*)
13.64 - scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
13.65 +"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
13.66 + = (sc, (pt, pos), ist, ctxt);
13.67 +
13.68 +(*+*)scrstate2str ist = "([\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)"
13.69 +(*+*) previous test succeeded with:
13.70 +(*+*)"([\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"], [R,R,L,L,R,R,R], e_rls, SOME??.empty, \nx = 0 + -1 * -1, ORundef, AppUndef_, false)"
13.71 +
13.72 + (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
13.73 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
13.74 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
13.75 (*if*) 0 = length path (*else*);
13.76 @@ -140,12 +155,16 @@
13.77 = ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
13.78 (*if*) 1 < length path (*then*);
13.79
13.80 +(*+*)scrstate2str ist =
13.81 +(*+*)"([\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, Skip_, false)"
13.82 +(*+*) previous test succeeded with:
13.83 +((*+*)"([\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"], [R,R,L,L,R,R,R], e_rls, SOME??.empty, \nx = 0 + -1 * -1, ORundef, Skip_, false)"
13.84 +
13.85 scan_up2 yyy (ist |> path_up) (go_up path prog);
13.86 "~~~~~ fun scan_up2 , args:"; val ((yyy as (_, xxx)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))
13.87 = (yyy, (ist |> path_up), (go_up path prog));
13.88
13.89 - (*case*)
13.90 - scan_dn2 xxx (ist |> path_down [R]) e (*of*);
13.91 + (*case*) scan_dn2 xxx (ist |> path_down [R]) e (*of*);
13.92 (*========== a leaf has been found ==========*)
13.93 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
13.94 = (xxx, (ist |> path_down [R]), e);
13.95 @@ -233,3 +252,4 @@
13.96 (*+*) handle Pattern.MATCH => @{term aaaaaaaaaaaaaaa} (* <<<<<<<<<-----------------(*TODO.90*)*)
13.97 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
13.98 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
13.99 +( *\\ --- oucommented after multiple renaming in lucin, which created cascaeds of error ------ //*)
14.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Nov 27 18:47:26 2019 +0100
14.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri Nov 29 15:22:29 2019 +0100
14.3 @@ -565,7 +565,7 @@
14.4 val Steps [(m',f',pt',p',c',s')] =
14.5 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
14.6 val is' = get_istate pt' p';
14.7 - determine_next_tactic thy' (pt'(*'*),p') sc is';
14.8 + determine_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
14.9
14.10
14.11
15.1 --- a/test/Tools/isac/Test_Isac.thy Wed Nov 27 18:47:26 2019 +0100
15.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Nov 29 15:22:29 2019 +0100
15.3 @@ -50,11 +50,15 @@
15.4 section \<open>code for copy & paste\<close>
15.5 text \<open>
15.6 "~~~~~ fun xxx , args:"; val () = ();
15.7 -"~~~~~ and xxx , args:"; val () = ();
15.8 -"~~~~~ from xxx to yyy return val:"; val () = ();
15.9 +"~~~~~ and xxx , args:"; val () = ();
15.10 +"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();
15.11 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
15.12 "xx"
15.13 -^ "xxx" (*+*) (*isa*) (*REP*)
15.14 +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
15.15 +\<close>
15.16 +ML \<open>
15.17 +\<close> ML \<open>
15.18 +\<close> ML \<open>
15.19 \<close>
15.20 section \<open>Run the tests\<close>
15.21 text \<open>
16.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Nov 27 18:47:26 2019 +0100
16.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Nov 29 15:22:29 2019 +0100
16.3 @@ -134,10 +134,14 @@
16.4 ML \<open>
16.5 "~~~~~ fun xxx , args:"; val () = ();
16.6 "~~~~~ and xxx , args:"; val () = ();
16.7 -"~~~~~ from xxx to yyy return val:"; val () = ();
16.8 +"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();
16.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
16.10 "xx"
16.11 -^ "xxx" (*+*)
16.12 +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
16.13 +\<close> ML \<open>
16.14 +\<close>
16.15 +ML \<open>
16.16 +\<close> ML \<open>
16.17 \<close> ML \<open>
16.18 \<close>
16.19
16.20 @@ -204,7 +208,6 @@
16.21 ML_file "MathEngBasic/mstools.sml"
16.22 ML_file "MathEngBasic/specification-elems.sml"
16.23 ML_file "MathEngBasic/ctree.sml" (*!...!see(25)*)
16.24 -
16.25 ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
16.26 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
16.27 ML_file "Specify/generate.sml"
17.1 --- a/test/Tools/isac/Test_Some.thy Wed Nov 27 18:47:26 2019 +0100
17.2 +++ b/test/Tools/isac/Test_Some.thy Fri Nov 29 15:22:29 2019 +0100
17.3 @@ -46,12 +46,16 @@
17.4 ML \<open>
17.5 "~~~~~ fun xxx , args:"; val () = ();
17.6 "~~~~~ and xxx , args:"; val () = ();
17.7 -"~~~~~ from xxx -> fun yyy -> fun zzz, return val:"; val () = ();
17.8 +"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();
17.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
17.10 "xx"
17.11 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
17.12 \<close> ML \<open>
17.13 \<close>
17.14 +ML \<open>
17.15 +\<close> ML \<open>
17.16 +\<close> ML \<open>
17.17 +\<close>
17.18 text \<open>
17.19 declare [[show_types]]
17.20 declare [[show_sorts]]
18.1 --- a/test/Tools/isac/Test_Some_meld.thy Wed Nov 27 18:47:26 2019 +0100
18.2 +++ b/test/Tools/isac/Test_Some_meld.thy Fri Nov 29 15:22:29 2019 +0100
18.3 @@ -43,10 +43,14 @@
18.4 ML \<open>
18.5 "~~~~~ fun xxx , args:"; val () = ();
18.6 "~~~~~ and xxx , args:"; val () = ();
18.7 -"~~~~~ from xxx to yyy return val:"; val () = ();
18.8 +"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();
18.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
18.10 "xx"
18.11 -^ "xxx" (*+*)
18.12 +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
18.13 +\<close> ML \<open>
18.14 +\<close>
18.15 +ML \<open>
18.16 +\<close> ML \<open>
18.17 \<close> ML \<open>
18.18 \<close>
18.19 text \<open>
19.1 --- a/test/Tools/isac/Test_Theory.thy Wed Nov 27 18:47:26 2019 +0100
19.2 +++ b/test/Tools/isac/Test_Theory.thy Fri Nov 29 15:22:29 2019 +0100
19.3 @@ -9,12 +9,16 @@
19.4 ML \<open>
19.5 "~~~~~ fun xxx , args:"; val () = ();
19.6 "~~~~~ and xxx , args:"; val () = ();
19.7 -"~~~~~ from xxx -> fun yyy -> fun zzz, return val:"; val () = ();
19.8 +"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = ();
19.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
19.10 "xx"
19.11 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
19.12 \<close> ML \<open>
19.13 \<close>
19.14 +ML \<open>
19.15 +\<close> ML \<open>
19.16 +\<close> ML \<open>
19.17 +\<close>
19.18 text \<open>
19.19 declare [[show_types]]
19.20 declare [[show_sorts]]