Project

General

Profile

Download (4.67 KB) Statistics
| Branch: | Tag: | Revision:
1
let sf_level = 2
2

    
3
(* Basic datatype for model elements: state and junction name, events ... *)
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

    
14
type user_variable_name_t = string
15

    
16
(* Connected to lustrec types *)
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
}
30

    
31
(* P(r)etty printers *)
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 =
37
  Utils.Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ".") pp_state_name fmt p
38

    
39
let pp_event fmt e =
40
  match e with
41
  | None ->
42
    Format.fprintf fmt "none"
43
  | Some s ->
44
    Format.fprintf fmt "%s" s
45

    
46
let pp_base_act fmt a = Printers.pp_node_stmts fmt a.defs
47

    
48
let pp_base_cond fmt c = Printers.pp_expr fmt c.expr
49

    
50
(* Action and Condition types and functions. *)
51

    
52
(* Actions are defined by string + the opening and closing of states *)
53

    
54
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
55
   use of function calls in action.
56

    
57
   TODO: these rich call type could be externalized and a functor introduced. *)
58

    
59
type frontier_t = Loose | Strict
60

    
61
let pp_frontier fmt frontier =
62
  match frontier with
63
  | Loose ->
64
    Format.fprintf fmt "Loose"
65
  | Strict ->
66
    Format.fprintf fmt "Strict"
67

    
68
type _ call_t =
69
  | Ecall : (path_t * path_t * frontier_t) call_t
70
  | Dcall : path_t call_t
71
  | Xcall : (path_t * frontier_t) call_t
72

    
73
let pp_call : type a. Format.formatter -> a call_t -> unit =
74
 fun fmt call ->
75
  match call with
76
  | Ecall ->
77
    Format.fprintf fmt "CallE"
78
  | Dcall ->
79
    Format.fprintf fmt "CallD"
80
  | Xcall ->
81
    Format.fprintf fmt "CallX"
82

    
83
module type ActionType = sig
84
  type t
85

    
86
  val nil : t
87

    
88
  val aquote : base_action_t -> t
89

    
90
  val open_path : path_t -> t
91

    
92
  val close_path : path_t -> t
93

    
94
  val call : 'c call_t -> 'c -> t
95

    
96
  val pp_act : Format.formatter -> t -> unit
97
end
98

    
99
module Action = struct
100
  type t =
101
    | Quote : base_action_t -> t
102
    | Close : path_t -> t
103
    | Open : path_t -> t
104
    | Call : 'c call_t * 'c -> t
105
    | Nil : t
106

    
107
  let nil = Nil
108

    
109
  let aquote act = Quote act
110

    
111
  let open_path p = Open p
112

    
113
  let close_path p = Close p
114

    
115
  let call c a = Call (c, a)
116

    
117
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
118
   fun fmt call ->
119
    match call with
120
    | Ecall ->
121
      fun (p, p', f) ->
122
        Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p'
123
          pp_frontier f
124
    | Dcall ->
125
      fun p -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p
126
    | Xcall ->
127
      fun (p, f) ->
128
        Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f
129

    
130
  let pp_act fmt act =
131
    match act with
132
    | Call (c, a) ->
133
      pp_call fmt c a
134
    | Quote a ->
135
      Format.fprintf fmt "%a" pp_base_act a
136
    | Close p ->
137
      Format.fprintf fmt "Close(%a)" pp_path p
138
    | Open p ->
139
      Format.fprintf fmt "Open(%a)" pp_path p
140
    | Nil ->
141
      Format.fprintf fmt "Nil"
142
end
143

    
144
let _ = (module Action : ActionType)
145

    
146
(* Conditions are either (1) simple strings, (2) the active status of a state or
147
   (3) occurence of an event. They can be combined (conjunction, negation) *)
148
module type ConditionType = sig
149
  type t
150

    
151
  val cquote : base_condition_t -> t
152

    
153
  val tru : t
154

    
155
  val active : path_t -> t
156

    
157
  val event : event_t -> t
158

    
159
  val ( && ) : t -> t -> t
160

    
161
  val neg : t -> t
162

    
163
  val pp_cond : Format.formatter -> t -> unit
164
end
165

    
166
module Condition = struct
167
  type t =
168
    | Quote of base_condition_t
169
    | Active of path_t
170
    | Event of event_base_t
171
    | And of t * t
172
    | Neg of t
173
    | True
174

    
175
  let cquote cond = Quote cond
176

    
177
  let tru = True
178

    
179
  let neg cond = Neg cond
180

    
181
  let ( && ) cond1 cond2 = And (cond1, cond2)
182

    
183
  let active path = Active path
184

    
185
  let event evt = match evt with None -> True | Some e -> Event e
186

    
187
  let rec pp_cond fmt cond =
188
    match cond with
189
    | True ->
190
      Format.fprintf fmt "true"
191
    | Active p ->
192
      Format.fprintf fmt "Active(%a)" pp_path p
193
    | Event e ->
194
      Format.fprintf fmt "Event(%s)" e
195
    | Neg cond ->
196
      Format.fprintf fmt "(neg %a)" pp_cond cond
197
    | And (cond1, cond2) ->
198
      Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2
199
    | Quote c ->
200
      Format.fprintf fmt "%a" pp_base_cond c
201
end
202

    
203
let _ = (module Condition : ConditionType)
204

    
205
module GlobalVarDef = struct
206
  type t = { variable : Lustre_types.var_decl; init_val : Lustre_types.expr }
207
end
(3-3/6)