1.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Nov 30 13:05:08 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 12 18:08:13 2016 +0100
1.3 @@ -216,35 +216,35 @@
1.4 tests for applicability are so expensive, that results (rewrites!)
1.5 are kept in the return-value of 'type tac_'.
1.6 .*)
1.7 -fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))
1.8 +fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Chead.Appl (Init_Proof' (ct', spec))
1.9
1.10 | applicable_in (p,p_) pt Model_Problem =
1.11 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.12 - then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
1.13 + then Chead.Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
1.14 else
1.15 let
1.16 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
1.17 val {ppc,...} = get_pbt pI'
1.18 val pbl = init_pbl ppc
1.19 - in Appl (Model_Problem' (pI', pbl, [])) end
1.20 + in Chead.Appl (Model_Problem' (pI', pbl, [])) end
1.21
1.22 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
1.23 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.24 - then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
1.25 + then Chead.Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
1.26 else
1.27 let
1.28 val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
1.29 val opt = refine_ori oris pI;
1.30 in case opt of
1.31 SOME pblID =>
1.32 - Appl (Refine_Tacitly' (pI, pblID,
1.33 + Chead.Appl (Refine_Tacitly' (pI, pblID,
1.34 e_domID, e_metID, [](*filled in specify*)))
1.35 - | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
1.36 + | NONE => Chead.Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
1.37 end
1.38
1.39 | applicable_in (p,p_) pt (Refine_Problem pI) =
1.40 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.41 - then Notappl ((tac2str (Refine_Problem pI))^
1.42 + then Chead.Notappl ((tac2str (Refine_Problem pI))^
1.43 " not for pos "^(pos'2str (p,p_)))
1.44 else
1.45 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1.46 @@ -252,65 +252,65 @@
1.47 val thy = if dI' = e_domID then dI else dI';
1.48 val rfopt = refine_pbl (assoc_thy thy) pI itms;
1.49 in case rfopt of
1.50 - NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.51 + NONE => Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.52 | SOME (rf as (pI',_)) =>
1.53 (* val SOME (rf as (pI',_)) = rfopt;
1.54 *)
1.55 if pI' = pI
1.56 - then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.57 - else Appl (Refine_Problem' rf)
1.58 + then Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.59 + else Chead.Appl (Refine_Problem' rf)
1.60 end
1.61
1.62 (*the specify-tacs have cterm' instead term:
1.63 parse+error here!!!: see appl_add*)
1.64 | applicable_in (p,p_) pt (Add_Given ct') =
1.65 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.66 - then Notappl ((tac2str (Add_Given ct'))^
1.67 + then Chead.Notappl ((tac2str (Add_Given ct'))^
1.68 " not for pos "^(pos'2str (p,p_)))
1.69 - else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
1.70 + else Chead.Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
1.71 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
1.72
1.73 | applicable_in (p,p_) pt (Del_Given ct') =
1.74 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.75 - then Notappl ((tac2str (Del_Given ct'))^
1.76 + then Chead.Notappl ((tac2str (Del_Given ct'))^
1.77 " not for pos "^(pos'2str (p,p_)))
1.78 - else Appl (Del_Given' ct')
1.79 + else Chead.Appl (Del_Given' ct')
1.80
1.81 | applicable_in (p,p_) pt (Add_Find ct') =
1.82 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.83 - then Notappl ((tac2str (Add_Find ct'))^
1.84 + then Chead.Notappl ((tac2str (Add_Find ct'))^
1.85 " not for pos "^(pos'2str (p,p_)))
1.86 - else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
1.87 + else Chead.Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
1.88
1.89 | applicable_in (p,p_) pt (Del_Find ct') =
1.90 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.91 - then Notappl ((tac2str (Del_Find ct'))^
1.92 + then Chead.Notappl ((tac2str (Del_Find ct'))^
1.93 " not for pos "^(pos'2str (p,p_)))
1.94 - else Appl (Del_Find' ct')
1.95 + else Chead.Appl (Del_Find' ct')
1.96
1.97 | applicable_in (p,p_) pt (Add_Relation ct') =
1.98 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.99 - then Notappl ((tac2str (Add_Relation ct'))^
1.100 + then Chead.Notappl ((tac2str (Add_Relation ct'))^
1.101 " not for pos "^(pos'2str (p,p_)))
1.102 - else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
1.103 + else Chead.Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
1.104
1.105 | applicable_in (p,p_) pt (Del_Relation ct') =
1.106 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.107 - then Notappl ((tac2str (Del_Relation ct'))^
1.108 + then Chead.Notappl ((tac2str (Del_Relation ct'))^
1.109 " not for pos "^(pos'2str (p,p_)))
1.110 - else Appl (Del_Relation' ct')
1.111 + else Chead.Appl (Del_Relation' ct')
1.112
1.113 | applicable_in (p,p_) pt (Specify_Theory dI) =
1.114 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.115 - then Notappl ((tac2str (Specify_Theory dI))^
1.116 + then Chead.Notappl ((tac2str (Specify_Theory dI))^
1.117 " not for pos "^(pos'2str (p,p_)))
1.118 - else Appl (Specify_Theory' dI)
1.119 + else Chead.Appl (Specify_Theory' dI)
1.120 (* val (p,p_) = p; val Specify_Problem pID = m;
1.121 val Specify_Problem pID = m;
1.122 *)
1.123 | applicable_in (p,p_) pt (Specify_Problem pID) =
1.124 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.125 - then Notappl ((tac2str (Specify_Problem pID))^
1.126 + then Chead.Notappl ((tac2str (Specify_Problem pID))^
1.127 " not for pos "^(pos'2str (p,p_)))
1.128 else
1.129 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
1.130 @@ -320,19 +320,19 @@
1.131 val pbl = if pI'=e_pblID andalso pI=e_pblID
1.132 then (false, (init_pbl ppc, []))
1.133 else match_itms_oris thy itms (ppc,where_,prls) oris;
1.134 - in Appl (Specify_Problem' (pID, pbl)) end
1.135 + in Chead.Appl (Specify_Problem' (pID, pbl)) end
1.136 (* val Specify_Method mID = nxt; val (p,p_) = p;
1.137 *)
1.138 | applicable_in (p,p_) pt (Specify_Method mID) =
1.139 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.140 - then Notappl ((tac2str (Specify_Method mID))^
1.141 + then Chead.Notappl ((tac2str (Specify_Method mID))^
1.142 " not for pos "^(pos'2str (p,p_)))
1.143 - else Appl (Specify_Method' (mID,[(*filled in specify*)],
1.144 + else Chead.Appl (Specify_Method' (mID,[(*filled in specify*)],
1.145 [(*filled in specify*)]))
1.146
1.147 | applicable_in (p,p_) pt (Apply_Method mI) =
1.148 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.149 - then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
1.150 + then Chead.Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
1.151 else
1.152 let
1.153 val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
1.154 @@ -343,23 +343,23 @@
1.155 then assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres
1.156 else ctxt
1.157 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.158 - and then decide on Notappl/Appl accordingly once more.
1.159 + and then decide on Chead.Notappl/Appl accordingly once more.
1.160 Implement after all tests are running, since this changes
1.161 overall system behavior*)
1.162 - in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
1.163 + in Chead.Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
1.164
1.165 | applicable_in (p,p_) pt (Check_Postcond pI) =
1.166 if member op = [Pbl,Met] p_
1.167 - then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
1.168 - else Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
1.169 + then Chead.Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
1.170 + else Chead.Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
1.171
1.172 (*these are always applicable*)
1.173 - | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
1.174 - | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
1.175 + | applicable_in (p,p_) _ (Take str) = Chead.Appl (Take' (str2term str))
1.176 + | applicable_in (p,p_) _ (Free_Solve) = Chead.Appl (Free_Solve')
1.177
1.178 | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm'')) =
1.179 if member op = [Pbl, Met] p_
1.180 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.181 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.182 else
1.183 let
1.184 val pp = par_pblobj pt p;
1.185 @@ -376,15 +376,15 @@
1.186 val subs' = subst2subs' subst;
1.187 in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
1.188 SOME (f',asm) =>
1.189 - Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
1.190 - | NONE => Notappl ((fst thm'')^" not applicable")
1.191 + Chead.Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
1.192 + | NONE => Chead.Notappl ((fst thm'')^" not applicable")
1.193 end
1.194 - handle _ => Notappl ("syntax error in "^(subs2str subs))
1.195 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs))
1.196 end
1.197
1.198 | applicable_in (p,p_) pt (m as Rewrite thm'') =
1.199 if member op = [Pbl,Met] p_
1.200 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.201 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.202 else
1.203 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm'' p pt;
1.204 val thy = assoc_thy thy';
1.205 @@ -396,14 +396,14 @@
1.206 in if msg = "OK"
1.207 then
1.208 case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
1.209 - SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.210 - | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
1.211 - else Notappl msg
1.212 + SOME (f',asm) => Chead.Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.213 + | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable")
1.214 + else Chead.Notappl msg
1.215 end
1.216
1.217 | applicable_in (p,p_) pt (m as Rewrite_Asm thm'') =
1.218 if member op = [Pbl,Met] p_
1.219 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.220 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.221 else
1.222 let
1.223 val pp = par_pblobj pt p;
1.224 @@ -418,13 +418,13 @@
1.225 | _ => error ("applicable_in: call by "^
1.226 (pos'2str (p,p_)));
1.227 in case rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
1.228 - SOME (f',asm) => Appl (
1.229 + SOME (f',asm) => Chead.Appl (
1.230 Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
1.231 - | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
1.232 + | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end
1.233
1.234 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
1.235 if member op = [Pbl,Met] p_
1.236 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.237 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.238 else
1.239 let
1.240 val pp = par_pblobj pt p;
1.241 @@ -439,14 +439,14 @@
1.242 let val subst = subs2subst thy subs
1.243 val subs' = subst2subs' subst
1.244 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.245 - SOME (f',asm) => Appl (
1.246 + SOME (f',asm) => Chead.Appl (
1.247 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
1.248 - | NONE => Notappl (rls^" not applicable") end
1.249 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.250 + | NONE => Chead.Notappl (rls^" not applicable") end
1.251 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) end
1.252
1.253 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
1.254 if member op = [Pbl,Met] p_
1.255 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.256 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.257 else
1.258 let
1.259 val pp = par_pblobj pt p;
1.260 @@ -463,14 +463,14 @@
1.261 let val subst = subs2subst thy subs;
1.262 val subs' = subst2subs' subst;
1.263 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
1.264 - SOME (f',asm) => Appl (
1.265 + SOME (f',asm) => Chead.Appl (
1.266 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
1.267 - | NONE => Notappl (rls^" not applicable") end
1.268 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.269 + | NONE => Chead.Notappl (rls^" not applicable") end
1.270 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) end
1.271
1.272 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
1.273 if member op = [Pbl,Met] p_
1.274 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.275 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.276 else
1.277 let
1.278 val pp = par_pblobj pt p;
1.279 @@ -483,13 +483,13 @@
1.280 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.281 SOME (f',asm) =>
1.282 ((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
1.283 - Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
1.284 + Chead.Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
1.285 )
1.286 - | NONE => Notappl (rls^" not applicable") end
1.287 + | NONE => Chead.Notappl (rls^" not applicable") end
1.288
1.289 | applicable_in (p,p_) pt (m as Detail_Set rls) =
1.290 if member op = [Pbl,Met] p_
1.291 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.292 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.293 else
1.294 let val pp = par_pblobj pt p
1.295 val thy' = (get_obj g_domID pt pp):theory'
1.296 @@ -500,8 +500,8 @@
1.297 (pos'2str (p,p_)));
1.298 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.299 SOME (f',asm) =>
1.300 - Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
1.301 - | NONE => Notappl (rls^" not applicable") end
1.302 + Chead.Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
1.303 + | NONE => Chead.Notappl (rls^" not applicable") end
1.304
1.305
1.306 | applicable_in p pt (End_Ruleset) =
1.307 @@ -512,7 +512,7 @@
1.308 *)
1.309 | applicable_in (p,p_) pt (m as Calculate op_) =
1.310 if member op = [Pbl,Met] p_
1.311 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.312 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.313 else
1.314 let
1.315 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
1.316 @@ -522,9 +522,9 @@
1.317 in if msg = "OK" then
1.318 case calculate_ (assoc_thy thy') isa_fn f of
1.319 SOME (f', (id, thm)) =>
1.320 - Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
1.321 - | NONE => Notappl ("'calculate "^op_^"' not applicable")
1.322 - else Notappl msg
1.323 + Chead.Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
1.324 + | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable")
1.325 + else Chead.Notappl msg
1.326 end
1.327
1.328 (*Substitute combines two different kind of "substitution":
1.329 @@ -533,7 +533,7 @@
1.330 (which raises exn for ?a..?z)*)
1.331 | applicable_in (p,p_) pt (m as Substitute sube) =
1.332 if member op = [Pbl,Met] p_
1.333 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.334 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.335 else
1.336 let
1.337 val pp = par_pblobj pt p
1.338 @@ -550,14 +550,14 @@
1.339 (*1*)
1.340 then
1.341 let val f' = subst_atomic subst f
1.342 - in if f = f' then Notappl (sube2str sube^" not applicable")
1.343 - else Appl (Substitute' (ro, erls, subte, f, f'))
1.344 + in if f = f' then Chead.Notappl (sube2str sube^" not applicable")
1.345 + else Chead.Appl (Substitute' (ro, erls, subte, f, f'))
1.346 end
1.347 (*2*)
1.348 else
1.349 case rewrite_terms_ thy ro erls subte f of
1.350 - SOME (f', _) => Appl (Substitute' (ro, erls, subte, f, f'))
1.351 - | NONE => Notappl (sube2str sube^" not applicable")
1.352 + SOME (f', _) => Chead.Appl (Substitute' (ro, erls, subte, f, f'))
1.353 + | NONE => Chead.Notappl (sube2str sube^" not applicable")
1.354 end
1.355
1.356 | applicable_in p pt (Apply_Assumption cts') =
1.357 @@ -566,12 +566,12 @@
1.358 (*'logical' applicability wrt. script in locate: Inconsistent?*)
1.359 | applicable_in (p,p_) pt (m as Take ct') =
1.360 if member op = [Pbl,Met] p_
1.361 - then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
1.362 + then Chead.Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
1.363 else
1.364 let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.365 in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
1.366 - SOME ct => Appl (Take' ct)
1.367 - | NONE => Notappl ("syntax error in " ^ ct'))
1.368 + SOME ct => Chead.Appl (Take' ct)
1.369 + | NONE => Chead.Notappl ("syntax error in " ^ ct'))
1.370 end
1.371
1.372 | applicable_in p pt (Take_Inst ct') =
1.373 @@ -584,11 +584,11 @@
1.374 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
1.375 case get_obj g_env pt p of
1.376 SOME is =>
1.377 - Appl (Subproblem' ((domID, pblID, e_metID), [],
1.378 + Chead.Appl (Subproblem' ((domID, pblID, e_metID), [],
1.379 e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
1.380 - | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.381 + | NONE => Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.382 else (*somewhere later in the script*)
1.383 - Appl (Subproblem' ((domID, pblID, e_metID), [],
1.384 + Chead.Appl (Subproblem' ((domID, pblID, e_metID), [],
1.385 e_term, [], e_ctxt, subpbl domID pblID))
1.386
1.387 | applicable_in p pt (End_Subproblem) =
1.388 @@ -613,7 +613,7 @@
1.389 | _ => error ("applicable_in: call by "^
1.390 (pos'2str (p,p_)));
1.391 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.392 - in (Appl (Begin_Trans' f))
1.393 + in (Chead.Appl (Begin_Trans' f))
1.394 handle _ => error ("applicable_in: Begin_Trans finds \
1.395 \syntaxerror in '"^(term2str f)^"'") end
1.396
1.397 @@ -621,8 +621,8 @@
1.398 | applicable_in (p,p_) pt (End_Trans) =
1.399 let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.400 in if p_ = Res
1.401 - then Appl (End_Trans' (get_obj g_result pt p))
1.402 - else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.403 + then Chead.Appl (End_Trans' (get_obj g_result pt p))
1.404 + else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.405 (*TODO: check parent branches*)
1.406 end
1.407 | applicable_in p pt (Begin_Sequ) =
1.408 @@ -636,7 +636,7 @@
1.409
1.410 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
1.411 if member op = [Pbl,Met] p_
1.412 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.413 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.414 else
1.415 let
1.416 val pp = par_pblobj pt p;
1.417 @@ -649,17 +649,17 @@
1.418 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
1.419 in case f of
1.420 Const ("List.list.Cons",_) $ _ $ _ =>
1.421 - Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
1.422 + Chead.Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
1.423 | Const ("Tools.UniversalList",_) =>
1.424 - Appl (Check_elementwise' (f, pred, (f,asm)))
1.425 + Chead.Appl (Check_elementwise' (f, pred, (f,asm)))
1.426 | Const ("List.list.Nil",_) =>
1.427 - Appl (Check_elementwise' (f, pred, (f, asm)))
1.428 - | _ => Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
1.429 + Chead.Appl (Check_elementwise' (f, pred, (f, asm)))
1.430 + | _ => Chead.Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
1.431 end
1.432
1.433 | applicable_in (p,p_) pt Or_to_List =
1.434 if member op = [Pbl,Met] p_
1.435 - then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
1.436 + then Chead.Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
1.437 else
1.438 let
1.439 val pp = par_pblobj pt p;
1.440 @@ -669,8 +669,8 @@
1.441 Frm => get_obj g_form pt p
1.442 | Res => (fst o (get_obj g_result pt)) p;
1.443 in (let val ls = or2list f
1.444 - in Appl (Or_to_List' (f, ls)) end)
1.445 - handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
1.446 + in Chead.Appl (Or_to_List' (f, ls)) end)
1.447 + handle _ => Chead.Notappl ("'Or_to_List' not applicable to "^(term2str f))
1.448 end
1.449
1.450 | applicable_in p pt (Collect_Trues) =
1.451 @@ -678,7 +678,7 @@
1.452 (tac2str (Collect_Trues)))
1.453
1.454 | applicable_in p pt (Empty_Tac) =
1.455 - Notappl "Empty_Tac is not applicable"
1.456 + Chead.Notappl "Empty_Tac is not applicable"
1.457
1.458 | applicable_in (p,p_) pt (Tac id) =
1.459 let
1.460 @@ -692,9 +692,9 @@
1.461 in case id of
1.462 "subproblem_equation_dummy" =>
1.463 if is_expliceq f
1.464 - then Appl (Tac_ (thy, term2str f, id,
1.465 + then Chead.Appl (Tac_ (thy, term2str f, id,
1.466 "subproblem_equation_dummy ("^(term2str f)^")"))
1.467 - else Notappl "applicable only to equations made explicit"
1.468 + else Chead.Notappl "applicable only to equations made explicit"
1.469 | "solve_equation_dummy" =>
1.470 let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
1.471 ^f);*)
1.472 @@ -702,13 +702,13 @@
1.473 (*val _= tracing("### applicable_in: f'= "^f');*)
1.474 (*val _= (Thm.term_of o the o (parse thy)) f';*)
1.475 (*val _= tracing"### applicable_in: solve_equation_dummy";*)
1.476 - in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
1.477 + in if id' <> "subproblem_equation_dummy" then Chead.Notappl "no subproblem"
1.478 else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
1.479 - then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
1.480 + then Chead.Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
1.481 else error ("applicable_in: f= " ^ f') end
1.482 - | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
1.483 + | _ => Chead.Appl (Tac_ (thy, term2str f, id, term2str f)) end
1.484
1.485 - | applicable_in p pt End_Proof' = Appl End_Proof''
1.486 + | applicable_in p pt End_Proof' = Chead.Appl End_Proof''
1.487
1.488 | applicable_in _ _ m =
1.489 error ("applicable_in called for "^(tac2str m));
1.490 @@ -716,7 +716,7 @@
1.491 (*WN060614 unused*)
1.492 fun tac2tac_ pt p m =
1.493 case applicable_in p pt m of
1.494 - Appl (m') => m'
1.495 - | Notappl _ => error ("tac2mstp': fails with"^
1.496 + Chead.Appl (m') => m'
1.497 + | Chead.Notappl _ => error ("tac2mstp': fails with"^
1.498 (tac2str m));
1.499