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