neuper@41943
|
1 |
(* Title: test/../appl.sml
|
neuper@41943
|
2 |
Author: Walther Neuper 110320
|
neuper@41943
|
3 |
(c) copyright due to lincense terms.
|
neuper@41943
|
4 |
*)
|
neuper@41958
|
5 |
|
neuper@41958
|
6 |
"-----------------------------------------------------------------";
|
neuper@41958
|
7 |
"table of contents -----------------------------------------------";
|
neuper@41958
|
8 |
"-----------------------------------------------------------------";
|
neuper@41958
|
9 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
wneuper@59285
|
10 |
"-------------- fun mk_set ---------------------------------------";
|
wneuper@59285
|
11 |
"-------------- fun check_elementwise ----------------------------";
|
wneuper@59285
|
12 |
"-------------- fun split_dummy ----------------------------------";
|
neuper@41958
|
13 |
"-----------------------------------------------------------------";
|
neuper@41958
|
14 |
"-----------------------------------------------------------------";
|
neuper@41958
|
15 |
"-----------------------------------------------------------------";
|
neuper@41958
|
16 |
|
neuper@41958
|
17 |
|
neuper@41958
|
18 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
neuper@41958
|
19 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
neuper@41958
|
20 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
neuper@41958
|
21 |
val fmz = ["equality (x+1=(2::real))",
|
neuper@41958
|
22 |
"solveFor (x::real)","solutions L"];
|
neuper@41958
|
23 |
val (dI',pI',mI') =
|
neuper@41958
|
24 |
("Test",["sqroot-test","univariate","equation","test"],
|
neuper@41958
|
25 |
["Test","squ-equ-test-subpbl1"]);
|
neuper@41958
|
26 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@41958
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
30 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
32 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
33 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
34 |
|
neuper@41958
|
35 |
val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt (fst p);
|
neuper@41958
|
36 |
val {where_, ...} = get_pbt pI;
|
neuper@41958
|
37 |
val where_ = [str2term "(lhs e_e) is_poly_in v_v"];(*just for test<>[]*)
|
neuper@41958
|
38 |
val pres = map (mk_env probl |> subst_atomic) where_;
|
neuper@41958
|
39 |
(*val pres = mk_env pbl |> subst_atomic #> where_;*)
|
neuper@41958
|
40 |
if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
|
neuper@41958
|
41 |
else error "appl.sml Apply_Method diff.behav.";
|
neuper@41958
|
42 |
|
walther@59728
|
43 |
val ctxt = assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres;
|
neuper@41958
|
44 |
(*TODO.WN110416 read pres from ctxt and check*)
|
neuper@41958
|
45 |
|
neuper@41958
|
46 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@41958
|
47 |
show_pt pt;
|
neuper@41975
|
48 |
|
akargl@42202
|
49 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
walther@59765
|
50 |
"~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
|
neuper@41975
|
51 |
val pIopt = get_pblID (pt,ip);
|
neuper@41975
|
52 |
tacis; (*= []*)
|
neuper@41975
|
53 |
pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
|
walther@59839
|
54 |
member op = [Pbl,Met] p_; (*= true*)
|
neuper@41975
|
55 |
"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
|
akargl@42202
|
56 |
(*============ inhibit exn AK110726 ==============================================
|
akargl@42202
|
57 |
(* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
|
akargl@42202
|
58 |
val pblobj as (PblObj{meth, origin = origin as (oris,(dI', pI', mI'), _),
|
akargl@42202
|
59 |
probl, spec = (dI, pI, mI), ...}) = get_obj I pt p;
|
neuper@41975
|
60 |
just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
|
neuper@41975
|
61 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@41975
|
62 |
val cmI = if mI = e_metID then mI' else mI;
|
neuper@41975
|
63 |
val {ppc, prls, where_, ...} = get_pbt cpI;
|
neuper@41975
|
64 |
val pre = check_preconds "thy 100820" prls where_ probl;
|
neuper@41975
|
65 |
val pb = foldl and_ (true, map fst pre);
|
neuper@41975
|
66 |
val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
|
neuper@41975
|
67 |
(ppc, (#ppc o get_met) cmI) (dI, pI, mI);
|
akargl@42202
|
68 |
============ inhibit exn AK110726 ==============================================*)
|
akargl@42202
|
69 |
|
akargl@42202
|
70 |
(*============ inhibit exn AK110726 ==============================================
|
akargl@42202
|
71 |
(* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
|
walther@59806
|
72 |
"~~~~~ fun Step_Specify.by_tactic_input, args:"; val (Add_Given ct, ptp) = (tac, ptp);
|
neuper@41975
|
73 |
"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
|
neuper@41975
|
74 |
val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
|
neuper@41975
|
75 |
probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
|
walther@59879
|
76 |
val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
|
neuper@41975
|
77 |
val cpI = if pI = e_pblID then pI' else pI;
|
neuper@41975
|
78 |
val ctxt = get_ctxt pt (p, Pbl);
|
wneuper@59595
|
79 |
oris; (*= [(1, [1], "#Given", Const ("Input_Descript.equality", "HOL.bool...*)
|
neuper@41975
|
80 |
"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
|
neuper@41975
|
81 |
(ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
|
neuper@41975
|
82 |
val SOME t = parseNEW ctxt str;
|
neuper@41975
|
83 |
if t = parseNEW "-1 + x = (0::real)" then ()
|
neuper@41975
|
84 |
else error "TODO"
|
neuper@41975
|
85 |
is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
|
akargl@42202
|
86 |
============ inhibit exn AK110726 ==============================================*)
|
akargl@42202
|
87 |
(*-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
wneuper@59285
|
88 |
|
wneuper@59285
|
89 |
"-------------- fun mk_set ---------------------------------------";
|
wneuper@59285
|
90 |
"-------------- fun mk_set ---------------------------------------";
|
wneuper@59285
|
91 |
"-------------- fun mk_set ---------------------------------------";
|
wneuper@59285
|
92 |
(*> val consts = str2term "[x=#4]";
|
wneuper@59285
|
93 |
> val pred = str2term "Assumptions";
|
wneuper@59285
|
94 |
> val pt = union_asm pt p
|
wneuper@59285
|
95 |
[("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
|
wneuper@59285
|
96 |
("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
|
wneuper@59285
|
97 |
> val p = [];
|
wneuper@59285
|
98 |
> val (sss,ttt) = mk_set thy pt p consts pred;
|
walther@59868
|
99 |
> (UnparseC.term sss, UnparseC.term ttt);
|
wneuper@59285
|
100 |
val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
|
wneuper@59285
|
101 |
|
walther@59620
|
102 |
val consts = str2term "TermC.UniversalList";
|
wneuper@59285
|
103 |
val pred = str2term "Assumptions";
|
wneuper@59285
|
104 |
*)
|
wneuper@59285
|
105 |
|
wneuper@59285
|
106 |
"-------------- fun check_elementwise ----------------------------";
|
wneuper@59285
|
107 |
"-------------- fun check_elementwise ----------------------------";
|
wneuper@59285
|
108 |
"-------------- fun check_elementwise ----------------------------";
|
wneuper@59285
|
109 |
(* 20.5.03
|
wneuper@59285
|
110 |
> val all_results = str2term "[x=a+b,x=b,x=3]";
|
wneuper@59285
|
111 |
> val bdv = str2term "x";
|
wneuper@59285
|
112 |
> val asm = str2term "(x ~= a) & (x ~= b)";
|
walther@59852
|
113 |
> val erls = Rule_Set.empty;
|
wneuper@59285
|
114 |
> val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
|
walther@59868
|
115 |
> UnparseC.term t; tracing(UnparseC.terms ts);
|
wneuper@59285
|
116 |
val it = "[x = a + b, x = b, x = c]" : string
|
wneuper@59285
|
117 |
["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
|
wneuper@59285
|
118 |
... with appropriate erls this should be:
|
wneuper@59285
|
119 |
val it = "[x = a + b, x = c]" : string
|
wneuper@59285
|
120 |
["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
|
wneuper@59285
|
121 |
////// because b ~= b False*)
|
wneuper@59285
|
122 |
|
wneuper@59285
|
123 |
"-------------- fun split_dummy ----------------------------------";
|
wneuper@59285
|
124 |
"-------------- fun split_dummy ----------------------------------";
|
wneuper@59285
|
125 |
"-------------- fun split_dummy ----------------------------------";
|
wneuper@59285
|
126 |
(* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
|
wneuper@59285
|
127 |
val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
|
wneuper@59285
|
128 |
> split_dummy "x=-#5//#12";
|
wneuper@59285
|
129 |
val it = ("x=-#5//#12","") : string * string*)
|
wneuper@59285
|
130 |
|