1 (* Title: 450-nxt-Check_Postcond
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
7 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
8 "----------- Minisubplb/490-nxt-Check_Postcond -------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
34 val (pt''''', p''''') = (pt, p);
36 "~~~~~ fun me, args:"; val (_,tac) = nxt;
37 val (pt, p) = case locatetac tac (pt,p) of
38 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
39 val (pt'''', p'''') = (pt, p);
40 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
41 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
44 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
45 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
46 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
47 val thy' = get_obj g_domID pt (par_pblobj pt p);
48 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
49 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
50 ;tac_; (* = Check_Postcond' *)
51 "~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
53 val pp = par_pblobj pt p
55 (case get_obj g_tac pt p of
56 Check_elementwise _ => (*collects and instantiates asms*)
57 (snd o (get_obj g_result pt)) p
58 | _ => get_assumptions_ pt (p,p_))
59 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
60 val metID = get_obj g_metID pt pp;
61 val {srls=srls,scr=sc,...} = get_met metID;
62 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
63 val thy' = get_obj g_domID pt pp;
64 val thy = assoc_thy thy';
65 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
67 val ppp = par_pblobj pt (lev_up p);
68 val thy' = get_obj g_domID pt ppp;
69 val thy = assoc_thy thy';
70 val metID = get_obj g_metID pt ppp;
71 val {scr,...} = get_met metID;
72 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
73 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
74 val tac_ = Check_Postcond' (pI, (scval, asm))
75 val is = ScrState (E,l,a,scval,scsaf,b);
76 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
77 (thy, tac_, (is, ctxt''), (pp, Res), pt);
78 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
79 (*----------------------------------------############### changed*)
81 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
82 case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
83 | _ => error "450-nxt-Check_Postcond broken"