Ur/Web: tests/specialize.ur annotate

Unpolyed a polymorphic function of two arguments

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 11 Sep 2008 10:14:59 -0400
parents	e21d0dddda09
children	6a4e365db60c

rev	line source
adamc@315	1 datatype list a = Nil \| Cons of a * list a
adamc@315	2
adamc@315	3 fun isNil (t ::: Type) (ls : list t) : bool =
adamc@315	4 case ls of
adamc@315	5 Nil => True
adamc@315	6 \| Cons _ => False
adamc@315	7
adamc@316	8 fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
adamc@315	9 case ls1 of
adamc@315	10 Nil => ls2
adamc@315	11 \| Cons (x, ls1') => Cons (x, append ls1' ls2)
adamc@315	12
adamc@315	13 fun delist (ls : list string) : xml body [] [] =
adamc@315	14 case ls of
adamc@315	15 Nil => <body>Nil</body>
adamc@316	16 \| Cons (h, t) => <body>{cdata h} :: {delist t}</body>
adamc@315	17
adamc@315	18 val ls = Cons ("X", Cons ("Y", Cons ("Z", Nil)))
adamc@316	19 val ls' = Cons ("A", Cons ("B", Nil))
adamc@315	20
adamc@315	21 fun main () : transaction page = return <html><body>
adamc@315	22 {if isNil ls then <body>It's Nil.</body> else <body>It's not Nil.</body>}
adamc@316	23
adamc@316	24 <p>{delist (append ls' ls)}</p>
adamc@315	25 </body></html>
adamc@315	26
adamc@315	27
adamc@315	28
adamc@316	29

Mercurial > urweb