Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/semantics/cPS.ml | ||
---|---|---|
3 | 3 |
open CPS_transformer |
4 | 4 |
open Theta |
5 | 5 |
|
6 |
module Semantics = functor (T: TransformerType) (M: MODEL_T) -> |
|
7 |
struct |
|
8 |
|
|
9 |
module Prog = |
|
10 |
struct |
|
11 |
let init, defs, state_vars, globals = |
|
12 |
let Program (init, defs, globals) = M.model in |
|
13 |
let state_vars = SF.states M.model in |
|
14 |
init, defs, state_vars, globals |
|
15 |
|
|
16 |
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *) |
|
17 |
end |
|
18 |
|
|
19 |
|
|
20 |
module Interp = CPS_interpreter.Interpreter (T) |
|
21 |
module KenvTheta = KenvTheta (T) |
|
22 |
module Tables = KenvTheta.MemoThetaTables () |
|
23 |
|
|
24 |
let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) = |
|
25 |
let module Modularity : KenvTheta.ModularType = |
|
26 |
struct |
|
27 |
let modular : type b. (path_t, b, bool) tag_t -> path_t -> b = |
|
28 |
fun tag -> |
|
29 |
match tag with |
|
30 |
| E -> (fun _p _p' _f -> modular_entry) |
|
31 |
| D -> (fun _p -> modular_during) |
|
32 |
| X -> (fun _p _f -> modular_exit) |
|
33 |
end |
|
34 |
in |
|
35 |
let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in |
|
36 |
let module EvalProg = Interp.Evaluation (Thetaify) (Prog) in |
|
37 |
(module EvalProg: Interp.EvaluationType) |
|
38 |
|
|
39 |
let compute modular = |
|
40 |
let module Eval = (val (eval modular)) in |
|
41 |
Eval.eval_prog |
|
42 |
|
|
43 |
let code_gen modular = |
|
44 |
let module Eval = (val (eval modular)) in |
|
45 |
let principal, components = Eval.eval_prog, Eval.eval_components in |
|
46 |
List.flatten (List.map (fun (c, tr) -> T.mkcomponent Ecall c tr) (components Ecall))@ |
|
47 |
List.flatten (List.map (fun (c, tr) -> T.mkcomponent Dcall c tr) (components Dcall))@ |
|
48 |
List.flatten (List.map (fun (c, tr) -> T.mkcomponent Xcall c tr) (components Xcall))@ |
|
49 |
(T.mkprincipal principal) |
|
50 |
end |
|
6 |
module Semantics = |
|
7 |
functor |
|
8 |
(T : TransformerType) |
|
9 |
(M : MODEL_T) |
|
10 |
-> |
|
11 |
struct |
|
12 |
module Prog = struct |
|
13 |
let init, defs, state_vars, globals = |
|
14 |
let (Program (init, defs, globals)) = M.model in |
|
15 |
let state_vars = SF.states M.model in |
|
16 |
init, defs, state_vars, globals |
|
17 |
|
|
18 |
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src |
|
19 |
defs; () *) |
|
20 |
end |
|
21 |
|
|
22 |
module Interp = CPS_interpreter.Interpreter (T) |
|
23 |
module KenvTheta = KenvTheta (T) |
|
24 |
|
|
25 |
module Tables = KenvTheta.MemoThetaTables () |
|
26 |
|
|
27 |
let eval |
|
28 |
((modular_entry : bool), (modular_during : bool), (modular_exit : bool)) |
|
29 |
= |
|
30 |
let module Modularity : KenvTheta.ModularType = struct |
|
31 |
let modular : type b. (path_t, b, bool) tag_t -> path_t -> b = |
|
32 |
fun tag -> |
|
33 |
match tag with |
|
34 |
| E -> |
|
35 |
fun _p _p' _f -> modular_entry |
|
36 |
| D -> |
|
37 |
fun _p -> modular_during |
|
38 |
| X -> |
|
39 |
fun _p _f -> modular_exit |
|
40 |
end in |
|
41 |
let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in |
|
42 |
let module EvalProg = Interp.Evaluation (Thetaify) (Prog) in |
|
43 |
(module EvalProg : Interp.EvaluationType) |
|
44 |
|
|
45 |
let compute modular = |
|
46 |
let module Eval = (val eval modular) in |
|
47 |
Eval.eval_prog |
|
48 |
|
|
49 |
let code_gen modular = |
|
50 |
let module Eval = (val eval modular) in |
|
51 |
let principal, components = Eval.eval_prog, Eval.eval_components in |
|
52 |
List.flatten |
|
53 |
(List.map (fun (c, tr) -> T.mkcomponent Ecall c tr) (components Ecall)) |
|
54 |
@ List.flatten |
|
55 |
(List.map |
|
56 |
(fun (c, tr) -> T.mkcomponent Dcall c tr) |
|
57 |
(components Dcall)) |
|
58 |
@ List.flatten |
|
59 |
(List.map |
|
60 |
(fun (c, tr) -> T.mkcomponent Xcall c tr) |
|
61 |
(components Xcall)) |
|
62 |
@ T.mkprincipal principal |
|
63 |
end |
Also available in: Unified diff
reformatting