chore: initial commit

exm/ball_discrete.zls

@@ -0,0 +1,21 @@
+
+let dt = 0.001
+let g  = 9.81
+
+let node f_integr (x0, x') = x where
+  rec x = x0 -> pre (x +. x' *. dt)
+let node b_integr (x0, x') = x where
+  rec x = x0 -> (pre x) +. x' *. dt
+
+let node bouncing_ball (p0, v0) = p where
+  rec p = reset f_integr (q, v)    every z
+  and v = reset b_integr (w, -. g) every z
+  and q = p0 -> 0.0 and w = v0 -> -0.8 *. (pre v)
+  and z = false fby (p < 0.0)
+
+let node main () =
+  let rec t = 0.0 fby (dt +. t) in
+  let p = bouncing_ball (5.0, 0.0) in
+  match t <= 10.0 with
+  | true -> (print_float t; print_string "\t"; print_float p; print_newline ())
+  | false -> ()

exm/dune

@@ -0,0 +1,17 @@
+(env
+ (dev
+  (flags
+   (:standard -w -a))))
+
+(rule
+ (targets exm_ball_discrete.ml ball_discrete.ml ball_discrete.zci)
+ (deps
+  (:zl ball_discrete.zls)
+  (package zelus))
+ (action
+  (run zeluc -s main -o exm_ball_discrete %{zl})))
+
+(executable
+ (name exm_ball_discrete)
+ (public_name exm_ball_discrete)
+ (libraries zelus))

exm/main.zls

@@ -0,0 +1,121 @@
+
+
+
+(** Zélus
+
+    Synchronous language kernel _à la_ Lustre:
+    - programs are Mealy machines (outputs on each transition)
+    - variables represent streams of values in time *)
+
+let node incr x = y where
+  y = x + 1
+
+(*   x │ 8  3  2  7  5  3  …
+    ───┼─────────────────────
+     y │ 9  4  3  8  6  4  …   *)
+
+
+
+
+
+
+(** - we can use values of the previous instants (using [pre]) and
+      initialize streams (using [->]) *)
+
+let node accumulate x = z where
+  rec w = pre x
+  and y = 0 -> pre x
+  and z = x -> (pre z) + x
+
+(*   x │ 1  2  5  2  5  3  …
+    ───┼─────────────────────
+     w │    1  2  5  2  5  …
+     y │ 0  1  2  5  2  5  …
+     z │ 1  3  8 10 15 18  …   *)
+
+
+
+(** - we can reset streams at will *)
+
+let node stay x = y where            (* output the first value forever        *)
+  rec y = x -> pre y
+
+let node from x = y where            (* count up from the first value         *)
+  rec y = x -> pre y + 1
+
+let node loop x = y where
+  rec y = reset from 0 every z
+  and z = false -> pre y >= w
+  and w = stay x
+
+(*        x │ 2  _  _  _  _  _  …
+    ────────┼─────────────────────
+     loop x │ 0  1  2  0  1  2  …   *)
+
+
+(** Already able to model physical behaviours! *)
+
+let dt = 0.001                        (* Integration step                     *)
+let g  = 9.81                         (* Gravitational constant               *)
+let node f_integr (x0, x') = x where  (* Forward Euler integrator             *)
+  rec x = x0 -> pre (x +. x' *. dt)
+let node b_integr (x0, x') = x where  (* Backward Euler integrator            *)
+  rec x = x0 -> (pre x) +. x' *. dt
+
+let node bouncing_ball (p0, v0) = p where
+  rec p = reset f_integr (q, v)    every z
+  and v = reset b_integr (w, -. g) every z
+  and q = p0 -> 0.0 and w = v0 -> -0.8 *. (pre v)
+  and z = false -> (pre p) < 0.0
+
+(** Quite cumbersome. *)
+
+
+
+
+
+
+(** Enter continuous-time constructs:
+    - express values with initial value problems with [der] and [init] *)
+
+let hybrid integr (x0, x') = x where
+  der x = x' init x0
+
+let hybrid position (p0, v0, a) = p where
+  rec der p = v init p0
+  and der v = a init v0
+
+
+
+
+
+
+
+
+
+
+
+
+
+(** We can intermingle discrete and continuous behaviours: *)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+(** We can now express physical systems much more precisely: *)
+
+let hybrid bouncing_ball (p0, v0) = p where
+  rec der p = v    init p0 reset z -> 0.0
+  and der v = -. g init v0 reset z -> -0.8 *. last v
+  and     z = up(-. p)