1.1 --- a/src/Tools/isac/Interpret/script.sml Tue May 03 16:23:07 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 04 09:01:10 2011 +0200
1.3 @@ -428,18 +428,18 @@
1.4
1.5 (*3.12.03 copied from assod SubProblem*)
1.6 (* val Const ("Script.SubProblem",_) $
1.7 - (Const ("Pair",_) $
1.8 + (Const ("Product_Type.Pair",_) $
1.9 Free (dI',_) $
1.10 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.11 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.12 str2term
1.13 "SubProblem (EqSystem_, [linear, system], [no_met])\
1.14 \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
1.15 \ REAL_LIST [c, c_2]]";
1.16 *)
1.17 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
1.18 - (Const ("Pair",_) $
1.19 + (Const ("Product_Type.Pair",_) $
1.20 Free (dI',_) $
1.21 - (Const ("Pair",_) $ pI' $ mI')) $ ags') =
1.22 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.23 (*compare "| assod _ (Subproblem'"*)
1.24 let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.25 val thy = maxthy (assoc_thy dI) (rootthy pt);
1.26 @@ -473,24 +473,9 @@
1.27 | stac2tac_ pt thy t = error
1.28 ("stac2tac_ TODO: no match for " ^
1.29 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t));
1.30 -(*
1.31 -> val t = (term_of o the o (parse thy))
1.32 - "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";
1.33 -> stac2tac_ pt t;
1.34 -val it = Rewrite_Set_Inst ([(#,#)],"isolate_bdv") : tac
1.35 -
1.36 -> val t = (term_of o the o (parse SqRoot.thy))
1.37 -"(SubProblem (SqRoot_,[equation,univariate],(SqRoot_,solve_linear))\
1.38 - \ [BOOL e_, REAL v_])::bool list";
1.39 -> stac2tac_ pt SqRoot.thy t;
1.40 -val it = (Subproblem ("SqRoot",[#,#]),Const (#,#) $ (# $ # $ (# $ #)))
1.41 -*)
1.42
1.43 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
1.44
1.45 -
1.46 -
1.47 -
1.48 (*test a term for being a _list_ (set ?) of constants; could be more rigorous*)
1.49 fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
1.50 | list_of_consts (Const ("List.list.Nil",_)) = true
1.51 @@ -642,15 +627,15 @@
1.52
1.53 val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;
1.54 val (Const ("Script.SubProblem",_) $
1.55 - (Const ("Pair",_) $
1.56 + (Const ("Product_Type.Pair",_) $
1.57 Free (dI',_) $
1.58 - (Const ("Pair",_) $ pI' $ mI')) $ ags') = stac;
1.59 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = stac;
1.60 *)
1.61 | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,f))
1.62 (stac as Const ("Script.SubProblem",_) $
1.63 - (Const ("Pair",_) $
1.64 + (Const ("Product_Type.Pair",_) $
1.65 Free (dI',_) $
1.66 - (Const ("Pair",_) $ pI' $ mI')) $ ags') =
1.67 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.68 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.69 let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.70 val thy = maxthy (assoc_thy dI) (rootthy pt);
1.71 @@ -1765,26 +1750,26 @@
1.72 ((thy',srls), (pt,pos), sc, is);
1.73 *)
1.74 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
1.75 - (ScrState (E,l,a,v,s,b), ctxt) =
1.76 - ((*tracing("### next_tac-----------------: E= ");
1.77 - tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
1.78 - case if l=[] then appy thy ptp E [R] body NONE v
1.79 - else nstep_up thy ptp sc E l Skip_ a v of
1.80 - Skip (v,_) => (*finished*)
1.81 - (case par_pbl_det pt p of
1.82 - (true, p', _) =>
1.83 - let val (_,pblID,_) = get_obj g_spec pt p';
1.84 - in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
1.85 - (e_istate, e_ctxt), (v,s)) end
1.86 - | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
1.87 - | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef)) (*helpless*)
1.88 - | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt),
1.89 - (v, Sundef))) (*next stac*)
1.90 + (ScrState (E,l,a,v,s,b), ctxt) =
1.91 + ((*tracing("### next_tac-----------------: E= ");
1.92 + tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
1.93 + case if l = []
1.94 + then appy thy ptp E [R] body NONE v
1.95 + else nstep_up thy ptp sc E l Skip_ a v of
1.96 + Skip (v, _) => (*finished*)
1.97 + (case par_pbl_det pt p of
1.98 + (true, p', _) =>
1.99 + let val (_,pblID,_) = get_obj g_spec pt p';
1.100 + in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
1.101 + (e_istate, e_ctxt), (v,s))
1.102 + end
1.103 + | (_, p', rls') =>
1.104 + (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
1.105 + | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef))(*helpless*)
1.106 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.107 + (m', (ScrState scrst, e_ctxt), (v, Sundef))) (*next stac*)
1.108
1.109 - | next_tac _ _ _ (is, _) = error ("next_tac: not impl for "^
1.110 - (istate2str is));
1.111 -
1.112 -
1.113 + | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.114
1.115
1.116 (*.create the initial interpreter state from the items of the guard.*)