1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Wed Oct 30 14:40:22 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Oct 30 16:46:05 2019 +0100
1.3 @@ -13,6 +13,13 @@
1.4 ML_file inform.sml
1.5 ML_file "lucas-interpreter.sml"
1.6 ML \<open>
1.7 +open LucinNEW
1.8 +\<close> ML \<open>
1.9 +Istate.AppUndef_: Istate.appy_ (*end =...*);
1.10 +Istate.Skip_
1.11 +\<close> ML \<open>
1.12 +Aundef: asap (*or = ... NOT : Istate TODO*)
1.13 +\<close> ML \<open>
1.14 \<close> ML \<open>
1.15 \<close> ML \<open>
1.16 \<close>
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 14:40:22 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 16:46:05 2019 +0100
2.3 @@ -43,10 +43,10 @@
2.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.5 datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
2.6 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
2.7 - val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy
2.8 - val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy
2.9 - val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy
2.10 - datatype asap = Aundef | AssOnly | AssGen;
2.11 + val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy
2.12 + val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy
2.13 + val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy
2.14 + datatype asap = Aundef | AssOnly | AssGen;
2.15 val go : Celem.loc_ -> term -> term
2.16 val go_up: Celem.loc_ -> term -> term
2.17 val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy
2.18 @@ -279,15 +279,15 @@
2.19 if ay = Skip_ then Skip (get_act_env ist) else Napp (get_env ist)
2.20 | nstep_up _ _ _ ist _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str (get_path ist))
2.21
2.22 -fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, rls, a, v, _, _)) =
2.23 - if l = []
2.24 - then appy thy ptp (E, [R], rls, NONE, v, AppUndef_, false) (Program.body_of prog)
2.25 - else nstep_up thy ptp sc (E, l, rls, a, v, AppUndef_, false) Skip_
2.26 +fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate ist) =
2.27 + if 0 = length (get_path ist)
2.28 + then appy thy ptp (trans_scan_down2 ist) (Program.body_of prog)
2.29 + else nstep_up thy ptp sc (trans_scan_down2 ist) Skip_
2.30 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
2.31
2.32 (* decide for the next applicable Prog_Tac in the program *)
2.33 -fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,rls,a,v,s,_), ctxt) =
2.34 - (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,s,false)) of
2.35 +fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate ist, ctxt) =
2.36 + (case execute_progr_1 thy ptp sc (Istate.Pstate ist) of
2.37 Skip (v, _) => (* program finished *)
2.38 (case par_pbl_det pt p of
2.39 (true, p', _) =>
2.40 @@ -492,7 +492,7 @@
2.41
2.42 fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate ist, ctxt) =
2.43 if get_path ist = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)
2.44 - then assy (ctxt,Rule.e_rls, (pt, p), Aundef) (ist |> upd_path [R], m) (Program.body_of sc)
2.45 + then assy (ctxt,Rule.e_rls, (pt, p), Aundef(*\<rightarrow> Istate*)) (ist |> upd_path [R], m) (Program.body_of sc)
2.46 else astep_up (ctxt,Rule.e_rls,scr, (pt, p)) (ist, m)
2.47 | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def"
2.48
2.49 @@ -584,7 +584,6 @@
2.50 if pp = []
2.51 then
2.52 let
2.53 - (*val is = Istate.Pstate (E, l, Rule.e_rls, a, scval, Istate.Skip_, b)*)
2.54 val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
2.55 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.56 (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
3.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Wed Oct 30 14:40:22 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Wed Oct 30 16:46:05 2019 +0100
3.3 @@ -25,6 +25,8 @@
3.4 val get_subst: pstate -> (Env.T * (term option * term))
3.5 val get_assoc: pstate -> bool
3.6
3.7 + val trans_scan_down2: pstate -> pstate
3.8 + val trans_scan_up2: pstate -> pstate
3.9 val trans_ass: pstate -> pstate -> pstate
3.10 val trans_env_act: pstate -> pstate -> pstate
3.11
3.12 @@ -55,6 +57,8 @@
3.13 struct
3.14 (**)
3.15
3.16 +open Celem
3.17 +
3.18 datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
3.19 (*Appy is only (final) returnvalue, not argument during search *)
3.20 AppUndef_
3.21 @@ -115,6 +119,10 @@
3.22 fun get_assoc (_, _, _, _, _, _, ass) = ass
3.23 fun get_subst (env, _, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
3.24
3.25 +fun trans_scan_down2 (env, _, rls, _, act_arg, _, _) =
3.26 + (env, [R], rls, NONE, act_arg, AppUndef_, false)
3.27 +fun trans_scan_up2 (env, path, rls, form_arg, act_arg, _, _) =
3.28 + (env, path, rls, form_arg, act_arg, AppUndef_, false)
3.29 fun trans_ass (_, _, _, _,_, _, ass) (env, path, rls, form_arg, act_arg, safe, _) =
3.30 (env, path, rls, form_arg, act_arg, safe, ass)
3.31 fun trans_env_act (env, _, _, _, act_arg, _, _) (_, path, rls, form_arg, _, safe, ass) =
4.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Oct 30 14:40:22 2019 +0100
4.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Oct 30 16:46:05 2019 +0100
4.3 @@ -1037,7 +1037,7 @@
4.4 (*+*)then () else error "inform with (positive) check_error_patterns broken 3";
4.5
4.6 val env = case Ctree.get_istate pt pos of
4.7 - Istate.Pstate (env, _, _, _, _, _, _) => env
4.8 + Istate.Pstate ist => Istate.get_env ist
4.9 | _ => error "inform: uncovered case of get_istate"
4.10 ;
4.11 (*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
4.12 @@ -1076,8 +1076,8 @@
4.13 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
4.14 val pp = par_pblobj pt p
4.15 val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
4.16 - val Pstate (env, _, _, _, _, _, _) = get_istate pt pos
4.17 - val subst = get_bdv_subst prog env
4.18 + val Pstate ist = get_istate pt pos
4.19 + val subst = get_bdv_subst prog (Istate.get_env ist)
4.20 val errpatthms = errpats
4.21 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
4.22 |> map (#3: errpat -> thm list)
5.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 14:40:22 2019 +0100
5.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 30 16:46:05 2019 +0100
5.3 @@ -47,8 +47,8 @@
5.4 val thy' = get_obj g_domID pt p;
5.5 val thy = assoc_thy thy';
5.6 val srls = Lucin.get_simplifier (pt, pos)
5.7 - val (is as Istate.Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
5.8 - val ini = init_form thy sc env;
5.9 + val (is as Istate.Pstate ist, ctxt, sc) = init_pstate srls ctxt itms mI;
5.10 + val ini = init_form thy sc (Istate.get_env ist);
5.11 val p = lev_dn p;
5.12 ini = NONE; (*true*)
5.13 val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
6.1 --- a/test/Tools/isac/Interpret/script.sml Wed Oct 30 14:40:22 2019 +0100
6.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Oct 30 16:46:05 2019 +0100
6.3 @@ -112,8 +112,8 @@
6.4 val thy' = get_obj g_domID pt p;
6.5 val thy = assoc_thy thy';
6.6 val srls = Lucin.get_simplifier (pt, pos)
6.7 -val (is as Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
6.8 -val ini = init_form thy sc env;
6.9 +val (is as Pstate ist, ctxt, sc) = init_pstate srls ctxt itms mI;
6.10 +val ini = init_form thy sc (Istate.get_env ist);
6.11 "----- fun init_form, args:"; val (Prog sc) = sc;
6.12 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
6.13 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
6.14 @@ -205,10 +205,10 @@
6.15 then (thd3 o snd3) (get_obj g_origin pt pp)
6.16 else metID
6.17 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
6.18 - val Pstate (env,_,_,a,v,_,_) = get_istate pt (p,p_)
6.19 + val Pstate ist = get_istate pt (p,p_)
6.20 val alltacs = (*we expect at least 1 stac in a script*)
6.21 map ((stac2tac pt thy) o rep_stacexpr o #2 o
6.22 - (handle_leaf "selrul" thy' srls (env, (a, v)))) (stacpbls sc)
6.23 + (handle_leaf "selrul" thy' srls (get_subst ist) )) (stacpbls sc)
6.24 val f =
6.25 case p_ of
6.26 Frm => get_obj g_form pt p
7.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Oct 30 14:40:22 2019 +0100
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Oct 30 16:46:05 2019 +0100
7.3 @@ -161,7 +161,7 @@
7.4 val thy = Celem.assoc_thy thy';
7.5 val srls = Lucin.get_simplifier (pt, pos)
7.6 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
7.7 - (is as Istate.Pstate (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
7.8 + (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
7.9 | _ => error "solve Apply_Method: uncovered case init_pstate"
7.10 val ini = Lucin.init_form thy sc env;
7.11 val p = lev_dn p;
7.12 @@ -181,53 +181,7 @@
7.13 Biegelinie
7.14 AbleitungBiegelinie
7.15 *)
7.16 -"~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p),
7.17 - (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,a,v,S,b), ctxt)) =
7.18 - ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
7.19 -val thy = Celem.assoc_thy thy';
7.20 -(*if*) l = [] orelse (
7.21 - (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
7.22 -(assy ((*thy',*)ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
7.23 -
7.24 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
7.25 - (((*thy',*)ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
7.26 -(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
7.27 -
7.28 -"~~~~~ fun assy , args:"; val (((*thy',*)ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
7.29 - (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
7.30 -val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*);
7.31 -(*+*)writeln (term2str stac); (*SubProblem
7.32 - (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
7.33 - [''Biegelinien'', ''ausBelastung''])
7.34 - [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
7.35 - val p' =
7.36 - case p_ of Frm => p
7.37 - | Res => lev_on p
7.38 - | _ => error ("assy: call by " ^ pos'2str (p,p_));
7.39 - val Ass (m,v', ctxt) = (*case*) associate pt ctxt (m, stac) (*of*);
7.40 -
7.41 -"~~~~~ fun associate , args:"; val (pt, _, (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
7.42 - (stac as Const ("Prog_Tac.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
7.43 - dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
7.44 - (pt, d, m, stac);
7.45 - val dI = HOLogic.dest_string dI';
7.46 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
7.47 - val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
7.48 - val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
7.49 - val ags = TermC.isalist2list ags';
7.50 -(*if*) mI = ["no_met"] = false; (*else*)
7.51 -(* val (pI, pors, mI) = *)
7.52 - (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
7.53 - handle ERROR "actual args do not match formal args"
7.54 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
7.55 -"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
7.56 -(*+*)pbt;
7.57 - fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
7.58 - val pbt' = filter_out is_copy_named pbt
7.59 - val cy = filter is_copy_named pbt
7.60 - val oris' = matc thy pbt' ags []
7.61 - val cy' = map (cpy_nam pbt' oris') cy
7.62 - val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
7.63 +"~~~~~ fun locate_input_tactic , args:"; val () = ();
7.64
7.65 (*+*)val c = [];
7.66 (*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
8.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Oct 30 14:40:22 2019 +0100
8.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Oct 30 16:46:05 2019 +0100
8.3 @@ -210,10 +210,8 @@
8.4 val d = e_rls;
8.5 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
8.6 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
8.7 -"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
8.8 - (scr as Prog (h $ body),d), (Pstate (E,l,rls,a,v,S,b), ctxt)) =
8.9 - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
8.10 -val thy = assoc_thy thy';
8.11 +"~~~~~ fun locate_input_tactic, args:"; val () = ();
8.12 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
8.13 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
8.14 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
8.15 ... Assoc ... is correct*)
8.16 @@ -249,6 +247,7 @@
8.17 term2str consts';
8.18 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
8.19 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
8.20 +( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
8.21
8.22 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
8.23 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
9.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Oct 30 14:40:22 2019 +0100
9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Oct 30 16:46:05 2019 +0100
9.3 @@ -103,9 +103,8 @@
9.4 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
9.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
9.7 -"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
9.8 - (sc as Prog (h $ body)),
9.9 -(Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
9.10 +"~~~~~ fun determine_next_tactic, args:"; val () = ();
9.11 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
9.12 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
9.13 (thy, ptp, sc, E, l, Skip_, a, v);
9.14 1 < length l; (*true*)
9.15 @@ -169,6 +168,7 @@
9.16 then case nxt of ("End_Proof'", End_Proof') => ()
9.17 | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
9.18 else error "rateq.sml: new behaviour: [x = 1 / 5] 2";
9.19 +( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
9.20
9.21 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
9.22 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
9.23 @@ -291,6 +291,7 @@
9.24 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
9.25 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
9.26 (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
9.27 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
9.28 l = []; (* = false*)
9.29 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
9.30 (thy, ptp, sc, E, l, Skip_, a, v);
9.31 @@ -326,4 +327,5 @@
9.32 then case nxt of ("End_Proof'", End_Proof') => ()
9.33 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 1"
9.34 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 2";
9.35 +( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
9.36
10.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 30 14:40:22 2019 +0100
10.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 30 16:46:05 2019 +0100
10.3 @@ -34,135 +34,7 @@
10.4 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
10.5 val (thyID, pblID, metID) =
10.6 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
10.7 -(*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================
10.8 -val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
10.9 -"----- ";
10.10 -(* call sequence: CalcTreeTEST
10.11 - > nxt_specify_init_calc
10.12 - > prep_ori
10.13 -*)
10.14 -val (thy, pbt) = (Thy_Info_get_theory thyID, (#ppc o get_pbt) pblID);
10.15 -"----- in prep_ori";
10.16 -val ctxt = Proof_Context.init_global thy;
10.17 -
10.18 -val ctopts = map (parseNEW ctxt) fmz;
10.19 -val dts = map (split_dts o the) ctopts;
10.20 -(*split_dts:
10.21 -(term * term list) list
10.22 - formulas: e.g. ((1+2)*4/3)^^^2
10.23 - description: e.g. realTestGiven
10.24 -*)
10.25 - prep_ori;
10.26 -(* FROM
10.27 -val it = fn:
10.28 - string list -> theory -> (string * (term * 'a)) list -> ori list
10.29 -TO
10.30 -val it = fn:
10.31 - string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
10.32 -AND
10.33 -FROM val oris = prep_ori...
10.34 -TO val (oris, _) = prep_ori...
10.35 -*)
10.36 -"----- insert ctxt in ctree";
10.37 -(* datatype ppobj
10.38 -FROM loc : istate option * istate option,
10.39 -TO loc : (istate * ctxt) option * (istate * ctxt) option,
10.40 -e.g.
10.41 -FROM val pt = Nd (PblObj
10.42 - {.., loc = (SOME (Pstate ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
10.43 - NONE),
10.44 -TO val pt = Nd (PblObj
10.45 - {.., loc =
10.46 - ((SOME (Pstate ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
10.47 - NONE),
10.48 -*)
10.49 -
10.50 -"===== interactive specification: from origin to specification (probl)";
10.51 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
10.52 - (*nxt =("Add_Given", Model_Problem)*)
10.53 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
10.54 - (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
10.55 -"----- ";
10.56 -(* call sequence: me Model_Problem
10.57 - > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
10.58 - > locatetac tac
10.59 - > loc_specify_
10.60 - > specify GET ctxt (stored in ctree)
10.61 - > specify_additem
10.62 - > appl_add
10.63 -
10.64 -*)
10.65 -"----- in appl_add";
10.66 -(* FROM appl_add thy
10.67 - TO appl_add ctxt
10.68 - FROM parse thy str
10.69 - TO parseNEW ctxt str
10.70 -*)
10.71 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
10.72 - (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
10.73 -val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
10.74 - (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
10.75 -
10.76 -"===== end specify: from specification (probl) to guard (method)";
10.77 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.78 - (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
10.79 -
10.80 -"===== start interpretation: from guard to environment";
10.81 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.82 - (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
10.83 -"----- ";
10.84 -(* call sequence: me ("Apply_Method",...
10.85 - > locatetac
10.86 - > loc_solve_
10.87 - > solve ("Apply_Method",...
10.88 -*)
10.89 -val ((_,tac), ptp) = (nxt, (pt, p));
10.90 -locatetac tac (pt,p);
10.91 - val (mI, m) = mk_tac'_ tac;
10.92 - val Appl m = applicable_in p pt m;
10.93 - member op = specsteps mI;
10.94 - loc_solve_ (mI,m) ptp;
10.95 - val (m, (pt, pos)) = ((mI,m), ptp);
10.96 - solve m (pt, pos);
10.97 - val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
10.98 - (m, (pt, pos));
10.99 - val {srls,...} = get_met mI;
10.100 - val PblObj{meth=itms,...} = get_obj I pt p;
10.101 - val thy' = get_obj g_domID pt p;
10.102 - val thy = assoc_thy thy';
10.103 - val (is as Pstate (env,_,_,_,_,_), ctxt, sc) = init_pstate thy itms mI;
10.104 -
10.105 -"----- go on in the calculation";
10.106 -val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
10.107 - (*nxt = ("Calculate",Calculate "PLUS")*)
10.108 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.109 - (*nxt = ("Calculate",Calculate "TIMES")*)
10.110 -
10.111 -"===== input a formula to be derived from previous istate";
10.112 -"----- appendFormula TODO: first repair error";
10.113 - val cs = ((pt,p),[]);
10.114 - val ("ok", cs' as (_,_,(pt,p))) = step p cs;
10.115 - val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
10.116 -(*
10.117 - val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
10.118 - here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
10.119 -*)
10.120 -
10.121 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.122 -(*nxt = ("Calculate",Calculate "DIVIDE")*)
10.123 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.124 -(*nxt = ("Calculate",Calculate "POWER")*)
10.125 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.126 -(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
10.127 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.128 -(*nxt = ("End_Proof'",End_Proof')*)
10.129 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
10.130 -else error "calculate.sml: script test_calculate changed behaviour";
10.131 -
10.132 -"===== tactic Subproblem: from environment to origin";
10.133 -"----- TODO";
10.134 -======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================*)
10.135 -
10.136 +(*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run =====================*)
10.137
10.138 "----------- debugging setContext..pbl_ -----------------";
10.139 "----------- debugging setContext..pbl_ -----------------";
10.140 @@ -617,6 +489,7 @@
10.141 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
10.142 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
10.143 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
10.144 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
10.145 l = [] = false;
10.146 nstep_up thy ptp sc ist Skip_ (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
10.147 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
10.148 @@ -678,6 +551,7 @@
10.149 (([2], Res), -1 + x = 0)]
10.150
10.151 pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
10.152 +( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
10.153
10.154 "----------- improved fun getTactic for interSteps and numeral calculations --";
10.155 "----------- improved fun getTactic for interSteps and numeral calculations --";