hms/hsim-live
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: no existential types, add hrun

Browse source
This commit is contained in:
Henri Saudubray 2026-03-27 10:53:26 +01:00
parent a41e6b2faa
commit ae1a5cf284
Signed by: hms
GPG key ID: 7065F57ED8856128
3 changed files with 166 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

83
lib/hsim/fill.ml
View file

@ -1,16 +1,14 @@
[@@@warning "-27-50"] [@@@warning "-27-50-69"]
let todo = assert false let todo = assert false
(* Little OCaml reminder *)
type t = { foo : int; bar : int; }
let f () =
(* Little OCaml reminder: *) let baz = { foo = 0; bar = 1 } in
type t = { a : int; b : int; c : int } let qux = { baz with foo = 2 } in (* same as "baz", except field "foo" *)
assert (qux = { foo = 2; bar = 1 })
let () =
let x = { a = 0; b = 1; c = 2 } in
let y = { x with a = 2 } in
assert (y = { a = 2; b = 1; c = 2 })
@ -20,22 +18,23 @@ let () =
(** Discrete-time node *) (** Discrete-time node *)
type ('i, 'o, 'r) dnode = type ('i, 'o, 'r, 's) dnode =
DNode : { DNode of {
state : 's; (** current state *) state : 's; (** current state *)
step : 's -> 'i -> 's * 'o; (** step function *) step : 's -> 'i -> 's * 'o; (** step function *)
reset : 's -> 'r -> 's; (** reset function *) reset : 's -> 'r -> 's; (** reset function *)
} -> ('i, 'o, 'r) dnode }
(** Run a discrete node on a list of inputs *) (** Run a discrete node on a list of inputs *)
let drun (DNode n : ('i, 'o, 'r) dnode) (i : 'i list) : 'o list = let drun (DNode n : ('i, 'o, 'r, 's) dnode) (i : 'i list) : 'o list =
todo todo
type time = type time =
float (** [≥ 0.0] *) float (** [≥ 0.0] *)
@ -75,13 +74,13 @@ type ('y, 'yder) ivp =
(** ODE solver *) (** ODE solver *)
type ('y, 'yder) csolver = type ('y, 'yder, 's) csolver =
(time, (** requested horizon *) (time, (** requested horizon *)
'y dense, (** solution approximation *) 'y dense, (** solution approximation *)
('y, 'yder) ivp) (** initial value problem *) ('y, 'yder) ivp, (** initial value problem *)
dnode 's) dnode
@ -111,13 +110,12 @@ type ('y, 'zin) zcp =
(** Zero-crossing solver *) (** Zero-crossing solver *)
type ('y, 'zin, 'zout) zsolver = type ('y, 'zin, 'zout, 's) zsolver =
('y dense, (** input value *) ('y dense, (** input value *)
time * 'zout, (** horizon and zero-crossing events *) time * 'zout, (** horizon and zero-crossing events *)
('y, 'zin) zcp) (** zero-crossing problem *) ('y, 'zin) zcp, (** zero-crossing problem *)
dnode 's) dnode
@ -131,11 +129,12 @@ type ('y, 'zin, 'zout) zsolver =
(** Full solver (composition of an ODE and zero-crossing solver) *) (** Full solver (composition of an ODE and zero-crossing solver) *)
type ('y, 'yder, 'zin, 'zout) solver = type ('y, 'yder, 'zin, 'zout, 's) solver =
(time, (** requested horizon *) (time, (** requested horizon *)
'y dense * 'zout, (** output and zero-crossing events *) 'y dense * 'zout, (** output and zero-crossing events *)
('y, 'yder) ivp * ('y, 'zin) zcp) (** (re)initialization parameters *) ('y, 'yder) ivp * ('y, 'zin) zcp, (** (re)initialization parameters *)
dnode 's) dnode
@ -145,15 +144,15 @@ type ('y, 'yder, 'zin, 'zout) solver =
(** Compose an ODE solver and a zero-crossing solver *) (** Compose an ODE solver and a zero-crossing solver *)
let build_solver : ('y, 'yder) csolver -> let build_solver : ('y, 'yder, 'cs) csolver ->
('y, 'zin, 'zout) zsolver -> ('y, 'zin, 'zout, 'zs) zsolver ->
('y, 'yder, 'zin, 'zout) solver ('y, 'yder, 'zin, 'zout, 'cs * 'zs) solver
= fun (DNode cs) (DNode zs) -> = fun (DNode cs) (DNode zs) ->
let state = (cs.state, zs.state) in let state = (cs.state, zs.state) in
let step (cstate, zstate) (h : time) = let step (cstate, zstate) (h : time) =
todo in todo in
let reset (cstate, zstate) (ivp, zcp) = let reset (cstate, zstate) (ivp, zcp) =
(cs.reset cstate ivp, zs.reset zstate zcp) in (cs.reset cstate ivp, zs.reset zstate zcp) in
DNode { state; step; reset } DNode { state; step; reset }
@ -161,10 +160,9 @@ let build_solver : ('y, 'yder) csolver ->
(** Hybrid (discrete-time and continuous-time) node *) (** Hybrid (discrete-time and continuous-time) node *)
type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode = type ('i, 'o, 'r, 's, 'y, 'yder, 'zin, 'zout) hnode =
HNode : { HNode of {
state : 's; (** current state *) state : 's; (** current state *)
step : 's -> 'i -> 's * 'o; (** discrete step function *) step : 's -> 'i -> 's * 'o; (** discrete step function *)
reset : 's -> 'r -> 's; (** reset function *) reset : 's -> 'r -> 's; (** reset function *)
@ -175,7 +173,7 @@ type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode =
cset : 's -> 'y -> 's; (** continuous state setter *) cset : 's -> 'y -> 's; (** continuous state setter *)
zset : 's -> 'zout -> 's; (** zero-crossing information setter *) zset : 's -> 'zout -> 's; (** zero-crossing information setter *)
jump : 's -> bool; (** discrete go-again indicator *) jump : 's -> bool; (** discrete go-again indicator *)
} -> ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode }
@ -184,16 +182,16 @@ type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode =
type mode = D | C type mode = D | C
(** Simulation state *) (** Simulation state *)
type ('i, 'o, 'r, 'y) state = type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state =
State : { State of {
solver : (** solver state *) solver : (** solver state *)
('y, 'yder, 'zin, 'zout) solver; ('y, 'yder, 'zin, 'zout,'ss) solver;
model : (** model state *) model : (** model state *)
('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode; ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode;
input : 'i signal; (** current input *) input : 'i signal; (** current input *)
time : time; (** current time *) time : time; (** current time *)
mode : mode; (** current step mode *) mode : mode; (** current step mode *)
} -> ('i, 'o, 'r, 'y) state }
@ -234,9 +232,9 @@ let cstep (State ({ model = HNode m; solver = DNode s; _ } as st)) =
(** Simulate a hybrid model with a solver *) (** Simulate a hybrid model with a solver *)
let hsim : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode -> let hsim : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode ->
('y, 'yder, 'zin, 'zout) solver -> ('y, 'yder, 'zin, 'zout, 'ss) solver ->
('i signal, 'o signal, 'r) dnode ('i signal, 'o signal, 'r, _) dnode
= fun model solver -> = fun model solver ->
let state = State { model; solver; input = None; time = 0.; mode = D } in let state = State { model; solver; input = None; time = 0.; mode = D } in
let step (State s as st) input = match (input, s.input, s.mode) with let step (State s as st) input = match (input, s.input, s.mode) with
@ -253,9 +251,10 @@ let hsim : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode ->
(** Run a simulation on a list of inputs *) (** Run a simulation on a list of inputs *)
let hrun (model : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode) let hrun (model : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode)
(solver : ('y, 'yder, 'zin, 'zout) solver) (solver : ('y, 'yder, 'zin, 'zout, 'ss) solver)
(i : 'i dense list) : 'o dense list (i : 'i dense list) : 'o dense list
= let sim = hsim model solver and i = List.map Option.some i in = let sim = hsim model solver and i = List.map Option.some i in
let rec step os (DNode sim) i = let rec step os (DNode sim) i =

110
lib/hsim/fill.mli Normal file
View file

@ -0,0 +1,110 @@
(** Discrete-time node *)
type ('i, 'o, 'r, 's) dnode =
DNode of {
state : 's; (** current state *)
step : 's -> 'i -> 's * 'o; (** step function *)
reset : 's -> 'r -> 's; (** reset function *)
}
(** Run a discrete node on a list of inputs *)
val drun : ('i, 'o, 'r, 's) dnode -> 'i list -> 'o list
type time =
float (** [≥ 0.0] *)
(** Interval-defined functions *)
type 'a dense =
{ h : time; (** horizon *)
f : time -> 'a } (** [f : [0, h] -> α] *)
(** Continuous-time signal *)
type 'a signal =
'a dense option
(** Initial value problem (IVP) *)
type ('y, 'yder) ivp =
{ y0 : 'y; (** initial position *)
fder : time -> 'y -> 'yder; (** derivative function on [[0.0, h]] *)
h : time; } (** maximal horizon *)
(** ODE solver *)
type ('y, 'yder, 's) csolver =
(time, (** requested horizon *)
'y dense, (** solution approximation *)
('y, 'yder) ivp, (** initial value problem *)
's) dnode
(** Zero-crossing problem (ZCP) *)
type ('y, 'zin) zcp =
{ y0 : 'y; (** initial position *)
fzer : time -> 'y -> 'zin; (** zero-crossing function *)
h : time; } (** maximal horizon *)
(** Zero-crossing solver *)
type ('y, 'zin, 'zout, 's) zsolver =
('y dense, (** input value *)
time * 'zout, (** horizon and zero-crossing events *)
('y, 'zin) zcp, (** zero-crossing problem *)
's) dnode
(** Full solver (composition of an ODE and zero-crossing solver) *)
type ('y, 'yder, 'zin, 'zout, 's) solver =
(time, (** requested horizon *)
'y dense * 'zout, (** output and zero-crossing events *)
('y, 'yder) ivp * ('y, 'zin) zcp, (** (re)initialization parameters *)
's) dnode
(** Compose an ODE solver and a zero-crossing solver *)
val build_solver : ('y, 'yder, 'cs) csolver ->
('y, 'zin, 'zout, 'zs) zsolver ->
('y, 'yder, 'zin, 'zout, 'cs * 'zs) solver
(** Hybrid (discrete-time and continuous-time) node *)
type ('i, 'o, 'r, 's, 'y, 'yder, 'zin, 'zout) hnode =
HNode of {
state : 's; (** current state *)
step : 's -> 'i -> 's * 'o; (** discrete step function *)
reset : 's -> 'r -> 's; (** reset function *)
fder : 's -> 'i -> 'y -> 'yder; (** derivative function *)
fzer : 's -> 'i -> 'y -> 'zin; (** zero-crossing function *)
fout : 's -> 'i -> 'y -> 'o; (** continuous output function *)
cget : 's -> 'y; (** continuous state getter *)
cset : 's -> 'y -> 's; (** continuous state setter *)
zset : 's -> 'zout -> 's; (** zero-crossing information setter *)
jump : 's -> bool; (** discrete go-again indicator *)
}
(** Simulation mode (either discrete or continuous) *)
type mode = D | C
(** Simulation state *)
type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state =
State of {
solver : (** solver state *)
('y, 'yder, 'zin, 'zout, 'ss) solver;
model : (** model state *)
('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode;
input : 'i signal; (** current input *)
time : time; (** current time *)
mode : mode; (** current step mode *)
}
(** Discrete simulation step *)
val dstep : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state ->
('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state * 'o signal
(** Continuous simulation step *)
val cstep : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state ->
('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state * 'o signal
(** Simulate a hybrid model with a solver *)
val hsim : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode ->
('y, 'yder, 'zin, 'zout, 'ss) solver ->
('i signal, 'o signal, 'r, ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state) dnode
(** Run a simulation on a list of inputs *)
val hrun : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode ->
('y, 'yder, 'zin, 'zout, 'ss) solver ->
'i dense list ->
'o dense list

15
lib/hsim/full.ml
View file

@ -278,3 +278,18 @@ let hsim : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode ->
let model = HNode { m with state = m.reset m.state r } in let model = HNode { m with state = m.reset m.state r } in
State { s with model; input = None; time = 0.; mode = D } in State { s with model; input = None; time = 0.; mode = D } in
DNode { state; step; reset } DNode { state; step; reset }
(** Run a simulation on a list of inputs
For each input value, we step the simulation as many times as
needed for it to reach the horizon. *)
let hrun (model : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode)
(solver : ('y, 'yder, 'zin, 'zout) solver)
(i : 'i dense list) : 'o dense list
= let sim = hsim model solver and i = List.map Option.some i in
let rec step os (DNode sim) i =
let state, o = sim.step sim.state i in
let sim = DNode { sim with state } in
if o = None then (sim, List.rev_map Option.get os)
else step (o :: os) sim None in
List.fold_left_map (step []) sim i |> snd |> List.flatten