3 for both, math-engine and isa-98-1-HOL-plus
4 however, functions closely related to original isabelle-98-1 functions
5 are in isa-98-1-HOL-plus/rewrite-parse/library_G
8 (* Isabelle2002 -> Isabelle2009 library changed:
12 val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
13 val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
14 val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
15 val take: int * 'a list -> 'a list
16 val drop: int * 'a list -> 'a list
17 val last_elem: 'a list -> 'a
19 FIXME: overwritten again...*)
20 fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = (*FIXME.2009*)
21 let fun itl (e, []) = e
22 | itl (e, a::l) = itl (f(e, a), l)
24 fun foldr f (l, e) = (*FIXME.2009*)
26 | itr (a::l) = f(a, itr l)
28 fun take (n, []) = [] (*FIXME.2009*)
30 if n > 0 then x :: take (n - 1, xs) else [];
31 fun drop (n, []) = [] (*FIXME.2009*)
33 if n > 0 then drop (n - 1, xs) else x :: xs;
35 (*exn LIST has disappeared in 2009 ... replaced by error...*)
36 fun last_elem [] = error "last_elem" (*FIXME.2009*)
38 | last_elem (_ :: xs) = last_elem xs;
40 fun gen_mem eq (x, []) = false (*FIXME.2009*)
41 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
42 fun gen_insert (les : 'a * 'a -> bool) ([], a) = [a]
43 | gen_insert les (x::xs, a) = if les (x, a) then x::(gen_insert les (xs, a))
45 fun gen_sort les xs = foldl (gen_insert les) (xs, []);
46 fun gen_distinct eq lst =
48 val memb = gen_mem eq;
50 fun dist (rev_seen, []) = rev rev_seen
51 | dist (rev_seen, x :: xs) =
52 if memb (x, rev_seen) then dist (rev_seen, xs)
53 else dist (x :: rev_seen, xs);
57 fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
58 fun distinct l = gen_distinct (op =) l;
62 (*.see 'fun (y :: ys) \ x' in Pure/library.ML.*)
63 fun gen_dif eq (y :: ys, x) = if eq (y, x) then ys
64 else y :: (gen_dif eq (ys, x))
65 | gen_dif eq ([], x) = [];
66 (* val (eq, (y :: ys, x)) = ();*)
68 (*.see 'fun ys \\ xs' in Pure/library.ML.*)
69 fun gen_diff eq (ys, xs) = foldl (gen_dif eq) (ys,xs);
70 (* val (eq, (ys, xs)) = (eq_thmI, (isacrlsthms, isacthms));
72 (* gen_diff op= ([1,2,3,4,5,6,7],[2,3,5]);
73 val it = [1, 4, 6, 7] : int list*)
76 (*an indulgent version of Isabelle/src/Pure/library.ML ~~*)
79 let fun aaa xys [] [] = xys
80 | aaa xys [] (y :: ys) = xys
81 | aaa xys (x :: xs) [] = xys
82 | aaa xys (x :: xs) (y :: ys) = aaa (xys @ [(x, y)]) xs ys
84 (*[1,2,3] ~~~ ["1","2","3"];
85 val it = [(1, "1"), (2, "2"), (3, "3")] : (int * string) list
86 > [1,2] ~~~ ["1","2","3"];
87 val it = [(1, "1"), (2, "2")] : (int * string) list
88 > [1,2,3] ~~~ ["1","2"];
89 val it = [(1, "1"), (2, "2")] : (int * string) list*)
91 (*from Isabelle2002/src/Pure/library.ML; has changed in 2009 FIXME replace*)
92 fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
93 fun gen_insI eq pr (x, xs) =
95 then (tracing ("### occurs twice: "^(pr x)); xs)
97 fun gen_union eq pr (xs, []) = xs
98 | gen_union eq pr ([], ys) = ys
99 | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));
101 fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)
103 fun nth _ [] = error "nth _ []" (*Isabelle2002, still saved the hours of update*)
105 | nth n (_::xs) = nth (n-1) xs;
106 (*fun nth xs i = List.nth (xs, i); recent Isabelle: TODO update all isac code *)
107 (*analogous to List.list_update*)
108 fun list_update [] _ _ = []
109 | list_update (x :: xs) i v =
112 | j => x :: list_update xs (j - 1) v
114 (*WN050106 quick for test: doesn't check for exns*)
115 fun drop_nth ls (_, []) = ls
116 | drop_nth ls (n, x :: xs) =
119 else drop_nth (ls @ [x]) (n - 1, xs);
120 (*> drop_nth [] (3,[1,2,3,4,5]);
121 val it = [1, 2, 4, 5] : int list
122 > drop_nth [] (1,[1,2,3,4,5]);
123 val it = [2, 3, 4, 5] : int list
124 > drop_nth [] (5,[1,2,3,4,5]);
125 val it = [1, 2, 3, 4] : int list *)
127 fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *)
128 fun or_ (b1,b2) = b1 orelse b2;
131 fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);
132 (*> takerest (3, ["normalize","polynomial","univariate","equation"]);
133 val it = ["equation"] : string list
135 fun takelast (i, ls) = (rev o take) (i, rev ls);
136 (* > takelast (2, ["normalize","polynomial","univariate","equation"]);
137 val it = ["univariate", "equation"] : pblID
138 > takelast (2, ["equation"]);
139 val it = ["equation"] : pblID
140 > takelast (3, ["normalize","polynomial","univariate","equation"]);
141 val it = ["polynomial", "univariate", "equation"]*)
142 fun split_nlast (i, ls) =
144 in (rev (takelast (i - 1, rv)), rev (take (i, rv))) end;
146 fun split_nlast (i, ls) = (take (length ls - i, ls), rev (take (i, rev ls)));
147 (* val (a, b) = split_nlast (3, ["a","b","[",".","]"]);
148 val a = ["a", "b"] : string list
149 val b = ["[", ".", "]"] : string list
150 > val (a, b) = split_nlast (3, [".","]"]);
151 val a = [] : string list
152 val b = [".", "]"] : string list *)
154 (*.analoguous to dropwhile in Pure/libarary.ML.*)
155 fun dropwhile P [] = []
156 | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
157 fun takewhile col P [] = col
158 | takewhile col P (ys as x::xs) = if P x then takewhile (col @ [x]) P xs
160 (* > takewhile [] (not o (curry op= 4)) [1,2,3,4,5,6,7];
161 val it = [1, 2, 3] : int list*)
162 fun dropuntil P [] = []
163 | dropuntil P (ys as x::xs) = if P x then ys else dropuntil P xs;
167 fun pair2tri ((a,b),c) = (a,b,c);
168 fun fst3 (a,_,_) = a;
169 fun snd3 (_,b,_) = b;
170 fun thd3 (_,_,c) = c;
172 fun skip_blanks strl =
174 fun skip strl [] = strl
175 | skip strl (" "::ss) = skip strl ss
176 | skip strl ( s ::ss) = skip (strl @ [s]) ss
182 let fun scan ss' [] = ss'
183 | scan ss' ("\""::ss) = scan ss' ss
184 | scan ss' (s::ss) = scan (ss' @ [s]) ss;
185 in (implode o (scan []) o Symbol.explode) str end;
186 (*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
187 val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
191 (* conversions to (quoted) strings
192 FIXME: rename *2str --> *2strq (quoted elems)
193 now *2str' (elems NOT quoted) instead of *2str *)
195 val commas = space_implode ",";
197 fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]";
198 (*> val str = strs2str ["123","asd"]; tracing str;
199 val it = "[\"123\", \"asd\"]" : string
201 fun strs2str' strl = "[" ^ (commas strl) ^ "]";
202 fun list2str strl = "[" ^ (commas strl) ^ "]";
203 (*> val str = list2str ["123","asd"]; tracing str;
204 val str = "[123, asd]" : string
206 fun strslist2strs strslist = map strs2str strslist |> strs2str';
207 fun spair2str (s1,s2) = "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")";
208 fun pair2str (s1,s2) = "(" ^ s1 ^ ", " ^ s2 ^ ")";
210 fun subs2str (subs:(string * string) list) =
211 (list2str o (map pair2str)) subs;*)
212 fun subs2str (subs: string list) = list2str subs;
213 (*> val sss = ["(bdv,x)","(err,#0)"];
215 val it = "[(bdv,x),(err,#0)]" : string*)
216 fun subs2str' (subs:(string * string) list) = (*12.12.99???*)
217 (list2str o (map pair2str)) subs;
218 (*> val subs = subs2str [("bdv","x")]; tracing subs;
219 val subs = "[(\"bdv\", \"x\")]" : string
221 fun con2str land_lor = quote " &| ";
222 val int2str = string_of_int;
223 fun ints2str ints = (strs2str o (map string_of_int)) ints;
224 fun ints2str' ints = (strs2str' o (map string_of_int)) ints;
226 (* findFillpatterns: the message's format is waiting for generalisation of CalcMessage *)
227 fun pair2str_ (s1,s2) = s1 ^ "#" ^ s2;
228 val nos = space_implode "#";
229 fun strs2str_ strl = "#" ^ (nos strl) ^ "#";
231 (*needed in Isa + ME*)
233 let fun get strl [] = strl
234 | get strl ("."::ss) = strl
235 | get strl ( s ::ss) = get (strl @ [s]) ss
236 in implode( get [] (Symbol.explode str)) end;
239 let fun strip bdVar [] = implode (rev bdVar)
240 | strip bdVar ("."::_ ) = implode (rev bdVar)
241 | strip bdVar (c ::cs) = strip (bdVar @[c]) cs
242 in strip [] (rev(Symbol.explode str)) end;
244 fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix)
245 | id_of (Free (id ,_)) = id
246 | id_of (Const(id ,_)) = id
247 | id_of _ = ""; (* never such an identifier *)
250 let fun con ss (Const (s,_)) = s::ss
251 | con ss (Free (s,_)) = s::ss
252 | con ss (Abs (s,_,b)) = s::(con ss b)
253 | con ss (t1 $ t2) = (con ss t1) @ (con ss t2)
255 in map strip_thy ((distinct o (con [])) t) end;
257 > val t = (term_of o the o (parse thy))
258 "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
260 ["solve'_univar","Product_Type.Pair","R","Cons","univar","equation","Nil",...]*)
263 (*FIXME.WN090819 fun overwrite missing in ..2009/../library.ML*)
264 fun overwrite (al, p as (key, _)) = (*FIXME.2009*)
265 let fun over ((q as (keyi, _)) :: pairs) =
266 if keyi = key then p :: pairs else q :: (over pairs)
269 fun overwritel (al, []) = al
270 | overwritel (al, b::bl) = overwritel (overwrite (al, b), bl);
271 (*> val aaa = [(1,11),(2,22),(3,33)];
272 > overwritel (aaa, [(2,2222),(4,4444)]);
273 val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*)
278 | intsto1 n = (intsto1 (n-1)) @ [n]
280 fun intsto n = if n < 0 then (error "intsto < 0") else intsto1 n
284 type 'a stack = 'a list;
285 fun top ((x::xs):'a stack) = x
286 | top _ = error "top called for empty list";
287 fun pop ((x::xs):'a stack) = xs:'a stack
288 | pop _ = error "pop called for empty list";
289 fun push x (xs:'a stack) = x::xs:'a stack;
292 fun drop_last l = ((rev o tl o rev) l);
293 fun drop_last_n n l = rev (takerest (n, rev l));
294 (*> drop_last_n 2 [1,2,3,4,5];
295 val it = [1, 2, 3] : int list
296 > drop_last_n 3 [1,2,3,4,5];
297 val it = [1, 2] : int list
298 > drop_last_n 7 [1,2,3,4,5];
299 val it = [] : int list
302 fun bool2str true = "true"
303 | bool2str false = "false";
304 fun string_to_bool "true" = true
305 | string_to_bool "false" = false
306 | string_to_bool str = error ("string_to_bool: arg = " ^ str)
308 (*.take elements from b to e including both.*)
309 fun take_fromto from to l =
310 if from > to then error ("take_fromto from="^string_of_int from^
311 " > to="^string_of_int to)
312 else drop (from - 1, take (to, l));
313 (*> take_fromto 3 5 [1,2,3,4,5,6,7];
314 val it = [3,4,5] : int list
315 > take_fromto 3 3 [1,2,3,4,5,6,7];
316 val it = [3] : int list*)
320 | idt str n = str ^ idt str (n-1);
322 | indt n = " " ^ indt (n-1);---------does not terminate with negatives*)
323 fun indt n = if n <= 0 then "" else " " ^ indt (n-1);
324 fun indent i = fold (curry op ^) (replicate i ". ") ""
326 fun dashs i = if 0<i then "-"^ dashs (i-1) else "";
327 fun dots i = if 0<i then "."^ dots (i-1) else "";
329 fun assoc ([], key) = NONE(*cp 2002 Pure/library.ML FIXXXME take AList.lookup*)
330 | assoc ((keyi, xi) :: pairs, key) =
331 if key = keyi then SOME xi else assoc (pairs, key);
332 (*association list lookup, optimized version for strings*)
333 fun assoc_string ([], (key:string)) = NONE
334 | assoc_string ((keyi, xi) :: pairs, key) =
335 if key = keyi then SOME xi else assoc_string (pairs, key);
336 fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)
337 | if_none (SOME x) _ = x;
339 (* redirect tracing, following The Isabelle Cookbook *)
340 (* TODO: how redirect tracing to emacs buffer again ?
343 fun strip ("\^A" :: _ :: cs) = strip cs
344 | strip (c :: cs) = c :: strip cs
347 implode o strip o Symbol.explode
350 Output.tracing_fn := (fn s =>
351 (TextIO.output (stream, (strip_specials s));
352 TextIO.output (stream, "\n");
353 TextIO.flushOut stream));
354 fun redirect_tracing path = redir (TextIO.openOut path);
357 fun compare_strs str1 str2 =
358 let fun comp_char (c1, c2) =
359 tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^
361 in map comp_char ((Symbol.explode str1) ~~ (Symbol.explode str2)) end;
363 fun triple2pair (a, b, c) = (a, b);
364 fun quad2pair (a, b, c, d) = (a, b);
366 (* append a counter to a string list *)
367 fun enumerate_strings strs =
368 let fun enum _ [] = []
369 | enum i (s :: ss) = (s ^ "--" ^ string_of_int i) :: (enum (i + 1) ss)