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
|
/// 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
/// ensures: if |lst| = 0 then
/// ret = None
/// else
/// ret = Some(lst[0])
// =============================
let ListToOption lst =
if List.length lst > 1 then
failwith "given list contains more than one element"
if List.isEmpty lst then
None
else
Some(lst.[0])
// =============================================================
/// 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
/// ensures: if |seq| = 0 then
/// ret = None
/// else
/// ret = Some(seq[0])
// =============================
let SeqToOption seq =
if Seq.length seq > 1 then
failwith "given seq contains more than one element"
if Seq.isEmpty seq then
None
else
Some(Seq.nth 0 seq)
// =============================
/// requires: Set.count set <= 1
/// ensures: if |set| = 0 then
/// ret = None
/// else
/// ret = Some(set[0])
// =============================
let SetToOption set =
if Set.count set > 1 then
failwith "give set contains more than one value"
if (Set.isEmpty set) then
None
else
Some(set |> Set.toList |> List.head)
// ===============================================================
/// requires: n >= 0
/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = None
// ===============================================================
let rec GenList n =
if n < 0 then
failwith "n must be positive"
if n = 0 then
[]
else
None :: (GenList (n-1))
// ==========================
/// 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
|
