src/sml/ME/solve.sml
author wneuper
Mon, 09 Feb 2004 19:46:32 +0100
changeset 1329 2c6a42a343c1
parent 1297 4ad32dd564e1
child 1360 a0b2c4613707
permissions -rw-r--r--
*** empty log message ***
agriesma@328
     1
(* use"../ME/solve.sml";
agriesma@328
     2
   use"ME/solve.sml";
agriesma@328
     3
   use"solve.sml";
agriesma@328
     4
   W.N.10.12.99
agriesma@328
     5
agriesma@328
     6
   cd ~/Isabelle/Zerlege-Isa98-1/src/HOL/
agriesma@328
     7
   /src/HOL> sml @SMLload=HOL-plus
agriesma@328
     8
   cd"~/MathEngine99/src/";
agriesma@328
     9
   use"ROOT.sml";
agriesma@328
    10
*)
agriesma@328
    11
agriesma@328
    12
fun safe (ScrState (_,_,_,_,s,_)) = s
agriesma@328
    13
  | safe (RrlsState _) = Safe;
agriesma@328
    14
agriesma@328
    15
type mstID = string;
wneuper@807
    16
type tac'_ = mstID * tac; (*DG <-> ME*)
wneuper@807
    17
val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;
agriesma@328
    18
wneuper@807
    19
fun mk_tac'_   m = case m of
agriesma@328
    20
  Init_Proof (ppc, spec)    => ("Init_Proof", Init_Proof (ppc, spec )) 
agriesma@328
    21
| Model_Problem pblID       => ("Model_Problem", Model_Problem pblID)
agriesma@328
    22
| Refine_Tacitly pblID      => ("Refine_Tacitly", Refine_Tacitly pblID)
agriesma@328
    23
| Refine_Problem pblID      => ("Refine_Problem", Refine_Problem pblID)
agriesma@328
    24
| Add_Given cterm'          => ("Add_Given", Add_Given cterm') 
agriesma@328
    25
| Del_Given cterm'          => ("Del_Given", Del_Given cterm') 
agriesma@328
    26
| Add_Find cterm'           => ("Add_Find", Add_Find cterm') 
agriesma@328
    27
| Del_Find cterm'           => ("Del_Find", Del_Find cterm') 
agriesma@328
    28
| Add_Relation cterm'       => ("Add_Relation", Add_Relation cterm') 
agriesma@328
    29
| Del_Relation cterm'       => ("Del_Relation", Del_Relation cterm') 
agriesma@328
    30
wneuper@839
    31
| Specify_Theory domID	    => ("Specify_Theory", Specify_Theory domID) 
agriesma@328
    32
| Specify_Problem pblID     => ("Specify_Problem", Specify_Problem pblID)
agriesma@328
    33
| Specify_Method metID	    => ("Specify_Method", Specify_Method metID) 
agriesma@328
    34
| Apply_Method metID	    => ("Apply_Method", Apply_Method metID) 
agriesma@328
    35
| Check_Postcond pblID	    => ("Check_Postcond", Check_Postcond pblID)
agriesma@328
    36
| Free_Solve                => ("Free_Solve",Free_Solve)
agriesma@328
    37
		    
agriesma@328
    38
| Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm')) 
agriesma@328
    39
| Rewrite thm'		    => ("Rewrite", Rewrite thm') 
agriesma@328
    40
| Rewrite_Asm thm'	    => ("Rewrite_Asm", Rewrite_Asm thm') 
agriesma@328
    41
| Rewrite_Set_Inst (subs, rls')
agriesma@328
    42
               => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls')) 
agriesma@328
    43
| Rewrite_Set rls'          => ("Rewrite_Set", Rewrite_Set rls') 
agriesma@328
    44
| End_Ruleset		    => ("End_Ruleset", End_Ruleset)
agriesma@328
    45
agriesma@328
    46
| End_Detail                => ("End_Detail", End_Detail)
agriesma@328
    47
| Detail_Set rls'           => ("Detail_Set", Detail_Set rls')
agriesma@328
    48
| Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls'))
agriesma@328
    49
agriesma@328
    50
| Calculate op_             => ("Calculate", Calculate op_)
agriesma@328
    51
| Substitute subs           => ("Substitute", Substitute subs) 
agriesma@328
    52
| Apply_Assumption cts'	    => ("Apply_Assumption", Apply_Assumption cts')
agriesma@328
    53
agriesma@328
    54
| Take cterm'               => ("Take", Take cterm') 
agriesma@328
    55
| Take_Inst cterm'          => ("Take_Inst", Take_Inst cterm') 
agriesma@328
    56
| Group (con, ints) 	    => ("Group", Group (con, ints)) 
agriesma@328
    57
| Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID)) 
agriesma@328
    58
(*
agriesma@328
    59
| Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts')) 
agriesma@328
    60
*)
agriesma@328
    61
| End_Subproblem            => ("End_Subproblem",End_Subproblem)
agriesma@328
    62
