Project

General

Profile

Download (5.42 KB) Statistics
| Branch: | Tag: | Revision:
1
(* Multiple export channels for switched systems: - lustre - matlab - text *)
2
open Lustre_types
3
open Machine_code_types
4
open Seal_utils
5

    
6
let verbose = true
7

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

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

    
119
let funsw_to_lustre m update_out =
120
  let orig_nd = m.mname in
121
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
122
  let output_eq =
123
    let e_update_out =
124
      process_sw copy_nd.node_outputs (fun x -> x) update_out
125
    in
126
    [
127
      Eq
128
        {
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
    {
137
      copy_nd with
138
      node_id = copy_nd.node_id ^ "_seal";
139
      node_locals = [];
140
      node_stmts = output_eq;
141
    }
142
  in
143
  new_nd, orig_nd
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 =
163
    !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus"
164
  in
165
  let out_verif = open_out output_file_verif in
166
  let fmt_verif = Format.formatter_of_out_channel out_verif in
167
  let check_nd = Lustre_utils.check_eq new_node orig_node in
168
  let check_top =
169
    Corelang.mktop_decl Location.dummy_loc output_file_verif false
170
      (Node check_nd)
171
  in
172
  Format.fprintf fmt_verif "%a@." Printers.pp_prog
173
    (prog @ [ new_top; check_top ])
174

    
175
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
176
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
177
  to_lustre basename prog new_node orig_nd
178

    
179
let fun_to_lustre basename prog m update_out =
180
  let new_node, orig_nd = funsw_to_lustre m update_out in
181
  to_lustre basename prog new_node orig_nd
(2-2/6)