Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_export.ml @ a0c92fa8

History | View | Annotate | Download (5.82 KB)

1
(* Multiple export channels for switched systems:
2
- lustre
3
- matlab
4
- text
5
 *)
6
open Lustre_types
7
open Machine_code_types
8
open Seal_utils
9

    
10
let verbose = true
11

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

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

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

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

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

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

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

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