import Vizagrams -- Working with Graphical Marks open GeometricPrimitive open VizBackend open GraphicalPrimitive open ProofWidgets Svg open GraphicalMark open FreeMonad open LinearAlgebra open Envelope open Sty /- d = Arrow() draw(d, height=100) -/ -- Criando Mark Arrow structure Arrow where pts : Vec2 × Vec2 headsize : Float headstyle: Sty.Style headmark : Mark instance : MarkInterface Arrow where θ m := let line : 𝕋 Mark := NewLine (m.pts.fst) (m.pts.snd) {strokeColor := Color.mk 1 0 0 , strokeWidth := Sty.StyleSize.px 10 } let 𝕞 : 𝕋 Mark := envelopePositionMarks line (m.pts.snd - m.pts.fst) m.headmark flat ( line + 𝕞) instance : Coe Arrow Mark where coe m := Mark.mk m -- Criando Mark de poligono regular structure RegularPolygon where center : Vec2 := ![0,0] sides : Nat size : Float h : sides >= 3 := by decide style : Sty.Style instance : ToString RegularPolygon where toString p := s!"Regular Polygon with {p.sides} sides of size {p.size}" def findPointbyAngle (x : Float) : Vec2 := ![Float.cos x , Float.sin x] def create_list (n : ℕ) : Array ℕ := Array.range n |>.map (λ x => x + 1) def multiply_by_scalar (lst : Array ℕ) (scalar : Float) : Array Float := lst.map (λ x => ↑x.toFloat * scalar) def regToPoly (p : RegularPolygon) : Array (Vec2) := let passo : Float := ( 2 * π ) / (p.sides.toFloat) let listn : Array ℕ := create_list (p.sides) let Arr := multiply_by_scalar listn passo Array.map findPointbyAngle Arr instance : MarkInterface RegularPolygon where θ h := NewPolygon (regToPoly h) h.style instance : Coe RegularPolygon Mark where coe m := Mark.mk m -- Desenhando uma Arrow com um Triangulo como HeadMark def triangle : RegularPolygon := {center := ![0, 0], sides := 3 , size := 1, style := {fillColor := Color.mk 0 0 1 }} #html draw₁ triangle def arrow₁ : 𝕋 Mark := { pts := (![0, 0], ![2, 0]), headsize := 0.3, headstyle := {fillColor := Color.mk 1 0 0}, headmark := Mark.mk { center := ![0, 0], sides := 3, size := 0.3, style := {fillColor := Color.mk 1 0 0} : RegularPolygon} : Arrow } #html draw₁ arrow₁ def 𝕋rotate (y : Float) : FreeMonad.ℍ := ℍ.mk {} (rotate y) #html draw₁ ( 𝕋rotate (π/3) * arrow₁) def 𝕋scale (y : Float) : ℍ := ℍ.mk {} (scale y) #html draw₁ (𝕋scale 0.5 * arrow₁) def 𝕋translate (v : Vec2) : ℍ := ℍ.mk {} (translate v) -- Criando Estrutura d eFace structure Face where center : Vec2 := ![0, 0] size : Float := 1 eyestyle : Style := {} headstyle : Style := {} smile : Float := 0 smilestyle : Style := {} instance : MarkInterface Face where θ f := -- estilos -------------------------------------------- let eyeStyle := { fillColor := some (Color.mk 0 0 1) } ++ f.eyestyle let headStyle := { fillColor := some (Color.mk 1 1 1), strokeColor := some (Color.mk 0 0 0) } ++ f.headstyle let smileStyle := { fillColor := none } ++ f.smilestyle -- cabeça --------------------------------------------- let head : 𝕋 Mark := NewCircle 5 f.center headStyle -- olhos ---------------------------------------------- let eyeOffsetY : Float := 2 let eyeOffsetX : Float := 2 let leftEyeCenter : Vec2 := f.center + ![-eyeOffsetX, eyeOffsetY] let rightEyeCenter : Vec2 := f.center + ![ eyeOffsetX, eyeOffsetY] let eyeLeft : 𝕋 Mark := NewCircle 1 leftEyeCenter eyeStyle let eyeRight : 𝕋 Mark := NewCircle 1 rightEyeCenter eyeStyle let eyes := eyeLeft + eyeRight ------------------------------------------------------- -- >>> sorriso (Quadratic Bézier) <<< ------------------------------------------------------- let moveto : Vec2 := f.center + ![75,250] let qbezier : Vec2 × Vec2 := {fst := f.center + ![(f.center 0) + 150, 300 + f.smile], snd := moveto + ![225,0] } let smile : 𝕋 Mark := NewQBezier moveto qbezier f.smilestyle flat (head + eyes + smile) instance : Coe Face Mark where coe f := Mark.mk f def face₁ : 𝕋 Mark := { center := ![5, 5], size := 0.0001, smile := 100., eyestyle := { fillColor := some (Color.mk 0.5 0.5 1) }, headstyle := {}, smilestyle := { strokeColor := Color.mk 0 0 1, fillColor := Color.mk 0 1 0, strokeWidth := Sty.StyleSize.px 5} : Face } #html draw ( (𝕋scale 1) * face₁) --(BoundingBox.toFrame (boundingBox𝕋 ( face₁)) ) def rectEstilo : Style := { fillColor := some (Color.mk 0.5 0.5 0.5) } def rect₁ : 𝕋 Mark := NewPolygon #[![0,0],![2,0],![2,1],![0,1]] rectEstilo def rectTransladada : 𝕋 Mark := 𝕋translate (![0, -1.5]) * rect₁ def angles : Array Float := (Array.range 11).map (fun i => i.toFloat * π / 10.0) def rotatedArrow (a : Float) : 𝕋 Mark := let headTri : RegularPolygon := { center := ![0, 0], sides := 3, size := a / 10, style := { fillColor := some (Color.mk 1 0 0) } } let arr : Arrow := { pts := (![1, 0], ![2, 0]), headsize := a / 10, headstyle := { fillColor := some (Color.mk 1 0 0) }, headmark := Mark.mk headTri } 𝕋rotate a * (arr : 𝕋 Mark) def allArrows : 𝕋 Mark := let arrowArray := angles.map rotatedArrow if h : arrowArray.size > 0 then arrowArray.foldl (fun acc arr => acc + arr) arrowArray[0] else rotatedArrow 0 def centerCircle : 𝕋 Mark := NewCircle 0.5 ![0, 0] { fillColor := some (Color.mk 0 0 1) } def greyRectangle : 𝕋 Mark := let rectStyle : Style := { fillColor := some (Color.mk 0.5 0.5 0.5) } let rect : 𝕋 Mark := NewPolygon #[![-1,0],![1,0],![1,1],![-1,1]] rectStyle 𝕋translate ![0, -1.5] * rect def finalDrawing : 𝕋 Mark := (centerCircle + greyRectangle) #html draw₁ ((𝕋scale 0.5 * allArrows) + finalDrawing) structure Tree_ where h : Float deriving Inhabited instance : MarkInterface Tree_ where θ t := let height := t.h let trunkStyle : Style := { fillColor := some (Color.mk 0.6 0.3 0.1) } let trunk : 𝕋 Mark := NewPolygon #[ ![-0.25, 0], ![ 0.25, 0], ![ 0.25, height/2], ![-0.25, height/2] ] trunkStyle let leafStyle : Style := { fillColor := some (Color.mk 0 0.8 0) } let bigLeaf : 𝕋 Mark := NewCircle 0.5 ![0,0] leafStyle let angles : Array Float := (Array.range 10).map (fun i => i.toFloat * 0.7) let smallLeaves : Array (𝕋 Mark) := angles.map fun θ => 𝕋translate (![Float.cos θ * 0.5, Float.sin θ * 0.5]) * (NewCircle 0.3 ![0,0] leafStyle : 𝕋 Mark) let leavesTotal : 𝕋 Mark := smallLeaves.foldl (· + ·) bigLeaf let leafOff : Float := height/2 + 0.5 flat (𝕋scale 0.75 * (trunk + ((𝕋translate (![0, leafOff])) * leavesTotal))) instance : Coe Tree_ Mark where coe t := Mark.mk t def diagram : 𝕋 Mark := (Tree_.mk 3) → Tree_.mk 6 #html draw₁ diagram structure Forest where n : Nat instance : MarkInterface Forest where θ f := let half := Float.sqrt (f.n.toFloat) * 0.5 + 1.0 let lcg (s : UInt32) : UInt32 := s * 1664525 + 1013904223 let randF (s : UInt32) : Float × UInt32 := let s' := lcg s (s'.toFloat / 4294967296.0, s') let (_, posArr) := Id.run do let mut s : UInt32 := 4 let mut arr : Array Vec2 := #[] for _ in [: f.n] do let (x, s1) := randF s; s := s1 let (y, s2) := randF s; s := s2 arr := arr.push ![(x * 2 - 1) * half, (y * 2 - 1) * half] pure (s, arr) let treePrimsArr : Array (Array Prim) := posArr.map fun p => flat (𝕋translate p * (𝕋scale 0.001) * (Tree_.mk 2 : 𝕋 Mark)) let allTreePrims : Array Prim := treePrimsArr.foldl (· ++ ·) #[] let bg : 𝕋 Mark := NewPolygon #[ ![-half, -half], ![ half, -half], ![ half, half], ![-half, half] ] { fillColor := some (Color.mk 0.5 0.5 0.5)} let bgPrims := flat bg bgPrims ++ allTreePrims instance : Coe Forest Mark where coe f := Mark.mk f #html draw (Forest.mk 20) (BoundingBox.toFrame (boundingBox𝕋 (Forest.mk 20)))