GitHub - krkx/agda-frp-js: ECMAScript back end for Functional Reactive Programming in Agda

krkx / agda-frp-js Public

forked from agda/agda-frp-js

Notifications You must be signed in to change notification settings
Fork 0
Star 1

ECMAScript back end for Functional Reactive Programming in Agda

View license

1 star 12 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 64 Commits
demo		demo
src		src
test		test
.gitignore		.gitignore
LICENSE		LICENSE
LICENSE-requirejs		LICENSE-requirejs
LICENSE.qunit		LICENSE.qunit
Makefile		Makefile
README		README

Repository files navigation

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.