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", ...]*)
42 (*if*) tacis; (*= []*)
44 (*if*) member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
46 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
47 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
48 val thy' = get_obj g_domID pt (par_pblobj pt p);
49 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
50 val (tac_,is, (t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
52 (*+*);tac_; (* = Check_Postcond' *)
54 "~~~~~ fun begin_end_prog, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
56 val pp = par_pblobj pt p
57 val asm = (case get_obj g_tac pt p of
58 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
59 | _ => get_assumptions_ pt (p, p_))
60 val metID = get_obj g_metID pt pp;
61 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
62 val (loc, pst, ctxt) = case get_loc pt (p, p_) of
63 loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
64 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
65 val thy' = get_obj g_domID pt pp;
66 val thy = Celem.assoc_thy thy';
67 val (_, _, (scval, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
69 (*if*) pp = []; (*false*)
71 val ppp = par_pblobj pt (lev_up p);
72 val thy' = get_obj g_domID pt ppp;
73 val thy = Celem.assoc_thy thy';
75 val (pst', ctxt') = case get_loc pt (pp, Frm) of
76 (Istate.Pstate pst', ctxt') => (pst', ctxt')
77 | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
78 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
79 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
80 val is = Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
82 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
83 (thy, tac_, (is, ctxt''), (pp, Res), pt);
84 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
85 (*----------------------------------------############### changed*)
87 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", ...]) *);
88 case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
89 | _ => error "450-nxt-Check_Postcond broken"