(* tests for ListG

   author: Walther Neuper 1.5.03

use"../smltest/Scripts/listg.sml";

use"listg.sml";

*)

"--------------------- nth_ ----------------------------------------------";

"--------------------- nth_ ----------------------------------------------";

"--------------------- nth_ ----------------------------------------------";

val t = str2term "nth_ 3 [a,b,c,d,e]";

atomty t;

val thm = (#prop o rep_thm o num_str) nth_Cons_;

atomty thm;

val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;

if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 

else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";

val t = str2term "nth_ 1 [a,b,c,d,e]";

atomty t;

val thm = (#prop o rep_thm o num_str) nth_Nil_;

atomty thm;

val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;

term2str t';

"a";

val t = str2term "nth_ 3 [a,b,c,d,e]";

atomty t;

trace_rewrite:=true;

val Some (t',_) = rewrite_set_ thy false list_rls t;

trace_rewrite:=false;

term2str t';

"c";

(*-------------------------------------------------------------------*)

val Some (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";

val ttt = (#prop o rep_thm) thm;

atomty ttt;

(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)

"--------------------- length_ -------------------------------------------";

"--------------------- length_ -------------------------------------------";

"--------------------- length_ -------------------------------------------";

val thy' = "ListG.thy";

val ct = "length_ [1,1,1]";

val thm = ("length_Cons_","");

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val thm = ("length_Nil_","");

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

if ct="1 + (1 + (1 + 0))"then()

else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);

val ct = "length_ [1,1,1]";

val rls = "list_rls";

val (ct,asm) = the (rewrite_set thy' false rls ct);

if ct="3"then()

else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);

val ct = "length_ [1,1,1]";

val t = (term_of o the o (parse ListG.thy)) ct;

val t = eval_listexpr_ ListG.thy list_rls t;

case t of Free ("3",_) => () 

| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);

"--------------------- 29.4.03: union ------------------------------------";

"--------------------- 29.4.03: union ------------------------------------";

"--------------------- 29.4.03: union ------------------------------------";

fun ins_ x xs = if x mem xs then xs else x :: xs;

fun union_ xs [] = xs

  | union_ [] ys = ys

  | union_ (x :: xs) ys = union_ xs (ins_ x ys);

val t = (term_of o the o (parse ListG.thy)) "1 mem []";

atomty t;