Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_export.ml @ 03c767b1

History | View | Annotate | Download (4.88 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 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 = (* memories *)
80
    match sw_init with
81
    | [] -> assert false
82
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
83
  in    
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
  let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
87
  let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
88
  let loc = Location.dummy_loc in
89
  let new_nd =
90
    { copy_nd with
91
    node_id = copy_nd.node_id ^ "_seal";
92
    node_locals = m.mmemory;
93
    node_stmts = [Eq
94
                    { eq_loc = loc;
95
                      eq_lhs = vl; 
96
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
97
                    };
98
                 Eq
99
                    { eq_loc = loc;
100
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
101
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
102
                    };
103
                 ];
104
    }
105
  in
106
  new_nd, orig_nd
107

    
108
  
109
let to_lustre basename prog m sw_init sw_step init_out update_out =
110
  let loc = Location.dummy_loc in
111
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
112
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
113
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
114

    
115
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
116

    
117
  (* Main output *)
118
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
119
  let new_top =
120
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
121
  in
122
  let out = open_out output_file in
123
  let fmt = Format.formatter_of_out_channel out in
124
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
125

    
126
  (* Verif output *)
127
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
128
  let out_verif = open_out output_file_verif in
129
  let fmt_verif = Format.formatter_of_out_channel out_verif in
130
  let check_nd = Lustre_utils.check_eq new_node orig_nd in
131
  let check_top =
132
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
133
  in
134
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top]);