p5.js is a JS client-side library for creating graphic and interactive experiences, based on the core principles of Processing.
P5Idr aims to prove access to this library through the programming language Idris to allow for creative coding. Currently, this library is still a work in progress, but has plans to eventually provide bindings for all p5.js functions along with various proofs to allow for experimentation with theorem proving without deriving everything from the ground up.
Below is an example of a basic sketch that moves a rectangle across the screen. (NOTE: Because this is still a work in progress, all of this is subject to change at any time):
module Main
import Data.Ref
import P5Idr
setup : IO ()
setup = P5Idr.Setup.setup $ do
createCanvas 400 400
width <- getWidth {ty=Nat}
height <- getHeight {ty=Nat}
putStrLn $ "Width: " ++ show width
putStrLn $ "Height: " ++ show height
draw : IORef Double -> IO ()
draw xRef = P5Idr.Setup.draw $ do
background (Gray 0)
width <- getWidth
x <- readRef xRef
stroke (Gray 255)
fill (RGB 255 0 0)
rect (MkRect x 10 50 50)
ellipse (MkCircle (x + 25) 100 50)
if x > width then writeRef xRef (-50) else writeRef xRef (x + 1)
main : IO ()
main = do
x <- newRef 0
setup *> draw x