Mercurial > urweb
annotate lib/ur/option.ur @ 1734:d2b3fada532e
Fix generation of normal datatypes from polymorphic variants
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 29 Apr 2012 20:37:45 -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 |