equal
deleted
inserted
replaced
18 val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
18 val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
19 val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
19 val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
20 val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
20 val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
21 val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq |
21 val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq |
22 val nat_seq : int Seq.seq |
22 val nat_seq : int Seq.seq |
23 val nth_of_seq : int -> 'a Seq.seq -> 'a Library.option |
23 val nth_of_seq : int -> 'a Seq.seq -> 'a option |
24 val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq |
24 val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq |
25 val seq_is_empty : 'a Seq.seq -> bool |
25 val seq_is_empty : 'a Seq.seq -> bool |
26 val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq |
26 val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq |
27 |
27 |
28 (* lists *) |
28 (* lists *) |
49 val str_indent : string -> string |
49 val str_indent : string -> string |
50 val string_of_intlist : int list -> string |
50 val string_of_intlist : int list -> string |
51 val string_of_list : ('a -> string) -> 'a list -> string |
51 val string_of_list : ('a -> string) -> 'a list -> string |
52 |
52 |
53 (* options *) |
53 (* options *) |
54 val aptosome : 'a Library.option -> ('a -> 'b) -> 'b Library.option |
54 val aptosome : 'a option -> ('a -> 'b) -> 'b option |
55 val seq_mapfilter : ('a -> 'b Library.option) -> 'a Seq.seq -> 'b Seq.seq |
55 val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq |
56 val seq_map_to_some_filter : ('a -> 'b) -> 'a Library.option Seq.seq |
56 val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq |
57 -> 'b Seq.seq |
57 -> 'b Seq.seq |
58 end; |
58 end; |
59 |
59 |
60 |
60 |
61 |
61 |
68 (* Seq *) |
68 (* Seq *) |
69 fun seq_map_to_some_filter f s0 = |
69 fun seq_map_to_some_filter f s0 = |
70 let |
70 let |
71 fun recf s () = |
71 fun recf s () = |
72 case (Seq.pull s) of |
72 case (Seq.pull s) of |
73 None => None |
73 NONE => NONE |
74 | Some (None,s') => recf s' () |
74 | SOME (NONE,s') => recf s' () |
75 | Some (Some d, s') => |
75 | SOME (SOME d, s') => |
76 Some (f d, Seq.make (recf s')) |
76 SOME (f d, Seq.make (recf s')) |
77 in Seq.make (recf s0) end; |
77 in Seq.make (recf s0) end; |
78 |
78 |
79 fun seq_mapfilter f s0 = |
79 fun seq_mapfilter f s0 = |
80 let |
80 let |
81 fun recf s () = |
81 fun recf s () = |
82 case (Seq.pull s) of |
82 case (Seq.pull s) of |
83 None => None |
83 NONE => NONE |
84 | Some (a,s') => |
84 | SOME (a,s') => |
85 (case f a of None => recf s' () |
85 (case f a of NONE => recf s' () |
86 | Some b => Some (b, Seq.make (recf s'))) |
86 | SOME b => SOME (b, Seq.make (recf s'))) |
87 in Seq.make (recf s0) end; |
87 in Seq.make (recf s0) end; |
88 |
88 |
89 |
89 |
90 |
90 |
91 (* a simple function to pair with each element of a list, a number *) |
91 (* a simple function to pair with each element of a list, a number *) |
96 (* check to see if a sequence is empty *) |
96 (* check to see if a sequence is empty *) |
97 fun seq_is_empty s = is_none (Seq.pull s); |
97 fun seq_is_empty s = is_none (Seq.pull s); |
98 |
98 |
99 (* the sequence of natural numbers *) |
99 (* the sequence of natural numbers *) |
100 val nat_seq = |
100 val nat_seq = |
101 let fun nseq i () = Some (i, Seq.make (nseq (i+1))) |
101 let fun nseq i () = SOME (i, Seq.make (nseq (i+1))) |
102 in Seq.make (nseq 1) |
102 in Seq.make (nseq 1) |
103 end; |
103 end; |
104 |
104 |
105 (* create a sequence of pairs of the elements of the two sequences |
105 (* create a sequence of pairs of the elements of the two sequences |
106 If one sequence becomes empty, then so does the pairing of them. |
106 If one sequence becomes empty, then so does the pairing of them. |
117 *) |
117 *) |
118 fun pair_seq seq1 seq2 = |
118 fun pair_seq seq1 seq2 = |
119 let |
119 let |
120 fun pseq s1 s2 () = |
120 fun pseq s1 s2 () = |
121 case Seq.pull s1 of |
121 case Seq.pull s1 of |
122 None => None |
122 NONE => NONE |
123 | Some (s1h, s1t) => |
123 | SOME (s1h, s1t) => |
124 case Seq.pull s2 of |
124 case Seq.pull s2 of |
125 None => None |
125 NONE => NONE |
126 | Some (s2h, s2t) => |
126 | SOME (s2h, s2t) => |
127 Some ((s1h, s2h), Seq.make (pseq s1t s2t)) |
127 SOME ((s1h, s2h), Seq.make (pseq s1t s2t)) |
128 in |
128 in |
129 Seq.make (pseq seq1 seq2) |
129 Seq.make (pseq seq1 seq2) |
130 end; |
130 end; |
131 |
131 |
132 (* number a sequence *) |
132 (* number a sequence *) |
135 (* cuts off the last element of a sequence *) |
135 (* cuts off the last element of a sequence *) |
136 fun all_but_last_of_seq s = |
136 fun all_but_last_of_seq s = |
137 let |
137 let |
138 fun f () = |
138 fun f () = |
139 case Seq.pull s of |
139 case Seq.pull s of |
140 None => None |
140 NONE => NONE |
141 | Some (a, s2) => |
141 | SOME (a, s2) => |
142 (case Seq.pull s2 of |
142 (case Seq.pull s2 of |
143 None => None |
143 NONE => NONE |
144 | Some (a2,s3) => |
144 | SOME (a2,s3) => |
145 Some (a, all_but_last_of_seq (Seq.cons (a2,s3)))) |
145 SOME (a, all_but_last_of_seq (Seq.cons (a2,s3)))) |
146 in |
146 in |
147 Seq.make f |
147 Seq.make f |
148 end; |
148 end; |
149 |
149 |
150 fun ALL_BUT_LAST r st = all_but_last_of_seq (r st); |
150 fun ALL_BUT_LAST r st = all_but_last_of_seq (r st); |
151 |
151 |
152 |
152 |
153 (* nth elem for sequenes, return none if out of bounds *) |
153 (* nth elem for sequenes, return none if out of bounds *) |
154 fun nth_of_seq i l = |
154 fun nth_of_seq i l = |
155 if (seq_is_empty l) then None |
155 if (seq_is_empty l) then NONE |
156 else if i <= 1 then Some (Seq.hd l) |
156 else if i <= 1 then SOME (Seq.hd l) |
157 else nth_of_seq (i-1) (Seq.tl l); |
157 else nth_of_seq (i-1) (Seq.tl l); |
158 |
158 |
159 (* for use with tactics... gives no_tac if element isn't there *) |
159 (* for use with tactics... gives no_tac if element isn't there *) |
160 fun NTH n f st = |
160 fun NTH n f st = |
161 let val r = nth_of_seq n (f st) in |
161 let val r = nth_of_seq n (f st) in |
288 |
288 |
289 val string_of_intlist = string_of_list string_of_int; |
289 val string_of_intlist = string_of_list string_of_int; |
290 |
290 |
291 |
291 |
292 (* options *) |
292 (* options *) |
293 fun aptosome None f = None |
293 fun aptosome NONE f = NONE |
294 | aptosome (Some x) f = Some (f x); |
294 | aptosome (SOME x) f = SOME (f x); |
295 |
295 |
296 end; |
296 end; |