Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/Ada/misc_lustre_function.ml
1

  
2 1
open Machine_code_types
3 2
open Lustre_types
4 3
open Corelang
5
(*
6
open Machine_code_common
7
*)
4
(* open Machine_code_common *)
8 5

  
9 6
let is_machine_statefull m = not m.mname.node_dec_stateless
10 7

  
11
(** Return true if its the arrow machine
12
   @param machine the machine to test
13
*)
8
(** Return true if its the arrow machine @param machine the machine to test *)
14 9
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
15 10

  
16
(** Extract a node from an instance.
17
   @param instance the instance
18
**)
11
(** Extract a node from an instance. @param instance the instance **)
19 12
let extract_node instance =
20
  let (_, (node, _)) = instance in
21
  match node.top_decl_desc with
22
    | Node nd         -> nd
23
    | _ -> assert false (*TODO*)
13
  let _, (node, _) = instance in
14
  match node.top_decl_desc with Node nd -> nd | _ -> assert false
15
(*TODO*)
24 16

  
25 17
(** Extract from a machine list the one corresponding to the given instance.
26
      assume that the machine is in the list.
27
   @param machines list of all machines
28
   @param instance instance of a machine
29
   @return the machine corresponding to hte given instance
30
**)
18
    assume that the machine is in the list. @param machines list of all machines
19
    @param instance instance of a machine @return the machine corresponding to
20
    hte given instance **)
31 21
let get_machine machines instance =
32
    let id = (extract_node instance).node_id in
33
    try
34
      List.find (function m -> m.mname.node_id=id) machines
35
    with
36
      Not_found -> assert false (*TODO*)
22
  let id = (extract_node instance).node_id in
23
  try List.find (function m -> m.mname.node_id = id) machines
24
  with Not_found -> assert false
25
(*TODO*)
37 26

  
38
(** Extract all the inputs and outputs.
39
   @param machine the machine
40
   @return a list of all the var_decl of a macine
41
**)
27
(** Extract all the inputs and outputs. @param machine the machine @return a
28
    list of all the var_decl of a macine **)
42 29
let get_all_vars_machine m =
43
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
30
  m.mmemory @ m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstatic
44 31

  
45
(** Check if a type is polymorphic.
46
   @param typ the type
47
   @return true if its polymorphic
48
**)
32
(** Check if a type is polymorphic. @param typ the type @return true if its
33
    polymorphic **)
49 34
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
50 35

  
51
(** Find all polymorphic type : Types.Tunivar in a machine.
52
   @param machine the machine
53
   @return a list of id corresponding to polymorphic type
54
**)
36
(** Find all polymorphic type : Types.Tunivar in a machine. @param machine the
37
    machine @return a list of id corresponding to polymorphic type **)
55 38
let find_all_polymorphic_type m =
56 39
  let vars = get_all_vars_machine m in
57 40
  let extract id = id.var_type.tid in
58 41
  let polymorphic_type_vars =
59
    List.filter (function x-> is_Tunivar x.var_type) vars in
60
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
61

  
42
    List.filter (function x -> is_Tunivar x.var_type) vars
43
  in
44
  List.sort_uniq ( - ) (List.map extract polymorphic_type_vars)
62 45

  
63
(** Check if a submachine is statefull.
64
    @param submachine a submachine
65
    @return true if the submachine is statefull
66
**)
46
(** Check if a submachine is statefull. @param submachine a submachine @return
47
    true if the submachine is statefull **)
67 48
let is_submachine_statefull submachine =
68
    not (snd (snd submachine)).mname.node_dec_stateless
49
  not (snd (snd submachine)).mname.node_dec_stateless
69 50

  
70
(** Find a submachine step call in a list of instructions.
71
    @param ident submachine instance ident
72
    @param instr_list List of instruction sto search
73
    @return a list of pair containing input types and output types for each step call found
74
**)
51
(** Find a submachine step call in a list of instructions. @param ident
52
    submachine instance ident @param instr_list List of instruction sto search
53
    @return a list of pair containing input types and output types for each step
54
    call found **)
75 55
let rec find_submachine_step_call ident instr_list =
76
  let search_instr instruction = 
56
  let search_instr instruction =
77 57
    match instruction.instr_desc with
78
      | MStep (il, i, vl) when String.equal i ident -> [
79
        (List.map (function x-> x.value_type) vl,
80
            List.map (function x-> x.var_type) il)]