| CAScmd cterm'		    => ("CAScmd", CAScmd cterm')
agriesma@328
    63
			    
agriesma@328
    64
| Split_And                 => ("Split_And", Split_And) 
agriesma@328
    65
| Conclude_And		    => ("Conclude_And", Conclude_And) 
agriesma@328
    66
| Split_Or                  => ("Split_Or", Split_Or) 
agriesma@328
    67
| Conclude_Or		    => ("Conclude_Or", Conclude_Or) 
agriesma@328
    68
| Begin_Trans               => ("Begin_Trans", Begin_Trans) 
agriesma@328
    69
| End_Trans		    => ("End_Trans", End_Trans) 
agriesma@328
    70
| Begin_Sequ                => ("Begin_Sequ", Begin_Sequ) 
agriesma@328
    71
| End_Sequ                  => ("End_Sequ", Begin_Sequ) 
agriesma@328
    72
| Split_Intersect           => ("Split_Intersect", Split_Intersect) 
agriesma@328
    73
| End_Intersect		    => ("End_Intersect", End_Intersect) 
agriesma@328
    74
| Check_elementwise cterm'  => ("Check_elementwise", Check_elementwise cterm')
agriesma@328
    75
| Or_to_List                => ("Or_to_List", Or_to_List) 
agriesma@328
    76
| Collect_Trues	            => ("Collect_Results", Collect_Trues) 
agriesma@328
    77
			    
wneuper@807
    78
| Empty_Tac               => ("Empty_Tac",Empty_Tac)
wneuper@807
    79
| Tac string              => ("Tac",Tac string)
agriesma@328
    80
| User                      => ("User",User)
agriesma@328
    81
| End_Proof'                => ("End_Proof'",End_Proof'); 
agriesma@328
    82
agriesma@328
    83
(*Detail*)
wneuper@807
    84
val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;
agriesma@328
    85
wneuper@807
    86
