1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Jul 25 17:44:19 2011 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(* Title: tests for ListC
     1.5 +   Author: Walther Neuper 030501
     1.6 +   (c) copyright due to lincense terms.
     1.7 +*)
     1.8 +
     1.9 +
    1.10 +
    1.11 +"--------------------- nth_ ----------------------------------------------";
    1.12 +"--------------------- nth_ ----------------------------------------------";
    1.13 +"--------------------- nth_ ----------------------------------------------";
    1.14 +val t = str2term "nth_ 3 [a,b,c,d,e]";
    1.15 +atomty t;
    1.16 +val thm = (#prop o rep_thm o num_str) nth_Cons_;
    1.17 +atomty thm;
    1.18 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
    1.19 +if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
    1.20 +else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
    1.21 +
    1.22 +val t = str2term "nth_ 1 [a,b,c,d,e]";
    1.23 +atomty t;
    1.24 +val thm = (#prop o rep_thm o num_str) nth_Nil_;
    1.25 +atomty thm;
    1.26 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;
    1.27 +term2str t';
    1.28 +"a";
    1.29 +
    1.30 +val t = str2term "nth_ 3 [a,b,c,d,e]";
    1.31 +atomty t;
    1.32 +trace_rewrite:=true;
    1.33 +val SOME (t',_) = rewrite_set_ thy false list_rls t;
    1.34 +trace_rewrite:=false;
    1.35 +term2str t';
    1.36 +"c";
    1.37 +
    1.38 +(*-------------------------------------------------------------------*)
    1.39 +val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
    1.40 +val ttt = (#prop o rep_thm) thm;
    1.41 +atomty ttt;
    1.42 +(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
    1.43 +
    1.44 +
    1.45 +
    1.46 +"--------------------- length_ -------------------------------------------";
    1.47 +"--------------------- length_ -------------------------------------------";
    1.48 +"--------------------- length_ -------------------------------------------";
    1.49 +val thy' = "ListG";
    1.50 +val ct = "length_ [1,1,1]";
    1.51 +val thm = ("length_Cons_","");
    1.52 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.53 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.54 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.55 +val thm = ("length_Nil_","");
    1.56 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
    1.57 +if ct="1 + (1 + (1 + 0))"then()
    1.58 +else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
    1.59 +
    1.60 +
    1.61 +val ct = "length_ [1,1,1]";
    1.62 +val rls = "list_rls";
    1.63 +val (ct,asm) = the (rewrite_set thy' false rls ct);
    1.64 +if ct="3"then()
    1.65 +else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
    1.66 +
    1.67 +
    1.68 +val ct = "length_ [1,1,1]";
    1.69 +val t = (term_of o the o (parse ListG.thy)) ct;
    1.70 +val t = eval_listexpr_ ListG.thy list_rls t;
    1.71 +case t of Free ("3",_) => () 
    1.72 +| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
    1.73 +
    1.74 +