(* Title: tests for ListC

   Author: Walther Neuper 030501

   (c) copyright due to lincense terms.

*)

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

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

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

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

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

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

"--------------------- LENGTH ------------------------------------------------";

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

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

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

"----------- 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 prog_expr = assoc_rls "prog_expr"

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

atomty t;

val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_NIL};

atomty thm;

val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;

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

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

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

val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $

  (Const ("List.list.Cons", _) $ Free ("b", _) $ 

    (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;

atomty t;

val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_CONS};

atomty thm;

val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{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 = str2term "NTH 3 [a,b,c,d,e]";

atomty t;

Rewrite.trace_on := false;

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

Rewrite.trace_on := false;

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 = str2term "LENGTH [1, 1, 1]";

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

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

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

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

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

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

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

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

val NONE          = rewrite_ thy 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 = str2term "LENGTH [1, 1, 1]";

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

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

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

val t = str2term "LENGTH [1, 1, 1]";

val t = eval_prog_expr thy prog_expr t;

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

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