Ur/Web: lib/ur/option.ur annotate

Be more conservative in choosing candidates for Especialize, re: mutual recursion

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 17 May 2012 10:20:24 -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

Mercurial > urweb