Mercurial > urweb
annotate demo/list.ur @ 758:8323c1beef2e
Subforms type-checks; lists urlified and unurlified
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 30 Apr 2009 11:48:56 -0400 |
parents | 7ef4b2911b09 |
children | 669ac5e9a69e |
rev | line source |
---|---|
adamc@397 | 1 datatype list t = Nil | Cons of t * list t |
adamc@397 | 2 |
adamc@501 | 3 fun length (t ::: Type) (ls : list t) = |
adamc@501 | 4 let |
adamc@501 | 5 fun length' (ls : list t) (acc : int) = |
adamc@501 | 6 case ls of |
adamc@501 | 7 Nil => acc |
adamc@501 | 8 | Cons (_, ls') => length' ls' (acc + 1) |
adamc@501 | 9 in |
adamc@501 | 10 length' ls 0 |
adamc@501 | 11 end |
adamc@397 | 12 |
adamc@501 | 13 fun rev (t ::: Type) (ls : list t) = |
adamc@501 | 14 let |
adamc@501 | 15 fun rev' (ls : list t) (acc : list t) = |
adamc@501 | 16 case ls of |
adamc@501 | 17 Nil => acc |
adamc@501 | 18 | Cons (x, ls') => rev' ls' (Cons (x, acc)) |
adamc@501 | 19 in |
adamc@501 | 20 rev' ls Nil |
adamc@501 | 21 end |