0 | {- Tian Z (ecburx@burx.vip) -}
  1 |
  2 | ||| Data / Types
  3 | module IdrisGL.DataType
  4 |
  5 | import IdrisGL.Color
  6 |
  7 | {- Types -}
  8 |
  9 | ||| A rectangle used to determine an area.
 10 | public export
 11 | record Rect where
 12 |     constructor MkRect
 13 |     ||| @ x X coordinate of the start point.
 14 |     x : Int
 15 |     ||| @ y Y coordinate of the start point.
 16 |     y : Int
 17 |     ||| @ w The width of the rectangle area.
 18 |     w : Int
 19 |     ||| @ h The height of the rectangle area.
 20 |     h : Int
 21 |
 22 | ||| A coordinate used to determine the position.
 23 | public export
 24 | record Coordinate where
 25 |     constructor MkCoor
 26 |     ||| @ x X coordinate of the point.
 27 |     x : Int
 28 |     ||| @ y Y coordinate of the point.
 29 |     y : Int
 30 |
 31 | {- Pinter Types -}
 32 |
 33 | ||| Surface.
 34 | ||| A structure that contains a collection of pixels used in software blitting.
 35 | public export
 36 | record Sur where
 37 |     constructor MkSur
 38 |     ||| A wrapper of SDL_Surface pointer.
 39 |     ||| @ ptr The C pointer of a SDL_Surface. You should not directly operate this pointer.
 40 |     ptr : AnyPtr
 41 |
 42 | ||| Window.
 43 | public export
 44 | record Win where
 45 |     constructor MkWin
 46 |     ||| A wrapper of SDL_Window pointer.
 47 |     ||| @ ptr The C pointer of a SDL_Window. You should not directly operate this pointer.
 48 |     ptr : AnyPtr
 49 |
 50 | ||| Renderer.
 51 | ||| A 2D rendering context for a window.
 52 | public export
 53 | record Renderer where
 54 |     constructor MkRenderer
 55 |     ||| A wrapper of SDL_Renderer pointer.
 56 |     ||| @ ptr The C pointer of a SDL_Renderer. You should not directly operate this pointer.
 57 |     ptr : AnyPtr
 58 |
 59 | ||| Texture.
 60 | ||| A structure that contains an efficient, driver-specific representation of pixel data.
 61 | public export
 62 | record Texture where
 63 |     constructor MkTexture
 64 |     ||| A wrapper of SDL_Texture pointer.
 65 |     ||| @ ptr The C pointer of a SDL_Texture. You should not directly operate this pointer.
 66 |     ptr : AnyPtr
 67 |
 68 | ||| Event.
 69 | ||| A union that contains structures for the different event types.
 70 | public export
 71 | record Event where
 72 |     constructor MkEvent
 73 |     ||| A wrapper of SDL_Event pointer.
 74 |     ||| @ ptr The C pointer of a SDL_Event. You should not directly operate this pointer.
 75 |     ptr : AnyPtr
 76 |
 77 | {- Datas -}
 78 |
 79 | ||| Describes how IdrisGL should display its output.
 80 | public export
 81 | data Display
 82 |     = ||| Display in a window with the given name and area (size and position).
 83 |     InWindow String Rect
 84 |     | ||| Display full screen.
 85 |     FullWindow
 86 |
 87 | ||| Font styles.
 88 | public export
 89 | data TextStyle   = TS_NORMAL | TS_BOLD  | TS_ITALIC | TS_UNDERLINE | TS_STRIKETHROUGH
 90 |
 91 | ||| FreeType hinter settings.
 92 | public export
 93 | data TextHinting = TH_NORMAL | TH_LIGHT | TH_MONO   | TH_NONE
 94 |
 95 | ||| Flip settings for SDL bindings.
 96 | ||| Instead you should avoid to use SDL bindings.
 97 | public export
 98 | data FlipSetting = FLIP_NONE | FLIP_HORIZONTAL | FLIP_VERTICAL
 99 |
