feat: pres

doc/notes.typ

@@ -7,6 +7,7 @@
 #let breakl(b) = {
   raw(b.text.replace(regex(" *\\\\\n *"), " "), lang: b.lang, block: b.block)
 }
+#set raw(syntaxes: "zelus.sublime-syntax")
 
 #show raw: set text(font: "CaskaydiaCove NF")
 #show link: underline
@@ -495,3 +496,71 @@ simulation loop as follows:
   implemented in an imperative language like C. Code generation for hybrid
   models has much in common with code generation for synchronous languages.
 ])
+
+== Miscellaneous
+
+=== Signals
+
+Superdense time defines signals as
+$S u p e r d e n s e(bb(V)) = bb(R) * bb(N) -> bb(V)$, where given
+$f : S u p e r d e n s e(bb(V))$, $f(t, n) = f(t + n partial)$ in the
+non-standard semantics.
+
+Our representation instead uses
+$S i g n a l(bb(V)) = S t r e a m((h : bb(R)) * ([0, h] -> bb(V)))$. Can we 
+convert between the two as we want?
+
+#breakl(```ocaml
+let (@.) f g x = f (g x)
+let splt f g x = f x, g x
+
+type 'a superdense = float * int -> 'a
+type 'a signal     = (float * (float -> 'a)) stream
+
+let h = fst @. hd
+let u = snd @. hd
+
+let compose : 'a signal -> 'a superdense * float stream =
+  let rec g v s n =
+    if n = 0 then v
+    else if h s <> 0. then u s 0.
+    else g (u s 0.) (tl s) (n - 1) in
+  let rec f s = fun (t, n) ->
+    if t < h s then u s t
+    else if t = h s then g (u s t) (tl s) n
+    else f (tl s) (t -. h s, n) in
+  splt f (map fst)
+
+let decompose : 'a superdense * float stream -> 'a signal =
+  let rec f r n = fun (s, h) ->
+    if hd h = 0. then (0., fun _ -> s (r, n)) @: f r (n + 1) (s, tl h)
+    else (hd h, fun t -> s (t +. r, 0)) @: f (r +. hd h) 0 (s, tl h) in
+  f 0. 0
+```)
+
+#pagebreak()
+=== Continuity of assertions
+
+In Zélus, the following program is forbidden:
+
+```zelus
+let hybrid f x = x >= 0
+```
+
+One cannot then write
+```zelus
+let hybrid ball () = y where
+  rec der y  = y'   init y0
+  and der y' = -. g init 0.0 reset z -> (-0.8 *. last y')
+  and     z  = up (-. y)
+  and assert (f y)
+```
+even though we want the following, equivalent program to work:
+```zelus
+let hybrid ball () = y where
+  rec der y  = y'   init y0
+  and der y' = -. g init 0.0 reset z -> (-0.8 *. last y')
+  and     z  = up (-. y)
+  and assert (y >= 0)
+```
+Is this an issue?