annotate lib/ur/option.ur @ 1824:216e92b39fc1
Paranoid inlining prevention for FFI types at the Core level; less paranoid inlining promotion for passive values at the Mono level
author |
Adam Chlipala <adam@chlipala.net> |
date |
Wed, 19 Sep 2012 18:01:22 -0400 |
parents |
a99b743a3087 |
children |
36428d853c97 |
rev |
line source |
adamc@841
|
1 datatype t = datatype Basis.option
|
adamc@841
|
2
|
adam@1544
|
3 val monad = mkMonad {Return = @@Some,
|
adam@1544
|
4 Bind = fn [a] [b] (m1 : t a) (m2 : a -> t b) =>
|
adam@1544
|
5 case m1 of
|
adam@1544
|
6 None => None
|
adam@1544
|
7 | Some v => m2 v}
|
adam@1544
|
8
|
adamc@846
|
9 fun eq [a] (_ : eq a) =
|
adamc@846
|
10 mkEq (fn x y =>
|
adamc@846
|
11 case (x, y) of
|
adamc@846
|
12 (None, None) => True
|
adamc@846
|
13 | (Some x, Some y) => x = y
|
adamc@846
|
14 | _ => False)
|
adamc@846
|
15
|
adamc@961
|
16 fun ord [a] (_ : ord a) =
|
adamc@961
|
17 mkOrd {Lt = fn x y =>
|
adamc@961
|
18 case (x, y) of
|
adamc@961
|
19 (None, Some _) => True
|
adamc@961
|
20 | (Some x, Some y) => x < y
|
adamc@961
|
21 | _ => False,
|
adamc@961
|
22 Le = fn x y =>
|
adamc@961
|
23 case (x, y) of
|
adamc@961
|
24 (None, _) => True
|
adamc@961
|
25 | (Some x, Some y) => x <= y
|
adamc@961
|
26 | _ => False}
|
adamc@961
|
27
|
adamc@944
|
28 fun isNone [a] x =
|
adamc@944
|
29 case x of
|
adamc@944
|
30 None => True
|
adamc@944
|
31 | Some _ => False
|
adamc@944
|
32
|
adamc@841
|
33 fun isSome [a] x =
|
adamc@841
|
34 case x of
|
adamc@841
|
35 None => False
|
adamc@841
|
36 | Some _ => True
|
adamc@844
|
37
|
adamc@844
|
38 fun mp [a] [b] f x =
|
adamc@844
|
39 case x of
|
adamc@844
|
40 None => None
|
adamc@844
|
41 | Some y => Some (f y)
|
adamc@846
|
42
|
adamc@846
|
43 fun bind [a] [b] f x =
|
adamc@846
|
44 case x of
|
adamc@846
|
45 None => None
|
adamc@846
|
46 | Some y => f y
|
adamc@1068
|
47
|
adamc@1068
|
48 fun get [a] (x : a) (o : option a) =
|
adamc@1068
|
49 case o of
|
adamc@1068
|
50 None => x
|
adamc@1068
|
51 | Some v => v
|