An implementation of Functional Reactive Programming for building HTML applications in Agda.
To build and application, start with an HTML file:
<html>
<head>
<title>Hello World</title>
<script data-main="agda.frp.main" src="require.js"></script>
</head>
<body>
<h1>A greeting</h1>
<p class="agda" data-agda="Demo.Hello"></p>
</body>
</html>This is just a regular old HTML file, which loads the agda.frp.main JavaScript module (using require.js, but any AMD-compliant JavaScript module loader should work). The important part is:
<p class="agda" data-agda="Demo.Hello"></p>The "agda" class and data-agda attribute indicates that an Agda program should be executed inside the annotated node.
Now write an Agda program:
open import FRP.JS.Behaviour using ( Beh ; [_] )
open import FRP.JS.DOM using ( DOM ; text )
open import FRP.JS.RSet using ( ⟦_⟧ )
module Demo.Hello where
main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = text ["Hello, world."]This program creates a text node whose content is always "Hello, World."
Compile (using the darcs snapshot of Agda 2.2.11):
agda --js Demo/Hello.agdathis will create a bunch of js files such as jAgda.Demo.Hello.js.
Put all the .js files (including require.js and the agda.frp.*.js files) in the same directory as hello.html.
Load hello.html in a browser, and enjoy.
There are unit tests in FRP.JS.Test, which link against John Resig's QUnit (http://docs.jquery.com/QUnit). To run the tests, first "make tests", then load build/tests.html in a browser.