1.1 --- a/src/Tools/isac/Interpret/script.sml Sun Oct 16 13:58:46 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
1.3 @@ -58,7 +58,7 @@
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 (_, thm)) = thm
1.8 +fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
1.9 | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
1.10 fun rule2rls' (Rls_ rls) = id_rls rls
1.11 | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
1.12 @@ -462,10 +462,8 @@
1.13 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.14 NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.15 *)
1.16 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', asm))) stac =
1.17 - let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
1.18 - in
1.19 - (case stac of
1.20 +fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', asm))) stac =
1.21 + (case stac of
1.22 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
1.23 if thmID = thmID_
1.24 then
1.25 @@ -479,11 +477,8 @@
1.26 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.27 else NotAss
1.28 | _ => NotAss)
1.29 - end
1.30 - | assod pt d (m as Rewrite' (thy, rod, rls, put, thm, f, (f', asm))) stac =
1.31 - let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
1.32 - in
1.33 - (case stac of
1.34 + | assod pt d (m as Rewrite' (thy, rod, rls, put, (thmID, _), f, (f', asm))) stac =
1.35 + (case stac of
1.36 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.37 ((*tracing ("3### assod: stac = " ^ ter2str t);
1.38 tracing ("3### assod: f(m)= " ^ term2str f);*)
1.39 @@ -503,7 +498,6 @@
1.40 if f = f_ then Ass (m,f') else AssWeak (m,f')
1.41 else NotAss
1.42 | _ => NotAss)
1.43 - end
1.44
1.45 | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
1.46 (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
1.47 @@ -648,10 +642,10 @@
1.48 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
1.49 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
1.50
1.51 - | tac_2tac (Rewrite' (_(*thy*), _, _, _, thm, _, _)) = Rewrite (thm''_of_thm thm)
1.52 + | tac_2tac (Rewrite' (thy,rod,erls,put, thm',f,(f',asm))) = Rewrite (thm'_to_thm'' thm')
1.53
1.54 - | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm, _, _))=
1.55 - Rewrite_Inst (subst2subs sub, thm''_of_thm thm)
1.56 + | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm', _, _))=
1.57 + Rewrite_Inst (subst2subs sub, thm'_to_thm'' thm')
1.58
1.59 | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
1.60 | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
1.61 @@ -698,7 +692,7 @@
1.62 (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
1.63 NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!
1.64 WN0508 only use in tac_2res, which uses only last return-value*)
1.65 -fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', _))) =
1.66 +fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
1.67 let val fT = type_of f;
1.68 val b = if put then @{term True} else @{term False};
1.69 val sT = (type_of o fst o hd) subs;
1.70 @@ -706,7 +700,7 @@
1.71 (map HOLogic.mk_prod subs);
1.72 val sT' = type_of subs';
1.73 val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT)
1.74 - $ subs' $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
1.75 + $ subs' $ Free (thmID, idT) $ b $ f;
1.76 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.77 (*Fehlersuche 25.4.01
1.78 (a)----- als String zusammensetzen:
1.79 @@ -749,12 +743,12 @@
1.80 ("Script","tless_true","eval_rls",false,subs,
1.81 ("square_equation_left",""),f,(f',[])));
1.82 *)
1.83 - | rep_tac_ (Rewrite' (thy', _, _, put, thm, f, (f', _)))=
1.84 + | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.85 let
1.86 val fT = type_of f;
1.87 val b = if put then @{term True} else @{term False};
1.88 val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
1.89 - $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
1.90 + $ Free (thmID, idT) $ b $ f;
1.91 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.92 (*
1.93 > val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
1.94 @@ -1183,9 +1177,9 @@
1.95 NOT IMPL. -- "error: do other step before"
1.96 NotLocatable: thus generate_hard
1.97 *)
1.98 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
1.99 +fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, (thmID, str), f, _)) (pt, p)
1.100 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.101 - (case lo rss f (Thm (thmID_of_derivation_name' thm, thm)) of
1.102 + (case lo rss f (Thm (thmID, mk_thm (assoc_thy thy') str)) of
1.103 [] => NotLocatable
1.104 | rts' =>
1.105 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.106 @@ -1465,9 +1459,9 @@
1.107 else
1.108 (case next_rule rss f of
1.109 NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.110 - | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.111 - (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.112 - thm, f, (e_term, [(*!?!8.6.03*)])),
1.113 + | SOME (Thm (id, thm))(*8.6.03: muss auch f' liefern ?!!*) =>
1.114 + (Rewrite' (thy, "e_rew_ord", e_rls, false,
1.115 + (id, thm |> Thm.prop_of |> term2str), f, (e_term, [(*!?!8.6.03*)])),
1.116 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.117
1.118 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))