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