author | wenzelm |
Tue, 14 Jun 2005 22:08:53 +0200 | |
changeset 16392 | 7212040b71f2 |
parent 16179 | fa7e70be26b0 |
child 17796 | 86daafee72d6 |
permissions | -rw-r--r-- |
15481 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
16179 | 2 |
(* Title: Pure/IsaPlanner/isaplib.ML |
3 |
ID: $Id$ |
|
15481 | 4 |
Author: Lucas Dixon, University of Edinburgh |
5 |
lucasd@dai.ed.ac.uk |
|
6 |
*) |
|
7 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
8 |
(* DESCRIPTION: |
|
9 |
||
10 |
A few useful system-independent utilities. |
|
11 |
*) |
|
12 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
13 |
signature ISAP_LIB = |
|
14 |
sig |
|
15 |
(* ints *) |
|
16 |
val max : int * int -> int |
|
17 |
||
18 |
(* seq operations *) |
|
19 |
val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
|
20 |
val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
|
21 |
val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
|
22 |
val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq |
|
23 |
val nat_seq : int Seq.seq |
|
15531 | 24 |
val nth_of_seq : int -> 'a Seq.seq -> 'a option |
15481 | 25 |
val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq |
26 |
val seq_is_empty : 'a Seq.seq -> bool |
|
27 |
val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq |
|
28 |
||
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
29 |
datatype 'a skipseqT = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
30 |
skipmore of int |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
31 |
| skipseq of 'a Seq.seq Seq.seq; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
32 |
val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
33 |
val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
34 |
|
15481 | 35 |
(* lists *) |
36 |
val mk_num_list : int -> int list |
|
37 |
val number_list : int -> 'a list -> (int * 'a) list |
|
38 |
val repeated_list : int -> 'a -> 'a list |
|
39 |
val all_pairs : 'a list -> 'b list -> ('a * 'b) list |
|
40 |
val get_ends_of : ('a * 'a -> bool) -> |
|
41 |
('a * 'a) -> 'a list -> ('a * 'a) |
|
42 |
val flatmap : ('a -> 'b list) -> 'a list -> 'b list |
|
43 |
||
44 |
val lrem : ('a * 'b -> bool) -> 'a list -> 'b list -> 'b list |
|
45 |
val forall_list : ('a -> bool) -> 'a list -> bool |
|
46 |
||
47 |
(* the list of lists with one of each of the original sublists *) |
|
48 |
val one_of_each : 'a list list -> 'a list list |
|
49 |
||
50 |
(* type changing *) |
|
51 |
exception NOT_A_DIGIT of string |
|
52 |
val int_of_string : string -> int |
|
53 |
||
54 |
(* string manipulations *) |
|
55 |
val remove_end_spaces : string -> string |
|
56 |
val str_indent : string -> string |
|
57 |
val string_of_intlist : int list -> string |
|
58 |
val string_of_list : ('a -> string) -> 'a list -> string |
|
59 |
||
60 |
(* options *) |
|
15531 | 61 |
val aptosome : 'a option -> ('a -> 'b) -> 'b option |
62 |
val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq |
|
63 |
val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq |
|
15481 | 64 |
-> 'b Seq.seq |
65 |
end; |
|
66 |
||
67 |
||
68 |
||
69 |
structure IsaPLib :> ISAP_LIB = |
|
70 |
struct |
|
71 |
||
72 |
(* Int *) |
|
73 |
fun max (x,y) = if x > y then x else y; |
|
74 |
||
75 |
(* Seq *) |
|
76 |
fun seq_map_to_some_filter f s0 = |
|
77 |
let |
|
78 |
fun recf s () = |
|
79 |
case (Seq.pull s) of |
|
15531 | 80 |
NONE => NONE |
81 |
| SOME (NONE,s') => recf s' () |
|
82 |
| SOME (SOME d, s') => |
|
83 |
SOME (f d, Seq.make (recf s')) |
|
15481 | 84 |
in Seq.make (recf s0) end; |
85 |
||
86 |
fun seq_mapfilter f s0 = |
|
87 |
let |
|
88 |
fun recf s () = |
|
89 |
case (Seq.pull s) of |
|
15531 | 90 |
NONE => NONE |
91 |
| SOME (a,s') => |
|
92 |
(case f a of NONE => recf s' () |
|
93 |
| SOME b => SOME (b, Seq.make (recf s'))) |
|
15481 | 94 |
in Seq.make (recf s0) end; |
95 |
||
96 |
||
97 |
||
98 |
(* a simple function to pair with each element of a list, a number *) |
|
99 |
fun number_list i [] = [] |
|
100 |
| number_list i (h::t) = |
|
101 |
(i,h)::(number_list (i+1) t) |
|
102 |
||
103 |
(* check to see if a sequence is empty *) |
|
104 |
fun seq_is_empty s = is_none (Seq.pull s); |
|
105 |
||
106 |
(* the sequence of natural numbers *) |
|
107 |
val nat_seq = |
|
15531 | 108 |
let fun nseq i () = SOME (i, Seq.make (nseq (i+1))) |
15481 | 109 |
in Seq.make (nseq 1) |
110 |
end; |
|
111 |
||
112 |
(* create a sequence of pairs of the elements of the two sequences |
|
113 |
If one sequence becomes empty, then so does the pairing of them. |
|
114 |
||
115 |
This is particularly useful if you wish to perform counting or |
|
116 |
other repeated operations on a sequence and you want to combvine |
|
117 |
this infinite sequence with a possibly finite one. |
|
118 |
||
119 |
behaviour: |
|
120 |
s1: a1, a2, ... an |
|
121 |
s2: b1, b2, ... bn ... |
|
122 |
||
123 |
pair_seq s1 s2: (a1,b1), (a2,b2), ... (an,bn) |
|
124 |
*) |
|
125 |
fun pair_seq seq1 seq2 = |
|
126 |
let |
|
127 |
fun pseq s1 s2 () = |
|
128 |
case Seq.pull s1 of |
|
15531 | 129 |
NONE => NONE |
130 |
| SOME (s1h, s1t) => |
|
15481 | 131 |
case Seq.pull s2 of |
15531 | 132 |
NONE => NONE |
133 |
| SOME (s2h, s2t) => |
|
134 |
SOME ((s1h, s2h), Seq.make (pseq s1t s2t)) |
|
15481 | 135 |
in |
136 |
Seq.make (pseq seq1 seq2) |
|
137 |
end; |
|
138 |
||
139 |
(* number a sequence *) |
|
140 |
fun number_seq s = pair_seq nat_seq s; |
|
141 |
||
142 |
(* cuts off the last element of a sequence *) |
|
143 |
fun all_but_last_of_seq s = |
|
144 |
let |
|
145 |
fun f () = |
|
146 |
case Seq.pull s of |
|
15531 | 147 |
NONE => NONE |
148 |
| SOME (a, s2) => |
|
15481 | 149 |
(case Seq.pull s2 of |
15531 | 150 |
NONE => NONE |
151 |
| SOME (a2,s3) => |
|
152 |
SOME (a, all_but_last_of_seq (Seq.cons (a2,s3)))) |
|
15481 | 153 |
in |
154 |
Seq.make f |
|
155 |
end; |
|
156 |
||
157 |
fun ALL_BUT_LAST r st = all_but_last_of_seq (r st); |
|
158 |
||
159 |
||
160 |
(* nth elem for sequenes, return none if out of bounds *) |
|
161 |
fun nth_of_seq i l = |
|
15531 | 162 |
if (seq_is_empty l) then NONE |
163 |
else if i <= 1 then SOME (Seq.hd l) |
|
15481 | 164 |
else nth_of_seq (i-1) (Seq.tl l); |
165 |
||
166 |
(* for use with tactics... gives no_tac if element isn't there *) |
|
167 |
fun NTH n f st = |
|
168 |
let val r = nth_of_seq n (f st) in |
|
15570 | 169 |
if (is_none r) then Seq.empty else (Seq.single (valOf r)) |
15481 | 170 |
end; |
171 |
||
172 |
(* First result of a tactic... uses NTH, so if there is no elements, |
|
173 |
||
174 |
then no_tac is returned. *) |
|
175 |
fun FST f = NTH 1 f; |
|
176 |
||
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
177 |
datatype 'a skipseqT = skipmore of int |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
178 |
| skipseq of 'a Seq.seq Seq.seq; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
179 |
(* given a seqseq, skip the first m non-empty seq's *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
180 |
fun skipto_seqseq m s = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
181 |
let |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
182 |
fun skip_occs n sq = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
183 |
case Seq.pull sq of |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
184 |
NONE => skipmore n |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
185 |
| SOME (h,t) => |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
186 |
(case Seq.pull h of NONE => skip_occs n t |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
187 |
| SOME _ => if n <= 1 then skipseq (Seq.cons (h, t)) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
188 |
else skip_occs (n - 1) t) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
189 |
in (skip_occs m s) end; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
190 |
|
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
191 |
(* handy function for re-arranging Sequence operations *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
192 |
(* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
193 |
fun seqflat_seq ss = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
194 |
let |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
195 |
fun pulltl LL () = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
196 |
(case Seq.pull LL of |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
197 |
NONE => NONE |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
198 |
| SOME (hL,tLL) => |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
199 |
(case Seq.pull hL of |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
200 |
NONE => pulltl tLL () |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
201 |
| SOME (h,tL) => |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
202 |
SOME (h, Seq.make (recf (tLL, (Seq.single tL)))))) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
203 |
and recf (fstLL,sndLL) () = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
204 |
(case Seq.pull fstLL of |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
205 |
NONE => pulltl sndLL () |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
206 |
| SOME (hL, tLL) => |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
207 |
(case Seq.pull hL of |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
208 |
NONE => recf (tLL, sndLL) () |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
209 |
| SOME (h,tL) => |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
210 |
SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL)))))) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
211 |
in Seq.make (pulltl ss) end; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
212 |
(* tested with: |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
213 |
val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]]; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
214 |
Seq.list_of (seqflat_seq ss); |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
215 |
val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
216 |
*) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
217 |
|
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
218 |
|
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15570
diff
changeset
|
219 |
|
15481 | 220 |
(* create a list opf the form (n, n-1, n-2, ... ) *) |
221 |
fun mk_num_list n = |
|
222 |
if n < 1 then [] else (n :: (mk_num_list (n-1))); |
|
223 |
||
224 |
fun repeated_list n a = |
|
225 |
if n < 1 then [] else (a :: (repeated_list (n-1) a)); |
|
226 |
||
227 |
(* create all possible pairs with fst element from the first list |
|
228 |
and snd element from teh second list *) |
|
229 |
fun all_pairs xs ys = |
|
230 |
let |
|
231 |
fun all_pairs_aux yss [] _ acc = acc |
|
232 |
| all_pairs_aux yss (x::xs) [] acc = |
|
233 |
all_pairs_aux yss xs yss acc |
|
234 |
| all_pairs_aux yss (xs as (x1::x1s)) (y::ys) acc = |
|
235 |
all_pairs_aux yss xs ys ((x1,y)::acc) |
|
236 |
in |
|
237 |
all_pairs_aux ys xs ys [] |
|
238 |
end; |
|
239 |
||
240 |
||
241 |
(* create all possible pairs with fst element from the first list |
|
242 |
and snd element from teh second list *) |
|
243 |
(* FIXME: make tail recursive and quick *) |
|
244 |
fun one_of_each [] = [] |
|
245 |
| one_of_each [[]] = [] |
|
246 |
| one_of_each [(h::t)] = [h] :: (one_of_each [t]) |
|
247 |
| one_of_each ([] :: xs) = [] |
|
248 |
| one_of_each ((h :: t) :: xs) = |
|
249 |
(map (fn z => h :: z) (one_of_each xs)) |
|
250 |
@ (one_of_each (t :: xs)); |
|
251 |
||
252 |
||
253 |
(* function to get the upper/lower bounds of a list |
|
254 |
given: |
|
255 |
gr : 'a * 'a -> bool = greater than check |
|
256 |
e as (u,l) : ('a * 'a) = upper and lower bits |
|
257 |
l : 'a list = the list to get the upper and lower bounds of |
|
258 |
returns a pair ('a * 'a) of the biggest and lowest value w.r.t "gr" |
|
259 |
*) |
|
260 |
fun get_ends_of gr (e as (u,l)) [] = e |
|
261 |
| get_ends_of gr (e as (u,l)) (h :: t) = |
|
262 |
if gr(h,u) then get_ends_of gr (h,l) t |
|
263 |
else if gr(l,h) then get_ends_of gr (u,h) t |
|
264 |
else get_ends_of gr (u,l) t; |
|
265 |
||
15570 | 266 |
fun flatmap f = List.concat o map f; |
15481 | 267 |
|
268 |
(* quick removal of "rs" elements from "ls" when (eqf (r,l)) is true |
|
269 |
Ignores ordering. *) |
|
270 |
fun lrem eqf rs ls = |
|
271 |
let fun list_remove rs ([],[]) = [] |
|
272 |
| list_remove [] (xs,_) = xs |
|
273 |
| list_remove (r::rs) ([],leftovers) = |
|
274 |
list_remove rs (leftovers,[]) |
|
275 |
| list_remove (r1::rs) ((x::xs),leftovers) = |
|
276 |
if eqf (r1, x) then list_remove (r1::rs) (xs,leftovers) |
|
277 |
else list_remove (r1::rs) (xs, x::leftovers) |
|
278 |
in |
|
279 |
list_remove rs (ls,[]) |
|
280 |
end; |
|
281 |
||
282 |
fun forall_list f [] = true |
|
283 |
| forall_list f (a::t) = f a orelse forall_list f t; |
|
284 |
||
285 |
||
286 |
(* crappy string indeter *) |
|
287 |
fun str_indent s = |
|
288 |
implode (map (fn s => if s = "\n" then "\n " else s) (explode s)); |
|
289 |
||
290 |
||
291 |
fun remove_end_spaces s = |
|
292 |
let |
|
293 |
fun rem_starts [] = [] |
|
294 |
| rem_starts (" " :: t) = rem_starts t |
|
295 |
| rem_starts ("\t" :: t) = rem_starts t |
|
296 |
| rem_starts ("\n" :: t) = rem_starts t |
|
297 |
| rem_starts l = l |
|
298 |
fun rem_ends l = rev (rem_starts (rev l)) |
|
299 |
in |
|
300 |
implode (rem_ends (rem_starts (explode s))) |
|
301 |
end; |
|
302 |
||
303 |
(* convert a string to an integer *) |
|
304 |
exception NOT_A_DIGIT of string; |
|
305 |
||
306 |
fun int_of_string s = |
|
307 |
let |
|
308 |
fun digits_to_int [] x = x |
|
309 |
| digits_to_int (h :: t) x = digits_to_int t (x * 10 + h); |
|
310 |
||
311 |
fun char_to_digit c = |
|
312 |
case c of |
|
313 |
"0" => 0 |
|
314 |
| "1" => 1 |
|
315 |
| "2" => 2 |
|
316 |
| "3" => 3 |
|
317 |
| "4" => 4 |
|
318 |
| "5" => 5 |
|
319 |
| "6" => 6 |
|
320 |
| "7" => 7 |
|
321 |
| "8" => 8 |
|
322 |
| "9" => 9 |
|
323 |
| _ => raise NOT_A_DIGIT c |
|
324 |
in |
|
325 |
digits_to_int (map char_to_digit (explode (remove_end_spaces s))) 0 |
|
326 |
end; |
|
327 |
||
328 |
(* Debugging/printing code for this datatype *) |
|
329 |
fun string_of_list f l = |
|
330 |
let |
|
331 |
fun auxf [] = "" |
|
332 |
| auxf [a] = (f a) |
|
333 |
| auxf (h :: (t as (h2 :: t2))) = (f h) ^ ", " ^ (auxf t) |
|
334 |
in |
|
335 |
"[" ^ (auxf l) ^ "]" |
|
336 |
end; |
|
337 |
||
338 |
val string_of_intlist = string_of_list string_of_int; |
|
339 |
||
340 |
||
341 |
(* options *) |
|
15531 | 342 |
fun aptosome NONE f = NONE |
343 |
| aptosome (SOME x) f = SOME (f x); |
|
15481 | 344 |
|
345 |
end; |