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

Implemented proper congruence closure, to the point where tests/policy works

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 08 Apr 2010 12:46:21 -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

Mercurial > urweb