Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / expand.ml @ b38ffff3

History | View | Annotate | Download (10.8 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Clocks
13
open Corelang
14

    
15
(* Applies variable substitutions *)
16
let subst_var var_substs vid =
17
  try Hashtbl.find var_substs vid with Not_found -> vid
18

    
19
(* Applies clock substitutions *)
20
let rec subst_ck ck_substs var_substs ck =
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)}
26
  | 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)}
44
  | Pck_const _ ->
45
      ck
46
  | Cvar _ | Cunivar _ ->
47
      begin
48
        try Hashtbl.find ck_substs ck with Not_found -> ck
49
      end
50
  | Clink ck' ->
51
      subst_ck ck_substs var_substs ck'
52
  | Ccarrying (_,ck') ->
53
      subst_ck ck_substs var_substs ck'
54

    
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]. *)
58
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
  
67
let locals_cpt = ref 0
68

    
69
(* Returns a new local variable (for the main node) *)
70
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_dec_type = ty_dec;
77
   var_dec_clock = ck_dec;
78
   var_dec_deadline = vdd;
79
   var_type = vtyp;
80
   var_clock = vck;
81
   var_loc = vloc}
82

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

    
93
(* [build_ck_substs ck for_ck] computes the variable substitutions
94
   corresponding to the substitution of [ck] for [for_ck] *)
95
let build_ck_substs ck for_ck =
96
  let substs = Hashtbl.create 10 in
97
  let rec aux ck for_ck =
98
    let ck, for_ck = Clocks.repr ck, Clocks.repr for_ck in
99
    match ck.Clocks.cdesc, for_ck.Clocks.cdesc with
100
    | Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 ->
101
        List.iter2 aux cklist1 cklist2
102
    | _, Clocks.Cunivar _ ->
103
        Hashtbl.add substs for_ck ck
104
    | _,_ ->
105
        ()
106
  in
107
  aux ck for_ck;
108
  substs
109

    
110
(* Expands a list of expressions *)
111
let rec expand_list ck_substs var_substs elist =
112
  List.fold_right
113
    (fun e (eqs,locs,elist) ->
114
      let eqs',locs',e' = expand_expr ck_substs var_substs e in
115
      eqs'@eqs,locs'@locs,e'::elist)
116
    elist ([],[],[])
117

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

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

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

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

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

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

    
287
(* Local Variables: *)
288
(* compile-command:"make -C .." *)
289
(* End: *)