Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/tools/stateflow/semantics/cPS_interpreter.ml | ||
|---|---|---|
| 1 | 1 |
open Basetypes |
| 2 | 2 |
open Datatype |
| 3 |
|
|
| 3 | 4 |
(* open ActiveEnv *) |
| 4 | 5 |
open CPS_transformer |
| 6 |
|
|
| 5 | 7 |
(* open Simulink *) |
| 6 | 8 |
open Theta |
| 7 | 9 |
|
| 8 |
module Interpreter (Transformer : TransformerType) = |
|
| 9 |
struct |
|
| 10 |
module Interpreter (Transformer : TransformerType) = struct |
|
| 10 | 11 |
module KT = KenvTheta (Transformer) |
| 11 | 12 |
open KT |
| 12 | 13 |
|
| 13 |
let ( >? ) cond tr = |
|
| 14 |
if cond then tr else Transformer.null |
|
| 14 |
let ( >? ) cond tr = if cond then tr else Transformer.null |
|
| 15 | 15 |
|
| 16 |
module type DenotationType = |
|
| 17 |
sig |
|
| 16 |
module type DenotationType = sig |
|
| 18 | 17 |
module Theta : MemoThetaType |
| 19 | 18 |
|
| 20 |
val eval_dest : destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 21 |
val eval_tau : trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 22 |
val eval_T : transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 23 |
val eval_C : (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t |
|
| 19 |
val eval_dest : |
|
| 20 |
destination_t -> |
|
| 21 |
Transformer.t wrapper_t -> |
|
| 22 |
Transformer.t success_t -> |
|
| 23 |
Transformer.t fail_t -> |
|
| 24 |
Transformer.t |
|
| 25 |
|
|
| 26 |
val eval_tau : |
|
| 27 |
trans_t -> |
|
| 28 |
Transformer.t wrapper_t -> |
|
| 29 |
Transformer.t success_t -> |
|
| 30 |
Transformer.t fail_t -> |
|
| 31 |
Transformer.t |
|
| 32 |
|
|
| 33 |
val eval_T : |
|
| 34 |
transitions_t -> |
|
| 35 |
Transformer.t wrapper_t -> |
|
| 36 |
Transformer.t success_t -> |
|
| 37 |
Transformer.t fail_t -> |
|
| 38 |
Transformer.t |
|
| 39 |
|
|
| 40 |
val eval_C : |
|
| 41 |
(path_t, 'b, Transformer.t) tag_t -> |
|
| 42 |
path_t -> |
|
| 43 |
composition_t -> |
|
| 44 |
Transformer.t |
|
| 45 |
|
|
| 24 | 46 |
val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
| 25 |
val eval_S : (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
| 47 |
|
|
| 48 |
val eval_S : |
|
| 49 |
(path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
| 26 | 50 |
end |
| 27 | 51 |
|
| 28 |
module type AbsDenotationType = |
|
| 29 |
sig |
|
| 30 |
val eval_dest : kenv_t -> destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 31 |
val eval_tau : kenv_t -> trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 32 |
val eval_T : kenv_t -> transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
| 33 |
val eval_C : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t |
|
| 34 |
val eval_open_path : kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
|
| 35 |
val eval_S : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
| 52 |
module type AbsDenotationType = sig |
|
| 53 |
val eval_dest : |
|
| 54 |
kenv_t -> |
|
| 55 |
destination_t -> |
|
| 56 |
Transformer.t wrapper_t -> |
|
| 57 |
Transformer.t success_t -> |
|
| 58 |
Transformer.t fail_t -> |
|
| 59 |
Transformer.t |
|
| 60 |
|
|
| 61 |
val eval_tau : |
|
| 62 |
kenv_t -> |
|
| 63 |
trans_t -> |
|
| 64 |
Transformer.t wrapper_t -> |
|
| 65 |
Transformer.t success_t -> |
|
| 66 |
Transformer.t fail_t -> |
|
| 67 |
Transformer.t |
|
| 68 |
|
|
| 69 |
val eval_T : |
|
| 70 |
kenv_t -> |
|
| 71 |
transitions_t -> |
|
| 72 |
Transformer.t wrapper_t -> |
|
| 73 |
Transformer.t success_t -> |
|
| 74 |
Transformer.t fail_t -> |
|
| 75 |
Transformer.t |
|
| 76 |
|
|
| 77 |
val eval_C : |
|
| 78 |
kenv_t -> |
|
| 79 |
(path_t, 'b, Transformer.t) tag_t -> |
|
| 80 |
path_t -> |
|
| 81 |
composition_t -> |
|
| 82 |
Transformer.t |
|
| 83 |
|
|
| 84 |
val eval_open_path : |
|
| 85 |
kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
|
| 86 |
|
|
| 87 |
val eval_S : |
|
| 88 |
kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
| 36 | 89 |
end |
| 37 | 90 |
|
| 38 |
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
|
|
| 39 |
struct |
|
| 91 |
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : |
|
| 92 |
AbsDenotationType = struct
|
|
| 40 | 93 |
let eval_dest kenv = |
| 41 |
let module Kenv = |
|
| 42 |
struct |
|
| 43 |
let kenv = kenv |
|
| 44 |
end in |
|
| 94 |
let module Kenv = struct |
|
| 95 |
let kenv = kenv |
|
| 96 |
end in |
|
| 45 | 97 |
let module D = Denot (Kenv) in |
| 46 | 98 |
D.eval_dest |
| 47 | 99 |
|
| 48 | 100 |
let eval_tau kenv = |
| 49 |
let module Kenv = |
|
| 50 |
struct |
|
| 51 |
let kenv = kenv |
|
| 52 |
end in |
|
| 101 |
let module Kenv = struct |
|
| 102 |
let kenv = kenv |
|
| 103 |
end in |
|
| 53 | 104 |
let module D = Denot (Kenv) in |
| 54 | 105 |
D.eval_tau |
| 55 | 106 |
|
| 56 | 107 |
let eval_T kenv = |
| 57 |
let module Kenv = |
|
| 58 |
struct |
|
| 59 |
let kenv = kenv |
|
| 60 |
end in |
|
| 108 |
let module Kenv = struct |
|
| 109 |
let kenv = kenv |
|
| 110 |
end in |
|
| 61 | 111 |
let module D = Denot (Kenv) in |
| 62 | 112 |
D.eval_T |
| 63 | 113 |
|
| 64 | 114 |
let eval_C kenv = |
| 65 |
let module Kenv = |
|
| 66 |
struct |
|
| 67 |
let kenv = kenv |
|
| 68 |
end in |
|
| 115 |
let module Kenv = struct |
|
| 116 |
let kenv = kenv |
|
| 117 |
end in |
|
| 69 | 118 |
let module D = Denot (Kenv) in |
| 70 | 119 |
D.eval_C |
| 71 | 120 |
|
| 72 | 121 |
let eval_open_path kenv = |
| 73 |
let module Kenv = |
|
| 74 |
struct |
|
| 75 |
let kenv = kenv |
|
| 76 |
end in |
|
| 122 |
let module Kenv = struct |
|
| 123 |
let kenv = kenv |
|
| 124 |
end in |
|
| 77 | 125 |
let module D = Denot (Kenv) in |
| 78 | 126 |
D.eval_open_path |
| 79 | 127 |
|
| 80 | 128 |
let eval_S kenv = |
| 81 |
let module Kenv = |
|
| 82 |
struct |
|
| 83 |
let kenv = kenv |
|
| 84 |
end in |
|
| 129 |
let module Kenv = struct |
|
| 130 |
let kenv = kenv |
|
| 131 |
end in |
|
| 85 | 132 |
let module D = Denot (Kenv) in |
| 86 | 133 |
D.eval_S |
| 87 | 134 |
end |
| 88 | 135 |
|
| 89 |
module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> DenotationType = |
|
| 90 |
functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> |
|
| 91 |
struct |
|
| 92 |
module Theta = Thetaify (Kenv) |
|
| 93 |
|
|
| 94 |
let eval_dest dest wrapper success fail = |
|
| 95 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest); |
|
| 96 |
match dest with |
|
| 97 |
| DPath p -> wrapper p (success p) |
|
| 98 |
| DJunction j -> Theta.theta J j wrapper success fail |
|
| 99 |
|
|
| 100 |
let eval_tau trans wrapper success fail = |
|
| 101 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans); |
|
| 102 |
let success' p = |
|
| 103 |
Transformer.(success p >> eval_act (module Theta) trans.transition_act) |
|
| 104 |
in |
|
| 105 |
let cond = Transformer.(event trans.event && trans.condition) in |
|
| 106 |
Transformer.(eval_cond cond |
|
| 107 |
(eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail) |
|
| 108 |
fail.local) |
|
| 109 |
|
|
| 110 |
let rec eval_T tl wrapper success fail = |
|
| 111 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl); |
|
| 112 |
match tl with |
|
| 113 |
| [] -> fail.global |
|
| 114 |
| t::[] -> eval_tau t wrapper success fail |
|
| 115 |
| t::tl -> |
|
| 116 |
let fail' = { fail with local = eval_T tl wrapper success fail } in
|
|
| 117 |
eval_tau t wrapper success fail' |
|
| 118 |
|
|
| 119 |
let frontier path = |
|
| 120 |
match path with |
|
| 121 |
| [] -> [], [] |
|
| 122 |
| t::q -> [t], q |
|
| 123 |
|
|
| 124 |
let rec eval_open_path mode p p1 p2 success_p2 = |
|
| 125 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2); |
|
| 126 |
match frontier p1, frontier p2 with |
|
| 127 |
| ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2 |
|
| 128 |
| (x , _ ), (y , pd) -> |
|
| 129 |
match mode with |
|
| 130 |
| Outer -> (Transformer.(Theta.theta X (p@x) Loose >> success_p2 >> Theta.theta E (p@y) pd Loose)) |
|
| 131 |
| Inner -> (assert (x = []); |
|
| 132 |
Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict)) |
|
| 133 |
| Enter -> (assert (x = [] && y <> []); |
|
| 134 |
Transformer.( success_p2 >> Theta.theta E (p@y) pd Loose)) |
|
| 135 |
|
|
| 136 |
let rec eval_C : type a b. (a, b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t = |
|
| 137 |
fun tag prefix comp -> |
|
| 138 |
match tag with |
|
| 139 |
| E -> Transformer.( |
|
| 140 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp); |
|
| 141 |
match comp with |
|
| 142 |
| Or (_T, []) -> null |
|
| 143 |
| Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null |
|
| 144 |
| Or (_T, _S) -> let wrapper = eval_open_path Enter [] prefix in |
|
| 145 |
let success _p_d = null in |
|
| 146 |
eval_T _T wrapper success { local = bot; global = bot }
|
|
| 147 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null |
|
| 148 |
) |
|
| 149 |
| D -> Transformer.( |
|
| 150 |
match comp with |
|
| 151 |
| Or (_T, []) -> null |
|
| 152 |
| Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S))) |
|
| 153 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta D (prefix@[p]))) _S null |
|
| 154 |
) |
|
| 155 |
| X -> Transformer.( |
|
| 156 |
match comp with |
|
| 157 |
| Or (_T, []) -> null |
|
| 158 |
| Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S))) |
|
| 159 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta X (prefix@[p]) Loose)) _S null |
|
| 160 |
) |
|
| 161 |
| J -> assert false |
|
| 162 |
|
|
| 163 |
let eval_S : type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b = |
|
| 164 |
fun tag p p_def -> |
|
| 165 |
match tag with |
|
| 166 |
| E -> fun path frontier -> Transformer.( |
|
| 167 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier); |
|
| 168 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> |
|
| 169 |
match path with |
|
| 170 |
| [] -> eval_C E p p_def.internal_composition |
|
| 171 |
| s::path_tl -> Theta.theta E (p@[s]) path_tl Loose |
|
| 172 |
) |
|
| 173 |
| D -> Transformer.( |
|
| 174 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p); |
|
| 175 |
let wrapper_i = eval_open_path Inner [] p in |
|
| 176 |
let wrapper_o = eval_open_path Outer [] p in |
|
| 177 |
let success _p_d = null in |
|
| 178 |
let fail_o = |
|
| 179 |
let fail_i = |
|
| 180 |
let same_fail_C = eval_C D p p_def.internal_composition in |
|
| 181 |
{ local = same_fail_C; global = same_fail_C }
|
|
| 182 |
in |
|
| 183 |
let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in |
|
| 184 |
{ local = same_fail_i; global = same_fail_i }
|
|
| 185 |
in |
|
| 186 |
eval_T p_def.outer_trans wrapper_o success fail_o |
|
| 187 |
) |
|
| 188 |
| X -> fun frontier -> Transformer.( |
|
| 189 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier); |
|
| 190 |
eval_C X p p_def.internal_composition >> |
|
| 191 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p))) |
|
| 192 |
) |
|
| 193 |
end |
|
| 136 |
module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> |
|
| 137 |
DenotationType = |
|
| 138 |
functor |
|
| 139 |
(Thetaify : ThetaifyType) |
|
| 140 |
(Kenv : KenvType) |
|
| 141 |
-> |
|
| 142 |
struct |
|
| 143 |
module Theta = Thetaify (Kenv) |
|
| 144 |
|
|
| 145 |
let eval_dest dest wrapper success fail = |
|
| 146 |
Log.report ~level:sf_level (fun fmt -> |
|
| 147 |
Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest); |
|
| 148 |
match dest with |
|
| 149 |
| DPath p -> |
|
| 150 |
wrapper p (success p) |
|
| 151 |
| DJunction j -> |
|
| 152 |
Theta.theta J j wrapper success fail |
|
| 153 |
|
|
| 154 |
let eval_tau trans wrapper success fail = |
|
| 155 |
Log.report ~level:sf_level (fun fmt -> |
|
| 156 |
Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans); |
|
| 157 |
let success' p = |
|
| 158 |
Transformer.( |
|
| 159 |
success p >> eval_act (module Theta) trans.transition_act) |
|
| 160 |
in |
|
| 161 |
let cond = Transformer.(event trans.event && trans.condition) in |
|
| 162 |
Transformer.( |
|
| 163 |
eval_cond cond |
|
| 164 |
(eval_act (module Theta) trans.condition_act |
|
| 165 |
>> eval_dest trans.dest wrapper success' fail) |
|
| 166 |
fail.local) |
|
| 167 |
|
|
| 168 |
let rec eval_T tl wrapper success fail = |
|
| 169 |
Log.report ~level:sf_level (fun fmt -> |
|
| 170 |
Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl); |
|
| 171 |
match tl with |
|
| 172 |
| [] -> |
|
| 173 |
fail.global |
|
| 174 |
| [ t ] -> |
|
| 175 |
eval_tau t wrapper success fail |
|
| 176 |
| t :: tl -> |
|
| 177 |
let fail' = { fail with local = eval_T tl wrapper success fail } in
|
|
| 178 |
eval_tau t wrapper success fail' |
|
| 179 |
|
|
| 180 |
let frontier path = match path with [] -> [], [] | t :: q -> [ t ], q |
|
| 181 |
|
|
| 182 |
let rec eval_open_path mode p p1 p2 success_p2 = |
|
| 183 |
Log.report ~level:sf_level (fun fmt -> |
|
| 184 |
Format.fprintf fmt |
|
| 185 |
"@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " |
|
| 186 |
pp_mode mode pp_path p pp_path p1 pp_path p2); |
|
| 187 |
match frontier p1, frontier p2 with |
|
| 188 |
| ([ x ], ps), ([ y ], pd) when x = y -> |
|
| 189 |
eval_open_path mode (p @ [ x ]) ps pd success_p2 |
|
| 190 |
| (x, _), (y, pd) -> ( |
|
| 191 |
match mode with |
|
| 192 |
| Outer -> |
|
| 193 |
Transformer.( |
|
| 194 |
Theta.theta X (p @ x) Loose |
|
| 195 |
>> success_p2 |
|
| 196 |
>> Theta.theta E (p @ y) pd Loose) |
|
| 197 |
| Inner -> |
|
| 198 |
assert (x = []); |
|
| 199 |
Transformer.( |
|
| 200 |
Theta.theta X (p @ x) Strict |
|
| 201 |
>> success_p2 |
|
| 202 |
>> Theta.theta E (p @ y) pd Strict) |
|
| 203 |
| Enter -> |
|
| 204 |
assert (x = [] && y <> []); |
|
| 205 |
Transformer.(success_p2 >> Theta.theta E (p @ y) pd Loose)) |
|
| 206 |
|
|
| 207 |
let rec eval_C : |
|
| 208 |
type a b. |
|
| 209 |
(a, b, Transformer.t) tag_t -> |
|
| 210 |
path_t -> |
|
| 211 |
composition_t -> |
|
| 212 |
Transformer.t = |
|
| 213 |
fun tag prefix comp -> |
|
| 214 |
match tag with |
|
| 215 |
| E -> ( |
|
| 216 |
Transformer.( |
|
| 217 |
Log.report ~level:sf_level (fun fmt -> |
|
| 218 |
Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path |
|
| 219 |
prefix SF.pp_comp comp); |
|
| 220 |
match comp with |
|
| 221 |
| Or (_T, []) -> |
|
| 222 |
null |
|
| 223 |
| Or ([], [ s0 ]) -> |
|
| 224 |
eval_open_path Enter prefix [] [ s0 ] null |
|
| 225 |
| Or (_T, _S) -> |
|
| 226 |
let wrapper = eval_open_path Enter [] prefix in |
|
| 227 |
let success _p_d = null in |
|
| 228 |
eval_T _T wrapper success { local = bot; global = bot }
|
|
| 229 |
| And _S -> |
|
| 230 |
List.fold_right |
|
| 231 |
(fun p -> ( >> ) (Theta.theta E (prefix @ [ p ]) [] Loose)) |
|
| 232 |
_S null)) |
|
| 233 |
| D -> ( |
|
| 234 |
Transformer.( |
|
| 235 |
match comp with |
|
| 236 |
| Or (_T, []) -> |
|
| 237 |
null |
|
| 238 |
| Or (_T, p :: _S) -> |
|
| 239 |
eval_cond |
|
| 240 |
(active (prefix @ [ p ])) |
|
| 241 |
(Theta.theta D (prefix @ [ p ])) |
|
| 242 |
(eval_C D prefix (Or (_T, _S))) |
|
| 243 |
| And _S -> |
|
| 244 |
List.fold_right |
|
| 245 |
(fun p -> ( >> ) (Theta.theta D (prefix @ [ p ]))) |
|
| 246 |
_S null)) |
|
| 247 |
| X -> ( |
|
| 248 |
Transformer.( |
|
| 249 |
match comp with |
|
| 250 |
| Or (_T, []) -> |
|
| 251 |
null |
|
| 252 |
| Or (_T, p :: _S) -> |
|
| 253 |
eval_cond |
|
| 254 |
(active (prefix @ [ p ])) |
|
| 255 |
(Theta.theta X (prefix @ [ p ]) Loose) |
|
| 256 |
(eval_C X prefix (Or (_T, _S))) |
|
| 257 |
| And _S -> |
|
| 258 |
List.fold_right |
|
| 259 |
(fun p -> ( >> ) (Theta.theta X (prefix @ [ p ]) Loose)) |
|
| 260 |
_S null)) |
|
| 261 |
| J -> |
|
| 262 |
assert false |
|
| 263 |
|
|
| 264 |
let eval_S : |
|
| 265 |
type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b |
|
| 266 |
= |
|
| 267 |
fun tag p p_def -> |
|
| 268 |
match tag with |
|
| 269 |
| E -> ( |
|
| 270 |
fun path frontier -> |
|
| 271 |
Transformer.( |
|
| 272 |
Log.report ~level:sf_level (fun fmt -> |
|
| 273 |
Format.fprintf fmt |
|
| 274 |
"@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag |
|
| 275 |
pp_path p pp_path path pp_frontier frontier); |
|
| 276 |
frontier = Loose |
|
| 277 |
>? (eval_act (module Theta) p_def.state_actions.entry_act |
|
| 278 |
>> eval_act (module Theta) (open_path p)) |
|
| 279 |
>> |
|
| 280 |
match path with |
|
| 281 |
| [] -> |
|
| 282 |
eval_C E p p_def.internal_composition |
|
| 283 |
| s :: path_tl -> |
|
| 284 |
Theta.theta E (p @ [ s ]) path_tl Loose)) |
|
| 285 |
| D -> |
|
| 286 |
Transformer.( |
|
| 287 |
Log.report ~level:sf_level (fun fmt -> |
|
| 288 |
Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path |
|
| 289 |
p); |
|
| 290 |
let wrapper_i = eval_open_path Inner [] p in |
|
| 291 |
let wrapper_o = eval_open_path Outer [] p in |
|
| 292 |
let success _p_d = null in |
|
| 293 |
let fail_o = |
|
| 294 |
let fail_i = |
|
| 295 |
let same_fail_C = eval_C D p p_def.internal_composition in |
|
| 296 |
{ local = same_fail_C; global = same_fail_C }
|
|
| 297 |
in |
|
| 298 |
let same_fail_i = |
|
| 299 |
eval_act (module Theta) p_def.state_actions.during_act |
|
| 300 |
>> eval_T p_def.inner_trans wrapper_i success fail_i |
|
| 301 |
in |
|
| 302 |
{ local = same_fail_i; global = same_fail_i }
|
|
| 303 |
in |
|
| 304 |
eval_T p_def.outer_trans wrapper_o success fail_o) |
|
| 305 |
| X -> |
|
| 306 |
fun frontier -> |
|
| 307 |
Transformer.( |
|
| 308 |
Log.report ~level:sf_level (fun fmt -> |
|
| 309 |
Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " |
|
| 310 |
pp_tag tag pp_path p pp_frontier frontier); |
|
| 311 |
eval_C X p p_def.internal_composition |
|
| 312 |
>> (frontier = Loose |
|
| 313 |
>? (eval_act (module Theta) p_def.state_actions.exit_act |
|
| 314 |
>> eval_act (module Theta) (close_path p)))) |
|
| 315 |
end |
|
| 194 | 316 |
|
| 195 |
module type ProgType = |
|
| 196 |
sig |
|
| 317 |
module type ProgType = sig |
|
| 197 | 318 |
val init : state_name_t |
| 319 |
|
|
| 198 | 320 |
val defs : prog_t src_components_t list |
| 199 | 321 |
end |
| 200 | 322 |
|
| 201 |
module type EvaluationType = |
|
| 202 |
sig |
|
| 323 |
module type EvaluationType = sig |
|
| 203 | 324 |
module Theta : ThetaType with type t = Transformer.t |
| 325 |
|
|
| 204 | 326 |
val eval_prog : Transformer.t |
| 327 |
|
|
| 205 | 328 |
val eval_components : 'c call_t -> ('c * Transformer.t) list
|
| 206 | 329 |
end |
| 207 | 330 |
|
| 208 |
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
|
|
| 209 |
struct |
|
| 331 |
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : |
|
| 332 |
EvaluationType = struct
|
|
| 210 | 333 |
module Denotation = Denotation (Thetaify) |
| 211 | 334 |
module AbsDenotation = AbstractKenv (Denotation) |
| 212 | 335 |
include AbsDenotation |
| 213 | 336 |
|
| 214 |
module Kenv : KenvType = |
|
| 215 |
struct |
|
| 337 |
module Kenv : KenvType = struct |
|
| 216 | 338 |
let kenv = |
| 217 |
List.fold_left ( |
|
| 218 |
fun accu d -> match d with |
|
| 219 |
| State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp),
|
|
| 220 |
(fun kenv -> eval_S kenv D p defp), |
|
| 221 |
(fun kenv -> eval_S kenv X p defp)))::accu.cont_node } |
|
| 222 |
| Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
|
|
| 223 |
| SFFunction _ -> accu |
|
| 224 |
) {cont_node = []; cont_junc = []} Prog.defs
|
|
| 339 |
List.fold_left |
|
| 340 |
(fun accu d -> |
|
| 341 |
match d with |
|
| 342 |
| State (p, defp) -> |
|
| 343 |
{
|
|
| 344 |
accu with |
|
| 345 |
cont_node = |
|
| 346 |
( p, |
|
| 347 |
( (fun kenv -> eval_S kenv E p defp), |
|
| 348 |
(fun kenv -> eval_S kenv D p defp), |
|
| 349 |
fun kenv -> eval_S kenv X p defp ) ) |
|
| 350 |
:: accu.cont_node; |
|
| 351 |
} |
|
| 352 |
| Junction (j, defj) -> |
|
| 353 |
{
|
|
| 354 |
accu with |
|
| 355 |
cont_junc = (j, fun kenv -> eval_T kenv defj) :: accu.cont_junc; |
|
| 356 |
} |
|
| 357 |
| SFFunction _ -> |
|
| 358 |
accu) |
|
| 359 |
{ cont_node = []; cont_junc = [] }
|
|
| 360 |
Prog.defs |
|
| 225 | 361 |
end |
| 226 | 362 |
|
| 227 | 363 |
module AppDenotation = Denotation (Kenv) |
| ... | ... | |
| 230 | 366 |
let eval_components = Theta.components |
| 231 | 367 |
|
| 232 | 368 |
let eval_prog = |
| 233 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose)) |
|
| 234 |
end |
|
| 235 |
(* |
|
| 236 |
module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType = |
|
| 237 |
struct |
|
| 238 |
include Denotation (Theta) |
|
| 239 |
|
|
| 240 |
let theta = |
|
| 241 |
let kenv = |
|
| 242 |
List.fold_left ( |
|
| 243 |
fun accu d -> match d with |
|
| 244 |
| State (p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node }
|
|
| 245 |
| Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc }
|
|
| 246 |
) {cont_node = []; cont_junc = []} Prog.defs
|
|
| 247 |
in Obj.magic (fun tag -> theta_ify kenv tag) |
|
| 369 |
Transformer.( |
|
| 370 |
eval_cond |
|
| 371 |
(active [ Prog.init ]) |
|
| 372 |
(Theta.theta D [ Prog.init ]) |
|
| 373 |
(Theta.theta E [ Prog.init ] [] Loose)) |
|
| 248 | 374 |
end |
| 249 |
module Rec (Prog : ProgType) = |
|
| 250 |
struct |
|
| 251 |
module rec Theta : ThetaType = ThetaFix (Prog) (Theta) |
|
| 252 |
end |
|
| 253 |
|
|
| 254 |
module Eval (Prog : ProgType) : EvaluationType = |
|
| 255 |
struct |
|
| 256 |
module RecTheta = Rec (Prog) |
|
| 257 |
module Theta = RecTheta.Theta |
|
| 258 |
|
|
| 259 |
let eval_prog = |
|
| 260 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) |
|
| 261 |
end |
|
| 262 |
|
|
| 263 |
module Eval (Prog : ProgType) = |
|
| 264 |
struct |
|
| 265 |
module ThetaFunctor (Evaluation : EvaluationType) : ThetaType = |
|
| 266 |
struct |
|
| 267 |
let theta tag = (theta_ify Evaluation.kenv) tag |
|
| 268 |
end |
|
| 269 |
module EvaluationFunctor (Theta : ThetaType) : EvaluationType = |
|
| 270 |
struct |
|
| 271 |
include Denotation (Theta) |
|
| 272 |
|
|
| 273 |
let kenv = |
|
| 274 |
List.fold_left ( |
|
| 275 |
fun accu d -> match d with |
|
| 276 |
| State (p, defp) -> { accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node }
|
|
| 277 |
| Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc }
|
|
| 278 |
) {cont_node = []; cont_junc = []} Prog.defs
|
|
| 279 |
|
|
| 280 |
let eval_prog = |
|
| 281 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) |
|
| 282 |
end |
|
| 283 |
module rec Theta : ThetaType = ThetaFunctor (Evaluation) |
|
| 284 |
and Evaluation : EvaluationType = EvaluationFunctor (Theta) |
|
| 285 |
end |
|
| 286 |
*) |
|
| 375 |
(* module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType = struct |
|
| 376 |
include Denotation (Theta) |
|
| 377 |
|
|
| 378 |
let theta = let kenv = List.fold_left ( fun accu d -> match d with | State |
|
| 379 |
(p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp,
|
|
| 380 |
eval_S X p defp))::accu.cont_node } | Junction (j, defj) -> { accu with
|
|
| 381 |
cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = [];
|
|
| 382 |
cont_junc = []} Prog.defs in Obj.magic (fun tag -> theta_ify kenv tag) end |
|
| 383 |
module Rec (Prog : ProgType) = struct module rec Theta : ThetaType = |
|
| 384 |
ThetaFix (Prog) (Theta) end |
|
| 385 |
|
|
| 386 |
module Eval (Prog : ProgType) : EvaluationType = struct module RecTheta = |
|
| 387 |
Rec (Prog) module Theta = RecTheta.Theta |
|
| 388 |
|
|
| 389 |
let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D |
|
| 390 |
[Prog.init]) (Theta.theta E [Prog.init] [])) end |
|
| 391 |
|
|
| 392 |
module Eval (Prog : ProgType) = struct module ThetaFunctor (Evaluation : |
|
| 393 |
EvaluationType) : ThetaType = struct let theta tag = (theta_ify |
|
| 394 |
Evaluation.kenv) tag end module EvaluationFunctor (Theta : ThetaType) : |
|
| 395 |
EvaluationType = struct include Denotation (Theta) |
|
| 396 |
|
|
| 397 |
let kenv = List.fold_left ( fun accu d -> match d with | State (p, defp) -> |
|
| 398 |
{ accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp,
|
|
| 399 |
eval_S X p defp))::accu.cont_node } | Junction (j, defj) -> { accu with
|
|
| 400 |
cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = [];
|
|
| 401 |
cont_junc = []} Prog.defs |
|
| 402 |
|
|
| 403 |
let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D |
|
| 404 |
[Prog.init]) (Theta.theta E [Prog.init] [])) end module rec Theta : |
|
| 405 |
ThetaType = ThetaFunctor (Evaluation) and Evaluation : EvaluationType = |
|
| 406 |
EvaluationFunctor (Theta) end *) |
|
| 287 | 407 |
end |
Also available in: Unified diff
reformatting