-
Notifications
You must be signed in to change notification settings - Fork 1
/
example1.agda
135 lines (107 loc) · 5.02 KB
/
example1.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
module example1 where
open import Data.String.Base using (String)
open import Data.Product
open import Data.List.Base using (List; []; _∷_)
open import Data.Bool.Base
open import Function
open import Control.Process.Type
open import FFI.JS as JS
open import FFI.JS.Proc
import FFI.JS.Console as Console
import FFI.JS.Process as Process
import FFI.JS.FS as FS
take-half : String → String
take-half s = substring s 0N (length s / 2N)
drop-half : String → String
drop-half s = substring1 s (length s / 2N)
test-value : Value
test-value = object (("array" , array (array [] ∷ array (array [] ∷ []) ∷ [])) ∷
("object" , array (object [] ∷ object (("a", string "b") ∷ []) ∷ [])) ∷
("string" , array (string "" ∷ string "a" ∷ [])) ∷
("number" , array (number 0N ∷ number 1N ∷ [])) ∷
("bool" , array (bool true ∷ bool false ∷ [])) ∷
("null" , array (null ∷ [])) ∷ [])
test =
fromString (JSON-stringify (fromValue test-value))
===
fromString "{\"array\":[[],[[]]],\"object\":[{},{\"a\":\"b\"}],\"string\":[\"\",\"a\"],\"number\":[0,1],\"bool\":[true,false],\"null\":[null]}"
module _ {A : Set} (_≤_ : A → A → Bool) where
merge-sort-list : (l₀ l₁ : List A) → List A
merge-sort-list [] l₁ = l₁
merge-sort-list l₀ [] = l₀
merge-sort-list (x₀ ∷ l₀) (x₁ ∷ l₁) with x₀ ≤ x₁
... | true = x₀ ∷ merge-sort-list l₀ (x₁ ∷ l₁)
... | false = x₁ ∷ merge-sort-list (x₀ ∷ l₀) l₁
merge-sort-string : String → String → String
merge-sort-string s₀ s₁ = List▹String (merge-sort-list _≤Char_ (String▹List s₀) (String▹List s₁))
mapStringChars : (JSArray Char → JSArray Char) → JSValue → JSValue
mapStringChars f = fromString ∘ JSArray▹String ∘ f ∘ String▹JSArray ∘ toString
reverser : URI → JSProc
reverser d = recv d λ s → send d (mapStringChars JS.reverse s) end
adder : URI → JSProc
adder d = recv d λ s₀ → recv d λ s₁ → send d (s₀ +JS s₁) end
adder-client : URI → JSValue → JSValue → JSProc
adder-client d s₀ s₁ = send d s₀ (send d s₁ (recv d λ _ → end))
module _ (adder-addr reverser-addr : URI)(s : JSValue) where
adder-reverser-client : JSProc
adder-reverser-client =
send reverser-addr s $
send adder-addr s $
recv reverser-addr λ rs →
send adder-addr rs $
recv adder-addr λ res →
end
str-sorter₀ : URI → JSProc
str-sorter₀ d = recv d λ s → send d (mapStringChars sort s) end
str-sorter-client : ∀ {D} → D → JSValue → Proc D JSValue
str-sorter-client d s = send d s $ recv d λ _ → end
module _ (upstream helper₀ helper₁ : URI) where
str-merger : JSProc
str-merger =
recv upstream λ s →
send helper₀ (fromString (take-half (toString s))) $
send helper₁ (fromString (drop-half (toString s))) $
recv helper₀ λ ss₀ →
recv helper₁ λ ss₁ →
send upstream (fromString (merge-sort-string (toString ss₀) (toString ss₁)))
end
dyn-merger : URI → (URI → JSProc) → JSProc
dyn-merger upstream helper =
spawn helper λ helper₀ →
spawn helper λ helper₁ →
str-merger upstream helper₀ helper₁
str-sorter₁ : URI → JSProc
str-sorter₁ upstream = dyn-merger upstream str-sorter₀
str-sorter₂ : URI → JSProc
str-sorter₂ upstream = dyn-merger upstream str-sorter₁
stringifier : URI → JSProc
stringifier d = recv d λ v → send d (fromString (JSON-stringify v)) end
stringifier-client : ∀ {D} → D → JSValue → Proc D JSValue
stringifier-client d v = send d v $ recv d λ _ → end
main : JS!
main =
Console.log "Hey!" >> assert test >>
Process.argv >>= λ argv → Console.log ("argv=" ++ join " " argv) >>
Console.log "server(adder):" >> server "127.0.0.1" "1337" adder >>= λ adder-uri →
Console.log "client(adderclient):" >>
client (adder-client adder-uri (fromString "Hello ") (fromString "World!")) >>
client (adder-client adder-uri (fromString "Bonjour ") (fromString "monde!")) >>
Console.log "server(reverser):" >>
server "127.0.0.1" "1338" reverser >>= λ reverser-uri →
Console.log "client(adder-reverser-client):" >>
client (adder-reverser-client adder-uri reverser-uri (fromString "red")) >>
server "127.0.0.1" "1339" str-sorter₀ >>= λ str-sorter₀-uri →
Console.log "str-sorter-client for str-sorter₀:" >>
client (str-sorter-client str-sorter₀-uri (fromString "Something to be sorted!")) >>
server "127.0.0.1" "1342" str-sorter₂ >>= λ str-sorter₂-uri →
Console.log "str-sorter-client:" >>
client (str-sorter-client str-sorter₂-uri (fromString "Something to be sorted!")) >>
server "127.0.0.1" "1343" stringifier >>= λ stringifier-uri →
client (stringifier-client stringifier-uri (fromValue test-value)) >>
FS.readFile "README.md" nullJS >>== λ err dat →
Console.log ("README.md, length is " ++ Number▹String (length (toString dat))) >>
Console.log "Bye!"
-- -}
-- -}
-- -}
-- -}