1.1 --- a/src/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -58,8 +58,8 @@
1.4 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
1.5 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
1.6
1.7 -fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
1.8 - | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
1.9 +fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
1.10 + | rule2thm'' r = error ("rule2thm': not defined for "^(rule2str r));
1.11 fun rule2rls' (Rls_ rls) = id_rls rls
1.12 | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
1.13
1.14 @@ -69,7 +69,7 @@
1.15 let
1.16 val thy = assoc_thy thy'
1.17 val ctxt = get_ctxt pt p |> insert_assumptions am
1.18 - val m = Rewrite' (thy', ro, er, pa, rule2thm' r, f, (f', am))
1.19 + val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.20 val is = RrlsState (f', f'', rss, rts)
1.21 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.22 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.23 @@ -78,7 +78,7 @@
1.24 let
1.25 val thy = assoc_thy thy'
1.26 val ctxt = get_ctxt pt p |> insert_assumptions am
1.27 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
1.28 + val m = Rewrite' (thy',ro,er,pa, rule2thm'' r, f, (f', am))
1.29 val is = RrlsState (f',f'',rss,rts)
1.30 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.31 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.32 @@ -340,20 +340,19 @@
1.33 (*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac,
1.34 then convert to a 'tac_' (as required in appy).
1.35 arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
1.36 -fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
1.37 +fun stac2tac_ _ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ _) =
1.38 let
1.39 val tid = (de_esc_underscore o strip_thy) thmID
1.40 - in (Rewrite (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term)), Empty_Tac_)
1.41 + in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_)
1.42 end
1.43
1.44 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) =
1.45 + | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ _) =
1.46 let
1.47 val subML = ((map isapair2pair) o isalist2list) sub
1.48 val subStr = subst2subs subML
1.49 val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
1.50 - in (Rewrite_Inst (subStr, (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term))), Empty_Tac_)
1.51 - end
1.52 -
1.53 + in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
1.54 +
1.55 | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
1.56 (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
1.57
1.58 @@ -462,7 +461,7 @@
1.59 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.60 NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.61 *)
1.62 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', asm))) stac =
1.63 +fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm'' as (thmID, _), f, (f', asm))) stac =
1.64 (case stac of
1.65 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
1.66 if thmID = thmID_
1.67 @@ -472,12 +471,12 @@
1.68 else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
1.69 else ((*tracing"3### assod ..NotAss";*)NotAss)
1.70 | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
1.71 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
1.72 + if contains_rule (Thm thm'') (assoc_rls rls_)
1.73 then
1.74 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.75 else NotAss
1.76 | _ => NotAss)
1.77 - | assod pt d (m as Rewrite' (thy, rod, rls, put, (thmID, _), f, (f', asm))) stac =
1.78 + | assod pt d (m as Rewrite' (thy, rod, rls, put, thm'' as (thmID, _), f, (f', asm))) stac =
1.79 (case stac of
1.80 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.81 ((*tracing ("3### assod: stac = " ^ ter2str t);
1.82 @@ -493,7 +492,7 @@
1.83 AssWeak (m,f'))
1.84 else ((*tracing"3### assod ..NotAss";*)NotAss))
1.85 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
1.86 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
1.87 + if contains_rule (Thm thm'') (assoc_rls rls_)
1.88 then
1.89 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.90 else NotAss
1.91 @@ -642,10 +641,8 @@
1.92 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
1.93 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
1.94
1.95 - | tac_2tac (Rewrite' (thy,rod,erls,put, thm',f,(f',asm))) = Rewrite (thm'_to_thm'' thm')
1.96 -
1.97 - | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm', _, _))=
1.98 - Rewrite_Inst (subst2subs sub, thm'_to_thm'' thm')
1.99 + | tac_2tac (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
1.100 + | tac_2tac (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (subst2subs sub, thm)
1.101
1.102 | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
1.103 | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
1.104 @@ -1177,9 +1174,9 @@
1.105 NOT IMPL. -- "error: do other step before"
1.106 NotLocatable: thus generate_hard
1.107 *)
1.108 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, (thmID, str), f, _)) (pt, p)
1.109 +fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
1.110 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.111 - (case lo rss f (Thm (thmID, mk_thm (assoc_thy thy') str)) of
1.112 + (case lo rss f (Thm thm) of
1.113 [] => NotLocatable
1.114 | rts' =>
1.115 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.116 @@ -1459,10 +1456,9 @@
1.117 else
1.118 (case next_rule rss f of
1.119 NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.120 - | SOME (Thm (id, thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.121 - (Rewrite' (thy, "e_rew_ord", e_rls, false,
1.122 - (id, thm |> Thm.prop_of |> term2str), f, (e_term, [(*!?!8.6.03*)])),
1.123 - (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.124 + | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
1.125 + (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
1.126 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.127
1.128 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
1.129 (ScrState (E,l,a,v,s,b), ctxt) =
1.130 @@ -1630,7 +1626,7 @@
1.131 Frm => get_obj g_form pt p
1.132 | Res => (fst o (get_obj g_result pt)) p
1.133 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
1.134 - in (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
1.135 + in ((gen_distinct eq_tac) o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
1.136
1.137
1.138 (*