Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

ECMAScript back end for Functional Reactive Programming in Agda

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 demo
Octocat-spinner-32 src
Octocat-spinner-32 test
Octocat-spinner-32 .gitignore
Octocat-spinner-32 LICENSE Added Larry Diehl to the list of copyright holders. February 13, 2012
Octocat-spinner-32 LICENSE-requirejs First commit. September 12, 2011
Octocat-spinner-32 LICENSE.qunit
Octocat-spinner-32 Makefile Join Behaviour February 11, 2012
Octocat-spinner-32 README
README
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.agda

this 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.

Something went wrong with that request. Please try again.