Mercurial > urweb

annotate lib/ur/option.ur @ 2194:f6e16c308566

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Return to working version mode
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Nov 2015 10:25:22 -0500
parents 36428d853c97
children
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
mad@1831 52
mad@1831 53 fun unsafeGet [a] (o : option a) =
mad@1831 54 case o of
mad@1831 55 None => error <xml>Option.unsafeGet: encountered None</xml>
mad@1831 56 | Some v => v