neuper@41985
|
1 |
(* Title: 300-init-subpbl.sml
|
neuper@41985
|
2 |
Author: Walther Neuper 1105
|
neuper@41985
|
3 |
(c) copyright due to lincense terms.
|
neuper@41985
|
4 |
*)
|
neuper@41985
|
5 |
|
neuper@42011
|
6 |
"----------- Minisubplb/300-init-subpbl.sml ----------------------";
|
neuper@42011
|
7 |
"----------- Minisubplb/300-init-subpbl.sml ----------------------";
|
neuper@42011
|
8 |
"----------- Minisubplb/300-init-subpbl.sml ----------------------";
|
neuper@41985
|
9 |
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
|
neuper@41985
|
10 |
val (dI',pI',mI') =
|
neuper@41985
|
11 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@41985
|
12 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41985
|
13 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41985
|
14 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
15 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
16 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
17 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
18 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
19 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
20 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
21 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
22 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@41986
|
23 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
|
neuper@41986
|
24 |
"~~~~~ fun me, args:"; val (_,tac) = nxt;
|
neuper@41986
|
25 |
"~~~~~ fun locatetac, args:"; val (tac, ptp as (pt, p)) = (tac, (pt,p));
|
neuper@41986
|
26 |
val (mI,m) = mk_tac'_ tac;
|
neuper@41986
|
27 |
val Appl m = applicable_in p pt m;
|
neuper@42092
|
28 |
member op = specsteps mI; (*false*)
|
neuper@42092
|
29 |
(*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
|
neuper@42092
|
30 |
"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
|
neuper@42092
|
31 |
(*val (msg, cs') = solve m (pt, pos);*)
|
neuper@42092
|
32 |
"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
|
neuper@42092
|
33 |
e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
|
neuper@42092
|
34 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@42092
|
35 |
val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
|
neuper@42092
|
36 |
val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
|
neuper@42092
|
37 |
(*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;*)
|
wneuper@59279
|
38 |
"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
|
neuper@48790
|
39 |
(scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
|
neuper@42092
|
40 |
((thy',srls), m, (pt,(p,p_)), (sc,d), is);
|
neuper@42092
|
41 |
val thy = assoc_thy thy';
|
neuper@42092
|
42 |
l = [] orelse ((*init.in solve..Apply_Method...*)
|
neuper@42092
|
43 |
(last_elem o fst) p = 0 andalso snd p = Res) (*false*);
|
neuper@42092
|
44 |
(*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
|
neuper@42092
|
45 |
(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
|
neuper@48790
|
46 |
"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
|
neuper@42092
|
47 |
((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
|
neuper@42092
|
48 |
1 < length l (*true*);
|
neuper@42092
|
49 |
val up = drop_last l;
|
neuper@42092
|
50 |
(*ass_up ys ((E,up,a,v,S,b),ss) (go up sc);*)
|
neuper@42092
|
51 |
"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Script.Try",_) $ e)) =
|
neuper@42092
|
52 |
(ys, ((E,up,a,v,S,b),ss), (go up sc));
|
neuper@42092
|
53 |
(* STOPPED stepping into HERE due to type problem: Can't unify _a to pos * pos_
|
neuper@42092
|
54 |
astep_up ysa iss;
|
neuper@42092
|
55 |
|
neuper@42092
|
56 |
at bottom of | assy we see:
|
neuper@42092
|
57 |
:
|
neuper@42092
|
58 |
case assod pt d m stac of
|
neuper@42092
|
59 |
"~~~~~ fun assod, args:"; val (...Subproblem'...) = ();
|
neuper@48761
|
60 |
val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
|
neuper@42092
|
61 |
|> declare_constraints' vals
|
neuper@42092
|
62 |
*)
|
neuper@41986
|
63 |
|
neuper@41985
|
64 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41986
|
65 |
case nxt of ("Model_Problem", _) => ()
|
neuper@41986
|
66 |
| _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
|
neuper@41986
|
67 |
|