Project

General

Profile

Download (5.83 KB) Statistics
| Branch: | Tag: | Revision:
1
(* Multiple export channels for switched systems:
2
- lustre
3
- matlab
4
- text
5
 *)
6
open Lustrec
7
open Lustre_types
8
open Machine_code_types
9
open Seal_utils
10

    
11
let verbose = true
12

    
13
let process_sw vars f_e sw =
14
  let process_branch g_opt up =
15
    let el = List.map (fun (v,e) -> v, f_e e) up in
16
    (* Sorting list of elements, according to vars, safety check to
17
         ensure that no variable is forgotten. *)
18
    let el, forgotten = List.fold_right (fun v (res, remaining) ->
19
                            let vid = v.var_id in
20
                            if List.mem_assoc vid remaining then
21
                              ((List.assoc vid remaining)::res),
22
                              (List.remove_assoc vid remaining)
23
                            else (
24
                              Format.eprintf
25
                                "Looking for variable %s in remaining expressions: [%a]@."
26
                                vid
27
                                (Utils.fprintf_list ~sep:";@ "
28
                                   (fun fmt (id,e) ->
29
                                     Format.fprintf fmt
30
                                       "(%s -> %a)"
31
                                       id
32
                                       Printers.pp_expr e))
33
                                remaining;
34
                              assert false (* Missing variable v in list *)
35
                            )
36
                          ) vars ([], el)
37
    in
38
    assert (forgotten = []);
39
    let loc = (List.hd el).expr_loc in
40
    let new_e = Corelang.mkexpr loc (Expr_tuple el) in
41
    match g_opt with
42
      None -> None, new_e, loc
43
    | Some g ->
44
       let g = f_e g in
45
       let ee = Corelang.mkeexpr loc g in
46
       let new_e = if verbose then
47
                     {new_e with
48
                       expr_annot =
49
                         Some ({annots = [["seal";"guards"],ee];
50
                                annot_loc = loc})} else new_e 
51
       in
52
       Some g, new_e, loc
53
  in
54
  let rec process_sw f_e sw = 
55
    match sw with
56
    | [] -> assert false
57
    | [g_opt,up] -> ((* last case, no need to guard it *)
58
      let _, up_e, _ = process_branch g_opt up in
59
      up_e
60
    )
61
    | (g_opt,up)::tl ->
62
       let g_opt, up_e, loc = process_branch g_opt up in
63
       match g_opt with
64
       | None -> (
65
         Format.eprintf "SEAL issue: process_sw with %a"
66
           (pp_sys Printers.pp_expr) sw
67
       ;
68
         assert false (* How could this happen anyway ? *)
69
       )
70
       | Some g ->
71
          let tl_e = process_sw f_e tl in
72
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
73
  in
74
  process_sw f_e sw
75

    
76
    
77
let sw_to_lustre m sw_init sw_step init_out update_out =
78
  let orig_nd = m.mname in
79
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
80
  let vl = (* vl are memories *)
81
    match sw_init with
82
    | [] -> [] (* the system is stateless. Returning an empty list
83
                  shall do the job *) 
84
          
85
    | (gl, up)::_ ->
86
       List.map (fun (v,_) -> v) up
87
  in
88
  let loc = Location.dummy_loc in
89
  let mem_eq =
90
    if m.mmemory = [] then
91
      []
92
    else
93
      let e_init = process_sw m.mmemory (fun x -> x) sw_init in
94
      let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
95
      [Eq
96
         { eq_loc = loc;
97
           eq_lhs = vl; 
98
           eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
99
      }]
100
  in
101
  let output_eq =
102
    let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
103
    let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
104
    [ 
105
      Eq
106
        { eq_loc = loc;
107
          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
108
          eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
109
        };
110
    ]
111
  in
112
  let new_nd =
113
    { copy_nd with
114
      node_id = copy_nd.node_id ^ "_seal";
115
      node_locals = m.mmemory;
116
      node_stmts = mem_eq @ output_eq;
117
    }
118
  in
119
  new_nd, orig_nd
120

    
121
    
122
let funsw_to_lustre m update_out =
123
  let orig_nd = m.mname in
124
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
125
  let output_eq =
126
    let e_update_out = process_sw copy_nd.node_outputs  (fun x -> x) update_out in
127
    [ 
128
      Eq
129
        { eq_loc = Location.dummy_loc;
130
          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
131
          eq_rhs = e_update_out
132
        };
133
    ]
134
  in
135
  let new_nd =
136
    { copy_nd with
137
      node_id = copy_nd.node_id ^ "_seal";
138
      node_locals = [];
139
      node_stmts = output_eq;
140
    }
141
  in
142
  new_nd, orig_nd
143
  
144
  
145

    
146
let to_lustre basename prog new_node orig_node =
147
  let loc = Location.dummy_loc in
148
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
149
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
150

    
151
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
152

    
153
  (* Main output *)
154
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
155
  let new_top =
156
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
157
  in
158
  let out = open_out output_file in
159
  let fmt = Format.formatter_of_out_channel out in
160
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
161

    
162
  (* Verif output *)
163
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
164
  let out_verif = open_out output_file_verif in
165
  let fmt_verif = Format.formatter_of_out_channel out_verif in
166
  let check_nd = Lustre_utils.check_eq new_node orig_node in
167
  let check_top =
168
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
169
  in
170
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top])
171
  
172
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
173
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
174
  to_lustre basename prog new_node orig_nd
175

    
176
let fun_to_lustre basename prog m update_out =
177
  let new_node, orig_nd = funsw_to_lustre m update_out in
178
  to_lustre basename prog new_node orig_nd
179

    
(2-2/6)