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

cselect

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 14 May 2009 09:33:48 -0400
parents	6271f0e3c272
children	e92cfac1608f

rev	line source
adamc@794	1 datatype t = datatype Basis.list
adamc@794	2
adamc@794	3 val show (a ::: Type) (_ : show a) =
adamc@794	4 let
adamc@794	5 fun show' (ls : list a) =
adamc@794	6 case ls of
adamc@794	7 [] => "[]"
adamc@794	8 \| x :: ls => show x ^ " :: " ^ show' ls
adamc@794	9 in
adamc@794	10 mkShow show'
adamc@794	11 end
adamc@794	12
adamc@794	13 val rev (a ::: Type) =
adamc@794	14 let
adamc@794	15 fun rev' acc (ls : list a) =
adamc@794	16 case ls of
adamc@794	17 [] => acc
adamc@794	18 \| x :: ls => rev' (x :: acc) ls
adamc@794	19 in
adamc@794	20 rev' []
adamc@794	21 end
adamc@794	22
adamc@794	23 fun mp (a ::: Type) (b ::: Type) f =
adamc@794	24 let
adamc@794	25 fun mp' acc ls =
adamc@794	26 case ls of
adamc@794	27 [] => rev acc
adamc@794	28 \| x :: ls => mp' (f x :: acc) ls
adamc@794	29 in
adamc@794	30 mp' []
adamc@794	31 end
adamc@796	32
adamc@796	33 fun mapX (a ::: Type) (ctx ::: {Unit}) f =
adamc@796	34 let
adamc@796	35 fun mapX' ls =
adamc@796	36 case ls of
adamc@796	37 [] => <xml/>
adamc@796	38 \| x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796	39 in
adamc@796	40 mapX'
adamc@796	41 end

Mercurial > urweb