adamc@794: datatype t = datatype Basis.list
adamc@794: 
adamc@794: val show (a ::: Type) (_ : show a) =
adamc@794:     let
adamc@794:         fun show' (ls : list a) =
adamc@794:             case ls of
adamc@794:                 [] => "[]"
adamc@794:               | x :: ls => show x ^ " :: " ^ show' ls
adamc@794:     in
adamc@794:         mkShow show'
adamc@794:     end
adamc@794: 
adamc@794: val rev (a ::: Type) =
adamc@794:     let
adamc@794:         fun rev' acc (ls : list a) =
adamc@794:             case ls of
adamc@794:                 [] => acc
adamc@794:               | x :: ls => rev' (x :: acc) ls
adamc@794:     in
adamc@794:         rev' []
adamc@794:     end
adamc@794: 
adamc@794: fun mp (a ::: Type) (b ::: Type) f =
adamc@794:     let
adamc@794:         fun mp' acc ls =
adamc@794:             case ls of
adamc@794:                 [] => rev acc
adamc@794:               | x :: ls => mp' (f x :: acc) ls
adamc@794:     in
adamc@794:         mp' []
adamc@794:     end
adamc@796: 
adamc@796: fun mapX (a ::: Type) (ctx ::: {Unit}) f =
adamc@796:     let
adamc@796:         fun mapX' ls =
adamc@796:             case ls of
adamc@796:                 [] => <xml/>
adamc@796:               | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796:     in
adamc@796:         mapX'
adamc@796:     end