|
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 ------------------";
|
|
neuper@41958
|
10 |
"-----------------------------------------------------------------";
|
|
neuper@41958
|
11 |
"-----------------------------------------------------------------";
|
|
neuper@41958
|
12 |
"-----------------------------------------------------------------";
|
|
neuper@41958
|
13 |
|
|
neuper@41958
|
14 |
|
|
neuper@41958
|
15 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
|
neuper@41958
|
16 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
|
neuper@41958
|
17 |
"-------------- fun applicable_in..Apply_Method ------------------";
|
|
neuper@41958
|
18 |
val fmz = ["equality (x+1=(2::real))",
|
|
neuper@41958
|
19 |
"solveFor (x::real)","solutions L"];
|
|
neuper@41958
|
20 |
val (dI',pI',mI') =
|
|
neuper@41958
|
21 |
("Test",["sqroot-test","univariate","equation","test"],
|
|
neuper@41958
|
22 |
["Test","squ-equ-test-subpbl1"]);
|
|
neuper@41958
|
23 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@41958
|
24 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@41958
|
25 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@41958
|
26 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
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 |
|
|
neuper@41958
|
32 |
val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt (fst p);
|
|
neuper@41958
|
33 |
val {where_, ...} = get_pbt pI;
|
|
neuper@41958
|
34 |
val where_ = [str2term "(lhs e_e) is_poly_in v_v"];(*just for test<>[]*)
|
|
neuper@41958
|
35 |
val pres = map (mk_env probl |> subst_atomic) where_;
|
|
neuper@41958
|
36 |
(*val pres = mk_env pbl |> subst_atomic #> where_;*)
|
|
neuper@41958
|
37 |
if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
|
|
neuper@41958
|
38 |
else error "appl.sml Apply_Method diff.behav.";
|
|
neuper@41958
|
39 |
|
|
neuper@41958
|
40 |
val ctxt = assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres;
|
|
neuper@41958
|
41 |
(*TODO.WN110416 read pres from ctxt and check*)
|
|
neuper@41958
|
42 |
|
|
neuper@41958
|
43 |
(*========== inhibit exn 110415 ================================================
|
|
neuper@41958
|
44 |
|
|
neuper@41958
|
45 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@41958
|
46 |
show_pt pt;
|
|
neuper@41958
|
47 |
============ inhibit exn 110415 ==============================================*)
|