Development of Path, Ellipse, Rectangle, and Text Primitives

[HenriqueBorges6]

Files Changed

• ProofWidgets/Data/Svg.lean: Added new primitives
• ProofWidgets/Demos/Svg.lean: Added examples of usage

This PR introduces new SVG primitives to the Shape data structure. The following primitives have been added:

• path
• ellipse
• rect
• text

Each of these primitives is defined as follows:

inductive Shape (f : Frame) where
  ...
  | path     (d : String)
  | ellipse  (center : Point f) (rx ry : Size f)
  | rect     (corner : Point f) (width height : Size f)
  | text     (pos : Point f) (content : String) (size : Size f)

• path: Defined by the attribute d = "path data".
• ellipse: Defined by its center and radii (rx and ry).
• rect: Defined by its corner point, width, and height.
• text: Defined by its position, content, and font size.

Note: In SVG 1.1, the path and text elements are specified in different sections under basic shapes. Here, I have considered them as shapes.

Additionally, the toHtmlData function has been updated to handle the new primitives and generate appropriate HTML attributes:

def Shape.toHtmlData {f : Frame} : Shape f → String × Array (String × Json)
  ...
  | .path d =>
      ("path", #[("d", d)])
  | .ellipse center rx ry =>
    let (cx,cy) := center.toPixels
    let rX := rx.toPixels
    let rY := ry.toPixels
    ("ellipse", #[("cx", cx), ("cy", cy), ("rx", rX), ("ry", rY)])
  | .rect corner width height =>
    let (x,y) := corner.toPixels
    let w := width.toPixels
    let h := height.toPixels
    ("rect", #[("x", x), ("y", y), ("width", w), ("height", h)])
  | .text pos content size =>
    let (x,y) := pos.toPixels
    let fontSize := size.toPixels
    ("text", #[("x", x), ("y", y), ("font-size", fontSize), ("text", content)])

The Element.toHtml function has also been modified to incorporate these changes:

def Element.toHtml {f : Frame} (e : Element f) : Html := Id.run do
  let mut (tag, args) := e.shape.toHtmlData
  let mut children := #[]

  if let .text _ content _ := e.shape then
    children := #[.text content]  -- adding children <text>
  
  ...

  return .element tag args #[]
  return .element tag args children

As done for the initial primitives, we have also defined the functions for the new ones:

def path {f} (d : String) : Element f := { shape := .path d }
def ellipse {f} (center : Point f) (rx ry : Size f) : Element f :=
  { shape := .ellipse center rx ry }
def rect {f} (corner : Point f) (width height : Size f) : Element f :=
  { shape := .rect corner width height }
def text {f} (pos : Point f) (content : String) (size : Size f) : Element f :=
  { shape := .text pos content size }