Project

General

Profile

Download (4.62 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 = 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

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

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

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

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

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

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

    
58
type frontier_t = Loose | Strict
59

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

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

    
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
83
  type t
84

    
85
  val nil : t
86

    
87
  val aquote : base_action_t -> t
88

    
89
  val open_path : path_t -> t
90

    
91
  val close_path : path_t -> t
92

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

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

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

    
106
  let nil = Nil
107

    
108
  let aquote act = Quote act
109

    
110
  let open_path p = Open p
111

    
112
  let close_path p = Close p
113

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

    
116
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
117
   fun fmt call ->
118
    match call with
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
128

    
129
  let pp_act fmt act =
130
    match act with
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"
141
end
142

    
143
let _ = (module Action : ActionType)
144

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

    
150
  val cquote : base_condition_t -> t
151

    
152
  val tru : t
153

    
154
  val active : path_t -> t
155

    
156
  val event : event_t -> t
157

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

    
160
  val neg : t -> t
161

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

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

    
174
  let cquote cond = Quote cond
175

    
176
  let tru = True
177

    
178
  let neg cond = Neg cond
179

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

    
182
  let active path = Active path
183

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

    
186
  let rec pp_cond fmt cond =
187
    match cond with
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
200
end
201

    
202
let _ = (module Condition : ConditionType)
203

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