|
agriesma@338
|
1 |
(* use"tests/list_rls.sml";
|
|
agriesma@338
|
2 |
W.N. 8.01
|
|
agriesma@338
|
3 |
only one item per file for test-impl.
|
|
agriesma@338
|
4 |
*)
|
|
agriesma@338
|
5 |
|
|
agriesma@338
|
6 |
|
|
agriesma@338
|
7 |
val thy' = "ListG.thy";
|
|
agriesma@338
|
8 |
val ct = "length_ [1,1,1]";
|
|
agriesma@338
|
9 |
val thm = ("length_Cons_","");
|
|
agriesma@338
|
10 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
|
agriesma@338
|
11 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
|
agriesma@338
|
12 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
|
agriesma@338
|
13 |
val thm = ("length_Nil_","");
|
|
agriesma@338
|
14 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
|
|
agriesma@338
|
15 |
if ct="1 + (1 + (1 + 0))"then()
|
|
agriesma@338
|
16 |
else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
|
|
agriesma@338
|
17 |
|
|
agriesma@338
|
18 |
|
|
agriesma@338
|
19 |
val ct = "length_ [1,1,1]";
|
|
agriesma@338
|
20 |
val rls = "list_rls";
|
|
agriesma@338
|
21 |
val (ct,asm) = the (rewrite_set thy' false rls ct);
|
|
agriesma@338
|
22 |
if ct="3"then()
|
|
agriesma@338
|
23 |
else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
|
|
agriesma@338
|
24 |
|
|
agriesma@338
|
25 |
|
|
agriesma@338
|
26 |
val ct = "length_ [1,1,1]";
|
|
agriesma@338
|
27 |
val t = (term_of o the o (parse ListG.thy)) ct;
|
|
agriesma@338
|
28 |
val t = eval_listexpr_ ListG.thy list_rls t;
|
|
agriesma@338
|
29 |
case t of Free ("3",_) => ()
|
|
agriesma@338
|
30 |
| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
|
|
agriesma@338
|
31 |
|
|
agriesma@338
|
32 |
|