1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
// ####################################################################
/// Various utility functions
///
/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
// ####################################################################
module Utils
// -------------------------------------------
// ----------- collection util funcs ---------
// -------------------------------------------
// =====================================
/// requres: x = Some(a) or failswith msg
/// ensures: ret = a
// =====================================
let ExtractOptionMsg msg x =
match x with
| Some(a) -> a
| None -> failwith msg
// ====================
/// requres: x = Some(a)
/// ensures: ret = a
// ====================
let ExtractOption x =
ExtractOptionMsg "can't extract anything from a None" x
// ==========================================================
/// requres: List.length lst <= 1, otherwise fails with errMsg
/// ensures: if |lst| = 0 then
/// ret = None
/// else
/// ret = Some(lst[0])
// ==========================================================
let ListToOptionMsg lst errMsg =
if List.length lst > 1 then
failwith errMsg
if List.isEmpty lst then
None
else
Some(lst.[0])
let ListToOption lst = ListToOptionMsg lst "given list contains more than one element"
// =============================================================
/// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])
// =============================================================
let rec ConvertToOptionList lst =
match lst with
| fs :: rest -> Some(fs) :: ConvertToOptionList rest
| [] -> []
// =========================================================
/// requres: Seq.length seq <= 1, otherwise fails with errMsg
/// ensures: if |seq| = 0 then
/// ret = None
/// else
/// ret = Some(seq[0])
// =========================================================
let SeqToOptionMsg seq errMsg =
if Seq.length seq > 1 then
failwith errMsg
if Seq.isEmpty seq then
None
else
Some(Seq.nth 0 seq)
let SeqToOption seq = SeqToOptionMsg seq "given seq contains more than one element"
// =========================================================
/// requires: Set.count set <= 1, otherwise fails with errMsg
/// ensures: if |set| = 0 then
/// ret = None
/// else
/// ret = Some(set[0])
// =========================================================
let SetToOptionMsg set errMsg =
if Set.count set > 1 then
failwith errMsg
if (Set.isEmpty set) then
None
else
Some(set |> Set.toList |> List.head)
let SetToOption set = SetToOptionMsg set "give set contains more than one value"
// ============================================================
/// requires: n >= 0
/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = e
// ============================================================
let rec GenList n e =
if n < 0 then
failwith "n must be positive"
if n = 0 then
[]
else
e :: (GenList (n-1) e)
// ==========================
/// ensures: ret = elem in lst
// ==========================
let ListContains elem lst =
lst |> List.exists (fun e -> e = elem)
// ===============================================================
/// ensures: |ret| = max(|lst| - cnt, 0)
/// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]
// ===============================================================
let rec ListSkip cnt lst =
if cnt = 0 then
lst
else
match lst with
| fs :: rest -> ListSkip (cnt-1) rest
| [] -> []
// ===============================================================
/// ensures: forall i :: 0 <= i < max(|srcList|, |dstList|) ==>
/// if i = idx then
/// ret[i] = v
/// elif i < |srcList| then
/// ret[i] = srcList[i]
/// else
/// ret[i] = dstList[i]
// ===============================================================
let rec ListBuild srcList idx v dstList =
match srcList, dstList with
| fs1 :: rest1, fs2 :: rest2 -> if idx = 0 then
v :: List.concat [rest1 ; ListSkip (List.length rest1) rest2]
else
fs1 :: ListBuild rest1 (idx-1) v rest2
| [], fs2 :: rest2 -> if idx = 0 then
v :: rest2
else
fs2 :: ListBuild [] (idx-1) v rest2
| _, [] -> failwith "index out of range"
// =======================================
/// ensures: forall i :: 0 <= i < |lst| ==>
/// if i = idx then
/// ret[i] = v
/// else
/// ret[i] = lst[i]
// =======================================
let rec ListSet idx v lst =
match lst with
| fs :: rest -> if idx = 0 then
v :: rest
else
fs :: ListSet (idx-1) v rest
| [] -> failwith "index out of range"
// =======================================
/// ensures: forall k,v ::
/// if k,v in map2 then
// k,v in ret
/// elif k,v in map1 then
/// k,v in ret
/// else
/// k,v !in ret
// =======================================
let rec MapAddAll map1 map2 =
map2 |> Map.fold (fun acc k v -> acc |> Map.add k v) map1
// -------------------------------------------
// ------ string active patterns -------------
// -------------------------------------------
let (|Prefix|_|) (p:string) (s:string) =
if s.StartsWith(p) then
Some(s.Substring(p.Length))
else
None
let (|Exact|_|) (p:string) (s:string) =
if s = p then
Some(s)
else
None
// -------------------------------------------
// ----------------- random ------------------
// -------------------------------------------
let IfDo1 cond func1 a =
if cond then
func1 a
else
a
let IfDo2 cond func2 (a1,a2) =
if cond then
func2 a1 a2
else
a1,a2
|