100 | ||| 2D Picture.
101 | public export
102 | data Picture : Type where
103 |     ||| A blank picture, with nothing in it.
104 |     Blank : Picture
105 |     ||| A picture consisting of several others.
106 |     ||| @ pics    Other pictures.
107 |     Pictures
108 |       :  (pics : List Picture)
109 |       -> Picture
110 |     ||| A picture rotated clockwise by the given angle (in degrees) and given center.
111 |     ||| @ angle   Rotation angle.
112 |     ||| @ center  Rotation center.
113 |     ||| @ pic     The picture to be rotated.
114 |     Rotate
115 |       :  (angle  : Double)
116 |       -> (center : Coordinate)
117 |       -> (pic    : Picture)
118 |       -> Picture
119 |
120 |     {-
121 |         Images.
122 |     -}
123 |
124 |     ||| A bitmap image.
125 |     ||| @ path The path of the bitmap.
126 |     ||| @ rect The size and position of placed bitmap.
127 |     Bitmap
128 |       :  (path : String)
129 |       -> (rect : Rect)
130 |       -> Picture
131 |     ||| An image in other format (PNG/JPG/WEBP/TIF).
132 |     ||| @ path The path of the image.
133 |     ||| @ rect The size and position of placed image.
134 |     Image
135 |       :  (path : String)
136 |       -> (rect : Rect)
137 |       -> Picture
138 |
139 |     {-
140 |         Shapes.
141 |     -}
142 |
143 |     ||| A pixel at given coordinate.
144 |     ||| @ position The position of the pixel.
145 |     ||| @ color    The color of the pixel.
146 |     Pixel
147 |       :  (position : Coordinate)
148 |       -> (color    : Color)
149 |       -> Picture
150 |     ||| A thick line with given thickness.
151 |     ||| @ start     The start position.
152 |     ||| @ end       The end position.
153 |     ||| @ color     The color of line.
154 |     ||| @ thickness The thickness of line.
155 |     ThickLine
156 |       :  (start     : Coordinate)
157 |       -> (end       : Coordinate)
158 |       -> (color     : Color)
159 |       -> (thickness : Int)
160 |       -> Picture
161 |     ||| A line.
162 |     ||| @ start     The start position.
163 |     ||| @ end       The end position.
164 |     ||| @ color     The color of line.
165 |     Line
166 |       :  (start : Coordinate)
167 |       -> (end   : Coordinate)
168 |       -> (color : Color)
169 |       -> Picture
170 |
171 |     {-
172 |         Rectangle
173 |     -}
174 |
175 |     ||| A rectangle.
176 |     ||| @ rect    The size of position of the rectangle.
177 |     ||| @ color   The color of the rectangle.
178 |     ||| @ filling True if fill the rectangle.
179 |     Rectangle
180 |       :  (rect    : Rect)
181 |       -> (color   : Color)
182 |       -> (filling : Bool)
183 |       -> Picture
184 |     ||| A rounded-corner rectangle.
185 |     ||| @ rect    The size of position of the rectangle.
186 |     ||| @ color   The color of the rectangle.
187 |     ||| @ filling True if fill the rectangle.
188 |     ||| @ radius  The radius of the corner arc.
189 |     R_Rectangle
190 |       :  (rect    : Rect)
191 |       -> (color   : Color)
192 |       -> (filling : Bool)
193 |       -> (radius  : Int)
194 |       -> Picture
195 |
196 |     {-
197 |         Circle
198 |     -}
199 |
200 |     ||| A circle.
201 |     ||| @ center  The center of the circle.
202 |     ||| @ color   The color of the circle.
203 |     ||| @ filling True if fill the circle.
204 |     ||| @ radius  The radius of the circle.
205 |     Circle
206 |       :  (center  : Coordinate)
207 |       -> (color   : Color)
208 |       -> (filling : Bool)
209 |       -> (radius  : Int)
210 |       -> Picture
211 |     ||| A circle with given thickness.
212 |     ||| @ center    The center of the circle.
213 |     ||| @ color     The color of the circle.
214 |     ||| @ filling   True if fill the circle.
215 |     ||| @ radius    The radius of the circle.
216 |     ||| @ thickness The thickness of the drawing line.
217 |     ThickCircle
218 |       :  (center    : Coordinate)
219 |       -> (color     : Color)
220 |       -> (radius    : Int)
221 |       -> (thickness : Int)
222 |       -> Picture
223 |
224 |     {-
225 |         Misc.
226 |     -}
227 |
228 |     ||| A circular arc drawn counter-clockwise between two angles (in degrees).
229 |     ||| @ center The center of the arc.
230 |     ||| @ color  The color of drawing line.
231 |     ||| @ radius The radius of the arc.
232 |     ||| @ start  Starting radius in degrees of the arc. 0 degrees is down, increasing counterclockwise.
233 |     ||| @ end    Ending radius in degrees of the arc. 0 degrees is down, increasing counterclockwise.
234 |     Arc
235 |       :  (center : Coordinate)
236 |       -> (color  : Color)
237 |       -> (radius : Int)
238 |       -> (start  : Int)
239 |       -> (end    : Int)
240 |       -> Picture
241 |     ||| A pie (outline) drawn counter-clockwise between two angles (in degrees).
242 |     ||| @ center The center of the pie.
243 |     ||| @ color  The color of drawing line.
244 |     ||| @ radius The radius of the pie.
245 |     ||| @ start  Starting radius in degrees of the arc. 0 degrees is down, increasing counterclockwise.
246 |     ||| @ end    Ending radius in degrees of the arc. 0 degrees is down, increasing counterclockwise.
247 |     Pie
248 |       :  (center : Coordinate)
249 |       -> (color  : Color)
250 |       -> (radius : Int)
251 |       -> (start  : Int)
252 |       -> (end    : Int)
253 |       -> (filled : Bool)
254 |       -> Picture
255 |     ||| An ellipse.
256 |     ||| @ center  The center of the ellipse.
257 |     ||| @ rx      Horizontal radius in pixels of the ellipse.
258 |     ||| @ ry      Vertical radius in pixels of the ellipse.
259 |     ||| @ color   The color of drawing line.
260 |     ||| @ filling True if fill the ellipse.
261 |     Ellipse
262 |       :  (center  : Coordinate)
263 |       -> (rx      : Int)
264 |       -> (ry      : Int)
265 |       -> (color   : Color)
266 |       -> (filling : Bool)
267 |       -> Picture
268 |     ||| A trigon.
269 |     ||| @ point1  The first point.
270 |     ||| @ point2  The second point.
271 |     ||| @ point3  The third point.
272 |     ||| @ color   The color of drawing line.
273 |     ||| @ filling True if fill the trigon.
274 |     Trigon
275 |       :  (point1  : Coordinate)
276 |       -> (point2  : Coordinate)
277 |       -> (point3  : Coordinate)
278 |       -> (color   : Color)
279 |       -> (filling : Bool)
280 |       -> Picture
281 |     ||| A polygon.
282 |     ||| @ points  A list of points.
283 |     ||| @ color   The color of drawing line.
284 |     ||| @ filling True if fill the trigon.
285 |     Polygon
286 |       :  (points  : List Coordinate)
287 |       -> (color   : Color)
288 |       -> (filling : Bool)
289 |       -> Picture
290 |
291 |     {-
292 |         Text
293 |     -}
294 |
295 |     ||| Blended text with default settings.
296 |     ||| @ text  Text.
297 |     ||| @ size  Font size.
298 |     ||| @ font  Path of font file.
299 |     ||| @ pos   Position of text.
300 |     ||| @ color The color of text.
301 |     Text
302 |       :  (text  : String)
303 |       -> (size  : Int)
304 |       -> (font  : String)
305 |       -> (pos   : Coordinate)
306 |       -> (color : Color)
307 |       -> Picture
308 |     ||| Solid text.
309 |     ||| @ text    Text.
310 |     ||| @ size    Font size.
311 |     ||| @ font    Path of font file.
312 |     ||| @ pos     Position of text.
313 |     ||| @ color   The color of text.
314 |     ||| @ style   Font style.
315 |     ||| @ hinting Hinting.
316 |     ||| @ kerning Kerning.
317 |     SolidText
318 |       :  (text    : String)
319 |       -> (size    : Int)
320 |       -> (font    : String)
321 |       -> (pos     : Coordinate)
322 |       -> (color   : Color)
323 |       -> (style   : TextStyle)
324 |       -> (hinting : TextHinting)
325 |       -> (kerning : Int)
326 |       -> Picture
327 |     ||| Blended text.
328 |     ||| @ text    Text.
329 |     ||| @ size    Font size.
330 |     ||| @ font    Path of font file.
331 |     ||| @ pos     Position of text.
332 |     ||| @ color   The color of text.
333 |     ||| @ style   Font style.
334 |     ||| @ hinting Hinting.
335 |     ||| @ kerning Kerning.
336 |     BlendedText
337 |       : (text     : String)
338 |       -> (size    : Int)
339 |       -> (font    : String)
340 |       -> (pos     : Coordinate)
341 |       -> (color   : Color)
342 |       -> (style   : TextStyle)
343 |       -> (hinting : TextHinting)
344 |       -> (kerning : Int)
345 |       -> Picture
346 |     ||| Shaded text. (Blended text with background color)
347 |     ||| @ text    Text.
348 |     ||| @ size    Font size.
349 |     ||| @ font    Path of font file.
350 |     ||| @ pos     Position of text.
351 |     ||| @ color   The color of text.
352 |     ||| @ bgColor The background color.
353 |     ||| @ style   Font style.
354 |     ||| @ hinting Hinting.
355 |     ||| @ kerning Kerning.
356 |     ShadedText
357 |       :  (text    : String)
358 |       -> (size    : Int)
359 |       -> (font    : String)
360 |       -> (pos     : Coordinate)
361 |       -> (color   : Color)
362 |       -> (bgColor : Color)
363 |       -> (style   : TextStyle)
364 |       -> (hinting : TextHinting)
365 |       -> (kerning : Int)
366 |       -> Picture
367 |