src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 42092 1a6d6089e594
parent 42090 908dfde7cf75
child 42281 19d9ab32a0ce
     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)