Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/seal/seal_export.ml
1
(* Multiple export channels for switched systems:
2
- lustre
3
- matlab
4
- text
5
 *)
1
(* Multiple export channels for switched systems: - lustre - matlab - text *)
6 2
open Lustre_types
7 3
open Machine_code_types
8 4
open Seal_utils
......
11 7

  
12 8
let process_sw vars f_e sw =
13 9
  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)
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)
36 27
    in
37 28
    assert (forgotten = []);
38 29
    let loc = (List.hd el).expr_loc in
39 30
    let new_e = Corelang.mkexpr loc (Expr_tuple el) in
40 31
    match g_opt with
41
      None -> None, new_e, loc
32
    | None ->
33
      None, new_e, loc
42 34
    | 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
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
52 47
  in
53
  let rec process_sw f_e sw = 
48
  let rec process_sw f_e sw =
54 49
    match sw with
55
    | [] -> assert false
56
    | [g_opt,up] -> ((* last case, no need to guard it *)
50
    | [] ->
51
      assert false
52
    | [ (g_opt, up) ] ->
53
      (* last case, no need to guard it *)
57 54
      let _, up_e, _ = process_branch g_opt up in
58 55
      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)) 
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)))
72 66
  in
73 67
  process_sw f_e sw
74 68

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

  
120
    
121 119
let funsw_to_lustre m update_out =
122 120
  let orig_nd = m.mname in
123 121
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
124 122
  let output_eq =
125
    let e_update_out = process_sw copy_nd.node_outputs  (fun x -> x) update_out in
126
    [ 
123
    let e_update_out =
124
      process_sw copy_nd.node_outputs (fun x -> x) update_out
125
    in
126
    [
127 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
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;
131 132
        };
132 133
    ]
133 134
  in
134 135
  let new_nd =
135
    { copy_nd with
136
    {
137
      copy_nd with
136 138
      node_id = copy_nd.node_id ^ "_seal";
137 139
      node_locals = [];
138 140
      node_stmts = output_eq;
139 141
    }
140 142
  in
141 143
  new_nd, orig_nd
142
  
143
  
144 144

  
145 145
let to_lustre basename prog new_node orig_node =
146 146
  let loc = Location.dummy_loc in
......
156 156
  in
157 157
  let out = open_out output_file in
158 158
  let fmt = Format.formatter_of_out_channel out in
159
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
159
  Format.fprintf fmt "%a@." Printers.pp_prog [ new_top ];
160 160

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

  
171 175
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
172 176
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
173 177
  to_lustre basename prog new_node orig_nd
......
175 179
let fun_to_lustre basename prog m update_out =
176 180
  let new_node, orig_nd = funsw_to_lustre m update_out in
177 181
  to_lustre basename prog new_node orig_nd
178

  

Also available in: Unified diff