1 (* Title: tests for Interpret/mstools.sml
2 Author: Walther Neuper 100930, Mathias Lehnfeld
3 (c) copyright due to lincense terms.
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
8 "--------------------------------------------------------";
9 "table of contents --------------------------------------";
10 "--------------------------------------------------------";
11 "----------- fun declare_constraints' -------------------";
12 "----------- fun declare_constraints --------------------";
13 "----------- fun get_assumptions, fun get_environments --";
14 "----------- fun transfer_asms_from_to ------------------";
15 "----------- fun from_subpbl_to_caller ------------------";
16 "----------- all ctxt changes in minimsubpbl x+1=2 ------";
17 "----------- go through Model_Problem until nxt_tac -----";
18 "--------------------------------------------------------";
19 "--------------------------------------------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
24 "----------- fun declare_constraints' -------------------";
25 "----------- fun declare_constraints' -------------------";
26 "----------- fun declare_constraints' -------------------";
27 val ctxt = ProofContext.init_global @{theory "Isac"};
28 val SOME ta = parseNEW ctxt "x";
29 if type_of ta = TFree ("'a",[]) then () else error "TODO";
31 (*----- add a type constraint to ctxt *)
32 val SOME ti = parseNEW ctxt "x::int";
33 val ctxt = declare_constraints' [ti] ctxt;
35 (*----- now parsing infers the type *)
36 val SOME t = parseNEW ctxt "x";
37 if type_of t = Type ("Int.int",[]) then () else error "TODO";
39 "----------- fun declare_constraints --------------------";
40 "----------- fun declare_constraints --------------------";
41 "----------- fun declare_constraints --------------------";
42 val ctxt = ProofContext.init_global @{theory "Isac"}
43 |> declare_constraints "xxx + yyy = (111::int)";
44 val t = case parseNEW ctxt "xxx = 123" of
45 NONE => error "mstools: syntax error"
47 if ((lhs t) |> type_of) = @{typ int} then ()
48 else error "mstools: incorrect type inference from parseNEW ctxt";
50 val t_bit = Syntax.read_term ctxt "11::int";
51 val t_free = numbers_to_string t_bit;
52 val ctxt = ProofContext.init_global @{theory "Isac"};
53 val SOME t = parseNEW ctxt "11";
54 if (t |> type_of) = TFree ("'a", ["Int.number"]) then ()
55 else error "parsed numeral correct";
56 val ctxt' = Variable.declare_constraints t_free ctxt;
57 val SOME t' = parseNEW ctxt' "11";
58 if (t' |> type_of) = TFree ("'a", ["Int.number"]) then ()
59 else error "Variable.declare_constraints did not recognize numeral";
61 "----------- fun get_assumptions, fun get_environments --";
62 "----------- fun get_assumptions, fun get_environments --";
63 "----------- fun get_assumptions, fun get_environments --";
64 val ctxt = insert_assumptions
65 [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
66 val ctxt = insert_assumptions
67 [@{term "x * v"}, @{term "2 * u"}] ctxt;
68 val asms = get_assumptions ctxt;
69 if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
70 else error "mstools.sml insert_/get_assumptions changed 1.";
72 val ctxt = insert_environments
73 [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
74 val envs = get_environments ctxt;
75 if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
76 else error "mstools.sml insert_/get_environments changed 2.";
78 "----------- fun transfer_asms_from_to ------------------";
79 "----------- fun transfer_asms_from_to ------------------";
80 "----------- fun transfer_asms_from_to ------------------";
81 val ctxt = ProofContext.init_global @{theory "Isac"}
82 val from_ctxt = insert_assumptions
83 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
84 val to_ctxt = insert_assumptions
85 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
86 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
87 if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
88 then () else error "fun transfer_asms_from_to changed"
90 "----------- fun from_subpbl_to_caller ------------------";
91 "----------- fun from_subpbl_to_caller ------------------";
92 "----------- fun from_subpbl_to_caller ------------------";
93 val ctxt = ProofContext.init_global @{theory "Isac"}
94 val sub_ctxt = insert_assumptions
95 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
96 val caller_ctxt = insert_assumptions
97 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
98 val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";
99 val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;
100 if terms2strs (get_assumptions new_ctxt) =
101 ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
102 then () else error "fun from_subpbl_to_caller changed"
104 "----------- all ctxt changes in minimsubpbl x+1=2 ------";
105 "----------- all ctxt changes in minimsubpbl x+1=2 ------";
106 "----------- all ctxt changes in minimsubpbl x+1=2 ------";
107 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
109 ("Test", ["sqroot-test","univariate","equation","test"],
110 ["Test","squ-equ-test-subpbl1"]);
112 (*========== inhibit exn AK110725 ================================================
113 (* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
115 ========== inhibit exn AK110725 ================================================*)
117 (*========== inhibit exn AK110725 ================================================
118 (* ERROR: pt and p are not declared due to above error *)
119 "=(1)= variables known from formalisation provide type-inference for further input";
120 val ctxt = get_ctxt pt p;
122 val SOME known_x = parseNEW ctxt "x+y+z";
123 val SOME unknown = parseNEW ctxt "xa+b+c";
125 if type_of known_x = Type ("RealDef.real",[]) then ()
126 else error "x+1=2 after start root-pbl wrong type-inference from known x";
127 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
128 else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
129 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
135 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
136 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
138 "=(2)= preconditions are known at start of interpretation of (root-)method";
139 if get_assumptions_ pt p = [str2term "precond_rootmet x"] then ()
140 else error "x+1=2 after start root-met no precondition";
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
146 "=(3)= variables known from arguments of (sub-)method provide type-inference for further input";
147 val ctxt = get_ctxt pt p;
148 val SOME known_x = parseNEW ctxt "x+y+z";
149 val SOME unknown = parseNEW ctxt "a+b+c";
150 if type_of known_x = Type ("RealDef.real",[]) then ()
151 else error "x+1=2 after start root-pbl wrong type-inference for known x";
152 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
153 else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
162 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
164 "=(4)= preconds are known at start of interpretation of (sub-)method";
165 if get_assumptions_ pt p =
166 [parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"] then ()
167 else error "x+1=2 after start sub-met no precondition";
169 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
171 "prep =(5)=: inject assumptions into sub-met: sub_asm_out, sub_asm_local";
172 val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
173 val ctxt = insert_assumptions [str2term "x < sub_asm_out", str2term "a < sub_asm_local"] cres;
174 val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
176 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
177 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
179 "=(5)= transfer non-local assumptions and result from sub-method to root-method." ^
180 " non-local assumptions are those contaning a variable known in root-method";
181 if terms2strs (get_assumptions_ pt p) =
182 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
183 then () else error "x+1=2 transfer from sub-met to root-met changed";
185 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)
186 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
188 "=(6)= assumptions collected during lucas-interpretation for proof of postcondition";
189 if terms2strs (get_assumptions_ pt p) = (*weak check: sub-result = root-result = [x = 1]*)
190 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
191 then () else error "x+1=2 transfer from sub-met to root-met changed";
192 ========== inhibit exn AK110725 ================================================*)
195 "----------- go through Model_Problem until nxt_tac -----";
196 "----------- go through Model_Problem until nxt_tac -----";
197 "----------- go through Model_Problem until nxt_tac -----";
198 (*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*)
199 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
201 ("Test", ["sqroot-test","univariate","equation","test"],
202 ["Test","squ-equ-test-subpbl1"]);
203 (*========== inhibit exn AK110725 ================================================
204 (* ERROR: same as above, see lines 120- 123 *)
205 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
206 ========== inhibit exn AK110725 ================================================*)
208 (*========== inhibit exn AK110725 ================================================
209 (* ERROR: p, nxt, pt not declared due to above error *)
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
219 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
221 "~~~~~ fun me, args:"; val (_,tac) = nxt;
222 val (pt, p) = case locatetac tac (pt,p) of
223 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
224 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
225 val pIopt = get_pblID (pt,ip);
227 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
228 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
229 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
230 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
231 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
232 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
233 val cpI = if pI = e_pblID then pI' else pI;
234 val cmI = if mI = e_metID then mI' else mI;
235 val {ppc, prls, where_, ...} = get_pbt cpI;
236 val pre = check_preconds "thy 100820" prls where_ probl;
237 val pb = foldl and_ (true, map fst pre);
238 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
239 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
240 "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
241 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
242 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
243 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
244 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
245 val cpI = if pI = e_pblID then pI' else pI;
246 val ctxt = get_ctxt pt (p, Pbl);
247 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
248 val SOME t = parseNEW ctxt str;
249 is_known ctxt sel oris t;
250 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
251 val _ = tracing ("RM is_known: t=" ^ term2str t);
252 val ots = (distinct o flat o (map #5)) (ori:ori list);
253 val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;
254 val (d, ts) = split_dts t;
255 "~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
256 (*if is_dsc d then () else error "TODO";*)
257 if is_dsc d then () else error "TODO";
258 "----- these were the errors (call hierarchy from bottom up)";
259 appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
260 Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
261 nxt_specif_additem "#Given" ct ptp;(*WAS
262 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
263 nxt_specif tac ptp;(*WAS
264 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
265 nxt_specify_ (pt,ip); (*WAS
266 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
267 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
268 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
269 ========== inhibit exn AK110725 ================================================*)