summaryrefslogtreecommitdiff
path: root/lib/ur/list.ur
blob: 2ee6053801af675fa847f64a278ca88e05f8fd92 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
datatype t = datatype Basis.list

val show (a ::: Type) (_ : show a) =
    let
        fun show' (ls : list a) =
            case ls of
                [] => "[]"
              | x :: ls => show x ^ " :: " ^ show' ls
    in
        mkShow show'
    end

val rev (a ::: Type) =
    let
        fun rev' acc (ls : list a) =
            case ls of
                [] => acc
              | x :: ls => rev' (x :: acc) ls
    in
        rev' []
    end

fun mp (a ::: Type) (b ::: Type) f =
    let
        fun mp' acc ls =
            case ls of
                [] => rev acc
              | x :: ls => mp' (f x :: acc) ls
    in
        mp' []
    end

fun mapX (a ::: Type) (ctx ::: {Unit}) f =
    let
        fun mapX' ls =
            case ls of
                [] => <xml/>
              | x :: ls => <xml>{f x}{mapX' ls}</xml>
    in
        mapX'
    end

fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
    let
        fun mapM' acc ls =
            case ls of
                [] => acc
              | x :: ls => mapM' (x' <- f x; ls' <- acc; return (x' :: ls')) ls
    in
        mapM' (return [])
    end