Ur/Web: demo/list.ur annotate

Fix MonoReduce unsoundness with lets and fns

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 13 Jun 2009 15:42:24 -0400
parents	669ac5e9a69e
children

rev	line source
adamc@397	1 datatype list t = Nil \| Cons of t * list t
adamc@397	2
adamc@823	3 fun length [t] (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@823	13 fun rev [t] (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

Mercurial > urweb