-
Notifications
You must be signed in to change notification settings - Fork 108
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #315 from google-research/dex-plot-library
Implement plotting in Dex instead of Haskell
- Loading branch information
Showing
32 changed files
with
813 additions
and
288 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,181 @@ | ||
| '# Vector graphics library | ||
|
|
||
| Point : Type = (Float & Float) | ||
|
|
||
| data Geom = | ||
| PointGeom | ||
| Circle Float | ||
| Rectangle Float Float -- width, height | ||
| Line Point | ||
|
|
||
| -- HTML color string. TODO: consider an RGB triple instead | ||
| HtmlColor : Type = String | ||
|
|
||
| -- TODO: we should add overloaded string literals so we don't need this | ||
| def str (n:Int) ?-> (s:(Fin n=>Char)) : String = AsList _ s | ||
|
|
||
| black : HtmlColor = str "black" | ||
| white : HtmlColor = str "white" | ||
| gray : HtmlColor = str "gray" | ||
| red : HtmlColor = str "red" | ||
| green : HtmlColor = str "green" | ||
| blue : HtmlColor = str "blue" | ||
|
|
||
| GeomStyle : Type = | ||
| { fillColor : Maybe HtmlColor | ||
| & strokeColor : Maybe HtmlColor | ||
| & strokeWidth : Int } | ||
|
|
||
| defaultGeomStyle : GeomStyle = | ||
| { fillColor = Nothing | ||
| , strokeColor = Just black | ||
| , strokeWidth = 1 } | ||
|
|
||
| -- TODO: consider sharing attributes among a set of objects for efficiency | ||
| data Diagram = MkDiagram (List (GeomStyle & Point & Geom)) | ||
|
|
||
| instance monoidDiagram : Monoid Diagram where | ||
| mempty = MkDiagram mempty | ||
| mcombine = \(MkDiagram d1) (MkDiagram d2). MkDiagram $ d1 <> d2 | ||
|
|
||
| def concatDiagrams (diagrams:n=>Diagram) : Diagram = | ||
| MkDiagram $ concat for i. | ||
| (MkDiagram d) = diagrams.i | ||
| d | ||
|
|
||
| -- TODO: arbitrary affine transformations. Our current representation of | ||
| -- rectangles and circles means we can only do scale/flip/rotate90. | ||
| -- Should we use lenses/isomorphisms for these instead? | ||
| def applyTransformation | ||
| (transformPoint: Point -> Point) | ||
| (transformGeom: Geom -> Geom) | ||
| (d:Diagram) : Diagram = | ||
| (MkDiagram (AsList _ objs)) = d | ||
| (MkDiagram $ AsList _ for i. | ||
| (attr, p, geom) = objs.i | ||
| (attr, transformPoint p, transformGeom geom)) | ||
|
|
||
| flipY : Diagram -> Diagram = | ||
| applyTransformation (\(x,y). (x, -y)) \geom. case geom of | ||
| PointGeom -> PointGeom | ||
| Circle r -> Circle r | ||
| Rectangle w h -> Rectangle w h | ||
| Line (x, y) -> Line (x, -y) | ||
|
|
||
| def scale (s:Float) : (Diagram -> Diagram) = | ||
| applyTransformation ( \(x,y). (s * x, s * y) ) \geom. case geom of | ||
| PointGeom -> PointGeom | ||
| Circle r -> Circle (s * r) | ||
| Rectangle w h -> Rectangle (s * w) (s * h) | ||
| Line (x, y) -> Line (s * x, s * y) | ||
|
|
||
| def moveXY ((offX, offY) : Point) : (Diagram -> Diagram) = | ||
| applyTransformation (\(x,y). (x + offX, y + offY) ) id | ||
|
|
||
| def singletonDefault (geom:Geom) : Diagram = | ||
| MkDiagram $ AsList _ [(defaultGeomStyle, (0.0, 0.0), geom)] | ||
|
|
||
| -- TODO: should really allow nullary functions with `def` | ||
| pointDiagram : Diagram = singletonDefault PointGeom | ||
| def circle (r:Float) : Diagram = singletonDefault $ Circle r | ||
| def rect (w:Float) (h:Float) : Diagram = singletonDefault $ Rectangle w h | ||
| def line (p:Point) : Diagram = singletonDefault $ Line p | ||
|
|
||
| def updateGeom (update: GeomStyle -> GeomStyle) (d:Diagram) : Diagram = | ||
| (MkDiagram (AsList _ objs)) = d | ||
| MkDiagram $ AsList _ for i. | ||
| (attr , geoms) = objs.i | ||
| (update attr, geoms) | ||
|
|
||
| def setFillColor (c:HtmlColor) : Diagram -> Diagram = updateGeom $ setAt #fillColor (Just c) | ||
| def setStrokeColor (c:HtmlColor) : Diagram -> Diagram = updateGeom $ setAt #strokeColor (Just c) | ||
| def setStrokeWidth (w:Int) : Diagram -> Diagram = updateGeom $ setAt #strokeWidth w | ||
| -- TODO: argumentless def! | ||
| removeStroke : Diagram -> Diagram = updateGeom $ setAt #strokeColor Nothing | ||
| removeFill : Diagram -> Diagram = updateGeom $ setAt #fillColor Nothing | ||
|
|
||
| '## Serialization to SVG string | ||
|
|
||
| def quote (s:String) : String = str "\"" <> s <> str "\"" | ||
|
|
||
| def (<+>) (s1:String) (s2:String) : String = s1 <> str " " <> s2 | ||
|
|
||
| def selfClosingBrackets (s:String) : String = str "<" <> s <> str "/>" | ||
|
|
||
| def tagBrackets (tag:String) (s:String) : String = | ||
| str "<" <> tag <> str ">" <> s <> str "</" <> tag <> str ">" | ||
|
|
||
| def tagBracketsAttr (tag:String) (attr:String) (s:String) : String = | ||
| str "<" <> tag <+> attr <> str ">" <> s <> str "</" <> tag <> str ">" | ||
|
|
||
| def makeAttr (attr:String) (val:String) : String = | ||
| attr <> str "=" <> quote val | ||
|
|
||
| def optionalStr (c: Maybe String) : String = | ||
| case c of | ||
| Nothing -> str "none" | ||
| Just s -> s | ||
|
|
||
| def attrString (attr:GeomStyle) : String = | ||
| ( makeAttr (str "stroke") (optionalStr $ getAt #strokeColor attr) | ||
| <+> makeAttr (str "fill") (optionalStr $ getAt #fillColor attr) | ||
| <+> makeAttr (str "stroke-width") (show $ getAt #strokeWidth attr)) | ||
|
|
||
| def pointAttrString (attr:GeomStyle) : String = | ||
| ( makeAttr (str "stroke") (optionalStr $ getAt #strokeColor attr) | ||
| <+> makeAttr (str "fill") (optionalStr $ getAt #strokeColor attr) | ||
| <+> makeAttr (str "stroke-width") (show $ getAt #strokeWidth attr)) | ||
|
|
||
| def renderGeom (attr:GeomStyle) ((x,y):Point) (geom:Geom) : String = | ||
| case geom of | ||
| PointGeom -> | ||
| tagBracketsAttr (str "g") (pointAttrString attr) $ selfClosingBrackets $ | ||
| (str "circle" <+> | ||
| str "cx=" <> quote (show x) <> | ||
| str "cy=" <> quote (show y) <> | ||
| str "r=\"1\"") | ||
| Circle r -> | ||
| tagBracketsAttr (str "g") (attrString attr) $ selfClosingBrackets $ | ||
| (str "circle" <+> | ||
| str "cx=" <> quote (show x) <> | ||
| str "cy=" <> quote (show y) <> | ||
| str "r=" <> quote (show r)) | ||
| Rectangle w h -> | ||
| tagBracketsAttr (str "g") (attrString attr) $ selfClosingBrackets $ | ||
| (str "rect" <+> | ||
| str "width=" <> quote (show w) <> | ||
| str "height=" <> quote (show h) <> | ||
| str "x=" <> quote (show (x - (w/2.0))) <> | ||
| str "y=" <> quote (show (y - (h/2.0)))) | ||
|
|
||
| BoundingBox : Type = (Point & Point) | ||
|
|
||
| def renderSVG (d:Diagram) (bounds:BoundingBox) : String = | ||
| ((xmin, ymin), (xmax, ymax)) = bounds | ||
| imgWidth = 400.0 | ||
| scaleFactor = imgWidth / (xmax - xmin) | ||
| imgHeight = (ymax - ymin) * scaleFactor | ||
| (MkDiagram (AsList _ objs)) = d |> flipY |> scale scaleFactor | ||
| viewBoxStr = makeAttr (str "viewBox") $ | ||
| (show (xmin * scaleFactor) <+> show (-(ymax * scaleFactor)) <+> | ||
| show imgWidth <+> show imgHeight) | ||
| svgAttrStr = ( makeAttr (str "width" ) (show imgWidth) | ||
| <+> makeAttr (str "height") (show imgHeight) | ||
| <+> viewBoxStr) | ||
| tagBracketsAttr (str "svg") svgAttrStr $ | ||
| concat for i. | ||
| (attr, pos, geom) = objs.i | ||
| renderGeom attr pos geom | ||
|
|
||
| '## Derived convenience methods and combinators | ||
|
|
||
| moveX : Float -> Diagram -> Diagram = \x. moveXY (x, 0.0) | ||
| moveY : Float -> Diagram -> Diagram = \y. moveXY (0.0, y) | ||
|
|
||
| -- mydiagram : Diagram = | ||
| -- ( (circle 7.0 |> moveXY (20.0, 20.0) |> setFillColor blue |> setStrokeColor red) | ||
| -- <> (circle 5.0 |> moveXY (40.0, 40.0)) | ||
| -- <> (rect 10.0 20.0 |> moveXY (5.0, 10.0) |> setStrokeColor red) | ||
| -- ) | ||
|
|
||
| -- :html renderSVG mydiagram ((0.0, 0.0), (100.0, 50.0)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.