Revision ca7ff3f7
Added by Lélio Brun 7 months 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