annotate lib/ur/option.ur @ 1272:56bd4a4f6e66
Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
| author |
Adam Chlipala <adamc@hcoop.net> |
| date |
Thu, 03 Jun 2010 13:04:37 -0400 |
| parents |
757dbac0454d |
| children |
a99b743a3087 |
| rev |
line source |
|
adamc@841
|
1 datatype t = datatype Basis.option
|
|
adamc@841
|
2
|
|
adamc@846
|
3 fun eq [a] (_ : eq a) =
|
|
adamc@846
|
4 mkEq (fn x y =>
|
|
adamc@846
|
5 case (x, y) of
|
|
adamc@846
|
6 (None, None) => True
|
|
adamc@846
|
7 | (Some x, Some y) => x = y
|
|
adamc@846
|
8 | _ => False)
|
|
adamc@846
|
9
|
|
adamc@961
|
10 fun ord [a] (_ : ord a) =
|
|
adamc@961
|
11 mkOrd {Lt = fn x y =>
|
|
adamc@961
|
12 case (x, y) of
|
|
adamc@961
|
13 (None, Some _) => True
|
|
adamc@961
|
14 | (Some x, Some y) => x < y
|
|
adamc@961
|
15 | _ => False,
|
|
adamc@961
|
16 Le = fn x y =>
|
|
adamc@961
|
17 case (x, y) of
|
|
adamc@961
|
18 (None, _) => True
|
|
adamc@961
|
19 | (Some x, Some y) => x <= y
|
|
adamc@961
|
20 | _ => False}
|
|
adamc@961
|
21
|
|
adamc@944
|
22 fun isNone [a] x =
|
|
adamc@944
|
23 case x of
|
|
adamc@944
|
24 None => True
|
|
adamc@944
|
25 | Some _ => False
|
|
adamc@944
|
26
|
|
adamc@841
|
27 fun isSome [a] x =
|
|
adamc@841
|
28 case x of
|
|
adamc@841
|
29 None => False
|
|
adamc@841
|
30 | Some _ => True
|
|
adamc@844
|
31
|
|
adamc@844
|
32 fun mp [a] [b] f x =
|
|
adamc@844
|
33 case x of
|
|
adamc@844
|
34 None => None
|
|
adamc@844
|
35 | Some y => Some (f y)
|
|
adamc@846
|
36
|
|
adamc@846
|
37 fun bind [a] [b] f x =
|
|
adamc@846
|
38 case x of
|
|
adamc@846
|
39 None => None
|
|
adamc@846
|
40 | Some y => f y
|
|
adamc@1068
|
41
|
|
adamc@1068
|
42 fun get [a] (x : a) (o : option a) =
|
|
adamc@1068
|
43 case o of
|
|
adamc@1068
|
44 None => x
|
|
adamc@1068
|
45 | Some v => v
|
