Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun 8 months ago

reformatting

View differences:

src/tools/stateflow/semantics/cPS_lustre_generator.ml
1 1
open Basetypes
2 2
open CPS_transformer
3 3

  
4
let ff = Format.fprintf 
5
       
6
module LustrePrinter (
7
  Vars : sig
8
    val state_vars : ActiveStates.Vars.t
9
    val global_vars : GlobalVarDef.t list
10

  
11
  end) : TransformerType =
12
struct
4
let ff = Format.fprintf
5

  
6
module LustrePrinter (Vars : sig
7
  val state_vars : ActiveStates.Vars.t
8

  
9
  val global_vars : GlobalVarDef.t list
10
end) : TransformerType = struct
13 11
  include TransformerStub
14 12

  
15 13
  type name_t = string
16
  type t_base = { statements : Lustre_types.statement list; assert_false: bool }
17
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
18 14

  
19
	
15
  type t_base = {
16
    statements : Lustre_types.statement list;
17
    assert_false : bool;
18
  }
19

  
20
  type t = name_t -> name_t -> ActiveStates.Vars.t * t_base
21

  
20 22
  let new_loc, reset_loc =
21 23
    let cpt = ref 0 in
22
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
23
     (fun () -> cpt := 0))
24
    ( (fun () ->
25
        incr cpt;
26
        Format.sprintf "loc_%i" !cpt),
27
      fun () -> cpt := 0 )
24 28

  
25 29
  let new_aut, _reset_aut =
26 30
    let cpt = ref 0 in
27
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
28
     (fun () -> cpt := 0))
29
      
31
    ( (fun () ->
32
        incr cpt;
33
        Format.sprintf "aut_%i" !cpt),
34
      fun () -> cpt := 0 )
35

  
30 36
  let pp_path prefix fmt path =
31
    Format.fprintf fmt "%s%t"
32
      prefix
33
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
37
    Format.fprintf fmt "%s%t" prefix (fun fmt ->
38
        Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
34 39

  
35 40
  (* let pp_typed_path sin fmt path =
36 41
   *   Format.fprintf fmt "%a : bool" (pp_path sin) path *)
......
39 44
   *   Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) *)
40 45
  (* let pp_vars_decl sin fmt vars =
41 46
   *   Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) *)
42
       
47

  
43 48
  let var_to_ident prefix p =
44 49
    pp_path prefix Format.str_formatter p;
45 50
    Format.flush_str_formatter ()
46 51

  
47
  let vars_to_ident_list ?(prefix="") vars =
48
    List.map (
49
      fun p -> var_to_ident prefix p
50
    ) (ActiveStates.Vars.elements vars)
52
  let vars_to_ident_list ?(prefix = "") vars =
53
    List.map (fun p -> var_to_ident prefix p) (ActiveStates.Vars.elements vars)
51 54

  
52
  let mkvar name typ = 
55
  let mkvar name typ =
53 56
    let loc = Location.dummy_loc in
54
    Corelang.mkvar_decl
55
      loc
56
      (name, typ, Corelang.mkclock loc Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *))
57
    Corelang.mkvar_decl loc
58
      ( name,
59
        typ,
60
        Corelang.mkclock loc Lustre_types.Ckdec_any,
61
        false,
62
        None,
63
        None (*"__no_parent__" *) )
64

  
65
  let var_to_vdecl ?(prefix = "") var typ = mkvar (var_to_ident prefix var) typ
57 66

  
58
  let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
59
  let state_vars_to_vdecl_list ?(prefix="") vars =
67
  let state_vars_to_vdecl_list ?(prefix = "") vars =
60 68
    let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in
61
    List.map 
62
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
69
    List.map
70
      (fun v -> var_to_vdecl ~prefix v bool_type)
63 71
      (ActiveStates.Vars.elements vars)
64 72

  
65 73
  let mk_locals locs =
66
    ActiveStates.Vars.fold (fun v accu ->
67
      (state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu
68
    ) locs []
69
     (* TODO: declare global vars *)
74
    ActiveStates.Vars.fold
75
      (fun v accu ->
76
        state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars @ accu)
77
      locs []
78
  (* TODO: declare global vars *)
70 79

  
71 80
  let mkeq = Corelang.mkeq Location.dummy_loc
81

  
72 82
  let mkexpr = Corelang.mkexpr Location.dummy_loc
83

  
73 84
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
74
  let expr_of_bool b = mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))
75
  let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =
76
    { statements = [
77
      Lustre_types.Eq (
78
	mkeq (
79
	  vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *)
80
	  rhs (* rhs *)
81
	)
82
      )
83
      ];
84
      assert_false = false
85

  
86
  let expr_of_bool b =
87
    mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))
88

  
89
  let mkstmt_eq lhs_vars ?(prefix_lhs = "") rhs =
90
    {
91
      statements =
92
        [
93
          Lustre_types.Eq
94
            (mkeq
95
               ( vars_to_ident_list ~prefix:prefix_lhs lhs_vars,
96
                 (* lhs *)
97
                 rhs (* rhs *) ));
98
        ];
99
      assert_false = false;
85 100
    }
101

  
86 102
  let base_to_assert b =
87 103
    if b.assert_false then
88
      [{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
89
    else
90
      []
104
      [
105
        {
106
          Lustre_types.assert_expr = expr_of_bool false;
107
          assert_loc = Location.dummy_loc;
108
        };
109
      ]
110
    else []
91 111

  
92
    
93
  let var_to_expr ?(prefix="") p =
112
  let var_to_expr ?(prefix = "") p =
94 113
    let id = var_to_ident prefix p in
95 114
    Corelang.expr_of_ident id Location.dummy_loc
96 115

  
97
  let vars_to_exprl ?(prefix="") vars =
98
    List.map
99
      (fun p -> var_to_expr ~prefix:prefix p)
100
      (ActiveStates.Vars.elements vars)
101

  
116
  let vars_to_exprl ?(prefix = "") vars =
117
    List.map (fun p -> var_to_expr ~prefix p) (ActiveStates.Vars.elements vars)
102 118

  
103 119
  (* Events *)
104 120
  let event_type_decl =
105 121
    Corelang.mktop
106
      (
107
	Lustre_types.TypeDef {
108
	  Lustre_types.tydef_id = "event_type";
109
	  tydef_desc = Lustre_types.Tydec_int
110
	}
111
      )
112
    
113
  let event_type = {
114
    Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
115
    Lustre_types.ty_dec_loc = Location.dummy_loc;
116
  }
117
    
118
  let event_var = mkvar "event" event_type 
122
      (Lustre_types.TypeDef
123
         {
124
           Lustre_types.tydef_id = "event_type";
125
           tydef_desc = Lustre_types.Tydec_int;
126
         })
119 127

  
128
  let event_type =
129
    {
130
      Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
131
      Lustre_types.ty_dec_loc = Location.dummy_loc;
132
    }
133

  
134
  let event_var = mkvar "event" event_type
120 135

  
121 136
  let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
137

  
122 138
  let get_event_const e =
123 139
    try Hashtbl.find const_map e
124
    with Not_found -> (
140
    with Not_found ->
125 141
      let nb = Hashtbl.length const_map in
126 142
      Hashtbl.add const_map e nb;
127
      nb	
128
    )
143
      nb
129 144

  
130

  
131
      
132 145
  let null sin sout =
133 146
    let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
134
    ActiveStates.Vars.empty,
135
    (
147
    ( ActiveStates.Vars.empty,
136 148
      (* Nothing happen here: out_vars = in_vars *)
137
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
138
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
139
    )
140
      
149
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
150
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs )
151

  
141 152
  let bot sin sout =
142 153
    let _, tr = null sin sout in
143
    (
144
      ActiveStates.Vars.empty,
145
      { tr with assert_false = true }
146
    )
147
      
154
    ActiveStates.Vars.empty, { tr with assert_false = true }
155

  
148 156
  let ( >> ) tr1 tr2 sin sout =
149 157
    let l = new_loc () in
150 158
    let vars1, tr1 = tr1 sin l in
151 159
    let vars2, tr2 = tr2 l sout in
152
    (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
153
     {
154
       statements = tr1.statements @ tr2.statements;
155
       assert_false = tr1.assert_false || tr2.assert_false
156
     }
157
    )
158
      
159
  let pp_name :
160
  type c. c call_t  -> c -> unit =
161
    fun call -> 
162
      match call with
163
      | Ecall -> (fun (p, p', f) ->
164
	Format.fprintf Format.str_formatter "theta%a%a%a_%a"
165
	  pp_call call
166
	  (pp_path "_from_") p
167
	  (pp_path "_to_") p'
168
	  pp_frontier f)
169
      | Dcall -> (fun p          ->
170
	Format.fprintf Format.str_formatter "theta%a%a"
171
	  pp_call call
172
	  (pp_path "_from_") p)
173
      | Xcall -> (fun (p, f)     ->
174
	Format.fprintf Format.str_formatter "theta%a%a_%a"
175
	  pp_call call
176
	  (pp_path "_from_") p
177
	  pp_frontier f)
178
	     
179

  
180
  let mkcall' :
181
  type c. name_t -> name_t -> c call_t -> c -> t_base =
182
    fun sin sout call arg ->
183
      pp_name call arg;
184
      let funname = Format.flush_str_formatter () in
185
      let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
186
      let rhs = mkpredef_call funname args in
187
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
188
	
160
    ( ActiveStates.Vars.add [ l ] (ActiveStates.Vars.union vars1 vars2),
161
      {
162
        statements = tr1.statements @ tr2.statements;
163
        assert_false = tr1.assert_false || tr2.assert_false;
164
      } )
165

  
166
  let pp_name : type c. c call_t -> c -> unit =
167
   fun call ->
168
    match call with
169
    | Ecall ->
170
      fun (p, p', f) ->
171
        Format.fprintf Format.str_formatter "theta%a%a%a_%a" pp_call call
172
          (pp_path "_from_") p (pp_path "_to_") p' pp_frontier f
173
    | Dcall ->
174
      fun p ->
175
        Format.fprintf Format.str_formatter "theta%a%a" pp_call call
176
          (pp_path "_from_") p
177
    | Xcall ->
178
      fun (p, f) ->
179
        Format.fprintf Format.str_formatter "theta%a%a_%a" pp_call call
180
          (pp_path "_from_") p pp_frontier f
181

  
182
  let mkcall' : type c. name_t -> name_t -> c call_t -> c -> t_base =
183
   fun sin sout call arg ->
184
    pp_name call arg;
185
    let funname = Format.flush_str_formatter () in
186
    let args =
187
      Corelang.expr_of_vdecl event_var
188
      :: vars_to_exprl ~prefix:sin Vars.state_vars
189
    in
190
    let rhs = mkpredef_call funname args in
191
    mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
192

  
189 193
  let mkact' action sin sout =
190 194
    match action with
191
    | Action.Call (c, a) -> mkcall' sin sout c a
192
    | Action.Quote a     ->
193
        (* TODO: check. This seems to be innappropriate *)
194
        (* let funname = "action_" ^ a.ident in
195
	let args = vars_to_exprl ~prefix:sin Vars.state_vars in
196
	let rhs = mkpredef_call funname args in
197
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
198
	*)
199
       {
200
	 statements = a.defs;
201
	 assert_false = false
202
       }
203
    | Action.Open p      ->
204
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
205
       (* eq1: sout_p = true *)
206
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in
207
       (* eq2: sout_xx = sin_xx *)
208
       let expr_list = vars_to_exprl ~prefix:sin vars' in
209
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
210
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
211
	 {
212
	   statements = [
213
	     Lustre_types.Eq (eq1);
214
	     Lustre_types.Eq (eq2);
215
	   ];
216
	   assert_false = false
217
	 }
218
	 
219
    | Action.Close p     ->
220
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
221
       (* eq1: sout_p = false *)
222
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in
223
       (* eq2: sout_xx = sin_xx *)
224
       let expr_list = vars_to_exprl ~prefix:sin vars' in
225
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
226
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
227
	 {
228
	   statements = [
229
	     Lustre_types.Eq (eq1);
230
	     Lustre_types.Eq (eq2);
231
	   ];
232
	   assert_false = false
233
	 }
234

  
235
    | Action.Nil         ->
236
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
237
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
238
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
239
	 
240
  let eval_act _kenv (action : act_t) =
241
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
242
    (fun sin sout -> (ActiveStates.Vars.empty,
243
    	      mkact' action sin sout   ))
195
    | Action.Call (c, a) ->
196
      mkcall' sin sout c a
197
    | Action.Quote a ->
198
      (* TODO: check. This seems to be innappropriate *)
199
      (* let funname = "action_" ^ a.ident in let args = vars_to_exprl
200
         ~prefix:sin Vars.state_vars in let rhs = mkpredef_call funname args in
201
         mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs *)
202
      { statements = a.defs; assert_false = false }
203
    | Action.Open p ->
204
      let vars' = ActiveStates.Vars.remove p Vars.state_vars in
205
      (* eq1: sout_p = true *)
206
      let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool true) in
207
      (* eq2: sout_xx = sin_xx *)
208
      let expr_list = vars_to_exprl ~prefix:sin vars' in
209
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
210
      let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
211
      {
212
        statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];
213
        assert_false = false;
214
      }
215
    | Action.Close p ->
216
      let vars' = ActiveStates.Vars.remove p Vars.state_vars in
217
      (* eq1: sout_p = false *)
218
      let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool false) in
219
      (* eq2: sout_xx = sin_xx *)
220
      let expr_list = vars_to_exprl ~prefix:sin vars' in
221
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
222
      let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
223
      {
224
        statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];
225
        assert_false = false;
226
      }
227
    | Action.Nil ->
228
      let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
229
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
230
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
231

  
232
  let eval_act _kenv (action : act_t)
233
      (*Format.printf "----- action = %a@." Action.pp_act action;*)
234
        sin sout =
235
    ActiveStates.Vars.empty, mkact' action sin sout
244 236

  
245 237
  let rec mkcond' sin condition =
246 238
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
247 239
    match condition with
248
    | Condition.True               -> expr_of_bool true
249
    | Condition.Active p           -> var_to_expr ~prefix:sin p
250
    | Condition.Event e            ->
251
       mkpredef_call "=" [
252
	 Corelang.expr_of_vdecl event_var;
253
	 mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e)))
