
  0 | module Data.OneOf
  1 | 
  2 | import public Data.List.Elem
  3 | import public Data.List.Quantifiers
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | data OneOf : List Type -> Type where
  9 |   Here : x -> OneOf (x :: xs)
 10 |   There : OneOf xs -> OneOf (x :: xs)
 11 | 
 12 | public export
 13 | make : Elem a as => a -> OneOf as
 14 | make x @{Here} = Here x
 15 | make x @{There _} = There (make x)
 16 | 
 17 | public export
 18 | TypeAt : (as : List Type) -> OneOf as -> Type
 19 | TypeAt (x :: _) (Here _) = x
 20 | TypeAt (_ :: xs) (There x) = TypeAt xs x
 21 | 
 22 | public export
 23 | Eliminators : (as : List Type) -> (r : Type) -> Type
 24 | Eliminators xs r = HList (map (\x => x -> r) xs)
 25 | 
 26 | public export
 27 | get : (o : OneOf as) -> TypeAt as o
 28 | get (Here x) = x
 29 | get (There x) = get x
 30 | 
 31 | public export
 32 | match : OneOf as -> Eliminators as r -> r
 33 | match (Here x) (f :: _) = f x
 34 | match (There x) (_ :: fs) = match x fs
 35 | 
 36 | public export
 37 | extend : OneOf as -> OneOf (as ++ bs)
 38 | extend (Here x) = Here x
 39 | extend (There x) = There (extend x)
 40 |