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