81
      | MBranch (_, l) -> List.flatten
82
          (List.map (function _, y -> find_submachine_step_call ident y) l)
83
      | _ -> []
58
    | MStep (il, i, vl) when String.equal i ident ->
59
      [
60
        ( List.map (function x -> x.value_type) vl,
61
          List.map (function x -> x.var_type) il );
62
      ]
63
    | MBranch (_, l) ->
64
      List.flatten
65
        (List.map (function _, y -> find_submachine_step_call ident y) l)
66
    | _ ->
67
      []
84 68
  in
85 69
  List.flatten (List.map search_instr instr_list)
86 70

  
87 71
(* Replace this function by check_type_equal but be careful to the fact that
88
   this function chck equality and that it is both basic type.
89
   This might be a required feature when it used *)
90
(** Test if two types are the same.
91
   @param typ1 the first type
92
   @param typ2 the second type
93
**)
94
let pp_eq_type typ1 typ2 = 
95
  let get_basic typ = match (Types.repr typ).Types.tdesc with
96
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
97
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
98
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
99
    | _ -> assert false (*TODO*)
72
   this function chck equality and that it is both basic type. This might be a
73
   required feature when it used *)
74

  
75
(** Test if two types are the same. @param typ1 the first type @param typ2 the
76
    second type **)
77
let pp_eq_type typ1 typ2 =
78
  let get_basic typ =
79
    match (Types.repr typ).Types.tdesc with
80
    | Types.Tbasic Types.Basic.Tint ->
81
      Types.Basic.Tint
82
    | Types.Tbasic Types.Basic.Treal ->
83
      Types.Basic.Treal
84
    | Types.Tbasic Types.Basic.Tbool ->
85
      Types.Basic.Tbool
86
    | _ ->
87
      assert false
88
    (*TODO*)
100 89
  in
101 90
  get_basic typ1 = get_basic typ2
102 91

  
103
(** Check that two types are the same.
104
   @param t1 a type
105
   @param t2 an other type
106
   @param return true if the two types are Tbasic or Tunivar and equal
107
**)
108
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
92
(** Check that two types are the same. @param t1 a type @param t2 an other type
93
    @param return true if the two types are Tbasic or Tunivar and equal **)
94
let rec check_type_equal (t1 : Types.type_expr) (t2 : Types.type_expr) =
109 95
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
110
    | Types.Tbasic x, Types.Tbasic y -> x = y
111
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
112
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
113
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
114
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
115
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
116
    | _ -> assert false
96
  | Types.Tbasic x, Types.Tbasic y ->
97
    x = y
98
  | Types.Tunivar, Types.Tunivar ->
99
    t1.tid = t2.tid
100
  | Types.Ttuple l, _ ->
101
    assert (List.length l = 1);
102
    check_type_equal (List.hd l) t2
103
  | _, Types.Ttuple l ->
104
    assert (List.length l = 1);
105
    check_type_equal t1 (List.hd l)
106
  | Types.Tstatic (_, t), _ ->
107
    check_type_equal t t2
108
  | _, Types.Tstatic (_, t) ->
109
    check_type_equal t1 t
110
  | _ ->
111
    assert false
117 112

  
118
(** Extend a substitution to unify the two given types. Only the
119
  first type can be polymorphic.
120
    @param subsitution the base substitution
121
    @param type_poly the type which can be polymorphic
122
    @param typ the type to match type_poly with
123
**)
124
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
125
  assert(not (is_Tunivar typ));
113
(** Extend a substitution to unify the two given types. Only the first type can
114
    be polymorphic. @param subsitution the base substitution @param type_poly
115
    the type which can be polymorphic @param typ the type to match type_poly
116
    with **)
117
let unification (substituion : (int * Types.type_expr) list)
118
    ((type_poly : Types.type_expr), (typ : Types.type_expr)) =
119
  assert (not (is_Tunivar typ));
126 120
  (* If type_poly is polymorphic *)
127 121
  if is_Tunivar type_poly then
128 122
    (* If a subsitution exists for it *)
129
    if List.mem_assoc type_poly.tid substituion then
130
    begin
