Project

General

Profile

Download (5.61 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

    
9
let verbose = true
10
            
11
let sw_to_lustre m sw_init sw_step init_out update_out =
12
  let orig_nd = m.mname in
13
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
14
  let vl = (* memories *)
15
    match sw_init with
16
    | [] -> assert false
17
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
18
  in
19
(*  let add_pre sw =
20
    List.map (fun (gl, up) ->
21
        List.map (fun (g,b) ->
22
            if not b then
23
              assert false (* should be guaranted by constrauction *)
24
            else
25
              add_pre_expr vl g) gl,
26
        List.map (fun (v,e) -> add_pre_expr vl e) up
27
      ) sw
28
  in
29
 *)
30
  
31
  let process_sw vars f_e sw =
32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> v, f_e e) up in
34
      (* Sorting list of elements, according to vars, safety check to
35
         ensure that no variable is forgotten. *)
36
      let el, forgotten = List.fold_right (fun v (res, remaining) ->
37
                   let vid = v.var_id in
38
                   if List.mem_assoc vid remaining then
39
                     ((List.assoc vid remaining)::res),
40
                     (List.remove_assoc vid remaining)
41
                   else
42
                     assert false (* Missing variable v in list *)
43
                            ) vars ([], el)
44
      in
45
      assert (forgotten = []);
46
      let loc = (List.hd el).expr_loc in
47
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
48
      match g_opt with
49
        None -> None, new_e, loc
50
      | Some g ->
51
         let g = f_e g in
52
         let ee = Corelang.mkeexpr loc g in
53
         let new_e = if verbose then
54
           {new_e with
55
             expr_annot =
56
               Some ({annots = [["seal";"guards"],ee];
57
                      annot_loc = loc})} else new_e 
58
         in
59
         Some g, new_e, loc
60
    in
61
    let rec process_sw f_e sw = 
62
      match sw with
63
    | [] -> assert false
64
    | [g_opt,up] -> ((* last case, no need to guard it *)
65
      let _, up_e, _ = process_branch g_opt up in
66
      up_e
67
    )
68
    | (g_opt,up)::tl ->
69
       let g_opt, up_e, loc = process_branch g_opt up in
70
       match g_opt with
71
       | None -> assert false (* How could this happen anyway ? *)
72
       | Some g ->
73
          let tl_e = process_sw f_e tl in
74
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
75
    in
76
    process_sw f_e sw
77
  in
78
    
79
  let e_init = process_sw m.mmemory (fun x -> x) sw_init in
80
  let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
81
  let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
82
  let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
83
  let loc = Location.dummy_loc in
84
  let new_nd =
85
    { copy_nd with
86
    node_id = copy_nd.node_id ^ "_seal";
87
    node_locals = m.mmemory;
88
    node_stmts = [Eq
89
                    { eq_loc = loc;
90
                      eq_lhs = vl; 
91
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
92
                    };
93
                 Eq
94
                    { eq_loc = loc;
95
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
96
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
97
                    };
98
                 ];
99
    (*node_spec = Some (Contract contract);*)
100
                 
101
(*
102
                   il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes
103

    
104

    
105
                                                                                                                                                                                        ecrire une expression
106

    
107
                                                                                                                                                                                        (mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2)
108

    
109
                                                                                                                                                                                                                                                                                         Il faut aussi calculer la fonction de sortie
110

    
111
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
112
   *)    
113
    }
114
  in
115
  new_nd, orig_nd
116

    
117
  
118
let to_lustre basename prog m sw_init sw_step init_out update_out =
119
  let loc = Location.dummy_loc in
120
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
121
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
122
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
123

    
124
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
125

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

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