Test_Isac works again, almost ..
4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"
The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82.
1 (* Title: tests on ProgLang/termC.sml
2 Author: Walther Neuper 051006,
3 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- numerals in Isabelle2011/12/13 -------------";
10 "----------- inst_bdv -----------------------------------";
11 "----------- subst_atomic_all ---------------------------";
12 "----------- Pattern.match ------------------------------";
13 "----------- fun matches --------------------------------";
14 "----------- fun parse, fun parse_patt, fun T_a2real ----";
15 "----------- uminus_to_string ---------------------------";
16 "----------- *** prep_pbt: syntax error in '#Where' of [v";
17 "----------- check writeln, tracing for string markup ---";
18 "-------- build fun is_bdv_subst ---------------------------------";
19 "--------------------------------------------------------";
20 "--------------------------------------------------------";
22 "----------- numerals in Isabelle2011/12/13 -------------";
23 "----------- numerals in Isabelle2011/12/13 -------------";
24 "----------- numerals in Isabelle2011/12/13 -------------";
25 "***Isabelle2011 ~= Isabelle2012 = Isabelle2013";
26 "***Isabelle2011**********************************************************************************";
28 (*Const ("Groups.zero_class.zero", "Nat.nat")*)
30 (*Const ("Groups.one_class.one", "Nat.nat")*)
32 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Nat.nat") $
33 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
34 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
35 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
36 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
38 (*Const ("Groups.zero_class.zero", "Int.int")*)
40 (*Const ("Groups.one_class.one", "Int.int")*)
42 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $
43 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
44 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
45 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
47 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $
48 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
49 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
50 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
52 (*Const ("Groups.uminus_class.uminus", "Int.int \<Rightarrow> Int.int") $
53 (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $
54 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
55 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
56 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
57 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
59 (*Const ("Groups.zero_class.zero", "RealDef.real")*)
63 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
64 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
65 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
66 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
68 (*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
69 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
70 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
71 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
73 (*Const ("Groups.uminus_class.uminus", "RealDef.real \<Rightarrow> RealDef.real") $
74 (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
75 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
76 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
77 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
78 "***Isabelle2012**********************************************************************************";
80 (*Const ("Groups.zero_class.zero", "nat")*)
82 (*Const ("Groups.one_class.one", "nat")*)
84 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $
85 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
86 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
87 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
89 (*Const ("Groups.zero_class.zero", "int")*)
91 (*Const ("Groups.one_class.one", "int")*)
93 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
94 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
95 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
97 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $
98 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
99 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
101 (*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $
102 (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
103 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
104 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
105 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
107 (*Const ("Groups.zero_class.zero", "real")*)
109 (*Const ("Groups.one_class.one", "real")*)
111 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
112 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
113 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
115 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $
116 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
117 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
119 (*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
120 (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
121 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
122 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
123 "***Isabelle2013**********************************************************************************";
125 (*Const ("Groups.zero_class.zero", "nat")*)
127 (*Const ("Groups.one_class.one", "nat")*)
129 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $
130 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
131 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
132 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
134 (*Const ("Groups.zero_class.zero", "int")*)
136 (*Const ("Groups.one_class.one", "int")*)
138 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
139 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
140 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
142 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $
143 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
144 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
146 (*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $
147 (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $
148 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
149 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
150 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
152 (*Const ("Groups.zero_class.zero", "real")*)
154 (*Const ("Groups.one_class.one", "real")*)
156 (*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
157 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
158 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
160 (*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $
161 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
162 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)
164 (*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
165 (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
166 (Const ("Num.num.Bit1", "num \<Rightarrow> num") $
167 (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)
169 "----------- inst_bdv -----------------------------------";
170 "----------- inst_bdv -----------------------------------";
171 "----------- inst_bdv -----------------------------------";
172 if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
173 "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)"
175 else error "termC.sml d1_isolate_add2";
176 val subst = [(str2term "bdv", str2term "x")];
177 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
178 val t' = inst_bdv subst t;
179 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)"
181 else error "termC.sml inst_bdv 1";
182 if (term2str o prop_of o num_str) @{thm separate_bdvs_add} =
183 "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^
184 " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
185 then () else error "termC.sml separate_bdvs_add";
189 [(str2term "bdv_1", str2term "c"),
190 (str2term "bdv_2", str2term "c_2"),
191 (str2term "bdv_3", str2term "c_3"),
192 (str2term "bdv_4", str2term "c_4")];
193 val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
194 val t' = inst_bdv subst t;
196 if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
197 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
198 then () else error "termC.sml inst_bdv 2";
200 "----------- subst_atomic_all ---------------------------";
201 "----------- subst_atomic_all ---------------------------";
202 "----------- subst_atomic_all ---------------------------";
203 val t = str2term "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
204 val env = [(str2term "vs_vs::real list", str2term "[c, c_2]"),
205 (str2term "es_es::bool list", str2term "[c_2 = 0, c + c_2 = 1]")];
206 val (all_Free_subst, t') = subst_atomic_all env t;
208 if all_Free_subst andalso
209 term2str t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"
211 else error "termC.sml subst_atomic_all should be 'true'";
213 val (all_Free_subst, t') = subst_atomic_all (tl env) t;
214 if not all_Free_subst andalso
215 term2str t' = "tl vs_vs from vs_vs occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" then ()
216 else error "termC.sml subst_atomic_all should be 'false'";
218 "----------- Pattern.match ------------------------------";
219 "----------- Pattern.match ------------------------------";
220 "----------- Pattern.match ------------------------------";
221 val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";
222 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
223 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
224 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
225 print_depth 3; (*999*) insts;
228 {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))),
229 (("b", 0), ("RealDef.real", Free ("x", "RealDef.real"))),
230 (("c", 0), ("RealDef.real", Free ("1", "RealDef.real")))})*)
232 "----- throws exn MATCH...";
233 (* val t = str2term "x";
234 (Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty))
235 handle MATCH => ???; *)
237 val thy = @{theory "Complex_Main"};
238 val PARSE = Syntax.read_term_global thy;
239 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
240 val (tye, tme) = (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
241 val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm) (tye, tme);
245 "----------- fun matches --------------------------------";
246 "----------- fun matches --------------------------------";
247 "----------- fun matches --------------------------------";
249 test/../Knowledge/polyeq.sml:
250 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
251 (*test/../Interpret/ptyps.sml:
252 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
253 val thy = @{theory "Complex_Main"};
256 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
257 tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
259 *** Const (op =, real => real => bool)
260 *** . Var ((a, 0), real)
261 *** . Const (Groups.zero_class.zero, real)
263 "----- test 1a true";
264 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
265 if matches thy tm pa then ()
266 else error "termC.sml diff.behav. in matches true 1";
267 "----- test 1b false";
268 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
269 if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
273 val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
274 tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
276 *** Const (op =, real => real => bool)
277 *** . Var ((a, 0), real)
278 *** . Var ((0, 0), real)
280 "----- test 2a true";
281 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
282 if matches thy tm pa then ()
283 else error "termC.sml diff.behav. in matches true 2";
284 "----- test 2b false";
285 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
286 if matches thy tm pa then ()
287 else error "termC.sml diff.behav. in matches false 2";
288 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
289 if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"
293 val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
294 tracing "paF2=..."; atomty pa; tracing "...=paF2";
296 *** Const (op =, real => real => bool)
297 *** . Var ((a, 0), real)
300 "----- test 3a true";
301 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
302 if matches thy tm pa then ()
303 else error "termC.sml diff.behav. in matches true 3";
304 "----- test 3b false";
305 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
306 if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
309 "----- test 4=3 with specific data";
310 val pa = free2var (str2term "M_b 0");
311 "----- test 4a true";
312 val tm = str2term "M_b 0";
313 if matches thy tm pa then ()
314 else error "termC.sml diff.behav. in matches true 4";
315 "----- test 4b false";
316 val tm = str2term "M_b x";
317 if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
321 "----------- fun parse, fun parse_patt, fun T_a2real ----";
322 "----------- fun parse, fun parse_patt, fun T_a2real ----";
323 "----------- fun parse, fun parse_patt, fun T_a2real ----";
324 val thy = @{theory "Complex_Main"};
329 val t = (Syntax.read_term_global thy str);
330 val t = numbers_to_string (Syntax.read_term_global thy str);
331 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
333 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
335 "===== fun parse_patt caused error in fun T_a2real ===";
336 val thy = @{theory "Poly"};
337 parse_patt thy "?p is_addUnordered";
338 parse_patt thy "?p :: real";
344 val t = (Syntax.read_term_global thy str);
345 val t = numbers_to_string (Syntax.read_term_global thy str);
346 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
348 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
350 "===== fun parse_patt caused error in fun T_a2real ===";
351 val thy = @{theory "Poly"};
352 parse_patt thy "?p is_addUnordered";
353 parse_patt thy "?p :: real";
355 (* Christian Urban, 101001
361 val parser = Args.context -- Scan.lift Args.name_source
362 fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt
363 |> ML_Syntax.print_term |> ML_Syntax.atomic
365 ML_Antiquote.inline "term_pat" (parser >> term_pat)
368 val t = @{term "a + b * x = (0 ::real)"};
369 val pat = @{term_pat "?l = (?r ::real)"};
370 val precond = @{term_pat "is_polynomial (?l::real)"};
371 val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
373 Envir.subst_term inst precond
374 |> Syntax.string_of_term @{context}
380 "----------- uminus_to_string ---------------------------";
381 "----------- uminus_to_string ---------------------------";
382 "----------- uminus_to_string ---------------------------";
383 val t1 = numbers_to_string @{term "-2::real"};
384 val t2 = numbers_to_string @{term "- 2::real"};
385 if uminus_to_string t2 = t1
387 else error "termC.sml diff.behav. in uminus_to_string";
389 "----------- *** prep_pbt: syntax error in '#Where' of [v";
390 "----------- *** prep_pbt: syntax error in '#Where' of [v";
391 "----------- *** prep_pbt: syntax error in '#Where' of [v";
392 "===== deconstruct datatype typ ===";
394 val t = (thy, str) |>> thy2ctxt
395 |-> Proof_Context.read_term_pattern
396 |> numbers_to_string;
397 val Var (("a", 0), ty) = t;
398 val TVar ((str, i), srt) = ty;
399 if str = "'a" andalso i = 1 andalso srt = []
401 else error "termC.sml type-structure of \"?a\" changed";
403 "----- real type in pattern ---";
404 val str = "?a :: real";
405 val t = (thy, str) |>> thy2ctxt
406 |-> Proof_Context.read_term_pattern
407 |> numbers_to_string;
408 val Var (("a", 0), ty) = t;
409 val Type (str, tys) = ty;
410 if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT
412 else error "termC.sml type-structure of \"?a :: real\" changed";
414 "===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";
415 val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^
416 " matchsub (?a + (?b - ?c)) t_t | " ^
417 " matchsub (?a - (?b + ?c)) t_t | " ^
418 " matchsub (?a + (?b - ?c)) t_t )");
419 val ctxt = Proof_Context.init_global thy;
420 val ctxt = Config.put show_types true ctxt;
421 "----- read_term_pattern ---";
422 val t = (thy, str) |>> thy2ctxt
423 |-> Proof_Context.read_term_pattern
424 |> numbers_to_string;
425 val t_real = typ_a2real t;
426 if term_to_string' ctxt t_real =
427 "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c))" ^
428 " t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" then ()
431 "----------- check writeln, tracing for string markup ---";
432 "----------- check writeln, tracing for string markup ---";
433 "----------- check writeln, tracing for string markup ---";
434 val t = @{term "x + 1"};
435 val str_markup = (Syntax.string_of_term
436 (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
437 val str = term_to_string'' "Isac" t;
439 writeln "----------------writeln str_markup---";
441 writeln "----------------writeln str---";
443 writeln "----------------SAME output: no markup----";
445 writeln "----------------writeln PolyML.makestring str_markup---";
446 writeln (PolyML.makestring str_markup);
447 writeln "----------------writeln PolyML.makestring str---";
448 writeln (PolyML.makestring str);
449 writeln "----------------DIFFERENT output----";
451 tracing "----------------tracing str_markup---";
453 tracing "----------------tracing str---";
455 tracing "----------------SAME output: no markup----";
457 tracing "----------------writeln PolyML.makestring str_markup---";
458 tracing (PolyML.makestring str_markup);
459 tracing "----------------writeln PolyML.makestring str---";
460 tracing (PolyML.makestring str);
461 tracing "----------------DIFFERENT output----";
463 redirect_tracing "../../tmp/";
464 tracing "----------------writeln str_markup---";
466 tracing "----------------writeln str---";
468 tracing "----------------DIFFERENT output----";
471 "----------- check writeln, tracing for string markup ---";
472 val t = @{term "x + 1"};
473 val str_markup = (Syntax.string_of_term
474 (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
475 val str = term_to_string'' "Isac" t;
477 writeln "----------------writeln str_markup---";
479 writeln "----------------writeln str---";
481 writeln "----------------SAME output: no markup----";
483 writeln "----------------writeln PolyML.makestring str_markup---";
484 writeln (PolyML.makestring str_markup);
485 writeln "----------------writeln PolyML.makestring str---";
486 writeln (PolyML.makestring str);
487 writeln "----------------DIFFERENT output----";
489 tracing "----------------tracing str_markup---";
491 tracing "----------------tracing str---";
493 tracing "----------------SAME output: no markup----";
495 tracing "----------------writeln PolyML.makestring str_markup---";
496 tracing (PolyML.makestring str_markup);
497 tracing "----------------writeln PolyML.makestring str---";
498 tracing (PolyML.makestring str);
499 tracing "----------------DIFFERENT output----";
501 redirect_tracing "../../tmp/";
502 tracing "----------------writeln str_markup---";
504 tracing "----------------writeln str---";
506 tracing "----------------DIFFERENT output----";
509 "-------- build fun is_bdv_subst ---------------------------------";
510 "-------- build fun is_bdv_subst ---------------------------------";
511 "-------- build fun is_bdv_subst ---------------------------------";
512 fun is_bdv_subst (Const ("List.list.Cons", _) $
513 (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
514 | is_bdv_subst _ = false;
516 if is_bdv_subst (str2term "[(bdv, v_v)]") then ()
517 else error "is_bdv_subst canged 1";
519 if is_bdv_subst (str2term "[(bdv_1, v_s1),(bdv_2, v_s2)]") then ()
520 else error "is_bdv_subst canged 2";