Project

General

Profile

Download (4.62 KB) Statistics
| Branch: | Tag: | Revision:
1 93119c3f ploc
let sf_level = 2
2 eb70bae5 Christophe Garion
3 2de7fa82 ploc
(* Basic datatype for model elements: state and junction name, events ... *)
4 ca7ff3f7 Lélio Brun
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 eb70bae5 Christophe Garion
type user_variable_name_t = string
15 93119c3f ploc
16
(* Connected to lustrec types *)
17 ca7ff3f7 Lélio Brun
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 eb70bae5 Christophe Garion
31 2de7fa82 ploc
(* P(r)etty printers *)
32 ca7ff3f7 Lélio Brun
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 9ae027f8 ploc
let pp_base_act fmt a = Printers.pp_node_stmts fmt a.defs
46 ca7ff3f7 Lélio Brun
47
let pp_base_cond fmt c = Printers.pp_expr fmt c.expr
48 eb70bae5 Christophe Garion
49 2de7fa82 ploc
(* 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 ca7ff3f7 Lélio Brun
type frontier_t = Loose | Strict
59 2de7fa82 ploc
60
let pp_frontier fmt frontier =
61
  match frontier with
62 ca7ff3f7 Lélio Brun
  | Loose ->
63
    Format.fprintf fmt "Loose"
64
  | Strict ->
65
    Format.fprintf fmt "Strict"
66 2de7fa82 ploc
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 ca7ff3f7 Lélio Brun
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 2de7fa82 ploc
  type t
84 ca7ff3f7 Lélio Brun
85 2de7fa82 ploc
  val nil : t
86 ca7ff3f7 Lélio Brun
87 2de7fa82 ploc
  val aquote : base_action_t -> t
88 ca7ff3f7 Lélio Brun
89 2de7fa82 ploc
  val open_path : path_t -> t
90 ca7ff3f7 Lélio Brun
91 2de7fa82 ploc
  val close_path : path_t -> t
92 ca7ff3f7 Lélio Brun
93 2de7fa82 ploc
  val call : 'c call_t -> 'c -> t
94 eb70bae5 Christophe Garion
95 2de7fa82 ploc
  val pp_act : Format.formatter -> t -> unit
96
end
97
98 ca7ff3f7 Lélio Brun
module Action = struct
99 2de7fa82 ploc
  type t =
100
    | Quote : base_action_t -> t
101
    | Close : path_t -> t
102 ca7ff3f7 Lélio Brun
    | Open : path_t -> t
103
    | Call : 'c call_t * 'c -> t
104
    | Nil : t
105 eb70bae5 Christophe Garion
106 2de7fa82 ploc
  let nil = Nil
107 ca7ff3f7 Lélio Brun
108 2de7fa82 ploc
  let aquote act = Quote act
109 ca7ff3f7 Lélio Brun
110 2de7fa82 ploc
  let open_path p = Open p
111 ca7ff3f7 Lélio Brun
112 2de7fa82 ploc
  let close_path p = Close p
113 ca7ff3f7 Lélio Brun
114 2de7fa82 ploc
  let call c a = Call (c, a)
115
116
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
117 ca7ff3f7 Lélio Brun
   fun fmt call ->
118 2de7fa82 ploc
    match call with
119 ca7ff3f7 Lélio Brun
    | 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 2de7fa82 ploc
129
  let pp_act fmt act =
130
    match act with
131 ca7ff3f7 Lélio Brun
    | 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 2de7fa82 ploc
end
142
143 eb70bae5 Christophe Garion
let _ = (module Action : ActionType)
144 2de7fa82 ploc
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 ca7ff3f7 Lélio Brun
module type ConditionType = sig
148 2de7fa82 ploc
  type t
149 ca7ff3f7 Lélio Brun
150 2de7fa82 ploc
  val cquote : base_condition_t -> t
151 ca7ff3f7 Lélio Brun
152 2de7fa82 ploc
  val tru : t
153 ca7ff3f7 Lélio Brun
154 2de7fa82 ploc
  val active : path_t -> t
155 ca7ff3f7 Lélio Brun
156 2de7fa82 ploc
  val event : event_t -> t
157 ca7ff3f7 Lélio Brun
158 2de7fa82 ploc
  val ( && ) : t -> t -> t
159 ca7ff3f7 Lélio Brun
160 2de7fa82 ploc
  val neg : t -> t
161
162
  val pp_cond : Format.formatter -> t -> unit
163
end
164 ca7ff3f7 Lélio Brun
165
module Condition = struct
166 2de7fa82 ploc
  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 ca7ff3f7 Lélio Brun
176 2de7fa82 ploc
  let tru = True
177 ca7ff3f7 Lélio Brun
178 2de7fa82 ploc
  let neg cond = Neg cond
179 ca7ff3f7 Lélio Brun
180 2de7fa82 ploc
  let ( && ) cond1 cond2 = And (cond1, cond2)
181 ca7ff3f7 Lélio Brun
182 2de7fa82 ploc
  let active path = Active path
183 ca7ff3f7 Lélio Brun
184
  let event evt = match evt with None -> True | Some e -> Event e
185 2de7fa82 ploc
186
  let rec pp_cond fmt cond =
187
    match cond with
188 ca7ff3f7 Lélio Brun
    | 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 2de7fa82 ploc
end
201
202
let _ = (module Condition : ConditionType)
203 9c654082 ploc
204 ca7ff3f7 Lélio Brun
module GlobalVarDef = struct
205
  type t = { variable : Lustre_types.var_decl; init_val : Lustre_types.expr }
206 9c654082 ploc
end