123
    if List.mem_assoc type_poly.tid substituion then (
131 124
      (* We check that the type corresponding to type_poly in the subsitution
132 125
         match typ *)
133
      (try
134
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
135
      with
136
        Not_found -> assert false);
126
      (try assert (check_type_equal (List.assoc type_poly.tid substituion) typ)
127
       with Not_found -> assert false);
137 128
      (* We return the original substituion, it is already correct *)
138 129
      substituion
139
    end
140
    (* If type_poly is not in the subsitution *)
141
    else
142
      (* We add it to the substituion *)
143
      (type_poly.tid, typ)::substituion
144
  (* iftype_poly is not polymorphic *)
145
  else
146
  begin
130
      (* If type_poly is not in the subsitution *))
131
    else (* We add it to the substituion *)
132
      (type_poly.tid, typ) :: substituion (* iftype_poly is not polymorphic *)
133
  else (
147 134
    (* We check that type_poly and typ are the same *)
148
    assert(check_type_equal type_poly typ);
135
    assert (check_type_equal type_poly typ);
149 136
    (* We return the original substituion, it is already correct *)
150
    substituion
151
  end
137
    substituion)
152 138

  
153
(** Check that two calls are equal. A call is
154
  a pair of list of types, the inputs and the outputs.
155
   @param calls a list of pair of list of types
156
   @param return true if the two pairs are equal
157
**)
139
(** Check that two calls are equal. A call is a pair of list of types, the
140
    inputs and the outputs. @param calls a list of pair of list of types @param
141
    return true if the two pairs are equal **)
158 142
let check_call_equal (i1, _) (i2, _) =
159
  (List.for_all2 check_type_equal i1 i2)
160
    && (List.for_all2 check_type_equal i1 i2)
143
  List.for_all2 check_type_equal i1 i2 && List.for_all2 check_type_equal i1 i2
161 144

  
162
(** Check that all the elements of list of calls are equal to one.
163
  A call is a pair of list of types, the inputs and the outputs.
164
   @param call a pair of list of types
165
   @param calls a list of pair of list of types
166
   @param return true if all the elements are equal
167
**)
168
let check_calls call calls =
169
  List.for_all (check_call_equal call) calls
145
(** Check that all the elements of list of calls are equal to one. A call is a
146
    pair of list of types, the inputs and the outputs. @param call a pair of
147
    list of types @param calls a list of pair of list of types @param return
148
    true if all the elements are equal **)
149
let check_calls call calls = List.for_all (check_call_equal call) calls
170 150

  
171 151
(** Extract from a subinstance that can have polymorphic type the instantiation
172 152
    of all its polymorphic type instanciation for a given machine. It searches
173
    the step calls and extract a substitution for all polymorphic type from
174
    it.
175
   @param machine the machine which instantiate the subinstance
176
   @param ident the identifier of the instance which permits to find the step call
177
   @param submachine the machine corresponding to the subinstance
178
   @return the correspondance between polymorphic type id and their instantiation
179
**)
153
    the step calls and extract a substitution for all polymorphic type from it.
154
    @param machine the machine which instantiate the subinstance @param ident
155
    the identifier of the instance which permits to find the step call @param
156
    submachine the machine corresponding to the subinstance @return the
157
    correspondance between polymorphic type id and their instantiation **)
180 158
let get_substitution machine ident submachine =
181 159
  (* extract the calls to submachines from the machine *)
182 160
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
183
  (* extract the first call  *)
184
  let call = match calls with
185
              (* assume that there is always one call to a subinstance *)
186
              | []    -> assert(false)
187
              | h::_  -> h in
161
  (* extract the first call *)
162
  let call =
163
    match calls with
164
    (* assume that there is always one call to a subinstance *)
165
    | [] ->
166
      assert false
167
    | h :: _ ->
168
      h
169
  in
188 170
  (* assume that all the calls to a subinstance are using the same type *)
189
  assert(check_calls call calls);
171
  assert (check_calls call calls);
190 172
  (* make a list of all types from input and output vars *)
191
  let call_types = (fst call)@(snd call) in
173
  let call_types = fst call @ snd call in
192 174
  (* extract all the input and output vars from the submachine *)
193
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
175
  let machine_vars =
176
    submachine.mstep.step_inputs @ submachine.mstep.step_outputs
177
  in
194 178
  (* keep only the type of vars *)
195
  let machine_types = List.map (function x-> x.var_type) machine_vars in
179
  let machine_types = List.map (function x -> x.var_type) machine_vars in
196 180
  (* assume that there is the same numer of input and output in the submachine
197
      and the call *)
181
     and the call *)
