Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

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