neuper@37906
|
1 |
(* use"library.sml";
|
neuper@37906
|
2 |
WN.22.10.99
|
neuper@37906
|
3 |
for both, math-engine and isa-98-1-HOL-plus
|
neuper@37906
|
4 |
however, functions closely related to original isabelle-98-1 functions
|
neuper@37906
|
5 |
are in isa-98-1-HOL-plus/rewrite-parse/library_G
|
neuper@37906
|
6 |
*)
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
(* Isabelle2002 -> Isabelle2009 library changed:
|
neuper@37906
|
9 |
signature LIBRARY =
|
neuper@37906
|
10 |
sig
|
neuper@37906
|
11 |
include BASIC_LIBRARY
|
neuper@37906
|
12 |
val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
|
neuper@37906
|
13 |
val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
|
neuper@37906
|
14 |
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
|
neuper@37906
|
15 |
val take: int * 'a list -> 'a list
|
neuper@37906
|
16 |
val drop: int * 'a list -> 'a list
|
neuper@37906
|
17 |
val last_elem: 'a list -> 'a
|
neuper@37906
|
18 |
end;
|
neuper@37906
|
19 |
FIXME: overwritten again...*)
|
neuper@37906
|
20 |
fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = (*FIXME.2009*)
|
neuper@37906
|
21 |
let fun itl (e, []) = e
|
neuper@37906
|
22 |
| itl (e, a::l) = itl (f(e, a), l)
|
neuper@37906
|
23 |
in itl end;
|
neuper@37906
|
24 |
fun foldr f (l, e) = (*FIXME.2009*)
|
neuper@37906
|
25 |
let fun itr [] = e
|
neuper@37906
|
26 |
| itr (a::l) = f(a, itr l)
|
neuper@37906
|
27 |
in itr l end;
|
neuper@37906
|
28 |
fun take (n, []) = [] (*FIXME.2009*)
|
neuper@37906
|
29 |
| take (n, x :: xs) =
|
neuper@37906
|
30 |
if n > 0 then x :: take (n - 1, xs) else [];
|
neuper@37906
|
31 |
fun drop (n, []) = [] (*FIXME.2009*)
|
neuper@37906
|
32 |
| drop (n, x :: xs) =
|
neuper@37906
|
33 |
if n > 0 then drop (n - 1, xs) else x :: xs;
|
neuper@38011
|
34 |
|
neuper@37906
|
35 |
(*exn LIST has disappeared in 2009 ... replaced by error...*)
|
neuper@38031
|
36 |
fun last_elem [] = error "last_elem" (*FIXME.2009*)
|
neuper@37906
|
37 |
| last_elem [x] = x
|
neuper@37906
|
38 |
| last_elem (_ :: xs) = last_elem xs;
|
neuper@37906
|
39 |
|
neuper@37906
|
40 |
fun gen_mem eq (x, []) = false (*FIXME.2009*)
|
neuper@37906
|
41 |
| gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
|
neuper@37906
|
42 |
fun gen_insert (les : 'a * 'a -> bool) ([], a) = [a]
|
neuper@37906
|
43 |
| gen_insert les (x::xs, a) = if les (x, a) then x::(gen_insert les (xs, a))
|
neuper@37906
|
44 |
else a::x::xs;
|
neuper@37906
|
45 |
fun gen_sort les xs = foldl (gen_insert les) (xs, []);
|
neuper@37906
|
46 |
fun gen_distinct eq lst =
|
neuper@37906
|
47 |
let
|
neuper@37906
|
48 |
val memb = gen_mem eq;
|
neuper@37906
|
49 |
|
neuper@37906
|
50 |
fun dist (rev_seen, []) = rev rev_seen
|
neuper@37906
|
51 |
| dist (rev_seen, x :: xs) =
|
neuper@37906
|
52 |
if memb (x, rev_seen) then dist (rev_seen, xs)
|
neuper@37906
|
53 |
else dist (x :: rev_seen, xs);
|
neuper@37906
|
54 |
in
|
neuper@37906
|
55 |
dist ([], lst)
|
neuper@37906
|
56 |
end;
|
neuper@37906
|
57 |
fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
|
neuper@37906
|
58 |
fun distinct l = gen_distinct (op =) l;
|
neuper@37906
|
59 |
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
(*.see 'fun (y :: ys) \ x' in Pure/library.ML.*)
|
neuper@37906
|
63 |
fun gen_dif eq (y :: ys, x) = if eq (y, x) then ys
|
neuper@37906
|
64 |
else y :: (gen_dif eq (ys, x))
|
neuper@37906
|
65 |
| gen_dif eq ([], x) = [];
|
neuper@37906
|
66 |
(* val (eq, (y :: ys, x)) = ();*)
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
(*.see 'fun ys \\ xs' in Pure/library.ML.*)
|
neuper@37906
|
69 |
fun gen_diff eq (ys, xs) = foldl (gen_dif eq) (ys,xs);
|
neuper@37906
|
70 |
(* val (eq, (ys, xs)) = (eq_thmI, (isacrlsthms, isacthms));
|
neuper@37906
|
71 |
*)
|
neuper@37906
|
72 |
(* gen_diff op= ([1,2,3,4,5,6,7],[2,3,5]);
|
neuper@37906
|
73 |
val it = [1, 4, 6, 7] : int list*)
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
(*an indulgent version of Isabelle/src/Pure/library.ML ~~*)
|
neuper@37906
|
77 |
infix ~~~;
|
neuper@37906
|
78 |
fun xs ~~~ ys =
|
neuper@37906
|
79 |
let fun aaa xys [] [] = xys
|
neuper@37906
|
80 |
| aaa xys [] (y :: ys) = xys
|
neuper@37906
|
81 |
| aaa xys (x :: xs) [] = xys
|
neuper@37906
|
82 |
| aaa xys (x :: xs) (y :: ys) = aaa (xys @ [(x, y)]) xs ys
|
neuper@37906
|
83 |
in aaa [] xs ys end;
|
neuper@37906
|
84 |
(*[1,2,3] ~~~ ["1","2","3"];
|
neuper@37906
|
85 |
val it = [(1, "1"), (2, "2"), (3, "3")] : (int * string) list
|
neuper@37906
|
86 |
> [1,2] ~~~ ["1","2","3"];
|
neuper@37906
|
87 |
val it = [(1, "1"), (2, "2")] : (int * string) list
|
neuper@37906
|
88 |
> [1,2,3] ~~~ ["1","2"];
|
neuper@37906
|
89 |
val it = [(1, "1"), (2, "2")] : (int * string) list*)
|
neuper@37906
|
90 |
|
neuper@37906
|
91 |
(*from Isabelle2002/src/Pure/library.ML; has changed in 2009 FIXME replace*)
|
neuper@37906
|
92 |
fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
|
neuper@37906
|
93 |
fun gen_insI eq pr (x, xs) =
|
neuper@37906
|
94 |
if gen_mem eq (x, xs)
|
neuper@38015
|
95 |
then (tracing ("### occurs twice: "^(pr x)); xs)
|
neuper@37906
|
96 |
else x :: xs;
|
neuper@37906
|
97 |
fun gen_union eq pr (xs, []) = xs
|
neuper@37906
|
98 |
| gen_union eq pr ([], ys) = ys
|
neuper@37906
|
99 |
| gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)
|
neuper@37906
|
102 |
|
neuper@38031
|
103 |
fun nth _ [] = error "nth _ []"
|
neuper@37906
|
104 |
| nth 1 (x::_) = x
|
neuper@37906
|
105 |
| nth n (_::xs) = nth (n-1) xs;
|
neuper@37906
|
106 |
(*WN050106 quick for test: doesn't check for exns*)
|
neuper@37906
|
107 |
fun drop_nth ls (_, []) = ls
|
neuper@37906
|
108 |
| drop_nth ls (n, x :: xs) =
|
neuper@37906
|
109 |
if n = 1
|
neuper@37906
|
110 |
then ls @ xs
|
neuper@37906
|
111 |
else drop_nth (ls @ [x]) (n - 1, xs);
|
neuper@37906
|
112 |
(*> drop_nth [] (3,[1,2,3,4,5]);
|
neuper@37906
|
113 |
val it = [1, 2, 4, 5] : int list
|
neuper@37906
|
114 |
> drop_nth [] (1,[1,2,3,4,5]);
|
neuper@37906
|
115 |
val it = [2, 3, 4, 5] : int list
|
neuper@37906
|
116 |
> drop_nth [] (5,[1,2,3,4,5]);
|
neuper@37906
|
117 |
val it = [1, 2, 3, 4] : int list *)
|
neuper@37906
|
118 |
|
neuper@37906
|
119 |
fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *)
|
neuper@37906
|
120 |
fun or_ (b1,b2) = b1 orelse b2;
|
neuper@37906
|
121 |
|
neuper@37906
|
122 |
|
neuper@37906
|
123 |
fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);
|
neuper@37906
|
124 |
(*> takerest (3, ["normalize","polynomial","univariate","equation"]);
|
neuper@37906
|
125 |
val it = ["equation"] : string list
|
neuper@37906
|
126 |
*)
|
neuper@37906
|
127 |
fun takelast (i, ls) = (rev o take) (i, rev ls);
|
neuper@37906
|
128 |
(* > takelast (2, ["normalize","polynomial","univariate","equation"]);
|
neuper@37906
|
129 |
val it = ["univariate", "equation"] : pblID
|
neuper@37906
|
130 |
> takelast (2, ["equation"]);
|
neuper@37906
|
131 |
val it = ["equation"] : pblID
|
neuper@37906
|
132 |
> takelast (3, ["normalize","polynomial","univariate","equation"]);
|
neuper@37906
|
133 |
val it = ["polynomial", "univariate", "equation"]*)
|
neuper@37906
|
134 |
fun split_nlast (i, ls) =
|
neuper@37906
|
135 |
let val rv = rev ls
|
neuper@37906
|
136 |
in (rev (takelast (i - 1, rv)), rev (take (i, rv))) end;
|
neuper@37906
|
137 |
|
neuper@37906
|
138 |
fun split_nlast (i, ls) = (take (length ls - i, ls), rev (take (i, rev ls)));
|
neuper@37906
|
139 |
(* val (a, b) = split_nlast (3, ["a","b","[",".","]"]);
|
neuper@37906
|
140 |
val a = ["a", "b"] : string list
|
neuper@37906
|
141 |
val b = ["[", ".", "]"] : string list
|
neuper@37906
|
142 |
> val (a, b) = split_nlast (3, [".","]"]);
|
neuper@37906
|
143 |
val a = [] : string list
|
neuper@37906
|
144 |
val b = [".", "]"] : string list *)
|
neuper@37906
|
145 |
|
neuper@37906
|
146 |
(*.analoguous to dropwhile in Pure/libarary.ML.*)
|
neuper@37906
|
147 |
fun dropwhile P [] = []
|
neuper@37906
|
148 |
| dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
|
neuper@37906
|
149 |
fun takewhile col P [] = col
|
neuper@37906
|
150 |
| takewhile col P (ys as x::xs) = if P x then takewhile (col @ [x]) P xs
|
neuper@37906
|
151 |
else col;
|
neuper@37906
|
152 |
(* > takewhile [] (not o (curry op= 4)) [1,2,3,4,5,6,7];
|
neuper@37906
|
153 |
val it = [1, 2, 3] : int list*)
|
neuper@37906
|
154 |
fun dropuntil P [] = []
|
neuper@37906
|
155 |
| dropuntil P (ys as x::xs) = if P x then ys else dropuntil P xs;
|
neuper@37906
|
156 |
|
neuper@37906
|
157 |
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
fun pair2tri ((a,b),c) = (a,b,c);
|
neuper@37906
|
160 |
fun fst3 (a,_,_) = a;
|
neuper@37906
|
161 |
fun snd3 (_,b,_) = b;
|
neuper@37906
|
162 |
fun thd3 (_,_,c) = c;
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
fun skip_blanks strl =
|
neuper@37906
|
165 |
let
|
neuper@37906
|
166 |
fun skip strl [] = strl
|
neuper@37906
|
167 |
| skip strl (" "::ss) = skip strl ss
|
neuper@37906
|
168 |
| skip strl ( s ::ss) = skip (strl @ [s]) ss
|
neuper@37906
|
169 |
in skip [] strl end;
|
neuper@37906
|
170 |
|
neuper@37906
|
171 |
|
neuper@37906
|
172 |
|
neuper@37906
|
173 |
fun de_quote str =
|
neuper@37906
|
174 |
let fun scan ss' [] = ss'
|
neuper@37906
|
175 |
| scan ss' ("\""::ss) = scan ss' ss
|
neuper@37906
|
176 |
| scan ss' (s::ss) = scan (ss' @ [s]) ss;
|
neuper@37906
|
177 |
in (implode o (scan []) o explode) str end;
|
neuper@37906
|
178 |
(*> de_quote "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
|
neuper@37906
|
179 |
val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
|
neuper@37906
|
180 |
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
|
neuper@37906
|
183 |
(* conversions to (quoted) strings
|
neuper@37906
|
184 |
FIXME: rename *2str --> *2strq (quoted elems)
|
neuper@37906
|
185 |
now *2str' (elems NOT quoted) instead of *2str *)
|
neuper@37906
|
186 |
|
neuper@37906
|
187 |
val commas = space_implode ",";
|
neuper@37906
|
188 |
|
neuper@37906
|
189 |
fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]";
|
neuper@38015
|
190 |
(*> val str = strs2str ["123","asd"]; tracing str;
|
neuper@37906
|
191 |
val it = "[\"123\", \"asd\"]" : string
|
neuper@37906
|
192 |
"123", "asd"] *)
|
neuper@37906
|
193 |
fun strs2str' strl = "[" ^ (commas strl) ^ "]";
|
neuper@37906
|
194 |
fun list2str strl = "[" ^ (commas strl) ^ "]";
|
neuper@38015
|
195 |
(*> val str = list2str ["123","asd"]; tracing str;
|
neuper@37906
|
196 |
val str = "[123, asd]" : string
|
neuper@37906
|
197 |
[123, asd] *)
|
neuper@37906
|
198 |
fun spair2str (s1,s2) = "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")";
|
neuper@37906
|
199 |
fun pair2str (s1,s2) = "(" ^ s1 ^ ", " ^ s2 ^ ")";
|
neuper@37906
|
200 |
(*16.11.00
|
neuper@37906
|
201 |
fun subs2str (subs:(string * string) list) =
|
neuper@37906
|
202 |
(list2str o (map pair2str)) subs;*)
|
neuper@37906
|
203 |
fun subs2str (subs: string list) = list2str subs;
|
neuper@37906
|
204 |
(*> val sss = ["(bdv,x)","(err,#0)"];
|
neuper@37906
|
205 |
> subs2str sss;
|
neuper@37906
|
206 |
val it = "[(bdv,x),(err,#0)]" : string*)
|
neuper@37906
|
207 |
fun subs2str' (subs:(string * string) list) = (*12.12.99???*)
|
neuper@37906
|
208 |
(list2str o (map pair2str)) subs;
|
neuper@38015
|
209 |
(*> val subs = subs2str [("bdv","x")]; tracing subs;
|
neuper@37906
|
210 |
val subs = "[(\"bdv\", \"x\")]" : string
|
neuper@37906
|
211 |
[("bdv", "x")] *)
|
neuper@37906
|
212 |
fun con2str land_lor = quote " &| ";
|
neuper@37906
|
213 |
val int2str = string_of_int;
|
neuper@37906
|
214 |
fun ints2str ints = (strs2str o (map string_of_int)) ints;
|
neuper@37906
|
215 |
fun ints2str' ints = (strs2str' o (map string_of_int)) ints;
|
neuper@37906
|
216 |
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
(* use"library.sml";
|
neuper@37906
|
219 |
*)
|
neuper@37906
|
220 |
|
neuper@37906
|
221 |
|
neuper@37906
|
222 |
(*needed in Isa + ME*)
|
neuper@37906
|
223 |
fun get_thy str =
|
neuper@37906
|
224 |
let fun get strl [] = strl
|
neuper@37906
|
225 |
| get strl ("."::ss) = strl
|
neuper@37906
|
226 |
| get strl ( s ::ss) = get (strl @ [s]) ss
|
neuper@37906
|
227 |
in implode( get [] (explode str)) end;
|
neuper@37906
|
228 |
|
neuper@37906
|
229 |
fun strip_thy str =
|
neuper@37906
|
230 |
let fun strip bdVar [] = implode (rev bdVar)
|
neuper@37906
|
231 |
| strip bdVar ("."::_ ) = implode (rev bdVar)
|
neuper@37906
|
232 |
| strip bdVar (c ::cs) = strip (bdVar @[c]) cs
|
neuper@37906
|
233 |
in strip [] (rev(explode str)) end;
|
neuper@37906
|
234 |
|
neuper@37906
|
235 |
fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix)
|
neuper@37906
|
236 |
| id_of (Free (id ,_)) = id
|
neuper@37906
|
237 |
| id_of (Const(id ,_)) = id
|
neuper@37906
|
238 |
| id_of _ = ""; (* never such an identifier *)
|
neuper@37906
|
239 |
|
neuper@37906
|
240 |
fun ids_of t =
|
neuper@37906
|
241 |
let fun con ss (Const (s,_)) = s::ss
|
neuper@37906
|
242 |
| con ss (Free (s,_)) = s::ss
|
neuper@37906
|
243 |
| con ss (Abs (s,_,b)) = s::(con ss b)
|
neuper@37906
|
244 |
| con ss (t1 $ t2) = (con ss t1) @ (con ss t2)
|
neuper@37906
|
245 |
| con ss _ = ss
|
neuper@37906
|
246 |
in map strip_thy ((distinct o (con [])) t) end;
|
neuper@37906
|
247 |
(*
|
neuper@37906
|
248 |
> val t = (term_of o the o (parse thy))
|
neuper@37906
|
249 |
"solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
|
neuper@37906
|
250 |
> ids_of t;
|
neuper@37906
|
251 |
["solve'_univar","Pair","R","Cons","univar","equation","Nil",...]*)
|
neuper@37906
|
252 |
|
neuper@37906
|
253 |
|
neuper@37906
|
254 |
(*FIXME.WN090819 fun overwrite missing in ..2009/../library.ML*)
|
neuper@37906
|
255 |
fun overwrite (al, p as (key, _)) = (*FIXME.2009*)
|
neuper@37906
|
256 |
let fun over ((q as (keyi, _)) :: pairs) =
|
neuper@37906
|
257 |
if keyi = key then p :: pairs else q :: (over pairs)
|
neuper@37906
|
258 |
| over [] = [p]
|
neuper@37906
|
259 |
in over al end;
|
neuper@37906
|
260 |
fun overwritel (al, []) = al
|
neuper@37906
|
261 |
| overwritel (al, b::bl) = overwritel (overwrite (al, b), bl);
|
neuper@37906
|
262 |
(*> val aaa = [(1,11),(2,22),(3,33)];
|
neuper@37906
|
263 |
> overwritel (aaa, [(2,2222),(4,4444)]);
|
neuper@37906
|
264 |
val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*)
|
neuper@37906
|
265 |
|
neuper@37906
|
266 |
|
neuper@37906
|
267 |
local
|
neuper@37906
|
268 |
fun intsto1 0 = []
|
neuper@37906
|
269 |
| intsto1 n = (intsto1 (n-1)) @ [n]
|
neuper@37906
|
270 |
in
|
neuper@38031
|
271 |
fun intsto n = if n < 0 then (error "intsto < 0") else intsto1 n
|
neuper@37906
|
272 |
end;
|
neuper@37906
|
273 |
|
neuper@37906
|
274 |
|
neuper@37906
|
275 |
type 'a stack = 'a list;
|
neuper@37906
|
276 |
fun top ((x::xs):'a stack) = x
|
neuper@38031
|
277 |
| top _ = error "top called for empty list";
|
neuper@37906
|
278 |
fun pop ((x::xs):'a stack) = xs:'a stack
|
neuper@38031
|
279 |
| pop _ = error "pop called for empty list";
|
neuper@37906
|
280 |
fun push x (xs:'a stack) = x::xs:'a stack;
|
neuper@37906
|
281 |
|
neuper@37906
|
282 |
|
neuper@37906
|
283 |
fun drop_last l = ((rev o tl o rev) l);
|
neuper@37906
|
284 |
fun drop_last_n n l = rev (takerest (n, rev l));
|
neuper@37906
|
285 |
(*> drop_last_n 2 [1,2,3,4,5];
|
neuper@37906
|
286 |
val it = [1, 2, 3] : int list
|
neuper@37906
|
287 |
> drop_last_n 3 [1,2,3,4,5];
|
neuper@37906
|
288 |
val it = [1, 2] : int list
|
neuper@37906
|
289 |
> drop_last_n 7 [1,2,3,4,5];
|
neuper@37906
|
290 |
val it = [] : int list
|
neuper@37906
|
291 |
*)
|
neuper@37906
|
292 |
|
neuper@37906
|
293 |
fun bool2str true = "true"
|
neuper@37906
|
294 |
| bool2str false = "false";
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
(*.take elements from b to e including both.*)
|
neuper@37906
|
297 |
fun take_fromto from to l =
|
neuper@38031
|
298 |
if from > to then error ("take_fromto from="^string_of_int from^
|
neuper@37906
|
299 |
" > to="^string_of_int to)
|
neuper@37906
|
300 |
else drop (from - 1, take (to, l));
|
neuper@37906
|
301 |
(*> take_fromto 3 5 [1,2,3,4,5,6,7];
|
neuper@37906
|
302 |
val it = [3,4,5] : int list
|
neuper@37906
|
303 |
> take_fromto 3 3 [1,2,3,4,5,6,7];
|
neuper@37906
|
304 |
val it = [3] : int list*)
|
neuper@37906
|
305 |
|
neuper@37906
|
306 |
|
neuper@37906
|
307 |
fun idt str 0 = " "
|
neuper@37906
|
308 |
| idt str n = str ^ idt str (n-1);
|
neuper@37906
|
309 |
(*fun indt 0 = ""
|
neuper@37906
|
310 |
| indt n = " " ^ indt (n-1);---------does not terminate with negatives*)
|
neuper@37906
|
311 |
fun indt n = if n <= 0 then "" else " " ^ indt (n-1);
|
neuper@37906
|
312 |
fun indent 0 = ""
|
neuper@37906
|
313 |
| indent n = ". " ^ indent(n-1);
|
neuper@37906
|
314 |
|
neuper@37906
|
315 |
fun dashs i = if 0<i then "-"^ dashs (i-1) else "";
|
neuper@37906
|
316 |
fun dots i = if 0<i then "."^ dots (i-1) else "";
|
neuper@37906
|
317 |
|
neuper@37906
|
318 |
fun assoc ([], key) = NONE(*cp 2002 Pure/library.ML FIXXXME take AList.lookup*)
|
neuper@37906
|
319 |
| assoc ((keyi, xi) :: pairs, key) =
|
neuper@37906
|
320 |
if key = keyi then SOME xi else assoc (pairs, key);
|
neuper@37906
|
321 |
(*association list lookup, optimized version for strings*)
|
neuper@37906
|
322 |
fun assoc_string ([], (key:string)) = NONE
|
neuper@37906
|
323 |
| assoc_string ((keyi, xi) :: pairs, key) =
|
neuper@37906
|
324 |
if key = keyi then SOME xi else assoc_string (pairs, key);
|
neuper@37906
|
325 |
fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)
|
neuper@37906
|
326 |
| if_none (SOME x) _ = x;
|
neuper@38022
|
327 |
|
neuper@38022
|
328 |
(* redirect tracing, following The Isabelle Cookbook *)
|
neuper@38022
|
329 |
(* TODO: how redirect tracing to emacs buffer again ? *)
|
neuper@38022
|
330 |
val strip_specials =
|
neuper@38022
|
331 |
let
|
neuper@38022
|
332 |
fun strip ("\^A" :: _ :: cs) = strip cs
|
neuper@38022
|
333 |
| strip (c :: cs) = c :: strip cs
|
neuper@38022
|
334 |
| strip [] = [];
|
neuper@38022
|
335 |
in
|
neuper@38022
|
336 |
implode o strip o explode
|
neuper@38022
|
337 |
end
|
neuper@38022
|
338 |
fun redir stream =
|
neuper@38022
|
339 |
Output.tracing_fn := (fn s =>
|
neuper@38022
|
340 |
(TextIO.output (stream, (strip_specials s));
|
neuper@38022
|
341 |
TextIO.output (stream, "\n");
|
neuper@38022
|
342 |
TextIO.flushOut stream));
|
neuper@38022
|
343 |
fun redirect_tracing path = redir (TextIO.openOut path);
|
neuper@38051
|
344 |
|
neuper@38051
|
345 |
fun compare_strs str1 str2 =
|
neuper@38051
|
346 |
let fun comp_char (c1, c2) =
|
neuper@38051
|
347 |
tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^
|
neuper@38051
|
348 |
bool2str (c1 = c2))
|
neuper@38051
|
349 |
in map comp_char ((explode str1) ~~ (explode str2)) end;
|