1.1 --- a/src/Tools/isac/Interpret/appl.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -21,13 +21,13 @@
1.4 (**)
1.5 open Ctree
1.6
1.7 -fun rew_info (Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.8 +fun rew_info (Celem.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.9 (rew_ord', erls, ca)
1.10 - | rew_info (Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.11 + | rew_info (Celem.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.12 (rew_ord', erls, ca)
1.13 - | rew_info (Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.14 + | rew_info (Celem.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.15 (rew_ord', erls, ca)
1.16 - | rew_info rls = error ("rew_info called with '" ^ rls2str rls ^ "'");
1.17 + | rew_info rls = error ("rew_info called with '" ^ Celem.rls2str rls ^ "'");
1.18
1.19 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
1.20 fun from_pblobj_or_detail_thm _ p pt =
1.21 @@ -60,7 +60,7 @@
1.22 in
1.23 case opt of
1.24 SOME isa_fn => ("OK", thy', isa_fn)
1.25 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
1.26 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Celem.e_evalfn))
1.27 end
1.28 else
1.29 let
1.30 @@ -69,14 +69,14 @@
1.31 in
1.32 case assoc (scr_isa_fns, scrop) of
1.33 SOME isa_fn => ("OK",thy',isa_fn)
1.34 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
1.35 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Celem.e_evalfn))
1.36 end
1.37 end;
1.38
1.39 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
1.40 -fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (e_term, [])
1.41 +fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Celem.e_term, [])
1.42 | mk_set _ pt p (Const ("Tools.UniversalList", _)) pred =
1.43 - (e_term, if pred <> Const ("Script.Assumptions", HOLogic.boolT)
1.44 + (Celem.e_term, if pred <> Const ("Script.Assumptions", HOLogic.boolT)
1.45 then [pred]
1.46 else get_assumptions_ pt (p, Res))
1.47 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
1.48 @@ -87,7 +87,7 @@
1.49 else get_assumptions_ pt (p, Res)
1.50 in (bdv, pred) end
1.51 | mk_set _ _ _ l _ =
1.52 - error ("check_elementwise: no set " ^ term2str l);
1.53 + error ("check_elementwise: no set " ^ Celem.term2str l);
1.54
1.55 (* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
1.56 fun check_elementwise thy erls all_results (bdv, asm) =
1.57 @@ -142,7 +142,7 @@
1.58 in
1.59 case Specify.refine_ori oris pI of
1.60 SOME pblID =>
1.61 - Chead.Appl (Tac.Refine_Tacitly' (pI, pblID, e_domID, e_metID, [](*filled in specify*)))
1.62 + Chead.Appl (Tac.Refine_Tacitly' (pI, pblID, Celem.e_domID, Celem.e_metID, [](*filled in specify*)))
1.63 | NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Tacitly pI)) ^ " not applicable")
1.64 end
1.65 | applicable_in (p, p_) pt (Tac.Refine_Problem pI) =
1.66 @@ -154,9 +154,9 @@
1.67 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
1.68 => (dI, dI', itms)
1.69 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
1.70 - val thy = if dI' = e_domID then dI else dI';
1.71 + val thy = if dI' = Celem.e_domID then dI else dI';
1.72 in
1.73 - case Specify.refine_pbl (assoc_thy thy) pI itms of
1.74 + case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
1.75 NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable")
1.76 | SOME (rf as (pI', _)) =>
1.77 if pI' = pI
1.78 @@ -202,9 +202,9 @@
1.79 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
1.80 => (oris, dI, pI, dI', pI', itms)
1.81 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
1.82 - val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.83 + val thy = Celem.assoc_thy (if dI' = Celem.e_domID then dI else dI');
1.84 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
1.85 - val pbl = if pI' = e_pblID andalso pI = e_pblID
1.86 + val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
1.87 then (false, (Generate.init_pbl ppc, []))
1.88 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
1.89 in
1.90 @@ -225,7 +225,7 @@
1.91 val {where_, ...} = Specify.get_pbt pI
1.92 val pres = map (Model.mk_env probl |> subst_atomic) where_
1.93 val ctxt = if is_e_ctxt ctxt
1.94 - then assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres
1.95 + then Celem.assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres
1.96 else ctxt
1.97 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.98 and then decide on Chead.Notappl/Appl accordingly once more.
1.99 @@ -237,7 +237,7 @@
1.100 | applicable_in (p, p_) _ (Tac.Check_Postcond pI) =
1.101 if member op = [Pbl, Met] p_
1.102 then Chead.Notappl ((Tac.tac2str (Tac.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
1.103 - else Chead.Appl (Tac.Check_Postcond' (pI, (e_term, [(*fun solve assigns returnvalue of scr*)])))
1.104 + else Chead.Appl (Tac.Check_Postcond' (pI, (Celem.e_term, [(*fun solve assigns returnvalue of scr*)])))
1.105 | applicable_in _ _ (Tac.Take str) = Chead.Appl (Tac.Take' (TermC.str2term str)) (* always applicable ?*)
1.106 | applicable_in _ _ (Tac.Free_Solve) = Chead.Appl (Tac.Free_Solve') (* always applicable *)
1.107 | applicable_in (p, p_) pt (m as Tac.Rewrite_Inst (subs, thm'')) =
1.108 @@ -246,8 +246,8 @@
1.109 else
1.110 let
1.111 val pp = par_pblobj pt p;
1.112 - val thy' = (get_obj g_domID pt pp): theory';
1.113 - val thy = assoc_thy thy';
1.114 + val thy' = get_obj g_domID pt pp;
1.115 + val thy = Celem.assoc_thy thy';
1.116 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
1.117 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
1.118 Frm => (get_obj g_form pt p, p)
1.119 @@ -257,7 +257,7 @@
1.120 let
1.121 val subst = Selem.subs2subst thy subs;
1.122 in
1.123 - case Rewrite.rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
1.124 + case Rewrite.rewrite_inst_ thy (Celem.assoc_rew_ord ro') erls false subst (snd thm'') f of
1.125 SOME (f',asm) =>
1.126 Chead.Appl (Tac.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
1.127 | NONE => Chead.Notappl ((fst thm'')^" not applicable")
1.128 @@ -270,7 +270,7 @@
1.129 else
1.130 let
1.131 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
1.132 - val thy = assoc_thy thy';
1.133 + val thy = Celem.assoc_thy thy';
1.134 val f = case p_ of
1.135 Frm => get_obj g_form pt p
1.136 | Res => (fst o (get_obj g_result pt)) p
1.137 @@ -278,7 +278,7 @@
1.138 in
1.139 if msg = "OK"
1.140 then
1.141 - case Rewrite.rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
1.142 + case Rewrite.rewrite_ thy (Celem.assoc_rew_ord ro) rls' false (snd thm'') f of
1.143 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
1.144 | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable")
1.145 else Chead.Notappl msg
1.146 @@ -289,15 +289,15 @@
1.147 else
1.148 let
1.149 val pp = par_pblobj pt p;
1.150 - val thy' = (get_obj g_domID pt pp):theory';
1.151 - val thy = assoc_thy thy';
1.152 + val thy' = get_obj g_domID pt pp;
1.153 + val thy = Celem.assoc_thy thy';
1.154 val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp);
1.155 val (f, _) = case p_ of
1.156 Frm => (get_obj g_form pt p, p)
1.157 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.158 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.159 in
1.160 - case Rewrite.rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
1.161 + case Rewrite.rewrite_ thy (Celem.assoc_rew_ord ro') erls false (snd thm'') f of
1.162 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
1.163 | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end
1.164 | applicable_in (p, p_) pt (m as Tac.Detail_Set_Inst (subs, rls)) =
1.165 @@ -307,7 +307,7 @@
1.166 let
1.167 val pp = par_pblobj pt p;
1.168 val thy' = get_obj g_domID pt pp;
1.169 - val thy = assoc_thy thy';
1.170 + val thy = Celem.assoc_thy thy';
1.171 val f = case p_ of Frm => get_obj g_form pt p
1.172 | Res => (fst o (get_obj g_result pt)) p
1.173 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.174 @@ -326,7 +326,7 @@
1.175 let
1.176 val pp = par_pblobj pt p;
1.177 val thy' = get_obj g_domID pt pp;
1.178 - val thy = assoc_thy thy';
1.179 + val thy = Celem.assoc_thy thy';
1.180 val (f, _) = case p_ of
1.181 Frm => (get_obj g_form pt p, p)
1.182 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.183 @@ -351,7 +351,7 @@
1.184 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.185 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.186 in
1.187 - case Rewrite.rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.188 + case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
1.189 SOME (f', asm)
1.190 => Chead.Appl (Tac.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.191 | NONE => Chead.Notappl (rls ^ " not applicable")
1.192 @@ -368,7 +368,7 @@
1.193 | Res => (fst o (get_obj g_result pt)) p
1.194 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.195 in
1.196 - case Rewrite.rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.197 + case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
1.198 SOME (f',asm) => Chead.Appl (Tac.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
1.199 | NONE => Chead.Notappl (rls^" not applicable")
1.200 end
1.201 @@ -386,9 +386,9 @@
1.202 in
1.203 if msg = "OK"
1.204 then
1.205 - case Rewrite.calculate_ (assoc_thy thy') isa_fn f of
1.206 + case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
1.207 SOME (f', (id, thm))
1.208 - => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, string_of_thmI thm))))
1.209 + => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, Celem.string_of_thmI thm))))
1.210 | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable")
1.211 else Chead.Notappl msg
1.212 end
1.213 @@ -401,7 +401,7 @@
1.214 else
1.215 let
1.216 val pp = par_pblobj pt p
1.217 - val thy = assoc_thy (get_obj g_domID pt pp)
1.218 + val thy = Celem.assoc_thy (get_obj g_domID pt pp)
1.219 val f = case p_ of
1.220 Frm => get_obj g_form pt p
1.221 | Res => (fst o (get_obj g_result pt)) p
1.222 @@ -409,7 +409,7 @@
1.223 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
1.224 val subte = Selem.sube2subte sube
1.225 val subst = Selem.sube2subst thy sube
1.226 - val ro = assoc_rew_ord rew_ord'
1.227 + val ro = Celem.assoc_rew_ord rew_ord'
1.228 in
1.229 if foldl and_ (true, map TermC.contains_Var subte)
1.230 then (*1*)
1.231 @@ -433,12 +433,12 @@
1.232 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
1.233 case get_obj g_env pt p of
1.234 SOME _ =>
1.235 - Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
1.236 - e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID))
1.237 + Chead.Appl (Tac.Subproblem' ((domID, pblID, Celem.e_metID), [],
1.238 + Celem.e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID))
1.239 | NONE => Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.240 else (*somewhere later in the script*)
1.241 - Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
1.242 - e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID))
1.243 + Chead.Appl (Tac.Subproblem' ((domID, pblID, Celem.e_metID), [],
1.244 + Celem.e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID))
1.245 | applicable_in _ _ (Tac.End_Subproblem) =
1.246 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Subproblem)
1.247 | applicable_in _ _ (Tac.CAScmd ct') =
1.248 @@ -458,7 +458,7 @@
1.249 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
1.250 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.251 in (Chead.Appl (Tac.Begin_Trans' f))
1.252 - handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ term2str f ^ "'")
1.253 + handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ Celem.term2str f ^ "'")
1.254 end
1.255 | applicable_in (p, p_) pt (Tac.End_Trans) = (*TODO: check parent branches*)
1.256 if p_ = Res
1.257 @@ -478,15 +478,15 @@
1.258 else
1.259 let
1.260 val pp = par_pblobj pt p;
1.261 - val thy' = (get_obj g_domID pt pp):theory';
1.262 - val thy = assoc_thy thy'
1.263 + val thy' = get_obj g_domID pt pp;
1.264 + val thy = Celem.assoc_thy thy'
1.265 val metID = (get_obj g_metID pt pp)
1.266 val {crls,...} = Specify.get_met metID
1.267 val (f, asm) = case p_ of
1.268 Frm => (get_obj g_form pt p , [])
1.269 | Res => get_obj g_result pt p
1.270 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.271 - val vp = (thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
1.272 + val vp = (Celem.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
1.273 in case f of
1.274 Const ("List.list.Cons",_) $ _ $ _ =>
1.275 Chead.Appl (Tac.Check_elementwise' (f, pred, check_elementwise thy crls f vp))
1.276 @@ -494,7 +494,7 @@
1.277 Chead.Appl (Tac.Check_elementwise' (f, pred, (f,asm)))
1.278 | Const ("List.list.Nil",_) =>
1.279 Chead.Appl (Tac.Check_elementwise' (f, pred, (f, asm)))
1.280 - | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ term2str f ^ " should be constants")
1.281 + | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ Celem.term2str f ^ " should be constants")
1.282 end
1.283 | applicable_in (p, p_) pt Tac.Or_to_List =
1.284 if member op = [Pbl, Met] p_
1.285 @@ -507,7 +507,7 @@
1.286 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
1.287 in (let val ls = or2list f
1.288 in Chead.Appl (Tac.Or_to_List' (f, ls)) end)
1.289 - handle _ => Chead.Notappl ("'Or_to_List' not applicable to "^(term2str f))
1.290 + handle _ => Chead.Notappl ("'Or_to_List' not applicable to " ^ Celem.term2str f)
1.291 end
1.292 | applicable_in _ _ Tac.Collect_Trues =
1.293 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Collect_Trues)
1.294 @@ -515,8 +515,8 @@
1.295 | applicable_in (p, p_) pt (Tac.Tac id) =
1.296 let
1.297 val pp = par_pblobj pt p;
1.298 - val thy' = (get_obj g_domID pt pp):theory';
1.299 - val thy = assoc_thy thy';
1.300 + val thy' = get_obj g_domID pt pp;
1.301 + val thy = Celem.assoc_thy thy';
1.302 val f = case p_ of
1.303 Frm => get_obj g_form pt p
1.304 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
1.305 @@ -525,18 +525,18 @@
1.306 in case id of
1.307 "subproblem_equation_dummy" =>
1.308 if TermC.is_expliceq f
1.309 - then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "subproblem_equation_dummy (" ^ term2str f ^ ")"))
1.310 + then Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "subproblem_equation_dummy (" ^ Celem.term2str f ^ ")"))
1.311 else Chead.Notappl "applicable only to equations made explicit"
1.312 | "solve_equation_dummy" =>
1.313 - let val (id', f') = split_dummy (term2str f);
1.314 + let val (id', f') = split_dummy (Celem.term2str f);
1.315 in
1.316 if id' <> "subproblem_equation_dummy"
1.317 then Chead.Notappl "no subproblem"
1.318 - else if (thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
1.319 - then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
1.320 + else if (Celem.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
1.321 + then Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "[" ^ f' ^ "]"))
1.322 else error ("applicable_in: f= " ^ f')
1.323 end
1.324 - | _ => Chead.Appl (Tac.Tac_ (thy, term2str f, id, term2str f))
1.325 + | _ => Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, Celem.term2str f))
1.326 end
1.327 | applicable_in _ _ Tac.End_Proof' = Chead.Appl Tac.End_Proof''
1.328 | applicable_in _ _ m = error ("applicable_in called for " ^ Tac.tac2str m);