neuper@42185: (* Title: tests for ListC
neuper@42185:    Author: Walther Neuper 030501
neuper@42185:    (c) copyright due to lincense terms.
neuper@42185: *)
neuper@42185: 
neuper@42185: 
neuper@42185: 
neuper@42185: "--------------------- nth_ ----------------------------------------------";
neuper@42185: "--------------------- nth_ ----------------------------------------------";
neuper@42185: "--------------------- nth_ ----------------------------------------------";
neuper@42185: val t = str2term "nth_ 3 [a,b,c,d,e]";
neuper@42185: atomty t;
neuper@42390: val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
neuper@42185: atomty thm;
neuper@42390: val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;
neuper@42185: if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
neuper@42185: else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
neuper@42185: 
neuper@42185: val t = str2term "nth_ 1 [a,b,c,d,e]";
neuper@42185: atomty t;
neuper@42390: val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
neuper@42185: atomty thm;
neuper@42390: val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;
neuper@42185: term2str t';
neuper@42185: "a";
neuper@42185: 
neuper@42185: val t = str2term "nth_ 3 [a,b,c,d,e]";
neuper@42185: atomty t;
neuper@42185: trace_rewrite:=true;
neuper@42185: val SOME (t',_) = rewrite_set_ thy false list_rls t;
neuper@42185: trace_rewrite:=false;
neuper@42185: term2str t';
neuper@42185: "c";
neuper@42185: 
neuper@42185: (*-------------------------------------------------------------------*)
neuper@42390: val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";
neuper@42185: val ttt = (#prop o rep_thm) thm;
neuper@42185: atomty ttt;
neuper@42185: (*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
neuper@42185: 
neuper@42185: 
neuper@42185: 
neuper@42185: "--------------------- length_ -------------------------------------------";
neuper@42185: "--------------------- length_ -------------------------------------------";
neuper@42185: "--------------------- length_ -------------------------------------------";
neuper@42185: val thy' = "ListG";
neuper@42185: val ct = "length_ [1,1,1]";
neuper@42390: val thm = (@{thm LENGTH_CONS},"");
neuper@42185: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
neuper@42185: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
neuper@42185: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
neuper@42390: val thm = (@{thm LENGTH_NIL},"");
neuper@42185: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
neuper@42185: if ct="1 + (1 + (1 + 0))"then()
neuper@42185: else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
neuper@42185: 
neuper@42185: 
neuper@42185: val ct = "length_ [1,1,1]";
neuper@42185: val rls = "list_rls";
neuper@42185: val (ct,asm) = the (rewrite_set thy' false rls ct);
neuper@42185: if ct="3"then()
neuper@42185: else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
neuper@42185: 
neuper@42185: 
neuper@42185: val ct = "length_ [1,1,1]";
neuper@42185: val t = (term_of o the o (parse ListG.thy)) ct;
neuper@42185: val t = eval_listexpr_ ListG.thy list_rls t;
neuper@42185: case t of Free ("3",_) => () 
neuper@42185: | _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
neuper@42185: 
neuper@42185: