1.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 01 10:24:13 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 01 12:42:39 2020 +0200
1.3 @@ -8,9 +8,9 @@
1.4 sig
1.5 exception PTREE of string
1.6 datatype appl = Appl of Tactic.T | Notappl of string
1.7 - val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> appl
1.8 + val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> appl
1.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.10 - val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
1.11 + val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
1.12 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.13 val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
1.14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.15 @@ -128,7 +128,7 @@
1.16 fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
1.17 | applicable_in (p, p_) pt Tactic.Model_Problem =
1.18 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.19 - then Notappl ((Tactic.tac2str Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
1.20 + then Notappl ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
1.21 else
1.22 let
1.23 val pI' = case get_obj I pt p of
1.24 @@ -139,7 +139,7 @@
1.25 in Appl (Tactic.Model_Problem' (pI', pbl, [])) end
1.26 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
1.27 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.28 - then Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
1.29 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
1.30 else
1.31 let
1.32 val oris = case get_obj I pt p of
1.33 @@ -149,11 +149,11 @@
1.34 case Specify.refine_ori oris pI of
1.35 SOME pblID =>
1.36 Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))
1.37 - | NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not applicable")
1.38 + | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
1.39 end
1.40 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
1.41 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.42 - then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
1.43 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
1.44 else
1.45 let
1.46 val (dI, dI', itms) = case get_obj I pt p of
1.47 @@ -163,45 +163,45 @@
1.48 val thy = if dI' = Rule.e_domID then dI else dI';
1.49 in
1.50 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
1.51 - NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
1.52 + NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
1.53 | SOME (rf as (pI', _)) =>
1.54 if pI' = pI
1.55 - then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
1.56 + then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
1.57 else Appl (Tactic.Refine_Problem' rf)
1.58 end
1.59 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
1.60 | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
1.61 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.62 - then Notappl ((Tactic.tac2str (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.63 + then Notappl ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.64 else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
1.65 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
1.66 | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
1.67 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.68 - then Notappl ((Tactic.tac2str (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.69 + then Notappl ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.70 else Appl (Tactic.Del_Given' ct')
1.71 | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
1.72 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.73 - then Notappl ((Tactic.tac2str (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.74 + then Notappl ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.75 else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
1.76 | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
1.77 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.78 - then Notappl ((Tactic.tac2str (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.79 + then Notappl ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.80 else Appl (Tactic.Del_Find' ct')
1.81 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
1.82 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.83 - then Notappl ((Tactic.tac2str (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.84 + then Notappl ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.85 else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
1.86 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
1.87 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.88 - then Notappl ((Tactic.tac2str (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.89 + then Notappl ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
1.90 else Appl (Tactic.Del_Relation' ct')
1.91 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
1.92 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.93 - then Notappl ((Tactic.tac2str (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
1.94 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
1.95 else Appl (Tactic.Specify_Theory' dI)
1.96 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
1.97 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.98 - then Notappl ((Tactic.tac2str (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
1.99 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
1.100 else
1.101 let
1.102 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
1.103 @@ -218,11 +218,11 @@
1.104 end
1.105 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
1.106 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.107 - then Notappl ((Tactic.tac2str (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
1.108 + then Notappl ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
1.109 else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
1.110 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
1.111 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.112 - then Notappl ((Tactic.tac2str (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
1.113 + then Notappl ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
1.114 else
1.115 let
1.116 val (dI, pI, probl, ctxt) = case get_obj I pt p of
1.117 @@ -230,7 +230,7 @@
1.118 | _ => error "applicable_in Apply_Method: uncovered case get_obj"
1.119 val {where_, ...} = Specify.get_pbt pI
1.120 val pres = map (Model.mk_env probl |> subst_atomic) where_
1.121 - val ctxt = if ContextC.is_e_ctxt ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
1.122 + val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
1.123 then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
1.124 else ctxt
1.125 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.126 @@ -238,17 +238,17 @@
1.127 Implement after all tests are running, since this changes
1.128 overall system behavior*)
1.129 in
1.130 - Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.e_istate (*filled in solve*), ctxt))
1.131 + Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
1.132 end
1.133 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
1.134 if member op = [Pbl, Met] p_
1.135 - then Notappl ((Tactic.tac2str (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
1.136 + then Notappl ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
1.137 else Appl (Tactic.Check_Postcond' (pI, Rule.e_term))
1.138 | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
1.139 | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve') (* always applicable *)
1.140 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
1.141 if member op = [Pbl, Met] p_
1.142 - then Notappl ((Tactic.tac2str m)^" not for pos " ^ pos'2str (p, p_))
1.143 + then Notappl ((Tactic.input_to_string m)^" not for pos " ^ pos'2str (p, p_))
1.144 else
1.145 let
1.146 val pp = par_pblobj pt p;
1.147 @@ -272,7 +272,7 @@
1.148 end
1.149 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
1.150 if member op = [Pbl, Met] p_
1.151 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
1.152 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
1.153 else
1.154 let
1.155 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
1.156 @@ -291,7 +291,7 @@
1.157 end
1.158 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
1.159 if member op = [Pbl, Met] p_
1.160 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
1.161 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
1.162 else
1.163 let
1.164 val pp = par_pblobj pt p;
1.165 @@ -310,7 +310,7 @@
1.166 end
1.167 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
1.168 if member op = [Pbl, Met] p_
1.169 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.170 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
1.171 else
1.172 let
1.173 val pp = par_pblobj pt p;
1.174 @@ -330,7 +330,7 @@
1.175 end
1.176 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
1.177 if member op = [Pbl, Met] p_
1.178 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
1.179 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
1.180 else
1.181 let
1.182 val pp = par_pblobj pt p;
1.183 @@ -347,7 +347,7 @@
1.184 end
1.185 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
1.186 if member op = [Pbl, Met] p_
1.187 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
1.188 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
1.189 else
1.190 let
1.191 val pp = par_pblobj pt p
1.192 @@ -361,10 +361,10 @@
1.193 SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.194 | NONE => Notappl (rls^" not applicable")
1.195 end
1.196 - | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Ruleset)
1.197 + | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
1.198 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
1.199 if member op = [Pbl, Met] p_
1.200 - then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.201 + then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
1.202 else
1.203 let
1.204 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
1.205 @@ -386,7 +386,7 @@
1.206 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
1.207 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
1.208 if member op = [Pbl, Met] p_
1.209 - then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
1.210 + then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
1.211 else
1.212 let
1.213 val pp = par_pblobj pt p
1.214 @@ -413,29 +413,29 @@
1.215 | NONE => Notappl (Selem.sube2str sube ^ " not applicable")
1.216 end
1.217 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
1.218 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Apply_Assumption cts'))
1.219 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
1.220 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
1.221 | applicable_in _ _ (Tactic.Take_Inst ct') =
1.222 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Take_Inst ct'))
1.223 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
1.224 | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) =
1.225 if Pos.on_specification p_
1.226 then
1.227 - Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
1.228 + Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
1.229 else (*some fields filled later in LI*)
1.230 Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
1.231 - Rule.e_term, [], ContextC.e_ctxt, Auto_Prog.subpbl domID pblID))
1.232 + Rule.e_term, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
1.233 | applicable_in _ _ (Tactic.End_Subproblem) =
1.234 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Subproblem)
1.235 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
1.236 | applicable_in _ _ (Tactic.CAScmd ct') =
1.237 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.CAScmd ct'))
1.238 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
1.239 | applicable_in _ _ (Tactic.Split_And) =
1.240 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_And)
1.241 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
1.242 | applicable_in _ _ (Tactic.Conclude_And) =
1.243 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_And)
1.244 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
1.245 | applicable_in _ _ (Tactic.Split_Or) =
1.246 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_Or)
1.247 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
1.248 | applicable_in _ _ (Tactic.Conclude_Or) =
1.249 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_Or)
1.250 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
1.251 | applicable_in (p, p_) pt (Tactic.Begin_Trans) =
1.252 let
1.253 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
1.254 @@ -450,16 +450,16 @@
1.255 then Appl (Tactic.End_Trans' (get_obj g_result pt p))
1.256 else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.257 | applicable_in _ _ (Tactic.Begin_Sequ) =
1.258 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Begin_Sequ))
1.259 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
1.260 | applicable_in _ _ (Tactic.End_Sequ) =
1.261 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Sequ))
1.262 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
1.263 | applicable_in _ _ (Tactic.Split_Intersect) =
1.264 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Split_Intersect))
1.265 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
1.266 | applicable_in _ _ (Tactic.End_Intersect) =
1.267 - error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Intersect))
1.268 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
1.269 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
1.270 if member op = [Pbl, Met] p_
1.271 - then Notappl ((Tactic.tac2str m) ^ " not for pos " ^ pos'2str (p, p_))
1.272 + then Notappl ((Tactic.input_to_string m) ^ " not for pos " ^ pos'2str (p, p_))
1.273 else
1.274 let
1.275 val pp = par_pblobj pt p;
1.276 @@ -477,7 +477,7 @@
1.277 end
1.278 | applicable_in (p, p_) pt Tactic.Or_to_List =
1.279 if member op = [Pbl, Met] p_
1.280 - then Notappl ((Tactic.tac2str Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
1.281 + then Notappl ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
1.282 else
1.283 let
1.284 val f = case p_ of
1.285 @@ -489,7 +489,7 @@
1.286 handle _ => Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)
1.287 end
1.288 | applicable_in _ _ Tactic.Collect_Trues =
1.289 - error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Collect_Trues)
1.290 + error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
1.291 | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"
1.292 | applicable_in (p, p_) pt (Tactic.Tac id) =
1.293 let
1.294 @@ -518,11 +518,11 @@
1.295 | _ => Appl (Tactic.Tac_ (thy, Rule.term2str f, id, Rule.term2str f))
1.296 end
1.297 | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''
1.298 - | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.tac2str m);
1.299 + | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m);
1.300
1.301 fun tac2tac_ pt p m =
1.302 case applicable_in p pt m of
1.303 Appl m' => m'
1.304 - | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.tac2str m);
1.305 + | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
1.306
1.307 end;