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