Li.agda

open import FRP.JS.Nat
open import FRP.JS.String hiding (length) renaming (_++_ to _++s_)
open import FRP.JS.List hiding (_++_; [_]) renaming (map to mapl)
open import FRP.JS.Behaviour renaming (map to mapb)
open import FRP.JS.DOM  renaming (_++_ to _++d_)
open import FRP.JS.RSet

module Li where

postulate
  join : ∀ {A} → ⟦ Beh (Beh A) ⇒ Beh A ⟧

natList : ⟦ Beh ⟨ List ℕ ⟩ ⟧
natList = [ 1 ∷ 2 ∷ 3 ∷ List.[] ]

strList : ⟦ Beh ⟨ String ⟩ ⟧
strList = mapb showList natList where
  showList : List ℕ → String
  showList = foldr (λ n acc → show n ++s acc ) ""

li : ∀ {w} n → ⟦ Beh (DOM w) ⟧
li n = element "li" (text [ show n ])

liList : ∀ {w} → ⟦ Beh (DOM w) ⟧
liList = join result where
  lis : ∀ {w} → List ℕ → ⟦ Beh (DOM w) ⟧
  lis xs = foldr (λ n acc → acc) FRP.JS.DOM.[] xs

  result : ∀ {w} → ⟦ Beh ( Beh (DOM w) ) ⟧
  result = mapb (λ xs → lis xs {_}) natList