Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/common/basetypes.ml | ||
---|---|---|
1 |
|
|
2 | 1 |
let sf_level = 2 |
3 | 2 |
|
4 | 3 |
(* Basic datatype for model elements: state and junction name, events ... *) |
5 |
type state_name_t = string |
|
6 |
type junction_name_t = string |
|
7 |
type path_t = state_name_t list |
|
8 |
type event_base_t = string |
|
9 |
type event_t = event_base_t option |
|
4 |
type state_name_t = string |
|
5 |
|
|
6 |
type junction_name_t = string |
|
7 |
|
|
8 |
type path_t = state_name_t list |
|
9 |
|
|
10 |
type event_base_t = string |
|
11 |
|
|
12 |
type event_t = event_base_t option |
|
13 |
|
|
10 | 14 |
type user_variable_name_t = string |
11 | 15 |
|
12 | 16 |
(* Connected to lustrec types *) |
13 |
type base_action_t = { defs : Lustre_types.statement list; |
|
14 |
ainputs: Lustre_types.var_decl list; |
|
15 |
aoutputs: Lustre_types.var_decl list; |
|
16 |
avariables: Lustre_types.var_decl list; |
|
17 |
(* ident: string; *) |
|
18 |
} |
|
19 |
type base_condition_t = { expr: Lustre_types.expr; |
|
20 |
cinputs: Lustre_types.var_decl list; |
|
21 |
coutputs: Lustre_types.var_decl list; |
|
22 |
cvariables: Lustre_types.var_decl list } |
|
17 |
type base_action_t = { |
|
18 |
defs : Lustre_types.statement list; |
|
19 |
ainputs : Lustre_types.var_decl list; |
|
20 |
aoutputs : Lustre_types.var_decl list; |
|
21 |
avariables : Lustre_types.var_decl list; (* ident: string; *) |
|
22 |
} |
|
23 |
|
|
24 |
type base_condition_t = { |
|
25 |
expr : Lustre_types.expr; |
|
26 |
cinputs : Lustre_types.var_decl list; |
|
27 |
coutputs : Lustre_types.var_decl list; |
|
28 |
cvariables : Lustre_types.var_decl list; |
|
29 |
} |
|
23 | 30 |
|
24 | 31 |
(* P(r)etty printers *) |
25 |
let pp_state_name = Format.pp_print_string |
|
26 |
let pp_junction_name = Format.pp_print_string |
|
27 |
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p |
|
28 |
let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s |
|
32 |
let pp_state_name = Format.pp_print_string |
|
33 |
|
|
34 |
let pp_junction_name = Format.pp_print_string |
|
35 |
|
|
36 |
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p |
|
37 |
|
|
38 |
let pp_event fmt e = |
|
39 |
match e with |
|
40 |
| None -> |
|
41 |
Format.fprintf fmt "none" |
|
42 |
| Some s -> |
|
43 |
Format.fprintf fmt "%s" s |
|
44 |
|
|
29 | 45 |
let pp_base_act fmt a = Printers.pp_node_stmts fmt a.defs |
30 |
let pp_base_cond fmt c= Printers.pp_expr fmt c.expr |
|
46 |
|
|
47 |
let pp_base_cond fmt c = Printers.pp_expr fmt c.expr |
|
31 | 48 |
|
32 | 49 |
(* Action and Condition types and functions. *) |
33 | 50 |
|
... | ... | |
38 | 55 |
|
39 | 56 |
TODO: these rich call type could be externalized and a functor introduced. *) |
40 | 57 |
|
41 |
type frontier_t = |
|
42 |
| Loose |
|
43 |
| Strict |
|
58 |
type frontier_t = Loose | Strict |
|
44 | 59 |
|
45 | 60 |
let pp_frontier fmt frontier = |
46 | 61 |
match frontier with |
47 |
| Loose -> Format.fprintf fmt "Loose" |
|
48 |
| Strict -> Format.fprintf fmt "Strict" |
|
62 |
| Loose -> |
|
63 |
Format.fprintf fmt "Loose" |
|
64 |
| Strict -> |
|
65 |
Format.fprintf fmt "Strict" |
|
49 | 66 |
|
50 | 67 |
type _ call_t = |
51 | 68 |
| Ecall : (path_t * path_t * frontier_t) call_t |
52 | 69 |
| Dcall : path_t call_t |
53 | 70 |
| Xcall : (path_t * frontier_t) call_t |
54 | 71 |
|
55 |
let pp_call : |
|
56 |
type a. Format.formatter -> a call_t -> unit = |
|
57 |
fun fmt call -> |
|
58 |
match call with |
|
59 |
| Ecall -> Format.fprintf fmt "CallE" |
|
60 |
| Dcall -> Format.fprintf fmt "CallD" |
|
61 |
| Xcall -> Format.fprintf fmt "CallX" |
|
62 |
|
|
63 |
module type ActionType = |
|
64 |
sig |
|
72 |
let pp_call : type a. Format.formatter -> a call_t -> unit = |
|
73 |
fun fmt call -> |
|
74 |
match call with |
|
75 |
| Ecall -> |
|
76 |
Format.fprintf fmt "CallE" |
|
77 |
| Dcall -> |
|
78 |
Format.fprintf fmt "CallD" |
|
79 |
| Xcall -> |
|
80 |
Format.fprintf fmt "CallX" |
|
81 |
|
|
82 |
module type ActionType = sig |
|
65 | 83 |
type t |
84 |
|
|
66 | 85 |
val nil : t |
86 |
|
|
67 | 87 |
val aquote : base_action_t -> t |
88 |
|
|
68 | 89 |
val open_path : path_t -> t |
90 |
|
|
69 | 91 |
val close_path : path_t -> t |
92 |
|
|
70 | 93 |
val call : 'c call_t -> 'c -> t |
71 | 94 |
|
72 | 95 |
val pp_act : Format.formatter -> t -> unit |
73 | 96 |
end |
74 | 97 |
|
75 |
|
|
76 |
module Action = |
|
77 |
struct |
|
98 |
module Action = struct |
|
78 | 99 |
type t = |
79 | 100 |
| Quote : base_action_t -> t |
80 | 101 |
| Close : path_t -> t |
81 |
| Open : path_t -> t |
|
82 |
| Call : 'c call_t * 'c -> t |
|
83 |
| Nil : t |
|
84 |
|
|
102 |
| Open : path_t -> t |
|
103 |
| Call : 'c call_t * 'c -> t |
|
104 |
| Nil : t |
|
85 | 105 |
|
86 | 106 |
let nil = Nil |
107 |
|
|
87 | 108 |
let aquote act = Quote act |
109 |
|
|
88 | 110 |
let open_path p = Open p |
111 |
|
|
89 | 112 |
let close_path p = Close p |
113 |
|
|
90 | 114 |
let call c a = Call (c, a) |
91 | 115 |
|
92 | 116 |
let pp_call : type c. Format.formatter -> c call_t -> c -> unit = |
93 |
fun fmt call ->
|
|
117 |
fun fmt call -> |
|
94 | 118 |
match call with |
95 |
| Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f) |
|
96 |
| Dcall -> (fun p -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p) |
|
97 |
| Xcall -> (fun (p, f) -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f) |
|
119 |
| Ecall -> |
|
120 |
fun (p, p', f) -> |
|
121 |
Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' |
|
122 |
pp_frontier f |
|
123 |
| Dcall -> |
|
124 |
fun p -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p |
|
125 |
| Xcall -> |
|
126 |
fun (p, f) -> |
|
127 |
Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f |
|
98 | 128 |
|
99 | 129 |
let pp_act fmt act = |
100 | 130 |
match act with |
101 |
| Call (c, a) -> pp_call fmt c a |
|
102 |
| Quote a -> Format.fprintf fmt "%a" pp_base_act a |
|
103 |
| Close p -> Format.fprintf fmt "Close(%a)" pp_path p |
|
104 |
| Open p -> Format.fprintf fmt "Open(%a)" pp_path p |
|
105 |
| Nil -> Format.fprintf fmt "Nil" |
|
131 |
| Call (c, a) -> |
|
132 |
pp_call fmt c a |
|
133 |
| Quote a -> |
|
134 |
Format.fprintf fmt "%a" pp_base_act a |
|
135 |
| Close p -> |
|
136 |
Format.fprintf fmt "Close(%a)" pp_path p |
|
137 |
| Open p -> |
|
138 |
Format.fprintf fmt "Open(%a)" pp_path p |
|
139 |
| Nil -> |
|
140 |
Format.fprintf fmt "Nil" |
|
106 | 141 |
end |
107 | 142 |
|
108 | 143 |
let _ = (module Action : ActionType) |
109 | 144 |
|
110 |
|
|
111 | 145 |
(* Conditions are either (1) simple strings, (2) the active status of a state or |
112 | 146 |
(3) occurence of an event. They can be combined (conjunction, negation) *) |
113 |
module type ConditionType = |
|
114 |
sig |
|
147 |
module type ConditionType = sig |
|
115 | 148 |
type t |
149 |
|
|
116 | 150 |
val cquote : base_condition_t -> t |
151 |
|
|
117 | 152 |
val tru : t |
153 |
|
|
118 | 154 |
val active : path_t -> t |
155 |
|
|
119 | 156 |
val event : event_t -> t |
157 |
|
|
120 | 158 |
val ( && ) : t -> t -> t |
159 |
|
|
121 | 160 |
val neg : t -> t |
122 | 161 |
|
123 | 162 |
val pp_cond : Format.formatter -> t -> unit |
124 | 163 |
end |
125 |
|
|
126 |
module Condition = |
|
127 |
struct |
|
164 |
|
|
165 |
module Condition = struct |
|
128 | 166 |
type t = |
129 | 167 |
| Quote of base_condition_t |
130 | 168 |
| Active of path_t |
... | ... | |
134 | 172 |
| True |
135 | 173 |
|
136 | 174 |
let cquote cond = Quote cond |
175 |
|
|
137 | 176 |
let tru = True |
177 |
|
|
138 | 178 |
let neg cond = Neg cond |
179 |
|
|
139 | 180 |
let ( && ) cond1 cond2 = And (cond1, cond2) |
181 |
|
|
140 | 182 |
let active path = Active path |
141 |
let event evt = |
|
142 |
match evt with |
|
143 |
| None -> True |
|
144 |
| Some e -> Event e |
|
183 |
|
|
184 |
let event evt = match evt with None -> True | Some e -> Event e |
|
145 | 185 |
|
146 | 186 |
let rec pp_cond fmt cond = |
147 | 187 |
match cond with |
148 |
| True -> Format.fprintf fmt "true" |
|
149 |
| Active p -> Format.fprintf fmt "Active(%a)" pp_path p |
|
150 |
| Event e -> Format.fprintf fmt "Event(%s)" e |
|
151 |
| Neg cond -> Format.fprintf fmt "(neg %a)" pp_cond cond |
|
152 |
| And (cond1, cond2) -> Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2 |
|
153 |
| Quote c -> Format.fprintf fmt "%a" pp_base_cond c |
|
154 |
|
|
188 |
| True -> |
|
189 |
Format.fprintf fmt "true" |
|
190 |
| Active p -> |
|
191 |
Format.fprintf fmt "Active(%a)" pp_path p |
|
192 |
| Event e -> |
|
193 |
Format.fprintf fmt "Event(%s)" e |
|
194 |
| Neg cond -> |
|
195 |
Format.fprintf fmt "(neg %a)" pp_cond cond |
|
196 |
| And (cond1, cond2) -> |
|
197 |
Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2 |
|
198 |
| Quote c -> |
|
199 |
Format.fprintf fmt "%a" pp_base_cond c |
|
155 | 200 |
end |
156 | 201 |
|
157 | 202 |
let _ = (module Condition : ConditionType) |
158 | 203 |
|
159 |
module GlobalVarDef = |
|
160 |
struct |
|
161 |
type t = {variable: Lustre_types.var_decl; init_val: Lustre_types.expr} |
|
204 |
module GlobalVarDef = struct |
|
205 |
type t = { variable : Lustre_types.var_decl; init_val : Lustre_types.expr } |
|
162 | 206 |
end |
Also available in: Unified diff
reformatting