6 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
6 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
7 val (dI',pI',mI') = |
7 val (dI',pI',mI') = |
8 ("Test", ["sqroot-test","univariate","equation","test"], |
8 ("Test", ["sqroot-test","univariate","equation","test"], |
9 ["Test","squ-equ-test-subpbl1"]); |
9 ["Test","squ-equ-test-subpbl1"]); |
10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*) |
10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*) |
|
11 (*for resuming after stepping into code*) |
|
12 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt); |
|
13 |
|
14 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ptree)) = (nxt, p, [], pt); |
|
15 val (pt, p) = |
|
16 case locatetac tac (pt,p) of |
|
17 ("ok", (_, _, ptp)) => ptp; |
|
18 (* val (_, ts) = |
|
19 (case step p ((pt, e_pos'),[]) of |
|
20 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)) |
|
21 ERROR: ts = [(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'", ...*) |
|
22 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
|
23 (p, ((pt, e_pos'),[])); |
|
24 val pIopt = get_pblID (pt,ip); |
|
25 ip = ([],Res); (* = false*) |
|
26 tacis; (* = []*) |
|
27 pIopt; (* = SOME ["sqroot-test", "univariate", "equation", "test"]*) |
|
28 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = true*) |
|
29 |
|
30 (* nxt_specify_ (pt, ip) |
|
31 ERROR: = ([(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'",...*) |
|
32 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip); |
|
33 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), |
|
34 probl,spec=(dI,pI,mI), ...}) = get_obj I pt p; |
|
35 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*) |
|
36 val cpI = if pI = e_pblID then pI' else pI; |
|
37 val cmI = if mI = e_metID then mI' else mI; |
|
38 val {ppc, prls, where_, ...} = get_pbt cpI; |
|
39 val pre = check_preconds "thy 100820" prls where_ probl; |
|
40 val pb = foldl and_ (true, map fst pre); |
|
41 |
|
42 (* val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) |
|
43 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); |
|
44 ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*) |
|
45 "~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : spec), |
|
46 ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : spec)) = |
|
47 (p_, pb, oris, (dI',pI',mI'), (probl, meth), |
|
48 (ppc, (#ppc o get_met) cmI), (dI, pI, mI)); |
|
49 |
|
50 dI' = e_domID andalso dI = e_domID; (* = false*) |
|
51 pI' = e_pblID andalso pI = e_pblID; (* = false*) |
|
52 find_first (is_error o #5) (pbl:itm list); (* = NONE*) |
|
53 |
|
54 (* nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl; |
|
55 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *) |
|
56 "~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) = |
|
57 ((assoc_thy (if dI = e_domID then dI' else dI)), oris, pbt, pbl); |
|
58 local infix mem; |
|
59 fun x mem [] = false |
|
60 | x mem (y :: ys) = x = y orelse x mem ys; |
|
61 in |
|
62 fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori)) |
|
63 andalso (#3 ori) <>"#undef"; |
|
64 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm)); |
|
65 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids; |
|
66 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = |
|
67 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts); |
|
68 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false |
|
69 | false_and_not_Sup (i,v,false,f, _) = true |
|
70 | false_and_not_Sup _ = false; |
|
71 end |
|
72 val v = if itms = [] then 1 else max_vt itms; |
|
73 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*) |
|
74 val vits = if v = 0 then itms (*because of dsc without dat*) |
|
75 else filter (testi_vt v) itms; (*itms..vat*) |
|
76 val icl = filter false_and_not_Sup vits; (* incomplete *) |
|
77 icl = []; (* = false*) |
|
78 val SOME ori = find_first (test_subset (hd icl)) vors; |
|
79 |
|
80 (* SOME (geti_ct thy ori (hd icl)) |
|
81 ERROR: SOME (geti_ct thy ori (hd icl))*) |
|
82 "~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) = |
|
83 (thy, ori, (hd icl)); |
|
84 "~~~~~ to return val:"; val xxx = |
|
85 ( fd, |
|
86 ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm' |
|
87 ); |
|
88 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error ""; |
|
89 |
|
90 (* resuming after stepping into code*) |
|
91 val (p,f,nxt,pt) = (p''',f''',nxt''',pt'''); |
|
92 |
11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*) |
93 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*) |
12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*) |
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*) |
13 case nxt of (_, Add_Given "solveFor x") => () |
95 case nxt of (_, Add_Given "solveFor x") => () |
14 | _ => error "minisubpbl: Add_Given is broken in root-problem"; |
96 | _ => error "minisubpbl: Add_Given is broken in root-problem"; |
15 |
|