From ae1a5cf2842c0ce11aabeb6f78132ec8d1743146 Mon Sep 17 00:00:00 2001 From: Henri Saudubray Date: Fri, 27 Mar 2026 10:53:26 +0100 Subject: [PATCH] feat: no existential types, add hrun --- lib/hsim/fill.ml | 83 +++++++++++++++++----------------- lib/hsim/fill.mli | 110 ++++++++++++++++++++++++++++++++++++++++++++++ lib/hsim/full.ml | 15 +++++++ 3 files changed, 166 insertions(+), 42 deletions(-) create mode 100644 lib/hsim/fill.mli diff --git a/lib/hsim/fill.ml b/lib/hsim/fill.ml index 3513baf..47f95b7 100644 --- a/lib/hsim/fill.ml +++ b/lib/hsim/fill.ml @@ -1,16 +1,14 @@ -[@@@warning "-27-50"] +[@@@warning "-27-50-69"] let todo = assert false +(* Little OCaml reminder *) +type t = { foo : int; bar : int; } - -(* Little OCaml reminder: *) -type t = { a : int; b : int; c : int } - -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 }) +let f () = + let baz = { foo = 0; bar = 1 } in + let qux = { baz with foo = 2 } in (* same as "baz", except field "foo" *) + assert (qux = { foo = 2; bar = 1 }) @@ -20,22 +18,23 @@ let () = (** Discrete-time node *) -type ('i, 'o, 'r) dnode = - DNode : { +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 *) - } -> ('i, 'o, 'r) dnode + } (** 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 + type time = float (** [≥ 0.0] *) @@ -75,13 +74,13 @@ type ('y, 'yder) ivp = - (** ODE solver *) -type ('y, 'yder) csolver = +type ('y, 'yder, 's) csolver = (time, (** requested horizon *) 'y dense, (** solution approximation *) - ('y, 'yder) ivp) (** initial value problem *) - dnode + ('y, 'yder) ivp, (** initial value problem *) + 's) dnode + @@ -111,13 +110,12 @@ type ('y, 'zin) zcp = - (** Zero-crossing solver *) -type ('y, 'zin, 'zout) zsolver = +type ('y, 'zin, 'zout, 's) zsolver = ('y dense, (** input value *) time * 'zout, (** horizon and zero-crossing events *) - ('y, 'zin) zcp) (** zero-crossing problem *) - dnode + ('y, 'zin) zcp, (** zero-crossing problem *) + 's) dnode @@ -131,11 +129,12 @@ type ('y, 'zin, 'zout) zsolver = (** 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 *) 'y dense * 'zout, (** output and zero-crossing events *) - ('y, 'yder) ivp * ('y, 'zin) zcp) (** (re)initialization parameters *) - dnode + ('y, 'yder) ivp * ('y, 'zin) zcp, (** (re)initialization parameters *) + 's) dnode + @@ -145,15 +144,15 @@ type ('y, 'yder, 'zin, 'zout) solver = (** Compose an ODE solver and a zero-crossing solver *) -let build_solver : ('y, 'yder) csolver -> - ('y, 'zin, 'zout) zsolver -> - ('y, 'yder, 'zin, 'zout) solver +let build_solver : ('y, 'yder, 'cs) csolver -> + ('y, 'zin, 'zout, 'zs) zsolver -> + ('y, 'yder, 'zin, 'zout, 'cs * 'zs) solver = fun (DNode cs) (DNode zs) -> let state = (cs.state, zs.state) in let step (cstate, zstate) (h : time) = todo in - + let reset (cstate, zstate) (ivp, zcp) = (cs.reset cstate ivp, zs.reset zstate zcp) in DNode { state; step; reset } @@ -161,10 +160,9 @@ let build_solver : ('y, 'yder) csolver -> - (** Hybrid (discrete-time and continuous-time) node *) -type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode = - HNode : { +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 *) @@ -175,7 +173,7 @@ type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode = cset : 's -> 'y -> 's; (** continuous state setter *) zset : 's -> 'zout -> 's; (** zero-crossing information setter *) 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 (** Simulation state *) -type ('i, 'o, 'r, 'y) state = - State : { +type ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout, 'ms, 'ss) state = + State of { solver : (** solver state *) - ('y, 'yder, 'zin, 'zout) solver; + ('y, 'yder, 'zin, 'zout,'ss) solver; 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 *) time : time; (** current time *) 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 *) -let hsim : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode -> - ('y, 'yder, 'zin, 'zout) solver -> - ('i signal, 'o signal, 'r) dnode +let hsim : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode -> + ('y, 'yder, 'zin, 'zout, 'ss) solver -> + ('i signal, 'o signal, 'r, _) dnode = fun model solver -> 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 @@ -253,9 +251,10 @@ let hsim : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode -> + (** Run a simulation on a list of inputs *) -let hrun (model : ('i, 'o, 'r, 'y, 'yder, 'zin, 'zout) hnode) - (solver : ('y, 'yder, 'zin, 'zout) solver) +let hrun (model : ('i, 'o, 'r, 'ms, 'y, 'yder, 'zin, 'zout) hnode) + (solver : ('y, 'yder, 'zin, 'zout, 'ss) 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 = diff --git a/lib/hsim/fill.mli b/lib/hsim/fill.mli new file mode 100644 index 0000000..00c27fd --- /dev/null +++ b/lib/hsim/fill.mli @@ -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 diff --git a/lib/hsim/full.ml b/lib/hsim/full.ml index e2e01d3..c0e8cac 100644 --- a/lib/hsim/full.ml +++ b/lib/hsim/full.ml @@ -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 State { s with model; input = None; time = 0.; mode = D } in 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