1 "-----------------------------------------------------------------------------------------------";
2 "-----------------------------------------------------------------------------------------------";
3 "table of contents -----------------------------------------------------------------------------";
4 "-----------------------------------------------------------------------------------------------";
5 "----------- fun union, fun merge --------------------------------------------------------------";
6 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
7 "----------- fun drop_last_n -------------------------------------------------------------------";
8 "----------- fun split_nlast, fun takewhile ----------------------------------------------------";
9 "----------- fun de_quote ----------------------------------------------------------------------";
10 "----------- fun ids_of ------------------------------------------------------------------------";
11 "----------- fun overwritel --------------------------------------------------------------------";
12 "----------- fun take_fromto --------------------------------------------------------------------";
13 "----------- val ~~~ ----------------------------------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
18 "----------- fun union, fun merge --------------------------------------------------------------";
19 "----------- fun union, fun merge --------------------------------------------------------------";
20 "----------- fun union, fun merge --------------------------------------------------------------";
21 if union (op =) [1,2,3] [3,4,5] = [2, 1, 3, 4, 5] then () else error "union changed";
22 if Library.merge (op =) ([1,2,3], [3,4,5]) = [4, 5, 1, 2, 3] then () else error "merge changed";
24 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
25 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
26 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
27 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
28 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
29 "----------- fun drop_nth, fun takerest, fun takelast -----------------------------------------";
30 if drop_nth [] (3, [1,2,3,4,5]) = [1, 2, 4, 5] then () else error "drop_nth 1 CHANGED";
31 if drop_nth [] (1,[1,2,3,4,5]) = [2, 3, 4, 5] then () else error "drop_nth 2 CHANGED";
32 if drop_nth [] (5,[1,2,3,4,5]) = [1, 2, 3, 4] then () else error "drop_nth 3 CHANGED";
33 if drop_nth [] (0,[1,2,3,4,5]) = [1, 2, 3, 4, 5] then () else error "drop_nth 4 CHANGED";
34 if drop_nth [] (999,[1,2,3,4,5]) = [1, 2, 3, 4, 5] then () else error "drop_nth 5 CHANGED";
36 (*> takerest (3, ["normalise", "polynomial", "univariate", "equation"]);
37 val it = ["equation"] : string list
40 (* > takelast (2, ["normalise", "polynomial", "univariate", "equation"]);
41 val it = ["univariate", "equation"] : pblID
42 > takelast (2, ["equation"]);
43 val it = ["equation"] : pblID
44 > takelast (3, ["normalise", "polynomial", "univariate", "equation"]);
45 val it = ["polynomial", "univariate", "equation"]*)
47 "----------- fun drop_last_n -------------------------------------------------------------------";
48 "----------- fun drop_last_n -------------------------------------------------------------------";
49 "----------- fun drop_last_n -------------------------------------------------------------------";
50 (*> drop_last_n 2 [1,2,3,4,5];
51 val it = [1, 2, 3] : int list
52 > drop_last_n 3 [1,2,3,4,5];
53 val it = [1, 2] : int list
54 > drop_last_n 7 [1,2,3,4,5];
55 val it = [] : int list
58 "----------- fun split_nlast, fun takewhile ----------------------------------------------------";
59 "----------- fun split_nlast, fun takewhile ----------------------------------------------------";
60 "----------- fun split_nlast, fun takewhile ----------------------------------------------------";
61 (* val (a, b) = split_nlast (3, ["a", "b", "[", ".", "]"]);
62 val a = ["a", "b"] : string list
63 val b = ["[", ".", "]"] : string list
64 > val (a, b) = split_nlast (3, [".", "]"]);
65 val a = [] : string list
66 val b = [".", "]"] : string list *)
68 (* > takewhile [] (not o (curry op= 4)) [1,2,3,4,5,6,7];
69 val it = [1, 2, 3] : int list*)
71 "----------- fun de_quote ----------------------------------------------------------------------";
72 "----------- fun de_quote ----------------------------------------------------------------------";
73 "----------- fun de_quote ----------------------------------------------------------------------";
74 (*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
75 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
77 "----------- fun ids_of ------------------------------------------------------------------------";
78 "----------- fun ids_of ------------------------------------------------------------------------";
79 "----------- fun ids_of ------------------------------------------------------------------------";
81 > val t = (Thm.term_of o the o (TermC.parse thy))
82 "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
84 ["solve'_univar", "Product_Type.Pair", "R", "Cons", "univar", "equation", "Nil",...]*)
86 "----------- fun overwritel --------------------------------------------------------------------";
87 "----------- fun overwritel --------------------------------------------------------------------";
88 "----------- fun overwritel --------------------------------------------------------------------";
89 (*> val aaa = [(1,11),(2,22),(3,33)];
90 > overwritel (aaa, [(2,2222),(4,4444)]);
91 val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*)
93 "----------- fun take_fromto --------------------------------------------------------------------";
94 "----------- fun take_fromto --------------------------------------------------------------------";
95 "----------- fun take_fromto --------------------------------------------------------------------";
96 (*> take_fromto 3 5 [1,2,3,4,5,6,7];
97 val it = [3,4,5] : int list
98 > take_fromto 3 3 [1,2,3,4,5,6,7];
99 val it = [3] : int list*)
101 "----------- val ~~~ ----------------------------------------------------------------------------";
102 "----------- val ~~~ ----------------------------------------------------------------------------";
103 "----------- val ~~~ ----------------------------------------------------------------------------";
104 (*[1,2,3] ~~~ ["1", "2", "3"];
105 val it = [(1, "1"), (2, "2"), (3, "3")] : (int * string) list
106 > [1,2] ~~~ ["1", "2", "3"];
107 val it = [(1, "1"), (2, "2")] : (int * string) list
108 > [1,2,3] ~~~ ["1", "2"];
109 val it = [(1, "1"), (2, "2")] : (int * string) list*)
111 "----------- fun strs2str, fun strs2str', fun list2str -----------------------------------------";
112 "----------- fun strs2str, fun strs2str', fun list2str -----------------------------------------";
113 "----------- fun strs2str, fun strs2str', fun list2str -----------------------------------------";
114 (*> val str = strs2str ["123", "asd"]; tracing str;
115 val it = "[\"123\", \"asd\"]" : string
118 (*> val str = list2str ["123", "asd"]; tracing str;
119 val str = "[123, asd]" : string