Ur/Web: tests/caseMod.ur annotate

Datatype positivity check

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 09 Sep 2008 09:15:00 -0400
parents	71bafe66dbe1
children

rev	line source
adamc@174	1 structure M = struct
adamc@174	2 datatype t = A \| B
adamc@174	3 end
adamc@174	4
adamc@174	5 val f = fn x : M.t => case x of M.A => M.B \| M.B => M.A
adamc@174	6
adamc@174	7 datatype t = datatype M.t
adamc@174	8
adamc@174	9 val g = fn x : t => case x of M.A => B \| B => M.A
adamc@174	10
adamc@174	11 structure N = struct
adamc@177	12 datatype u = C of t \| D
adamc@174	13 end
adamc@174	14
adamc@177	15 val h = fn x : N.u => case x of N.C x => x \| N.D => M.A
adamc@174	16
adamc@177	17 datatype u = datatype N.u
adamc@174	18
adamc@174	19 val i = fn x : u => case x of N.C x => x \| D => M.A
adamc@177	20
adamc@177	21 val toString = fn x =>
adamc@177	22 case x of
adamc@177	23 C A => "C A"
adamc@177	24 \| C B => "C B"
adamc@177	25 \| D => "D"
adamc@177	26
adamc@183	27 val rec page = fn x => <html><body>
adamc@183	28 {cdata (toString x)}<br/>
adamc@183	29 <br/>
adamc@183	30
adamc@183	31 <a link={page x}>Again!</a>
adamc@177	32 </body></html>
adamc@177	33
adamc@177	34 val main : unit -> page = fn () => <html><body>
adamc@177	35 <li> <a link={page (C A)}>C A</a></li>
adamc@177	36 <li> <a link={page (C B)}>C B</a></li>
adamc@177	37 <li> <a link={page D}>D</a></li>
adamc@177	38 </body></html>

Mercurial > urweb