Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_export.ml @ b8dfc744

History | View | Annotate | Download (4.92 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

    
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 rec process_sw f_e sw =
32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> f_e e) up in
34
      let loc = (List.hd el).expr_loc in
35
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
36
      match g_opt with
37
        None -> None, new_e, loc
38
      | Some g ->
39
         let g = f_e g in
40
         let ee = Corelang.mkeexpr loc g in
41
         let new_e = if verbose then
42
           {new_e with
43
             expr_annot =
44
               Some ({annots = [["seal";"guards"],ee];
45
                      annot_loc = loc})} else new_e 
46
         in
47
         Some g, new_e, loc
48
    in
49
    match sw with
50
    | [] -> assert false
51
    | [g_opt,up] -> ((* last case, no need to guard it *)
52
      let _, up_e, _ = process_branch g_opt up in
53
      up_e
54
    )
55
    | (g_opt,up)::tl ->
56
       let g_opt, up_e, loc = process_branch g_opt up in
57
       match g_opt with
58
       | None -> assert false (* How could this happen anyway ? *)
59
       | Some g ->
60
          let tl_e = process_sw f_e tl in
61
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
62
  in
63
    
64
  let e_init = process_sw (fun x -> x) sw_init in
65
  let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in
66
  let e_init_out = process_sw (fun x -> x) init_out in
67
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
68
  let loc = Location.dummy_loc in
69
  let new_nd =
70
    { copy_nd with
71
    node_id = copy_nd.node_id ^ "_seal";
72
    node_locals = m.mmemory;
73
    node_stmts = [Eq
74
                    { eq_loc = loc;
75
                      eq_lhs = vl; 
76
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
77
                    };
78
                 Eq
79
                    { eq_loc = loc;
80
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
81
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
82
                    };
83
                 ];
84
    (*node_spec = Some (Contract contract);*)
85
                 
86
(*
87
                   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
88

    
89

    
90
                                                                                                                                                                                        ecrire une expression
91

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

    
94
                                                                                                                                                                                                                                                                                         Il faut aussi calculer la fonction de sortie
95

    
96
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
97
   *)    
98
    }
99
  in
100
  new_nd, orig_nd
101

    
102
  
103
let to_lustre basename prog m sw_init sw_step init_out update_out =
104
  let loc = Location.dummy_loc in
105
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
106
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
107
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
108

    
109
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
110

    
111
  (* Main output *)
112
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
113
  let new_top =
114
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
115
  in
116
  let out = open_out output_file in
117
  let fmt = Format.formatter_of_out_channel out in
118
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
119

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