1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Fri May 01 15:28:40 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri May 01 16:06:59 2020 +0200
1.3 @@ -20,7 +20,10 @@
1.4 struct
1.5 (**)
1.6
1.7 -(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)
1.8 +(*
1.9 + check tactics (input by the user, mostly) for applicability
1.10 + and determine as much of the result of the tactic as possible initially.
1.11 +*)
1.12 fun check (Tactic.Check_Postcond pI) (_, (p, p_)) =
1.13 if member op = [Pos.Pbl, Pos.Met] p_
1.14 then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.1 --- a/src/Tools/isac/MathEngine/step.sml Fri May 01 15:28:40 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngine/step.sml Fri May 01 16:06:59 2020 +0200
2.3 @@ -30,7 +30,7 @@
2.4
2.5 fun check tac (ctree, pos) =
2.6 if Pos.on_specification (snd pos)
2.7 - then ApplicableOLD.applicable_in pos ctree tac
2.8 + then Specify_Step.check tac (ctree, pos)
2.9 else Solve_Step.check tac (ctree, pos)
2.10
2.11
3.1 --- a/src/Tools/isac/Specify/appl.sml Fri May 01 15:28:40 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/appl.sml Fri May 01 16:06:59 2020 +0200
3.3 @@ -6,14 +6,12 @@
3.4
3.5 signature APPLICABLE_OLD =
3.6 sig
3.7 - val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> Applicable.T
3.8 -
3.9 val from_pblobj_or_detail_thm: 'a -> Pos.pos -> Ctree.ctree -> string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
3.10 val from_pblobj_or_detail_calc: string -> Pos.pos -> Ctree.ctree -> string * ThyC.id * (string * Rule_Def.eval_fn)
3.11 val mk_set: 'a -> Ctree.ctree -> Pos.pos -> term -> term -> term * term list
3.12 val split_dummy: string -> string * string
3.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.14 - val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
3.15 + (*NONE*)
3.16 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.17 val check_elementwise: theory -> Rule_Def.rule_set -> term -> term * term list -> term * term list
3.18 val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
3.19 @@ -119,414 +117,4 @@
3.20 else scan (s' @ [s]) ss;
3.21 in ((scan []) o Symbol.explode) str end;
3.22
3.23 -(* applicability of a tacic wrt. a calc-state (ctree, pos').
3.24 - additionally used by find_next_step.
3.25 - tests for applicability are so expensive, that results (rewrites!)
3.26 - are kept in the return-value of 'type tac_' *)
3.27 -fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
3.28 - | applicable_in (p, p_) pt Tactic.Model_Problem =
3.29 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
3.30 - Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.31 - else
3.32 - let
3.33 - val pI' = case Ctree.get_obj I pt p of
3.34 - Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
3.35 - | _ => error "applicable_in Init_Proof: uncovered case Ctree.get_obj"
3.36 - val {ppc, ...} = Specify.get_pbt pI'
3.37 - val pbl = Generate.init_pbl ppc
3.38 - in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
3.39 - | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
3.40 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.41 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.42 - else
3.43 - let
3.44 - val oris = case Ctree.get_obj I pt p of
3.45 - Ctree.PblObj {origin = (oris, _, _), ...} => oris
3.46 - | _ => error "applicable_in Refine_Tacitly: uncovered case Ctree.get_obj"
3.47 - in
3.48 - case Specify.refine_ori oris pI of
3.49 - SOME pblID =>
3.50 - Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
3.51 - | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
3.52 - end
3.53 - | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
3.54 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.55 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
3.56 - else
3.57 - let
3.58 - val (dI, dI', itms) = case Ctree.get_obj I pt p of
3.59 - Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
3.60 - => (dI, dI', itms)
3.61 - | _ => error "applicable_in Refine_Problem: uncovered case Ctree.get_obj"
3.62 - val thy = if dI' = ThyC.id_empty then dI else dI';
3.63 - in
3.64 - case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
3.65 - NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.66 - | SOME (rf as (pI', _)) =>
3.67 - if pI' = pI
3.68 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
3.69 - else Applicable.Yes (Tactic.Refine_Problem' rf)
3.70 - end
3.71 - (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
3.72 - | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
3.73 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.74 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.75 - else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
3.76 - (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
3.77 - | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
3.78 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.79 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.80 - else Applicable.Yes (Tactic.Del_Given' ct')
3.81 - | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
3.82 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.83 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.84 - else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
3.85 - | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
3.86 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.87 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.88 - else Applicable.Yes (Tactic.Del_Find' ct')
3.89 - | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
3.90 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.91 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.92 - else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
3.93 - | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
3.94 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.95 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.96 - else Applicable.Yes (Tactic.Del_Relation' ct')
3.97 - | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
3.98 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.99 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.100 - else Applicable.Yes (Tactic.Specify_Theory' dI)
3.101 - | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
3.102 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.103 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.104 - else
3.105 - let
3.106 - val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
3.107 - Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
3.108 - => (oris, dI, pI, dI', pI', itms)
3.109 - | _ => error "applicable_in Specify_Problem: uncovered case Ctree.get_obj"
3.110 - val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
3.111 - val {ppc, where_, prls, ...} = Specify.get_pbt pID;
3.112 - val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
3.113 - then (false, (Generate.init_pbl ppc, []))
3.114 - else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
3.115 - in
3.116 - Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
3.117 - end
3.118 - | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
3.119 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.120 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.121 - else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
3.122 - | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
3.123 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.124 - then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.125 - else
3.126 - let
3.127 - val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
3.128 - Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
3.129 - | _ => error "applicable_in Apply_Method: uncovered case Ctree.get_obj"
3.130 - val {where_, ...} = Specify.get_pbt pI
3.131 - val pres = map (Model.mk_env probl |> subst_atomic) where_
3.132 - val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
3.133 - then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
3.134 - else ctxt
3.135 - (*TODO.WN110416 here do evalprecond according to fun check_preconds'
3.136 - and then decide on Applicable.No/Applicable.Yes accordingly once more.
3.137 - Implement after all tests are running, since this changes
3.138 - overall system behavior*)
3.139 - in
3.140 - Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
3.141 - end
3.142 - (*required for corner cases, e.g. test setup in inssort.sml*)
3.143 - | applicable_in pos _ Tactic.Empty_Tac = Applicable.No "Empty_Tac is not applicable"
3.144 - | applicable_in pos _ m =
3.145 - raise ERROR ("applicable_in called for " ^ Tactic.input_to_string m ^ " at" ^ Pos.pos'2str pos);
3.146 -(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------* )
3.147 - | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
3.148 - if member op = [Pos.Pbl, Pos.Met] p_
3.149 - then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.150 - else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
3.151 - | applicable_in _ _ (Tactic.Take str) = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
3.152 - | applicable_in _ _ (Tactic.Free_Solve) = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
3.153 - | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
3.154 - if member op = [Pos.Pbl, Pos.Met] p_
3.155 - then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
3.156 - else
3.157 - let
3.158 - val pp = Ctree.par_pblobj pt p;
3.159 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.160 - val thy = ThyC.get_theory thy';
3.161 - val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
3.162 - val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
3.163 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
3.164 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
3.165 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.166 - in
3.167 - let
3.168 - val subst = Subst.T_from_input thy subs;
3.169 - in
3.170 - case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
3.171 - SOME (f',asm) =>
3.172 - Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
3.173 - | NONE => Applicable.No ((fst thm'')^" not applicable")
3.174 - end
3.175 - handle _ => Applicable.No ("syntax error in "^(subs2str subs))
3.176 - end
3.177 - | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
3.178 - if member op = [Pos.Pbl, Pos.Met] p_
3.179 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
3.180 - else
3.181 - let
3.182 - val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
3.183 - val thy = ThyC.get_theory thy';
3.184 - val f = case p_ of
3.185 - Frm => Ctree.get_obj Ctree.g_form pt p
3.186 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.187 - | _ => error ("applicable_in Rewrite: call by " ^ Pos.pos'2str (p, p_));
3.188 - in
3.189 - if msg = "OK"
3.190 - then
3.191 - case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
3.192 - SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
3.193 - | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
3.194 - else Applicable.No msg
3.195 - end
3.196 - | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
3.197 - if member op = [Pos.Pbl, Pos.Met] p_
3.198 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
3.199 - else
3.200 - let
3.201 - val pp = Ctree.par_pblobj pt p;
3.202 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.203 - val thy = ThyC.get_theory thy';
3.204 - val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
3.205 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.206 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.207 - val subst = Subst.T_from_input thy subs
3.208 - in
3.209 - case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
3.210 - SOME (f', asm)
3.211 - => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
3.212 - | NONE => Applicable.No (rls ^ " not applicable")
3.213 - handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
3.214 - end
3.215 - | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
3.216 - if member op = [Pos.Pbl, Pos.Met] p_
3.217 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
3.218 - else
3.219 - let
3.220 - val pp = Ctree.par_pblobj pt p;
3.221 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.222 - val thy = ThyC.get_theory thy';
3.223 - val (f, _) = case p_ of
3.224 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
3.225 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
3.226 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.227 - val subst = Subst.T_from_input thy subs;
3.228 - in
3.229 - case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
3.230 - SOME (f',asm)
3.231 - => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
3.232 - | NONE => Applicable.No (rls ^ " not applicable")
3.233 - handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
3.234 - end
3.235 - | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
3.236 - if member op = [Pos.Pbl, Pos.Met] p_
3.237 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.238 - else
3.239 - let
3.240 - val pp = Ctree.par_pblobj pt p;
3.241 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.242 - val (f, _) = case p_ of
3.243 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
3.244 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
3.245 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.246 - in
3.247 - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
3.248 - SOME (f', asm)
3.249 - => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
3.250 - | NONE => Applicable.No (rls ^ " not applicable")
3.251 - end
3.252 - | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
3.253 - if member op = [Pos.Pbl, Pos.Met] p_
3.254 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.255 - else
3.256 - let
3.257 - val pp = Ctree.par_pblobj pt p
3.258 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
3.259 - val f = case p_ of
3.260 - Frm => Ctree.get_obj Ctree.g_form pt p
3.261 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.262 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.263 - in
3.264 - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
3.265 - SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
3.266 - | NONE => Applicable.No (rls^" not applicable")
3.267 - end
3.268 - | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
3.269 - | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
3.270 - if member op = [Pos.Pbl, Pos.Met] p_
3.271 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
3.272 - else
3.273 - let
3.274 - val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
3.275 - val f = case p_ of
3.276 - Frm => Ctree.get_obj Ctree.g_form pt p
3.277 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.278 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.279 - in
3.280 - if msg = "OK"
3.281 - then
3.282 - case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
3.283 - SOME (f', (id, thm))
3.284 - => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
3.285 - | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
3.286 - else Applicable.No msg
3.287 - end
3.288 - (*Substitute combines two different kind of "substitution":
3.289 - (1) subst_atomic: for ?a..?z
3.290 - (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
3.291 - | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
3.292 - if member op = [Pos.Pbl, Pos.Met] p_
3.293 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.294 - else
3.295 - let
3.296 - val pp = Ctree.par_pblobj pt p
3.297 - val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
3.298 - val f = case p_ of
3.299 - Frm => Ctree.get_obj Ctree.g_form pt p
3.300 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.301 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.302 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
3.303 - val subte = Subst.input_to_terms sube
3.304 - val subst = Subst.T_from_string_eqs thy sube
3.305 - val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
3.306 - in
3.307 - if foldl and_ (true, map TermC.contains_Var subte)
3.308 - then (*1*)
3.309 - let val f' = subst_atomic subst f
3.310 - in if f = f'
3.311 - then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
3.312 - else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
3.313 - end
3.314 - else (*2*)
3.315 - case Rewrite.rewrite_terms_ thy ro erls subte f of
3.316 - SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
3.317 - | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
3.318 - end
3.319 - | applicable_in _ _ (Tactic.Apply_Assumption cts') =
3.320 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
3.321 - (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
3.322 - | applicable_in _ _ (Tactic.Take_Inst ct') =
3.323 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
3.324 - | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) =
3.325 - if Pos.on_specification p_
3.326 - then
3.327 - Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.328 - else (*some fields filled later in LI*)
3.329 - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
3.330 - TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
3.331 - | applicable_in _ _ (Tactic.End_Subproblem) =
3.332 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
3.333 - | applicable_in _ _ (Tactic.CAScmd ct') =
3.334 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
3.335 - | applicable_in _ _ (Tactic.Split_And) =
3.336 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
3.337 - | applicable_in _ _ (Tactic.Conclude_And) =
3.338 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
3.339 - | applicable_in _ _ (Tactic.Split_Or) =
3.340 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
3.341 - | applicable_in _ _ (Tactic.Conclude_Or) =
3.342 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
3.343 - | applicable_in (p, p_) pt (Tactic.Begin_Trans) =
3.344 - let
3.345 - val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
3.346 - Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
3.347 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
3.348 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.349 - in (Applicable.Yes (Tactic.Begin_Trans' f))
3.350 - handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
3.351 - end
3.352 - | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*)
3.353 - if p_ = Pos.Res
3.354 - then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
3.355 - else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
3.356 - | applicable_in _ _ (Tactic.Begin_Sequ) =
3.357 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
3.358 - | applicable_in _ _ (Tactic.End_Sequ) =
3.359 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
3.360 - | applicable_in _ _ (Tactic.Split_Intersect) =
3.361 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
3.362 - | applicable_in _ _ (Tactic.End_Intersect) =
3.363 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
3.364 - | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
3.365 - if member op = [Pos.Pbl, Pos.Met] p_
3.366 - then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.367 - else
3.368 - let
3.369 - val pp = Ctree.par_pblobj pt p;
3.370 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.371 - val thy = ThyC.get_theory thy'
3.372 - val metID = (Ctree.get_obj Ctree.g_metID pt pp)
3.373 - val {crls, ...} = Specify.get_met metID
3.374 - val (f, asm) = case p_ of
3.375 - Frm => (Ctree.get_obj Ctree.g_form pt p , [])
3.376 - | Pos.Res => Ctree.get_obj Ctree.g_result pt p
3.377 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.378 - val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
3.379 - in
3.380 - Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
3.381 - end
3.382 - | applicable_in (p, p_) pt Tactic.Or_to_List =
3.383 - if member op = [Pos.Pbl, Pos.Met] p_
3.384 - then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
3.385 - else
3.386 - let
3.387 - val f = case p_ of
3.388 - Frm => Ctree.get_obj Ctree.g_form pt p
3.389 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.390 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.391 - in (let val ls = Prog_Expr.or2list f
3.392 - in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
3.393 - handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
3.394 - end
3.395 - | applicable_in _ _ Tactic.Collect_Trues =
3.396 - error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
3.397 - | applicable_in _ _ Tactic.Empty_Tac = Applicable.No "Empty_Tac is not applicable"
3.398 - | applicable_in (p, p_) pt (Tactic.Tac id) =
3.399 - let
3.400 - val pp = Ctree.par_pblobj pt p;
3.401 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
3.402 - val thy = ThyC.get_theory thy';
3.403 - val f = case p_ of
3.404 - Frm => Ctree.get_obj Ctree.g_form pt p
3.405 - | Pos.Pbl => error "applicable_in (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"
3.406 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.407 - | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
3.408 - in case id of
3.409 - "subproblem_equation_dummy" =>
3.410 - if TermC.is_expliceq f
3.411 - then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
3.412 - else Applicable.No "applicable only to equations made explicit"
3.413 - | "solve_equation_dummy" =>
3.414 - let val (id', f') = split_dummy (UnparseC.term f);
3.415 - in
3.416 - if id' <> "subproblem_equation_dummy"
3.417 - then Applicable.No "no subproblem"
3.418 - else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
3.419 - then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
3.420 - else error ("applicable_in: f= " ^ f')
3.421 - end
3.422 - | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
3.423 - end
3.424 - | applicable_in _ _ Tactic.End_Proof' = Applicable.Yes Tactic.End_Proof''
3.425 - | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m);
3.426 -( *-----^^^^^- solve ---------------------------------------------------------------------------*)
3.427 -
3.428 -fun tac2tac_ pt p m =
3.429 - case applicable_in p pt m of
3.430 - Applicable.Yes m' => m'
3.431 - | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
3.432 -
3.433 (**)end(**);
4.1 --- a/src/Tools/isac/Specify/specify-step.sml Fri May 01 15:28:40 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/specify-step.sml Fri May 01 16:06:59 2020 +0200
4.3 @@ -7,7 +7,12 @@
4.4
4.5 signature SPECIFY_STEP =
4.6 sig
4.7 -
4.8 + val check: Tactic.input -> Calc.T -> Applicable.T
4.9 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.10 + (*NONE*)
4.11 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.12 + (*NONE*)
4.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.14 end
4.15
4.16 (**)
4.17 @@ -15,6 +20,129 @@
4.18 struct
4.19 (**)
4.20
4.21 +(*
4.22 + check tactics (input by the user, mostly) for applicability
4.23 + and determine as much of the result of the tactic as possible initially.
4.24 +*)
4.25 +fun check (Tactic.Init_Proof (ct', spec)) _ = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
4.26 + | check Tactic.Model_Problem (pt, (p, p_)) =
4.27 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
4.28 + Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.29 + else
4.30 + let
4.31 + val pI' = case Ctree.get_obj I pt p of
4.32 + Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
4.33 + | _ => error "Specify_Step.check Init_Proof: uncovered case Ctree.get_obj"
4.34 + val {ppc, ...} = Specify.get_pbt pI'
4.35 + val pbl = Generate.init_pbl ppc
4.36 + in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
4.37 + | check (Tactic.Refine_Tacitly pI) (pt, (p, p_)) =
4.38 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.39 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.40 + else
4.41 + let
4.42 + val oris = case Ctree.get_obj I pt p of
4.43 + Ctree.PblObj {origin = (oris, _, _), ...} => oris
4.44 + | _ => error "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
4.45 + in
4.46 + case Specify.refine_ori oris pI of
4.47 + SOME pblID =>
4.48 + Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
4.49 + | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
4.50 + end
4.51 + | check (Tactic.Refine_Problem pI) (pt, (p, p_)) =
4.52 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.53 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
4.54 + else
4.55 + let
4.56 + val (dI, dI', itms) = case Ctree.get_obj I pt p of
4.57 + Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
4.58 + => (dI, dI', itms)
4.59 + | _ => error "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
4.60 + val thy = if dI' = ThyC.id_empty then dI else dI';
4.61 + in
4.62 + case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
4.63 + NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
4.64 + | SOME (rf as (pI', _)) =>
4.65 + if pI' = pI
4.66 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
4.67 + else Applicable.Yes (Tactic.Refine_Problem' rf)
4.68 + end
4.69 + (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
4.70 + | check (Tactic.Add_Given ct') (pt, (p, p_)) =
4.71 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.72 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.73 + else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
4.74 + (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
4.75 + | check (Tactic.Del_Given ct') (pt, (p, p_)) =
4.76 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.77 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.78 + else Applicable.Yes (Tactic.Del_Given' ct')
4.79 + | check (Tactic.Add_Find ct') (pt, (p, p_)) =
4.80 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.81 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.82 + else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
4.83 + | check (Tactic.Del_Find ct') (pt, (p, p_)) =
4.84 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.85 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.86 + else Applicable.Yes (Tactic.Del_Find' ct')
4.87 + | check (Tactic.Add_Relation ct') (pt, (p, p_)) =
4.88 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.89 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.90 + else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
4.91 + | check (Tactic.Del_Relation ct') (pt, (p, p_)) =
4.92 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.93 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.94 + else Applicable.Yes (Tactic.Del_Relation' ct')
4.95 + | check (Tactic.Specify_Theory dI) (pt, (p, p_)) =
4.96 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.97 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.98 + else Applicable.Yes (Tactic.Specify_Theory' dI)
4.99 + | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =
4.100 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.101 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.102 + else
4.103 + let
4.104 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
4.105 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
4.106 + => (oris, dI, pI, dI', pI', itms)
4.107 + | _ => error "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
4.108 + val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
4.109 + val {ppc, where_, prls, ...} = Specify.get_pbt pID;
4.110 + val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
4.111 + then (false, (Generate.init_pbl ppc, []))
4.112 + else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
4.113 + in
4.114 + Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
4.115 + end
4.116 + | check (Tactic.Specify_Method mID) (pt, (p, p_)) =
4.117 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.118 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.119 + else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
4.120 + | check (Tactic.Apply_Method mI) (pt, (p, p_)) =
4.121 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
4.122 + then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
4.123 + else
4.124 + let
4.125 + val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
4.126 + Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
4.127 + | _ => error "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
4.128 + val {where_, ...} = Specify.get_pbt pI
4.129 + val pres = map (Model.mk_env probl |> subst_atomic) where_
4.130 + val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
4.131 + then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
4.132 + else ctxt
4.133 + (*TODO.WN110416 here do evalprecond according to fun check_preconds'
4.134 + and then decide on Applicable.No/Applicable.Yes accordingly once more.
4.135 + Implement after all tests are running, since this changes
4.136 + overall system behavior*)
4.137 + in
4.138 + Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
4.139 + end
4.140 + (*required for corner cases, e.g. test setup in inssort.sml*)
4.141 + | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
4.142 + | check tac (_, pos) =
4.143 + raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
4.144
4.145
4.146 (**)end(**);
5.1 --- a/src/Tools/isac/TODO.thy Fri May 01 15:28:40 2020 +0200
5.2 +++ b/src/Tools/isac/TODO.thy Fri May 01 16:06:59 2020 +0200
5.3 @@ -293,9 +293,9 @@
5.4 \begin{itemize}
5.5 \item Step*: Step_Specify | Step_Solve | Step
5.6 \begin{itemize}
5.7 - \item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve
5.8 - Specify_Step.check | Specify_Step.add <-- ApplicableOLD.applicable_in
5.9 - Solve_Step.check | Solve_Step.add <-- Generate.generate1
5.10 + \item *.check | *.add
5.11 + Specify_Step.add <-- Generate.generate1
5.12 + Solve_Step.add <-- Generate.generate1
5.13 \item xxx
5.14 \end{itemize}
5.15 \item xxx
6.1 --- a/src/Tools/isac/Test_Code/test-code.sml Fri May 01 15:28:40 2020 +0200
6.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Fri May 01 16:06:59 2020 +0200
6.3 @@ -17,6 +17,8 @@
6.4 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
6.5 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
6.6 Calc.T * Tactic.input * Generate.mout
6.7 +
6.8 + val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
6.9 end
6.10
6.11 (**)
6.12 @@ -159,4 +161,9 @@
6.13 ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
6.14 end
6.15
6.16 +fun tac2tac_ pt p m =
6.17 + case Step.check m (pt, p) of
6.18 + Applicable.Yes m' => m'
6.19 + | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
6.20 +
6.21 (**)end(**)
7.1 --- a/test/Tools/isac/Interpret/li-tool.sml Fri May 01 15:28:40 2020 +0200
7.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Fri May 01 16:06:59 2020 +0200
7.3 @@ -36,7 +36,7 @@
7.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.5 "~~~~~ fun me, args:"; val tac = nxt;
7.6 "~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
7.7 -val Applicable.Yes m = applicable_in p pt tac;
7.8 +val Applicable.Yes m = Step.check tac (pt, p);
7.9 (*if*) Tactic.for_specify' m; (*false*)
7.10 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
7.11 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Fri May 01 15:28:40 2020 +0200
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Fri May 01 16:06:59 2020 +0200
8.3 @@ -37,7 +37,7 @@
8.4
8.5 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
8.6 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.7 -val Applicable.Yes m = applicable_in p pt tac;
8.8 +val Applicable.Yes m = Step.check tac (pt, p);
8.9 (*if*) Tactic.for_specify' m; (*false*)
8.10 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
8.11
9.1 --- a/test/Tools/isac/Knowledge/rateq.sml Fri May 01 15:28:40 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri May 01 16:06:59 2020 +0200
9.3 @@ -133,7 +133,7 @@
9.4 val m = LItool.tac_from_prog pt (ThyC.get_theory th) stac;
9.5 case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
9.6 val (p''''', pt''''', m''''') = (p, pt, m);
9.7 -"~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
9.8 +"~~~~~ fun check , args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
9.9 Library.member op = [Pbl,Met] p_; (* = false*)
9.10 val pp = par_pblobj pt p;
9.11 val thy' = (get_obj g_domID pt pp):theory';
9.12 @@ -155,7 +155,7 @@
9.13 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above.
9.14 *)
9.15
9.16 -val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = applicable_in p''''' pt''''' m''''';
9.17 +val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = check p''''' pt''''' m''''';
9.18 UnparseC.term curr_form = "[x = 1 / 5]";
9.19 pred = "Assumptions";
9.20 res = str2term "[]::bool list";
10.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Fri May 01 15:28:40 2020 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Fri May 01 16:06:59 2020 +0200
10.3 @@ -40,7 +40,7 @@
10.4 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
10.5 Step.by_tactic tac (pt, p) (*of*);
10.6 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
10.7 - val Applicable.Yes m = (*case*) applicable_in p pt tac (*of*);
10.8 + val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
10.9 (*if*) Tactic.for_specify' m; (*false*)
10.10
10.11 Step_Solve.by_tactic m ptp;
11.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 01 15:28:40 2020 +0200
11.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 01 16:06:59 2020 +0200
11.3 @@ -553,7 +553,7 @@
11.4 (*me------------
11.5 val (mI,m) = nxt; val pos' as (p,p_) = p;
11.6
11.7 - val Applicable.Yes m = applicable_in (p,p_) pt m;
11.8 + val Applicable.Yes m = Step.check m (pt, (p,p_));
11.9 (*solve*)
11.10 val pp = par_pblobj pt p;
11.11 val metID = get_obj g_metID pt pp;
12.1 --- a/test/Tools/isac/OLDTESTS/script.sml Fri May 01 15:28:40 2020 +0200
12.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Fri May 01 16:06:59 2020 +0200
12.3 @@ -277,7 +277,7 @@
12.4 " --------------- 1. ---------------------------------------------";
12.5 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test",""))(str2term ct,[])Complete;
12.6 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
12.7 -val Applicable.Yes m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
12.8 +val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv","")) (pt, p);
12.9 *)
12.10
12.11
13.1 --- a/test/Tools/isac/Specify/appl.sml Fri May 01 15:28:40 2020 +0200
13.2 +++ b/test/Tools/isac/Specify/appl.sml Fri May 01 16:06:59 2020 +0200
13.3 @@ -6,7 +6,7 @@
13.4 "-----------------------------------------------------------------";
13.5 "table of contents -----------------------------------------------";
13.6 "-----------------------------------------------------------------";
13.7 -"-------------- fun applicable_in..Apply_Method ------------------";
13.8 +"-------------- fun Step.check..Apply_Method ------------------";
13.9 "-------------- fun mk_set ---------------------------------------";
13.10 "-------------- fun check_elementwise ----------------------------";
13.11 "-------------- fun split_dummy ----------------------------------";
13.12 @@ -15,9 +15,9 @@
13.13 "-----------------------------------------------------------------";
13.14
13.15
13.16 -"-------------- fun applicable_in..Apply_Method ------------------";
13.17 -"-------------- fun applicable_in..Apply_Method ------------------";
13.18 -"-------------- fun applicable_in..Apply_Method ------------------";
13.19 +"-------------- fun Step.check..Apply_Method ------------------";
13.20 +"-------------- fun Step.check..Apply_Method ------------------";
13.21 +"-------------- fun Step.check..Apply_Method ------------------";
13.22 val fmz = ["equality (x+1=(2::real))",
13.23 "solveFor (x::real)","solutions L"];
13.24 val (dI',pI',mI') =