1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Jan 05 17:43:48 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Jan 07 10:06:06 2012 +0100
1.3 @@ -468,17 +468,21 @@
1.4 term (*for itr_arg,result in ets*)
1.5 | NotAss;
1.6
1.7 -(*.assod: tac_ associated with stac w.r.t. d
1.8 +(* check if tac_ is associated with stac.
1.9 + Additional task: check if term t (the result has been calculated from) in tac_
1.10 + has been changed (see "datatype tac_"); if yes, recalculate result
1.11 + TODO.WN120106 recalculate impl.only for Substitute'
1.12 args
1.13 - pt:ptree for pushing the thy specified in rootpbl into subpbls
1.14 + pt : ptree for pushing the thy specified in rootpbl into subpbls
1.15 + d : unused (planned for data for comparison)
1.16 + tac_ : from user (via applicable_in); to be compared with ...
1.17 + stac : found in Script
1.18 returns
1.19 - Ass : associated: e.g. thmID in stac = thmID in m
1.20 + Ass : associated: e.g. thmID in stac = thmID in m
1.21 +++ arg in stac = arg in m
1.22 - AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.23 - NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.24 -8.01:
1.25 - tac_ SubProblem with args completed from script
1.26 -.*)
1.27 + AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.28 + NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.29 +*)
1.30 fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
1.31 (case stac of
1.32 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
1.33 @@ -579,8 +583,18 @@
1.34 | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
1.35 Ass (m, term)
1.36
1.37 - | assod pt _ (m as Substitute' (_, _, res)) (Const ("Script.Substitute",_) $ _ $ _) =
1.38 - Ass (m, res)
1.39 + | assod pt _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute",_) $ _ $ t) =
1.40 + if f = t then Ass (m, f')
1.41 + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.42 + if foldl and_ (true, map contains_Var subte)
1.43 + then
1.44 + let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
1.45 + in if t = t' then error "assod: Substitute' not applicable to val of Expr"
1.46 + else Ass (Substitute' (ro, erls, subte, t, t'), t')
1.47 + end
1.48 + else (case rewrite_terms_ (Isac()) ro erls subte t of
1.49 + SOME (t', _) => Ass (Substitute' (ro, erls, subte, t, t'), t')
1.50 + | NONE => error "assod: Substitute' not applicable to val of Expr")
1.51
1.52 | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
1.53 if id = id'
1.54 @@ -664,7 +678,7 @@
1.55
1.56 | tac_2tac (Or_to_List' _) = Or_to_List
1.57 | tac_2tac (Take' term) = Take (term2str term)
1.58 - | tac_2tac (Substitute' (subte, t, res)) = Substitute (subte2sube subte)
1.59 + | tac_2tac (Substitute' (_, _, subte, t, res)) = Substitute (subte2sube subte)
1.60
1.61 | tac_2tac (Tac_ (_,f,id,f')) = Tac id
1.62
1.63 @@ -829,7 +843,7 @@
1.64 | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
1.65 | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
1.66 | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
1.67 - | rep_tac_ (Substitute' (subst,t,t')) = (Erule, (t, t'))
1.68 + | rep_tac_ (Substitute' (_, _, subst,t,t')) = (Erule, (t, t'))
1.69 | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
1.70 | rep_tac_ m = error ("rep_tac_: not impl.for "^
1.71 (tac_2str m));
1.72 @@ -843,9 +857,9 @@
1.73
1.74
1.75 (* handle a leaf at the end of recursive descent:
1.76 - a leaf is either a tactic or an 'exp' in 'let v = expr'
1.77 - where 'exp' does not contain a tactic.
1.78 - handling a leaf comprises
1.79 + a leaf is either a tactic or an 'expr' in "let v = expr"
1.80 + where "expr" does not contain a tactic.
1.81 + Handling a leaf comprises
1.82 (1) 'subst_stacexpr' substitute env and complete curried tactic
1.83 (2) rewrite the leaf by 'srls'
1.84 *)
1.85 @@ -854,7 +868,7 @@
1.86 case subst_stacexpr E a v t of
1.87 (a', STac stac) => (*script-tactic*)
1.88 let val stac' =
1.89 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.90 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.91 in
1.92 (if (!trace_script)
1.93 then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
1.94 @@ -863,12 +877,12 @@
1.95 end
1.96 | (a', Expr lexpr) => (*leaf-expression*)
1.97 let val lexpr' =
1.98 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.99 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.100 in
1.101 (if (!trace_script)
1.102 then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
1.103 else ();
1.104 - (a', Expr lexpr'))
1.105 + (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
1.106 end;
1.107
1.108
1.109 @@ -917,7 +931,7 @@
1.110 val id' = mk_Free (id, T);
1.111 val E' = upd_env E' (id', v);
1.112 in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.113 - | NasNap (v,E) =>
1.114 + | NasNap (v,E) =>
1.115 let
1.116 val id' = mk_Free (id, T);
1.117 val E' = upd_env E (id', v);
1.118 @@ -983,7 +997,7 @@
1.119 (case handle_leaf "locate" thy' sr E a v t of
1.120 (a', Expr s) =>
1.121 (NasNap (eval_listexpr_ (assoc_thy thy') sr
1.122 - (subst_atomic (upd_env_opt E (a',v)) t), E))
1.123 + (subst_atomic (upd_env_opt E (a',v)) t), E))
1.124 | (a', STac stac) =>
1.125 let
1.126 val p' =
1.127 @@ -994,7 +1008,7 @@
1.128 case assod pt d m stac of
1.129 Ass (m,v') =>
1.130 let val (p'',c',f',pt') =
1.131 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.132 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.133 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.134 | AssWeak (m,v') =>
1.135 let val (p'',c',f',pt') =
1.136 @@ -1210,11 +1224,12 @@
1.137 (last_elem o fst) p = 0 andalso snd p = Res)
1.138 then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.139 else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.140 - Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
1.141 - (if bb
1.142 - then Steps (ScrState is, ss)
1.143 - else
1.144 - if rew_only ss (*andalso 'not bb'= associated weakly*)
1.145 + Assoc (iss as (is as (_,_,_,_,_,strong_ass), ss as ((m',f',pt',p',c')::_))) =>
1.146 + (if strong_ass
1.147 + then
1.148 + (Steps (ScrState is, ss))
1.149 + else
1.150 + if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
1.151 then
1.152 let
1.153 val (po,p_) = p