254
       ]
255
    | Condition.Neg cond           -> mkpredef_call "not" [mkcond' sin cond]
256
    | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1;
257
							  mkcond' sin cond2]
258
    | Condition.Quote c            -> c.expr (* TODO: shall we prefix with sin ? *)
259

  
260
  let eval_cond condition (ok:t) ko sin sout =
240
    | Condition.True ->
241
      expr_of_bool true
242
    | Condition.Active p ->
243
      var_to_expr ~prefix:sin p
244
    | Condition.Event e ->
245
      mkpredef_call "="
246
        [
247
          Corelang.expr_of_vdecl event_var;
248
          mkexpr
249
            (Lustre_types.Expr_const
250
               (Lustre_types.Const_int (get_event_const e)));
251
        ]
252
    | Condition.Neg cond ->
253
      mkpredef_call "not" [ mkcond' sin cond ]
254
    | Condition.And (cond1, cond2) ->
255
      mkpredef_call "&&" [ mkcond' sin cond1; mkcond' sin cond2 ]
256
    | Condition.Quote c ->
257
      c.expr
258
  (* TODO: shall we prefix with sin ? *)
259

  
260
  let eval_cond condition (ok : t) ko sin sout =
261 261
    let open Lustre_types in
262 262
    let loc = Location.dummy_loc in
263 263
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
......
265 265
    let vars2, tr2 = ko sin sout in
266 266
    let _, tr0 = bot sin sout in
267 267
    let aut = new_aut () in
268
    (ActiveStates.Vars.empty,
269
     {
270
       statements = [
271
	 let handler_default_mode =          	      (* Default mode : CenterPoint *)
272
	   let handler_default_mode_unless = [
273
	     (loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut);
274
	     (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);
275
	   ]
276
	   in
277
	   Automata.mkhandler
278
	     loc                                      (* location *)
279
	     ("CenterPoint_" ^ aut)                   (* state name *)
280
	     handler_default_mode_unless              (* unless *)
281
	     []                                       (* until *)
282
	     []                                       (* locals *)
283
	     (tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *)
284
	 in
285
	 let handler_cond_mode =                       	 (* Cond mode *)
286
       	   let handler_cond_mode_until = [
287
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
288
       	   ]
289
	   in
290
	   Automata.mkhandler
291
	     loc                                      (* location *)
292
	     ("Cond_" ^ aut)                          (* state name *)
293
	     []                                       (* unless *)
294
	     handler_cond_mode_until                  (* until *)
295
	     (mk_locals vars1)                        (* locals *)
296
	     (tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *)
297
	 in
298
	 let handler_notcond_mode =                       	 (* NotCond mode *)
299
       	   let handler_notcond_mode_until = [
300
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
301
       	   ]
302
	   in
303
	   Automata.mkhandler
304
	     loc                                      (* location *)
305
	     ("NotCond_" ^ aut)                       (* state name *)
306
	     []                                       (* unless *)
307
	     handler_notcond_mode_until               (* until *)
308
	     (mk_locals vars2)                        (* locals *)
309
	     (tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *)
310
	 in
311
	 let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in
312
	 Aut (Automata.mkautomata loc aut handlers)
313
       ];
314
       assert_false = false
315
     }
316
    )
317
      
268
    ( ActiveStates.Vars.empty,
269
      {
270
        statements =
271
          [
272
            (let handler_default_mode =
273
               (* Default mode : CenterPoint *)
274
               let handler_default_mode_unless =
275
                 [
276
                   loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut;
277
                   ( loc,
278
                     mkcond' sin (Condition.Neg condition),
279
                     true (* restart *),
280
                     "NotCond_" ^ aut );
281
                 ]
282
               in
283
               Automata.mkhandler loc
284
                 (* location *)
285
                 ("CenterPoint_" ^ aut)
286
                 (* state name *)
287
                 handler_default_mode_unless (* unless *) [] (* until *) []
288
                 (* locals *)
289
                 (tr0.statements, base_to_assert tr0, [])
290
               (* stmts, asserts, annots *)
291
             in
292
             let handler_cond_mode =
293
               (* Cond mode *)
294
               let handler_cond_mode_until =
295
                 [
296
                   ( loc,
297
                     expr_of_bool true,
298
                     true (* restart *),
299
                     "CenterPoint_" ^ aut );
300
                 ]
301
               in
302
               Automata.mkhandler loc
303
                 (* location *)
304
                 ("Cond_" ^ aut)
305
                 (* state name *)
306
                 [] (* unless *) handler_cond_mode_until
307
                 (* until *)
308
                 (mk_locals vars1)
309
                 (* locals *)
310
                 (tr1.statements, base_to_assert tr1, [])
311
               (* stmts, asserts, annots *)
312
             in
313
             let handler_notcond_mode =
314
               (* NotCond mode *)
315
               let handler_notcond_mode_until =
316
                 [
317
                   ( loc,
318
                     expr_of_bool true,
319
                     true (* restart *),
320
                     "CenterPoint_" ^ aut );
321
                 ]
322
               in
323
               Automata.mkhandler loc
324
                 (* location *)
325
                 ("NotCond_" ^ aut)
326
                 (* state name *)
327
                 [] (* unless *) handler_notcond_mode_until
328
                 (* until *)
329
                 (mk_locals vars2)
330
                 (* locals *)
331
                 (tr2.statements, base_to_assert tr2, [])
332
               (* stmts, asserts, annots *)
333
             in
334
             let handlers =
335
               [ handler_default_mode; handler_cond_mode; handler_notcond_mode ]
336
             in
337
             Aut (Automata.mkautomata loc aut handlers));
338
          ];
339
        assert_false = false;
340
      } )
341

  
318 342
  (* let mktransformer tr =
319 343
   *   let _, tr = tr "sin_" "sout_"
320
   *   in tr  *)
321
    
322
  let mkcomponent :
323
  type c. c call_t -> c -> t -> Lustre_types.program_t =
324
    fun call args ->
325
      fun tr ->
326
	reset_loc ();
327
	let (vars', tr') = tr "sin_" "sout_" in
328
	pp_name call args;
329
	let funname = Format.flush_str_formatter () in
330
	let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in
331
	let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
332
	let node =
333
	  Corelang.mktop (	
334
	    Lustre_types.Node {Lustre_types.node_id = funname;
335
			   node_type = Types.new_var ();
336
			   node_clock = Clocks.new_var true;
337
			   node_inputs = inputs;
338
			   node_outputs = outputs;
339
			   node_locals = mk_locals vars'; (* TODO: add global vars *)
340
			   node_gencalls = [];
341
			   node_checks = [];
342
			   node_stmts = tr'.statements;
343
			   node_asserts = base_to_assert tr';
344
			   node_dec_stateless = false;
345
			   node_stateless = None;
346
			   node_spec = None;
347
			   node_annot = [];
348
                           node_iscontract = false}
349
      )  
350
	in
351
	[node]
352

  
353

  
354

  
355
	  (* TODO
356
	     C'est pas evident. 
357
Il faut faire les choses suivantes:
358
- rajouter dans un ensemble les variables manipulées localement
359
- on doit comprendre comment les variables globales sont injectées dans le modele final:
360
   - le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.
361
   - elles peuvent/doivent etre dans input et output de ce node thetacallD
362
	  *)
363

  
364
	  
344
   *   in tr *)
345

  
346
  let mkcomponent : type c. c call_t -> c -> t -> Lustre_types.program_t =
347
   fun call args tr ->
348
    reset_loc ();
349
    let vars', tr' = tr "sin_" "sout_" in
350
    pp_name call args;
351
    let funname = Format.flush_str_formatter () in
352
    let inputs =
353
      event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars
354
    in
355
    let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
356
    let node =
357
      Corelang.mktop
358
        (Lustre_types.Node
359
           {
360
             Lustre_types.node_id = funname;
361
             node_type = Types.new_var ();
362
             node_clock = Clocks.new_var true;
363
             node_inputs = inputs;
364
             node_outputs = outputs;
365
             node_locals = mk_locals vars';
366
             (* TODO: add global vars *)
367
             node_gencalls = [];
368
             node_checks = [];
369
             node_stmts = tr'.statements;
370
             node_asserts = base_to_assert tr';
371
             node_dec_stateless = false;
372
             node_stateless = None;
373
             node_spec = None;
374
             node_annot = [];
375
             node_iscontract = false;
376
           })
377
    in
378
    [ node ]
379

  
380
  (* TODO C'est pas evident. Il faut faire les choses suivantes: - rajouter dans
381
     un ensemble les variables manipulées localement - on doit comprendre
382
     comment les variables globales sont injectées dans le modele final: - le
383
     node principal doit uniquement les afficher. Il peut les initialiser avec
384
     les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.
385
     - elles peuvent/doivent etre dans input et output de ce node thetacallD *)
386

  
365 387
  let mk_main_loop () =
366 388
    (* let loc = Location.dummy_loc in *)
367
    
368 389
    let call_stmt =
369 390
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
370 391
      let init =
371
	let init_state_false =
372
	  List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
373
	let init_globals =
374
	  List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
375
	mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))
