Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

some updates

  • Loading branch information...
commit 2249cf6194c871e39a6b365eaba1e5748be43e3c 1 parent 83b2de2
Larry Diehl authored February 07, 2012
2  src/agda/FRP/JS/DOM.agda
@@ -21,10 +21,12 @@ postulate
21 21
 
22 22
 postulate
23 23
   DOW : Set
  24
+  unattached : DOW
24 25
   left right : DOW → DOW
25 26
   child : String → DOW → DOW
26 27
   events : ∀ {A} → EventType A → DOW → ⟦ Evt A ⟧
27 28
 
  29
+{-# COMPILED_JS unattached require("agda.frp").unattached() #-}
28 30
 {-# COMPILED_JS left function(w) { return w.left(); } #-}
29 31
 {-# COMPILED_JS right function(w) { return w.right(); } #-}
30 32
 {-# COMPILED_JS child function(a) { return function(w) { return w.child(a); }; } #-}
2  src/js/agda.frp.js
@@ -7,7 +7,7 @@ define(["agda.frp.signal","agda.frp.time"],function(signal,time) { return {
7 7
     empty: signal.empty,
8 8
     geolocation: signal.geolocation,
9 9
     reactimate: signal.reactimate,
10  
-    dow: signal.dow,
  10
+    unattached: signal.unattached,
11 11
     // Re-export agda.frp.time
12 12
     seconds: time.seconds,
13 13
     minutes: time.minutes,
4  src/js/agda.frp.signal.js
@@ -789,7 +789,7 @@ define(["agda.frp.taskqueue","agda.mixin"],function(taskqueue,mixin) {
789 789
 	constant: function(value) { return new ConstantBehaviour(value); },
790 790
         empty: function() { return new EmptyBehaviour(); },
791 791
 	geolocation: function() { return geolocation; },
792  
-	reactimate: function(f) { return f(new DOW())(taskqueue.singleton.time); },
793  
-        dow: function() { return new DOW(); }
  792
+        unattached: function() { return new DOW(); },
  793
+	reactimate: function(f) { return f(new DOW())(taskqueue.singleton.time); }
794 794
     };
795 795
 });
2  test/agda/FRP/JS/QUnit.agda
@@ -14,7 +14,7 @@ data Test : Set where
14 14
   _,_ : Test → Test → Test
15 15
   ok : String → (b : {t : ⊤} → Bool) → {b✓ : True b} → Test
16 16
   ok! : String → (b : {t : ⊤} → Bool) → Test
17  
-  ok[t] : String → (b : ⟦ Beh ⟨ Bool ⟩ ⟧) → Test
  17
+  ok : String → (b : ⟦ Beh ⟨ Bool ⟩ ⟧) → Test
18 18
 
19 19
 data TestSuite : Set where
20 20
   ε : TestSuite
20  test/agda/FRP/JS/Test/Behaviour.agda
@@ -5,7 +5,7 @@ open import FRP.JS.Delay using ( _ms )
5 5
 open import FRP.JS.Behaviour
6 6
 open import FRP.JS.Event using ( ∅ )
7 7
 open import FRP.JS.Bool using ( Bool ; not ; true )
8  
-open import FRP.JS.QUnit using ( TestSuite ; ok[t] ; test ; _,_ ; ε )
  8
+open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ ; ε )
9 9
 
10 10
 module FRP.JS.Test.Behaviour where
11 11
 
@@ -17,15 +17,15 @@ _≟*_ = map2 _≟_
17 17
 tests : TestSuite
18 18
 tests =
19 19
   ( test "≟*"
20  
-    ( ok[t] "[ 1 ] ≟* [ 1 ]" ([ 1 ] ≟* [ 1 ])
21  
-    , ok[t] "[ 1 ] ≟* [ 0 ]" (not* ([ 1 ] ≟* [ 0 ]))
22  
-    , ok[t] "[ 0 ] ≟* [ 1 ]" (not* ([ 0 ] ≟* [ 1 ])) )
  20
+    ( ok◇ "[ 1 ] ≟* [ 1 ]" ([ 1 ] ≟* [ 1 ])
  21
+    , ok◇ "[ 1 ] ≟* [ 0 ]" (not* ([ 1 ] ≟* [ 0 ]))
  22
+    , ok◇ "[ 0 ] ≟* [ 1 ]" (not* ([ 0 ] ≟* [ 1 ])) )
23 23
   , test "map"
24  
-    ( ok[t] "map suc [ 0 ] ≟* [ 1 ]" (map suc [ 0 ] ≟* [ 1 ])
25  
-    , ok[t] "map suc [ 1 ] ≟* [ 1 ]" (not* (map suc [ 1 ] ≟* [ 1 ])) )
  24
+    ( ok◇ "map suc [ 0 ] ≟* [ 1 ]" (map suc [ 0 ] ≟* [ 1 ])
  25
+    , ok◇ "map suc [ 1 ] ≟* [ 1 ]" (not* (map suc [ 1 ] ≟* [ 1 ])) )
26 26
   , test "join"
27  
-    ( ok[t] "join (map [ suc ] [ 0 ] ) ≟* [ 1 ]" (join (map (λ n → [ suc n ]) [ 0 ]) ≟* [ 1 ])
28  
-    , ok[t] "join (map [ suc ] [ 1 ]) ≟* [ 1 ]" (not* (join (map (λ n → [ suc n ]) [ 1 ]) ≟* [ 1 ])) )
  27
+    ( ok◇ "join (map [ suc ] [ 0 ] ) ≟* [ 1 ]" (join (map (λ n → [ suc n ]) [ 0 ]) ≟* [ 1 ])
  28
+    , ok◇ "join (map [ suc ] [ 1 ]) ≟* [ 1 ]" (not* (join (map (λ n → [ suc n ]) [ 1 ]) ≟* [ 1 ])) )
29 29
   , test "hold"
30  
-    ( ok[t] "hold 1 ∅ ≟* [ 1 ]" (hold 1 ∅ ≟* [ 1 ])
31  
-    , ok[t] "hold 0 ∅ ≟* [ 1 ]" (not* (hold 0 ∅ ≟* [ 1 ])) ) )
  30
+    ( ok◇ "hold 1 ∅ ≟* [ 1 ]" (hold 1 ∅ ≟* [ 1 ])
  31
+    , ok◇ "hold 0 ∅ ≟* [ 1 ]" (not* (hold 0 ∅ ≟* [ 1 ])) ) )
60  test/agda/FRP/JS/Test/DOM.agda
@@ -5,73 +5,69 @@ open import FRP.JS.Time using ( Time ; epoch )
5 5
 open import FRP.JS.Delay using ( _ms )
6 6
 open import FRP.JS.Behaviour
7 7
 open import FRP.JS.Bool using ( Bool ; not ; true )
8  
-open import FRP.JS.QUnit using ( TestSuite ; ok[t] ; test ; _,_ ; ε )
  8
+open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ ; ε )
9 9
 
10 10
 module FRP.JS.Test.DOM where
11 11
 
12  
-postulate
13  
-  withDOW : {A : Set} → ((w : DOW) → A) → A
14  
-
15  
-{-# COMPILED_JS withDOW function(A) { return function(f) {
16  
-  return f(require("agda.frp").dow());
17  
-}; } #-}
  12
+withDOW : {A : Set} → ((w : DOW) → A) → A
  13
+withDOW f = f unattached
18 14
 
19 15
 tests : TestSuite
20 16
 tests =
21 17
   ( test "≟*"
22  
-    ( ok[t] "[] ≟* []"
  18
+    ( ok "[] ≟* []"
23 19
       (withDOW λ w → [] {w} ≟* [])
24  
-    , ok[t] "[] ++ [] ≟* []"
  20
+    , ok "[] ++ [] ≟* []"
25 21
       (withDOW λ w → [] {left w} ++ [] ≟* []) )
26 22
   , test "attr"
27  
-    ( ok[t] "attr class [ alpha ] ≟* attr class [ alpha ]"
  23
+    ( ok "attr class [ alpha ] ≟* attr class [ alpha ]"
28 24
       (withDOW λ w → attr {w} "class" [ "alpha" ] ≟* attr "class" [ "alpha" ])
29  
-    , ok[t] "attr foo [ alpha ] ≟* attr foo [ alpha ]"
  25
+    , ok "attr foo [ alpha ] ≟* attr foo [ alpha ]"
30 26
       (withDOW λ w → attr {w} "foo" [ "alpha" ] ≟* attr "foo" [ "alpha" ])
31  
-    , ok[t] "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ] ++ attr bar [ alpha ]"
  27
+    , ok "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ] ++ attr bar [ alpha ]"
32 28
       (withDOW λ w → attr {left w} "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ] ≟* attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ])
33  
-    , ok[t] "attr class [ beta ] ≟* attr class [ alpha ]"
  29
+    , ok "attr class [ beta ] ≟* attr class [ alpha ]"
34 30
       (withDOW λ w → not* (attr {w} "class" [ "beta" ] ≟* attr "class" [ "alpha" ]))
35  
-    , ok[t] "attr foo [ alpha ] ≟* attr class [ alpha ]"
  31
+    , ok "attr foo [ alpha ] ≟* attr class [ alpha ]"
36 32
       (withDOW λ w → not* (attr {w} "foo" [ "alpha" ] ≟* attr "class" [ "alpha" ]))
37  
-    , ok[t] "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ]"
  33
+    , ok "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ]"
38 34
       (withDOW λ w → not* (attr {left w} "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ] ≟* attr "foo" [ "alpha" ])) )
39 35
   , test "text"
40  
-    ( ok[t] "text [ abc ] ≟* text [ abc ]"
  36
+    ( ok "text [ abc ] ≟* text [ abc ]"
41 37
       (withDOW λ w → text {w} [ "abc" ] ≟* text [ "abc" ])
42  
-    , ok[t] "text [ a ] ≟* text [ abc ]"
  38
+    , ok "text [ a ] ≟* text [ abc ]"
43 39
       (withDOW λ w → not* (text {w} [ "a" ] ≟* text [ "abc" ]))
44  
-    , ok[t] "[] ≟* text [ abc ]"
  40
+    , ok "[] ≟* text [ abc ]"
45 41
       (withDOW λ w → not* ([] ≟* text {w} [ "abc" ]))
46  
-    , ok[t] "text [ abc ] ++ [] ≟* text [ abc ]"
  42
+    , ok "text [ abc ] ++ [] ≟* text [ abc ]"
47 43
       (withDOW λ w → text {left w} [ "abc" ] ++ [] ≟* (text [ "abc" ]))
48  
-    , ok[t] "[] ++ text [ abc ] ≟* text [ abc ]"
  44
+    , ok "[] ++ text [ abc ] ≟* text [ abc ]"
49 45
       (withDOW λ w → [] ++ text {right w} [ "abc" ] ≟* (text [ "abc" ])) )
50 46
   , test "element"
51  
-    ( ok[t] "element p (text [ abc ]) ≟* element p (text [ abc ])"
  47
+    ( ok "element p (text [ abc ]) ≟* element p (text [ abc ])"
52 48
       (withDOW λ w → element "p" {w} (text [ "abc" ]) ≟* element "p" (text [ "abc" ]))
53  
-    , ok[t] "element p (text [ a ]) ≟* element p (text [ abc ])"
  49
+    , ok "element p (text [ a ]) ≟* element p (text [ abc ])"
54 50
       (withDOW λ w → not* (element "p" {w} (text [ "a" ]) ≟* element "p" (text [ "abc" ])))
55  
-    , ok[t] "element div (attr class [ alpha ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
  51
+    , ok "element div (attr class [ alpha ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
56 52
       (withDOW λ w → element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ]) ≟* element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ]))
57  
-    , ok[t] "element div (attr class [ beta ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
  53
+    , ok "element div (attr class [ beta ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
58 54
       (withDOW λ w → not* (element "div" {w} (attr "class" [ "beta" ] ++ text [ "abc" ]) ≟* element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ])))
59  
-    , ok[t] "element p (text [ abc ]) ≟* element p (text [ abc ])"
  55
+    , ok "element p (text [ abc ]) ≟* element p (text [ abc ])"
60 56
       (withDOW λ w → element "p" {w} (text [ "abc" ]) ≟* element "p" (text [ "abc" ]))
61  
-    , ok[t] "element p (text [ a ]) ++ element p (text [ b ]) ≟* element p (text [ a ])"
  57
+    , ok "element p (text [ a ]) ++ element p (text [ b ]) ≟* element p (text [ a ])"
62 58
       (withDOW λ w → not* (element "p" {left w} (text [ "a" ]) ++ element "p" (text [ "b" ]) ≟* element "p" (text [ "a" ])))
63 59
       )
64 60
   , test "join"
65  
-    ( ok[t] "text (join (map [ x ] [ abc ])) ≟* text [ abc ]"
  61
+    ( ok "text (join (map [ x ] [ abc ])) ≟* text [ abc ]"
66 62
       (withDOW λ w → text {w} (join (map (λ s → [ s ]) [ "abc" ])) ≟* text [ "abc" ])
67  
-    , ok[t] "join (map (text [ x ]) [ abc ]) ≟* text [ abc ]"
  63
+    , ok "join (map (text [ x ]) [ abc ]) ≟* text [ abc ]"
68 64
       (withDOW λ w → join (map (λ s → text {w} [ s ]) [ "abc" ]) ≟* text [ "abc" ])
69  
-   , ok[t] "element p (join (map (attr foo [ x ]) [ alpha ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
  65
+   , ok "element p (join (map (attr foo [ x ]) [ alpha ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
70 66
       (withDOW λ w → element "p" {w} (join (map (λ s → attr "foo" [ s ]) [ "alpha" ]) ++ join (map (λ s → attr "bar" [ s ]) [ "alpha" ])) ≟* element "p" (attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ]))
71  
-   , ok[t] "element p (join (map (attr foo [ x ]) [ beta ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
  67
+   , ok "element p (join (map (attr foo [ x ]) [ beta ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
72 68
       (withDOW λ w → not* (element "p" {w} (join (map (λ s → attr "foo" [ s ]) [ "beta" ]) ++ join (map (λ s → attr "bar" [ s ]) [ "alpha" ])) ≟* element "p" (attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ])))
73  
-    , ok[t] "text (join (map [ x ] [ a ])) ≟* text [ abc ]"
  69
+    , ok "text (join (map [ x ] [ a ])) ≟* text [ abc ]"
74 70
       (withDOW λ w → not* (text {w} (join (map (λ s → [ s ]) [ "a" ])) ≟* text [ "abc" ]))
75  
-    , ok[t] "join (map (text [ x ]) [ a ]) ≟* text [ abc ]"
  71
+    , ok "join (map (text [ x ]) [ a ]) ≟* text [ abc ]"
76 72
       (withDOW λ w → not* (join (map (λ s → text {w} [ s ]) [ "a" ]) ≟* text [ "abc" ])) ) )
77 73
 
4  test/js/agda.qunit.js
@@ -6,7 +6,9 @@ require(["agda.frp.taskqueue", "qunit.js"],function(taskqueue) {
6 6
 	    "_,_": function(test1,test2) { test1(visitor); test2(visitor); },
7 7
 	    "ok": function(name,fun) { ok(fun(),name); },
8 8
 	    "ok!": function(name,fun) { ok(fun(),name); },
9  
-	    "ok[t]": function(name,fun) { ok(fun(taskqueue.singleton.time).value,name); },
  9
+            // TODO: make ok◇ use setInterval + setTimeout to search for
  10
+            // the value appearing later,  mimicking LTL "eventually" semantics
  11
+	    "ok◇": function(name,fun) { ok(fun(taskqueue.singleton.time).value,name); },
10 12
 	    "test": function(name,tests) { test(name,function() { tests(visitor); }); },
11 13
 	    "suite": function(name,tests) { module(name); tests(visitor); }
12 14
 	};

0 notes on commit 2249cf6

Please sign in to comment.
Something went wrong with that request. Please try again.