
  0 | module Lana.Schemas
  1 | 
  2 | import Lana.Class
  3 | import Lana.Name
  4 | 
  5 | import Data.List.Elem
  6 | import Data.List.Quantifiers
  7 | 
  8 | export
  9 | transformNamed :
 10 |   {schema: Type -> Type} ->
 11 |   Lana schema =>
 12 |   Name ->
 13 |   (a -> b) ->
 14 |   (b -> a) ->
 15 |   schema b ->
 16 |   schema a
 17 | transformNamed name aToB bToA =
 18 |   validateNamed name aToB (Right . bToA)
 19 | 
 20 | export
 21 | eitherOfNamed :
 22 |   {schema: Type -> Type} -> {a: Type} -> {b: Type} ->
 23 |   Lana schema =>
 24 |   Name ->
 25 |   schema a ->
 26 |   schema b ->
 27 |   schema (Either a b)
 28 | eitherOfNamed name leftSchema rightSchema =
 29 |   let
 30 |     toUnion : Either a b -> Union [a, b]
 31 |     toUnion eitherAOrB =
 32 |       case eitherAOrB of
 33 |         Left a => Here a
 34 |         Right b => There $ Here b
 35 | 
 36 |     fromUnion : Union [a, b] -> Either a b
 37 |     fromUnion union =
 38 |       case union of
 39 |         Here aa => Left aa
 40 |         There (Here bb) => Right bb
 41 | 
 42 |     unionSchema : schema (Union [a, b])
 43 |     unionSchema =
 44 |       unionNamed name $
 45 |         unionMemberWithIndex Here leftSchema
 46 |           #| unionMemberWithIndex (There Here) rightSchema
 47 |   in
 48 |     transformNamed
 49 |       name
 50 |       toUnion
 51 |       fromUnion
 52 |       unionSchema
 53 |