198 182
  assert (List.length machine_types = List.length call_types);
199 183
  (* Unify the two lists of types *)
200
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
201
  (* Assume that our substitution match all the possible
202
       polymorphic type of the node *)
184
  let substitution =
185
    List.fold_left unification [] (List.combine machine_types call_types)
186
  in
187
  (* Assume that our substitution match all the possible polymorphic type of the
188
     node *)
203 189
  let polymorphic_types = find_all_polymorphic_type submachine in
204 190
  assert (List.length polymorphic_types = List.length substitution);
205 191
  (try
206
    assert (List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
207
  with
208
    Not_found -> assert false);
192
     assert (
193
       List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
194
   with Not_found -> assert false);
209 195
  substitution
210 196

  
197
(** Extract from a machine the instance corresponding to the identifier, assume
198
    that the identifier exists in the instances of the machine.
211 199

  
212
(** Extract from a machine the instance corresponding to the identifier,
213
      assume that the identifier exists in the instances of the machine.
214

  
215
   @param identifier the instance identifier
216
   @param machine a machine
217
   @return the instance of machine.minstances corresponding to identifier
218
**)
200
    @param identifier the instance identifier @param machine a machine @return
201
    the instance of machine.minstances corresponding to identifier **)
219 202
let get_instance identifier typed_submachines =
220
  try
221
    List.assoc identifier typed_submachines
222
  with Not_found -> assert false
203
  try List.assoc identifier typed_submachines with Not_found -> assert false
223 204

  
224 205
(*Usefull for debug*)
225
let pp_type_debug fmt typ = 
226
  (match (Types.repr typ).Types.tdesc with
227
    | Types.Tbasic Types.Basic.Tint  -> Format.fprintf fmt "INTEGER"
228
    | Types.Tbasic Types.Basic.Treal -> Format.fprintf fmt "FLOAT"
229
    | Types.Tbasic Types.Basic.Tbool -> Format.fprintf fmt "BOOLEAN"
230
    | Types.Tunivar                  -> Format.fprintf fmt "POLY(%i)" typ.Types.tid
231
    | _ -> assert false
232
  )
206
let pp_type_debug fmt typ =
207
  match (Types.repr typ).Types.tdesc with
208
  | Types.Tbasic Types.Basic.Tint ->
209
    Format.fprintf fmt "INTEGER"
210
  | Types.Tbasic Types.Basic.Treal ->
211
    Format.fprintf fmt "FLOAT"
212
  | Types.Tbasic Types.Basic.Tbool ->
213
    Format.fprintf fmt "BOOLEAN"
214
  | Types.Tunivar ->
215
    Format.fprintf fmt "POLY(%i)" typ.Types.tid
216
  | _ ->
217
    assert false
233 218

  
234 219
let build_if g c1 i1 tl =
235
  let neg = c1=tag_false in
236
  let other = match tl with
237
    | []         -> None
238
    | [(_, i2)]  -> Some i2
239
    | _          -> assert false
220
  let neg = c1 = tag_false in
221
  let other =
222
    match tl with [] -> None | [ (_, i2) ] -> Some i2 | _ -> assert false
240 223
  in
241 224
  match neg, other with
242
    | true, Some x -> (false, g, x, Some i1)
243
    | _ ->
244
  (neg, g, i1, other)
225
  | true, Some x ->
226
    false, g, x, Some i1
227
  | _ ->
228
    neg, g, i1, other
245 229

  
246 230
let rec push_if_in_expr = function
247
  | [] -> []
248
  | instr::q ->
249
    (
250
      match get_instr_desc instr with
251
        | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
252
            let (_, g, instrs1, instrs2) = build_if g c1 i1 tl in
253
            let instrs1_pushed = push_if_in_expr instrs1 in
254
            let get_assign instr = match get_instr_desc instr with
255
              | MLocalAssign (id, value) -> (false, id, value)
256
              | MStateAssign (id, value) -> (true, id, value)
257
              | _ -> assert false
258
            in
259
            let gen_eq ident state value1 value2 =
260
              assert(check_type_equal ident.var_type value1.value_type);
261
              assert(check_type_equal ident.var_type value2.value_type);
262
              let value = {
263
                            value_desc   = Fun ("ite", [g;value1;value2]);
264
                            value_type   = ident.var_type;
265
                            value_annot  = None
266
                          }
267
              in
268
              let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
269
              { instr_desc = assign;
270
                lustre_eq  = None;
271
                instr_spec = []
272
              }
273
            in
274
            let mkval_var id = {
275
              value_desc   = Var id;
276
              value_type   = id.var_type;
277
              value_annot  = None
278
            }
279
            in
280
            let rec find_split s1 id1 accu = function
281
              | [] -> [], accu, mkval_var id1
282
              | (s2, id2, v2)::q when s1 = s2
283
                                  && id1.var_id = id2.var_id -> accu, q, v2
284
              | t::q -> find_split s1 id1 (t::accu) q
285
            in
286
            let gen_from_else l =
287
              List.map
288
                (fun (s2, id2, v2) -> gen_eq id2 s2 (mkval_var id2) v2)
289
                l
290
            in
291
            let rec gen_assigns if_assigns else_assigns =
292
              let res, accu_else = match if_assigns with
293
                | (s1, id1, v1)::q ->
294
                  let accu, remain, v2 = find_split s1 id1 [] else_assigns in
295
                  (gen_eq id1 s1 v1 v2)::(gen_assigns q remain), accu
296
                | [] -> [], else_assigns
297
              in
298
              (gen_from_else accu_else)@res
299
            in
300
            let if_assigns = List.map get_assign instrs1_pushed in
301
            let else_assigns = match instrs2 with
302
              | None -> []
303
              | Some instrs2 -> 
304
                  let instrs2_pushed = push_if_in_expr instrs2 in
305
                  List.map get_assign instrs2_pushed
306
            in
307
            gen_assigns if_assigns else_assigns
308
        | _ -> [instr]
309
      )@(push_if_in_expr q)
310

  
311

  
312

  
313

  
231
  | [] ->
232
    []
233
  | instr :: q ->
234
    (match get_instr_desc instr with
235
    | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
236
      let _, g, instrs1, instrs2 = build_if g c1 i1 tl in
237
      let instrs1_pushed = push_if_in_expr instrs1 in
238
      let get_assign instr =
239
        match get_instr_desc instr with
240
        | MLocalAssign (id, value) ->
241
          false, id, value
242
        | MStateAssign (id, value) ->
243
          true, id, value
244
        | _ ->
245
          assert false
246
      in
247
      let gen_eq ident state value1 value2 =
248
        assert (check_type_equal ident.var_type value1.value_type);
249
        assert (check_type_equal ident.var_type value2.value_type);
250
        let value =
251
          {
252
            value_desc = Fun ("ite", [ g; value1; value2 ]);
253
            value_type = ident.var_type;
254
            value_annot = None;
255
          }
256
        in
257
        let assign =
258
          if state then MStateAssign (ident, value)
259
          else MLocalAssign (ident, value)
260
        in
261
        { instr_desc = assign; lustre_eq = None; instr_spec = [] }
262
      in
263
      let mkval_var id =
264
        { value_desc = Var id; value_type = id.var_type; value_annot = None }
265
      in
266
      let rec find_split s1 id1 accu = function
267
        | [] ->
268
          [], accu, mkval_var id1
269
        | (s2, id2, v2) :: q when s1 = s2 && id1.var_id = id2.var_id ->
270
          accu, q, v2
271
        | t :: q ->
272
          find_split s1 id1 (t :: accu) q
273
      in
274
      let gen_from_else l =
275
        List.map (fun (s2, id2, v2) -> gen_eq id2 s2 (mkval_var id2) v2) l
276
      in
277
      let rec gen_assigns if_assigns else_assigns =
278
        let res, accu_else =
279
          match if_assigns with
280
          | (s1, id1, v1) :: q ->
281
            let accu, remain, v2 = find_split s1 id1 [] else_assigns in
282
            gen_eq id1 s1 v1 v2 :: gen_assigns q remain, accu
283
          | [] ->
284
            [], else_assigns
285
        in
286
        gen_from_else accu_else @ res
287
      in
288
      let if_assigns = List.map get_assign instrs1_pushed in
289
      let else_assigns =
290
        match instrs2 with
291
        | None ->
292
          []
293
        | Some instrs2 ->
294
          let instrs2_pushed = push_if_in_expr instrs2 in
295
          List.map get_assign instrs2_pushed
296
      in
297
      gen_assigns if_assigns else_assigns
298
    | _ ->
299
      [ instr ])
300
    @ push_if_in_expr q

Also available in: Unified diff