neuper@42185
|
1 |
(* Title: tests for ListC
|
neuper@42185
|
2 |
Author: Walther Neuper 030501
|
neuper@42185
|
3 |
(c) copyright due to lincense terms.
|
neuper@42185
|
4 |
*)
|
neuper@42185
|
5 |
|
neuper@42185
|
6 |
|
neuper@42185
|
7 |
|
neuper@42185
|
8 |
"--------------------- nth_ ----------------------------------------------";
|
neuper@42185
|
9 |
"--------------------- nth_ ----------------------------------------------";
|
neuper@42185
|
10 |
"--------------------- nth_ ----------------------------------------------";
|
neuper@42185
|
11 |
val t = str2term "nth_ 3 [a,b,c,d,e]";
|
neuper@42185
|
12 |
atomty t;
|
neuper@42390
|
13 |
val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
|
neuper@42185
|
14 |
atomty thm;
|
neuper@42390
|
15 |
val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;
|
neuper@42185
|
16 |
if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
|
neuper@42185
|
17 |
else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
|
neuper@42185
|
18 |
|
neuper@42185
|
19 |
val t = str2term "nth_ 1 [a,b,c,d,e]";
|
neuper@42185
|
20 |
atomty t;
|
neuper@42390
|
21 |
val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
|
neuper@42185
|
22 |
atomty thm;
|
neuper@42390
|
23 |
val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;
|
neuper@42185
|
24 |
term2str t';
|
neuper@42185
|
25 |
"a";
|
neuper@42185
|
26 |
|
neuper@42185
|
27 |
val t = str2term "nth_ 3 [a,b,c,d,e]";
|
neuper@42185
|
28 |
atomty t;
|
neuper@42185
|
29 |
trace_rewrite:=true;
|
neuper@42185
|
30 |
val SOME (t',_) = rewrite_set_ thy false list_rls t;
|
neuper@42185
|
31 |
trace_rewrite:=false;
|
neuper@42185
|
32 |
term2str t';
|
neuper@42185
|
33 |
"c";
|
neuper@42185
|
34 |
|
neuper@42185
|
35 |
(*-------------------------------------------------------------------*)
|
neuper@42390
|
36 |
val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";
|
neuper@42185
|
37 |
val ttt = (#prop o rep_thm) thm;
|
neuper@42185
|
38 |
atomty ttt;
|
neuper@42185
|
39 |
(*Free ( 1, real) ...OK, Var ((x, 0), ?'a) OK*)
|
neuper@42185
|
40 |
|
neuper@42185
|
41 |
|
neuper@42185
|
42 |
|
neuper@42185
|
43 |
"--------------------- length_ -------------------------------------------";
|
neuper@42185
|
44 |
"--------------------- length_ -------------------------------------------";
|
neuper@42185
|
45 |
"--------------------- length_ -------------------------------------------";
|
neuper@42185
|
46 |
val thy' = "ListG";
|
neuper@42185
|
47 |
val ct = "length_ [1,1,1]";
|
neuper@42390
|
48 |
val thm = (@{thm LENGTH_CONS},"");
|
neuper@42185
|
49 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
neuper@42185
|
50 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
neuper@42185
|
51 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
neuper@42390
|
52 |
val thm = (@{thm LENGTH_NIL},"");
|
neuper@42185
|
53 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
neuper@42185
|
54 |
if ct="1 + (1 + (1 + 0))"then()
|
neuper@42185
|
55 |
else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
|
neuper@42185
|
56 |
|
neuper@42185
|
57 |
|
neuper@42185
|
58 |
val ct = "length_ [1,1,1]";
|
neuper@42185
|
59 |
val rls = "list_rls";
|
neuper@42185
|
60 |
val (ct,asm) = the (rewrite_set thy' false rls ct);
|
neuper@42185
|
61 |
if ct="3"then()
|
neuper@42185
|
62 |
else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
|
neuper@42185
|
63 |
|
neuper@42185
|
64 |
|
neuper@42185
|
65 |
val ct = "length_ [1,1,1]";
|
neuper@42185
|
66 |
val t = (term_of o the o (parse ListG.thy)) ct;
|
neuper@42185
|
67 |
val t = eval_listexpr_ ListG.thy list_rls t;
|
neuper@42185
|
68 |
case t of Free ("3",_) => ()
|
neuper@42185
|
69 |
| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
|
neuper@42185
|
70 |
|
neuper@42185
|
71 |
|