1.1 --- a/src/Tools/isac/Interpret/generate.sml Fri Apr 15 15:58:52 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri Apr 15 17:07:34 2011 +0200
1.3 @@ -373,18 +373,21 @@
1.4 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
1.5 pt) end
1.6
1.7 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
1.8 + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt)
1.9 + (p,p_) pt =
1.10 let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
1.11 - val (pt,c) = cappend_atomic pt p l f
1.12 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.13 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
1.14 val pt = update_branch pt p TransitiveB (*040312*)
1.15 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.16 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.17 pt) end
1.18
1.19 - | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
1.20 + | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt)
1.21 + (p,p_) pt =
1.22 let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
1.23 - val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
1.24 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.25 + (Rewrite thm') (f',asm) Complete
1.26 val pt = update_branch pt p TransitiveB (*040312*)
1.27 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.28 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.29 @@ -393,44 +396,46 @@
1.30 | generate1 thy (Rewrite_Asm' all) l p pt =
1.31 generate1 thy (Rewrite' all) l p pt
1.32
1.33 - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
1.34 + | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt)
1.35 + (p,p_) pt =
1.36 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
1.37 (assoc_thy "Isac", tac_, is, pos, pt);
1.38 *)
1.39 let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
1.40 - val (pt,c) = cappend_atomic pt p l f
1.41 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.42 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.43 val pt = update_branch pt p TransitiveB (*040312*)
1.44 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.45 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.46 pt) end
1.47
1.48 - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt =
1.49 - let val (pt,c) = cappend_form pt p l f
1.50 + | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_)
1.51 + pt =
1.52 + let val ctxt' = insert_assumptions asm ctxt
1.53 + val (pt,c) = cappend_form pt p (is, ctxt') f
1.54 val pt = update_branch pt p TransitiveB (*040312*)
1.55 + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.56 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.57 + val pos' = ((lev_on o lev_dn) p, Frm)
1.58 + in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.59
1.60 - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.61 - val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
1.62 - val pos' = ((lev_on o lev_dn) p, Frm)
1.63 - in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
1.64 -
1.65 - | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
1.66 + | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.67 let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
1.68 - val (pt,c) = cappend_atomic pt p l f
1.69 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.70 (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.71 val pt = update_branch pt p TransitiveB (*040312*)
1.72 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.73 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.74 pt) end
1.75
1.76 - | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt =
1.77 - let val (pt,c) = cappend_form pt p l f
1.78 + | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
1.79 + let val (pt,c) = cappend_form pt p (is, ctxt) f
1.80 val pt = update_branch pt p TransitiveB (*040312*)
1.81
1.82 val is = init_istate (Rewrite_Set (id_rls rls)) f
1.83 - val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
1.84 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
1.85 val pos' = ((lev_on o lev_dn) p, Frm)
1.86 - in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
1.87 + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
1.88
1.89 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
1.90 let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
1.91 @@ -552,7 +557,7 @@
1.92 val (SOME (ist, ctxt),_) = get_obj g_loc pt p
1.93 val form = get_obj g_form pt p
1.94 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.95 - val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt)))
1.96 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
1.97 ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.98 @ [(End_Trans, End_Trans' (res, asm),
1.99 (pos_plus (length tacis) (lev_dn p, Res),
1.100 @@ -573,7 +578,7 @@
1.101 val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
1.102 val (f,a) = get_obj g_result pt p
1.103 val p = lev_on p(*---------------only difference to (..,Frm) above*);
1.104 - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt)))
1.105 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
1.106 ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.107 @ [(End_Trans, End_Trans' (res, asm),
1.108 (pos_plus (length tacis) (lev_dn p, Res),