wneuper/isa: comparison src/Tools/isac/Interpret/solve.sml

equal deleted inserted replaced

-:72187c16c796
+:023ebb7d9759
 (*FIXME.WN050821 compare solve ... nxt_solv*)
 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
 *)
-fun solve ("Apply_Method", m as Apply_Method' (mI, _, _))
+fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _))
 	  (pt:ptree, (pos as (p,_))) =
 let val {srls,...} = get_met mI;
 val PblObj{meth=itms,...} = get_obj I pt p;
 val thy' = get_obj g_domID pt p;
 val thy = assoc_thy thy';
-val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
+val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
 val ini = init_form thy sc env;
 val p = lev_dn p;
 in
 case ini of
 	  SOME t => (* val SOME t = ini;
 	             *)
 	  let val (pos,c,_,pt) =
-		  generate1 thy (Apply_Method' (mI, SOME t, is))
+		  generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
-			    is (lev_on p, Frm)(*implicit Take*) pt;
+			    (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
-	  in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is),
+	  in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
-		      ((lev_on p, Frm), is))], c, (pt,pos)):calcstate')
+		      ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
 	  end
 	| NONE => (*execute the first tac in the Script, compare solve m*)
-	  let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is;
+	  let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
 	      val d = e_rls (*FIXME: get simplifier from domID*);
 	  in
