mattpolzin/incomplete_dom_ex.html

## incomplete_dom_ex.html
<html>
 <head>
  <meta charset='utf-8'>
  <link rel="stylesheet" type="text/css" href="web.css" media="screen"/>
 </head>
 <body>
  <script type='text/javascript' src='build/exec/web.js'></script>
 </body>
</html>

## incomplete_dom_ex.idr
module Web

import Data.Vect
import Data.Fuel
import Data.String
import Data.Nat

import JS
import Web.Dom
import Web.Html

import Nested

edgeDescriptor : Edge -> String
edgeDescriptor Vert = "vertical"
edgeDescriptor Horiz = "horizontal"

cornerDescriptor : Corner -> String
cornerDescriptor TopLeft = "top-left"
cornerDescriptor Bottomleft = "bottom-left"
cornerDescriptor TopRight = "top-right"
cornerDescriptor BottomRight = "bottom-right"

classify : (t -> String) -> t -> String
classify f x = (f x) ++ "-cell"

divWithClass : String -> JSIO HTMLDivElement
divWithClass x =
  newElement Div [ className =. x ]

spanWithClass : String -> JSIO HTMLSpanElement
spanWithClass x =
  newElement Span [ className =. x ]

cell : Cell -> JSIO HTMLSpanElement
cell (E x) = spanWithClass $ classify edgeDescriptor x
cell (C x) = spanWithClass $ classify cornerDescriptor x
cell Blank = spanWithClass $ classify (const "blank") ()

row : Traversable t => t Cell -> JSIO (t HTMLSpanElement)
row = traverse cell

grid : Traversable t => Traversable t' => t (t' Cell) -> JSIO (t (t' HTMLSpanElement))
grid = traverse row

addGrid : HTMLElement -> Traversable t => Traversable t' => t (t' Cell) -> JSIO ()
addGrid elem gridCells = for_ !(grid gridCells) $ \row =>
                           do rowDiv <- divWithClass "grid-row"
                              ignore $ elem `appendChild` rowDiv
                              for_ row $ \cell =>
                                rowDiv `appendChild` cell

inputDiv : JSIO (HTMLInputElement, HTMLDivElement)
inputDiv = do
  div <- createElement Div
  txt <- newElement Input [ type =. "text" ]
  ignore $ div `appendChild` txt
  pure (txt, div)

loop : Fuel -> Nat -> (prev : Maybe HTMLDivElement) -> HTMLInputElement -> JSIO ()
loop Dry _ _ _ = pure ()
loop (More fuel) size prev txt = do
  traverse_ (!body `removeChild`) prev
  gridDiv <- divWithClass "grid"
  ignore $ !body `appendChild` gridDiv
  addGrid (up gridDiv) (nestedBoxes size)

  oninput txt ?> do inp <- txt `get` value
                    let posNum : Maybe Nat = parsePositive inp
                    case posNum of
                         Nothing  => loop fuel size (Just gridDiv) txt
                         (Just x) => loop fuel x    (Just gridDiv) txt


prog : Fuel -> JSIO ()
prog Dry = pure ()
prog (More fuel) = do
  (txt, inputs) <- inputDiv
  ignore $ !body `appendChild` inputs

  loop fuel 20 Nothing txt

partial
main : IO ()
main = runJS $ prog forever

## incomplete_dom_ex.ipkg
package web

modules = Web
main = Web

executable = "web.js"

opts = "--codegen javascript"
depends = nested-squares, elab-util, sop, dom
	<html>
	<head>
	<meta charset='utf-8'>
	<link rel="stylesheet" type="text/css" href="web.css" media="screen"/>
	</head>
	<body>
	<script type='text/javascript' src='build/exec/web.js'></script>
	</body>
	</html>
	module Web

	import Data.Vect
	import Data.Fuel
	import Data.String
	import Data.Nat

	import JS
	import Web.Dom
	import Web.Html

	import Nested

	edgeDescriptor : Edge -> String
	edgeDescriptor Vert = "vertical"
	edgeDescriptor Horiz = "horizontal"

	cornerDescriptor : Corner -> String
	cornerDescriptor TopLeft = "top-left"
	cornerDescriptor Bottomleft = "bottom-left"
	cornerDescriptor TopRight = "top-right"
	cornerDescriptor BottomRight = "bottom-right"

	classify : (t -> String) -> t -> String
	classify f x = (f x) ++ "-cell"

	divWithClass : String -> JSIO HTMLDivElement
	divWithClass x =
	newElement Div [ className =. x ]

	spanWithClass : String -> JSIO HTMLSpanElement
	spanWithClass x =
	newElement Span [ className =. x ]

	cell : Cell -> JSIO HTMLSpanElement
	cell (E x) = spanWithClass $ classify edgeDescriptor x
	cell (C x) = spanWithClass $ classify cornerDescriptor x
	cell Blank = spanWithClass $ classify (const "blank") ()

	row : Traversable t => t Cell -> JSIO (t HTMLSpanElement)
	row = traverse cell

	grid : Traversable t => Traversable t' => t (t' Cell) -> JSIO (t (t' HTMLSpanElement))
	grid = traverse row

	addGrid : HTMLElement -> Traversable t => Traversable t' => t (t' Cell) -> JSIO ()
	addGrid elem gridCells = for_ !(grid gridCells) $ \row =>
	do rowDiv <- divWithClass "grid-row"
	ignore $ elem `appendChild` rowDiv
	for_ row $ \cell =>
	rowDiv `appendChild` cell

	inputDiv : JSIO (HTMLInputElement, HTMLDivElement)
	inputDiv = do
	div <- createElement Div
	txt <- newElement Input [ type =. "text" ]
	ignore $ div `appendChild` txt
	pure (txt, div)

	loop : Fuel -> Nat -> (prev : Maybe HTMLDivElement) -> HTMLInputElement -> JSIO ()
	loop Dry _ _ _ = pure ()
	loop (More fuel) size prev txt = do
	traverse_ (!body `removeChild`) prev
	gridDiv <- divWithClass "grid"
	ignore $ !body `appendChild` gridDiv
	addGrid (up gridDiv) (nestedBoxes size)

	oninput txt ?> do inp <- txt `get` value
	let posNum : Maybe Nat = parsePositive inp
	case posNum of
	Nothing => loop fuel size (Just gridDiv) txt
	(Just x) => loop fuel x (Just gridDiv) txt


	prog : Fuel -> JSIO ()
	prog Dry = pure ()
	prog (More fuel) = do
	(txt, inputs) <- inputDiv
	ignore $ !body `appendChild` inputs

	loop fuel 20 Nothing txt

	partial
	main : IO ()
	main = runJS $ prog forever
	package web

	modules = Web
	main = Web

	executable = "web.js"

	opts = "--codegen javascript"
	depends = nested-squares, elab-util, sop, dom