wneuper/isa: test/Tools/isac/ProgLang/listC.sml@96174a374a7a

     1 (* Title: tests for ListC

     2    Author: Walther Neuper 030501

     3    (c) copyright due to lincense terms.

     4 *)

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

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

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

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

    12 atomty t;

    13 val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};

    14 atomty thm;

    15 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;

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

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

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

    20 atomty t;

    21 val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};

    22 atomty thm;

    23 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;

    24 term2str t';

    25 "a";

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

    28 atomty t;

    29 trace_rewrite:=true;

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

    31 trace_rewrite:=false;

    32 term2str t';

    33 "c";

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

    36 val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";

    37 val ttt = (#prop o rep_thm) thm;

    38 atomty ttt;

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

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

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

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

    46 val thy' = "ListG";

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

    48 val thm = (@{thm LENGTH_CONS},"");

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

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

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

    52 val thm = (@{thm LENGTH_NIL},"");

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

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

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

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

    59 val rls = "list_rls";

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

    61 if ct="3"then()

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

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

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

    67 val t = eval_listexpr_ ListG.thy list_rls t;

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

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 13 Mar 2012 15:04:09 +0100
changeset 42390	96174a374a7a
parent 42185	332a0653d4c9
child 52148	aabc6c8e930a
permissions	-rw-r--r--