1 (* Title: test/../appl.sml
2 Author: Walther Neuper 110320
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "-------------- fun applicable_in..Apply_Method ------------------";
10 "-----------------------------------------------------------------";
11 "-----------------------------------------------------------------";
12 "-----------------------------------------------------------------";
15 "-------------- fun applicable_in..Apply_Method ------------------";
16 "-------------- fun applicable_in..Apply_Method ------------------";
17 "-------------- fun applicable_in..Apply_Method ------------------";
18 val fmz = ["equality (x+1=(2::real))",
19 "solveFor (x::real)","solutions L"];
21 ("Test",["sqroot-test","univariate","equation","test"],
22 ["Test","squ-equ-test-subpbl1"]);
23 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32 val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt (fst p);
33 val {where_, ...} = get_pbt pI;
34 val where_ = [str2term "(lhs e_e) is_poly_in v_v"];(*just for test<>[]*)
35 val pres = map (mk_env probl |> subst_atomic) where_;
36 (*val pres = mk_env pbl |> subst_atomic #> where_;*)
37 if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
38 else error "appl.sml Apply_Method diff.behav.";
40 val ctxt = assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres;
41 (*TODO.WN110416 read pres from ctxt and check*)
43 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
46 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
47 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
48 val pIopt = get_pblID (pt,ip);
50 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
51 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
52 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
53 (*============ inhibit exn AK110726 ==============================================
54 (* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
55 val pblobj as (PblObj{meth, origin = origin as (oris,(dI', pI', mI'), _),
56 probl, spec = (dI, pI, mI), ...}) = get_obj I pt p;
57 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
58 val cpI = if pI = e_pblID then pI' else pI;
59 val cmI = if mI = e_metID then mI' else mI;
60 val {ppc, prls, where_, ...} = get_pbt cpI;
61 val pre = check_preconds "thy 100820" prls where_ probl;
62 val pb = foldl and_ (true, map fst pre);
63 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
64 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
65 ============ inhibit exn AK110726 ==============================================*)
67 (*============ inhibit exn AK110726 ==============================================
68 (* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
69 "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
70 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
71 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
72 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
73 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
74 val cpI = if pI = e_pblID then pI' else pI;
75 val ctxt = get_ctxt pt (p, Pbl);
76 oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
77 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
78 (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
79 val SOME t = parseNEW ctxt str;
80 if t = parseNEW "-1 + x = (0::real)" then ()
82 is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
83 ============ inhibit exn AK110726 ==============================================*)
84 (*-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)