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