Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

src/backends/Ada/misc_lustre_function.ml
1 1

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

  
9
let is_machine_statefull m = m.mmemory != [] || m.mcalls != []
9
let is_machine_statefull m = not m.mname.node_dec_stateless
10 10

  
11 11
(** Return true if its the arrow machine
12 12
   @param machine the machine to test
......
35 35
    with
36 36
      Not_found -> assert false (*TODO*)
37 37

  
38
(** Test if two types are the same.
39
   @param typ1 the first type
40
   @param typ2 the second type
41
**)
42
let pp_eq_type typ1 typ2 = 
43
  let get_basic typ = match (Types.repr typ).Types.tdesc with
44
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
45
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
46
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
47
    | _ -> assert false (*TODO*)
48
  in
49
  get_basic typ1 = get_basic typ2
50

  
51 38
(** Extract all the inputs and outputs.
52 39
   @param machine the machine
53 40
   @return a list of all the var_decl of a macine
......
97 84
  in
98 85
  List.flatten (List.map search_instr instr_list)
99 86

  
87
(* 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*)
100
  in
101
  get_basic typ1 = get_basic typ2
102

  
100 103
(** Check that two types are the same.
101 104
   @param t1 a type
102 105
   @param t2 an other type
......
218 221
    List.assoc identifier typed_submachines
219 222
  with Not_found -> assert false
220 223

  
224
(*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
  )
233

  
234
let build_if g c1 i1 tl =
235
  let neg = c1=tag_false in
236
  let other = match tl with
237
    | []         -> None
238
    | [(c2, i2)] -> Some i2
239
    | _          -> assert false
240
  in
241
  match neg, other with
242
    | true, Some x -> (false, g, x, Some i1)
243
    | _ ->
244
  (neg, g, i1, other)
245

  
246
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 (neg, 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
              }
272
            in
273
            let mkval_var id = {
274
                              value_desc   = Var id;
275
                              value_type   = id.var_type;
276
                              value_annot  = None
277
                            }
278
            in
279
            let rec find_split s1 id1 accu = function
280
              | [] -> [], accu, mkval_var id1
281
              | (s2, id2, v2)::q when s1 = s2
282
                                  && id1.var_id = id2.var_id -> accu, q, v2
283
              | t::q -> find_split s1 id1 (t::accu) q
284
            in
285
            let gen_from_else l =
286
              List.map
287
                (fun (s2, id2, v2) -> gen_eq id2 s2 (mkval_var id2) v2)
288
                l
289
            in
290
            let rec gen_assigns if_assigns else_assigns =
291
              let res, accu_else = match if_assigns with
292
                | (s1, id1, v1)::q ->
293
                  let accu, remain, v2 = find_split s1 id1 [] else_assigns in
294
                  (gen_eq id1 s1 v1 v2)::(gen_assigns q remain), accu
295
                | [] -> [], else_assigns
296
              in
297
              (gen_from_else accu_else)@res
298
            in
299
            let if_assigns = List.map get_assign instrs1_pushed in
300
            let else_assigns = match instrs2 with
301
              | None -> []
302
              | Some instrs2 -> 
303
                  let instrs2_pushed = push_if_in_expr instrs2 in
304
                  List.map get_assign instrs2_pushed
305
            in
306
            gen_assigns if_assigns else_assigns
307
        | x -> [instr]
308
      )@(push_if_in_expr q)
309

  
310

  
311

  
312

  

Also available in: Unified diff