1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7signature SUM =
8sig
9  datatype ('a, 'b) sum = Inl of 'a | Inr of 'b
10  val case_sum : ('a -> 'c) -> ('b -> 'c) -> ('a, 'b) sum -> 'c
11  val map_sum : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) sum -> ('c, 'd) sum
12  val isl : ('a, 'b) sum -> bool
13  val isr : ('a, 'b) sum -> bool
14  val froml : 'a -> ('a, 'b) sum -> 'a
15  val fromr : 'b -> ('a, 'b) sum -> 'b
16  val lefts : ('a, 'b) sum list -> 'a list
17  val rights : ('a, 'b) sum list -> 'b list
18end
19
20
21structure Sum: SUM =
22struct
23
24datatype ('a, 'b) sum = Inl of 'a | Inr of 'b
25
26fun case_sum f _ (Inl x) = f x
27  | case_sum _ g (Inr y) = g y;
28
29fun map_sum f _ (Inl x) = Inl (f x)
30  | map_sum _ g (Inr y) = Inr (g y);
31
32fun isl (Inl _) = true
33  | isl (Inr _) = false;
34
35fun isr (Inl _) = false
36  | isr (Inr _) = true;
37
38fun froml _ (Inl x) = x
39  | froml x _ = x;
40
41fun fromr _ (Inr y) = y
42  | fromr y _ = y;
43
44fun lefts [] = []
45  | lefts (Inl x :: xs) = x :: lefts xs
46  | lefts (_ :: xs) = lefts xs;
47
48fun rights [] = []
49  | rights (Inr y :: ys) = y :: rights ys
50  | rights (_ :: ys) = rights ys;
51
52end
53
54open Sum;
55