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