Project

General

Profile

Download (5 KB) Statistics
| Branch: | Tag: | Revision:
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 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 to_lustre basename prog m sw_init sw_step init_out update_out =
122
  let loc = Location.dummy_loc in
123
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
124
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
125
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
126

    
127
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
128

    
129
  (* Main output *)
130
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
131
  let new_top =
132
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
133
  in
134
  let out = open_out output_file in
135
  let fmt = Format.formatter_of_out_channel out in
136
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
137

    
138
  (* Verif output *)
139
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
140
  let out_verif = open_out output_file_verif in
141
  let fmt_verif = Format.formatter_of_out_channel out_verif in
142
  let check_nd = Lustre_utils.check_eq new_node orig_nd in
143
  let check_top =
144
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
145
  in
146
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top]);
(1-1/5)