-	      case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of
+	      case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
 		  Steps (is'', ss as (m'',f',pt',p',c')::_) =>
 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
 locate_gen (thy',srls) m'  (pt,(p,Res)) (sc,d) is';
 *)
 		  ("ok", (map step2taci ss, c', (pt',p')))
 		| NotLocatable =>
 		  let val (p,ps,f,pt) =
 			  generate_hard (assoc_thy "Isac") m (p,Frm) pt;
 		  in ("not-found-in-script",
-		      ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
+		      ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
 (*just-before------------------------------------------------------
 	      ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
 		       (pos, is))],
 		     [], (update_env pt (fst pos) (SOME is),pos)))
 -----------------------------------------------------------------*)
 | solve ("Free_Solve", Free_Solve')  (pt,po as (p,_)) =
 let (*val _=tracing"###solve Free_Solve";*)
 val p' = lev_dn_ (p,Res);
 val pt = update_metID pt (par_pblobj pt p) e_metID;
 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
-[(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end
+[(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
 (  m,                                       (pt, pos));
 *)
 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
 		    (snd o (get_obj g_result pt)) p
 		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
 	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
 val metID = get_obj g_metID pt pp;
 val {srls=srls,scr=sc,...} = get_met metID;
-val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
+val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
 val thy' = get_obj g_domID pt pp;
 val thy = assoc_thy thy';
-val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
+val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
 in if pp = [] then
 	   let val is = ScrState (E,l,a,scval,scsaf,b)
 	       val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
-	       val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt;
+	       val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
 	   in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
-	       [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end
+	       [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
 else
 let
 	  (*resume script of parpbl, transfer value of subpbl-script*)
 val ppp = par_pblobj pt (lev_up p);
 	val thy' = get_obj g_domID pt ppp;
 val thy = assoc_thy thy';
 	val metID = get_obj g_metID pt ppp;
 val sc = (#scr o get_met) metID;
-val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
+val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm);
 (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
 	val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
 	val _=tracing("### solve Check_postc, is'= "^
 		      (istate2str (E,l,a,scval,scsaf,b)));*)
 val ((p,p_),ps,f,pt) =
 	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
-		(ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
+		(ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt;
 	(*val _=tracing("### solve Check_postc, is(pt')= "^
 		      (istate2str (get_istate pt ([3],Res))));
 	val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
 				(ScrState (E,l,a,scval,scsaf,b));*)
 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
 	   ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
-	      ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_))))
+	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
 	end
 end
 (* val (msg, cs') =
 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
 	    ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
 (* tracing(istate2str(get_istate pt (p,p_)));
 *)
 | solve (_,End_Proof'') (pt, (p,p_)) =
 ("end-proof",
 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
-[(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_))))
+[(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
 | solve (_,End_Detail' t) (pt,(p,p_)) =
 let val pr as (p',_) = (lev_up p, Res)
 	val pp = par_pblobj pt p
 	val r = (fst o (get_obj g_result pt)) p'
 	(*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
 	val thy' = get_obj g_domID pt pp
 	val (srls, is, sc) = from_pblobj' thy' pr pt
-	val (tac_,is',_) = next_tac (thy',srls)  (pt,pr) sc is
+	val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
 in ("ok", ((*((pp,Frm(*???*)),is,tac_),
 	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
 	tac_2tac tac_, Sundef,*)
 	[(End_Detail, End_Detail' t ,
 	  ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end
 *)
 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
 						      could be detail, too !!*)
 then let val ((p,p_),ps,f,pt) =
 		 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
-			   m e_istate (p,p_) pt;
+			   m (e_istate, e_ctxt) (p,p_) pt;
 	 in ("no-method-specified", (*Free_Solve*)
 	     ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
-	     [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end
+	     [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
 else
 	let
 	    val thy' = get_obj g_domID pt (par_pblobj pt p);
 	    val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
 (*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
 	end;
 (*FIXME.WN050821 compare solve ... nxt_solv*)
 (* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
-fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
+fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
 (* val ((Apply_Method' (mI,_,_)),             _,    (pt:ptree, pos as (p,_))) =
 ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
 *)
 let val {srls,ppc,...} = get_met mI;
 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
 val itms = if itms <> [] then itms
 	       else complete_metitms oris probl [] ppc
 val thy' = get_obj g_domID pt p;
 val thy = assoc_thy thy';
-val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
+val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
 val ini = init_form thy scr env;
 in
 case ini of
 SOME t => (* val SOME t = ini;
 	         *)
 let val pos = ((lev_on o lev_dn) p, Frm)
-	val tac_ = Apply_Method' (mI, SOME t, is);
+	val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
 	val (pos,c,_,pt) = (*implicit Take*)
-	    generate1 thy tac_ is pos pt
+	    generate1 thy tac_ (is, ctxt) pos pt
 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
-in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end
+in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
 | NONE =>
-let val pt = update_env pt (fst pos) (SOME is)
+let val pt = update_env pt (fst pos) (SOME (is, ctxt))
 	val (tacis, c, ptp) = nxt_solve_ (pt, pos)
 in (tacis @
-	[(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))],
+	[(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
 	c, ptp) end
 end
 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) =
 (tac_,                  is,  ptp);
 		    (snd o (get_obj g_result pt)) p
 		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
 	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
 val metID = get_obj g_metID pt pp;
 val {srls=srls,scr=sc,...} = get_met metID;
-val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
+val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
 val thy' = get_obj g_domID pt pp;
 val thy = assoc_thy thy';
-val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
+val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
 in if pp = [] then
 	   let val is = ScrState (E,l,a,scval,scsaf,b)
 	       val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
 (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
 val _= tracing(istate2str is);*)
 	       val ((p,p_),ps,f,pt) =
-		   generate1 thy tac_ is (pp,Res) pt;
+		   generate1 thy tac_ (is, ctxt) (pp,Res) pt;
-	   in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
+	   in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
 else
 let
 	  (*resume script of parpbl, transfer value of subpbl-script*)
 val ppp = par_pblobj pt (lev_up p);
 	val thy' = get_obj g_domID pt ppp;
 val thy = assoc_thy thy';
 	val metID = get_obj g_metID pt ppp;
 	val {scr,...} = get_met metID;
-val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
+val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm)
 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
 	val is = ScrState (E,l,a,scval,scsaf,b)
 (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
 val _= tracing(istate2str is);*)
-val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
+val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
 	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
-in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
+in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
 end
 (* tracing(istate2str(get_istate pt (p,p_)));
 *)
 (*.start interpreter and do one rewrite.*)
 (* val (ptp as (pt, (p,_))) = ptp;
 val (ptp as (pt, (p,_))) = ptp';
 val (ptp as (pt, (p,_))) = (pt, pos);
 *)
 let val (_,_,mI) = get_obj g_spec pt p;
-val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
+val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
-				e_istate ptp;
+				(e_istate, e_ctxt) ptp;
 in complete_solve auto (c@c') ptp end;
 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
 if p = ([], Res) then ("end-of-calculation", [], ptp) else
 if member op = [Pbl,Met] p_
 	     if autoord auto < 6 then ("ok", c@c', ptp')
 	     else complete_solve auto (c@c') ptp'
 	   | (_, c', ptp') => complete_solve auto (c@c') ptp'
 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
 let val (_,_,mI) = get_obj g_spec pt p
-val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
+val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
-				    e_istate ptp
+				    (e_istate, e_ctxt) ptp
 in complete_solve auto (c@c') ptp end;
 (*.aux.fun for detailrls with Rrls, reverse rewriting.*)
 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
 *)
 fun rul_terms_2nds nds t [] = nds
 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
-(append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) ::
+(append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
 (rul_terms_2nds nds t' rts);
 (*. detail steps done internally by Rewrite_Set*
 into ctree by use of a script .*)
 	 | _ =>
 	   let val is = init_istate tac t
 	(*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
 				      is wrong for simpl, but working ?!? *)
 	       val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
-					 SOME t, is)
+					 SOME t, is, e_ctxt)
 	       val pos' = ((lev_on o lev_dn) p, Frm)
 	       val thy = assoc_thy "Isac"
-	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
+	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
 	       val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
 	       val newnds = children (get_nd pt'' p)
 	       val pt''' = ins_chn newnds pt p
 	   (*complete_solve cuts branches after*)
 	   in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),

branch	decompose-isar
changeset 41948	023ebb7d9759
parent 38050	4c52ad406c20
child 41953	63c956fc503e