1.1 --- a/src/Tools/isac/Interpret/generate.sml Sat Mar 19 15:18:10 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Mar 21 00:32:53 2011 +0100
1.3 @@ -102,11 +102,11 @@
1.4 (tac * (*for comparison with input tac*)
1.5 tac_ * (*for ptree generation*)
1.6 (pos' * (*after applying tac_, for ptree generation*)
1.7 - istate)); (*after applying tac_, for ptree generation*)
1.8 -val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci;
1.9 + (istate * Proof.context))); (*after applying tac_, for ptree generation*)
1.10 +val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
1.11 (* val (tac, tac_, (pos', istate))::_ = tacis';
1.12 *)
1.13 -fun taci2str ((tac, tac_, (pos', istate)):taci) =
1.14 +fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
1.15 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
1.16 ^", "^istate2str istate^" ))";
1.17 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
1.18 @@ -259,25 +259,25 @@
1.19
1.20 (*generate 1 ppobj in ptree*)
1.21 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
1.22 -fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.23 +fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
1.24 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
1.25 (Upblmet,itms2itemppc thy [][]))),
1.26 case p_ of Pbl => update_pbl pt p itmlist
1.27 | Met => update_met pt p itmlist)
1.28 - | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.29 + | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
1.30 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.31 case p_ of Pbl => update_pbl pt p itmlist
1.32 | Met => update_met pt p itmlist)
1.33 - | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt =
1.34 + | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
1.35 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.36 case p_ of Pbl => update_pbl pt p itmlist
1.37 | Met => update_met pt p itmlist)
1.38
1.39 - | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt =
1.40 + | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
1.41 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.42 update_domID pt p domID)
1.43
1.44 - | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate
1.45 + | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
1.46 (pos as (p,_)) pt =
1.47 let val pt = update_pbl pt p itms
1.48 val pt = update_pblID pt p pI
1.49 @@ -285,7 +285,7 @@
1.50 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.51 pt) end
1.52
1.53 - | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate
1.54 + | generate1 thy (Specify_Method' (mID, oris, itms)) _
1.55 (pos as (p,_)) pt =
1.56 let val pt = update_oris pt p oris
1.57 val pt = update_met pt p itms
1.58 @@ -294,7 +294,7 @@
1.59 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.60 pt) end
1.61
1.62 - | generate1 thy (Model_Problem' (_, itms, met)) Uistate (pos as (p,_)) pt =
1.63 + | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
1.64 (* val (itms,pos as (p,_)) = (pbl, pos);
1.65 *)
1.66 let val pt = update_pbl pt p itms
1.67 @@ -303,32 +303,32 @@
1.68 (Upblmet,itms2itemppc thy [][]))), pt) end
1.69
1.70 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
1.71 - Uistate (pos as (p,_)) pt =
1.72 + _ (pos as (p,_)) pt =
1.73 let val pt = update_pbl pt p pbl
1.74 val pt = update_orispec pt p (domID,pIre,metID)
1.75 in (pos,[],
1.76 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
1.77 pt) end
1.78
1.79 - | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt =
1.80 + | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
1.81 let val (dI,_,mI) = get_obj g_spec pt p
1.82 val pt = update_spec pt p (dI, pI, mI)
1.83 in (pos,[],
1.84 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
1.85 end
1.86
1.87 - | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
1.88 + | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
1.89 ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
1.90 tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
1.91 tracing("###generate1 Apply_Method': is = "^istate2str is);*)
1.92 case topt of
1.93 SOME t =>
1.94 - let val (pt,c) = cappend_form pt p is t
1.95 + let val (pt,c) = cappend_form pt p (is, ctxt) t
1.96 (*val _= tracing("###generate1 Apply_Method: after cappend")*)
1.97 in (pos,c, EmptyMout,pt)
1.98 end
1.99 | NONE =>
1.100 - (pos,[],EmptyMout,update_env pt p (SOME is)))
1.101 + (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
1.102 (* val (thy, (Take' t), l, (p,p_), pt) =
1.103 ((assoc_thy "Isac"), tac_, is, pos, pt);
1.104 *)
1.105 @@ -409,10 +409,11 @@
1.106 let val (pt,c) = cappend_form pt p l f
1.107 val pt = update_branch pt p TransitiveB (*040312*)
1.108
1.109 + val ctxt = e_ctxt;
1.110 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.111 - val tac_ = Apply_Method' (e_metID, SOME t, is)
1.112 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
1.113 val pos' = ((lev_on o lev_dn) p, Frm)
1.114 - in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.115 + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
1.116
1.117 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
1.118 let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
1.119 @@ -427,10 +428,11 @@
1.120 let val (pt,c) = cappend_form pt p l f
1.121 val pt = update_branch pt p TransitiveB (*040312*)
1.122
1.123 + val ctxt = e_ctxt;
1.124 val is = init_istate (Rewrite_Set (id_rls rls)) f
1.125 - val tac_ = Apply_Method' (e_metID, SOME t, is)
1.126 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
1.127 val pos' = ((lev_on o lev_dn) p, Frm)
1.128 - in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.129 + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
1.130
1.131 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
1.132 let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
1.133 @@ -485,12 +487,11 @@
1.134 error ("generate1: not impl.for "^(tac_2str m'))
1.135 ;
1.136
1.137 -
1.138 fun generate_hard thy m' (p,p_) pt =
1.139 let
1.140 val p = case p_ of Frm => p | Res => lev_on p
1.141 | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
1.142 - in generate1 thy m' e_istate (p,p_) pt end;
1.143 + in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
1.144
1.145
1.146
1.147 @@ -549,14 +550,14 @@
1.148 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
1.149 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
1.150 let val (res, asm) = (res_from_taci o last_elem) tacis
1.151 - val (SOME ist,_) = get_obj g_loc pt p
1.152 + val (SOME (ist, ctxt),_) = get_obj g_loc pt p
1.153 val form = get_obj g_form pt p
1.154 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.155 - val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate))
1.156 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt)))
1.157 ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.158 @ [(End_Trans, End_Trans' (res, asm),
1.159 (pos_plus (length tacis) (lev_dn p, Res),
1.160 - new_val res ist))]
1.161 + (new_val res ist, ctxt)))]
1.162 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.163 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.164 val pt = update_tac pt p (Derive (id_rls nrls))
1.165 @@ -570,14 +571,14 @@
1.166 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
1.167 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
1.168 let val (res, asm) = (res_from_taci o last_elem) tacis
1.169 - val (_, SOME ist) = get_obj g_loc pt p
1.170 + val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
1.171 val (f,a) = get_obj g_result pt p
1.172 val p = lev_on p(*---------------only difference to (..,Frm) above*);
1.173 - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate))
1.174 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt)))
1.175 ::(insert_pos ((lev_on o lev_dn) p) tacis)
1.176 @ [(End_Trans, End_Trans' (res, asm),
1.177 (pos_plus (length tacis) (lev_dn p, Res),
1.178 - new_val res ist))];
1.179 + (new_val res ist, ctxt)))];
1.180 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.181 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
1.182 val pt = update_tac pt p (Derive (id_rls nrls))