1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Sun Sep 22 16:52:14 2019 +0200
     1.3 @@ -0,0 +1,100 @@
     1.4 +(* Title: tests for ListC
     1.5 +   Author: Walther Neuper 030501
     1.6 +   (c) copyright due to lincense terms.
     1.7 +*)
     1.8 +
     1.9 +"-----------------------------------------------------------------------------";
    1.10 +"-----------------------------------------------------------------------------";
    1.11 +"table of contents -----------------------------------------------------------";
    1.12 +"-----------------------------------------------------------------------------";
    1.13 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.14 +"--------------------- NTH ---------------------------------------------------";
    1.15 +"--------------------- LENGTH ------------------------------------------------";
    1.16 +"--------------------- tl ----------------------------------------------------";
    1.17 +"-----------------------------------------------------------------------------";
    1.18 +"-----------------------------------------------------------------------------";
    1.19 +
    1.20 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.21 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.22 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.23 +(* ML representation *)
    1.24 +val t1 = @{term "{|| ||}"};
    1.25 +val t2 = @{term "{||1,2,3||}"};
    1.26 +
    1.27 +(* pretty printing *)
    1.28 +if Print_Mode.setmp [] 
    1.29 +  (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
    1.30 +  = "{|| ||}"
    1.31 +then () else error "CHANGED pretty printing of '{|| ||}'";
    1.32 +
    1.33 +if Print_Mode.setmp [] 
    1.34 +  (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
    1.35 +  = "{|| 1::'a, 2::'a, 3::'a ||}"
    1.36 +then () else error "CHANGED pretty printing of '{||1,2,3||}'"
    1.37 +
    1.38 +(* parsing *)
    1.39 +Syntax.read_term_global @{theory} "{|| ||}";
    1.40 +Syntax.read_term_global @{theory} "{||1,2,3||}";
    1.41 +
    1.42 +"--------------------- NTH ---------------------------------------------------";
    1.43 +"--------------------- NTH ---------------------------------------------------";
    1.44 +"--------------------- NTH ---------------------------------------------------";
    1.45 +val list_rls = assoc_rls "list_rls"
    1.46 +
    1.47 +val t = str2term "NTH 1 [a,b,c,d,e]";
    1.48 +atomty t;
    1.49 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
    1.50 +atomty thm;
    1.51 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
    1.52 +if term2str t' = "a" then () 
    1.53 +else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.54 +
    1.55 +val t = str2term "NTH 3 [a,b,c,d,e]";
    1.56 +val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
    1.57 +  (Const ("List.list.Cons", _) $ Free ("b", _) $ 
    1.58 +    (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
    1.59 +atomty t;
    1.60 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
    1.61 +atomty thm;
    1.62 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
    1.63 +if term2str t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.64 +else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.65 +
    1.66 +(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.67 +val t = str2term "NTH 3 [a,b,c,d,e]";
    1.68 +atomty t;
    1.69 +trace_rewrite := false;
    1.70 +val SOME (t', _) = rewrite_set_ thy false list_rls t;
    1.71 +trace_rewrite := false;
    1.72 +if term2str t' = "c" then () 
    1.73 +else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.74 +
    1.75 +"--------------------- LENGTH ------------------------------------------------";
    1.76 +"--------------------- LENGTH ------------------------------------------------";
    1.77 +"--------------------- LENGTH ------------------------------------------------";
    1.78 +val list_rls = assoc_rls "list_rls"
    1.79 +
    1.80 +val thy = @{theory ListC};
    1.81 +val t = str2term "LENGTH [1, 1, 1]";
    1.82 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.83 +term2str t = "1 + LENGTH [1, 1]";
    1.84 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.85 +term2str t = "1 + (1 + LENGTH [1])";
    1.86 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.87 +term2str t = "1 + (1 + (1 + LENGTH []))";
    1.88 +val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.89 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.90 +val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.91 +if term2str t = "1 + (1 + (1 + 0))" then () 
    1.92 +else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.93 +
    1.94 +val t = str2term "LENGTH [1, 1, 1]";
    1.95 +val SOME (t, asm) = rewrite_set_ thy false list_rls t;
    1.96 +if term2str t = "3" then ()
    1.97 +else error "LENGTH [1, 1, 1] = 3  ..list_rls changed";
    1.98 +
    1.99 +val t = str2term "LENGTH [1, 1, 1]";
   1.100 +val t = eval_listexpr_ thy list_rls t;
   1.101 +case t of Free ("3", _) => () 
   1.102 +| _ => error "LENGTH [1, 1, 1] = 3  ..eval_listexpr_ changed";
   1.103 +