wneuper/isa: test/Tools/isac/ProgLang/listg.sml@460c24a6a6ba

     1 (* tests for ListG

     2    author: Walther Neuper 1.5.03

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

     5 use"listg.sml";

     6 *)

    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 @{thm nth_Cons_}) t;

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

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

    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 @{thm nth_Nil_}) t;

    26 term2str t';

    27 "a";

    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";

    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*)

    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 error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);

    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 error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);

    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 | _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37970	6df5d02e46ba
child 38058	ad0485155c0e
permissions	-rw-r--r--