(* Title: tests for ListC

   Author: Walther Neuper 030501

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------";

"-----------------------------------------------------------------------------";

"----------- correct list_erls -----------------------------------------------------------------";

"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";

"--------------------- NTH ---------------------------------------------------";

"--------------------- Length ------------------------------------------------";

"--------------------- tl ----------------------------------------------------";

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"----------- correct list_erls -----------------------------------------------------------------";

"----------- correct list_erls -----------------------------------------------------------------";

"----------- correct list_erls -----------------------------------------------------------------";

"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";

"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";

"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";

(* ML representation *)

val t1 = @{term "{|| ||}"};

val t2 = @{term "{||1,2,3||}"};

(* pretty printing *)

if Print_Mode.setmp [] 

  (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1

  = "{|| ||}"

then () else error "CHANGED pretty printing of '{|| ||}'";

if Print_Mode.setmp [] 

  (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2

  = "{|| 1::'a, 2::'a, 3::'a ||}"

then () else error "CHANGED pretty printing of '{||1,2,3||}'"

(* parsing *)

Syntax.read_term_global @{theory} "{|| ||}";

Syntax.read_term_global @{theory} "{||1,2,3||}";

"--------------------- NTH ---------------------------------------------------";

"--------------------- NTH ---------------------------------------------------";

"--------------------- NTH ---------------------------------------------------";

val ctxt = Proof_Context.init_global @{theory}

val prog_expr = assoc_rls "prog_expr"

val t = TermC.str2term "NTH 1 [a,b,c,d,e]";

TermC.atomty t;

val thm = Thm.prop_of @{thm NTH_NIL};

TermC.atomty thm;

val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;

if UnparseC.term t' = "a" then () 

else error "NTH 1 [a,b,c,d,e] = a ..changed";

val t = TermC.str2term "NTH 3 [a,b,c,d,e]";

case TermC.str2term "NTH 3 [a,b,c,d,e]" of

 Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $

     (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $

       (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $

         (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $

           (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $

             (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()

| _ => error "ListC.NTH changed";

val thm = Thm.prop_of @{thm NTH_CONS};

TermC.atomty thm;

val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;

if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 

else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";

(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)

val t = TermC.str2term "NTH 3 [a,b,c,d,e]";

TermC.atomty t;

val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;

if UnparseC.term t' = "c" then () 

else error "NTH 3 [a,b,c,d,e] = c ..changed";

"--------------------- Length ------------------------------------------------";

"--------------------- Length ------------------------------------------------";

"--------------------- Length ------------------------------------------------";

val prog_expr = assoc_rls "prog_expr"

val thy = @{theory ListC};

val t = TermC.str2term "Length [1, 1, 1]";

val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;

UnparseC.term t = "1 + Length [1, 1]";

val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;

UnparseC.term t = "1 + (1 + Length [1])";

val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;

UnparseC.term t = "1 + (1 + (1 + Length []))";

val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;

val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;

val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;

if UnparseC.term t = "1 + (1 + (1 + 0))" then () 

else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";

val t = TermC.str2term "Length [1, 1, 1]";

val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;

if UnparseC.term t = "3" then ()

else error "Length [1, 1, 1] = 3  ..prog_expr changed";

val t = TermC.str2term "Length [1, 1, 1]";

val t = eval_prog_expr ctxt prog_expr t;

case t of 

  Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 

| _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";