0 | module Lana.Class
  1 |
  2 | import Data.SortedMap as Map
  3 | import Data.Finite as Finite
  4 | import Data.List.Elem
  5 | import Data.List.Quantifiers
  6 |
  7 | import Lana.Name
  8 |
  9 | public export
 10 | data Null = MkNull
 11 |
 12 | -- https://github.com/flipstone/shrubbery/blob/main/src/Shrubbery/Union.hs
 13 | public export
 14 | Union: (types: List Type) -> Type
 15 | Union = Any id
 16 |
 17 | public export
 18 | BranchIndex: (a: Type) -> (types: List Type) -> Type
 19 | BranchIndex = Elem
 20 |
 21 | --export
 22 | --record Rational where
 23 | --  constructor MkRational
 24 | --  numerator: Integer
 25 | --  denominator: Integer
 26 |
 27 | public export
 28 | interface Lana (schema: Type -> Type) where
 29 |   data Object: Type -> Type -> Type
 30 |   data Field: Type -> Type -> Type
 31 |   data AdditionalFields: Type -> Type -> Type
 32 |   data UnionMembers: List Type -> List Type -> Type
 33 |
 34 |   schemaName : {a: Type} -> schema a -> Name
 35 |
 36 |   double : schema Double
 37 |
 38 |   text : schema String
 39 |
 40 |   boolean : schema Bool
 41 |
 42 |   array : schema a -> schema (List a)
 43 |
 44 |   null : schema Null
 45 |
 46 |   nullable : schema a -> schema (Either Null a)
 47 |
 48 |   required :
 49 |     String ->
 50 |     (object -> a) ->
 51 |     schema a ->
 52 |     Field object a
 53 |
 54 |   optional :
 55 |     String ->
 56 |     (object -> Maybe a) ->
 57 |     schema a ->
 58 |     Field object (Maybe a)
 59 |
 60 |   mapField :
 61 |     (a -> b) ->
 62 |     Field object a ->
 63 |     Field object b
 64 |
 65 |   additionalFields :
 66 |     {object, a: Type} ->
 67 |     (object -> Map.SortedMap String a) ->
 68 |     schema a ->
 69 |     AdditionalFields object (Map.SortedMap String a)
 70 |
 71 |   objectNamed :
 72 |     Name ->
 73 |     Object a a ->
 74 |     schema a
 75 |
 76 |   constructor :
 77 |     {constructorType: Type} ->
 78 |     constructorType ->
 79 |     Object object constructorType
 80 |
 81 |   field :
 82 |     {object, a, b: Type} ->
 83 |     Object object (a -> b) ->
 84 |     Field object a ->
 85 |     Object object b
 86 |
 87 |   additional :
 88 |     {object, a: Type} ->
 89 |     Object object (a -> object) ->
 90 |     AdditionalFields object a ->
 91 |     Object object object
 92 |
 93 |   validateNamed :
 94 |     Name ->
 95 |     (a -> b) ->
 96 |     (b -> Either String a) ->
 97 |     (schema b) ->
 98 |     (schema a)
 99 |
100 |   finiteNamed :
101 |     Finite.Finite a =>
102 |     Name ->
103 |     (a -> String) ->
104 |     schema a
105 |
106 |   unionNamed :
107 |     {types: List Type} ->
108 |     Name ->
109 |     UnionMembers types types ->
110 |     schema (Union types)
111 |
112 |   unionMemberWithIndex :
113 |     {a: Type} ->
114 |     {types: List Type} ->
115 |     BranchIndex a types ->
116 |     schema a ->
117 |     UnionMembers types [a]
118 |
119 |   unionCombine :
120 |     {types, left, right: List Type} ->
121 |     UnionMembers types left ->
122 |     UnionMembers types right ->
123 |     UnionMembers types (left ++ right)
124 |
125 |   jsonString :
126 |     schema a ->
127 |     schema a
128 |
129 |   implementation Lana schema => Functor (Field object) where
130 |     map = mapField
131 |
132 | export infixl 9 #+
133 | export
134 | (#+) :
135 |   {schema: Type -> Type} ->
136 |   {object, a, b: Type} ->
137 |   Lana schema =>
138 |   Object {schema} object (a -> b) ->
139 |   Field {schema} object a ->
140 |   Object {schema} object b
141 | (#+) =
142 |   field
143 |
144 | export infixl 9 #|
145 | export
146 | (#|) :
147 |   {schema: Type -> Type} ->
148 |   {types: List Type} ->
149 |   {left, right: List Type} ->
150 |   Lana schema =>
151 |   UnionMembers {schema} types left ->
152 |   UnionMembers {schema} types right ->
153 |   UnionMembers {schema} types (left ++ right)
154 | (#|) =
155 |   unionCombine
156 |
157 | export infixl 9 #*
158 | export
159 | (#*) :
160 |   {schema: Type -> Type} ->
161 |   {object, a: Type} ->
162 |   Lana schema =>
163 |   Object {schema} object (a -> object) ->
164 |   AdditionalFields {schema} object a ->
165 |   Object {schema} object object
166 | (#*) =
167 |   additional
168 |