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@52148: "-----------------------------------------------------------------------------";
neuper@52148: "-----------------------------------------------------------------------------";
neuper@52148: "table of contents -----------------------------------------------------------";
neuper@52148: "-----------------------------------------------------------------------------";
walther@60317: "----------- correct list_erls -----------------------------------------------------------------";
wneuper@59244: "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
neuper@52148: "--------------------- NTH ---------------------------------------------------";
walther@60121: "--------------------- Length ------------------------------------------------";
neuper@52148: "--------------------- tl ----------------------------------------------------";
neuper@52148: "-----------------------------------------------------------------------------";
neuper@52148: "-----------------------------------------------------------------------------";
neuper@42185: 
walther@60317: "----------- correct list_erls -----------------------------------------------------------------";
walther@60317: "----------- correct list_erls -----------------------------------------------------------------";
walther@60317: "----------- correct list_erls -----------------------------------------------------------------";
walther@60317: 
wneuper@59244: "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
wneuper@59244: "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
wneuper@59244: "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
wneuper@59234: (* ML representation *)
wneuper@59244: val t1 = @{term "{|| ||}"};
wneuper@59244: val t2 = @{term "{||1,2,3||}"};
wneuper@59234: 
wneuper@59234: (* pretty printing *)
wneuper@59234: if Print_Mode.setmp [] 
wneuper@59234:   (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
wneuper@59244:   = "{|| ||}"
wneuper@59244: then () else error "CHANGED pretty printing of '{|| ||}'";
wneuper@59234: 
wneuper@59234: if Print_Mode.setmp [] 
wneuper@59234:   (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
wneuper@59244:   = "{|| 1::'a, 2::'a, 3::'a ||}"
wneuper@59244: then () else error "CHANGED pretty printing of '{||1,2,3||}'"
wneuper@59234: 
wneuper@59234: (* parsing *)
wneuper@59244: Syntax.read_term_global @{theory} "{|| ||}";
wneuper@59244: Syntax.read_term_global @{theory} "{||1,2,3||}";
neuper@42185: 
neuper@52148: "--------------------- NTH ---------------------------------------------------";
neuper@52148: "--------------------- NTH ---------------------------------------------------";
neuper@52148: "--------------------- NTH ---------------------------------------------------";
Walther@60500: val ctxt = Proof_Context.init_global @{theory}
walther@59801: val prog_expr = assoc_rls "prog_expr"
neuper@52148: 
walther@60230: val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
walther@60230: TermC.atomty t;
walther@60337: val thm = Thm.prop_of @{thm NTH_NIL};
walther@60230: TermC.atomty thm;
Walther@60509: val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
walther@59868: if UnparseC.term t' = "a" then () 
neuper@52148: else error "NTH 1 [a,b,c,d,e] = a ..changed";
neuper@52148: 
walther@60230: val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
walther@60317: case TermC.str2term "NTH 3 [a,b,c,d,e]" of
walther@60336:  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>, _))) $
walther@60336:      (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
walther@60336:        (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
walther@60336:          (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $
walther@60336:            (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
walther@60336:              (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
walther@60317: | _ => error "ListC.NTH changed";
walther@60337: val thm = Thm.prop_of @{thm NTH_CONS};
walther@60230: TermC.atomty thm;
Walther@60509: val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;
walther@60317: if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
neuper@52148: else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
neuper@42185: 
neuper@52148: (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
walther@60230: val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
walther@60230: TermC.atomty t;
Walther@60500: 
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
walther@59868: if UnparseC.term t' = "c" then () 
neuper@52148: else error "NTH 3 [a,b,c,d,e] = c ..changed";
neuper@42185: 
walther@60121: "--------------------- Length ------------------------------------------------";
walther@60121: "--------------------- Length ------------------------------------------------";
walther@60121: "--------------------- Length ------------------------------------------------";
walther@59801: val prog_expr = assoc_rls "prog_expr"
neuper@42185: 
neuper@52148: val thy = @{theory ListC};
walther@60230: val t = TermC.str2term "Length [1, 1, 1]";
Walther@60500: val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
walther@60121: UnparseC.term t = "1 + Length [1, 1]";
Walther@60500: val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
walther@60121: UnparseC.term t = "1 + (1 + Length [1])";
Walther@60500: val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
walther@60121: UnparseC.term t = "1 + (1 + (1 + Length []))";
Walther@60500: val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
Walther@60500: val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
Walther@60500: val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
walther@59868: if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
walther@60121: else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
neuper@42185: 
walther@60230: val t = TermC.str2term "Length [1, 1, 1]";
Walther@60500: val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;
walther@59868: if UnparseC.term t = "3" then ()
walther@60121: else error "Length [1, 1, 1] = 3  ..prog_expr changed";
neuper@42185: 
walther@60230: val t = TermC.str2term "Length [1, 1, 1]";
Walther@60500: val t = eval_prog_expr ctxt prog_expr t;
walther@60317: case t of 
walther@60336:   Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 
walther@60121: | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
neuper@42185: