1.1 --- a/src/Tools/isac/Interpret/solve.sml Fri Jul 15 13:51:50 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Jul 18 09:29:17 2011 +0200
1.3 @@ -366,18 +366,19 @@
1.4 (pos, is))], [], (pt, pos))
1.5 | _ => nxt_solv tac_ is ptp end;
1.6
1.7 -(*.says how may steps of a calculation should be done by "fun autocalc".*)
1.8 +(* says how may steps of a calculation should be done by "fun autocalc" *)
1.9 (*TODO.WN0512 redesign togehter with autocalc ?*)
1.10 datatype auto =
1.11 Step of int (*1 do #int steps; may stop in model/specify:
1.12 IS VERY INEFFICIENT IN MODEL/SPECIY*)
1.13 | CompleteModel (*2 complete modeling
1.14 - if model complete, finish specifying + start solving*)
1.15 + if model complete, finish specifying + start solving*)
1.16 | CompleteCalcHead (*3 complete model/specify in one go + start solving*)
1.17 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
1.18 - if none, complete the actual (sub)problem*)
1.19 + if none, complete the actual (sub)problem*)
1.20 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
1.21 | CompleteCalc; (*6 complete the calculation as a whole*)
1.22 +
1.23 fun autoord (Step _ ) = 1
1.24 | autoord CompleteModel = 2
1.25 | autoord CompleteCalcHead = 3
1.26 @@ -385,38 +386,6 @@
1.27 | autoord CompleteSubpbl = 5
1.28 | autoord CompleteCalc = 6;
1.29
1.30 -(* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
1.31 - *)
1.32 -fun complete_solve auto c (ptp as (_, p): ptree * pos') =
1.33 - if p = ([], Res)
1.34 - then ("end-of-calculation", [], ptp)
1.35 - else
1.36 - case nxt_solve_ ptp of
1.37 - ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.38 - if autoord auto < 5
1.39 - then ("ok", c@c', ptp)
1.40 - else
1.41 - let
1.42 - val ptp = all_modspec ptp';
1.43 - val (_, c'', ptp) = all_solve auto (c@c') ptp;
1.44 - in complete_solve auto (c@c'@c'') ptp end
1.45 - | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.46 - if autoord auto < 6 orelse p' = ([],Res)
1.47 - then ("ok", c @ c', ptp')
1.48 - else complete_solve auto (c @ c') ptp'
1.49 - | ((End_Detail, _, _)::_, c', ptp') =>
1.50 - if autoord auto < 6
1.51 - then ("ok", c @ c', ptp')
1.52 - else complete_solve auto (c @ c') ptp'
1.53 - | (_, c', ptp') => complete_solve auto (c @ c') ptp'
1.54 -
1.55 -and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') =
1.56 - let
1.57 - val (_,_,mI) = get_obj g_spec pt p;
1.58 - val ctxt = get_ctxt pt pos
1.59 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
1.60 - in complete_solve auto (c @ c') ptp end;
1.61 -
1.62 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
1.63 if p = ([], Res)
1.64 then ("end-of-calculation", [], ptp)