1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 04 11:40:29 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100
1.3 @@ -31,8 +31,8 @@
1.4 | Helpless | End_Program
1.5 (*val determine_next_tactic :
1.6 Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *)
1.7 - val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T * 'a ->
1.8 - Tactic.T * (Istate.T * 'a) * (term * Telem.safe)
1.9 + val determine_next_tactic: Rule.theory' * 'a -> Ctree.state -> Rule.program -> Istate.T * 'b
1.10 + -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe)
1.11
1.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.13 datatype assoc =
1.14 @@ -41,26 +41,23 @@
1.15 | NasNap of term * Env.T;
1.16 val assoc2str : assoc -> string
1.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.18 - datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
1.19 - val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
1.20 -(*old* )val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy( *old*)
1.21 -(*new*)val appy: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy(*new*)
1.22 -(*old* )val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy( *old*)
1.23 -(*new*)val nxt_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy(*new*)
1.24 -(*old* )val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy( *old*)
1.25 -(*new*)val nstep_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> appy(*new*)
1.26 val go : Celem.loc_ -> term -> term
1.27 val go_up: Celem.loc_ -> term -> term
1.28 - val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy
1.29 - val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc
1.30 val check_Let_up : Istate.pstate -> term -> term * term
1.31 val check_Seq_up: Istate.pstate -> term -> term
1.32 -(*old* )val assy : Proof.context * Rule.rls * Ctree.state * Istate.asap -> Istate.pstate * Tactic.T -> term -> assoc( *old*)
1.33 -(*new*)val assy: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc(*new*)
1.34 -(*old* )val ass_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> term -> assoc( *old*)
1.35 -(*new*)val ass_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc;(*new*)
1.36 -(*old* )val astep_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> assoc( *old*)
1.37 -(*new*)val astep_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;(*new*)
1.38 +
1.39 + datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
1.40 + val appy: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy
1.41 + val nxt_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy
1.42 + val nstep_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> appy
1.43 + val execute_progr_1: Rule.program * (Ctree.state * Rule.theory') -> Istate.T -> appy
1.44 +
1.45 + val assy: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc
1.46 + val ass_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc;
1.47 + val astep_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;
1.48 + val execute_progr_2: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> assoc
1.49 +
1.50 + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
1.51 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.52 end
1.53
1.54 @@ -185,7 +182,7 @@
1.55 | _ => Napp env)
1.56 end
1.57
1.58 -fun nxt_up (yyy as (Rule.Prog sc, xxx)) (ist as {finish, ...}) (Const ("HOL.Let"(*1a*), _) $ _) =
1.59 +fun nxt_up (yyy as (Rule.Prog sc, xxx)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
1.60 if finish = Napp_
1.61 then nstep_up yyy (ist |> path_up)
1.62 else (*Skip_*)
1.63 @@ -267,19 +264,18 @@
1.64 nxt_up yyy (ist |> path_up) (go_up path sc)
1.65 else (*interpreted to end*)
1.66 if finish = Skip_ then Skip (get_act_env ist) else Napp env
1.67 - | nstep_up _ (ist as {path, ...}) =
1.68 + | nstep_up _ {path, ...} =
1.69 raise ERROR ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str path)
1.70
1.71 -
1.72 -fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (ist as {path, ...})) =
1.73 +fun execute_progr_1 (sc as Rule.Prog prog, cct) (Istate.Pstate (ist as {path, ...})) =
1.74 if 0 = length path
1.75 - then appy (ptp, (fst thy)) (trans_scan_down2 ist)(*sets AppUndef?!?*) (Program.body_of prog)(*new*)
1.76 - else nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_)(*sets AppUndef?!?*)(*new*)
1.77 -| execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
1.78 + then appy cct (trans_scan_down2 ist) (Program.body_of prog)
1.79 + else nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_)
1.80 +| execute_progr_1 _ _ = raise ERROR "execute_progr_1: uncovered pattern";
1.81
1.82 (* decide for the next applicable Prog_Tac in the program *)
1.83 -fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate ist, ctxt) =
1.84 - (case execute_progr_1 thy ptp sc (Istate.Pstate ist) of
1.85 +fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) sc (Istate.Pstate ist, _(*ctxt*)) =
1.86 + (case execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) of
1.87 Skip (v, _) => (* program finished *)
1.88 (case par_pbl_det pt p of
1.89 (true, p', _) =>
1.90 @@ -287,14 +283,14 @@
1.91 val (_, pblID, _) = get_obj g_spec pt p';
1.92 in
1.93 (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
1.94 - (Istate.e_istate, ctxt), (v, Telem.Safe))
1.95 + (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe))
1.96 end
1.97 | _ =>
1.98 - (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))
1.99 + (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)))
1.100 | Napp _ =>
1.101 - (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
1.102 + (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
1.103 | Appy (m', (ist as {act_arg, ...})) =>
1.104 - (m', (Pstate ist, ctxt), (act_arg, Telem.Safe))) (* found next tac *)
1.105 + (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *)
1.106 | determine_next_tactic _ _ _ (is, _) =
1.107 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
1.108
1.109 @@ -322,7 +318,7 @@
1.110
1.111 fun assy xxx ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =
1.112 (case assy xxx (ist |> path_down [L, R]) e of
1.113 - NasApp (ist', ctxt, ss) =>
1.114 + NasApp (ist', _, _) =>
1.115 assy xxx (ist' |> path_down [R, D] |> upd_env' (TermC.mk_Free (id, T)) |> trans_ass ist) b
1.116 | NasNap (v, E) =>
1.117 assy xxx (ist |> path_down [R, D] |> upd_env (Env.upd_env E (TermC.mk_Free (id, T), v))) b
1.118 @@ -400,7 +396,7 @@
1.119 | Chead.Notappl _ => (NasNap (ist |> get_act_env)))
1.120 ));
1.121
1.122 -fun ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, ctxt, tac))) ist (Const ("HOL.Let"(*1*), _) $ _) =
1.123 +fun ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =
1.124 let
1.125 val (i, body) = check_Let_up ist p
1.126 in case assy xxx (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef) body of
1.127 @@ -412,21 +408,21 @@
1.128 | ass_up yyy ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = astep_up yyy ist
1.129
1.130 (*all has been done in (*2*) below*)
1.131 - | ass_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist
1.132 + | ass_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist
1.133 | ass_up yyy ist (Const ("Tactical.Seq"(*2*), _) $ _ $ _) = astep_up yyy ist (*2*: comes from e2*)
1.134 (* comes from e1, goes to e2 *)
1.135 | ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))) ist (Const ("Tactical.Seq"(*3*), _) $ _ ) =
1.136 let
1.137 val e2 = check_Seq_up ist p
1.138 in
1.139 - case assy xxx (ist |> path_up_down[R] |> upd_or Aundef) e2 of
1.140 + case assy xxx (ist |> path_up_down [R] |> upd_or Aundef) e2 of
1.141 NasNap (v, E) => astep_up yyy (ist |> path_up |> upd_act_env (v, E))
1.142 | NasApp (ist', ctxt', tac') => astep_up (prog, (cstate, ctxt', tac')) ist'
1.143 | zzz => zzz
1.144 end
1.145
1.146 - | ass_up yyy ist (Const ("Tactical.Try"(*1*),_) $ _ $ _) = astep_up yyy ist
1.147 - | ass_up yyy ist (Const ("Tactical.Try"(*2*),_) $ _) = astep_up yyy ist
1.148 + | ass_up yyy ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = astep_up yyy ist
1.149 + | ass_up yyy ist (Const ("Tactical.Try"(*2*), _) $ _) = astep_up yyy ist
1.150
1.151 | ass_up (yyy as (prog, xxx as (cstate, _, _))) (ist as {eval, ...}) (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
1.152 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.upd_env' a (get_act_env ist)) c)
1.153 @@ -468,18 +464,17 @@
1.154 if 1 < length path
1.155 then ass_up yyy (ist |> path_up) (go (path_up' path) sc)
1.156 else (NasNap (get_act_env ist))
1.157 - | astep_up _ (ist as {path, ...}) =
1.158 + | astep_up _ {path, ...} =
1.159 raise ERROR ("astep_up: uncovered fun-def with " ^ Celem.loc_2str path)
1.160
1.161 -
1.162 -fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate (ist as {path, ...}), ctxt) =
1.163 +fun execute_progr_2 (scr as Rule.Prog sc, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
1.164 if path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)
1.165 - then assy ((pt, p), ctxt, m) (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc)
1.166 - else astep_up (scr, ((pt, p), ctxt, m)) ist
1.167 - | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def"
1.168 + then assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc)
1.169 + else astep_up (scr, cctt) ist
1.170 + | execute_progr_2 _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def"
1.171
1.172 fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac =
1.173 - (case execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) of
1.174 + (case execute_progr_2 (progr, (cstate, ctxt, tac)) istate of
1.175 Assoc ((ist as {assoc, ...}), ctxt, tac') =>
1.176 if assoc
1.177 then Safe_Step (Istate.Pstate ist, ctxt, tac')
1.178 @@ -556,8 +551,7 @@
1.179 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
1.180 val thy' = get_obj g_domID pt pp;
1.181 val thy = Celem.assoc_thy thy';
1.182 - val (_, _, (scval, _(*scsaf*))) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
1.183 - (* Telem.safe should go on to Check_Postcond' vvvvv *)
1.184 + val (_, _, (scval, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
1.185 in
1.186 if pp = []
1.187 then
1.188 @@ -604,11 +598,11 @@
1.189 val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;
1.190 (* TODO here ^^^ return finished/helpless/ok ?*)
1.191 in case tac_ of
1.192 - Tactic.End_Detail' _ => ([(Tactic.End_Detail,
1.193 - Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
1.194 - | _ => begin_end_prog tac_ is ptp
1.195 + Tactic.End_Detail' _ =>
1.196 + ([(Tactic.End_Detail, Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
1.197 + | _ => begin_end_prog tac_ is ptp
1.198 end;
1.199 -
1.200 +
1.201 (* compare inform with ctree.form at current pos by nrls;
1.202 if found, embed the derivation generated during comparison
1.203 if not, let the mat-engine compute the next ctree.form *)
2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Nov 04 11:40:29 2019 +0100
2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Wed Nov 06 15:08:27 2019 +0100
2.3 @@ -1373,6 +1373,25 @@
2.4 additionally a notepad is required.
2.5 Further examples for GCD are at [[2]].
2.6 \<close>
2.7 +
2.8 +section \<open>structure providing unique identifiers in tests\<close>
2.9 +ML \<open>
2.10 +\<close> ML \<open>
2.11 +signature GCD_POLY_ML =
2.12 +sig
2.13 + val eval: poly -> int -> int -> poly
2.14 end
2.15
2.16 +(**)
2.17 +structure Gcd_ML(**): GCD_POLY_ML(**) =
2.18 +struct
2.19 +(**)
2.20 + fun eval (p: poly) var value = order (map (eval_monom var value) p)
2.21
2.22 +end
2.23 +\<close> ML \<open>
2.24 +\<close>
2.25 +
2.26 +end
2.27 +
2.28 +
3.1 --- a/src/Tools/isac/MathEngine/solve.sml Mon Nov 04 11:40:29 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Nov 06 15:08:27 2019 +0100
3.3 @@ -141,18 +141,15 @@
3.4 in
3.5 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
3.6 LucinNEW.Safe_Step (istate, ctxt, tac) =>
3.7 -(*NEW*) let
3.8 -(*NEW*) val (p'', _, _,pt') =
3.9 -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.10 -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.11 -(*NEW*) (istate, ctxt) (lev_on p, Pbl) pt;
3.12 -(*NEW*) in
3.13 -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.14 -(*NEW*) [(*ctree NOT cut*)], (pt', p'')))
3.15 -(*NEW*) end
3.16 -(*OLD* ) ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))],
3.17 -(*OLD*) [(*ctree NOT cut*)], cstate))
3.18 -( *OLD*)
3.19 + let
3.20 + val (p'', _, _,pt') =
3.21 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.22 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.23 + (istate, ctxt) (lev_on p, Pbl) pt;
3.24 + in
3.25 + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.26 + [(*ctree NOT cut*)], (pt', p'')))
3.27 + end
3.28 | _ => (* NotLocatable, but applicable_in from the beginning *)
3.29 let
3.30 val (p, ps, _, pt) =
3.31 @@ -236,38 +233,34 @@
3.32 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
3.33 in
3.34 case LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
3.35 -(*OLD* ) LucinNEW.Safe_Step ((*->*)cstate(*<-*), istate, (*->*)ctxt(*<-*), tac) =>
3.36 -( *NEW*) LucinNEW.Safe_Step (istate, ctxt, tac) =>
3.37 -(*NEW*) let
3.38 -(*NEW*) val p' =
3.39 -(*NEW*) case p_ of Frm => p
3.40 -(*NEW*) | Res => lev_on p
3.41 -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.42 -(*NEW*) val (p'', _, _,pt') =
3.43 -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.44 -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.45 -(*NEW*) (istate, ctxt) (p', p_) pt;
3.46 -(*NEW*) in
3.47 -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.48 -(*NEW*) [(*ctree NOT cut*)], (pt', p'')))
3.49 -(*NEW*) end
3.50 -(*OLD* ) ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))],
3.51 -(*OLD*) [(*ctree NOT cut*)], cstate))
3.52 -( *OLD*)
3.53 + LucinNEW.Safe_Step (istate, ctxt, tac) =>
3.54 + let
3.55 + val p' =
3.56 + case p_ of Frm => p
3.57 + | Res => lev_on p
3.58 + | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.59 + val (p'', _, _,pt') =
3.60 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.61 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.62 + (istate, ctxt) (p', p_) pt;
3.63 + in
3.64 + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.65 + [(*ctree NOT cut*)], (pt', p'')))
3.66 + end
3.67 | LucinNEW.Unsafe_Step (istate, ctxt, tac) =>
3.68 -(*NEW*) let
3.69 -(*NEW*) val p' =
3.70 -(*NEW*) case p_ of Frm => p
3.71 -(*NEW*) | Res => lev_on p
3.72 -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.73 -(*NEW*) val (p'', _, _,pt') =
3.74 -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.75 -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.76 -(*NEW*) (istate, ctxt) (p', p_) pt;
3.77 -(*NEW*) in
3.78 -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.79 -(*NEW*) [(*ctree NOT cut*)], (pt', p'')))
3.80 -(*NEW*) end
3.81 + let
3.82 + val p' =
3.83 + case p_ of Frm => p
3.84 + | Res => lev_on p
3.85 + | _ => error ("solve: call by " ^ pos'2str (p, p_));
3.86 + val (p'', _, _,pt') =
3.87 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
3.88 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
3.89 + (istate, ctxt) (p', p_) pt;
3.90 + in
3.91 + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
3.92 + [(*ctree NOT cut*)], (pt', p'')))
3.93 + end
3.94 | _ => (* NotLocatable *)
3.95 let
3.96 val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
3.97 @@ -401,10 +394,10 @@
3.98 SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
3.99 | NONE => (*/-------------------------------------- NEW fun locate_input_formula------*)
3.100 let
3.101 - (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
3.102 - (*NEW*)val {scr = prog, ...} = Specify.get_met metID
3.103 - (*NEW*)val istate = get_istate pt pos
3.104 - (*NEW*)val ctxt = get_ctxt pt pos
3.105 + val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
3.106 + val {scr = prog, ...} = Specify.get_met metID
3.107 + val istate = get_istate pt pos
3.108 + val ctxt = get_ctxt pt pos
3.109 in
3.110 case LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in of
3.111 LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>
4.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Mon Nov 04 11:40:29 2019 +0100
4.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Wed Nov 06 15:08:27 2019 +0100
4.3 @@ -22,13 +22,13 @@
4.4
4.5 (* a simplified getter *)
4.6 fun test_get_calc cI =
4.7 - case assoc (!test_states, cI) of
4.8 + case LibraryC.assoc (!test_states, cI) of
4.9 NONE => error ("get_calc " ^ string_of_int cI ^ " not existent")
4.10 | SOME c => c;
4.11
4.12 (* a simplified updater *)
4.13 fun test_upd_calc cI cs =
4.14 - (if is_none (assoc (!test_states, cI))
4.15 + (if is_none (LibraryC.assoc (!test_states, cI))
4.16 then writeln ("upd_calc created new calculation " ^ string_of_int cI)
4.17 else ();
4.18 test_states := overwrite (!test_states, (cI, cs)))
5.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Nov 04 11:40:29 2019 +0100
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Nov 06 15:08:27 2019 +0100
5.3 @@ -1044,7 +1044,7 @@
5.4 val p = get_pos 1 1;
5.5 val (Form f, tac, asms) = pt_extract (pt, p);
5.6 if term2str f = "[x = 1]" andalso p = ([], Res)
5.7 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
5.8 + andalso terms2str asms = "[]" then ()
5.9 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
5.10 DEconstrCalcTree 1;
5.11
5.12 @@ -1062,7 +1062,7 @@
5.13 val p = get_pos 1 1;
5.14 val (Form f, tac, asms) = pt_extract (pt, p);
5.15 if term2str f = "[x = 1]" andalso p = ([], Res)
5.16 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
5.17 + andalso terms2str asms = "[]" then ()
5.18 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
5.19 DEconstrCalcTree 1;
5.20
6.1 --- a/test/Tools/isac/Interpret/inform.sml Mon Nov 04 11:40:29 2019 +0100
6.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Nov 06 15:08:27 2019 +0100
6.3 @@ -599,8 +599,7 @@
6.4 val ((pt, p), _) = get_calc 1;
6.5 val (t, asm) = get_obj g_result pt [];
6.6 if term2str t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
6.7 -terms2str asm = "[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\"," ^
6.8 - "\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"
6.9 +terms2str asm = "[]"
6.10 then () else error "inform [rational,simplification] changed at end";
6.11 (*show_pt pt;
6.12 [
7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 04 11:40:29 2019 +0100
7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 06 15:08:27 2019 +0100
7.3 @@ -40,35 +40,49 @@
7.4 val Appl m = applicable_in p pt m;
7.5 member op = specsteps mI (*false*);
7.6 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
7.7 -"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
7.8 +
7.9 +"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
7.10 (m, (pt, pos));
7.11 -val {srls, ...} = get_met mI;
7.12 - val PblObj {meth=itms, ...} = get_obj I pt p;
7.13 - val thy' = get_obj g_domID pt p;
7.14 - val thy = assoc_thy thy';
7.15 - val srls = Lucin.get_simplifier (pt, pos)
7.16 - val (is as Istate.Pstate (ist as {env, ...}), ctxt, sc) = init_pstate srls ctxt itms mI;
7.17 - val ini = init_form thy sc env;
7.18 -(*+*)ini = NONE; (*true*)
7.19 - val p = lev_dn p;
7.20 - val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
7.21 - val d = e_rls (*FIXME: get simplifier from domID*);
7.22 -"~~~~~ fun locate_input_tactic , args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
7.23 - (scr as Prog (h $ body),d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt)) =
7.24 - ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
7.25 -val thy = assoc_thy thy';
7.26 -l = [] orelse ((*init.in solve..Apply_Method...*)
7.27 - (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
7.28 -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,asap,S,b),ss),
7.29 - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
7.30 - ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]), body);
7.31 - (*check: true*) term2str e = "Take (Integral f_f D v_v)";
7.32 -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,asap,S,b), (m,_,pt,(p,p_),c)::ss), t) =
7.33 - (ya, ((E , l@[L,R], rls,a,v,asap,S,b),ss), e);
7.34 -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t;
7.35 -(* val ctxt = get_ctxt pt (p,p_)
7.36 -exception PTREE "get_obj: pos = [0] does not exist" raised
7.37 -(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
7.38 + val {srls, ...} = get_met mI;
7.39 + val itms = case get_obj I pt p of
7.40 + PblObj {meth=itms, ...} => itms
7.41 + | _ => error "solve Apply_Method: uncovered case get_obj"
7.42 + val thy' = get_obj g_domID pt p;
7.43 + val thy = Celem.assoc_thy thy';
7.44 + val srls = Lucin.get_simplifier (pt, pos)
7.45 + val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
7.46 + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
7.47 + | _ => error "solve Apply_Method: uncovered case init_pstate"
7.48 + val ini = Lucin.init_form thy sc env;
7.49 + val p = lev_dn p;
7.50 +
7.51 + val NONE = (*case*) ini (*of*);
7.52 + val (m', (is', ctxt'), _) =
7.53 + LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
7.54 +
7.55 + val Safe_Step (_, _, Take' _) = (*case*)
7.56 + locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
7.57 +"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), cstate, istate, ctxt, tac)
7.58 + = (sc, (pt, (p, Res)), is', ctxt', m');
7.59 +
7.60 + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*);
7.61 +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
7.62 + = ((progr, (cstate, ctxt, tac)), istate);
7.63 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
7.64 +
7.65 + val Assoc (_, _, Take' _) =
7.66 + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc);
7.67 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
7.68 + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc));
7.69 +
7.70 +(*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "assy Integral changed";
7.71 +
7.72 + (*case*)
7.73 + assy xxx (ist |> path_down [L, R]) e (*of*);
7.74 + (*======= end of scanning tacticals, a leaf =======*)
7.75 +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
7.76 + = (xxx, (ist |> path_down [L, R]), e);
7.77 +val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
7.78
7.79
7.80 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
7.81 @@ -88,7 +102,7 @@
7.82 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
7.83
7.84 (*// relevant call --------------------------------------------------------------------------\\*)
7.85 -(*[1], Res* )val (*** )xxx( ***) (p,_,f,nxt,_,pt) =*) me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
7.86 +(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
7.87
7.88 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
7.89
7.90 @@ -114,57 +128,54 @@
7.91 val srls = get_simplifier cstate;
7.92
7.93 (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
7.94 - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
7.95 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
7.96 - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
7.97 - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
7.98 + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*);
7.99 +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
7.100 + = ((progr, (cstate, ctxt, tac)), istate);
7.101 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
7.102
7.103 (** )val xxxxx_xx = ( **)
7.104 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc);
7.105 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
7.106 - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,asap,S,b), m), (Program.body_of sc));
7.107 + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc);
7.108 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
7.109 + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc));
7.110
7.111 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e (*of*);
7.112 -"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
7.113 - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac), e);
7.114 + (*case*) assy xxx (ist |> path_down [L, R]) e (*of*);
7.115 +"~~~~~ fun assy , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Seq"(*1*), _) $ e1 $ e2 $ a))
7.116 + = (xxx, (ist |> path_down [L, R]), e);
7.117
7.118 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss) e1 (*of*);
7.119 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
7.120 - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss), e1);
7.121 + (*case*) assy xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
7.122 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
7.123 + = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
7.124
7.125 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
7.126 + (*case*) assy xxx (ist |> path_down [R]) e (*of*);
7.127 (*======= end of scanning tacticals, a leaf =======*)
7.128 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
7.129 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
7.130 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
7.131 - val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
7.132 - (* 1st ContextC.insert_assumptions asms' ctxt *)
7.133 +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
7.134 + = (xxx, (ist |> path_down [R]), e);
7.135 + val (a', Celem.STac stac) =
7.136 + (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
7.137 + val Lucin.Ass (m, v', ctxt) =
7.138 + (*case*) associate pt ctxt (m, stac) (*of*);
7.139
7.140 -(*NEW*) Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m) (*return value*);
7.141 + Assoc (ist |> upd_subst_true (a', v'), ctxt, m) (*return value*);
7.142 "~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx)
7.143 - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); (*return value*)
7.144 + = (Assoc (ist |> upd_subst_true (a', v'), ctxt, m));
7.145
7.146 -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
7.147 - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m));
7.148 - (*if*) strong_ass; (*then*)
7.149 +"~~~~~ from execute_progr_2 to fun locate_input_tactic return val:"; val Assoc ((ist as {assoc, ...}), ctxt, tac')
7.150 + = (Assoc (ist |> upd_subst_true (a', v'), ctxt, m));
7.151 + (*if*) LibraryC.assoc (*then*);
7.152
7.153 -"~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac)
7.154 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate is, ctxt, tac')(**);
7.155 + Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
7.156 +"~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac)
7.157 + = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
7.158
7.159 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
7.160 -(*NEW*) val p' =
7.161 -(*NEW*) case p_ of Frm => p
7.162 -(*NEW*) | Res => lev_on p
7.163 -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_));
7.164 -(*NEW*) val (p'', _, _,pt') =
7.165 -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m
7.166 -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
7.167 -(*NEW*) (Istate.Pstate (E,l,rls,a',v',asap,S,true), ctxt) (p', p_) pt;
7.168 -(*NEW*) (*in*)
7.169 -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
7.170 -(*NEW*) [(*ctree NOT cut*)], (pt', p'')));
7.171 + val (p'', _, _,pt') =
7.172 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
7.173 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
7.174 + (istate, ctxt) (lev_on p, Pbl) pt;
7.175 + (*in*)
7.176
7.177 -(*NEW*)("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [], (pt', p'')));
7.178 + ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
7.179 + [(*ctree NOT cut*)], (pt', p''))) (*return value*);
7.180 "~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
7.181 = ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
7.182
7.183 @@ -191,8 +202,8 @@
7.184 = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
7.185
7.186 (*//--------------------- check results from modified me ----------------------------------\\*)
7.187 -if p = ([1], Res) andalso
7.188 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n"
7.189 +if p = ([2], Res) andalso
7.190 + pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
7.191 then
7.192 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
7.193 | _ => error "")
7.194 @@ -201,7 +212,8 @@
7.195
7.196 "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
7.197 (*\\------------------ end of modified "fun me" ---------------------------------------------//*)
7.198 -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
7.199 +
7.200 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
7.201 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
7.202 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
7.203 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
7.204 @@ -244,15 +256,17 @@
7.205 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
7.206 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
7.207
7.208 -(*+*)map tac2str (sel_appl_atomic_tacs pt p) =
7.209 +(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
7.210 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
7.211 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"];
7.212 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
7.213 + then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
7.214 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
7.215
7.216 -(*+*)map tac2str (sel_appl_atomic_tacs pt p) =
7.217 +(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
7.218 ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
7.219 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
7.220 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"];
7.221 + "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
7.222 + then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
7.223 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
7.224
7.225 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
7.226 @@ -271,64 +285,62 @@
7.227 val thy' = get_obj g_domID pt (par_pblobj pt p);
7.228 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
7.229
7.230 - (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
7.231 + (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
7.232 "~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
7.233 = (sc, (pt, po), (fst is), (snd is), m);
7.234 val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
7.235
7.236 - (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*);
7.237 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
7.238 - = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt));
7.239 - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
7.240 + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*);
7.241 +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
7.242 + = ((progr, (cstate, ctxt, tac)), istate);
7.243 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
7.244
7.245 - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,asap,S,b), m);
7.246 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
7.247 - = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,asap,S,b), m));
7.248 - (*if*) 1 < length l (*then*);
7.249 - val up = drop_last l; (* = [R, L, R, L, R]*)
7.250 + astep_up (scr, cctt) ist;
7.251 +"~~~~~ and astep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
7.252 + = ((scr, cctt), ist);
7.253 + (*if*) 1 < length path (*then*);
7.254
7.255 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
7.256 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _))
7.257 - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
7.258 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
7.259 +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
7.260 + = (yyy, (ist |> path_up), (go (path_up' path) sc));
7.261
7.262 - astep_up ysa iss;
7.263 -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)))
7.264 - = (ysa, iss);
7.265 - (*if*) 1 < length l (*then*);
7.266 - val up = drop_last l; (* = [R, L, R, L]*)
7.267 + astep_up yyy ist;
7.268 +"~~~~~ and astep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
7.269 + = (yyy, ist);
7.270 + (*if*) 1 < length path (*then*);
7.271
7.272 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
7.273 -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss),
7.274 - (Const ("Tactical.Seq"(*3*),_) $ _ ))
7.275 - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
7.276 - val up = drop_last l;
7.277 - val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*);
7.278 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
7.279 +"~~~~~ fun ass_up , args:"; val ((yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))), ist,
7.280 + (Const ("Tactical.Seq"(*3*), _) $ _ ))
7.281 + = (yyy, (ist |> path_up), (go (path_up' path) sc));
7.282 + val e2 = check_Seq_up ist p
7.283 +;
7.284 + (*case*) assy xxx (ist |> path_up_down [R] |> upd_or Aundef) e (*of*);
7.285 +"~~~~~ fun assy , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _))
7.286 + = (xxx, (ist |> path_up_down [R] |> upd_or Aundef), e2);
7.287
7.288 - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss) e2 (*of*);
7.289 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
7.290 - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
7.291 - val NasApp ((E,_,_,_,v,_,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,asap,S,b),ss) e1 (*of*);
7.292 + (*case*) assy xxx (ist |> path_down [L, R]) e1 (*of*);
7.293 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
7.294 + = (xxx, (ist |> path_down [L, R]), e1);
7.295
7.296 - assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e2;
7.297 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
7.298 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
7.299 + (*case*) assy xxx (ist |> path_down [R]) e (*of*);
7.300 + (*======= end of scanning tacticals, a leaf =======*)
7.301 +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
7.302 + = (xxx, (ist |> path_down [R]), e);
7.303 + val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
7.304 + val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
7.305 + val Aundef = (*case*) or (*of*);
7.306 + val Notappl "norm_equation not applicable" =
7.307 + (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
7.308
7.309 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
7.310 - (*======= end of scanning tacticals, a leaf =======*)
7.311 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
7.312 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
7.313 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
7.314 - val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
7.315 - val Aundef = (*case*) ap (*of*);
7.316 - val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
7.317 - val is = (E,l,rls,a',Lucin.tac_2res m',asap,S,false(*FIXXXME.WN0?*));
7.318 - NasApp (is, ctxt, m) (* return value *);
7.319 + (NasNap (ist |> get_act_env)) (* return value *);
7.320
7.321 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
7.322 t, (res, asm)) = m;
7.323 -if scrstate2str is =
7.324 - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^
7.325 - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
7.326 +
7.327 +if scrstate2str ist =
7.328 + "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^
7.329 + "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
7.330 andalso
7.331 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
7.332 andalso
7.333 @@ -346,3 +358,4 @@
7.334 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
7.335 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
7.336 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
7.337 +
8.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Nov 04 11:40:29 2019 +0100
8.2 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Nov 06 15:08:27 2019 +0100
8.3 @@ -387,7 +387,7 @@
8.4 "----------- fun eval_binop -----------------------------";
8.5 "----------- fun eval_binop -----------------------------";
8.6 "----------- fun eval_binop -----------------------------";
8.7 -val (op_, ef) = the (assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
8.8 +val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
8.9 val t = (Thm.term_of o the o (parse thy)) "2 * 3";
8.10 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
8.11 ;
9.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Nov 04 11:40:29 2019 +0100
9.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Wed Nov 06 15:08:27 2019 +0100
9.3 @@ -36,10 +36,10 @@
9.4 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
9.5 (num_str @{thm "int_isolate_add"}) t; term2str t;
9.6
9.7 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
9.8 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
9.9 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
9.10
9.11 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.12 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.13 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
9.14
9.15 "----------- mathengine with usecase1 -------------------";
9.16 @@ -71,10 +71,10 @@
9.17 SOME t' => t'
9.18 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
9.19
9.20 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
9.21 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
9.22 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
9.23
9.24 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.25 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.26 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
9.27
9.28
10.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml Mon Nov 04 11:40:29 2019 +0100
10.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml Wed Nov 06 15:08:27 2019 +0100
10.3 @@ -55,7 +55,7 @@
10.4 "----------- infix %%*%% --------------------------------";
10.5 "----------- fun gcd_coeff ------------------------------";
10.6 (*"----------- fun gcd_coeff_poly -------------------------";*)
10.7 -"----------- fun eval -----------------------------------";
10.8 +"----------- fun Gcd_ML.eval -----------------------------------";
10.9 "----------- fun multi_to_uni ---------------------------";
10.10 "----------- fun uni_to_multi ---------------------------";
10.11 "----------- fun find_new_r ----------------------------";
10.12 @@ -578,17 +578,17 @@
10.13 if gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 then ()
10.14 else error "gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 changed";*)
10.15
10.16 -"----------- fun eval -----------------------------------";
10.17 -"----------- fun eval -----------------------------------";
10.18 -"----------- fun eval -----------------------------------";
10.19 -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 1 = [(1, [0]), (~1, [1])] then ()
10.20 - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 1 = [(1, [0]), (~1, [1])] changed";
10.21 -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 1 = [(2, [0]), (~2, [2])] then ()
10.22 - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 1 =[(2, [0]), (~2, [2])] changed";
10.23 -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 3 = [(9, [0]), (~25, [1])] then ()
10.24 - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 3 = [(9, [0]), (~25, [1])] changed";
10.25 -if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 3 = [(6, [0]), (~8, [2])] then ()
10.26 - else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 3 = [ (6, [0]), (~8, [2])] changed";
10.27 +"----------- fun Gcd_ML.eval -----------------------------------";
10.28 +"----------- fun Gcd_ML.eval -----------------------------------";
10.29 +"----------- fun Gcd_ML.eval -----------------------------------";
10.30 +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 1 = [(1, [0]), (~1, [1])] then ()
10.31 + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 1 = [(1, [0]), (~1, [1])] changed";
10.32 +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 1 = [(2, [0]), (~2, [2])] then ()
10.33 + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 1 =[(2, [0]), (~2, [2])] changed";
10.34 +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 3 = [(9, [0]), (~25, [1])] then ()
10.35 + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 3 = [(9, [0]), (~25, [1])] changed";
10.36 +if Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 3 = [(6, [0]), (~8, [2])] then ()
10.37 + else error " Gcd_ML.eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 3 = [ (6, [0]), (~8, [2])] changed";
10.38
10.39 "----------- fun multi_to_uni ---------------------------";
10.40 "----------- fun multi_to_uni ---------------------------";
10.41 @@ -846,8 +846,8 @@
10.42 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, [], []);
10.43 val r = find_new_r a b r;
10.44 val r_list = r_list @ [r];
10.45 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.46 - (order (eval b (n - 2) r)) (n - 1) 0
10.47 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.48 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0
10.49 val steps = steps @ [g_r];
10.50 (*HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1]
10.51 exception Div raised*)
10.52 @@ -856,8 +856,8 @@
10.53 m > M = false;
10.54 val r = find_new_r a b r;
10.55 val r_list = r_list @ [r];
10.56 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.57 - (order (eval b (n - 2) r)) (n - 1) 0;
10.58 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.59 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0;
10.60 lex_ord (lmonom g) (lmonom g_r) = false;
10.61 lexp g = lexp g_r = true;
10.62 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
10.63 @@ -873,8 +873,8 @@
10.64 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
10.65 val r = find_new_r a b r;
10.66 val r_list = r_list @ [r];
10.67 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.68 - (order (eval b (n - 2) r)) (n - 1) 0
10.69 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.70 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0
10.71 val steps = steps @ [g_r];
10.72 (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
10.73 exception Div raised*)
10.74 @@ -883,8 +883,8 @@
10.75 m > M = false;
10.76 val r = find_new_r a b r;
10.77 val r_list = r_list @ [r];
10.78 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.79 - (order (eval b (n - 2) r)) (n - 1) 0;
10.80 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.81 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0;
10.82 lex_ord (lmonom g) (lmonom g_r) = false;
10.83 lexp g = lexp g_r = true;
10.84 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
10.85 @@ -900,8 +900,8 @@
10.86 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
10.87 val r = find_new_r a b r;
10.88 val r_list = r_list @ [r];
10.89 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.90 - (order (eval b (n - 2) r)) (n - 1) 0
10.91 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.92 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0
10.93 val steps = steps @ [g_r];
10.94 (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
10.95 exception Div raised*)
10.96 @@ -910,8 +910,8 @@
10.97 m > M = false;
10.98 val r = find_new_r a b r;
10.99 val r_list = r_list @ [r];
10.100 - val g_r = gcd_poly' (order (eval a (n - 2) r))
10.101 - (order (eval b (n - 2) r)) (n - 1) 0;
10.102 + val g_r = gcd_poly' (order (Gcd_ML.eval a (n - 2) r))
10.103 + (order (Gcd_ML.eval b (n - 2) r)) (n - 1) 0;
10.104 lex_ord (lmonom g) (lmonom g_r) = false;
10.105 lexp g = lexp g_r = true;
10.106 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
11.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Nov 04 11:40:29 2019 +0100
11.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 06 15:08:27 2019 +0100
11.3 @@ -334,10 +334,11 @@
11.4 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
11.5 if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
11.6 else error "autoCalculate..CompleteCalc: final result";
11.7 -if terms2strs (get_assumptions_ pt p) =
11.8 +if terms2strs (get_assumptions_ pt p) = []
11.9 +(* assumptions are handled by Proof.context now:
11.10 ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
11.11 "x = 1", (*result of subpbl and rootpbl*)
11.12 - "precond_rootmet x"] (*precond of rootmet*)
11.13 + "precond_rootmet x"] (*precond of rootmet*) *)
11.14 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
11.15
11.16
12.1 --- a/test/Tools/isac/MathEngine/solve.sml Mon Nov 04 11:40:29 2019 +0100
12.2 +++ b/test/Tools/isac/MathEngine/solve.sml Wed Nov 06 15:08:27 2019 +0100
12.3 @@ -58,8 +58,7 @@
12.4 | _ => error "solve.sml: interSteps on norm_Rational 2";
12.5 get_obj g_res pt [];
12.6 val (t, asm) = get_obj g_result pt [];
12.7 -if terms2str asm = "[\"8 * x \<noteq> 0\",\"-9 + x ^^^ 2 \<noteq> 0\"," ^
12.8 - "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]"
12.9 +if terms2str asm = "[]"
12.10 then () else error "solve.sml: interSteps on norm_Rational 2, asms";
12.11
12.12
13.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Nov 04 11:40:29 2019 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Nov 06 15:08:27 2019 +0100
13.3 @@ -38,31 +38,31 @@
13.4 val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
13.5 member op = Solve.specsteps mI (* = false*);
13.6
13.7 -loc_solve_ (mI,m) ptp ; (* assy: call by ([3], Pbl)*)
13.8 + loc_solve_ (mI,m) ptp ; (* assy: call by ([3], Pbl)*)
13.9 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = ((mI,m), ptp);
13.10 -Solve.solve m (pt, pos); (* assy: call by ([3], Pbl)*)
13.11 - (* step somewhere within a calculation *)
13.12 -"~~~~~ fun solve, args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
13.13 -Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
13.14 + solve m (pt, pos); (* assy: call by ([3], Pbl)*)
13.15 + (* ======== general tactic as fall through ======== *)
13.16 +"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
13.17 + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
13.18 val thy' = get_obj g_domID pt (par_pblobj pt p);
13.19 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.20 + val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.21
13.22 - locate_input_tactic sc (pt, po) (fst is) (snd is) m; (* assy: call by ([3], Pbl)*)
13.23 + val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
13.24 + locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
13.25 "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
13.26 = (sc, (pt, po), (fst is), (snd is), m);
13.27 val srls = get_simplifier cstate;
13.28
13.29 - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
13.30 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d),
13.31 - (Istate.Pstate (ist as {env=E,path=l,eval=rls,form_arg=a,act_arg=v,or=asap,finish=S,assoc=b}), ctxt))
13.32 - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
13.33 - (*if*)l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
13.34 + (*case*) execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*);
13.35 +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
13.36 + = ((progr, (cstate, ctxt, tac)), istate);
13.37 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
13.38
13.39 - assy ((pt, p), ctxt, m) (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc);
13.40 -"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
13.41 - = (((pt, p), ctxt, m), (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc));
13.42 + assy cctt (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc);
13.43 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
13.44 + = (cctt, (ist |> upd_path [R] |> upd_or Aundef), (Program.body_of sc));
13.45
13.46 -val Assoc (_, _, Rewrite_Set' (_, _, _, _, _)) = (*case*)
13.47 +val Assoc (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
13.48 assy xxx (ist |> path_down [L, R]) e (*of*);
13.49 "~~~~~ fun assy, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Seq"(*1*),_) $e1 $ e2 $ a)) =
13.50 (xxx, (ist |> path_down [L, R]), e);
13.51 @@ -77,9 +77,9 @@
13.52 val Assoc _ = (*case*)
13.53 assy xxx (ist |> path_down_form ([L, R], a)) e (*of*);
13.54 (*======= end of scanning tacticals, a leaf =======*)
13.55 -"~~~~~ fun assy, args:"; val (((pt, p), ctxt, tac), ist, t) =
13.56 +"~~~~~ fun assy, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
13.57 (xxx, (ist |> path_down_form ([L, R], a)), e);
13.58 -val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) (get_rls ist) (get_subst ist) t (*of*);
13.59 +val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
13.60
13.61 val Ass (Rewrite_Set' _, _, _) = (*case*)
13.62 associate pt ctxt (m, stac) (*of*);
13.63 @@ -99,31 +99,31 @@
13.64 (*if*) member op = [Pbl, Met] p_ = false;
13.65
13.66 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
13.67 -e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
13.68 + e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
13.69 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);
13.70 val thy' = get_obj g_domID pt (par_pblobj pt p);
13.71 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.72 + val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.73
13.74 val (_, _, _) =
13.75 determine_next_tactic (thy', srls) (pt, pos) sc is;
13.76 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, ctxt))
13.77 +"~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _))
13.78 = ((thy', srls), (pt, pos), sc, is);
13.79
13.80 val Appy (Rewrite_Set' _, _) = (*case*)
13.81 - execute_progr_1 thy ptp sc (Istate.Pstate ist) (*of*);
13.82 -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate ist))
13.83 - = (thy, ptp, sc, (Istate.Pstate ist));
13.84 - (*if*) 0 = length (get_path ist) (*else*);
13.85 + execute_progr_1 (sc, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
13.86 +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...})))
13.87 + = ((sc, (ptp, ctxt)), (Istate.Pstate ist));
13.88 + (*if*) 0 = length path (*else*);
13.89
13.90 val Appy (Rewrite_Set' _, _) =
13.91 - nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_);
13.92 -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) =
13.93 - ((sc, (ptp, (fst thy))), (trans_scan_up2 ist |> upd_appy Skip_));
13.94 - (*if*) 1 < length (get_path ist) (*then*);
13.95 + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_);
13.96 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...})) =
13.97 + ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_));
13.98 + (*if*) 1 < length path (*then*);
13.99
13.100 - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc);
13.101 + nxt_up yyy (ist |> path_up) (go_up path sc);
13.102 "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) =
13.103 - (yyy, (ist |> path_up), (go_up (get_path ist) sc));
13.104 + (yyy, (ist |> path_up), (go_up path sc));
13.105
13.106 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
13.107
13.108 @@ -158,51 +158,54 @@
13.109 val thy' = get_obj g_domID pt (par_pblobj pt p);
13.110 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.111
13.112 + val (_, _, _) =
13.113 determine_next_tactic (thy', srls) (pt, pos) sc is;
13.114 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, ctxt))
13.115 +"~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _))
13.116 = ((thy', srls), (pt, pos), sc, is);
13.117
13.118 val Appy (_, _) = (*case*)
13.119 - execute_progr_1 thy ptp sc (Istate.Pstate ist) (*of*);
13.120 -"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.Pstate ist))
13.121 - = (thy, ptp, sc, (Istate.Pstate ist));
13.122 - (*if*) 0 = length (get_path ist) (*else*);
13.123 + execute_progr_1 (sc, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
13.124 +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...})))
13.125 + = ((sc, (ptp, ctxt)), (Istate.Pstate ist));
13.126 + (*if*) 0 = length path (*else*);
13.127
13.128 - nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_);
13.129 -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist)
13.130 - = ((sc, (ptp, (fst thy))), (trans_scan_up2 ist |> upd_appy Skip_));
13.131 - (*if*) 1 < length (get_path ist) (*then*);
13.132 + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_);
13.133 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}))
13.134 + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_));
13.135 + (*if*) 1 < length path (*then*);
13.136
13.137 - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc);
13.138 + nxt_up yyy (ist |> path_up) (go_up path sc);
13.139 "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*1*),_) $ _ ))
13.140 - = (yyy, (ist |> path_up), (go_up (get_path ist) sc));
13.141 + = (yyy, (ist |> path_up), (go_up path sc));
13.142
13.143 nstep_up yyy (ist |> upd_appy Skip_);
13.144 -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist)
13.145 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}))
13.146 = (yyy, (ist |> upd_appy Skip_));
13.147 - (*if*) 1 < length (get_path ist) (*then*);
13.148 + (*if*) 1 < length path (*then*);
13.149
13.150 - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc);
13.151 + nxt_up yyy (ist |> path_up) (go_up path sc);
13.152 "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _))
13.153 - = (yyy, (ist |> path_up), (go_up (get_path ist) sc));
13.154 + = (yyy, (ist |> path_up), (go_up path sc));
13.155
13.156 nstep_up yyy ist;
13.157 -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) = (yyy, ist);
13.158 - (*if*) 1 < length (get_path ist) (*then*);
13.159 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}))
13.160 + = (yyy, ist);
13.161 + (*if*) 1 < length path (*then*);
13.162
13.163 - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc);
13.164 + nxt_up yyy (ist |> path_up) (go_up path sc);
13.165 "~~~~~ fun nxt_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _))
13.166 - = (yyy, (ist |> path_up), (go_up (get_path ist) sc));
13.167 + = (yyy, (ist |> path_up), (go_up path sc));
13.168
13.169 nstep_up yyy ist;
13.170 -"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), ist) = (yyy, ist);
13.171 - (*if*) 1 < length (get_path ist) (*then*);
13.172 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}))
13.173 + = (yyy, ist);
13.174 + (*if*) 1 < length path (*then*);
13.175
13.176 - nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc);
13.177 -"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), ist, (Const ("HOL.Let"(*1*), _) $ _))
13.178 - = (yyy, (ist |> path_up), (go_up (get_path ist) sc));
13.179 - (*if*) get_fini ist = Napp_ (*else*);
13.180 - val (i, body) = check_Let_up (get_path ist) sc;
13.181 + nxt_up yyy (ist |> path_up) (go_up path sc);
13.182 +"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
13.183 + = (yyy, (ist |> path_up), (go_up path sc));
13.184 + (*if*) finish = Napp_ (*else*);
13.185 + val (i, body) = check_Let_up ist sc;
13.186
13.187 (*case*) appy xxx (ist |> path_up_down [R, D] |> upd_env' i) body (*of*);
13.188 "~~~~~ fun appy , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))
13.189 @@ -211,9 +214,9 @@
13.190 val Appy (Subproblem' _, _) = (*case*)
13.191 appy xxx (ist |> path_down [L, R]) e (*of*);
13.192 (*========== a leaf has been found ==========*)
13.193 -"~~~~~ fun appy , args:"; val (((pt, p), ctxt), ist, t)
13.194 +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
13.195 = (xxx, (ist |> path_down [L, R]), e);
13.196 - val (a', STac stac) = (*case*) Lucin.handle_leaf "next " ctxt (get_rls ist) (get_subst ist) t (*of*);
13.197 + val (a', STac stac) = (*case*) Lucin.handle_leaf "next " ctxt eval (get_subst ist) t (*of*);
13.198
13.199 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac;
13.200 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
14.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Nov 04 11:40:29 2019 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Nov 06 15:08:27 2019 +0100
14.3 @@ -40,67 +40,64 @@
14.4 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
14.5 "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
14.6 = (sc, (pt, po), (fst is), (snd is), m);
14.7 - val srls = get_simplifier cstate;
14.8
14.9 - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
14.10 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
14.11 - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
14.12 - (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
14.13 - (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
14.14 -(*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
14.15 - (astep_up (thy',srls,scr,d) ((E,l,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]) );*)
14.16 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
14.17 - = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,asap,S,b), m));
14.18 - (*if*) 1 < length l (*true*);
14.19 -val up = drop_last l;
14.20 + val Assoc (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
14.21 + execute_progr_2 (progr, (cstate, ctxt, tac)) istate (*of*);
14.22 +"~~~~~ fun execute_progr_2 , args:"; val ((scr as Rule.Prog sc, (cctt as ((_, p), _, _))),
14.23 + (Istate.Pstate (ist as {path, ...})))
14.24 + = ( (progr, (cstate, ctxt, tac)), istate);
14.25 + (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
14.26
14.27 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
14.28 -"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) =
14.29 - (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
14.30 - astep_up ysa iss;
14.31 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
14.32 - (*if*) 1 < length l; (*then*)
14.33 - val up = drop_last l;
14.34 + astep_up (scr, cctt) ist;
14.35 +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
14.36 + = ((scr, cctt), ist);
14.37 + (*if*) 1 < length path (*true*);
14.38
14.39 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
14.40 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
14.41 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
14.42 +"~~~~~ fun ass_up, args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
14.43 + = (yyy, (ist |> path_up), (go (path_up' path) sc));
14.44
14.45 - astep_up ysa iss (*2*: comes from e2*);
14.46 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
14.47 - (*if*) 1 < length l; (*then*)
14.48 - val up = drop_last l;
14.49 + astep_up yyy ist;
14.50 +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
14.51 + = (yyy, ist);
14.52 + (*if*) 1 < length path (*true*);
14.53
14.54 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
14.55 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
14.56 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
14.57 +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*2*), _) $ _ $ _))
14.58 + = (yyy, (ist |> path_up), (go (path_up' path) sc));
14.59
14.60 - astep_up ysa iss (*all has been done in (*2*) below*);
14.61 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
14.62 - (*if*) 1 < length l; (*then*)
14.63 - val up = drop_last l;
14.64 + astep_up yyy ist (*2*: comes from e2*);
14.65 +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
14.66 + = (yyy, ist);
14.67 + (*if*) 1 < length path (*true*);
14.68
14.69 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
14.70 -"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ _))
14.71 - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
14.72 - val l = drop_last l; (*comes from e, goes to Abs*)
14.73 - val (i, T, body) =
14.74 - (case go l sc of
14.75 - Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
14.76 - | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t))
14.77 - val i = TermC.mk_Free (i, T);
14.78 - val E = Env.upd_env E (i, v);
14.79 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
14.80 +"~~~~~ fun ass_up , args:"; val (yyy, ist, (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _))
14.81 + = (yyy, (ist |> path_up), (go (path_up' path) sc));
14.82
14.83 - (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss) body (*of*);
14.84 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
14.85 - = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss), body);
14.86 + astep_up yyy ist (*all has been done in (*2*) below*);
14.87 +"~~~~~ and astep_up, args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {path, ...}))
14.88 + = (yyy, ist);
14.89 + (*if*) 1 < length path (*true*);
14.90
14.91 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss) e (*of*);
14.92 + ass_up yyy (ist |> path_up) (go (path_up' path) sc);
14.93 +"~~~~~ fun ass_up , args:"; val ((yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))
14.94 + = ( yyy, (ist |> path_up), (go (path_up' path) sc));
14.95 + val (i, body) = check_Let_up ist p
14.96 +;
14.97 + (*case*) assy xxx (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef) body (*of*);
14.98 +"~~~~~ fun assy , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
14.99 + = (xxx, (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef), body);
14.100 +
14.101 + (*case*) assy xxx (ist |> path_down [L, R]) e (*of*);
14.102 (*======= end of scanning tacticals, a leaf =======*)
14.103 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
14.104 - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss), e);
14.105 +"~~~~~ fun assy , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
14.106 + = (xxx, (ist |> path_down [L, R]), e);
14.107
14.108 -(*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
14.109 +val (NONE, STac _) = (*case*)
14.110 + handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
14.111 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
14.112 - = ("locate", "Isac_Knowledge", sr, (E, (a, v)), t);
14.113 + = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t);
14.114
14.115 val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
14.116 "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
15.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Nov 04 11:40:29 2019 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Nov 06 15:08:27 2019 +0100
15.3 @@ -36,51 +36,51 @@
15.4 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.5
15.6 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
15.7 - val ("ok", (_, _, (pt'''', p''''))) =
15.8 - (*case*) locatetac tac (pt, p) (*of*);
15.9 + val ("ok", (_, _, (pt'''', p''''))) = (*case*)
15.10 +
15.11 + locatetac tac (pt, p) (*of*);
15.12 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
15.13 val (mI,m) = mk_tac'_ tac;
15.14 val Appl m = (*case*) applicable_in p pt m (*of*);
15.15 member op = specsteps mI; (*else*)
15.16
15.17 - loc_solve_ (mI, m) ptp;
15.18 + loc_solve_ (mI, m) ptp;
15.19 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
15.20
15.21 solve m (pt, pos);
15.22 "~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
15.23 = (m, (pt, pos));
15.24 - val {srls, ...} = get_met mI;
15.25 - val PblObj {meth=itms, ...} = get_obj I pt p;
15.26 - val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.27 - val thy' = get_obj g_domID pt p;
15.28 - val thy = assoc_thy thy';
15.29 - val srls = Lucin.get_simplifier (pt, pos)
15.30 - val (is as Pstate (env,_,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
15.31 - (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
15.32 + val itms = case get_obj I pt p of
15.33 + PblObj {meth=itms, ...} => itms
15.34 + | _ => error "solve Apply_Method: uncovered case get_obj"
15.35 + val thy' = get_obj g_domID pt p;
15.36 + val thy = Celem.assoc_thy thy';
15.37 + val srls = Lucin.get_simplifier (pt, pos)
15.38 + val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
15.39 + (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
15.40 + | _ => error "solve Apply_Method: uncovered case init_pstate"
15.41
15.42 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
15.43 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
15.44 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.45
15.46 -
15.47 "~~~~~ from solve to..to me return"; val (pt, p) = (pt'''', p'''');
15.48
15.49 - (*case*) step p ((pt, e_pos'), []) (*of*);
15.50 + val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*)
15.51 + step p ((pt, e_pos'), []) (*of*);
15.52 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p'''', ((pt'''', e_pos'), []))
15.53 val pIopt = get_pblID (pt,ip);
15.54 tacis; (*= []*)
15.55 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
15.56 -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
15.57 +
15.58 +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
15.59 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.60 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
15.61 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
15.62 - (Pstate (ist as (E,l,rls,a,v,asap,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.63 +
15.64 +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
15.65 + = ((thy',srls), (pt,pos), sc, is);
15.66
15.67 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.68 -
15.69 -(*+*)val Appy (xxx, _) = appy thy ptp ist body;
15.70 -(*+*)if l = [] andalso tac_2str xxx = "Rewrite_Set_Inst' "
15.71 -then () else error "Minisubpbl/400-start-meth-subpbl changed -1";
15.72 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
15.73
15.74 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
16.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Nov 04 11:40:29 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Nov 06 15:08:27 2019 +0100
16.3 @@ -33,46 +33,52 @@
16.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
16.5 val (pt''''', p''''') = (pt, p);
16.6
16.7 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
16.8 +"~~~~~ fun me , args:"; val (_,tac) = nxt;
16.9 val (pt, p) = case locatetac tac (pt,p) of
16.10 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
16.11 val (pt'''', p'''') = (pt, p);
16.12 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
16.13 +"~~~~~ fun step , args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
16.14 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
16.15 -tacis; (*= []*)
16.16 -val SOME pI = pIopt;
16.17 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
16.18 -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
16.19 + (*if*) tacis; (*= []*)
16.20 + val SOME pI = pIopt;
16.21 + (*if*) member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
16.22 +
16.23 +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
16.24 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
16.25 val thy' = get_obj g_domID pt (par_pblobj pt p);
16.26 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
16.27 -val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
16.28 -;tac_; (* = Check_Postcond' *)
16.29 +val (tac_,is, (t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
16.30 +
16.31 +(*+*);tac_; (* = Check_Postcond' *)
16.32 +
16.33 "~~~~~ fun begin_end_prog, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
16.34 (tac_, is, ptp);
16.35 - val pp = par_pblobj pt p
16.36 - val asm =
16.37 - (case get_obj g_tac pt p of
16.38 - Check_elementwise _ => (*collects and instantiates asms*)
16.39 - (snd o (get_obj g_result pt)) p
16.40 - | _ => get_assumptions_ pt (p,p_))
16.41 - handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
16.42 - val metID = get_obj g_metID pt pp;
16.43 - val {srls=srls,scr=sc,...} = get_met metID;
16.44 - val loc as (Pstate (E,l,rls,a,_,_,_,b), ctxt) = get_loc pt (p,p_);
16.45 - val thy' = get_obj g_domID pt pp;
16.46 - val thy = assoc_thy thy';
16.47 - val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc;
16.48 -;pp = []; (*false*)
16.49 - val ppp = par_pblobj pt (lev_up p);
16.50 - val thy' = get_obj g_domID pt ppp;
16.51 - val thy = assoc_thy thy';
16.52 - val metID = get_obj g_metID pt ppp;
16.53 - val {scr,...} = get_met metID;
16.54 - val (Pstate (E,l,rls,a,_,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
16.55 - val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
16.56 - val tac_ = Check_Postcond' (pI, (scval, asm))
16.57 - val is = Pstate (E,l,rls,a,scval,asap,Istate.Skip_,b);
16.58 + val pp = par_pblobj pt p
16.59 + val asm = (case get_obj g_tac pt p of
16.60 + Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
16.61 + | _ => get_assumptions_ pt (p, p_))
16.62 + val metID = get_obj g_metID pt pp;
16.63 + val {srls = srls, scr = sc, ...} = Specify.get_met metID;
16.64 + val (loc, pst, ctxt) = case get_loc pt (p, p_) of
16.65 + loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
16.66 + | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
16.67 + val thy' = get_obj g_domID pt pp;
16.68 + val thy = Celem.assoc_thy thy';
16.69 + val (_, _, (scval, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
16.70 +
16.71 + (*if*) pp = []; (*false*)
16.72 +
16.73 + val ppp = par_pblobj pt (lev_up p);
16.74 + val thy' = get_obj g_domID pt ppp;
16.75 + val thy = Celem.assoc_thy thy';
16.76 +
16.77 + val (pst', ctxt') = case get_loc pt (pp, Frm) of
16.78 + (Istate.Pstate pst', ctxt') => (pst', ctxt')
16.79 + | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
16.80 + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
16.81 + val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
16.82 + val is = Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
16.83 +;
16.84 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
16.85 (thy, tac_, (is, ctxt''), (pp, Res), pt);
16.86 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
17.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Nov 04 11:40:29 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Nov 06 15:08:27 2019 +0100
17.3 @@ -52,35 +52,46 @@
17.4 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
17.5 tacis; (*= []*)
17.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
17.7 -"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
17.8 -val thy' = get_obj g_domID pt (par_pblobj pt p);
17.9 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
17.10 -"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
17.11 -(Pstate (E,l,rls,a,v,asap,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
17.12 -val ctxt = get_ctxt pt pos
17.13 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
17.14 -l; (*= [R, R, D, L, R]*)
17.15 -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
17.16 -(thy, ptp, sc, E, l, Skip_, a, v);
17.17 -1 < length l; (*true*)
17.18 -val up = drop_last l;
17.19 -go up sc; (* = Const ("HOL.Let", *)
17.20 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
17.21 -(t as Const ("HOL.Let",_) $ _), a, v) =
17.22 -(thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
17.23 -ay = Napp_; (*false*)
17.24 -val up = drop_last l;
17.25 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
17.26 -val i = mk_Free (i, T);
17.27 -val E = Env.upd_env E (i, v);
17.28 -body; (*= Const ("Prog_Tac.Check'_elementwise"*)
17.29 -"~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
17.30 -(thy, ptp, E, (up@[R,D]), body, a, v);
17.31 -handle_leaf "next " th sr (E, (a, v)) t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*)
17.32 -val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t;
17.33 -"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $
17.34 -(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
17.35 -(*2011 changed ^^^^^ *)
17.36 +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
17.37 + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
17.38 + val thy' = get_obj g_domID pt (par_pblobj pt p);
17.39 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
17.40 +
17.41 + val (Check_elementwise' _, (Pstate _, _), _) =
17.42 + determine_next_tactic (thy', srls) (pt, pos) sc is;
17.43 +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
17.44 + = ((thy', srls), (pt, pos), sc, is);
17.45 +
17.46 + (*case*)
17.47 + execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) (*of*);
17.48 +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...})))
17.49 + = ((sc, (ptp, thy)), (Istate.Pstate ist));
17.50 + (*if*) 0 = length path (*else*);
17.51 +
17.52 + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_);
17.53 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}))
17.54 + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_));
17.55 + (*if*) 1 < length path (*then*);
17.56 +
17.57 + nxt_up yyy (ist |> path_up) (go_up path sc);
17.58 +"~~~~~ fun nxt_up , args:"; val ((yyy as (Rule.Prog sc, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
17.59 + = (yyy, (ist |> path_up), (go_up path sc));
17.60 + (*if*) finish = Napp_ (*else*);
17.61 + val (i, body) = check_Let_up ist sc;
17.62 +
17.63 + (*case*)
17.64 + appy xxx (ist |> path_up_down [R, D] |> upd_env' i) body (*of*);
17.65 + (*========== a leaf has been found ==========*)
17.66 +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
17.67 + = (xxx, (ist |> path_up_down [R, D] |> upd_env' i), body);
17.68 + val (a', STac stac) = (*case*)
17.69 + handle_leaf "next " ctxt eval (get_subst ist) t;
17.70 +
17.71 + val (Check_elementwise "Assumptions", Empty_Tac_) =
17.72 + stac2tac_ pt (Celem.assoc_thy ctxt) stac;
17.73 +"~~~~~ fun stac2tac_ , args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $
17.74 + (set as Const ("Set.Collect",_) $ Abs (_,_,pred))))
17.75 + = (pt, (assoc_thy th), stac);
17.76
17.77 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
17.78 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
18.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Nov 04 11:40:29 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Nov 06 15:08:27 2019 +0100
18.3 @@ -41,12 +41,14 @@
18.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18.7 +
18.8 if p = ([], Res)
18.9 then case nxt of ("End_Proof'", End_Proof') => ()
18.10 | _ => error "calculation not finished correctly 1"
18.11 else error "calculation not finished correctly 2";
18.12 show_pt pt; (* 11 lines with subpbl *)
18.13 ;
18.14 +
18.15 "----- no thy-context at result -----";
18.16 (** val p = ([], Res);
18.17 ** initContext 1 Thy_ p
18.18 @@ -99,18 +101,19 @@
18.19
18.20 show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)
18.21
18.22 -(* val (_,_, (pt'', _)) =*) complete_solve CompleteSubpbl [] (pt', pos')
18.23 -;
18.24 + complete_solve CompleteSubpbl [] (pt', pos');
18.25 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));
18.26 (*if*) p = ([], Res) (* = false*);
18.27 (*if*) member op = [Pbl,Met] p_ (* = false*);
18.28 -(*case*) do_solve_step ptp (*of*)
18.29 -;
18.30 -"~~~~~ and do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
18.31 -(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*);
18.32 +
18.33 +val ([(Rewrite_Inst (["(''bdv'', x)"], ("risolate_bdv_add", _)), _, _)], _, _) = (*case*)
18.34 + do_solve_step ptp (*of*);
18.35 +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
18.36 + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*);
18.37 val thy' = get_obj g_domID pt (par_pblobj pt p);
18.38
18.39 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
18.40 + val (srls, is, sc) =
18.41 + from_pblobj_or_detail' thy' (p,p_) pt;
18.42 "~~~~~ fun from_pblobj_or_detail' , args:"; val (_, (p, p_), pt) = (thy', (p,p_), pt);
18.43 (*if*) member op = [Pbl, Met] p_ (*else*);
18.44 val (pbl, p', rls') = par_pbl_det pt p;
18.45 @@ -120,47 +123,49 @@
18.46
18.47 (*+*)id_rls rls' = "isolate_bdv";
18.48 "~~~~~ from from_pblobj_or_detail' to do_solve_step return val:"; val () = ();
18.49 -(* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
18.50 -;
18.51 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
18.52 - (Istate.Pstate (ist as (E,l,rls,a,v,asap,s,_)), ctxt)) = ((thy', srls), (pt, pos), sc, is);
18.53 -(*if*) l = [] (* = true *);
18.54
18.55 - appy thy ptp ist body;
18.56 -"~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("Tactical.Repeat"(*2*),_) $ e), a, v) =
18.57 -(thy, ptp, E, [Celem.R], body, NONE, v);
18.58 + val (Rewrite_Inst' (_, _, _, _, _, ("risolate_bdv_add", _), _, _), is, (t, _)) =
18.59 + determine_next_tactic (thy', srls) (pt, pos) sc is;
18.60 +"~~~~~ fun determine_next_tactic , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
18.61 + = ((thy', srls), (pt, pos), sc, is);
18.62
18.63 - appy thy ptp ist e;
18.64 -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Seq"(*1*),_) $ e1 $ e2 $ a)) =
18.65 - (thy, ptp, ist, e);
18.66 + (*case*)
18.67 + execute_progr_1 (sc, (ptp, thy)) (Istate.Pstate ist) (*of*);
18.68 +"~~~~~ fun execute_progr_1 , args:"; val ((sc as Rule.Prog prog, cct), (Istate.Pstate (ist as {path, ...})))
18.69 + = ((sc, (ptp, thy)), (Istate.Pstate ist));
18.70 + (*if*) 0 = length path (*else*);
18.71
18.72 - (*case*) appy thy ptp (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
18.73 -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Try"(*2*),_) $ e)) =
18.74 - (thy, ptp, (ist |> path_down_form ([L, L, R], a)), e1);
18.75 + nstep_up (sc, cct) (trans_scan_up2 ist |> upd_appy Skip_);
18.76 +"~~~~~ and nstep_up , args:"; val ((yyy as (Rule.Prog sc, _)), (ist as {env, path, finish, ...}) )
18.77 + = ((sc, cct), (trans_scan_up2 ist |> upd_appy Skip_));
18.78 + (*if*) 1 < length path (*then*);
18.79
18.80 - (*case*) appy thy ptp (ist |> path_down [R]) e (*of*);
18.81 -"~~~~~ fun appy , args:"; val (thy, ptp, ist, (Const ("Tactical.Repeat"(*2*),_) $ e)) =
18.82 - (thy, ptp, (ist |> path_down [R]), e);
18.83 + nxt_up yyy (ist |> path_up) (go_up path sc);
18.84 +"~~~~~ fun nxt_up , args:"; val ((yyy as (_, xxx)), ist, (Const ("Tactical.Repeat"(*2*), _) $ e))
18.85 + = (yyy, (ist |> path_up), (go_up path sc));
18.86
18.87 + (*case*)
18.88 + appy xxx (ist |> path_down [R]) e (*of*);
18.89 (*========== a leaf has been found ==========*)
18.90 - appy thy ptp (ist |> path_down [R]) e;
18.91 -"~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
18.92 - (thy, ptp, E, (l @ [Celem.R]), e, a, v);
18.93 +"~~~~~ fun appy , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
18.94 + = (xxx, (ist |> path_down [R]), e);
18.95
18.96 val (a', STac stac) =
18.97 (*case*) handle_leaf "next " th sr (get_subst ist) t (*of*);
18.98 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (get_subst ist), t);
18.99 +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
18.100 + = ("next ", th, sr, (get_subst ist), t);
18.101 +
18.102 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),
18.103 (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*)
18.104
18.105 (*+*)val TFree ("'z", ["HOL.type"]) = Tt_t;
18.106 -(*+*)val Type ("Real.real",[]) = Tv;
18.107 -(*+*)val Type ("Real.real",[]) = Tx;
18.108 +(*+*)val Type ("Real.real", []) = Tv;
18.109 +(*+*)val Type ("Real.real", []) = Tx;
18.110
18.111 (*+*)val SOME (Const ("empty", Ta)) = a;
18.112 -(*+*)val Type ("'a",[]) = Ta;
18.113 -(*+*)val Const ("empty", Tv) = v;
18.114 -(*+*)val Type ("'a",[]) = Tv;
18.115 +(*+*)val Type ("'a", []) = Ta;
18.116 +(*+*)if term2str v = "x = 0 + -1 * -1" then () else error "handle_leaf changed";
18.117 +(*+*)val Type ("Real.real", []) = Tv;
18.118
18.119 (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
18.120 "~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)))
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml Wed Nov 06 15:08:27 2019 +0100
19.3 @@ -0,0 +1,47 @@
19.4 +(* Title: "Minisubpbl/799-complete.sml"
19.5 + Author: Walther Neuper 1105
19.6 + (c) copyright due to lincense terms.
19.7 +*)
19.8 +"----------- Minisubpbl/799-complete.sml -------------------------";
19.9 +"----------- Minisubpbl/799-complete.sml -------------------------";
19.10 +"----------- Minisubpbl/799-complete.sml -------------------------";
19.11 + val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
19.12 + val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
19.13 + ["Test","squ-equ-test-subpbl1"]);
19.14 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.15 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.16 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.17 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.18 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.19 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.20 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.21 + (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
19.22 + (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
19.23 + (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
19.24 + (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
19.25 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
19.26 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
19.27 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
19.28 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
19.29 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
19.30 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
19.31 + (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
19.32 + (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
19.33 + (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
19.34 + (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
19.35 + (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
19.36 + (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
19.37 + (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
19.38 + (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
19.39 +
19.40 + (* final test ...*)
19.41 + if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
19.42 + andalso pr_ctree pr_short pt =
19.43 + ". ----- pblobj -----\n" ^
19.44 + "1. x + 1 = 2\n" ^
19.45 + "2. x + 1 + -1 * 2 = 0\n" ^
19.46 + "3. ----- pblobj -----\n" ^
19.47 + "3.1. -1 + x = 0\n" ^
19.48 + "3.2. x = 0 + -1 * -1\n" ^
19.49 + "4. [x = 1]\n"
19.50 + then () else error "re-build: fun locate_input_tactic changed";
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/test/Tools/isac/Minisubpbl/791-complete-NEXT_STEP.sml Wed Nov 06 15:08:27 2019 +0100
20.3 @@ -0,0 +1,59 @@
20.4 +(* Title: "Minisubpbl/791-complete-NEXT_STEP.sml"
20.5 + Author: Walther Neuper 1105
20.6 + (c) copyright due to lincense terms.
20.7 +*)
20.8 +
20.9 +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------";
20.10 +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------";
20.11 +"----------- Minisubpbl/791-complete-NEXT_STEP.sml --------------------------------------------";
20.12 +
20.13 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
20.14 +val (dI',pI',mI') =
20.15 + ("Test", ["sqroot-test","univariate","equation","test"],
20.16 + ["Test","squ-equ-test-subpbl1"]);
20.17 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.18 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Model_Problem*)
20.19 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Specify_Theory*)
20.20 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
20.21 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
20.22 +(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
20.23 +(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
20.24 +(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
20.25 +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
20.26 +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Model_Problem*)
20.27 +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
20.28 +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
20.29 +(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
20.30 +(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
20.31 +(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
20.32 +(*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
20.33 +(*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
20.34 +
20.35 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*)
20.36 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)
20.37 +(* there are questionable assumptions either ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
20.38 +
20.39 +(*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)
20.40 +
20.41 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*)
20.42 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"precond_rootmet 1\"]";(*REP*)
20.43 +
20.44 +(*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
20.45 +
20.46 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[]";(*isa*)
20.47 +((get_obj g_result pt (fst p)) |> snd |> terms2str) = "[\"precond_rootmet 1\"]";(*REP*)
20.48 +
20.49 +(*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
20.50 +
20.51 +(*/--------------------- final test ----------------------------------\\*)
20.52 +val (res, asm) = (get_obj g_result pt (fst p));
20.53 +
20.54 +if term2str res = "[x = 1]" andalso terms2str asm = "[]"
20.55 +then () else error "Minisubpbl/791-complete-NEXT_STEP.sml, determine_next_tactic CHANGED";
20.56 +
20.57 +if p = ([], Und)
20.58 +then
20.59 + case get_obj g_tac pt (fst p) of
20.60 + Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
20.61 + | _ => error "Minisubpbl/791-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"
20.62 +else error "Minisubpbl/791-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1"
21.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Nov 04 11:40:29 2019 +0100
21.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Nov 06 15:08:27 2019 +0100
21.3 @@ -28,7 +28,7 @@
21.4
21.5 (*
21.6 > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
21.7 -> val eval_fn = the (assoc (!eval_list, "pow"));
21.8 +> val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
21.9 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
21.10 > Syntax.string_of_term (thy2ctxt thy) t';
21.11 *)
22.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Nov 04 11:40:29 2019 +0100
22.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Nov 06 15:08:27 2019 +0100
22.3 @@ -121,7 +121,7 @@
22.4 ie. cancel does not work properly
22.5 *)
22.6 val thy = @{theory "Test"};
22.7 - val op_ = the (assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
22.8 + val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
22.9 val ct = numbers_to_string @{term
22.10 "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
22.11 case calculate_ thy op_ ct of
22.12 @@ -247,32 +247,32 @@
22.13
22.14 val thy = @{theory Test};
22.15 val t = (Thm.term_of o the o (parse thy)) "12 / 3";
22.16 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.17 +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.18 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.19 "12 / 3 = 4";
22.20 val thy = @{theory Test};
22.21 val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
22.22 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.23 +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.24 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.25 "4 ^ 2 = 16";
22.26
22.27 val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
22.28 - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
22.29 + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
22.30 "1 + 2 = 3";
22.31 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.32 term2str t;
22.33 "(3 * 4 / 3) ^^^ 2";
22.34 - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
22.35 + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
22.36 "3 * 4 = 12";
22.37 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.38 term2str t;
22.39 "(12 / 3) ^^^ 2";
22.40 - val SOME (thmID,thm) =adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.41 + val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.42 "12 / 3 = 4";
22.43 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.44 term2str t;
22.45 "4 ^^^ 2";
22.46 - val SOME (thmID,thm) = adhoc_thm thy(the(assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
22.47 + val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
22.48 "4 ^^^ 2 = 16";
22.49 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.50 term2str t;
22.51 @@ -283,10 +283,10 @@
22.52 (*13.9.02 *** calc: operator = pow not defined*)
22.53 val t = (Thm.term_of o the o (parse thy)) "3^^^2";
22.54 val SOME (thmID,thm) =
22.55 - adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.56 + adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.57 (*** calc: operator = pow not defined*)
22.58
22.59 - val (op_, eval_fn) = the (assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
22.60 + val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
22.61 (*
22.62 val op_ = "Prog_Expr.pow" : string
22.63 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
22.64 @@ -333,7 +333,7 @@
22.65 "----------- fun get_pair: examples ------------------------------------------------------------";
22.66 "----------- fun get_pair: examples ------------------------------------------------------------";
22.67 val thy = @{theory};
22.68 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.69 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.70
22.71 val t = (Thm.term_of o the o (parse thy)) "3 + 4";
22.72 val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.73 @@ -355,14 +355,14 @@
22.74 if str = "#: 3 + (4 + a) = 7 + a" andalso term2str term = "3 + (4 + a) = 7 + a"
22.75 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
22.76
22.77 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.78 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.79
22.80 val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
22.81 val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.82 if str = "#divide_e-4_-2" andalso term2str term = "-4 / -2 = 2"
22.83 then () else error "get_pair -4 / -2 changed";
22.84
22.85 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
22.86 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
22.87
22.88 val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
22.89 val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.90 @@ -373,7 +373,7 @@
22.91 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.92 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.93 (*--------------------------------------------------------------------vvvvvvvvvv*)
22.94 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
22.95 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
22.96 val SOME t = parseNEW @{context} "9 is_const";
22.97 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.98 if str = "#is_const_9_" andalso thm2str thm = "(9 is_const) = True"
22.99 @@ -383,7 +383,7 @@
22.100 case assoc_calc thy "Orderings.ord_class.less" of
22.101 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
22.102 (*--------------------------------------------------------------------vvvvvvvvvv*)
22.103 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "le");
22.104 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
22.105
22.106 val SOME t = parseNEW @{context} "4 < 4";
22.107 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.108 @@ -396,14 +396,14 @@
22.109
22.110
22.111 (*--------------------------------------------------------------------vvvvvvvvvv*)
22.112 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.113 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.114 val SOME t = parseNEW @{context} "1 + 2";
22.115 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.116 if str = "#: 1 + 2 = 3" andalso thm2str thm = "1 + 2 = 3"
22.117 then () else error "adhoc_thm 1 + 2 changed";
22.118
22.119 (*--------------------------------------------------------------------vvvvvvvvvv*)
22.120 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.121 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.122 val SOME t = parseNEW @{context} "6 / -8";
22.123 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.124 if str = "#divide_e6_-8" andalso thm2str thm = "6 / -8 = -3 / 4"
22.125 @@ -413,7 +413,7 @@
22.126 case assoc_calc thy "Prog_Expr.ident" of
22.127 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
22.128 (*--------------------------------------------------------------------vvvvvvvvvv*)
22.129 -val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "ident");
22.130 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
22.131
22.132 val SOME t = parseNEW @{context} "3 =!= 3";
22.133 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
23.1 --- a/test/Tools/isac/Specify/calchead.sml Mon Nov 04 11:40:29 2019 +0100
23.2 +++ b/test/Tools/isac/Specify/calchead.sml Wed Nov 06 15:08:27 2019 +0100
23.3 @@ -601,9 +601,9 @@
23.4 (*[x+1=2, x] OLD: [x+1=2, x] : term list*)
23.5 vars' ~~ vals;
23.6 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
23.7 -(assoc (vars'~~vals, cy'));
23.8 +(LibraryC.assoc (vars'~~vals, cy'));
23.9 (*SOME (Free ("x", "Real.real")) : term option*)
23.10 - val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
23.11 + val cy_ext = (free2str o the) (LibraryC.assoc (vars'~~vals, cy'))^"_"^ext;
23.12 (*x_i*)
23.13 "-----------------continue step through code match_ags---";
23.14 val cy' = map (cpy_nam pbt' oris') cy;
24.1 --- a/test/Tools/isac/Test_Isac.thy Mon Nov 04 11:40:29 2019 +0100
24.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 06 15:08:27 2019 +0100
24.3 @@ -54,7 +54,7 @@
24.4 "~~~~~ from xxx to yyy return val:"; val () = ();
24.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
24.6 "xx"
24.7 -^ "xxx" (*+*)
24.8 +^ "xxx" (*+*) (*isa*) (*REP*)
24.9 \<close>
24.10 section \<open>Run the tests\<close>
24.11 text \<open>
24.12 @@ -193,7 +193,8 @@
24.13 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
24.14 ML_file "Minisubpbl/600-postcond.sml"
24.15 ML_file "Minisubpbl/700-interSteps.sml"
24.16 - ML_file "Minisubpbl/799-complete.sml"
24.17 + ML_file "Minisubpbl/790-complete.sml"
24.18 + ML_file "Minisubpbl/791-complete-NEXT_STEP.sml"
24.19
24.20 subsection \<open>further functionality alongside batch build sequence\<close>
24.21 ML_file "MathEngBasic/model.sml"
25.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Nov 04 11:40:29 2019 +0100
25.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Nov 06 15:08:27 2019 +0100
25.3 @@ -193,7 +193,8 @@
25.4 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
25.5 ML_file "Minisubpbl/600-postcond.sml"
25.6 ML_file "Minisubpbl/700-interSteps.sml"
25.7 - ML_file "Minisubpbl/799-complete.sml"
25.8 + ML_file "Minisubpbl/790-complete.sml"
25.9 + ML_file "Minisubpbl/791-complete-NEXT_STEP.sml"
25.10
25.11 subsection \<open>further functionality alongside batch build sequence\<close>
25.12 ML_file "MathEngBasic/model.sml"
25.13 @@ -212,6 +213,7 @@
25.14 ML_file "Interpret/script.sml"
25.15 ML_file "Interpret/inform.sml"
25.16 ML_file "Interpret/lucas-interpreter.sml"
25.17 +
25.18 ML_file "MathEngine/solve.sml"
25.19 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
25.20 ML_file "MathEngine/messages.sml"
26.1 --- a/test/Tools/isac/Test_Some.thy Mon Nov 04 11:40:29 2019 +0100
26.2 +++ b/test/Tools/isac/Test_Some.thy Wed Nov 06 15:08:27 2019 +0100
26.3 @@ -79,596 +79,15 @@
26.4 "~~~~~ fun xxx , args:"; val () = ();
26.5 \<close>
26.6
26.7 -section \<open>===============--- test/../lucas-interpreter.sml ----================\<close>
26.8 +section \<open>===================================================================================\<close>
26.9 ML \<open>
26.10 "~~~~~ fun xxx , args:"; val () = ();
26.11 \<close> ML \<open>
26.12 -(* Title: "Interpret/lucas-interpreter.sml"
26.13 - Author: Walther Neuper
26.14 - (c) due to copyright terms
26.15 -*)
26.16 -
26.17 -"-----------------------------------------------------------------------------------------------";
26.18 -"table of contents -----------------------------------------------------------------------------";
26.19 -"-----------------------------------------------------------------------------------------------";
26.20 -"----------- Take as 1st stac in program -------------------------------------------------------";
26.21 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.22 -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
26.23 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
26.24 -"----------- re-build: fun locate_input_formula ------------------------------------------------";
26.25 -"-----------------------------------------------------------------------------------------------";
26.26 -"-----------------------------------------------------------------------------------------------";
26.27 -"-----------------------------------------------------------------------------------------------";
26.28 -
26.29 -"----------- Take as 1st stac in program -------------------------------------------------------";
26.30 -"----------- Take as 1st stac in program -------------------------------------------------------";
26.31 -"----------- Take as 1st stac in program -------------------------------------------------------";
26.32 -val p = e_pos'; val c = [];
26.33 -val (p,_,f,nxt,_,pt) =
26.34 - CalcTreeTEST
26.35 - [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
26.36 - ("Integrate", ["integrate","function"], ["diff","integration"]))];
26.37 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
26.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.40 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.41 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.43 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.44 -case nxt of (_, Apply_Method ["diff", "integration"]) => ()
26.45 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
26.46 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
26.47 -
26.48 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
26.49 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
26.50 -val (mI,m) = mk_tac'_ tac;
26.51 -val Appl m = applicable_in p pt m;
26.52 -member op = specsteps mI (*false*);
26.53 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
26.54 -"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
26.55 - (m, (pt, pos));
26.56 -val {srls, ...} = get_met mI;
26.57 - val PblObj {meth=itms, ...} = get_obj I pt p;
26.58 - val thy' = get_obj g_domID pt p;
26.59 - val thy = assoc_thy thy';
26.60 - val srls = Lucin.get_simplifier (pt, pos)
26.61 - val (is as Istate.Pstate (ist as {env, ...}), ctxt, sc) = init_pstate srls ctxt itms mI;
26.62 - val ini = init_form thy sc env;
26.63 - val p = lev_dn p;
26.64 -
26.65 - val NONE = (*case*) ini (*of*);
26.66 - val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
26.67 - val d = e_rls (*FIXME: get simplifier from domID*);
26.68 -\<close> ML \<open>
26.69 -val Safe_Step _ = (*case*)
26.70 - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
26.71 -\<close> ML \<open>
26.72 -"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), cstate, istate, ctxt, tac) =
26.73 - (sc, (pt, (p, Res)), is', ctxt', m');
26.74 -
26.75 -\<close> ML \<open>
26.76 -(*val Assoc ((ist as {assoc, ...}), ctxt, tac') = ( *case*)
26.77 - execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*);
26.78 -\<close> ML \<open>
26.79 -"~~~~~ fun execute_progr_2 , args:"; val () = ();
26.80 -\<close> ML \<open>
26.81 -\<close> ML \<open>
26.82 -\<close> ML \<open>
26.83 -val thy = assoc_thy thy';
26.84 -l = [] orelse ((*init.in solve..Apply_Method...*)
26.85 - (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
26.86 -\<close> ML \<open>
26.87 -\<close> ML \<open>
26.88 -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,rls,a,v,asap,S,b),ss),
26.89 - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
26.90 - ((thy',ctxt,srls,d,Aundef), ((E,[R],rls,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]), body);
26.91 - (*check: true*) term2str e = "Take (Integral f_f D v_v)";
26.92 -\<close> ML \<open>
26.93 -\<close> ML \<open>
26.94 -"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,rls,a,v,asap,S,b), (m,_,pt,(p,p_),c)::ss), t) =
26.95 - (ya, ((E , l@[L,R], rls,a,v,asap,S,b),ss), e);
26.96 -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t;
26.97 -(* val ctxt = get_ctxt pt (p,p_)
26.98 -exception PTREE "get_obj: pos = [0] does not exist" raised
26.99 -(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
26.100 -
26.101 -
26.102 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.103 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.104 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.105 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
26.106 -val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
26.107 - ["Test","squ-equ-test-subpbl1"]);
26.108 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.110 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.111 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.112 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.113 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.114 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.115 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
26.116 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
26.117 -
26.118 -(*// relevant call --------------------------------------------------------------------------\\*)
26.119 -(*[1], Res* )val (*** )xxx( ***) (p,_,f,nxt,_,pt) =*) me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
26.120 -
26.121 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
26.122 -
26.123 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
26.124 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
26.125 - val (mI, m) = Solve.mk_tac'_ tac;
26.126 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
26.127 - (*if*) member op = Solve.specsteps mI; (*else*)
26.128 -
26.129 - (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
26.130 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
26.131 -
26.132 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
26.133 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
26.134 -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
26.135 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
26.136 - val thy' = get_obj g_domID pt (par_pblobj pt p);
26.137 - val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
26.138 -
26.139 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
26.140 -"~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
26.141 - = (sc, (pt, po), (fst is), (snd is), m);
26.142 - val srls = get_simplifier cstate;
26.143 -
26.144 - (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
26.145 - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
26.146 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
26.147 - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
26.148 - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
26.149 -
26.150 - (** )val xxxxx_xx = ( **)
26.151 - assy (ctxt,srls, (pt, p), Aundef) ((E,[Celem.R],rls,a,v,asap,S,b), m) (Program.body_of sc);
26.152 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,asap,S,b), tac), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
26.153 - = ((ctxt,srls, (pt, p), Aundef), ((E,[Celem.R],a,v,asap,S,b), m), (Program.body_of sc));
26.154 -
26.155 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac) e (*of*);
26.156 -"~~~~~ fun xxx , args:"; val (ya, ((E,l,rls,_,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $ e1 $ e2 $ a))
26.157 - = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), tac), e);
26.158 -
26.159 - (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss) e1 (*of*);
26.160 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e))
26.161 - = (ya, ((E, l @ [Celem.L, Celem.L, Celem.R], rls,SOME a,v,asap,S,b),ss), e1);
26.162 -
26.163 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
26.164 - (*======= end of scanning tacticals, a leaf =======*)
26.165 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
26.166 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
26.167 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
26.168 - val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
26.169 - (* 1st ContextC.insert_assumptions asms' ctxt *)
26.170 -
26.171 -(*NEW*) Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m) (*return value*);
26.172 -"~~~~~ from assy to execute_progr_2 return val:"; val (xxxxx_xx)
26.173 - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m)); (*return value*)
26.174 -
26.175 -"~~~~~ from execute_progr_2 to locate_input_tactic return val:"; val Assoc (is as (_,_,_,_,_,_,_,strong_ass), ctxt(*NEW*), tac')
26.176 - = (Assoc ((E,l,rls,a',v',asap,S,true), ctxt, m));
26.177 - (*if*) strong_ass; (*then*)
26.178 -
26.179 -"~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (istate, ctxt, tac)
26.180 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate is, ctxt, tac')(**);
26.181 -
26.182 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
26.183 -(*NEW*) val p' =
26.184 -(*NEW*) case p_ of Frm => p
26.185 -(*NEW*) | Res => lev_on p
26.186 -(*NEW*) | _ => error ("solve: call by " ^ pos'2str (p, p_));
26.187 -(*NEW*) val (p'', _, _,pt') =
26.188 -(*NEW*) Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m
26.189 -(*NEW*) (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
26.190 -(*NEW*) (Istate.Pstate (E,l,rls,a',v',asap,S,true), ctxt) (p', p_) pt;
26.191 -(*NEW*) (*in*)
26.192 -(*NEW*) ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
26.193 -(*NEW*) [(*ctree NOT cut*)], (pt', p'')));
26.194 -
26.195 -(*NEW*)("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [], (pt', p'')));
26.196 -"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
26.197 - = ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
26.198 -
26.199 -"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
26.200 - = (*** )xxxxx( ***) (Updated (cs'));
26.201 - (*if*) p' = ([], Ctree.Res); (*else*)
26.202 - ("ok", cs');
26.203 -"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
26.204 - val (_, ts) =
26.205 - (case step p ((pt, Ctree.e_pos'), []) of
26.206 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
26.207 - | ("helpless", _) => ("helpless: cannot propose tac", [])
26.208 - | ("no-fmz-spec", _) => error "no-fmz-spec"
26.209 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
26.210 - | _ => error "me: uncovered case")
26.211 - handle ERROR msg => raise ERROR msg
26.212 - val tac =
26.213 - case ts of
26.214 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
26.215 - | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
26.216 -
26.217 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
26.218 -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
26.219 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
26.220 -
26.221 -(*//--------------------- check results from modified me ----------------------------------\\*)
26.222 -if p = ([1], Res) andalso
26.223 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n"
26.224 -then
26.225 - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
26.226 - | _ => error "")
26.227 -else error "check results from modified me CHANGED";
26.228 -(*\\--------------------- check results from modified me ----------------------------------//*)
26.229 -
26.230 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
26.231 -(*\\------------------ end of modified "fun me" ---------------------------------------------//*)
26.232 -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
26.233 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
26.234 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
26.235 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
26.236 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
26.237 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
26.238 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
26.239 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
26.240 -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
26.241 -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
26.242 -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
26.243 -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
26.244 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
26.245 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
26.246 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
26.247 -
26.248 -(*/--------------------- final test ----------------------------------\\*)
26.249 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
26.250 - andalso pr_ctree pr_short pt =
26.251 - ". ----- pblobj -----\n" ^
26.252 - "1. x + 1 = 2\n" ^
26.253 - "2. x + 1 + -1 * 2 = 0\n" ^
26.254 - "3. ----- pblobj -----\n" ^
26.255 - "3.1. -1 + x = 0\n" ^
26.256 - "3.2. x = 0 + -1 * -1\n" ^
26.257 - "4. [x = 1]\n"
26.258 -then () else error "re-build: fun locate_input_tactic changed";
26.259 -
26.260 -
26.261 -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
26.262 -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
26.263 -"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
26.264 -(*cp from -- try fun applyTactics ------- *)
26.265 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
26.266 - "normalform N"],
26.267 - ("PolyMinus",["plus_minus","polynom","vereinfachen"],
26.268 - ["simplification","for_polynomials","with_minus"]))];
26.269 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.270 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.271 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.272 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
26.273 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
26.274 -
26.275 -(*+*)map tac2str (sel_appl_atomic_tacs pt p) =
26.276 - ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
26.277 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"];
26.278 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
26.279 -
26.280 -(*+*)map tac2str (sel_appl_atomic_tacs pt p) =
26.281 - ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
26.282 - "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
26.283 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"];
26.284 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
26.285 -
26.286 -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
26.287 -(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
26.288 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
26.289 - val (mI, m) = Solve.mk_tac'_ tac;
26.290 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
26.291 - (*if*) member op = Solve.specsteps mI (*else*);
26.292 -
26.293 - loc_solve_ (mI, m) ptp;
26.294 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
26.295 - solve m (pt, pos);
26.296 - (* ======== general case ======== *)
26.297 -"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
26.298 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
26.299 - val thy' = get_obj g_domID pt (par_pblobj pt p);
26.300 - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
26.301 -
26.302 - (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
26.303 -"~~~~~ fun locate_input_tactic , args:"; val ((progr as Rule.Prog _), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
26.304 - = (sc, (pt, po), (fst is), (snd is), m);
26.305 - val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
26.306 -
26.307 - (*case*) execute_progr_2 srls tac cstate (progr, Rule.e_rls) (istate, ctxt) (*of*);
26.308 -"~~~~~ fun execute_progr_2 , args:"; val (srls, m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
26.309 - = (srls, tac, cstate ,(progr, Rule.e_rls), (istate, ctxt));
26.310 - (*if*) l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
26.311 -
26.312 - astep_up (ctxt,srls,scr,(pt, p)) ((E,l,rls,a,v,asap,S,b), m);
26.313 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
26.314 - = ((ctxt,srls,scr,(pt, p)), ((E,l,a,v,asap,S,b), m));
26.315 - (*if*) 1 < length l (*then*);
26.316 - val up = drop_last l; (* = [R, L, R, L, R]*)
26.317 -
26.318 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
26.319 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Try"(*2*),_) $ _))
26.320 - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
26.321 -
26.322 - astep_up ysa iss;
26.323 -"~~~~~ fun astep_up , args:"; val (((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)))
26.324 - = (ysa, iss);
26.325 - (*if*) 1 < length l (*then*);
26.326 - val up = drop_last l; (* = [R, L, R, L]*)
26.327 -
26.328 - ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
26.329 -"~~~~~ fun ass_up , args:"; val ((ysa as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss),
26.330 - (Const ("Tactical.Seq"(*3*),_) $ _ ))
26.331 - = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
26.332 - val up = drop_last l;
26.333 - val Const ("Tactical.Seq",_) $ _ $ e2 = (*case*) go up sc (*of*);
26.334 -
26.335 - (*case*) assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss) e2 (*of*);
26.336 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Seq"(*2*),_) $e1 $ e2))
26.337 - = (((*y,*)ctxt,s,d,Aundef), ((E, up @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
26.338 - val NasApp ((E,_,_,_,v,_,_,_), ctxt(*NEW*), ss) = (*case*) assy ya ((E, l @ [Celem.L, Celem.R], rls,a,v,asap,S,b),ss) e1 (*of*);
26.339 -
26.340 - assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e2;
26.341 -"~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("Tactical.Try"(*2*),_) $ e))
26.342 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e2);
26.343 -
26.344 - (*case*) assy ya ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss) e (*of*);
26.345 - (*======= end of scanning tacticals, a leaf =======*)
26.346 -"~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
26.347 - = (ya, ((E, l @ [Celem.R], rls,a,v,asap,S,b),ss), e);
26.348 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
26.349 - val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
26.350 - val Aundef = (*case*) ap (*of*);
26.351 - val Appl m' = (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
26.352 - val is = (E,l,rls,a',Lucin.tac_2res m',asap,S,false(*FIXXXME.WN0?*));
26.353 - NasApp (is, ctxt, m) (* return value *);
26.354 -
26.355 -val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
26.356 - t, (res, asm)) = m;
26.357 -if scrstate2str is =
26.358 - "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], e_rls, SOMEt_t, \n" ^
26.359 - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
26.360 -andalso
26.361 - term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
26.362 -andalso
26.363 - term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
26.364 -andalso
26.365 - terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
26.366 -then () else error "locate_input_tactic Helpless, but applicable CHANGED";
26.367 -
26.368 -
26.369 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
26.370 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
26.371 -"----------- re-build: fun determine_next_tactic -----------------------------------------------";
26.372 -
26.373 -
26.374 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.375 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.376 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
26.377 \<close> ML \<open>
26.378 \<close> ML \<open>
26.379 "~~~~~ fun xxx , args:"; val () = ();
26.380 \<close>
26.381
26.382 -section \<open>=== --- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic --- =========\<close>
26.383 -ML \<open>
26.384 -\<close> ML \<open>
26.385 -\<close> ML \<open>
26.386 -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------";
26.387 -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------";
26.388 -"----------- Minisubpbl/251-Rewrite_Set-from-method.sml, determine_next_tactic ------ ----------";
26.389 -\<close> ML \<open>
26.390 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
26.391 -val (dI',pI',mI') =
26.392 - ("Test", ["sqroot-test","univariate","equation","test"],
26.393 - ["Test","squ-equ-test-subpbl1"]);
26.394 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.395 -\<close> ML \<open>
26.396 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.397 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.398 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.399 -(*([], Met)*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
26.400 -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
26.401 -\<close> ML \<open>
26.402 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
26.403 -
26.404 -(*// relevant call --------------------------------------------------------------------------\\*)
26.405 -\<close> ML \<open>
26.406 -"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
26.407 -\<close> ML \<open>
26.408 - val pIopt = get_pblID (pt,ip);
26.409 -\<close> ML \<open>
26.410 - (*if*) ip = ([], Ctree.Res) (*else*);
26.411 -\<close> ML \<open>
26.412 - val _ = (*case*) tacis (*of*);
26.413 -\<close> ML \<open>
26.414 - val SOME _ = (*case*) pIopt (*of*);
26.415 -\<close> ML \<open>
26.416 - (*if*) member op = [Ctree.Pbl, Ctree.Met] p_
26.417 - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
26.418 -\<close> ML \<open>
26.419 - do_solve_step (pt, ip);
26.420 -\<close> ML \<open>
26.421 -"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
26.422 -\<close> ML \<open>
26.423 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
26.424 -\<close> ML \<open>
26.425 - val thy' = get_obj g_domID pt (par_pblobj pt p);
26.426 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
26.427 -\<close> ML \<open>
26.428 - determine_next_tactic (thy', srls) (pt, pos) sc is;
26.429 - (* TODO here ^^^ return finished/helpless/ok ?*)
26.430 -\<close> ML \<open>
26.431 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))
26.432 - = ((thy', srls), (pt, pos), sc, is);
26.433 -\<close> ML \<open>
26.434 - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);
26.435 -\<close> ML \<open>
26.436 -"~~~~~ fun execute_progr_1 , args:"; val () = ();
26.437 -\<close> ML \<open>
26.438 -\<close> ML \<open>
26.439 -\<close> ML \<open>
26.440 -\<close> ML \<open>
26.441 -\<close> ML \<open>
26.442 -\<close> ML \<open>
26.443 -\<close> ML \<open>
26.444 -\<close> ML \<open>
26.445 -\<close> ML \<open>
26.446 -\<close> ML \<open>
26.447 -\<close> ML \<open>
26.448 -\<close> ML \<open>
26.449 -\<close> ML \<open>
26.450 -\<close> ML \<open>
26.451 -(*//--------------------- check results from modified step ----------------------------------\\*)
26.452 -(*\\--------------------- check results from modified step ----------------------------------//*)
26.453 -\<close> ML \<open>
26.454 -"~~~~~ from me to TOPLEVEL return:"; val () = (*** )xxx( ***) (**)()(**);
26.455 -(*\\------------------ end of modified "fun step" -------------------------------------------//*)
26.456 -\<close> ML \<open>
26.457 -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "Test_simplify"*)
26.458 -\<close> ML \<open>
26.459 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) =(**) step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
26.460 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(**)
26.461 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.462 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.463 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.464 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.465 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.466 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.467 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.468 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.469 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.470 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.471 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.472 -\<close> ML \<open>
26.473 -(**)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.474 -\<close> ML \<open>
26.475 -
26.476 -(*/--------------------- final test ----------------------------------\\*)
26.477 -\<close> ML \<open>
26.478 -val (res, asm) = (get_obj g_result pt (fst p));
26.479 -if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
26.480 -then () else error "Minisubpbl/301-init-subpbl.sml, determine_next_tactic CHANGED"
26.481 -
26.482 -\<close> ML \<open>
26.483 -if p = ([], Und)
26.484 -then
26.485 - case get_obj g_tac pt (fst p) of
26.486 - Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
26.487 - | _ => error "301-init-subpbl WRONG RESULT CHANGED 2"
26.488 -else error "301-init-subpbl WRONG RESULT CHANGED 1"
26.489 -\<close> ML \<open>
26.490 -\<close>
26.491 -
26.492 -section \<open>=== --- Minisubpbl/301-init-subpbl.sml, determine_next_tactic --- ======================\<close>
26.493 -ML \<open>
26.494 -\<close> ML \<open>
26.495 -\<close> ML \<open>
26.496 -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------";
26.497 -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------";
26.498 -"----------- Minisubpbl/301-init-subpbl.sml, determine_next_tactic -----------------------------";
26.499 -\<close> ML \<open>
26.500 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
26.501 -val (dI',pI',mI') =
26.502 - ("Test", ["sqroot-test","univariate","equation","test"],
26.503 - ["Test","squ-equ-test-subpbl1"]);
26.504 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.505 -\<close> ML \<open>
26.506 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.507 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.508 -val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, Ctree.e_pos'), []);
26.509 -(*([], Met)*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
26.510 -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
26.511 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
26.512 -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
26.513 -\<close> ML \<open>
26.514 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) =(**) step p ((pt, e_pos'), []);(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
26.515 -
26.516 -(*// relevant call --------------------------------------------------------------------------\\*)
26.517 -\<close> ML \<open>
26.518 -"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []));
26.519 -\<close> ML \<open>
26.520 - val pIopt = get_pblID (pt,ip);
26.521 -\<close> ML \<open>
26.522 - (*if*) ip = ([], Ctree.Res) (*else*);
26.523 -\<close> ML \<open>
26.524 - val _ = (*case*) tacis (*of*);
26.525 -\<close> ML \<open>
26.526 - val SOME _ = (*case*) pIopt (*of*);
26.527 -\<close> ML \<open>
26.528 - (*if*) member op = [Ctree.Pbl, Ctree.Met] p_
26.529 - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
26.530 -\<close> ML \<open>
26.531 - do_solve_step (pt, ip);
26.532 -\<close> ML \<open>
26.533 -"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
26.534 -\<close> ML \<open>
26.535 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
26.536 -\<close> ML \<open>
26.537 - val thy' = get_obj g_domID pt (par_pblobj pt p);
26.538 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
26.539 -\<close> ML \<open>
26.540 - determine_next_tactic (thy', srls) (pt, pos) sc is;
26.541 - (* TODO here ^^^ return finished/helpless/ok ?*)
26.542 -\<close> ML \<open>
26.543 -"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.Pstate (E,l,a,v,s,_), ctxt))
26.544 - = ((thy', srls), (pt, pos), sc, is);
26.545 -\<close> ML \<open>
26.546 - (*case*) execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) (*of*);
26.547 -\<close> ML \<open>
26.548 -"~~~~~ fun execute_progr_1 , args:"; val () = ();
26.549 -\<close> ML \<open>
26.550 -\<close> ML \<open>
26.551 -\<close> ML \<open>
26.552 -\<close> ML \<open>
26.553 -\<close> ML \<open>
26.554 -\<close> ML \<open>
26.555 -\<close> ML \<open>
26.556 -\<close> ML \<open>
26.557 -\<close> ML \<open>
26.558 -\<close> ML \<open>
26.559 -\<close> ML \<open>
26.560 -\<close> ML \<open>
26.561 -\<close> ML \<open>
26.562 -\<close> ML \<open>
26.563 -(*//--------------------- check results from modified step ----------------------------------\\*)
26.564 -(*\\--------------------- check results from modified step ----------------------------------//*)
26.565 -\<close> ML \<open>
26.566 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
26.567 -(*\\------------------ end of modified "fun step" -------------------------------------------//*)
26.568 -\<close> ML \<open>
26.569 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p''''' ((pt''''', e_pos'), []);(**)
26.570 -\<close> ML \<open>
26.571 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.572 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.573 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.574 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.575 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.576 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.577 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.578 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.579 -(**)val (_, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.580 -(**)val ("end-of-calculation", ([], _, (pt, p))) = step p ((pt, e_pos'), []);(**)
26.581 -
26.582 -(*/--------------------- final test ----------------------------------\\*)
26.583 -\<close> ML \<open>
26.584 -val (res, asm) = (get_obj g_result pt (fst p));
26.585 -if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
26.586 -then () else error "Minisubpbl/301-init-subpbl.sml, determine_next_tactic CHANGED"
26.587 -
26.588 -\<close> ML \<open>
26.589 -if p = ([], Und)
26.590 -then
26.591 - case get_obj g_tac pt (fst p) of
26.592 - Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
26.593 - | _ => error "301-init-subpbl WRONG RESULT CHANGED 2"
26.594 -else error "301-init-subpbl WRONG RESULT CHANGED 1"
26.595 -\<close> ML \<open>
26.596 -\<close>
26.597 -
26.598 section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
26.599 ML \<open>
26.600 "~~~~~ fun xxx , args:"; val () = ();
27.1 --- a/test/Tools/isac/Test_Theory.thy Mon Nov 04 11:40:29 2019 +0100
27.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Nov 06 15:08:27 2019 +0100
27.3 @@ -1,17 +1,19 @@
27.4 (* use this theory for tests before Build_Isac.thy has succeeded *)
27.5 -theory Test_Theory imports Isac.Program
27.6 +theory Test_Theory imports "~~/src/Tools/isac/Specify/Specify"
27.7 begin
27.8 -ML_file "~~/src/Tools/isac/library.sml"
27.9 -(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
27.10 +ML_file "~~/src/Tools/isac/CalcElements/libraryC.sml"
27.11 +(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.getfu _theory
27.12 requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)
27.13
27.14 section \<open>code for copy & paste ===============================================================\<close>
27.15 ML \<open>
27.16 -"~~~~~ fun , args:"; val () = ();
27.17 -"~~~~~ and , args:"; val () = ();
27.18 -
27.19 -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
27.20 -
27.21 +"~~~~~ fun xxx , args:"; val () = ();
27.22 +"~~~~~ and xxx , args:"; val () = ();
27.23 +"~~~~~ from xxx -> fun yyy -> fun zzz, return val:"; val () = ();
27.24 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
27.25 +"xx"
27.26 +^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*)
27.27 +\<close> ML \<open>
27.28 \<close>
27.29 text \<open>
27.30 declare [[show_types]]
27.31 @@ -46,7 +48,6 @@
27.32 \<close> ML \<open>
27.33 \<close> ML \<open>
27.34 \<close> ML \<open>
27.35 -\<close> ML \<open>
27.36 \<close>
27.37 section \<open>=================================================================\<close>
27.38 ML \<open>