fun mk_tac ((_,m):tac'_) = m; 
wneuper@807
    87
fun mk_mstID ((mI,_):tac'_) = mI;
agriesma@328
    88
wneuper@807
    89
fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);
wneuper@807
    90
(* TODO: tac2str, tac'_2str NOT tested *)
agriesma@328
    91
agriesma@328
    92
agriesma@328
    93
agriesma@328
    94
type squ = ptree; (* TODO: safe etc. *)
agriesma@328
    95
agriesma@328
    96
(*13.9.02--------------
agriesma@328
    97
type ctr = (loc * pos) list;
agriesma@328
    98
val ops = [("plus","op +"),("minus","op -"),("times","op *"),
agriesma@328
    99
	   ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
agriesma@328
   100
fun op_intern op_ =
agriesma@328
   101
  case assoc (ops,op_) of
agriesma@328
   102
    Some op' => op' | None => raise error ("op_intern: no op= "^op_);
agriesma@328
   103
-----------------------*)
agriesma@328
   104
agriesma@328
   105
agriesma@328
   106
agriesma@328
   107
(* use"ME/solve.sml";
agriesma@328
   108
   use"solve.sml";
agriesma@328
   109
agriesma@328
   110
val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
agriesma@328
   111
val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
agriesma@328
   112
agriesma@328
   113
  Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
agriesma@328
   114
   *)
agriesma@328
   115
agriesma@328
   116
agriesma@328
   117
agriesma@328
   118
val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem",
agriesma@328
   119
		 "Model_Problem",(*"Match_Problem",*)
agriesma@328
   120
		 "Add_Given","Del_Given","Add_Find","Del_Find",
agriesma@328
   121
		 "Add_Relation","Del_Relation",
wneuper@839
   122
		 "Specify_Theory","Specify_Problem","Specify_Method"];
agriesma@328
   123
wneuper@825
   124
"-----------------------------------------------------------------------";
agriesma@328
   125
wneuper@816
   126
(* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
wneuper@1267
   127
   val (("Apply_Method",Apply_Method' (mI,_)), pos as (p,_))=(m, pos);
agriesma@328
   128
   *)
wneuper@816
   129
fun solve ("Apply_Method",Apply_Method' (mI,_)) (pos as (p,_)) (pt:ptree) =
agriesma@328
   130
  let val {srls,...} = get_met mI;
agriesma@328
   131
    val PblObj{meth=itms,...} = get_obj I pt p;
agriesma@328
   132
    val thy' = get_obj g_domID pt p;
agriesma@328
   133
    val thy = assoc_thy thy';
agriesma@328
   134
    val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
agriesma@328
   135
    val ini = init_form thy scr env;
agriesma@328
   136
    val (p,p_) = (lev_dn p,Res);
agriesma@328
   137
  in 
agriesma@328
   138
    case ini of
agriesma@328
   139
    Some t => (* val Some t = ini; 
agriesma@328
   140
	         *)
wneuper@816
   141
    let (*val (p,p_) = (lev_on p,Frm); implicit Take -> generate1*)
agriesma@328
   142
	val f = Sign.string_of_term (sign_of (assoc_thy thy')) t;
wneuper@1250
   143
    (*val _= writeln"### solve Apply_Method: is =";
wneuper@1250
   144
        val _= writeln(istate2str is);*)
wneuper@1250
   145
	val ((p,p_),_,_,pt) = 
wneuper@816
   146
	    generate1 thy (Apply_Method' (mI,Some (t, is)))
wneuper@1267
   147
		      is (lev_on p, Frm)(*implicit Take*) pt;
wneuper@1267
   148
	val {srls,...} = get_met mI;
wneuper@1267
   149
	val (nx,is,_) = next_tac (thy',srls) (pt,(p,p_)) scr is;
wneuper@825
   150
    in ((p,p_), ((lev_onFrm o lev_dnRes) pos, is, nx), 
wneuper@825
   151
	Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), 
wneuper@825
   152
	tac_2tac nx, Safe, pt) end
agriesma@328
   153
  | None =>
wneuper@825
   154
    let val m = fst3 (next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is);
agriesma@328
   155
	val f = case m of 
wneuper@1124
   156
		    Subproblem' ((domID, pblID,_),_,_,_,_) => 
agriesma@328
   157
		    Form' (FormKF (~1,EdUndef,(length p), Nundef, 
agriesma@328
   158
			   (Sign.string_of_term (sign_of (assoc_thy thy')) 
agriesma@328
   159
						(subpbl domID pblID))))
neuper@711
   160
		  | _ => EmptyMout;
agriesma@328
   161
    (*nothing written to pt !!!*)
wneuper@825
   162
    in ((p,p_), (lev_dnRes pos, is, m), f, tac_2tac m, Safe, pt) end
agriesma@328
   163
  end
agriesma@328
   164
agriesma@328
   165
  | solve ("Free_Solve", Free_Solve') (p,_) pt =
wneuper@1250
   166
  let (*val _=writeln"###solve Free_Solve";*)
agriesma@328
   167
    val p' = lev_dn_ (p,Res);
agriesma@328
   168
    val pt = update_metID pt (par_pblobj pt p) e_metID;
wneuper@825
   169
  in (p', (p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe, pt) end
agriesma@328
   170
agriesma@328
   171
(* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
agriesma@328
   172
   *)
wneuper@825
   173
  | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pos as (p,p_)) pt =
agriesma@328
   174
    let (*val _=writeln"###solve Check_Postcond";*)
neuper@732
   175
      val pp = par_pblobj pt p
wneuper@807
   176
      val asm = (case get_obj g_tac pt p of
neuper@732
   177
		    Check_elementwise _ => (*collects and instantiates asms*)
neuper@732
   178
		    (snd o (get_obj g_result pt)) p
neuper@732
   179
		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
neuper@732
   180
	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
agriesma@328
   181
      val metID = get_obj g_metID pt pp;
agriesma@328
   182
      val {srls=srls,scr=sc,...} = get_met metID;
agriesma@328
   183
      val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); 
agriesma@328
   184
     (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
agriesma@328
   185
      val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
agriesma@328
   186
      val thy' = get_obj g_domID pt pp;
agriesma@328
   187
      val thy = assoc_thy thy';
wneuper@825
   188
      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
agriesma@328
   189
      (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
agriesma@328
   190
    in if pp = [] then 
wneuper@825
   191
	   let val is = ScrState (E,l,a,scval,scsaf,b)
wneuper@825
   192
	       val ((p,p_),ps,f,pt) = 
neuper@750
   193
		   generate1 thy (Check_Postcond'(pI,(scval,
neuper@750
   194
						      map term2str asm)))
wneuper@825
   195
			     is (pp,Res) pt;
wneuper@825
   196
	   in ((p,p_), (([],Res),is,End_Proof''), f, End_Proof', scsaf, pt) end
agriesma@328
   197
       else
agriesma@328
   198
        let
agriesma@328
   199
	  (*resume script of parpbl, transfer value of subpbl-script*)
wneuper@819
   200
        val ppp = par_pblobj pt (lev_up p);
agriesma@328
   201
	val thy' = get_obj g_domID pt ppp;
agriesma@328
   202
        val thy = assoc_thy thy';
agriesma@328
   203
	val metID = get_obj g_metID pt ppp;
agriesma@328
   204
        val sc = (#scr o get_met) metID;
agriesma@328
   205
        val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); 
agriesma@328
   206
     (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
agriesma@328
   207
  	val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is));
agriesma@328
   208
  	val _=writeln("### solve Check_postc, is'= "^
agriesma@328
   209
		      (istate2str (E,l,a,scval,scsaf,b)));*)
neuper@750
   210
        val ((p,p_),ps,f,pt) = 
neuper@750
   211
	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
agriesma@328
   212
		(ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
agriesma@328
   213
	(*val _=writeln("### solve Check_postc, is(pt')= "^
agriesma@328
   214
		      (istate2str (get_istate pt ([3],Res))));*)
wneuper@825
   215
	val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc 
wneuper@825
   216
				(ScrState (E,l,a,scval,scsaf,b));
wneuper@825
   217
       in ((p,p_), ((pp,Res),is',nx), f, tac_2tac nx, scsaf, pt) end
agriesma@328
   218
    end
agriesma@328
   219
(* writeln(istate2str(get_istate pt (p,p_)));
agriesma@328
   220
   *)
agriesma@328
   221
agriesma@328
   222
  | solve (_,End_Proof'') (p,p_) pt =
wneuper@825
   223
      ((p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt)
agriesma@328
   224
agriesma@328
   225
(*.start interpreter and do one rewrite.*)
neuper@750
   226
(* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
neuper@750
   227
   solve ("",Detail_Set'(thy', rls, t)) p pt;
agriesma@328
   228
   *)
neuper@750
   229
  | solve (_,Detail_Set'(thy', rls, t)) p pt =
agriesma@328
   230
    let (*val rls = the (assoc(!ruleset',rls'))
agriesma@328
   231
	    handle _ => raise error ("solve: '"^rls'^"' not known");*)
agriesma@328
   232
	val thy = assoc_thy thy';
agriesma@328
   233
        val (srls, sc, is) = 
agriesma@328
   234
	    case rls of
agriesma@328
   235
		Rrls {scr=sc as Rfuns {init_state=ii,...},...} => 
agriesma@328
   236
		(e_rls, sc, RrlsState (ii t))
agriesma@328
   237
	      | Rls {srls=srls,scr=sc as Script s,...} => 
agriesma@328
   238
		(srls, sc, ScrState ([(one_scr_arg s,t)], [], 
agriesma@328
   239
			       None, e_term, Sundef, true));
wneuper@807
   240
	val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
agriesma@328
   241
	val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
wneuper@825
   242
	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
agriesma@328
   243
	val aopt = applicable_in p pt nx;
agriesma@328
   244
    in case aopt of
agriesma@328
   245
	   Notappl s => raise error ("solve Detail_Set: "^s)
agriesma@328
   246
	 (* val Appl m = aopt;
agriesma@328
   247
	    *)
agriesma@328
   248
	 | Appl m => solve ("discardFIXME",m) p pt end
agriesma@328
   249
agriesma@328
   250
  | solve (_,End_Detail' t) (p,p_) pt =
agriesma@328
   251
    let val pr as (p',_) = (lev_up p, Res)
agriesma@328
   252
	val pp = par_pblobj pt p
neuper@703
   253
	val r = (fst o (get_obj g_result pt)) p' 
wneuper@825
   254
	(*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
agriesma@328
   255
	val thy' = get_obj g_domID pt pp
agriesma@328
   256
	val (srls, is, sc) = from_pblobj' thy' pr pt
wneuper@825
   257
	val (tac_,is',_) = next_tac (thy',srls)  (pt,pr) sc is
wneuper@825
   258
    in (pr, ((pp,Frm(*???*)),is,tac_), 
wneuper@825
   259
	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
wneuper@825
   260
	tac_2tac tac_, Sundef, pt)end
agriesma@328
   261
(* val (mI,(p,p_)) = ("xxx",p);
agriesma@328
   262
   *)
agriesma@328
   263
  | solve (mI,m) (p,p_) pt =
wneuper@856
   264
(* val ((mI,m), (p,p_)) = (m, pos);
wneuper@856
   265
   *)
agriesma@328
   266
    if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
agriesma@328
   267
						      could be detail, too !!*)
agriesma@328
   268
    then let val ((p,p_),ps,f,pt) = 
agriesma@328
   269
		 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
agriesma@328
   270
			   m e_istate (p,p_) pt;
wneuper@825
   271
	 in ((p,p_),((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end
agriesma@328
   272
    else
neuper@711
   273
	let 
neuper@711
   274
	    val thy' = get_obj g_domID pt (par_pblobj pt p);
agriesma@328
   275
	    val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
agriesma@328
   276
(*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
agriesma@328
   277
		val d = e_rls; (*FIXME: canon.simplifier for domain is missing
agriesma@328
   278
				8.01: generate from domID?*)
agriesma@328
   279
	in case locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is of 
agriesma@328
   280
	       Steps (is', (m',f',pt',p',c')::ss) =>
wneuper@856
   281
(* val Steps (is', (m',f',pt',p',c')::ss) =
wneuper@856
   282
       locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
wneuper@856
   283
 *)
wneuper@1250
   284
	       let (**)val _= writeln("### solve, after locate_gen: is= ")
wneuper@1250
   285
		       val _= writeln(istate2str is')(**)
wneuper@1250
   286
		   val nxt_ = 
wneuper@807
   287
		       case p' of (*change from solve to model subprobl#####*)
wneuper@825
   288
			   (_,Pbl) => nxt_model_pbl m' (pt',p')
wneuper@825
   289
			 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is'); 
wneuper@825
   290
	       (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
wneuper@825
   291
	       in (p',(p',is',nxt_), f', tac_2tac nxt_, safe is', pt'(*'*)) end
agriesma@328
   292
	     | NotLocatable =>  
agriesma@328
   293
	       let val (p,ps,f,pt) = 
agriesma@328
   294
		       generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
wneuper@825
   295
	       in (p,(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end
agriesma@328
   296
	end;
agriesma@328
   297
wneuper@1297
   298
(* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
wneuper@1250
   299
fun nxt_solv (Apply_Method' (mI,_)) _ (pt:ptree, pos as (p,_)) =
wneuper@1297
   300
(* val (mI, (pt:ptree, pos as (p,_))) = (mI, ptp);
wneuper@1297
   301
   *)
wneuper@1297
   302
  let val {srls,ppc,...} = get_met mI;
wneuper@1297
   303
    val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
wneuper@1297
   304
    val itms = if itms <> [] then itms
wneuper@1297
   305
	       else complete_metitms oris probl [] ppc
wneuper@839
   306
    val thy' = get_obj g_domID pt p;
wneuper@839
   307
    val thy = assoc_thy thy';
wneuper@839
   308
    val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
wneuper@839
   309
    val ini = init_form thy scr env;
wneuper@839
   310
    val (p,p_) = (lev_dn p,Res);
wneuper@839
   311
  in 
wneuper@839
   312
    case ini of
wneuper@839
   313
    Some t => (* val Some t = ini; 
wneuper@839
   314
	         *)
wneuper@839
   315
    let (*val (p,p_) = (lev_on p,Frm); implicit Take -> generate1*)
wneuper@839
   316
	val f = Sign.string_of_term (sign_of (assoc_thy thy')) t;
wneuper@1250
   317
    (*val _= writeln"### nxt_solv1 Apply_Method: store is =";
wneuper@1250
   318
        val _= writeln(istate2str is);*)
wneuper@856
   319
        val tac_ = Apply_Method' (mI, Some (t, is));
wneuper@839
   320
	val ((p,p_),_,_,pt) = (*implicit Take*)
wneuper@856
   321
	    generate1 thy tac_ is(*Uistate.19.8.03*) (lev_on p,Frm) pt
wneuper@1250
   322
    in ([(Apply_Method mI, tac_, ((lev_on p,Frm), is))], 
wneuper@1250
   323
	(pt, (p,p_))):calcstate'
wneuper@856
   324
    (*(p,p_), ((lev_onFrm o lev_dnRes) pos, is, nx), 
wneuper@856
   325
    Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), 
wneuper@856
   326
    tac_2tac nx, Safe, pt*) end
wneuper@839
   327
  | None =>
wneuper@839
   328
    (*nothing written to pt !!!*)
wneuper@1250
   329
    ([(Apply_Method mI, Apply_Method' (mI, None), ((lev_on p,Frm), is))],
wneuper@1250
   330
     (pt, (lev_dnRes pos)))
wneuper@839
   331
  end
wneuper@839
   332
wneuper@839
   333
(* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
wneuper@839
   334
   *)
wneuper@1250
   335
  | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_))  =
wneuper@839
   336
    let (*val _=writeln"###solve Check_Postcond";*)
wneuper@839
   337
      val pp = par_pblobj pt p
wneuper@839
   338
      val asm = (case get_obj g_tac pt p of
wneuper@839
   339
		    Check_elementwise _ => (*collects and instantiates asms*)
wneuper@839
   340
		    (snd o (get_obj g_result pt)) p
wneuper@839
   341
		  | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
wneuper@839
   342
	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
wneuper@839
   343
      val metID = get_obj g_metID pt pp;
wneuper@839
   344
      val {srls=srls,scr=sc,...} = get_met metID;
wneuper@839
   345
      val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); 
wneuper@839
   346
     (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
wneuper@839
   347
      val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
wneuper@839
   348
      val thy' = get_obj g_domID pt pp;
wneuper@839
   349
      val thy = assoc_thy thy';
wneuper@839
   350
      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
wneuper@839
   351
      (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
wneuper@839
   352
    in if pp = [] then 
wneuper@839
   353
	   let val is = ScrState (E,l,a,scval,scsaf,b)
wneuper@1250
   354
	       val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
wneuper@1250
   355
           (*val _= writeln"### nxt_solv2 Apply_Method: stored is =";
wneuper@1250
   356
               val _= writeln(istate2str is);*)
wneuper@839
   357
	       val ((p,p_),ps,f,pt) = 
wneuper@1250
   358
		   generate1 thy tac_ is (pp,Res) pt;
wneuper@1250
   359
	   in ([(Check_Postcond pI, tac_, ((pp,Res), is))], (pt, (p,p_))) end
wneuper@839
   360
       else
wneuper@839
   361
        let
wneuper@839
   362
	  (*resume script of parpbl, transfer value of subpbl-script*)
wneuper@839
   363
        val ppp = par_pblobj pt (lev_up p);
wneuper@839
   364
	val thy' = get_obj g_domID pt ppp;
wneuper@839
   365
        val thy = assoc_thy thy';
wneuper@839
   366
	val metID = get_obj g_metID pt ppp;
wneuper@839
   367
        val sc = (#scr o get_met) metID;
wneuper@1250
   368
        val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
wneuper@1250
   369
        val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
wneuper@1250
   370
	val is = ScrState (E,l,a,scval,scsaf,b)
wneuper@1250
   371
    (*val _= writeln"### nxt_solv3 Apply_Method: stored is =";
wneuper@1250
   372
        val _= writeln(istate2str is);*)
wneuper@1250
   373
        val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
wneuper@1250
   374
	val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc is;
wneuper@1250
   375
       in ([(Check_Postcond pI, tac_, ((pp, Res), is))], (pt, (p,p_))) end
wneuper@839
   376
    end
wneuper@839
   377
(* writeln(istate2str(get_istate pt (p,p_)));
wneuper@839
   378
   *)
wneuper@839
   379
wneuper@839
   380
(*.start interpreter and do one rewrite.*)
wneuper@839
   381
(* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
wneuper@839
   382
   solve ("",Detail_Set'(thy', rls, t)) p pt;
wneuper@1250
   383
  | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********
wneuper@856
   384
---> FE-interface/sml.sml
wneuper@839
   385
wneuper@1250
   386
  | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = **********
wneuper@839
   387
    let val pr as (p',_) = (lev_up p, Res)
wneuper@839
   388
	val pp = par_pblobj pt p
wneuper@839
   389
	val r = (fst o (get_obj g_result pt)) p' 
wneuper@839
   390
	(*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
wneuper@839
   391
	val thy' = get_obj g_domID pt pp
wneuper@839
   392
	val (srls, is, sc) = from_pblobj' thy' pr pt
wneuper@839
   393
	val (tac_,is',_) = next_tac (thy',srls)  (pt,pr) sc is
wneuper@839
   394
    in (pr, ((pp,Frm(*???*)),is,tac_), 
wneuper@839
   395
	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
wneuper@856
   396
	tac_2tac tac_, Sundef, pt) end
wneuper@856
   397
*)
wneuper@1329
   398
  | nxt_solv (End_Proof'') _ ptp = ([], ptp)
wneuper@1329
   399
wneuper@1329
   400
  | nxt_solv tac_ is (pt, pos as (p,p_)) =
wneuper@1329
   401
    let val pos = case pos of (p,Res) => (lev_on p,Res) | _ => pos
wneuper@1329
   402
    (*val _= writeln"### nxt_solv4 Apply_Method: stored is =";
wneuper@1329
   403
        val _= writeln(istate2str is);*)
wneuper@1329
   404
	val (pos',_,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
wneuper@1329
   405
    in ([(tac_2tac tac_, tac_, (pos,is))], (pt, pos')) end;
wneuper@1329
   406
wneuper@1329
   407
wneuper@1329
   408
  (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
wneuper@1329
   409
wneuper@856
   410
wneuper@1250
   411
(*.find the next tac from the script, nxt_solv will update the ptree.*)
wneuper@1250
   412
fun nxt_solve_ (ptp as (pt, pos as (p,p_))) =
wneuper@1250
   413
(* val (pt,pos as (p,p_)) = ptp;
wneuper@1329
   414
   val (pt,pos as (p,p_)) = ptp''';
wneuper@1250
   415
   *)
wneuper@1250
   416
    if e_metID = get_obj g_metID pt (par_pblobj pt p)
wneuper@1250
   417
    then ([], (pt,(p,p_))):calcstate'
wneuper@1250
   418
    else let val thy' = get_obj g_domID pt (par_pblobj pt p);
wneuper@1250
   419
	     val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
wneuper@1329
   420
	     val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
wneuper@1250
   421
	 (*here ^^^  return finished/helpless/ok !*)
wneuper@1250
   422
	 (* val (tac_',is',_) = next_tac (thy',srls) (pt,pos) sc is;
wneuper@1250
   423
            val Subproblem' (_,ooos,_,_,_) = tac_';
wneuper@1250
   424
            writeln (oris2str ooos);
wneuper@1250
   425
	    *)
wneuper@1329
   426
	 in case tac_ of
wneuper@1329
   427
		End_Detail' _ => ([(End_Detail, End_Detail' t, 
wneuper@1329
   428
				    (pos, is))], (pt, pos))
wneuper@1329
   429
	      | _ => nxt_solv tac_ is ptp end;
wneuper@856
   430
wneuper@1267
   431
datatype auto = 
wneuper@1297
   432
  Step of int      (*1 do #int steps; may stop in model/specify:
wneuper@1267
   433
		     IS VERY INEFFICIENT IN MODEL/SPECIY*)
wneuper@1267
   434
| CompleteModel    (*2 complete modeling
wneuper@1267
   435
                     if model complete, finish specifying + start solving*)
wneuper@1267
   436
| CompleteCalcHead (*3 complete model/specify in one go + start solving*)
wneuper@1267
   437
| CompleteToSubpbl (*4 stop at the next begin of a subproblem,
wneuper@1267
   438
                     if none, complete the actual (sub)problem*)
wneuper@1267
   439
| CompleteSubpbl   (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
wneuper@1267
   440
| CompleteCalc;    (*6 complete the calculation as a whole*)	
wneuper@1267
   441
fun autoord (Step _ ) = 1
wneuper@1267
   442
  | autoord CompleteModel = 2
wneuper@1267
   443
  | autoord CompleteCalcHead = 3
wneuper@1267
   444
  | autoord CompleteToSubpbl = 4
wneuper@1267
   445
  | autoord CompleteSubpbl = 5
wneuper@1267
   446
  | autoord CompleteCalc = 6;
wneuper@1329
   447
(* val ptp as (_, p) = ptp;
wneuper@1329
   448
wneuper@1329
   449
   val ptp as (_, p) = (pt, pos); val auto = CompleteSubpbl;
wneuper@1329
   450
   *)
wneuper@1267
   451
fun complete_solve auto (ptp as (_, p): ptree * pos') =
wneuper@1267
   452
    if p = ([], Res) then ("end-of-calculation", ptp) else
wneuper@1250
   453
    case nxt_solve_ ptp of
wneuper@1250
   454
	((Subproblem _, tac_, (_, is))::_, ptp') =>
wneuper@1250
   455
(* val ptp' = ptp''';
wneuper@1250
   456
   *)
wneuper@1267
   457
	if autoord auto < 5 then ("ok", ptp)
wneuper@1250
   458
	else let val ptp = all_modspec ptp';
wneuper@1267
   459
	         val (_, ptp) = all_solve auto ptp;
wneuper@1267
   460
	     in complete_solve auto ptp end
wneuper@1250
   461
      | ((Check_Postcond _, tac_, (_, is))::_, ptp' as (_, p')) =>
wneuper@1267
   462
	if autoord auto < 6 orelse p' = ([],Res) then ("ok", ptp')
wneuper@1267
   463
	else complete_solve auto ptp'
wneuper@1329
   464
      | ((End_Detail, _, _)::_, ptp') => if autoord auto < 6 then ("ok", ptp')
wneuper@1329
   465
					 else complete_solve auto ptp'
wneuper@1267
   466
      | (_, ptp') => complete_solve auto ptp'
wneuper@1250
   467
(* val (tacis, ptp') = nxt_solve_ ptp;
wneuper@1250
   468
   val (tacis, ptp'') = nxt_solve_ ptp';
wneuper@1250
   469
   val (tacis, ptp''') = nxt_solve_ ptp'';
wneuper@1329
   470
   val (tacis, ptp'''') = nxt_solve_ ptp''';
wneuper@1329
   471
   val (tacis, ptp''''') = nxt_solve_ ptp'''';
wneuper@1250
   472
   *)
wneuper@1267
   473
and all_solve auto (ptp as (pt, (p,_)): ptree * pos') = 
wneuper@1250
   474
(* val (ptp as (pt, (p,_))) = ptp;
wneuper@1250
   475
   val (ptp as (pt, (p,_))) = ptp';
wneuper@1297
   476
   val (ptp as (pt, (p,_))) = (pt, pos);
wneuper@1250
   477
   *)
wneuper@1250
   478
    let val (_,_,mI) = get_obj g_spec pt p;
wneuper@1329
   479
        val (_, ptp) = nxt_solv (Apply_Method' (mI, None)) (*FIXXXME.0401 is!*)
wneuper@1329
   480
				e_istate ptp;
wneuper@1267
   481
    in complete_solve auto ptp end;
wneuper@839
   482
agriesma@328
   483
wneuper@1329
   484
(*. detail steps done internally by Rewrite_Set* 
wneuper@1329
   485
  by use of a script into ctree .*)
wneuper@1329
   486
(* val (p,p_) = pos;
wneuper@1329
   487
   *)
wneuper@1329
   488
fun detailrls pt (p,p_) = 
wneuper@1329
   489
    let val t = get_obj g_form pt p
wneuper@1329
   490
	val is = case get_obj g_tac pt p of
wneuper@1329
   491
(* val Rewrite_Set rls = get_obj g_tac pt p;
wneuper@1329
   492
   *)
wneuper@1329
   493
		     Rewrite_Set rls =>
wneuper@1329
   494
		     (case assoc_rls rls of
wneuper@1329
   495
			  Rrls {scr=sc as Rfuns {init_state=ii,...},...} => 
wneuper@1329
   496
			  (RrlsState (ii t))
wneuper@1329
   497
			| Rls {scr=Script s,...} =>
wneuper@1329
   498
(* val Rls {scr=Script s,...} = assoc_rls rls;
wneuper@1329
   499
   *)
wneuper@1329
   500
			  (ScrState ([(one_scr_arg s, t)], [], 
wneuper@1329
   501
				     None, e_term, Sundef, true))
wneuper@1329
   502
			| Seq {srls=srls,scr=Script s,...} =>
wneuper@1329
   503
			  (ScrState ([(one_scr_arg s, t)], [], 
wneuper@1329
   504
				     None, e_term, Sundef, true)))
wneuper@1329
   505
		   | Rewrite_Set_Inst (subs, rls) =>
wneuper@1329
   506
		     let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
wneuper@1329
   507
		     in case assoc_rls rls of
wneuper@1329
   508
			    Rls {scr=Script s,...} =>
wneuper@1329
   509
			    let val (a1, a2) = two_scr_arg s
wneuper@1329
   510
			    in (ScrState ([(a1, v), (a2, t)], [], 
wneuper@1329
   511
					  None, e_term, Sundef, true)) end
wneuper@1329
   512
			  | Seq {scr=Script s,...} =>
wneuper@1329
   513
			    let val (a1, a2) = two_scr_arg s
wneuper@1329
   514
			    in (ScrState ([(a1, v), (a2, t)], [], 
wneuper@1329
   515
				     None, e_term, Sundef, true)) end
wneuper@1329
   516
		     end
wneuper@1329
   517
	val tac_ = Apply_Method' (e_metID(*WN.0402: see generate1 !?!*), 
wneuper@1329
   518
				  Some (t, is));
wneuper@1329
   519
	val pos = ((lev_on o lev_dn) p, Frm);
wneuper@1329
   520
	val (_,_,_,pt) = (*implicit Take*) generate1 thy tac_ is pos pt;
wneuper@1329
   521
	val (_, (pt,_)) = complete_solve CompleteSubpbl (pt, pos);
wneuper@1329
   522
(* val (_, (pt',_)) = complete_solve CompleteSubpbl (pt, pos);
wneuper@1329
   523
   val nd' = get_nd pt' p;
wneuper@1329
   524
   val cn' = children nd';   
wneuper@1329
   525
   *)
wneuper@1329
   526
	val nd = get_nd pt p;
wneuper@1329
   527
	val cn = children nd;
wneuper@1329
   528
in ("detailrls", pt, get_formress [] ((lev_on o lev_dn) p) cn) end;
wneuper@1329
   529
(*
wneuper@1329
   530
 val (_, (pt',_)) = complete_solve CompleteSubpbl (pt, pos);
wneuper@1329
   531
wneuper@1329
   532
*)
wneuper@1329
   533
wneuper@1329
   534
wneuper@1329
   535
wneuper@1329
   536
agriesma@328
   537
(* val (pos' as (p,p_),pt) = (p,EmptyPtree);
agriesma@328
   538
   
agriesma@328
   539
   val (mI,m) = nxt; val pos' as (p,p_) = p;
agriesma@328
   540
   *)
wneuper@825
   541
fun meOLD ((mI,m):tac'_) (pos' as (p,p_):pos') (c:cid) (pt:ptree) =
agriesma@328
   542
  case applicable_in (p,p_) pt m of
neuper@718
   543
    Appl m => (* val Appl m''' = applicable_in (p,p_) pt m;
neuper@718
   544
                 val Appl m = applicable_in (p,p_) pt m;
neuper@750
   545
	       *)
agriesma@328
   546
    (case m of
wneuper@1050
   547
	( Refine_Problem' (ms as (pI,_))) => 
wneuper@825
   548
	 (pos',[], Problems (RefinedKF ms), 
wneuper@1050
   549
	  ("Specify_Problem", Specify_Problem pI), Safe, pt)
agriesma@328
   550
agriesma@328
   551
       | _ => (if mI mem specsteps
wneuper@825
   552
	       then let val (p',c,f,m,s,pt) = specify m (p,p_) [] pt;
wneuper@825
   553
		   in (p',[],f,mk_tac'_ m,s,pt)
agriesma@328
   554
		    end
agriesma@328
   555
	       else let val ((p,p_),c,f,m,s,pt) = solve (mI,m) (p,p_) pt;
wneuper@825
   556
		   in ((p,p_),[],f,mk_tac'_ m,s,pt) end))
wneuper@825
   557
  | Notappl e => ((p,p_),[], Error' (Error_ e),
wneuper@807
   558
		  mk_tac'_ Empty_Tac (*nxtstep ??*), Unsafe,pt);
agriesma@328
   559
wneuper@825
   560
val me = meOLD;
wneuper@825
   561
agriesma@328
   562
(* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);
wneuper@807
   563
   get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
agriesma@328
   564
   *)
wneuper@807
   565
fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = 
agriesma@328
   566
  case applicable_in (p,p_) pt m of
agriesma@328
   567
    Notappl e => Error' (Error_ e)
agriesma@328
   568
  | Appl m => 
agriesma@328
   569
      (* val Appl m=applicable_in (p,p_) pt m;
agriesma@328
   570
         *)
agriesma@328
   571
      if mI mem specsteps
agriesma@328
   572
	then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
agriesma@328
   573
	     in f end
agriesma@328
   574
      else let val (_,_,f,_,_,_) = solve (mI,m) (p,p_) pt
agriesma@328
   575
	   in f end;
wneuper@825
   576