Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/expand.ml
19 19
(* Applies clock substitutions *)
20 20
let rec subst_ck ck_substs var_substs ck =
21 21
  match ck.cdesc with
22
  | Carrow (ck1,ck2) ->
23
      {ck with cdesc =
24
       Carrow (subst_ck ck_substs var_substs ck1,
25
               subst_ck ck_substs var_substs ck2)}
22
  | Carrow (ck1, ck2) ->
23
    {
24
      ck with
25
      cdesc =
26
        Carrow
27
          (subst_ck ck_substs var_substs ck1, subst_ck ck_substs var_substs ck2);
28
    }
26 29
  | Ctuple cklist ->
27
      {ck with cdesc =
28
       Ctuple (List.map (subst_ck ck_substs var_substs) cklist)}
29
  | Con (ck',c) ->
30
      {ck with cdesc =
31
       Con (subst_ck ck_substs var_substs ck',c)}
32
  | Connot (ck',c) ->
33
      {ck with cdesc =
34
       Connot (subst_ck ck_substs var_substs ck',c)}
35
  | Pck_up (ck',k) ->
36
      {ck with cdesc = 
37
       Pck_up (subst_ck ck_substs var_substs ck', k)}
38
  | Pck_down (ck',k) ->
39
      {ck with cdesc = 
40
       Pck_down (subst_ck ck_substs var_substs ck', k)}
41
  | Pck_phase (ck',q) ->
42
      {ck with cdesc = 
43
       Pck_phase (subst_ck ck_substs var_substs ck', q)}
30
    { ck with cdesc = Ctuple (List.map (subst_ck ck_substs var_substs) cklist) }
31
  | Con (ck', c) ->
32
    { ck with cdesc = Con (subst_ck ck_substs var_substs ck', c) }
33
  | Connot (ck', c) ->
34
    { ck with cdesc = Connot (subst_ck ck_substs var_substs ck', c) }
35
  | Pck_up (ck', k) ->
36
    { ck with cdesc = Pck_up (subst_ck ck_substs var_substs ck', k) }
37
  | Pck_down (ck', k) ->
38
    { ck with cdesc = Pck_down (subst_ck ck_substs var_substs ck', k) }
39
  | Pck_phase (ck', q) ->
40
    { ck with cdesc = Pck_phase (subst_ck ck_substs var_substs ck', q) }
44 41
  | Pck_const _ ->
45
      ck
46
  | Cvar _ | Cunivar _ ->
47
      begin
48
        try Hashtbl.find ck_substs ck with Not_found -> ck
49
      end
42
    ck
43
  | Cvar _ | Cunivar _ -> (
44
    try Hashtbl.find ck_substs ck with Not_found -> ck)
50 45
  | Clink ck' ->
51
      subst_ck ck_substs var_substs ck'
52
  | Ccarrying (_,ck') ->
53
      subst_ck ck_substs var_substs ck'
46
    subst_ck ck_substs var_substs ck'
47
  | Ccarrying (_, ck') ->
48
    subst_ck ck_substs var_substs ck'
54 49

  
55
(* [new_expr_instance ck_substs var_substs e edesc] returns a new
56
   "instance" of expressions [e] of expression [e], where [edesc] is the
57
   expanded version of [e]. *)
50
(* [new_expr_instance ck_substs var_substs e edesc] returns a new "instance" of
51
   expressions [e] of expression [e], where [edesc] is the expanded version of
52
   [e]. *)
58 53
let new_expr_instance ck_substs var_substs e edesc =
59
  {expr_tag = Utils.new_tag ();
60
   expr_desc = edesc;
61
   expr_type = e.expr_type;
62
   expr_clock = subst_ck ck_substs var_substs e.expr_clock;
63
   expr_delay = Delay.new_var ();
64
   expr_loc = e.expr_loc;
65
   expr_annot = e.expr_annot}
66
  
54
  {
55
    expr_tag = Utils.new_tag ();
56
    expr_desc = edesc;
57
    expr_type = e.expr_type;
58
    expr_clock = subst_ck ck_substs var_substs e.expr_clock;
59
    expr_delay = Delay.new_var ();
60
    expr_loc = e.expr_loc;
61
    expr_annot = e.expr_annot;
62
  }
63

  
67 64
let locals_cpt = ref 0
68 65

  
69 66
(* Returns a new local variable (for the main node) *)
70 67
let new_local vtyp vck vdd vloc =
71
  let vid = "_"^(string_of_int !locals_cpt) in
72
  locals_cpt := !locals_cpt+1;
73
  let ty_dec = {ty_dec_desc = Tydec_any; ty_dec_loc = vloc} in (* dummy *)
74
  let ck_dec = {ck_dec_desc = Ckdec_any; ck_dec_loc = vloc} in (* dummy *)
75
  {var_id = vid;
76
   var_orig = false;
77
   var_dec_type = ty_dec;
78
   var_dec_clock = ck_dec;
79
   var_dec_deadline = vdd;
80
   var_type = vtyp;
81
   var_clock = vck;
82
   var_loc = vloc}
68
  let vid = "_" ^ string_of_int !locals_cpt in
69
  locals_cpt := !locals_cpt + 1;
70
  let ty_dec = { ty_dec_desc = Tydec_any; ty_dec_loc = vloc } in
71
  (* dummy *)
72
  let ck_dec = { ck_dec_desc = Ckdec_any; ck_dec_loc = vloc } in
73
  (* dummy *)
74
  {
75
    var_id = vid;
76
    var_orig = false;
77
    var_dec_type = ty_dec;
78
    var_dec_clock = ck_dec;
79
    var_dec_deadline = vdd;
80
    var_type = vtyp;
81
    var_clock = vck;
82
    var_loc = vloc;
83
  }
83 84

  
84 85
(* Returns an expression correponding to variable v *)
85 86
let expr_of_var v =
86
  {expr_tag = Utils.new_tag ();
87
   expr_desc = Expr_ident v.var_id;
88
   expr_type = v.var_type;
89
   expr_clock = v.var_clock;
90
   expr_delay = Delay.new_var ();
91
   expr_loc = v.var_loc;
92
   expr_annot = None}
87
  {
88
    expr_tag = Utils.new_tag ();
89
    expr_desc = Expr_ident v.var_id;
90
    expr_type = v.var_type;
91
    expr_clock = v.var_clock;
92
    expr_delay = Delay.new_var ();
93
    expr_loc = v.var_loc;
94
    expr_annot = None;
95
  }
93 96

  
94
(* [build_ck_substs ck for_ck] computes the variable substitutions
95
   corresponding to the substitution of [ck] for [for_ck] *)
97
(* [build_ck_substs ck for_ck] computes the variable substitutions corresponding
98
   to the substitution of [ck] for [for_ck] *)
96 99
let build_ck_substs ck for_ck =
97 100
  let substs = Hashtbl.create 10 in
98 101
  let rec aux ck for_ck =
99 102
    let ck, for_ck = Clocks.repr ck, Clocks.repr for_ck in
100 103
    match ck.Clocks.cdesc, for_ck.Clocks.cdesc with
101 104
    | Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 ->
102
        List.iter2 aux cklist1 cklist2
105
      List.iter2 aux cklist1 cklist2
103 106
    | _, Clocks.Cunivar _ ->
104
        Hashtbl.add substs for_ck ck
105
    | _,_ ->
106
        ()
107
      Hashtbl.add substs for_ck ck
108
    | _, _ ->
109
      ()
107 110
  in
108 111
  aux ck for_ck;
109 112
  substs
......
111 114
(* Expands a list of expressions *)
112 115
let rec expand_list ck_substs var_substs elist =
113 116
  List.fold_right
114
    (fun e (eqs,locs,elist) ->
115
      let eqs',locs',e' = expand_expr ck_substs var_substs e in
116
      eqs'@eqs,locs'@locs,e'::elist)
117
    elist ([],[],[])
117
    (fun e (eqs, locs, elist) ->
118
      let eqs', locs', e' = expand_expr ck_substs var_substs e in
119
      eqs' @ eqs, locs' @ locs, e' :: elist)
120
    elist ([], [], [])
118 121

  
119 122
(* Expands the node instance [nd(args)]. *)
120 123
and expand_nodeinst parent_ck_substs parent_vsubsts nd args =
121 124
  (* Expand arguments *)
122 125
  let args_eqs, args_locs, args' =
123
    expand_expr parent_ck_substs parent_vsubsts args in
126
    expand_expr parent_ck_substs parent_vsubsts args
127
  in
124 128
  (* Compute clock substitutions to apply inside node's body *)
125 129
  let ck_ins = args'.expr_clock in
126
  let for_ck_ins,_ = Clocks.split_arrow nd.node_clock in
130
  let for_ck_ins, _ = Clocks.split_arrow nd.node_clock in
127 131
  let ck_substs = build_ck_substs ck_ins for_ck_ins in
128
  (* Compute variable substitutions to apply inside node's body, due
129
     to the transformation of node variables into local variables of the
130
     main node. *)
132
  (* Compute variable substitutions to apply inside node's body, due to the
133
     transformation of node variables into local variables of the main node. *)
131 134
  let var_substs = Hashtbl.create 10 in
132
  (* Add an equation in=arg for each node input + transform node input
133
     into a local variable of the main node *)
135
  (* Add an equation in=arg for each node input + transform node input into a
136
     local variable of the main node *)
134 137
  let eq_ins, loc_ins =
135 138
    List.split
136 139
      (List.map2
137 140
         (fun i e ->
138 141
           let i' =
139
             new_local i.var_type i.var_clock i.var_dec_deadline i.var_loc in
142
             new_local i.var_type i.var_clock i.var_dec_deadline i.var_loc
143
           in
140 144
           Hashtbl.add var_substs i.var_id i'.var_id;
141
           {eq_lhs = [i'.var_id];
142
            eq_rhs = e;
143
            eq_loc = i.var_loc}, i')
145
           { eq_lhs = [ i'.var_id ]; eq_rhs = e; eq_loc = i.var_loc }, i')
144 146
         nd.node_inputs (expr_list_of_expr args'))
145 147
  in
146
  (* Transform node local variables into local variables of the main
147
     node *)
148
  (* Transform node local variables into local variables of the main node *)
148 149
  let loc_sub =
149 150
    List.map
150 151
      (fun v ->
151
        let v' = new_local v.var_type v.var_clock v.var_dec_deadline v.var_loc in
152
        let v' =
153
          new_local v.var_type v.var_clock v.var_dec_deadline v.var_loc
154
        in
152 155
        Hashtbl.add var_substs v.var_id v'.var_id;
153 156
        v')
154 157
      nd.node_locals
155
  in  
158
  in
156 159
  (* Same for outputs *)
157 160
  let loc_outs =
158 161
    List.map
159 162
      (fun o ->
160
        let o' = new_local o.var_type o.var_clock o.var_dec_deadline o.var_loc in
163
        let o' =
164
          new_local o.var_type o.var_clock o.var_dec_deadline o.var_loc
165
        in
161 166
        Hashtbl.add var_substs o.var_id o'.var_id;
162 167
        o')
163 168
      nd.node_outputs
164
  in  
169
  in
165 170
  (* A tuple made of the node outputs will replace the node call in the parent
166 171
     node *)
167 172
  let eout = Expr_tuple (List.map expr_of_var loc_outs) in
168 173
  let new_eqs, new_locals = expand_eqs ck_substs var_substs nd.node_eqs in
169
  args_eqs@eq_ins@new_eqs,
170
  args_locs@loc_ins@loc_outs@loc_sub@new_locals,
171
  eout
174
  ( args_eqs @ eq_ins @ new_eqs,
175
    args_locs @ loc_ins @ loc_outs @ loc_sub @ new_locals,
176
    eout )
172 177

  
173 178
(* Expands an expression *)
174 179
and expand_expr ck_substs var_substs expr =
175 180
  match expr.expr_desc with
176 181
  | Expr_const cst ->
177
      [],[],new_expr_instance ck_substs var_substs expr expr.expr_desc
182
    [], [], new_expr_instance ck_substs var_substs expr expr.expr_desc
178 183
  | Expr_ident id ->
179
      let id' = subst_var var_substs id in
180
      let edesc = Expr_ident id' in
181
      [],[],new_expr_instance ck_substs var_substs expr edesc
184
    let id' = subst_var var_substs id in
185
    let edesc = Expr_ident id' in
186
    [], [], new_expr_instance ck_substs var_substs expr edesc
182 187
  | Expr_tuple elist ->
183
      let new_eqs,new_locals,exp_elist =
184
        expand_list ck_substs var_substs elist in
185
      new_eqs, new_locals,
186
      new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist)
187
  | Expr_fby (cst,e) ->
188
      let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
189
      let edesc = Expr_fby (cst, e') in
190
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
191
  | Expr_concat (cst,e) ->
192
      let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
193
      let edesc = Expr_concat (cst, e') in
194
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
188
    let new_eqs, new_locals, exp_elist =
189
      expand_list ck_substs var_substs elist
190
    in
191
    ( new_eqs,
192
      new_locals,
193
      new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist) )
194
  | Expr_fby (cst, e) ->
195
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
196
    let edesc = Expr_fby (cst, e') in
197
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
198
  | Expr_concat (cst, e) ->
199
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
200
    let edesc = Expr_concat (cst, e') in
201
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
195 202
  | Expr_tail e ->
196
      let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
197
      let edesc = Expr_tail e' in
198
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
199
  | Expr_when (e,c) ->
200
      let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
201
      let edesc = Expr_when (e',c) in
202
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
203
  | Expr_whennot (e,c) ->
204
      let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
205
      let edesc = Expr_whennot (e',c) in
206
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
207
  | Expr_merge (c,e1,e2) ->
208
      let new_eqs1,new_locals1, e1' = expand_expr ck_substs var_substs e1 in
209
      let new_eqs2,new_locals2, e2' = expand_expr ck_substs var_substs e2 in
210
      let edesc = Expr_merge (c,e1',e2') in
211
      new_eqs1@new_eqs2,
212
      new_locals1@new_locals2,
213
      new_expr_instance ck_substs var_substs expr edesc
214
  | Expr_appl (id, e, r) ->
215
      let decl = Hashtbl.find node_table id in
216
      begin
217
        match decl.top_decl_desc with
218
        | ImportedNode _ ->
219
            let new_eqs,new_locals, e' = expand_expr ck_substs var_substs e in
220
            let edesc = Expr_appl (id, e', r) in
221
            new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
222
        | Node nd ->
223
            let new_eqs, new_locals, outs =
224
              expand_nodeinst ck_substs var_substs nd e in
225
            new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs
226
        | Include _ | Consts _ | SensorDecl _ | ActuatorDecl _ -> failwith "Internal error expand_expr"
227
      end
228
  | Expr_uclock (e,k) ->
229
      let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
230
      let edesc = Expr_uclock (e',k) in
231
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
232
  | Expr_dclock (e,k) ->
203
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
204
    let edesc = Expr_tail e' in
205
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
206
  | Expr_when (e, c) ->
207
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
208
    let edesc = Expr_when (e', c) in
209
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
210
  | Expr_whennot (e, c) ->
211
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
212
    let edesc = Expr_whennot (e', c) in
213
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
214
  | Expr_merge (c, e1, e2) ->
215
    let new_eqs1, new_locals1, e1' = expand_expr ck_substs var_substs e1 in
216
    let new_eqs2, new_locals2, e2' = expand_expr ck_substs var_substs e2 in
217
    let edesc = Expr_merge (c, e1', e2') in
218
    ( new_eqs1 @ new_eqs2,
219
      new_locals1 @ new_locals2,
220
      new_expr_instance ck_substs var_substs expr edesc )
221
  | Expr_appl (id, e, r) -> (
222
    let decl = Hashtbl.find node_table id in
223
    match decl.top_decl_desc with
224
    | ImportedNode _ ->
233 225
      let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
234
      let edesc = Expr_dclock (e',k) in
226
      let edesc = Expr_appl (id, e', r) in
235 227
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
236
  | Expr_phclock (e,q) ->
237
      let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
238
      let edesc = Expr_phclock (e',q) in
239
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
240
  | Expr_pre _ | Expr_arrow _ -> assert false (* Not used in the Prelude part of the code *)
228
    | Node nd ->
229
      let new_eqs, new_locals, outs =
230
        expand_nodeinst ck_substs var_substs nd e
231
      in
232
      new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs
233
    | Include _ | Consts _ | SensorDecl _ | ActuatorDecl _ ->
234
      failwith "Internal error expand_expr")
235
  | Expr_uclock (e, k) ->
236
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
237
    let edesc = Expr_uclock (e', k) in
238
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
239
  | Expr_dclock (e, k) ->
240
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
241
    let edesc = Expr_dclock (e', k) in
242
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
243
  | Expr_phclock (e, q) ->
244
    let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
245
    let edesc = Expr_phclock (e', q) in
246
    new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
247
  | Expr_pre _ | Expr_arrow _ ->
248
    assert false
249
  (* Not used in the Prelude part of the code *)
241 250

  
242 251
(* Expands an equation *)
243 252
and expand_eq ck_substs var_substs eq =
244 253
  let new_eqs, new_locals, expr = expand_expr ck_substs var_substs eq.eq_rhs in
245 254
  let lhs' = List.map (subst_var var_substs) eq.eq_lhs in
246
  let eq' = {eq_lhs = lhs'; eq_rhs = expr; eq_loc = eq.eq_loc} in
255
  let eq' = { eq_lhs = lhs'; eq_rhs = expr; eq_loc = eq.eq_loc } in
247 256
  new_eqs, new_locals, eq'
248 257

  
249 258
(* Expands a set of equations *)
250 259
and expand_eqs ck_substs var_substs eqs =
251 260
  List.fold_left
252
    (fun (acc_eqs,acc_locals) eq ->
261
    (fun (acc_eqs, acc_locals) eq ->
253 262
      let new_eqs, new_locals, eq' = expand_eq ck_substs var_substs eq in
254
      (eq'::(new_eqs@acc_eqs)), (new_locals@acc_locals))
255
    ([],[]) eqs
263
      eq' :: (new_eqs @ acc_eqs), new_locals @ acc_locals)
264
    ([], []) eqs
256 265

  
257
(* Expands the body of a node, replacing recursively all the node calls
258
   it contains by the body of the corresponding node. *)
266
(* Expands the body of a node, replacing recursively all the node calls it
267
   contains by the body of the corresponding node. *)
259 268
let expand_node nd =
260 269
  let new_eqs, new_locals =
261
    expand_eqs (Hashtbl.create 10) (Hashtbl.create 10) nd.node_eqs in
262
  {node_id = nd.node_id;
263
   node_type = nd.node_type;
264
   node_clock = nd.node_clock;
265
   node_inputs = nd.node_inputs;
266
   node_outputs = nd.node_outputs;
267
   node_locals = new_locals@nd.node_locals;
268
   node_asserts = nd.node_asserts;
269
   node_eqs = new_eqs;
270
   node_spec = nd.node_spec;
271
   node_annot = nd.node_annot}
270
    expand_eqs (Hashtbl.create 10) (Hashtbl.create 10) nd.node_eqs
271
  in
272
  {
273
    node_id = nd.node_id;
274
    node_type = nd.node_type;
275
    node_clock = nd.node_clock;
276
    node_inputs = nd.node_inputs;
277
    node_outputs = nd.node_outputs;
278
    node_locals = new_locals @ nd.node_locals;
279
    node_asserts = nd.node_asserts;
280
    node_eqs = new_eqs;
281
    node_spec = nd.node_spec;
282
    node_annot = nd.node_annot;
283
  }
272 284

  
273 285
let expand_program () =
274
  if !Options.main_node = "" then
275
    raise (Corelang.Error No_main_specified);
286
  if !Options.main_node = "" then raise (Corelang.Error No_main_specified);
276 287
  let main =
277
    try
278
      Hashtbl.find node_table !Options.main_node
279
    with Not_found ->
280
      raise (Corelang.Error Main_not_found)
288
    try Hashtbl.find node_table !Options.main_node
289
    with Not_found -> raise (Corelang.Error Main_not_found)
281 290
  in
282 291
  match main.top_decl_desc with
283 292
  | Include _ | Consts _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ ->
284
      raise (Corelang.Error Main_wrong_kind)
293
    raise (Corelang.Error Main_wrong_kind)
285 294
  | Node nd ->
286
      expand_node nd
295
    expand_node nd
287 296

  
288 297
(* Local Variables: *)
289 298
(* compile-command:"make -C .." *)

Also available in: Unified diff