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