0 | module Text.SVG.Tag
  1 |
  2 | %default total
  3 |
  4 | --------------------------------------------------------------------------------
  5 | -- Predicates
  6 | --------------------------------------------------------------------------------
  7 |
  8 | ||| Proof that the given element can have an `href` attribute
  9 | public export
 10 | data HasHref : (s : String) -> Type where
 11 |   HasHrefImage   : HasHref "image"
 12 |   HasHrefPattern : HasHref "pattern"
 13 |   HasHrefUse     : HasHref "use"
 14 |
 15 | ||| Proof that the given element can have a `cx` attribute
 16 | public export
 17 | data HasCX : (s : String) -> Type where
 18 |   HasCXCircle  : HasCX "circle"
 19 |   HasCXEllipse : HasCX "ellipse"
 20 |
 21 | ||| Proof that the given element can have a `cy` attribute
 22 | public export
 23 | data HasCY : (s : String) -> Type where
 24 |   HasCYCircle  : HasCY "circle"
 25 |   HasCYEllipse : HasCY "ellipse"
 26 |
 27 | ||| Proof that the given element can have an `rx` attribute
 28 | public export
 29 | data HasRX : (s : String) -> Type where
 30 |   HasRXEllipse : HasRX "ellipse"
 31 |   HasRXRect    : HasRX "rect"
 32 |
 33 | ||| Proof that the given element can have an `ry` attribute
 34 | public export
 35 | data HasRY : (s : String) -> Type where
 36 |   HasRYEllipse : HasRY "ellipse"
 37 |   HasRYRect    : HasRY "rect"
 38 |
 39 | ||| Proof that the given element can have an `x` attribute
 40 | public export
 41 | data HasX : (s : String) -> Type where
 42 |   HasXFilter  : HasX "filter"
 43 |   HasXImage   : HasX "image"
 44 |   HasXRect    : HasX "rect"
 45 |   HasXText    : HasX "text"
 46 |
 47 | ||| Proof that the given element can have a `y` attribute
 48 | public export
 49 | data HasY : (s : String) -> Type where
 50 |   HasYFilter  : HasY "filter"
 51 |   HasYImage   : HasY "image"
 52 |   HasYRect    : HasY "rect"
 53 |   HasYText    : HasY "text"
 54 |
 55 | ||| Proof that the given element can have a `height` attribute
 56 | public export
 57 | data HasHeight : (s : String) -> Type where
 58 |   HasHeightFilter  : HasHeight "filter"
 59 |   HasHeightImage   : HasHeight "image"
 60 |   HasHeightMask    : HasHeight "mask"
 61 |   HasHeightPath    : HasHeight "path"
 62 |   HasHeightPattern : HasHeight "pattern"
 63 |   HasHeightRect    : HasHeight "rect"
 64 |   HasHeightSVG     : HasHeight "svg"
 65 |   HasHeightUse     : HasHeight "use"
 66 |
 67 | ||| Proof that the given element can have a `fill` attribute
 68 | public export
 69 | data HasFill : (s : String) -> Type where
 70 |   HasFillCircle   : HasFill "circle"
 71 |   HasFillEllipse  : HasFill "ellipse"
 72 |   HasFillGroup    : HasFill "g"
 73 |   HasFillLine     : HasFill "line"
 74 |   HasFillPath     : HasFill "path"
 75 |   HasFillPolygon  : HasFill "polygon"
 76 |   HasFillPolyline : HasFill "polyline"
 77 |   HasFillRect     : HasFill "rect"
 78 |   HasFillSVG      : HasFill "svg"
 79 |   HasFillText     : HasFill "text"
 80 |
 81 | ||| Proof that the given element can have a `stroke` attribute
 82 | public export
 83 | data HasStroke : (s : String) -> Type where
 84 |   HasStrokeCircle   : HasStroke "circle"
 85 |   HasStrokeEllipse  : HasStroke "ellipse"
 86 |   HasStrokeGroup    : HasStroke "g"
 87 |   HasStrokeLine     : HasStroke "line"
 88 |   HasStrokePath     : HasStroke "path"
 89 |   HasStrokePolygon  : HasStroke "polygon"
 90 |   HasStrokePolyline : HasStroke "polyline"
 91 |   HasStrokeRect     : HasStroke "rect"
 92 |   HasStrokeSVG      : HasStroke "svg"
 93 |   HasStrokeText     : HasStroke "text"
 94 |
 95 | ||| Proof that the given element can have a `width` attribute
 96 | public export
 97 | data HasWidth : (s : String) -> Type where
 98 |   HasWidthFilter  : HasWidth "filter"
 99 |   HasWidthImage   : HasWidth "image"
100 |   HasWidthMask    : HasWidth "mask"
101 |   HasWidthPath    : HasWidth "path"
102 |   HasWidthPattern : HasWidth "pattern"
103 |   HasWidthRect    : HasWidth "rect"
104 |   HasWidthSVG     : HasWidth "svg"
105 |   HasWidthUse     : HasWidth "use"
106 |
107 | ||| Proof that the given element can have a `viewPort` attribute
108 | public export
109 | data HasViewBox : (s : String) -> Type where
110 |   HasViewBoxMarker  : HasViewBox "marker"
111 |   HasViewBoxPattern : HasViewBox "pattern"
112 |   HasViewBoxSVG     : HasViewBox "svg"
113 |   HasViewBoxSymbol  : HasViewBox "symbol"
114 |   HasViewBoxView    : HasViewBox "view"
115 |
116 | ||| Proof that the given element can have a `points` attribute
117 | public export
118 | data HasPoints : (s : String) -> Type where
119 |   HasPointsPolygon  : HasPoints "polygon"
120 |   HasPointsPolyline  : HasPoints "polyline"
121 |
122 | ||| Proof that the given element displays some text
123 | public export
124 | data IsText : (s : String) -> Type where
125 |   IsTextText  : IsText "text"
126 |   IsTextTSpan : IsText "tspan"
127 |   IsTextGroup : IsText "g"
128 |   IsTextSVG   : IsText "svg"
129 |