392
        let init_state_false =
393
          List.map
394
            (fun _ -> expr_of_bool false)
395
            (ActiveStates.Vars.elements Vars.state_vars)
396
        in
397
        let init_globals =
398
          List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars
399
        in
400
        mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))
376 401
      in
377
      let args = (Corelang.expr_of_vdecl event_var)::
378
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
402
      let args =
403
        Corelang.expr_of_vdecl event_var
404
        :: vars_to_exprl ~prefix:"sout_" Vars.state_vars
379 405
      in
380 406
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
381
      let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in
407
      let pre_call_expr = mkexpr (Lustre_types.Expr_pre call_expr) in
382 408
      let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in
383 409
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
384 410
    in
385
    let inputs = List.map Corelang.copy_var_decl [event_var] in
411
    let inputs = List.map Corelang.copy_var_decl [ event_var ] in
386 412
    let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
387 413
    (* TODO add the globals as sout_data_x entry values *)
388 414
    let node_principal =
389
      Corelang.mktop (	
390
	Lustre_types.Node {Lustre_types.node_id = "principal_loop";
391
			 node_type = Types.new_var ();
392
			 node_clock = Clocks.new_var true;
393
			 node_inputs = inputs;
394
			 node_outputs = outputs;
395
			 node_locals = []; (* TODO: add global vars *)
396
			 node_gencalls = [];
397
			 node_checks = [];
398
			 node_asserts = base_to_assert call_stmt; 
399
			 node_stmts = call_stmt.statements;
400
			 node_dec_stateless = false;
401
			 node_stateless = None;
402
			 node_spec = None;
403
			 node_annot = [];
404
                         node_iscontract = false;}
405
      )  
415
      Corelang.mktop
416
        (Lustre_types.Node
417
           {
418
             Lustre_types.node_id = "principal_loop";
419
             node_type = Types.new_var ();
420
             node_clock = Clocks.new_var true;
421
             node_inputs = inputs;
422
             node_outputs = outputs;
423
             node_locals = [];
424
             (* TODO: add global vars *)
425
             node_gencalls = [];
426
             node_checks = [];
427
             node_asserts = base_to_assert call_stmt;
428
             node_stmts = call_stmt.statements;
429
             node_dec_stateless = false;
430
             node_stateless = None;
431
             node_spec = None;
432
             node_annot = [];
433
             node_iscontract = false;
434
           })
406 435
    in
407 436
    node_principal
408
    
409 437

  
410 438
  let mkprincipal tr =
411
    event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
412

  
439
    event_type_decl :: mkcomponent Dcall [ "principal" ] tr
440
    @ [ mk_main_loop () ]
413 441
end
414 442

  
415 443
(* Local Variables: *)

Also available in: Unified diff